Merge pull request #68 from leanprover/update-lean

chore: update toolchain

.gitignore

@@ -1,2 +1,3 @@
 /build
 /lean_packages
+!/lean_packages/manifest.json

DocGen4/Load.lean

@@ -21,18 +21,17 @@ as well as all the dependencies.
 -/
 def lakeSetup (imports : List String) : IO (Except UInt32 (Lake.Workspace × String)) := do
   let (leanInstall?, lakeInstall?) ← Lake.findInstall?
-  match Lake.Cli.mkLakeConfig {leanInstall?, lakeInstall?} with
+  match ←(EIO.toIO' $ Lake.mkLoadConfig {leanInstall?, lakeInstall?}) with
-  | Except.ok config =>
+  | .ok config =>
     let ws : Lake.Workspace ← Lake.loadWorkspace config |>.run Lake.MonadLog.eio
-    let lean := config.leanInstall
+    let libraryLeanGitHash := ws.env.lean.githash
-    if lean.githash ≠ Lean.githash then
+    if libraryLeanGitHash ≠ Lean.githash then
-      IO.println s!"WARNING: This doc-gen was built with Lean: {Lean.githash} but the project is running on: {lean.githash}"
+      IO.println s!"WARNING: This doc-gen was built with Lean: {Lean.githash} but the project is running on: {libraryLeanGitHash}"
-    let lake := config.lakeInstall
+    let ctx ← Lake.mkBuildContext ws
-    let ctx ← Lake.mkBuildContext ws lean lake
     (ws.root.buildImportsAndDeps imports *> pure ()) |>.run Lake.MonadLog.eio ctx
     initSearchPath (←findSysroot) ws.leanPaths.oleanPath
-    pure $ Except.ok (ws, lean.githash)
+    pure $ Except.ok (ws, libraryLeanGitHash)
-  | Except.error err =>
+  | .error err =>
     throw $ IO.userError err.toString
 
 /--

DocGen4/Output/Base.lean

@@ -123,7 +123,7 @@ Returns the doc-gen4 link to a declaration name.
 -/
 def declNameToLink (name : Name) : HtmlM String := do
   let res ← getResult
-  let module := res.moduleNames[res.name2ModIdx.find! name]
+  let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]!
   pure $ (←moduleNameToLink module) ++ "#" ++ name.toString
 
 /--
@@ -137,7 +137,7 @@ Returns the LeanInk link to a declaration name.
 -/
 def declNameToInkLink (name : Name) : HtmlM String := do
   let res ← getResult
-  let module := res.moduleNames[res.name2ModIdx.find! name]
+  let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]!
   pure $ (←moduleNameToInkLink module) ++ "#" ++ name.toString
 
 /--
@@ -179,7 +179,7 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
     match a.info.val.info with
     | Info.ofTermInfo i =>
       match i.expr.consumeMData with
-      | Expr.const name _ _ =>
+      | Expr.const name _ =>
          match t with
          | TaggedText.text t =>
            let (front, t, back) := splitWhitespaces $ Html.escape t

DocGen4/Output/SourceLinker.lean

@@ -63,7 +63,8 @@ def sourceLinker (ws : Lake.Workspace) (leanHash : String): IO (Name → Option
   for pkg in ws.packageArray do
     for dep in pkg.dependencies do
       let value := match dep.src with
-        | Lake.Source.git url commit => (getGithubBaseUrl url, commit.getD "main")
+        -- 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

DocGen4/Process/DocInfo.lean

@@ -114,7 +114,7 @@ def isBlackListed (declName : Name) : MetaM Bool := do
 def isProjFn (declName : Name) : MetaM Bool := do
   let env ← getEnv
   match declName with
-  | Name.str parent name _ =>
+  | Name.str parent name =>
     if isStructure env parent then
       match getStructureInfo? env parent with
       | some i =>

DocGen4/Process/NameInfo.lean

@@ -21,23 +21,21 @@ partial def typeToArgsType (e : Expr) : (Array (Name × Expr × BinderInfo) × E
     -- and print what is left after the : instead. The only exception
     -- to this is instances since these almost never have a name
     -- but should still be printed as arguments instead of after the :.
-    if name.hasMacroScopes ∧ ¬data.binderInfo.isInstImplicit then
+    if name.hasMacroScopes ∧ ¬data.isInstImplicit then
       (#[], e)
     else
       let name := name.eraseMacroScopes
-      let arg := (name, type, data.binderInfo)
+      let arg := (name, type, data)
       let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
       (#[arg] ++ args, final)
   match e.consumeMData with
-  | Expr.lam name type body data => helper name type body data
+  | Expr.lam name type body binderInfo => helper name type body binderInfo
-  | Expr.forallE name type body data => helper name type body data
+  | Expr.forallE name type body binderInfo => helper name type body binderInfo
   | _ => (#[], e)
 
 def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
-  let env ← getEnv
   let (args, type) := typeToArgsType v.type
   let args ← args.mapM (λ (n, e, b) => do pure $ Arg.mk n (←prettyPrintTerm e) b)
-  let doc ← findDocString? env v.name
   let nameInfo ← NameInfo.ofTypedName v.name type
   match ←findDeclarationRanges? v.name with
   -- TODO: Maybe selection range is more relevant? Figure this out in the future

lakefile.lean

@@ -12,16 +12,16 @@ lean_exe «doc-gen4» {
 }
 
 require CMark from git
-  "https://github.com/xubaiw/CMark.lean" @ "192939e27263b0932700ade3442e1bf2ce67c3a6"
+  "https://github.com/xubaiw/CMark.lean" @ "main"
 
 require Unicode from git
-  "https://github.com/hargonix/Unicode.lean" @ "b73232aeefd6391951f9bd256e3dc4ec937c7238"
+  "https://github.com/xubaiw/Unicode.lean" @ "main"
 
 require Cli from git
-  "https://github.com/mhuisi/lean4-cli" @ "f7590ce072b0321752a7b9942892d0104dee4036"
+  "https://github.com/mhuisi/lean4-cli" @ "nightly"
 
 require lake from git
-  "https://github.com/leanprover/lake" @ "401e738e4ca989ced8d9bb0cf7f66be9133fc435"
+  "https://github.com/leanprover/lake" @ "master"
 
 require leanInk from git
   "https://github.com/hargonix/LeanInk" @ "doc-gen"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2022-06-30
+leanprover/lean4:nightly-2022-07-20