attempt: fix workflow

scripts/add-copilot.sh

@@ -1,18 +0,0 @@
-#!/usr/bin/env bash
-
-
-cp ./scripts/copilot_lakefile.txt lakefile.lean
-
-lake update LeanCopilot 
-
-lake exe LeanCopilot/download
-
-lake build 
-
-echo ".........................................................................."
-echo "Please do not push changes to the following files: 
-     - lakefile.lean
-     - .lake/lakefile.olean
-     - .lake/lakefile.olean.trace
-     - lake-manifest.json
-Please ensure that there are no 'import LeanCopilot' statements in the lean files."

scripts/check_file_imports.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import Lean
-import Batteries.Lean.HashSet
 import HepLean
 /-!
 

scripts/copilot_lakefile.txt

@@ -1,23 +0,0 @@
-import Lake
-open Lake DSL
-
-package «hep_lean» {
-  -- add any package configuration options here
-}
-
-require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"
-
-@[default_target]
-lean_lib «HepLean» {
-  -- add any library configuration options here
-  moreLinkArgs := #[
-    "-L./.lake/packages/LeanCopilot/.lake/build/lib",
-    "-lctranslate2"
-  ]
-}
-
-meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
-require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
-
-require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v1.2.1"