From a896e65f693a008c6d8721db83c5fb16b0457e84 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 6 Oct 2024 22:04:10 -0700 Subject: [PATCH 1/2] chore: Update Pantograph and Lean version to 4.12 --- examples/Example/lake-manifest.json | 6 ++-- examples/Example/lakefile.lean | 2 +- examples/all.ipynb | 2 +- .../dsp/lean_src_proj/lake-manifest.json | 32 ++++++++++++------- experiments/dsp/lean_src_proj/lakefile.lean | 4 +-- .../minif2f/MiniF2F/lake-manifest.json | 32 ++++++++++++------- experiments/minif2f/MiniF2F/lakefile.lean | 4 +-- src | 2 +- 8 files changed, 52 insertions(+), 32 deletions(-) diff --git a/examples/Example/lake-manifest.json b/examples/Example/lake-manifest.json index 2199727..fe0adeb 100644 --- a/examples/Example/lake-manifest.json +++ b/examples/Example/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "2ead90d24b4fac3a05c9c4294daa39bd8686fb98", + "rev": "4756e0fc48acce0cc808df0ad149de5973240df6", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,10 +15,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6", + "rev": "28fa80508edc97d96ed6342c9a771a67189e0baa", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.10.0-rc1", + "inputRev": "v4.12.0", "inherited": false, "configFile": "lakefile.toml"}], "name": "Example", diff --git a/examples/Example/lakefile.lean b/examples/Example/lakefile.lean index 8759d91..a85cd79 100644 --- a/examples/Example/lakefile.lean +++ b/examples/Example/lakefile.lean @@ -2,7 +2,7 @@ import Lake open Lake DSL require aesop from git - "https://github.com/leanprover-community/aesop.git" @ "v4.10.0-rc1" + "https://github.com/leanprover-community/aesop.git" @ "v4.12.0" package Example diff --git a/examples/all.ipynb b/examples/all.ipynb index 21e668e..8195cd4 100644 --- a/examples/all.ipynb +++ b/examples/all.ipynb @@ -232,7 +232,7 @@ "output_type": "stream", "text": [ "$PWD: /home/aniva/Projects/atp/PyPantograph/examples/Example\n", - "$LEAN_PATH: b'././.lake/packages/batteries/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/build/lib:/home/aniva/.elan/toolchains/leanprover--lean4---v4.10.0-rc1/lib/lean\\n'\n" + "$LEAN_PATH: b'././.lake/packages/batteries/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/build/lib:/home/aniva/.elan/toolchains/leanprover--lean4---v4.12/lib/lean\\n'\n" ] } ], diff --git a/experiments/dsp/lean_src_proj/lake-manifest.json b/experiments/dsp/lean_src_proj/lake-manifest.json index c0d830c..0f19392 100644 --- a/experiments/dsp/lean_src_proj/lake-manifest.json +++ b/experiments/dsp/lean_src_proj/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "2ead90d24b4fac3a05c9c4294daa39bd8686fb98", + "rev": "4756e0fc48acce0cc808df0ad149de5973240df6", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,17 +15,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6", + "rev": "28fa80508edc97d96ed6342c9a771a67189e0baa", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.10.0-rc1", + "inputRev": "v4.12.0", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", + "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,40 +35,50 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d1b33202c3a29a079f292de65ea438648123b635", + "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.39", + "inputRev": "v0.0.42", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "", - "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", + "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d366a602cc4a325a6f9db3a3991dfa6d6cf409c5", + "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "2ba60fa2c384a94735454db11a2d523612eaabff", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "f5c3f06aa7f6d6c221786d2890c345a00e6341f8", + "rev": "809c3fb3b5c8f5d7dace56e200b426187516535a", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.10.0-rc1", + "inputRev": "v4.12.0", "inherited": false, "configFile": "lakefile.lean"}], "name": "LeanSrcProj", diff --git a/experiments/dsp/lean_src_proj/lakefile.lean b/experiments/dsp/lean_src_proj/lakefile.lean index ecc34f5..7e2f4ad 100644 --- a/experiments/dsp/lean_src_proj/lakefile.lean +++ b/experiments/dsp/lean_src_proj/lakefile.lean @@ -3,9 +3,9 @@ open Lake DSL require aesop from git - "https://github.com/leanprover-community/aesop.git" @ "v4.10.0-rc1" + "https://github.com/leanprover-community/aesop.git" @ "v4.12.0" require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" @ "v4.10.0-rc1" + "https://github.com/leanprover-community/mathlib4.git" @ "v4.12.0" package LeanSrcProj @[default_target] diff --git a/experiments/minif2f/MiniF2F/lake-manifest.json b/experiments/minif2f/MiniF2F/lake-manifest.json index b0a5048..b25b1ce 100644 --- a/experiments/minif2f/MiniF2F/lake-manifest.json +++ b/experiments/minif2f/MiniF2F/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "2ead90d24b4fac3a05c9c4294daa39bd8686fb98", + "rev": "4756e0fc48acce0cc808df0ad149de5973240df6", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,17 +15,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6", + "rev": "28fa80508edc97d96ed6342c9a771a67189e0baa", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.10.0-rc1", + "inputRev": "v4.12.0", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", + "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,40 +35,50 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d1b33202c3a29a079f292de65ea438648123b635", + "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.39", + "inputRev": "v0.0.42", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "", - "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", + "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d366a602cc4a325a6f9db3a3991dfa6d6cf409c5", + "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "2ba60fa2c384a94735454db11a2d523612eaabff", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "f5c3f06aa7f6d6c221786d2890c345a00e6341f8", + "rev": "809c3fb3b5c8f5d7dace56e200b426187516535a", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.10.0-rc1", + "inputRev": "v4.12.0", "inherited": false, "configFile": "lakefile.lean"}], "name": "MiniF2F", diff --git a/experiments/minif2f/MiniF2F/lakefile.lean b/experiments/minif2f/MiniF2F/lakefile.lean index f5ec5eb..eb1f3a8 100644 --- a/experiments/minif2f/MiniF2F/lakefile.lean +++ b/experiments/minif2f/MiniF2F/lakefile.lean @@ -2,9 +2,9 @@ import Lake open Lake DSL require aesop from git - "https://github.com/leanprover-community/aesop.git" @ "v4.10.0-rc1" + "https://github.com/leanprover-community/aesop.git" @ "v4.12.0" require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" @ "v4.10.0-rc1" + "https://github.com/leanprover-community/mathlib4.git" @ "v4.12.0" package MiniF2F diff --git a/src b/src index d0321e7..c3494ed 160000 --- a/src +++ b/src @@ -1 +1 @@ -Subproject commit d0321e72ddb477a5eea1ebee346c5ee00512d22e +Subproject commit c3494edc750f776689d25c0cd59a3b718583145a From 2075a58661f126cdc4efd8e2018c5b7b606d8bb7 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 8 Oct 2024 00:18:39 -0700 Subject: [PATCH 2/2] chore: Update to REPL version with error handling --- src | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src b/src index c3494ed..5e776a1 160000 --- a/src +++ b/src @@ -1 +1 @@ -Subproject commit c3494edc750f776689d25c0cd59a3b718583145a +Subproject commit 5e776a1b49e02e5ecc75d7011ac488fcc2b514ce