From d29e14a26aba91fcb39baa39477ebb9cd464ecb5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 9 Aug 2022 23:30:43 +0200 Subject: [PATCH] chore: update toolchain and dependencies --- DocGen4.lean | 1 - DocGen4/IncludeStr.lean | 57 ------------------------------- DocGen4/Load.lean | 13 ++++--- DocGen4/Output/Base.lean | 1 - DocGen4/Output/SourceLinker.lean | 21 ++++++------ DocGen4/Process/Attributes.lean | 3 +- DocGen4/Process/InstanceInfo.lean | 3 +- lakefile.lean | 19 ----------- lean-toolchain | 2 +- lean_packages/manifest.json | 12 +++---- 10 files changed, 27 insertions(+), 105 deletions(-) delete mode 100644 DocGen4/IncludeStr.lean diff --git a/DocGen4.lean b/DocGen4.lean index 8456fa1..09a4641 100644 --- a/DocGen4.lean +++ b/DocGen4.lean @@ -5,6 +5,5 @@ Authors: Henrik Böving -/ import DocGen4.Process import DocGen4.Load -import DocGen4.IncludeStr import DocGen4.Output import DocGen4.LeanInk diff --git a/DocGen4/IncludeStr.lean b/DocGen4/IncludeStr.lean deleted file mode 100644 index c4b28a9..0000000 --- a/DocGen4/IncludeStr.lean +++ /dev/null @@ -1,57 +0,0 @@ -/- -Copyright (c) 2021 Henrik Böving. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Henrik Böving --/ -import Lean - -namespace DocGen4 - -open Lean System IO Lean.Elab.Term FS - -deriving instance DecidableEq for FileType - -/-- - Traverse all subdirectories fo `f` to find if one satisfies `p`. --/ -partial def traverseDir (f : FilePath) (p : FilePath → IO Bool) : IO (Option FilePath) := do - if (← p f) then - return f - for d in (← System.FilePath.readDir f) do - let subDir := d.path - let metadata ← subDir.metadata - if metadata.type = FileType.dir then - if let some p ← traverseDir subDir p then - return p - return none - -syntax (name := includeStr) "include_str" str : term - -/-- -Provides a way to include the contents of a file at compile time as a String. -This is used to include things like the CSS and JS in the binary so we -don't have to carry them around as files. --/ -@[termElab includeStr] def includeStrImpl : TermElab := λ stx _ => do - let str := stx[1].isStrLit?.get! - let srcPath := FilePath.mk <| ←getFileName - let currentDir ← IO.currentDir - -- HACK: Currently we cannot get current file path in VSCode, we have to traversely find the matched subdirectory in the current directory. - if let some path ← match srcPath.parent with - | some p => pure <| some <| p / str - | none => do - let foundDir ← traverseDir currentDir λ p => p / str |>.pathExists - pure <| foundDir.map (· / str) - then - if ←path.pathExists then - if ←path.isDir then - throwError s!"{str} is a directory" - else - let content ← FS.readFile path - pure <| mkStrLit content - else - throwError s!"{path} does not exist as a file" - else - throwError s!"No such file in whole directory: {str}" - -end DocGen4 diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index e6e9db9..d682e38 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -23,13 +23,16 @@ def lakeSetup (imports : List String) : IO (Except UInt32 Lake.Workspace) := do let (leanInstall?, lakeInstall?) ← Lake.findInstall? match ←(EIO.toIO' <| Lake.mkLoadConfig {leanInstall?, lakeInstall?}) with | .ok config => - let ws : Lake.Workspace ← Lake.loadWorkspace config |>.run Lake.MonadLog.eio - let libraryLeanGitHash := ws.env.lean.githash + let ws : Lake.Workspace ← Lake.loadWorkspace config + |>.run Lake.MonadLog.eio + |>.toIO (λ _ => IO.userError "Failed to load Lake workspace") + let libraryLeanGitHash := ws.lakeEnv.lean.githash if libraryLeanGitHash ≠ Lean.githash then IO.println s!"WARNING: This doc-gen was built with Lean: {Lean.githash} but the project is running on: {libraryLeanGitHash}" - let ctx ← Lake.mkBuildContext ws - (ws.root.buildImportsAndDeps imports *> pure ()) |>.run Lake.MonadLog.eio ctx - initSearchPath (←findSysroot) ws.leanPaths.oleanPath + let _libs ← ws.runBuild (Lake.buildImportsAndDeps imports) false + |>.run (Lake.MonadLog.eio config.verbosity) + |>.toIO (λ _ => IO.userError "Failed to compile imports via Lake") + initSearchPath (←findSysroot) (ws.packageList.map (·.oleanDir)) pure <| Except.ok ws | .error err => throw <| IO.userError err.toString diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 469b77c..e8c1ee3 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ import DocGen4.Process -import DocGen4.IncludeStr import DocGen4.Output.ToHtmlFormat namespace DocGen4.Output diff --git a/DocGen4/Output/SourceLinker.lean b/DocGen4/Output/SourceLinker.lean index e403c5e..d6f66e7 100644 --- a/DocGen4/Output/SourceLinker.lean +++ b/DocGen4/Output/SourceLinker.lean @@ -55,20 +55,18 @@ compiler release to work with this provides a function to turn names of declarations into (optionally positional) Github URLs. -/ def sourceLinker (ws : Lake.Workspace) : IO (Name → Option DeclarationRange → String) := do - let leanHash := ws.env.lean.githash + let leanHash := ws.lakeEnv.lean.githash -- Compute a map from package names to source URL let mut gitMap := Std.mkHashMap let projectBaseUrl := getGithubBaseUrl (←getProjectGithubUrl) let projectCommit ← getProjectCommit gitMap := gitMap.insert ws.root.name (projectBaseUrl, projectCommit) - for pkg in ws.packageArray do - for dep in pkg.dependencies do - let value := match dep.src with - -- TODO: subdir handling - | Lake.Source.git url commit _ => (getGithubBaseUrl url, commit.getD "main") - -- TODO: What do we do here if linking a source is not possible? - | _ => ("https://example.com", "master") - gitMap := gitMap.insert dep.name value + 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 + let value := (getGithubBaseUrl pkg.url, pkg.rev) + gitMap := gitMap.insert pkg.name value pure λ module range => let parts := module.components.map Name.toString @@ -79,8 +77,9 @@ def sourceLinker (ws : Lake.Workspace) : IO (Name → Option DeclarationRange else match ws.packageArray.find? (·.isLocalModule module) with | some pkg => - let (baseUrl, commit) := gitMap.find! pkg.name - s!"{baseUrl}/blob/{commit}/{path}.lean" + match gitMap.find? pkg.name with + | some (baseUrl, commit) => s!"{baseUrl}/blob/{commit}/{path}.lean" + | none => "https://example.com" | none => "https://example.com" match range with diff --git a/DocGen4/Process/Attributes.lean b/DocGen4/Process/Attributes.lean index a7b1317..3ed7ca3 100644 --- a/DocGen4/Process/Attributes.lean +++ b/DocGen4/Process/Attributes.lean @@ -39,7 +39,7 @@ instance : ValueAttr EnumAttributes where Obtain the value of a parametric attribute for a certain name. -/ def parametricGetValue {α : Type} [Inhabited α] [ToString α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option String := do - let val ← ParametricAttribute.getParam attr env decl + let val ← ParametricAttribute.getParam? attr env decl some (attr.attr.name.toString ++ " " ++ toString val) instance : ValueAttr ParametricAttribute where @@ -108,7 +108,6 @@ def getValuesAux {α : Type} {attrKind : Type → Type} [va : ValueAttr attrKind pure <| va.getValue attr env decl def getValues {attrKind : Type → Type} [ValueAttr attrKind] (decl : Name) (attrs : Array (ValueAttrWrapper attrKind)) : MetaM (Array String) := do - let env ← getEnv let mut res := #[] for attr in attrs do if let some val ← @getValuesAux attr.α attrKind _ attr.inhab attr.str decl attr.attr then diff --git a/DocGen4/Process/InstanceInfo.lean b/DocGen4/Process/InstanceInfo.lean index dbccd67..14220ce 100644 --- a/DocGen4/Process/InstanceInfo.lean +++ b/DocGen4/Process/InstanceInfo.lean @@ -25,8 +25,7 @@ where def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do let mut info ← DefinitionInfo.ofDefinitionVal v - let some className := getClassName (←getEnv) v.type | unreachable! - + let some className ← isClass? v.type | unreachable! if let some instAttr ← getDefaultInstance v.name className then info := { info with attrs := info.attrs.push instAttr } let typeNames ← getInstanceTypes v.type diff --git a/lakefile.lean b/lakefile.lean index 657a3b0..af7ebaf 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -26,22 +26,3 @@ require lake from git require leanInk from git "https://github.com/hargonix/LeanInk" @ "doc-gen-json" - -module_facet docs : FilePath := fun mod => do - let some docGen4 ← findLeanExe? `«doc-gen4» - | error "no doc-gen4 executable configuration found in workspace" - let exeTarget ← docGen4.exe.recBuild - let modTarget ← mod.leanBin.recBuild - let buildDir := (← getWorkspace).root.buildDir - let docFile := mod.filePath (buildDir / "doc") "html" - let task ← show SchedulerM _ from do - exeTarget.bindAsync fun exeFile exeTrace => do - modTarget.bindSync fun _ modTrace => do - let depTrace := exeTrace.mix modTrace - buildFileUnlessUpToDate docFile depTrace do - proc { - cmd := exeFile.toString - args := #["single", mod.name.toString] - env := #[("LEAN_PATH", (← getAugmentedLeanPath).toString)] - } - return ActiveTarget.mk docFile task diff --git a/lean-toolchain b/lean-toolchain index d1e3f76..f62cade 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-07-24 +leanprover/lean4:nightly-2022-08-09 diff --git a/lean_packages/manifest.json b/lean_packages/manifest.json index e0cb385..83376d9 100644 --- a/lean_packages/manifest.json +++ b/lean_packages/manifest.json @@ -1,20 +1,20 @@ -{"version": 1, +{"version": 2, "packages": [{"url": "https://github.com/mhuisi/lean4-cli", "rev": "112b35fc348a4a18d2111ac2c6586163330b4941", "name": "Cli"}, {"url": "https://github.com/hargonix/LeanInk", - "rev": "5d0aaba8b4fceeaf3a719e014dd42ca5d02f4810", + "rev": "eed51a5e121233c3d15fb14642048a9bd3e00695", "name": "leanInk"}, {"url": "https://github.com/xubaiw/Unicode.lean", - "rev": "1fb004da96aa1d1e98535951e100439a60f5b7f0", + "rev": "25b32ef69fd6d8ae34300d51dc0b9403ffb1fd29", "name": "Unicode"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "rev": "ecd37441047e490ff2ad339e16f45bb8b58591bd", "name": "mathlib"}, {"url": "https://github.com/leanprover/lake", - "rev": "a7bc6addee9fc07c0ee43d0dcb537faa41844217", + "rev": "6cfb4e3fd7ff700ace8c2cfdb85056d59f321920", "name": "lake"}, {"url": "https://github.com/xubaiw/CMark.lean", - "rev": "8f17d13d3046c517f7f02062918d81bc69e45cce", - "name": "CMark"}]} \ No newline at end of file + "rev": "8c0f9c1b16ee8047813f43b1f92de471782114ff", + "name": "CMark"}]}