Skip to content

Commit

Permalink
chore: Use lean v4.4.0
Browse files Browse the repository at this point in the history
  • Loading branch information
Anderssorby committed Dec 26, 2023
1 parent 8fe9efe commit 51bb1ba
Show file tree
Hide file tree
Showing 4 changed files with 45 additions and 38 deletions.
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
/build
/lake-packages
/.lake

# Ignore nix stuff, just in case?
/result
74 changes: 40 additions & 34 deletions lake-manifest.json
Original file line number Diff line number Diff line change
@@ -1,35 +1,41 @@
{"version": 5,
"packagesDir": "lake-packages",
{"version": 7,
"packagesDir": ".lake/packages",
"packages":
[{"git":
{"url": "https://github.com/lurk-lab/YatimaStdLib.lean",
"subDir?": null,
"rev": "5b64c5150e371fb280728cbb5b7c225b9c96b348",
"opts": {},
"name": "YatimaStdLib",
"inputRev?": "5b64c5150e371fb280728cbb5b7c225b9c96b348",
"inherited": false}},
{"git":
{"url": "https://github.com/lurk-lab/straume",
"subDir?": null,
"rev": "053d9feccbface9a0b2c1a72447914376aac74ea",
"opts": {},
"name": "Straume",
"inputRev?": "053d9feccbface9a0b2c1a72447914376aac74ea",
"inherited": false}},
{"git":
{"url": "https://github.com/lurk-lab/LSpec",
"subDir?": null,
"rev": "3b6023654b917c8641ec5e626724a43380cff8f0",
"opts": {},
"name": "LSpec",
"inputRev?": "3b6023654b917c8641ec5e626724a43380cff8f0",
"inherited": false}},
{"git":
{"url": "https://github.com/leanprover/std4/",
"subDir?": null,
"rev": "642cbc9960b49a65a779b8fce56b05ff83cf9e35",
"opts": {},
"name": "std",
"inputRev?": "642cbc9960b49a65a779b8fce56b05ff83cf9e35",
"inherited": true}}]}
[{"url": "https://github.com/lurk-lab/LSpec",
"type": "git",
"subDir": null,
"rev": "3b6023654b917c8641ec5e626724a43380cff8f0",
"name": "LSpec",
"manifestFile": "lake-manifest.json",
"inputRev": "3b6023654b917c8641ec5e626724a43380cff8f0",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/std4/",
"type": "git",
"subDir": null,
"rev": "9e37a01f8590f81ace095b56710db694b5bf8ca0",
"name": "std",
"manifestFile": "lake-manifest.json",
"inputRev": "9e37a01f8590f81ace095b56710db694b5bf8ca0",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/lurk-lab/YatimaStdLib.lean",
"type": "git",
"subDir": null,
"rev": "3037f0c14128751b95510c2723f067ec7a494f08",
"name": "YatimaStdLib",
"manifestFile": "lake-manifest.json",
"inputRev": "3037f0c14128751b95510c2723f067ec7a494f08",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/lurk-lab/straume",
"type": "git",
"subDir": null,
"rev": "ad2aa666b7e4148df450ecf74aedb477f1535534",
"name": "Straume",
"manifestFile": "lake-manifest.json",
"inputRev": "ad2aa666b7e4148df450ecf74aedb477f1535534",
"inherited": false,
"configFile": "lakefile.lean"}],
"name": "Megaparsec",
"lakeDir": ".lake"}
6 changes: 3 additions & 3 deletions lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -7,13 +7,13 @@ package Megaparsec
lean_lib Megaparsec

require LSpec from git
"https://github.com/lurk-lab/LSpec" @ "3b6023654b917c8641ec5e626724a43380cff8f0"
"https://github.com/lurk-lab/LSpec" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114"

require YatimaStdLib from git
"https://github.com/lurk-lab/YatimaStdLib.lean" @ "5b64c5150e371fb280728cbb5b7c225b9c96b348"
"https://github.com/lurk-lab/YatimaStdLib.lean" @ "3037f0c14128751b95510c2723f067ec7a494f08"

require Straume from git
"https://github.com/lurk-lab/straume" @ "053d9feccbface9a0b2c1a72447914376aac74ea"
"https://github.com/lurk-lab/straume" @ "ad2aa666b7e4148df450ecf74aedb477f1535534"

@[default_target]
lean_exe megaparsec {
Expand Down
2 changes: 1 addition & 1 deletion lean-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:v4.0.0
leanprover/lean4:v4.4.0

0 comments on commit 51bb1ba

Please sign in to comment.