diff --git a/lake-manifest.json b/lake-manifest.json index 836242b..6106804 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,20 +15,20 @@ "type": "git", "subDir": null, "scope": "", - "rev": "5a0ec8588855265ade536f35bcdcf0fb24fd6030", + "rev": "79402ad9ab4be9a2286701a9880697e2351e4955", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", + "inputRev": "master", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "", - "rev": "8d6c853f11a5172efa0e96b9f2be1a83d861cdd9", + "rev": "8ce422eb59adf557fac184f8b1678c75fa03075c", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", + "inputRev": "v4.16.0-rc1", "inherited": true, "configFile": "lakefile.toml"}], "name": "TensorLib", diff --git a/lakefile.lean b/lakefile.lean index babbe24..913da0f 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -11,14 +11,8 @@ lean_lib «TensorLib» where lean_exe "tensorlib" where root := `Main --- require aesop from git --- "https://github.com/leanprover-community/aesop" @ "v4.15.0-rc1" - --- require Cli from git --- "https://github.com/seanmcl/lean4-cli.git" @ "v4.15.0-rc1" - require aesop from git - "https://github.com/leanprover-community/aesop" @ "v4.14.0" + "https://github.com/leanprover-community/aesop" @ "master" -- 'master' rather than a tag is a workaround for segfault bug https://github.com/leanprover/lean4/issues/6518#issuecomment-2574607960 require Cli from git "https://github.com/leanprover/lean4-cli.git" @ "v2.2.0-lv4.14.0-rc1" diff --git a/lean-toolchain b/lean-toolchain index 1e70935..d0eb99f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0 +leanprover/lean4:v4.15.0