aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 4 Packages Projects Releases Wiki Activity

chore: Update Pantograph and Lean version to 4.12

This commit is contained in:
Leni Aniva 2024-10-06 22:04:10 -07:00
parent 1ecfa35e1c
commit 034fd458e3
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
8 changed files with 52 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
examples/Example/lake-manifest.json
View File

@ -5,7 +5,7 @@
"type": "git", "type": "git",
"subDir": null, "subDir": null,
"scope": "", "scope": "",
"rev": "2ead90d24b4fac3a05c9c4294daa39bd8686fb98", "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
"name": "batteries", "name": "batteries",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "main", "inputRev": "main",
@ -15,10 +15,10 @@
"type": "git", "type": "git",
"subDir": null, "subDir": null,
"scope": "", "scope": "",
"rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6", "rev": "28fa80508edc97d96ed6342c9a771a67189e0baa",
"name": "aesop", "name": "aesop",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "v4.10.0-rc1", "inputRev": "v4.12.0",
"inherited": false, "inherited": false,
"configFile": "lakefile.toml"}], "configFile": "lakefile.toml"}],
"name": "Example", "name": "Example",

2
examples/Example/lakefile.lean
View File

@ -2,7 +2,7 @@ import Lake
open Lake DSL open Lake DSL
require aesop from git 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 package Example

2
examples/all.ipynb
View File

@ -232,7 +232,7 @@
"output_type": "stream", "output_type": "stream",
"text": [ "text": [
"$PWD: /home/aniva/Projects/atp/PyPantograph/examples/Example\n", "$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"
] ]
} }
], ],

32
experiments/dsp/lean_src_proj/lake-manifest.json
View File

@ -5,7 +5,7 @@
"type": "git", "type": "git",
"subDir": null, "subDir": null,
"scope": "", "scope": "",
"rev": "2ead90d24b4fac3a05c9c4294daa39bd8686fb98", "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
"name": "batteries", "name": "batteries",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "main", "inputRev": "main",
@ -15,17 +15,17 @@
"type": "git", "type": "git",
"subDir": null, "subDir": null,
"scope": "", "scope": "",
"rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6", "rev": "28fa80508edc97d96ed6342c9a771a67189e0baa",
"name": "aesop", "name": "aesop",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "v4.10.0-rc1", "inputRev": "v4.12.0",
"inherited": false, "inherited": false,
"configFile": "lakefile.toml"}, "configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/quote4", {"url": "https://github.com/leanprover-community/quote4",
"type": "git", "type": "git",
"subDir": null, "subDir": null,
"scope": "leanprover-community", "scope": "leanprover-community",
"rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
"name": "Qq", "name": "Qq",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "master", "inputRev": "master",
@ -35,40 +35,50 @@
"type": "git", "type": "git",
"subDir": null, "subDir": null,
"scope": "leanprover-community", "scope": "leanprover-community",
"rev": "d1b33202c3a29a079f292de65ea438648123b635", "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
"name": "proofwidgets", "name": "proofwidgets",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "v0.0.39", "inputRev": "v0.0.42",
"inherited": true, "inherited": true,
"configFile": "lakefile.lean"}, "configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/lean4-cli", {"url": "https://github.com/leanprover/lean4-cli",
"type": "git", "type": "git",
"subDir": null, "subDir": null,
"scope": "", "scope": "",
"rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
"name": "Cli", "name": "Cli",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "main", "inputRev": "main",
"inherited": true, "inherited": true,
"configFile": "lakefile.lean"}, "configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/import-graph", {"url": "https://github.com/leanprover-community/import-graph",
"type": "git", "type": "git",
"subDir": null, "subDir": null,
"scope": "leanprover-community", "scope": "leanprover-community",
"rev": "d366a602cc4a325a6f9db3a3991dfa6d6cf409c5", "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1",
"name": "importGraph", "name": "importGraph",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "main", "inputRev": "main",
"inherited": true, "inherited": true,
"configFile": "lakefile.toml"}, "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", {"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git", "type": "git",
"subDir": null, "subDir": null,
"scope": "", "scope": "",
"rev": "f5c3f06aa7f6d6c221786d2890c345a00e6341f8", "rev": "809c3fb3b5c8f5d7dace56e200b426187516535a",
"name": "mathlib", "name": "mathlib",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "v4.10.0-rc1", "inputRev": "v4.12.0",
"inherited": false, "inherited": false,
"configFile": "lakefile.lean"}], "configFile": "lakefile.lean"}],
"name": "LeanSrcProj", "name": "LeanSrcProj",

