chore: update toolchain

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

DocGen4/IncludeStr.lean

@@ -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

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

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

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

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

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

lakefile.lean

@@ -26,22 +26,3 @@ require lake from git
 
 require leanInk from git
   "https://github.com/hargonix/LeanInk" @ "doc-gen"
-
-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

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2022-07-24
+leanprover/lean4:nightly-2022-08-09

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": "0c113bb4cc88d4b8dc6b2d26a4c4c9cf6008a2eb",
+   "rev": "439303af06465824588a486f5f9c023ca69979f3",
    "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"}]}
+   "rev": "8c0f9c1b16ee8047813f43b1f92de471782114ff",
+   "name": "CMark"}]}