Merge pull request #94 from lean-dojo/peiyang

Bump to Lean v4.10.0-rc1

lake-manifest.json

@@ -1,22 +1,24 @@
-{"version": "1.0.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries.git",
    "type": "git",
    "subDir": null,
-   "rev": "73c7f46f4c0eaa48e9538c9fd108d3ee5524868a",
+   "scope": "",
+   "rev": "2ead90d24b4fac3a05c9c4294daa39bd8686fb98",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "73c7f46f4c0eaa48e9538c9fd108d3ee5524868a",
+   "inputRev": "2ead90d24b4fac3a05c9c4294daa39bd8686fb98",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "f465af4466eeb1f195692745fd58bb3f552692f1",
+   "scope": "",
+   "rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "f465af4466eeb1f195692745fd58bb3f552692f1",
+   "inputRev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "LeanCopilot",

lakefile.lean

@@ -285,7 +285,7 @@ def buildCpp (pkg : Package) (path : FilePath) (dep : BuildJob FilePath) : Spawn
   let flags := #["-fPIC", "-std=c++17", optLevel]
   let args := flags ++ #["-I", (← getLeanIncludeDir).toString, "-I", (pkg.buildDir / "include").toString]
   let oFile := pkg.buildDir / (path.withExtension "o")
-  let srcJob ← inputFile <| pkg.dir / path
+  let srcJob ← inputTextFile <| pkg.dir / path
   buildFileAfterDepList oFile [srcJob, dep] (extraDepTrace := computeHash flags) fun deps =>
     compileO oFile deps[0]! args "c++"
 
@@ -302,8 +302,8 @@ extern_lib libleanffi pkg := do
   buildStaticLib (pkg.nativeLibDir / name) #[ct2O]
 
 
-require batteries from git "https://github.com/leanprover-community/batteries.git" @ "54bb04c3119f24fde14b9068c4b2e69db52a1450" -- Lean v4.9.0
-require aesop from git "https://github.com/leanprover-community/aesop" @ "06cca4bd36b2af743d4858c5cc31604aa9da26bc" -- Lean v4.9.0
+require batteries from git "https://github.com/leanprover-community/batteries.git" @ "2ead90d24b4fac3a05c9c4294daa39bd8686fb98" -- Lean v4.10.0-rc1
+require aesop from git "https://github.com/leanprover-community/aesop" @ "a64fe24aa94e21404940e9217363a9a1ed9a33a6" -- Lean v4.10.0-rc1
 
 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" @ "1daa0de7eea6bf8d3e1b0814156ede21a8a9e9e9" -- Lean v4.9.0
+require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "c369436d21c583a60da62d4513c7b9ea08389074" -- Lean v4.10.0-rc1

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.9.0
+leanprover/lean4:v4.10.0-rc1

scripts/unpickle_premises.py

@@ -3,7 +3,7 @@
 import numpy as np
 
 
-# indexed_corpurs.pickle is produced by retrieval/index.py in [ReProver](https://github.com/lean-dojo/ReProver).
+# `indexed_corpurs.pickle` is produced by `retrieval/index.py` in [ReProver](https://github.com/lean-dojo/ReProver).
 indexed_corpus = pickle.load(open("indexed_corpus.pickle", "rb"))
 
 embeddings_tensor = indexed_corpus.embeddings