4
experiments/dsp/lean_src_proj/lakefile.lean
View File

@ -3,9 +3,9 @@ open Lake DSL
require aesop from git 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 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 package LeanSrcProj
@[default_target] @[default_target]

32
experiments/minif2f/MiniF2F/lake-manifest.json
View File

@ -5,7 +5,7 @@
"type": "git", "type": "git",
"subDir": null, "subDir": null,
"scope": "", "scope": "",
"rev": "2ead90d24b4fac3a05c9c4294daa39bd8686fb98", "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
"name": "batteries", "name": "batteries",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "main", "inputRev": "main",
@ -15,17 +15,17 @@
"type": "git", "type": "git",
"subDir": null, "subDir": null,
"scope": "", "scope": "",
"rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6", "rev": "28fa80508edc97d96ed6342c9a771a67189e0baa",
"name": "aesop", "name": "aesop",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "v4.10.0-rc1", "inputRev": "v4.12.0",
"inherited": false, "inherited": false,
"configFile": "lakefile.toml"}, "configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/quote4", {"url": "https://github.com/leanprover-community/quote4",
"type": "git", "type": "git",
"subDir": null, "subDir": null,
"scope": "leanprover-community", "scope": "leanprover-community",
"rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
"name": "Qq", "name": "Qq",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "master", "inputRev": "master",
@ -35,40 +35,50 @@
"type": "git", "type": "git",
"subDir": null, "subDir": null,
"scope": "leanprover-community", "scope": "leanprover-community",
"rev": "d1b33202c3a29a079f292de65ea438648123b635", "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
"name": "proofwidgets", "name": "proofwidgets",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "v0.0.39", "inputRev": "v0.0.42",
"inherited": true, "inherited": true,
"configFile": "lakefile.lean"}, "configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/lean4-cli", {"url": "https://github.com/leanprover/lean4-cli",
"type": "git", "type": "git",
"subDir": null, "subDir": null,
"scope": "", "scope": "",
"rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
"name": "Cli", "name": "Cli",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "main", "inputRev": "main",
"inherited": true, "inherited": true,
"configFile": "lakefile.lean"}, "configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/import-graph", {"url": "https://github.com/leanprover-community/import-graph",
"type": "git", "type": "git",
"subDir": null, "subDir": null,
"scope": "leanprover-community", "scope": "leanprover-community",
"rev": "d366a602cc4a325a6f9db3a3991dfa6d6cf409c5", "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1",
"name": "importGraph", "name": "importGraph",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "main", "inputRev": "main",
"inherited": true, "inherited": true,
"configFile": "lakefile.toml"}, "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", {"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git", "type": "git",
"subDir": null, "subDir": null,
"scope": "", "scope": "",
"rev": "f5c3f06aa7f6d6c221786d2890c345a00e6341f8", "rev": "809c3fb3b5c8f5d7dace56e200b426187516535a",
"name": "mathlib", "name": "mathlib",
"manifestFile": "lake-manifest.json", "manifestFile": "lake-manifest.json",
"inputRev": "v4.10.0-rc1", "inputRev": "v4.12.0",
"inherited": false, "inherited": false,
"configFile": "lakefile.lean"}], "configFile": "lakefile.lean"}],
"name": "MiniF2F", "name": "MiniF2F",

4
experiments/minif2f/MiniF2F/lakefile.lean
View File

@ -2,9 +2,9 @@ import Lake
open Lake DSL open Lake DSL
require aesop from git 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 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 package MiniF2F

2
src

@ -1 +1 @@
Subproject commit d0321e72ddb477a5eea1ebee346c5ee00512d22e Subproject commit c3494edc750f776689d25c0cd59a3b718583145a