Skip to content

Commit

Permalink
bump
Browse files Browse the repository at this point in the history
  • Loading branch information
Kaiyu Yang committed Oct 19, 2024
1 parent 880f820 commit bad1406
Show file tree
Hide file tree
Showing 4 changed files with 9 additions and 8 deletions.
1 change: 1 addition & 0 deletions LeanCopilot/Tactics.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ import LeanCopilot.Options
import LeanCopilot.Frontend
import Aesop.Util.Basic
import Batteries.Data.String.Basic
import Batteries.Data.String.Matcher

open Lean Meta Parser Elab Term Tactic

Expand Down
8 changes: 4 additions & 4 deletions lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -5,20 +5,20 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f",
"rev": "1e0bf50b357069e1d658512a579a5faac6587c40",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f",
"inputRev": null,
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
"scope": "",
"rev": "deb279eb7be16848d0bc8387f80d6e41bcdbe738",
"rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "deb279eb7be16848d0bc8387f80d6e41bcdbe738",
"inputRev": null,
"inherited": false,
"configFile": "lakefile.toml"}],
"name": "LeanCopilot",
Expand Down
6 changes: 3 additions & 3 deletions lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -303,8 +303,8 @@ extern_lib libleanffi pkg := do
buildStaticLib (pkg.nativeLibDir / name) #[ct2O]


require batteries from git "https://github.com/leanprover-community/batteries.git" @ "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f" -- Lean v4.11.0
require aesop from git "https://github.com/leanprover-community/aesop" @ "deb279eb7be16848d0bc8387f80d6e41bcdbe738" -- Lean v4.11.0
require batteries from git "https://github.com/leanprover-community/batteries.git"
require aesop from git "https://github.com/leanprover-community/aesop"

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" @ "e490631b72a43a6a82b4ddd3a2d020b2029491d0" -- Lean v4.11.0
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4"
2 changes: 1 addition & 1 deletion lean-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:v4.11.0
leanprover/lean4:v4.13.0-rc3

0 comments on commit bad1406

Please sign in to comment.