chore: update toolchain

main
Henrik 2023-07-30 20:45:40 +02:00
parent 9b524d7c5a
commit c312f00c88
3 changed files with 4 additions and 14 deletions

View File

@ -4,15 +4,9 @@
[{"git":
{"url": "https://github.com/xubaiw/CMark.lean",
"subDir?": null,
"rev": "2cc7cdeef67184f84db6731450e4c2b258c28fe8",
"rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
"name": "CMark",
"inputRev?": "main"}},
{"git":
{"url": "https://github.com/leanprover/lake",
"subDir?": null,
"rev": "0d4da61cbfe65f19ac7070c2c9f62f36db529c4c",
"name": "lake",
"inputRev?": "master"}},
{"git":
{"url": "https://github.com/mhuisi/lean4-cli",
"subDir?": null,
@ -28,6 +22,6 @@
{"git":
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
"subDir?": null,
"rev": "ce508dcd1fd49ba15675861aafd864572a0b8252",
"rev": "f09250282cea3ed8c010f430264d9e8e50d7bc32",
"name": "UnicodeBasic",
"inputRev?": "main"}}]}

View File

@ -20,9 +20,6 @@ require UnicodeBasic from git
require Cli from git
"https://github.com/mhuisi/lean4-cli" @ "nightly"
require lake from git
"https://github.com/leanprover/lake" @ "master"
require leanInk from git
"https://github.com/hargonix/LeanInk" @ "doc-gen"
@ -70,8 +67,7 @@ library_facet docs (lib) : FilePath := do
let exeJob ← docGen4.exe.fetch
-- XXX: Workaround remove later
let coreJob ← if h : docGen4Pkg.name = _package.name then
have : PackageName docGen4Pkg _package.name := ⟨h⟩
let coreJob ← if docGen4Pkg.name = _package.name then
let job := fetch <| docGen4Pkg.target `coreDocs
job
else

View File

@ -1 +1 @@
leanprover/lean4:nightly-2023-05-31
leanprover/lean4:nightly-2023-07-29