From 504f39edc5ff51ff4ae978f44dd8bc220a1d697e Mon Sep 17 00:00:00 2001 From: tydeu Date: Fri, 3 May 2024 15:41:22 -0400 Subject: [PATCH 1/2] chore: update Lean/Lake to v4.8.0-rc1 --- lakefile.lean | 56 +++++++++++++++++++++----------------------------- lean-toolchain | 2 +- 2 files changed, 24 insertions(+), 34 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 3c219dd4..ab9ee0f5 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -63,8 +63,8 @@ def appendModPath (libUri : String) (pathSep : Char) (mod : Module) : String := /-- Append the library and mod path to the given Uri referring to the package source. -/ -def appendLibModPath (pkgUri : String) (pathSep : Char) (lib : LeanLibConfig) (mod : Module) : String := - let libPath := filteredPath lib.srcDir +def appendLibModPath (pkgUri : String) (pathSep : Char) (mod : Module) : String := + let libPath := filteredPath mod.lib.srcDir appendModPath (pathSep.toString.intercalate (pkgUri :: libPath)) pathSep mod /-- @@ -87,62 +87,55 @@ def getGithubBaseUrl (url : String) : Option String := else .none -def getGithubUrl (pkg : Package) (lib : LeanLibConfig) (mod : Module) : IO String := do - let url ← getGitRemoteUrl pkg.dir "origin" +def getGithubUrl (mod : Module) : IO String := do + let url ← getGitRemoteUrl mod.pkg.dir "origin" let .some baseUrl := getGithubBaseUrl url | throw <| IO.userError <| s!"Could not interpret Git remote uri {url} as a Github source repo.\n" ++ "See README on source URIs for more details." - let commit ← getProjectCommit pkg.dir - let srcDir := filteredPath pkg.config.srcDir + let commit ← getProjectCommit mod.pkg.dir + let srcDir := filteredPath mod.pkg.config.srcDir let pkgUri := "/".intercalate <| baseUrl :: "blob" :: commit :: srcDir - - pure <| appendLibModPath pkgUri '/' lib mod + return appendLibModPath pkgUri '/' mod /-- Return a File uri for the module. -/ -def getFileUri (pkg : Package) (lib : LeanLibConfig) (mod : Module) := do - let dir ← IO.FS.realPath (pkg.dir / pkg.config.srcDir) - pure <| appendLibModPath s!"file://{dir}" FilePath.pathSeparator lib mod +def getFileUri (mod : Module) : IO String := do + let dir ← IO.FS.realPath (mod.pkg.dir / mod.pkg.config.srcDir) + return appendLibModPath s!"file://{dir}" FilePath.pathSeparator mod /-- Return a VSCode uri for the module. -/ -def getVSCodeUri (pkg : Package) (lib : LeanLibConfig) (mod : Module) : IO String := do - let dir ← IO.FS.realPath (pkg.dir / pkg.config.srcDir) - pure <| appendLibModPath s!"vscode://file/{dir}" FilePath.pathSeparator lib mod +def getVSCodeUri (mod : Module) : IO String := do + let dir ← IO.FS.realPath (mod.pkg.dir / mod.pkg.config.srcDir) + return appendLibModPath s!"vscode://file/{dir}" FilePath.pathSeparator mod /-- Attempt to determine URI to use for the module source file. -/ -def getSrcUri (pkg : Package) (lib : LeanLibConfig) (mod : Module) : IO String := do +def getSrcUri (mod : Module) : IO String := do match ←IO.getEnv "DOCGEN_SRC" with - | .none | .some "github" | .some "" => getGithubUrl pkg lib mod - | .some "vscode" => getVSCodeUri pkg lib mod - | .some "file" => getFileUri pkg lib mod + | .none | .some "github" | .some "" => getGithubUrl mod + | .some "vscode" => getVSCodeUri mod + | .some "file" => getFileUri mod | .some _ => throw <| IO.userError "$DOCGEN_SRC should be github, file, or vscode." module_facet docs (mod) : FilePath := do - let some docGen4 ← findLeanExe? `«doc-gen4» - | error "no doc-gen4 executable configuration found in workspace" - let exeJob ← docGen4.exe.fetch + let exeJob ← «doc-gen4».fetch let modJob ← mod.leanArts.fetch - let ws ← getWorkspace - let pkg ← ws.packages.find? (·.isLocalModule mod.name) - let libConfig ← pkg.leanLibConfigs.toArray.find? (·.isLocalModule mod.name) -- Build all documentation imported modules let imports ← mod.imports.fetch let depDocJobs ← BuildJob.mixArray <| ← imports.mapM fun mod => fetch <| mod.facet `docs - let srcUri ← getSrcUri pkg libConfig mod - let buildDir := ws.root.buildDir + let srcUri ← getSrcUri mod + let buildDir := (←getWorkspace).root.buildDir let docFile := mod.filePath (buildDir / "doc") "html" depDocJobs.bindAsync fun _ depDocTrace => do exeJob.bindAsync fun exeFile exeTrace => do modJob.bindSync fun _ modTrace => do let depTrace := mixTraceArray #[exeTrace, modTrace, depDocTrace] let trace ← buildFileUnlessUpToDate docFile depTrace do - logStep s!"Documenting module: {mod.name}" proc { cmd := exeFile.toString args := #["single", mod.name.toString, srcUri] @@ -150,16 +143,13 @@ module_facet docs (mod) : FilePath := do } return (docFile, trace) --- TODO: technically speaking this facet does not show all file dependencies +-- TODO: technically speaking this target does not show all file dependencies target coreDocs : FilePath := do - let some docGen4 ← findLeanExe? `«doc-gen4» - | error "no doc-gen4 executable configuration found in workspace" - let exeJob ← docGen4.exe.fetch + let exeJob ← «doc-gen4».fetch let basePath := (←getWorkspace).root.buildDir / "doc" let dataFile := basePath / "declarations" / "declaration-data-Lean.bmp" exeJob.bindSync fun exeFile exeTrace => do let trace ← buildFileUnlessUpToDate dataFile exeTrace do - logStep "Documenting Lean core: Init and Lean" proc { cmd := exeFile.toString args := #["genCore"] @@ -170,7 +160,7 @@ target coreDocs : FilePath := do library_facet docs (lib) : FilePath := do let mods ← lib.modules.fetch let moduleJobs ← BuildJob.mixArray <| ← mods.mapM (fetch <| ·.facet `docs) - let coreJob : BuildJob FilePath ← coreDocs.fetch + let coreJob ← coreDocs.fetch let exeJob ← «doc-gen4».fetch -- Shared with DocGen4.Output let basePath := (←getWorkspace).root.buildDir / "doc" diff --git a/lean-toolchain b/lean-toolchain index 9ad30404..d8a6d7ef 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.7.0 +leanprover/lean4:v4.8.0-rc1 From d6176afce4c94eb1893b15b4c8965431f8880640 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 3 May 2024 23:47:02 +0200 Subject: [PATCH 2/2] chore: rest of the 4.8 upgrade --- DocGen4/LeanInk/Output.lean | 14 +++++++------- DocGen4/Output/Module.lean | 6 +++--- DocGen4/Output/Navbar.lean | 7 +++---- DocGen4/Output/Structure.lean | 22 ++++++++++++---------- DocGen4/Process/Attributes.lean | 17 +++++++++++++---- DocGen4/Process/DocInfo.lean | 2 +- DocGen4/Process/InstanceInfo.lean | 6 +++--- lake-manifest.json | 6 +++--- 8 files changed, 45 insertions(+), 35 deletions(-) diff --git a/DocGen4/LeanInk/Output.lean b/DocGen4/LeanInk/Output.lean index ae238322..6c6d1e18 100644 --- a/DocGen4/LeanInk/Output.lean +++ b/DocGen4/LeanInk/Output.lean @@ -129,26 +129,26 @@ def Message.toHtml (m : Message) : AlectryonM Html := do def Sentence.toHtml (s : Sentence) : AlectryonM Html := do - let messages := + let messages ← do if s.messages.size > 0 then - #[ + pure #[
[← s.messages.mapM Message.toHtml]
] else - #[] - - let goals := + pure #[] + + let goals ← if s.goals.size > 0 then -- TODO: Alectryon has a "alectryon-extra-goals" here, implement it - #[ + pure #[
[← s.goals.mapM Goal.toHtml]
] else - #[] + pure #[] let buttonLabel ← getNextButtonLabel diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index dbaa504f..f0ff9289 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -114,15 +114,15 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do #[Html.element "div" false #[("class", "attributes")] #[attrStr]] else #[] - let leanInkHtml := + let leanInkHtml ← do if ← leanInkEnabled? then - #[ + pure #[
ink
] else - #[] + pure #[] pure
diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index 33f06f7b..b25a74a2 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -29,12 +29,11 @@ partial def moduleListDir (h : Hierarchy) : BaseHtmlM Html := do let dirNodes ← dirs.mapM moduleListDir let fileNodes ← files.mapM moduleListFile let moduleLink ← moduleNameToLink h.getName - let summary := + let summary ← do if h.isFile then - {s!"{h.getName.getString!} ({file})"} + pure {s!"{h.getName.getString!} ({file})"} else - {h.getName.getString!} - + pure {h.getName.getString!} pure
{summary} diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean index 8f48dc36..ad019949 100644 --- a/DocGen4/Output/Structure.lean +++ b/DocGen4/Output/Structure.lean @@ -31,20 +31,22 @@ def fieldToHtml (f : Process.NameInfo) : HtmlM Html := do Render all information about a structure as HTML. -/ def structureToHtml (i : Process.StructureInfo) : HtmlM (Array Html) := do - let structureHtml := + let structureHtml ← do if Name.isSuffixOf `mk i.ctor.name then - (
    - [← i.fieldInfo.mapM fieldToHtml] -
) + pure +
    + [← i.fieldInfo.mapM fieldToHtml] +
else let ctorShortName := i.ctor.name.componentsRev.head!.toString - (
    -
  • {s!"{ctorShortName} "} :: (
    • -
      - [← i.fieldInfo.mapM fieldToHtml] + pure +
        +
      • {s!"{ctorShortName} "} :: (
        • +
          + [← i.fieldInfo.mapM fieldToHtml] +
        +
      • )
      -
    • )
      • -
    ) return #[structureHtml] end Output diff --git a/DocGen4/Process/Attributes.lean b/DocGen4/Process/Attributes.lean index ff6e7f34..7c74e866 100644 --- a/DocGen4/Process/Attributes.lean +++ b/DocGen4/Process/Attributes.lean @@ -1,4 +1,5 @@ import Lean +import Lean.ReducibilityAttrs namespace DocGen4 @@ -86,7 +87,7 @@ instance : ToString ReducibilityStatus where The list of all enum based attributes doc-gen knows about and can recover. -/ @[reducible] -def enumAttributes : Array EnumAttrWrapper := #[⟨Compiler.inlineAttrs⟩, ⟨reducibilityAttrs⟩] +def enumAttributes : Array EnumAttrWrapper := #[⟨Compiler.inlineAttrs⟩] instance : ToString ExternEntry where toString entry := @@ -127,8 +128,8 @@ def getEnumValues (decl : Name) : MetaM (Array String) := getValues decl enumAtt def getParametricValues (decl : Name) : MetaM (Array String) := do let mut uniform ← getValues decl parametricAttributes -- This attribute contains an `Option Name` but we would like to pretty print it better - if let some depTag := Linter.deprecatedAttr.getParam? (← getEnv) decl then - let str := match depTag with + if let some depEntry := Linter.deprecatedAttr.getParam? (← getEnv) decl then + let str := match depEntry.newName? with | some alt => s!"deprecated {alt.toString}" | none => "deprecated" uniform := uniform.push str @@ -155,11 +156,19 @@ def hasCsimp (decl : Name) : MetaM (Option String) := do else return none +def getReducibility (decl : Name) : MetaM (Option String) := do + let status ← getReducibilityStatus decl + match status with + | .reducible => return some "reducible" + | .irreducible => return some "irreducible" + -- This is the default so we don't print it. + | .semireducible => return none + /-- The list of custom attributes, that don't fit in the parametric or enum attribute kinds, doc-gen konws about and can recover. -/ -def customAttrs := #[hasSimp, hasCsimp] +def customAttrs := #[hasSimp, hasCsimp, getReducibility] def getCustomAttrs (decl : Name) : MetaM (Array String) := do let mut values := #[] diff --git a/DocGen4/Process/DocInfo.lean b/DocGen4/Process/DocInfo.lean index e736c166..b4e6339d 100644 --- a/DocGen4/Process/DocInfo.lean +++ b/DocGen4/Process/DocInfo.lean @@ -137,7 +137,7 @@ def isProjFn (declName : Name) : MetaM Bool := do if isStructure env parent then match getStructureInfo? env parent with | some i => - match i.fieldNames.find? (· == name) with + match i.fieldNames.find? (·.toString == name) with | some _ => return true | none => return false | none => panic! s!"{parent} is not a structure" diff --git a/DocGen4/Process/InstanceInfo.lean b/DocGen4/Process/InstanceInfo.lean index df37004d..b97d389f 100644 --- a/DocGen4/Process/InstanceInfo.lean +++ b/DocGen4/Process/InstanceInfo.lean @@ -21,9 +21,9 @@ def getInstanceTypes (typ : Expr) : MetaM (Array Name) := do return names where findName : BinderInfo × Expr → StateRefT (Array Name) MetaM Unit - | (.default, .sort .zero) => modify (·.push "_builtin_prop") - | (.default, .sort (.succ _)) => modify (·.push "_builtin_typeu") - | (.default, .sort _) => modify (·.push "_builtin_sortu") + | (.default, .sort .zero) => modify (·.push `_builtin_prop) + | (.default, .sort (.succ _)) => modify (·.push `_builtin_typeu) + | (.default, .sort _) => modify (·.push `_builtin_sortu) | (.default, e) => match e.getAppFn with | .const name .. => modify (·.push name) diff --git a/lake-manifest.json b/lake-manifest.json index ef3b798b..91c0e1d8 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/xubaiw/CMark.lean", "type": "git", "subDir": null, - "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77", + "rev": "ba7b47bd773954b912ecbf5b1c9993c71a166f05", "name": "CMark", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -13,7 +13,7 @@ {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, - "rev": "6a350f4ec7323a4e8ad6bf50736f779853d441e9", + "rev": "8b53cc65534bc2c6888c3d4c53a3439648213f74", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -22,7 +22,7 @@ {"url": "https://github.com/mhuisi/lean4-cli", "type": "git", "subDir": null, - "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa", + "rev": "10d88b52fa8d717fa8e29af3abf0c3a2bf175497", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "nightly",