diff --git a/DocGen4/Output/SourceLinker.lean b/DocGen4/Output/SourceLinker.lean index 30c0657..2678f8e 100644 --- a/DocGen4/Output/SourceLinker.lean +++ b/DocGen4/Output/SourceLinker.lean @@ -64,7 +64,7 @@ def sourceLinker (ws : Lake.Workspace) : IO (Name → Option DeclarationRange let manifest ← Lake.Manifest.loadOrEmpty ws.root.manifestFile |>.run (Lake.MonadLog.eio .normal) |>.toIO (λ _ => IO.userError "Failed to load lake manifest") - for pkg in manifest.toArray do + for pkg in manifest.entryArray do if let .git _ url rev .. := pkg then gitMap := gitMap.insert pkg.name (getGithubBaseUrl url, rev) diff --git a/lake-manifest.json b/lake-manifest.json index b546371..c8fda0d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,6 +1,19 @@ -{"version": 3, +{"version": 4, + "packagesDir": "./lake-packages", "packages": [{"git": + {"url": "https://github.com/xubaiw/CMark.lean", + "subDir?": null, + "rev": "2cc7cdeef67184f84db6731450e4c2b258c28fe8", + "name": "CMark", + "inputRev?": "main"}}, + {"git": + {"url": "https://github.com/leanprover/lake", + "subDir?": null, + "rev": "235383015cdcb0082777b0347b84dba01843c79c", + "name": "lake", + "inputRev?": "master"}}, + {"git": {"url": "https://github.com/mhuisi/lean4-cli", "subDir?": null, "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e", @@ -17,16 +30,4 @@ "subDir?": null, "rev": "6dd6ae3a3839c8350a91876b090eda85cf538d1d", "name": "Unicode", - "inputRev?": "main"}}, - {"git": - {"url": "https://github.com/leanprover/lake", - "subDir?": null, - "rev": "051cf403f12da80a44802810d9098f2bbed61d93", - "name": "lake", - "inputRev?": "master"}}, - {"git": - {"url": "https://github.com/xubaiw/CMark.lean", - "subDir?": null, - "rev": "2cc7cdeef67184f84db6731450e4c2b258c28fe8", - "name": "CMark", "inputRev?": "main"}}]} diff --git a/lakefile.lean b/lakefile.lean index 5aa26df..9a8b32f 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -77,7 +77,8 @@ library_facet docs (lib) : FilePath := do else error "wrong package" - let moduleJobs ← BuildJob.mixArray (α := FilePath) <| ← lib.recBuildLocalModules #[`docs] + let mods ← lib.modules.fetch + let moduleJobs ← BuildJob.mixArray <| ← mods.mapM (fetch <| ·.facet `docs) -- Shared with DocGen4.Output let basePath := (←getWorkspace).root.buildDir / "doc" let dataFile := basePath / "declarations" / "declaration-data.bmp" diff --git a/lean-toolchain b/lean-toolchain index a287eeb..5ca06ea 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-11-30 +leanprover/lean4:nightly-2022-12-03