diff --git a/.github/workflows/copyright-header.yml b/.github/workflows/copyright-header.yml index 4727a4f80..c21f2baaa 100644 --- a/.github/workflows/copyright-header.yml +++ b/.github/workflows/copyright-header.yml @@ -15,10 +15,22 @@ jobs: - name: Verify .lean files start with a copyright header. run: | - FILES=$(find ./src ./test-projects -path ./src/tests/interactive -prune -type f -name "*.lean" -exec perl -ne 'BEGIN { $/ = undef; } print "$ARGV\n" if !m{\A/-\nCopyright}; exit;' {} \;) - if [ -n "$FILES" ]; then + OFFENDING=() + while IFS= read -r -d '' file; do + if ! head -1 "$file" | grep -q '^/-$'; then + OFFENDING+=("$file") + elif ! head -2 "$file" | tail -1 | grep -q '^Copyright'; then + OFFENDING+=("$file") + fi + done < <(find ./src ./test-projects \ + -path ./src/tests/interactive -prune -o \ + -path '*/.lake' -prune -o \ + -path './test-projects/literate-*' -prune -o \ + -type f -name "*.lean" -print0) + + if [ ${#OFFENDING[@]} -gt 0 ]; then echo "Found .lean files which do not have a copyright header:" - echo "$FILES" + printf '%s\n' "${OFFENDING[@]}" exit 1 else echo "All copyright headers present." diff --git a/doc-sources.toml b/doc-sources.toml new file mode 100644 index 000000000..c8f6872ec --- /dev/null +++ b/doc-sources.toml @@ -0,0 +1,3 @@ +# These are the libraries documented in the Verso User's Guide +libraries = ["Verso", "VersoManual", "VersoBlog"] +include_core = true diff --git a/doc/UsersGuide.lean b/doc/UsersGuide.lean index d29407a4b..954b8f04f 100644 --- a/doc/UsersGuide.lean +++ b/doc/UsersGuide.lean @@ -1,3 +1,4 @@ +module import VersoManual import UsersGuide.Basic diff --git a/doc/UsersGuide/Basic.lean b/doc/UsersGuide/Basic.lean index 41d733a56..192644a71 100644 --- a/doc/UsersGuide/Basic.lean +++ b/doc/UsersGuide/Basic.lean @@ -3,7 +3,8 @@ Copyright (c) 2023-2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ -import VersoManual +module +public import VersoManual import UsersGuide.Markup import UsersGuide.Websites import UsersGuide.Manuals diff --git a/doc/UsersGuide/Elab.lean b/doc/UsersGuide/Elab.lean index 4bfa0738f..9128e9483 100644 --- a/doc/UsersGuide/Elab.lean +++ b/doc/UsersGuide/Elab.lean @@ -3,11 +3,13 @@ Copyright (c) 2023-2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ - +module import Lean.DocString.Syntax -import VersoManual +public import VersoManual -open Verso Genre Manual +open Verso Genre +open Verso.Genre.Manual hiding docstring tactic conv +open Verso.Genre.Manual.DocGen open Verso.Genre.Manual.InlineLean diff --git a/doc/UsersGuide/Extensions.lean b/doc/UsersGuide/Extensions.lean index fe4d0882c..e741e0763 100644 --- a/doc/UsersGuide/Extensions.lean +++ b/doc/UsersGuide/Extensions.lean @@ -3,10 +3,13 @@ Copyright (c) 2023-2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ +module import Lean.DocString.Syntax -import VersoManual +public import VersoManual -open Verso Genre Manual +open Verso Genre +open Verso.Genre.Manual hiding docstring tactic conv +open Verso.Genre.Manual.DocGen open InlineLean #doc (Manual) "Extensions" => diff --git a/doc/UsersGuide/Literate.lean b/doc/UsersGuide/Literate.lean index 35dba726f..d26bd6a92 100644 --- a/doc/UsersGuide/Literate.lean +++ b/doc/UsersGuide/Literate.lean @@ -3,8 +3,9 @@ Copyright (c) 2026 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ +module import Lean.DocString.Syntax -import VersoManual +public import VersoManual import VersoBlog open Verso Genre Manual diff --git a/doc/UsersGuide/Manuals.lean b/doc/UsersGuide/Manuals.lean index 21576de23..e4b35be44 100644 --- a/doc/UsersGuide/Manuals.lean +++ b/doc/UsersGuide/Manuals.lean @@ -3,15 +3,20 @@ Copyright (c) 2023-2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ +module import Lean.DocString.Syntax -import VersoManual +public import VersoManual import VersoBlog -open Verso Genre Manual +open Verso Genre +open Verso.Genre.Manual hiding docstring tactic conv +open Verso.Genre.Manual.DocGen open InlineLean open Verso.Doc +set_option pp.rawOnError true + #doc (Manual) "Manuals and Books" => %%% tag := "manual" @@ -23,6 +28,7 @@ It supports generating both HTML and PDFs via LaTeX, but the PDF support is rela {docstring Manual} + {docstring Manual.PartMetadata} {docstring Manual.HtmlSplitMode} @@ -143,6 +149,83 @@ results in :::: +## Docstrings From `doc-gen4` (Experimental) +%%% +tag := "docgen-docstrings" +%%% + +:::paragraph +Ordinarily, the {name Verso.Genre.Manual.docstring}`docstring` command extracts documentation directly from the Lean environment. +This requires that the documented library be imported into the Verso document, which has two drawbacks: + + * Declarations from Verso itself and its dependencies are present in the environment alongside the documented library, making it difficult to distinguish the two. + * When using the module system, docstrings are saved in the server `.olean`, and are not available when building at the command line. + This means that complicated documents written in Verso cannot get the benefits of the module system, such as improved incremental rebuilds and less memory use. + * Documentation does not necessarily have a global view of the package being documented, making it difficult to automatically take care of cross-cutting concerns such as listing all instances of a type class. +::: + +The {name}`DocGen.docstring` command is an experimental alternative implementation that displays docstrings extracted by `doc-gen4` rather than from the Lean environment. +It produces the same output as the standard {name Verso.Genre.Manual.docstring}`docstring` command. + +Before the text that includes the docstrings is built, `doc-gen4` is invoked to produce a SQLite database that includes the documented declarations. +Then, each page of documentation reads this database during elaboration. + +### Setup + +To use docstrings from `doc-gen4`, two pieces of configuration are needed: + * The documentation extraction tool must be configured to include the correct libraries. + * Lake needs to run this tool prior to building the documetnation. + +The extraction tool is configured in a file called `doc-sources.toml` in the root of the package in which documentation is written. +It contains two fields: `libraries` is an array of strings, each of which is a library's module root, and `include_core` is a Boolean that determines whether the Lean standard library and metaprogramming API are included (defaulting to `true`). + +:::paragraph +For example, to include `MyLib` and `MyOtherLib` along with the Lean standard library, use this file: +``` +libraries = ["MyLib", "MyOtherLib"] +``` +::: + +To instruct Lake to build the documentation database before building the document that refers to it, add a `needs` field to the documentation in the Lake configuration file. +In particular, the package facet `docSource` uses the package's `doc-sources.toml` to create the database. +To avoid problems with circularity, the library that contains the documentation should not be in `doc-sources.toml`. + +:::paragraph +For example, a suitable `needs` field may look like this, where `MyDocs` is a document written in the manual genre: + +``` +lean_lib MyDocs where + needs := #[`@:docSource] +``` +::: + +### Usage + +:::paragraph +The `docstring` command and the `tactic` and `conv` directives have equivalents based on the database. +These equivalents have the same API as the environment-based versions, but they are in the `Verso.Genre.Manual.DocGen` namespace. +The indended mode of use is that the original commands should be hidden when opening the `Verso.Genre.Manual` namespace. +For example: +``` +open Verso Genre +open Verso.Genre.Manual hiding docstring tactic conv +open Verso.Genre.Manual.DocGen +``` +::: + +### Editor Experience + +Before the first `lake build`, `DocGen.docstring` commands show an error directing you to run `lake build`. +After the documentation data has been generated, the editor is fully responsive. +If you change the documented library, running `lake build` again updates the data. + +### Coexistence with Environment-Based Commands + +The doc-gen-sourced commands live in the `Verso.Genre.Manual.DocGen` namespace and do not replace the standard commands. +Projects that document declarations available in their own environment can continue to use `docstring` with no changes. +Both sets of commands produce the same block types, so they can coexist within a single document if needed. + + # Technical Terminology %%% shortTitle := "Glossary" @@ -158,7 +241,6 @@ References to technical terms are valid both before and after their definition s {docstring tech} - # Open-Source Licenses %%% tag := "oss-licenses" diff --git a/doc/UsersGuide/Markup.lean b/doc/UsersGuide/Markup.lean index 33c72b928..171aa0e05 100644 --- a/doc/UsersGuide/Markup.lean +++ b/doc/UsersGuide/Markup.lean @@ -3,14 +3,21 @@ Copyright (c) 2023-2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ +module import Lean.DocString.Syntax +public import Verso.Doc.Elab.Monad +public meta import Verso.Parser +import Verso import VersoManual +public import VersoManual.Basic +import VersoManual.InlineLean.LongLines +public meta import VersoManual.InlineLean.LongLines set_option guard_msgs.diff true open Verso Genre Manual -section +meta section open Lean open Lean.Doc.Syntax @@ -129,7 +136,7 @@ partial def preview (stx : Syntax) : m Std.Format := throwErrorAt stx "Didn't understand {Verso.SyntaxUtils.ppSyntax stx} for preview" end -block_extension MarkupExample (title : String) where +public block_extension MarkupExample (title : String) where data := title traverse _ _ _ := pure none toHtml := some fun _goI goB _id data contents => open Verso.Output.Html in do @@ -266,15 +273,15 @@ open Lean open ArgParse open Doc.Elab -structure MarkupPreviewConfig where +public structure MarkupPreviewConfig where title : StrLit -instance : FromArgs MarkupPreviewConfig DocElabM where +public meta instance : FromArgs MarkupPreviewConfig DocElabM where fromArgs := MarkupPreviewConfig.mk <$> .positional `title .strLit end -private def withNl (s : String) : String := if s.endsWith "\n" then s else s.push '\n' +private meta def withNl (s : String) : String := if s.endsWith "\n" then s else s.push '\n' open Verso Doc Elab in @@ -282,7 +289,7 @@ open Lean Elab in open Verso.Parser in open Lean.Doc.Syntax in @[directive] -def markupPreview : DirectiveExpanderOf MarkupPreviewConfig +public meta def markupPreview : DirectiveExpanderOf MarkupPreviewConfig | {title}, contents => do let #[blk1, blk2] := contents.filter nonempty | throwError "Expected precisely two code blocks, got {contents.filter nonempty}" @@ -324,7 +331,7 @@ where open Lean Verso Doc Elab in open Verso.Parser in @[code_block markupPreview] -def markupPreviewPre : CodeBlockExpanderOf MarkupPreviewConfig +public meta def markupPreviewPre : CodeBlockExpanderOf MarkupPreviewConfig | {title}, contents => do let stx ← blocks {} |>.parseString contents.getString diff --git a/doc/UsersGuide/Output.lean b/doc/UsersGuide/Output.lean index ba2ad0805..4012794ce 100644 --- a/doc/UsersGuide/Output.lean +++ b/doc/UsersGuide/Output.lean @@ -3,11 +3,14 @@ Copyright (c) 2023-2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ +module import Lean.DocString.Syntax -import VersoManual +public import VersoManual import VersoBlog -open Verso Genre Manual +open Verso Genre +open Verso.Genre.Manual hiding docstring tactic conv +open Verso.Genre.Manual.DocGen open Verso.Genre.Blog (Page Post) diff --git a/doc/UsersGuide/Releases.lean b/doc/UsersGuide/Releases.lean index 0d7ae5f24..3bb27a757 100644 --- a/doc/UsersGuide/Releases.lean +++ b/doc/UsersGuide/Releases.lean @@ -3,8 +3,8 @@ Copyright (c) 2026 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Emilio J. Gallego Arias -/ - -import VersoManual +module +public import VersoManual import UsersGuide.Releases.«v4_29_0» import UsersGuide.Releases.«v4_28_0» diff --git a/doc/UsersGuide/Releases/v4_28_0.lean b/doc/UsersGuide/Releases/v4_28_0.lean index 0a7097afa..a95bb2f72 100644 --- a/doc/UsersGuide/Releases/v4_28_0.lean +++ b/doc/UsersGuide/Releases/v4_28_0.lean @@ -3,8 +3,8 @@ Copyright (c) 2026 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Emilio J. Gallego Arias -/ - -import VersoManual +module +public import VersoManual open Verso.Genre diff --git a/doc/UsersGuide/Releases/v4_29_0.lean b/doc/UsersGuide/Releases/v4_29_0.lean index 84326a20b..53d0b774a 100644 --- a/doc/UsersGuide/Releases/v4_29_0.lean +++ b/doc/UsersGuide/Releases/v4_29_0.lean @@ -3,8 +3,8 @@ Copyright (c) 2026 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Emilio J. Gallego Arias -/ - -import VersoManual +module +public import VersoManual open Verso.Genre Manual @@ -18,6 +18,8 @@ file := "v4.29.0" * Fix Verso folding ranges / TOC for Lean.Doc syntax and #doc (#768) * Align Blog inline Lean role naming with Manual; add `{lean}` and deprecate `{leanInline}` (#762) * A zero-config {ref "literate429"}[literate programming] feature was added in [#809](https://github.com/leanprover/verso/pull/809). +* A {ref "docgen429"}[`doc-gen4`-based backend for extracted API docs] was added in [#776](https://github.com/leanprover/verso/pull/776). + # Literate Programming %%% @@ -27,3 +29,14 @@ tag := "literate429" PR [#809](https://github.com/leanprover/verso/pull/809) added support for a simple literate programming system, in which module docstrings are rendered as the text of a page. While no configuration is necessary to use it, aside from adding Verso as a dependency, some configuration is possible in order to customize aspects of the display. See {ref "literate"}[its section in this guide] for more details. + +# Docstrings via `doc-gen4` +%%% +tag := "docgen429" +%%% + +PR [#776](https://github.com/leanprover/verso/pull/776) implements an alternative backend for the docstring features in the manual genre. +Instead of retrieving them from the in-memory Lean environment, they can be read from a SQLite database dumped by `doc-gen4`. +This allows manuals written in Verso to use the Lean module system, which eliminates docstrings from environments for performance reasons, and it can enable features that require a global perspective, such as lists of instances. +This very document now uses this new feature and has enabled the module system. +See {ref "docgen-docstrings"}[its section in this guide] for more details. diff --git a/doc/UsersGuide/Websites.lean b/doc/UsersGuide/Websites.lean index 116214076..71c564896 100644 --- a/doc/UsersGuide/Websites.lean +++ b/doc/UsersGuide/Websites.lean @@ -3,11 +3,15 @@ Copyright (c) 2023-2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ +module import Lean.DocString.Syntax -import VersoManual -import VersoBlog +public import VersoManual +public meta import VersoManual.DB +meta import VersoBlog -open Verso Genre Manual +open Verso Genre +open Verso.Genre.Manual hiding docstring tactic conv +open Verso.Genre.Manual.DocGen open Verso.Genre.Blog (Page Post) @@ -44,7 +48,7 @@ However, their metadata are different: tag := "blogMain" %%% -Blogs should have an executable that invokes `blogMain` on the appropriate {ref "site-config"}[site and theme], forwarding on command-line arguments. +Blogs should have an executable that invokes {name Verso.Genre.Blog.blogMain}`blogMain` on the appropriate {ref "site-config"}[site and theme], forwarding on command-line arguments. It is responsible for {ref "traversal"}[traversing] the site and generating the HTML. {docstring Blog.blogMain} diff --git a/lake-manifest.json b/lake-manifest.json index b2322313d..8f8198de9 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,7 +1,17 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/plausible", + [{"url": "https://github.com/david-christiansen/doc-gen4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "1bec291d9b93db694d25887e9695f5e277102e79", + "name": "«doc-gen4»", + "manifestFile": "lake-manifest.json", + "inputRev": "pp-db", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "", @@ -30,6 +40,46 @@ "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": false, - "configFile": "lakefile.lean"}], + "configFile": "lakefile.lean"}, + {"url": "https://github.com/kim-em/leansqlite", + "type": "git", + "subDir": null, + "scope": "", + "rev": "d14544c72b593af6a66131bc34cdab16bf7c0940", + "name": "leansqlite", + "manifestFile": "lake-manifest.json", + "inputRev": "suppress-reducibility-warning", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "", + "rev": "61cd682f2a25175996bc1b9e8d8231e76cded866", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "scope": "", + "rev": "629254926fb54ef83d582bd41a0b9eb72b934015", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "nightly-testing", + "inherited": true, + "configFile": "lakefile.toml"}], "name": "verso", "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index a3bfd7561..d558cfaaf 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,6 +4,7 @@ open Lake DSL require subverso from git "https://github.com/leanprover/subverso"@"main" require MD4Lean from git "https://github.com/acmepjz/md4lean"@"main" require plausible from git "https://github.com/leanprover-community/plausible"@"main" +require «doc-gen4» from git "https://github.com/david-christiansen/doc-gen4"@"pp-db" package verso where precompileModules := false -- temporarily disabled to work around an issue with nightly-2025-03-30 @@ -136,6 +137,7 @@ lean_exe «verso-demo» where lean_lib UsersGuide where srcDir := "doc" leanOptions := #[⟨`weak.linter.verso.manual.headerTags, true⟩] + needs := #[`@:docSource] @[default_target] lean_exe usersguide where @@ -246,6 +248,41 @@ package_facet literate pkg : Array System.FilePath := do let exes := Job.collectArray (← pkg.leanExes.mapM (·.toLeanLib.facet `literate |>.fetch)) return libs.zipWith (·.flatten ++ ·.flatten) exes +lean_exe «verso-docgen-analyze» where + root := `VersoManual.DB.Analyze + srcDir := "src/verso-manual" + supportInterpreter := true + +package_facet docSource pkg : System.FilePath := do + let ws ← getWorkspace + let exeJob ← «verso-docgen-analyze».fetch + let buildDir := ws.root.buildDir + let tomlPath := ws.root.dir / "doc-sources.toml" + let dbPath := buildDir / "api-docs.db" + + -- The exe reads doc-sources.toml to determine which libraries to analyze. + -- It uses LEAN_PATH to locate their .olean files. + -- We don't depend on those libraries' olean jobs here to avoid build cycles + -- (modules that consume the DB declare `needs := #[`@:docSource]`, which + -- would create a cycle if we also depended on all libraries). + exeJob.mapM fun exeFile => do + addTrace (← computeTrace exeFile) + if ← tomlPath.pathExists then + addTrace (← computeTrace tomlPath) + + buildFileUnlessUpToDate' dbPath do + IO.FS.createDirAll buildDir + let mut args := #[buildDir.toString, "api-docs.db"] + if ← tomlPath.pathExists then + args := args ++ #["--toml", tomlPath.toString] + proc { + cmd := exeFile.toString + args + env := ← getAugmentedEnv + } + + pure dbPath + section variable [Monad m] variable [MonadWorkspace m] [MonadLog m] diff --git a/src/multi-verso/MultiVerso.lean b/src/multi-verso/MultiVerso.lean index 813939ced..6f18af005 100644 --- a/src/multi-verso/MultiVerso.lean +++ b/src/multi-verso/MultiVerso.lean @@ -281,7 +281,7 @@ public structure RefDomain where contents : HashMap String (Array RefObject) deriving Inhabited, Repr -instance : GetElem? RefDomain String (Array RefObject) fun dom name => name ∈ dom.contents where +public instance : GetElem? RefDomain String (Array RefObject) fun dom name => name ∈ dom.contents where getElem dom name ok := dom.contents[name]'ok getElem? dom name := dom.contents[name]? diff --git a/src/multi-verso/MultiVerso/Path.lean b/src/multi-verso/MultiVerso/Path.lean index a7c3135c9..663dc459b 100644 --- a/src/multi-verso/MultiVerso/Path.lean +++ b/src/multi-verso/MultiVerso/Path.lean @@ -32,7 +32,7 @@ Adds {lean}`component` to the end of {name}`path`. public def Path.join (path : Path) (component : String) : Path := Array.push path component -instance : HDiv Path String Path := ⟨Path.join⟩ +public instance : HDiv Path String Path := ⟨Path.join⟩ /-- Retrieves a string that can be used as a link. diff --git a/src/tests/TestMain.lean b/src/tests/TestMain.lean index b182dcf50..92ef2142f 100644 --- a/src/tests/TestMain.lean +++ b/src/tests/TestMain.lean @@ -166,6 +166,16 @@ def testLiterateHtml (_ : Config) : IO Unit := def testLiterateHtmlMultiRoot (_ : Config) : IO Unit := Tests.LiterateHtml.testLiterateHtmlMultiRoot +def testDocSourceConfig (_ : Config) : IO Unit := do + let fails ← runDocSourceConfigTests + if fails > 0 then + throw <| .userError s!"{fails} doc source config tests failed" + +def testIndentColumn (_ : Config) : IO Unit := do + let fails ← runIndentColumnTests + if fails > 0 then + throw <| .userError s!"{fails} indentColumn tests failed" + -- Interactive tests via the LSP server def testInteractive (_ : Config) : IO Unit := do IO.println "Running interactive (LSP) tests..." @@ -266,6 +276,8 @@ open Verso.Integration in def tests := [ testSerialization, testBlog, + testDocSourceConfig, + testIndentColumn, testStemmer, testTexOutput "sample-doc" SampleDoc.doc, testTexOutput "inheritance-doc" InheritanceDoc.doc, diff --git a/src/tests/Tests.lean b/src/tests/Tests.lean index 93f55e65f..f7bd62d2d 100644 --- a/src/tests/Tests.lean +++ b/src/tests/Tests.lean @@ -31,5 +31,8 @@ import Tests.VersoBlog import Tests.VersoManual import Tests.Z85 import Tests.Zip +import Tests.DocSourceConfig +import Tests.IndentColumn +import Tests.UrlSubst import Tests.LiterateConfig import Tests.LiterateHtml diff --git a/src/tests/Tests/DocSourceConfig.lean b/src/tests/Tests/DocSourceConfig.lean new file mode 100644 index 000000000..a463a4f4a --- /dev/null +++ b/src/tests/Tests/DocSourceConfig.lean @@ -0,0 +1,98 @@ +/- +Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +import Lake.Toml +import VersoManual.DB.Config + +/-! +# Tests for Documentation Source Configuration Parsing + +Tests for `Verso.Genre.Manual.DocSource.Config` — TOML parsing for `doc-sources.toml`. + +This file describes the libraries that are being documented in a Verso project. The libraries should +be available in the current workspace. +-/ + +open Verso.Genre.Manual.DocSource +open Lake.Toml + +/-- Parses a TOML string into a `Table`. Throws on parse error. -/ +private def parseToml (input : String) : IO Table := do + let ictx := Lean.Parser.mkInputContext input "" + match (← Lake.Toml.loadToml ictx |>.toBaseIO) with + | .ok table => pure table + | .error msgs => + let msgStrs ← msgs.toList.mapM fun msg => msg.data.toString + throw <| .userError s!"TOML parse error:\n{"\n".intercalate msgStrs}" + +/-- Checks that two values are equal, throwing a descriptive error if not. -/ +private def assertEqual [BEq α] [Repr α] (label : String) (expected actual : α) : IO Unit := do + unless expected == actual do + throw <| IO.userError s!"{label}: expected\n {repr expected}\nbut got\n {repr actual}" + +-- ============================================================================ +-- Config.ofToml tests +-- ============================================================================ + +private def testEmptyConfig : IO Unit := do + let table ← parseToml "" + let config ← IO.ofExcept <| Config.ofToml table + assertEqual "empty config libraries" #[] config.libraries + assertEqual "empty config includeCore" true config.includeCore + +private def testLibrariesField : IO Unit := do + let table ← parseToml " +libraries = [\"Mathlib\", \"Batteries\"] +" + let config ← IO.ofExcept <| Config.ofToml table + assertEqual "libraries" #["Mathlib", "Batteries"] config.libraries + +private def testLibrariesOnly : IO Unit := do + let table ← parseToml " +libraries = [\"Init\"] +" + let config ← IO.ofExcept <| Config.ofToml table + assertEqual "libraries only" #["Init"] config.libraries + +private def testIncludeCore : IO Unit := do + let table ← parseToml " +include_core = false +" + let config ← IO.ofExcept <| Config.ofToml table + assertEqual "includeCore" false config.includeCore + +private def testIncludeCoreFalse : IO Unit := do + let table ← parseToml " +include_core = false +libraries = [\"Foo\"] +" + let config ← IO.ofExcept <| Config.ofToml table + assertEqual "includeCore false" false config.includeCore + assertEqual "libraries with core false" #["Foo"] config.libraries + +-- ============================================================================ +-- Test runner +-- ============================================================================ + +private def docSourceConfigTests : List (String × IO Unit) := [ + ("Config.ofToml: empty config", testEmptyConfig), + ("Config.ofToml: libraries field", testLibrariesField), + ("Config.ofToml: libraries only", testLibrariesOnly), + ("Config.ofToml: include_core true", testIncludeCore), + ("Config.ofToml: include_core false", testIncludeCoreFalse), +] + +public def runDocSourceConfigTests : IO Nat := do + IO.println "Running doc source config tests..." + let mut failures := 0 + for (name, test) in docSourceConfigTests do + IO.print s!" {name}: " + try + test + IO.println "ok" + catch e => + IO.println s!"FAIL\n {e}" + failures := failures + 1 + return failures diff --git a/src/tests/Tests/IndentColumn.lean b/src/tests/Tests/IndentColumn.lean new file mode 100644 index 000000000..455243abe --- /dev/null +++ b/src/tests/Tests/IndentColumn.lean @@ -0,0 +1,52 @@ +/- +Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +import VersoManual.Docstring.Show + +open Verso.Genre.Manual + +private def assertEqual (label : String) (expected actual : Nat) : IO Unit := do + unless expected == actual do + throw <| IO.userError s!"{label}: expected {expected} but got {actual}" + +private def testIndentColumnEmpty : IO Unit := + assertEqual "empty string" 0 (indentColumn "") + +private def testIndentColumnNoIndent : IO Unit := + assertEqual "no indent" 0 (indentColumn "abc") + +private def testIndentColumnSimple : IO Unit := + assertEqual "simple indent" 3 (indentColumn " abc") + +private def testIndentColumnUniform : IO Unit := + assertEqual "uniform indent" 3 (indentColumn " abc\n\n def") + +private def testIndentColumnMinimum : IO Unit := + assertEqual "minimum indent" 2 (indentColumn " abc\n\n def") + +private def testIndentColumnMultiline : IO Unit := + assertEqual "multiline minimum" 2 (indentColumn " abc\n\n def\n a") + +private def indentColumnTests : List (String × IO Unit) := [ + ("indentColumn: empty string", testIndentColumnEmpty), + ("indentColumn: no indent", testIndentColumnNoIndent), + ("indentColumn: simple indent", testIndentColumnSimple), + ("indentColumn: uniform indent", testIndentColumnUniform), + ("indentColumn: minimum indent", testIndentColumnMinimum), + ("indentColumn: multiline minimum", testIndentColumnMultiline), +] + +public def runIndentColumnTests : IO Nat := do + IO.println "Running indentColumn tests..." + let mut failures := 0 + for (name, test) in indentColumnTests do + IO.print s!" {name}: " + try + test + IO.println "ok" + catch e => + IO.println s!"FAIL\n {e}" + failures := failures + 1 + return failures diff --git a/src/tests/Tests/UrlSubst.lean b/src/tests/Tests/UrlSubst.lean new file mode 100644 index 000000000..bf25f4acd --- /dev/null +++ b/src/tests/Tests/UrlSubst.lean @@ -0,0 +1,12 @@ +/- +Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +import VersoBlog.LiterateLeanPage + +open Verso.Genre.Blog.Literate.Internal + +/-- info: some (Except.ok "foo/foo/bar/baz/f.png") -/ +#guard_msgs in +#eval (url_subst "xy/" z "/static/" pic ".jpg" => "foo/" z "/" pic ".png") "xy/foo/static/bar/baz/f.jpg" diff --git a/src/verso-blog/VersoBlog.lean b/src/verso-blog/VersoBlog.lean index e8664c1ff..48fbb7802 100644 --- a/src/verso-blog/VersoBlog.lean +++ b/src/verso-blog/VersoBlog.lean @@ -3,24 +3,41 @@ Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ +module +public meta import Lean.Data.FuzzyMatching import SubVerso.Highlighting import SubVerso.Examples +public import SubVerso.Module +public meta import SubVerso.Examples.Messages +public import SubVerso.Examples.Env +public import SubVerso.Examples import VersoBlog.Basic -import VersoBlog.LiterateLeanPage +public import VersoBlog.NameSuffixMap +public meta import VersoBlog.NameSuffixMap +public import VersoBlog.LiterateLeanPage import VersoBlog.LiterateModuleDocs import VersoBlog.Generate import VersoBlog.Site import VersoBlog.Site.Syntax import VersoBlog.Template -import VersoBlog.Theme -import VersoBlog.Traverse -import Verso.Doc.ArgParse +public import VersoBlog.Theme +public import VersoBlog.Traverse +public import Verso.Code.Highlighted +public import Verso.Doc.ArgParse +public import Verso.Doc.Elab.Block +public import Verso.Doc.Elab.Inline +public import Verso.Doc.Elab.Monad import Verso.Doc.Lsp import Verso.Doc.Suggestion +public import Verso.Doc.Suggestion.Basic +import Verso.FS import Verso.Hover -import Verso.WithoutAsync +public meta import Verso.Output.Html +public meta import Verso.WithoutAsync +public section + open Verso.Output Html namespace Verso.Genre.Blog @@ -32,17 +49,14 @@ open Lean Elab open Verso.SyntaxUtils (parserInputString) open SubVerso.Examples (loadExamples Example) -open SubVerso.Examples.Messages (messagesMatch) open SubVerso.Module (ModuleItem) -def classArgs : ArgParse DocElabM String := .named `«class» .string false - -structure ClassArgs where +meta structure ClassArgs where «class» : String section variable [Monad m] [MonadError m] -instance : FromArgs ClassArgs m where +meta instance : FromArgs ClassArgs m where fromArgs := ClassArgs.mk <$> .named `«class» .string false end @@ -50,7 +64,7 @@ end Wraps the contents in an HTML `` element with the provided `class`. -/ @[role] -def htmlSpan : RoleExpanderOf ClassArgs +meta def htmlSpan : RoleExpanderOf ClassArgs | {«class»}, stxs => do let contents ← stxs.mapM elabInline ``(Inline.other (Blog.InlineExt.htmlSpan $(quote «class»)) #[$contents,*]) @@ -60,13 +74,13 @@ def htmlSpan : RoleExpanderOf ClassArgs Wraps the contents in an HTML `
` element with the provided `class`. -/ @[directive] -def htmlDiv : DirectiveExpanderOf ClassArgs +meta def htmlDiv : DirectiveExpanderOf ClassArgs | {«class»}, stxs => do let contents ← stxs.mapM elabBlock ``(Block.other (Blog.BlockExt.htmlDiv $(quote «class»)) #[ $contents,* ]) -private partial def attrs : ArgParse DocElabM (Array (String × String)) := List.toArray <$> .many attr +meta partial def attrs : ArgParse DocElabM (Array (String × String)) := List.toArray <$> .many attr where attr : ArgParse DocElabM (String × String) := (fun (k, v) => (k.getId.toString (escape := false), v)) <$> .anyNamed `attribute .string @@ -75,12 +89,12 @@ structure HtmlArgs where name : Name attrs : Array (String × String) -instance : FromArgs HtmlArgs DocElabM where +meta instance : FromArgs HtmlArgs DocElabM where fromArgs := HtmlArgs.mk <$> .positional `name .name <*> attrs @[directive] -def html : DirectiveExpanderOf HtmlArgs +meta def html : DirectiveExpanderOf HtmlArgs | {name, attrs}, stxs => do let tag := name.toString (escape := false) let contents ← stxs.mapM elabBlock @@ -89,18 +103,18 @@ def html : DirectiveExpanderOf HtmlArgs structure BlobArgs where blobName : Ident -instance : FromArgs BlobArgs DocElabM where +meta instance : FromArgs BlobArgs DocElabM where fromArgs := BlobArgs.mk <$> .positional `blobName .ident @[directive] -def blob : DirectiveExpanderOf BlobArgs +meta def blob : DirectiveExpanderOf BlobArgs | {blobName}, stxs => do if h : stxs.size > 0 then logErrorAt stxs[0] "Expected no contents" let actualName ← realizeGlobalConstNoOverloadWithInfo blobName ``(Block.other (Blog.BlockExt.blob ($(mkIdentFrom blobName actualName) : Html)) #[]) @[role blob] -def inlineBlob : RoleExpanderOf BlobArgs +meta def inlineBlob : RoleExpanderOf BlobArgs | {blobName}, stxs => do if h : stxs.size > 0 then logErrorAt stxs[0] "Expected no contents" let actualName ← realizeGlobalConstNoOverloadWithInfo blobName @@ -109,17 +123,17 @@ def inlineBlob : RoleExpanderOf BlobArgs structure LabelArgs where label : Name -instance : FromArgs LabelArgs DocElabM where +meta instance : FromArgs LabelArgs DocElabM where fromArgs := LabelArgs.mk <$> .positional `blobName .name @[role] -def label : RoleExpanderOf LabelArgs +meta def label : RoleExpanderOf LabelArgs | {label}, stxs => do let args ← stxs.mapM elabInline ``(Inline.other (Blog.InlineExt.label $(quote label)) #[ $[ $args ],* ]) @[role] -def ref : RoleExpanderOf LabelArgs +meta def ref : RoleExpanderOf LabelArgs | {label}, stxs => do let args ← stxs.mapM elabInline ``(Inline.other (Blog.InlineExt.ref $(quote label)) #[ $[ $args ],* ]) @@ -128,70 +142,19 @@ structure PageLinkArgs where page : Name id? : Option String -instance : FromArgs PageLinkArgs DocElabM where +meta instance : FromArgs PageLinkArgs DocElabM where fromArgs := PageLinkArgs.mk <$> .positional `page .name <*> (some <$> .positional `id .string <|> pure none) @[role] -def page_link : RoleExpanderOf PageLinkArgs +meta def page_link : RoleExpanderOf PageLinkArgs | {page, id?}, stxs => do let inls ← stxs.mapM elabInline ``(Inline.other (Blog.InlineExt.pageref $(quote page) $(quote id?)) #[ $[ $inls ],* ]) --- The assumption here is that suffixes are _mostly_ unique, so the arrays will likely be very --- small. -structure NameSuffixMap (α : Type) : Type where - contents : Lean.NameMap (Array (Name × α)) := {} -deriving Inhabited - -def NameSuffixMap.empty : NameSuffixMap α := {} - -def NameSuffixMap.insert (map : NameSuffixMap α) (key : Name) (val : α) : NameSuffixMap α := Id.run do - let some last := key.components.getLast? - | map - let mut arr := map.contents.find? last |>.getD #[] - for h : i in [0:arr.size] do - have : i < arr.size := by get_elem_tactic - if arr[i].fst == key then - return {map with contents := map.contents.insert last (arr.set i (key, val))} - return {map with contents := map.contents.insert last (arr.push (key, val))} - -def NameSuffixMap.toArray (map : NameSuffixMap α) : Array (Name × α) := Id.run do - let mut arr := #[] - for (_, arr') in map.contents.toList do - arr := arr ++ arr' - arr.qsort (fun x y => x.fst.toString < y.fst.toString) - -def NameSuffixMap.toList (map : NameSuffixMap α) : List (Name × α) := map.toArray.toList - -def NameSuffixMap.get (map : NameSuffixMap α) (key : Name) : Array (Name × α) := Id.run do - let ks := key.componentsRev - let some k' := ks.head? - | #[] - let some candidates := map.contents.find? k' - | #[] - let mut result := none - for (n, c) in candidates do - match matchLength ks n.componentsRev, result with - | none, _ => continue - | some l, none => result := some (l, #[(n, c)]) - | some l, some (l', found) => - if l > l' then result := some (l, #[(n, c)]) - else if l == l' then result := some (l', found.push (n, c)) - else continue - let res := result.map Prod.snd |>.getD #[] - res.qsort (fun x y => x.fst.toString < y.fst.toString) -where - matchLength : List Name → List Name → Option Nat - | [], _ => some 0 - | _ :: _, [] => none - | x::xs, y::ys => - if x == y then - matchLength xs ys |>.map (· + 1) - else none section @@ -201,29 +164,29 @@ inductive LeanExampleData where | module (positioned : Array ModuleItem) deriving Inhabited -structure ExampleContext where +meta structure ExampleContext where contexts : Lean.NameMap LeanExampleData := {} deriving Inhabited -initialize exampleContextExt : EnvExtension ExampleContext ← registerEnvExtension (pure {}) +meta initialize exampleContextExt : EnvExtension ExampleContext ← registerEnvExtension (pure {}) -structure ExampleMessages where +meta structure ExampleMessages where messages : NameSuffixMap ((Environment × MessageLog) ⊕ List (MessageSeverity × String)) := {} deriving Inhabited -initialize messageContextExt : EnvExtension ExampleMessages ← registerEnvExtension (pure {}) +meta initialize messageContextExt : EnvExtension ExampleMessages ← registerEnvExtension (pure {}) initialize registerTraceClass `Elab.Verso.block.lean -def leanExampleProject.Args := Name × String +@[expose] meta def leanExampleProject.Args := Name × String -instance : FromArgs leanExampleProject.Args DocElabM := +meta instance : FromArgs leanExampleProject.Args DocElabM := ⟨(·, ·) <$> .positional `name .name <*> .positional `projectDir .string⟩ open System in @[block_command] -def leanExampleProject : BlockCommandOf leanExampleProject.Args +meta def leanExampleProject : BlockCommandOf leanExampleProject.Args | (name, projectDir) => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"Loading example project") <| do if exampleContextExt.getState (← getEnv) |>.contexts |>.contains name then throwError "Example context '{name}' already defined in this module" @@ -244,13 +207,14 @@ def leanExampleProject : BlockCommandOf leanExampleProject.Args Verso.Hover.addCustomHover (← getRef) <| "Contains:\n" ++ String.join (savedExamples.toList.map (s!" * `{toString ·.fst}`\n")) ``(Block.concat #[]) -def leanExampleModule.Args := Name × String × Name -instance : FromArgs leanExampleModule.Args DocElabM := +@[expose] meta def leanExampleModule.Args := Name × String × Name + +meta instance : FromArgs leanExampleModule.Args DocElabM := ⟨(·, ·, ·) <$> .positional `name .name <*> .positional `projectDir .string <*> .positional `module .name⟩ open System in @[block_command] -def leanExampleModule : BlockCommandOf leanExampleModule.Args +meta def leanExampleModule : BlockCommandOf leanExampleModule.Args | (name, projectDir, module) => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"Loading example project") <| do if exampleContextExt.getState (← getEnv) |>.contexts |>.contains name then throwError "Example context '{name}' already defined in this module" @@ -265,7 +229,7 @@ def leanExampleModule : BlockCommandOf leanExampleModule.Args ``(Block.concat #[]) -private def getSubproject (project : Ident) : TermElabM (NameSuffixMap Example) := do +private meta def getSubproject (project : Ident) : TermElabM (NameSuffixMap Example) := do let some ctxt := exampleContextExt.getState (← getEnv) |>.contexts |>.find? project.getId | throwErrorAt project "Subproject '{project}' not loaded" let .subproject projectExamples := ctxt @@ -273,14 +237,14 @@ private def getSubproject (project : Ident) : TermElabM (NameSuffixMap Example) Verso.Hover.addCustomHover project <| "Contains:\n" ++ String.join (projectExamples.toList.map (s!" * `{toString ·.fst}`\n")) pure projectExamples -private def getModule (project : Ident) : TermElabM (Array ModuleItem) := do +private meta def getModule (project : Ident) : TermElabM (Array ModuleItem) := do let some ctxt := exampleContextExt.getState (← getEnv) |>.contexts |>.find? project.getId | throwErrorAt project "Subproject '{project}' not loaded" let .module modExamples := ctxt | throwErrorAt project "'{project}' is not loaded as a subproject" pure modExamples -def NameSuffixMap.getOrSuggest [Monad m] [MonadInfoTree m] [MonadError m] +meta def NameSuffixMap.getOrSuggest [Monad m] [MonadInfoTree m] [MonadError m] (map : NameSuffixMap α) (key : Ident) : m (Name × α) := do match map.get key.getId with | #[(n', v)] => @@ -306,13 +270,13 @@ structure LeanCommandConfig where section variable [Monad m] [MonadError m] [MonadLiftT CoreM m] -instance : FromArgs LeanCommandConfig m where +meta instance : FromArgs LeanCommandConfig m where fromArgs := LeanCommandConfig.mk <$> .positional `project .ident <*> .positional `exampleName .ident <*> .flag `showProofStates true end @[block_command] -def leanCommand : BlockCommandOf LeanCommandConfig +meta def leanCommand : BlockCommandOf LeanCommandConfig | { project, exampleName, showProofStates } => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"leanCommand") <| do let projectExamples ← getSubproject project let (_, {highlighted := hls, original := str, ..}) ← projectExamples.getOrSuggest exampleName @@ -324,10 +288,10 @@ structure LeanCommandAtArgs where line : Nat endLine? : Option Nat -instance [Monad m] [MonadError m] : FromArgs LeanCommandAtArgs m where +meta instance [Monad m] [MonadError m] : FromArgs LeanCommandAtArgs m where fromArgs := LeanCommandAtArgs.mk <$> .positional `project .ident <*> .positional `line .nat <*> (some <$> .positional `endLine .nat <|> pure none) -private def useRange (startLine : Nat) (endLine? : Option Nat) (range : Position × Position) : Bool := +private meta def useRange (startLine : Nat) (endLine? : Option Nat) (range : Position × Position) : Bool := let startLine' := range.1.line let endLine' := range.2.line if let some endLine := endLine? then @@ -336,7 +300,7 @@ private def useRange (startLine : Nat) (endLine? : Option Nat) (range : Position startLine ≥ startLine' && startLine ≤ endLine' -- point is in region @[block_command] -def leanCommandAt : BlockCommandOf LeanCommandAtArgs +meta def leanCommandAt : BlockCommandOf LeanCommandAtArgs | {project, line, endLine?} => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"leanCommand") <| do let projectExamples ← getModule project @@ -359,11 +323,11 @@ def leanCommandAt : BlockCommandOf LeanCommandAtArgs structure NoArgs where -instance : FromArgs NoArgs m where +meta instance : FromArgs NoArgs m where fromArgs := pure ⟨⟩ @[role] -def leanKw : RoleExpanderOf NoArgs +meta def leanKw : RoleExpanderOf NoArgs | ⟨⟩, #[arg] => do let `(inline|code( $kw:str )) := arg | throwErrorAt arg "Expected code literal with the keyword" @@ -379,14 +343,14 @@ structure LeanTermArgs where project : Ident showProofStates : Bool -instance : FromArgs LeanTermArgs DocElabM where +meta instance : FromArgs LeanTermArgs DocElabM where fromArgs := LeanTermArgs.mk <$> .positional `project .ident <*> .flag `showProofStates true @[role] -def leanTerm : RoleExpanderOf LeanTermArgs +meta def leanTerm : RoleExpanderOf LeanTermArgs | {project, showProofStates}, #[arg] => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"leanTerm") <| do let `(inline|code( $name:str )) := arg | throwErrorAt arg "Expected code literal with the example name" @@ -411,7 +375,7 @@ structure LeanBlockConfig where /-- Whether to render proof states -/ showProofStates : Bool -instance [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : FromArgs LeanBlockConfig m where +meta instance [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : FromArgs LeanBlockConfig m where fromArgs := LeanBlockConfig.mk <$> .positional `exampleContext .ident <*> @@ -421,9 +385,9 @@ instance [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadErr .flag `error false "Error expected in code?" <*> .flag `showProofStates true "Show proof states in rendered page?" -def LeanInitBlockConfig := LeanBlockConfig +@[expose] def LeanInitBlockConfig := LeanBlockConfig -instance [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : FromArgs LeanInitBlockConfig m where +meta instance [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : FromArgs LeanInitBlockConfig m where fromArgs := LeanBlockConfig.mk <$> .positional `exampleContext .ident <*> @@ -435,7 +399,7 @@ instance [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadErr @[code_block] -def leanInit : CodeBlockExpanderOf LeanInitBlockConfig +meta def leanInit : CodeBlockExpanderOf LeanInitBlockConfig | config , str => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"leanInit") <| do let context := Parser.mkInputContext (← parserInputString str) (← getFileName) let (header, state, msgs) ← Parser.parseHeader context @@ -468,7 +432,7 @@ where open SubVerso.Highlighting Highlighted in @[code_block] -def lean : CodeBlockExpanderOf LeanBlockConfig +meta def lean : CodeBlockExpanderOf LeanBlockConfig | config, str => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"lean block") <| withoutAsync do let x := config.exampleContext let (commandState, state) ← match exampleContextExt.getState (← getEnv) |>.contexts.find? x.getId with @@ -535,7 +499,7 @@ structure LeanInlineConfig where /-- Universe variables allowed in the term -/ universes : Option StrLit -instance [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : FromArgs LeanInlineConfig m where +meta instance [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : FromArgs LeanInlineConfig m where fromArgs := LeanInlineConfig.mk <$> .positional `exampleContext .ident <*> .named `type strLit true <*> .named `universes strLit true where strLit : ValDesc m StrLit := { @@ -551,7 +515,7 @@ open Lean Elab Command in Runs an elaborator action with the current namespace and open declarations that have been found via inline Lean blocks. -/ -def runWithOpenDecls (scopes : List Scope) (act : TermElabM α) : TermElabM α := do +meta def runWithOpenDecls (scopes : List Scope) (act : TermElabM α) : TermElabM α := do let scope := scopes.head! withTheReader Core.Context ({· with currNamespace := scope.currNamespace, openDecls := scope.openDecls}) do let initNames := (← getThe Term.State).levelNames @@ -568,7 +532,7 @@ Runs an elaborator action with the section variables that have been established This is a version of `Lean.Elab.Command.runTermElabM`. -/ -def runWithVariables (scopes : List Scope) (elabFn : Array Expr → TermElabM α) : TermElabM α := do +meta def runWithVariables (scopes : List Scope) (elabFn : Array Expr → TermElabM α) : TermElabM α := do let scope := scopes.head! Term.withAutoBoundImplicit do let msgLog ← Core.getMessageLog @@ -599,7 +563,7 @@ where modifyInfoState fun s => { s with trees := f s.trees } open SubVerso.Highlighting Highlighted in -private def leanInlineImpl : RoleExpanderOf LeanInlineConfig +private meta def leanInlineImpl : RoleExpanderOf LeanInlineConfig | config, elts => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"lean block") <| do let #[code] := elts | throwError "Expected precisely one code element" @@ -675,11 +639,11 @@ private def leanInlineImpl : RoleExpanderOf LeanInlineConfig `(Inline.other (Blog.InlineExt.highlightedCode { contextName := $(quote config.exampleContext.getId) } $(quote hls)) #[Inline.code $(quote str.getString)]) @[role lean] -def leanCanonical : RoleExpanderOf LeanInlineConfig := +meta def leanCanonical : RoleExpanderOf LeanInlineConfig := leanInlineImpl @[role] -def leanInline : RoleExpanderOf LeanInlineConfig +meta def leanInline : RoleExpanderOf LeanInlineConfig | config, elts => do if h : 0 < elts.size then logWarningAt elts[0] "`{leanInline}` is deprecated; use `{lean}` instead." @@ -696,7 +660,7 @@ structure LeanOutputConfig where summarize : Bool whitespace : WhitespaceMode -instance [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : FromArgs LeanOutputConfig m where +meta instance [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : FromArgs LeanOutputConfig m where fromArgs := LeanOutputConfig.mk <$> .positional `name output <*> @@ -726,7 +690,7 @@ private def leanOutputInline [bg : BlogGenre genre] (message : Highlighted.Messa .other (bg.inline_eq ▸ InlineExt.message message expandTraces) #[.code message.toString] @[code_block] -def leanOutput : CodeBlockExpanderOf LeanOutputConfig +meta def leanOutput : CodeBlockExpanderOf LeanOutputConfig | config, str => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"leanOutput") <| do let (_, savedInfo) ← messageContextExt.getState (← getEnv) |>.messages |>.getOrSuggest config.name let messages ← match savedInfo with @@ -788,7 +752,7 @@ where pure <| withNewline <| head ++ (← message.data.toString) mostlyEqual (ws : WhitespaceMode) (s1 s2 : String) : Bool := - messagesMatch (ws.apply s1.trimAscii.copy) (ws.apply s2.trimAscii.copy) + SubVerso.Examples.Messages.messagesMatch (ws.apply s1.trimAscii.copy) (ws.apply s2.trimAscii.copy) open Lean Elab Command in elab "define_lexed_text" blockName:ident " ← " lexerName:ident : command => do @@ -893,7 +857,7 @@ instance [bg : BlogGenre genre] : ExternalCode genre where .other (bg.inline_eq ▸ InlineExt.highlightedCode { cfg with contextName := `verso } hl) #[] leanBlock hl cfg := .other (bg.block_eq ▸ BlockExt.highlightedCode { cfg with contextName := `verso } hl) #[] - leanOutputInline message plain (expandTraces := []) := + leanOutputInline message plain (expandTraces := []) := private leanOutputInline message plain (expandTraces := expandTraces) - leanOutputBlock message (summarize := false) (expandTraces : List Name := []) := + leanOutputBlock message (summarize := false) (expandTraces : List Name := []) := private leanOutputBlock message (summarize := summarize) (expandTraces := expandTraces) diff --git a/src/verso-blog/VersoBlog/Basic.lean b/src/verso-blog/VersoBlog/Basic.lean index 4ef70da16..eb54fae18 100644 --- a/src/verso-blog/VersoBlog/Basic.lean +++ b/src/verso-blog/VersoBlog/Basic.lean @@ -3,22 +3,25 @@ Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ -import Lean.Data.Json.FromToJson +module +public import Lean.Data.Json.FromToJson.Basic import Std.Data.HashMap import Std.Data.HashSet -import SubVerso.Highlighting - +public import SubVerso.Highlighting import Verso.Code -import Verso.Doc +public import Verso.Doc import Verso.Doc.Html +public import Verso.Output.Html import Verso.Method -import MultiVerso - +public import MultiVerso +public import MultiVerso.Path +public import MultiVerso.Slug -import VersoBlog.LexedText +public import VersoBlog.LexedText +public section open Std (HashSet HashMap) open Lean (Json ToJson FromJson) @@ -288,6 +291,7 @@ deriving Repr, BEq, ToJson, FromJson /-- An ordinary web page that is not a blog post. -/ +@[expose] def Page : Genre where PartMetadata := Page.Meta Block := Blog.BlockExt @@ -326,6 +330,7 @@ deriving TypeName, Repr /-- A blog post. -/ +@[expose] def Post : Genre where PartMetadata := Post.Meta Block := Blog.BlockExt diff --git a/src/verso-blog/VersoBlog/Component.lean b/src/verso-blog/VersoBlog/Component.lean index c49db2188..6d80f9d76 100644 --- a/src/verso-blog/VersoBlog/Component.lean +++ b/src/verso-blog/VersoBlog/Component.lean @@ -3,10 +3,16 @@ Copyright (c) 2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ -import VersoBlog.Basic -import VersoBlog.Component.Ext +module +public import VersoBlog.Basic +public import VersoBlog.Component.Ext import Verso.Doc.ArgParse -import Std.Data.HashSet +public import Verso.Doc.Html +import Verso.Doc.Elab.Monad +import Verso.Doc.Elab.Block +public import Std.Data.HashSet.Basic +public meta import VersoBlog.Component.Ext +public section open Verso Genre Blog open Verso.Doc @@ -142,7 +148,7 @@ def Components.fromLists (blocks : List (Name × BlockComponent)) (inlines : Lis inlines := .ofList (inlines.map fun (x, b) => (x, Dynamic.mk b)) _ open Lean in -private def nameAndDef [Monad m] [MonadRef m] [MonadQuotation m] (ext : Name × Name) : m Term := do +private meta def nameAndDef [Monad m] [MonadRef m] [MonadQuotation m] (ext : Name × Name) : m Term := do let quoted : Term := quote ext.fst let ident ← mkCIdentFromRef ext.snd `(($quoted, $(⟨ident⟩))) @@ -173,7 +179,7 @@ scoped elab "%registered_inline_components" : term => do open Lean.Parser Term in -def extContents := structInstFields (sepByIndent Term.structInstField "; " (allowTrailingSep := true)) +meta def extContents := structInstFields (sepByIndent Term.structInstField "; " (allowTrailingSep := true)) /-- Defines a new block component. @@ -210,7 +216,7 @@ def argType : Lean.TSyntax ``Lean.Parser.Term.bracketedBinder → Option Term | _ => none open Lean in -def argNamesTypes : Lean.TSyntax ``Lean.Parser.Term.bracketedBinder → Array (Ident × Term) +meta def argNamesTypes : Lean.TSyntax ``Lean.Parser.Term.bracketedBinder → Array (Ident × Term) | `(bracketedBinder| ($xs* : $t) ) | `(bracketedBinder| {$xs* : $t} ) | `(bracketedBinder| ⦃$xs* : $t⦄ ) => xs.filterMap getIdents |>.map ((·, t)) @@ -222,7 +228,7 @@ where open Lean Elab Command in -def splitToHtml (fields : Array (TSyntax ``Lean.Parser.Term.structInstField)) : +meta def splitToHtml (fields : Array (TSyntax ``Lean.Parser.Term.structInstField)) : CommandElabM (Option Term × Array (TSyntax ``Lean.Parser.Term.structInstField)) := do let (is, isNot) := fields.partition fun | `(Lean.Parser.Term.structInstField|toHtml) => true @@ -254,7 +260,7 @@ where `(_) open Lean in -def deJson [Monad m] [MonadQuotation m] +meta def deJson [Monad m] [MonadQuotation m] (b : Ident × Term) : m (TSyntax `Lean.Parser.Term.doSeqItem) := let (x, t) := b `(Lean.Parser.Term.doSeqItem| let $x ← match FromJson.fromJson? (α := $t) $x with @@ -307,7 +313,7 @@ elab_rules : command ``((·, ·) <$> ArgParse.positional $(quote x.getId) (FromArgVal.fromArgVal (α := $t)) <*> $y) let argT ← argNames.foldrM (init := ← `(Unit)) fun (_, t) y => `($t × $y) elabCommand (← `(def T := $argT)) - elabCommand (← `(instance : FromArgs T DocElabM := ⟨$argP⟩)) + elabCommand (← `(instance : FromArgs T Verso.Doc.Elab.DocElabM := ⟨$argP⟩)) let qArgs : Term ← argNames.foldlM (init := x) fun tm (x, _) => `($tm $$(quote $x)) let cmd3 ← diff --git a/src/verso-blog/VersoBlog/Component/Ext.lean b/src/verso-blog/VersoBlog/Component/Ext.lean index 719b4493a..4bd3ea8f9 100644 --- a/src/verso-blog/VersoBlog/Component/Ext.lean +++ b/src/verso-blog/VersoBlog/Component/Ext.lean @@ -3,12 +3,13 @@ Copyright (c) 2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ -import Lean.Environment +module +public import Lean.Environment open Lean namespace Verso.Genre.Blog -initialize blockComponentExt : +public initialize blockComponentExt : PersistentEnvExtension (Name × Name) (Name × Name) (NameMap Name) ← registerPersistentEnvExtension { mkInitial := pure {}, @@ -18,7 +19,7 @@ initialize blockComponentExt : es.foldl (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1) } -initialize inlineComponentExt : +public initialize inlineComponentExt : PersistentEnvExtension (Name × Name) (Name × Name) (NameMap Name) ← registerPersistentEnvExtension { mkInitial := pure {}, diff --git a/src/verso-blog/VersoBlog/Generate.lean b/src/verso-blog/VersoBlog/Generate.lean index 7d95cb60c..3814bfeae 100644 --- a/src/verso-blog/VersoBlog/Generate.lean +++ b/src/verso-blog/VersoBlog/Generate.lean @@ -3,11 +3,16 @@ Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ - +module import Verso.FS -import VersoBlog.Basic +public import Verso.Doc.Html +public import VersoBlog.Basic +public import VersoBlog.Site import VersoBlog.Template -import VersoBlog.Theme +public import VersoBlog.Theme +public import VersoBlog.Traverse +import MultiVerso +public section open Verso Doc Output Html HtmlT FS open Verso.Code.Hover (State) diff --git a/src/verso-blog/VersoBlog/LexedText.lean b/src/verso-blog/VersoBlog/LexedText.lean index 414cb34f4..92cd8d100 100644 --- a/src/verso-blog/VersoBlog/LexedText.lean +++ b/src/verso-blog/VersoBlog/LexedText.lean @@ -3,9 +3,13 @@ Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ -import Lean.Parser -import Lean.Data.Json.FromToJson -import Verso.Instances.Deriving +module +public import Lean.Parser +public import Lean.Data.Json.FromToJson.Basic +meta import Verso.Instances.Deriving +import Verso.Instances +import Lean.DocString.Parser +public section open Lean (ToJson FromJson) @@ -63,4 +67,4 @@ def highlight (hl : Highlighter) (str : String) : IO LexedText := do pure ⟨hl.name, out⟩ def token (kind : Name) (p : ParserFn) : ParserFn := - nodeFn kind <| Lean.Doc.Parser.ignoreFn p + nodeFn kind <| Doc.Parser.ignoreFn p diff --git a/src/verso-blog/VersoBlog/LiterateLeanPage.lean b/src/verso-blog/VersoBlog/LiterateLeanPage.lean index 6cc2c45f9..12e47edd3 100644 --- a/src/verso-blog/VersoBlog/LiterateLeanPage.lean +++ b/src/verso-blog/VersoBlog/LiterateLeanPage.lean @@ -3,12 +3,18 @@ Copyright (c) 2023-2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ -import SubVerso.Helper -import SubVerso.Module +module +public meta import SubVerso.Helper +public meta import SubVerso.Module import Verso.Doc.Concrete +public meta import Verso.Doc.Elab.Inline +public import Verso.Doc.Elab.Monad +public meta import Verso.Parser import VersoBlog.Basic import VersoBlog.LiterateLeanPage.Options -import MD4Lean +public meta import VersoBlog.LiterateLeanPage.Options +public meta import MD4Lean +public section open Verso Doc open Lean @@ -24,7 +30,7 @@ structure LitPageConfig where header : Bool := false open System in -def loadModuleContent +meta def loadModuleContent (leanProject : FilePath) (mod : String) (overrideToolchain : Option String := none) : IO (Array ModuleItem) := do @@ -94,7 +100,7 @@ structure Helper where highlight (term : String) (type? : Option String) : IO Highlighted open System in -def Helper.fromModule +meta def Helper.fromModule (leanProject : FilePath) (mod : String) (overrideToolchain : Option String := none) : IO Helper := do @@ -191,11 +197,11 @@ where decorateOut "stderr" res.stderr -def loadLiteratePage (root : System.FilePath) (module : String) : IO (Array ModuleItem) := do +meta def loadLiteratePage (root : System.FilePath) (module : String) : IO (Array ModuleItem) := do loadModuleContent root module -inductive Pat where +meta inductive Pat where | char : Char → Pat | str : String → Pat | var : Name → Pat @@ -203,7 +209,7 @@ inductive Pat where deriving BEq, Hashable, Repr, Inhabited -- TODO rewrite with dynamic programming -partial def Pat.match (p : List Pat) (str : String) : Option (Lean.NameMap String) := +meta partial def Pat.match (p : List Pat) (str : String) : Option (Lean.NameMap String) := go str.startPos p where go iter @@ -244,12 +250,12 @@ where continue failure -inductive Template where +meta inductive Template where | str : String → Template | var : Name → Template deriving BEq, Hashable, Repr, Inhabited -def Template.subst (vars : Lean.NameMap String) : Template → Except String String +meta def Template.subst (vars : Lean.NameMap String) : Template → Except String String | .str s => pure s | .var x => if let some s := vars.find? x then pure s else throw s!"Not found: '{x}'" @@ -278,11 +284,7 @@ macro_rules | `(term|url_subst $pat* => $template*) => `(fun s => url_subst(s) $pat* => $template*) -/-- info: some (Except.ok "foo/foo/bar/baz/f.png") -/ -#guard_msgs in -#eval (url_subst "xy/" z "/static/" pic ".jpg" => "foo/" z "/" pic ".png") "xy/foo/static/bar/baz/f.jpg" - -def getSubst [Monad m] : TSyntax ``url_case → m (List Pat × List Template) +meta def getSubst [Monad m] : TSyntax ``url_case → m (List Pat × List Template) | `(url_case|$pat* => $template*) => do let pat := pat.map fun | `(url_pattern| *) => Pat.any @@ -297,18 +299,13 @@ def getSubst [Monad m] : TSyntax ``url_case → m (List Pat × List Template) pure (pat.toList, template.toList) | c => panic! s!"Didn't understand case {c}" - -/-- info: some (Except.ok "foo/foo/bar/baz/f.png") -/ -#guard_msgs in -#eval (url_subst "xy/" z "/static/" pic ".jpg" => "foo/" z "/" pic ".png") "xy/foo/static/bar/baz/f.jpg" - end Internal section variable [Monad m] [MonadError m] [MonadQuotation m] -partial def getModuleDocString (hl : Highlighted) : m String := do +meta partial def getModuleDocString (hl : Highlighted) : m String := do let str := (← getString hl).trimAscii let str := str.dropPrefix "/-!" |>.dropSuffix "-/" |>.trimAscii |>.copy pure str @@ -321,7 +318,7 @@ where getString : Highlighted → m String | .token ⟨_, txt⟩ => pure txt end -def getFirstMessage : Highlighted → Option (Highlighted.Span.Kind × Highlighted.MessageContents Highlighted) +meta def getFirstMessage : Highlighted → Option (Highlighted.Span.Kind × Highlighted.MessageContents Highlighted) | .span msgs x => msgs[0]? <|> getFirstMessage x | .point k m => pure (k, m) @@ -351,7 +348,7 @@ partial def examplesFromMod [Monad m] [MonadError m] open Elab PartElabM in open Lean.Parser.Command in -partial def docFromMod (project : System.FilePath) (mod : String) +meta partial def docFromMod (project : System.FilePath) (mod : String) (config : LitPageConfig) (content : Array ModuleItem) (rewriter : Array (List Pat × List Template)) : PartElabM Unit := do let mut mdHeaders : Array Nat := #[] @@ -494,7 +491,7 @@ syntax rewrites := "rewriting " ("| " url_case)+ open Verso Doc in open Lean Elab Command in open PartElabM in -def elabLiteratePage (x : Ident) (path : StrLit) (mod : Ident) (config : LitPageConfig) (title : StrLit) (genre : Term) (metadata? : Option Term) (rw : Option (TSyntax ``rewrites)) : CommandElabM Unit := +meta def elabLiteratePage (x : Ident) (path : StrLit) (mod : Ident) (config : LitPageConfig) (title : StrLit) (genre : Term) (metadata? : Option Term) (rw : Option (TSyntax ``rewrites)) : CommandElabM Unit := withTraceNode `verso.blog.literate (fun _ => pure m!"Literate '{title.getString}'") do let rewriter ← rw.mapM fun @@ -590,8 +587,9 @@ prevented elaboration of inline elements. syntax "def_literate_post " ident optConfig " from " ident " in " str " as " str (" with " term)? (rewrites)? : command - +meta section declare_config_elab litPageConfig LitPageConfig +end open Verso Doc in open Lean Elab Command in diff --git a/src/verso-blog/VersoBlog/LiterateLeanPage/Options.lean b/src/verso-blog/VersoBlog/LiterateLeanPage/Options.lean index 114aabea2..ad220a798 100644 --- a/src/verso-blog/VersoBlog/LiterateLeanPage/Options.lean +++ b/src/verso-blog/VersoBlog/LiterateLeanPage/Options.lean @@ -3,7 +3,9 @@ Copyright (c) 2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ -import Lean.Data.Options +module +public import Lean.Data.Options +public section open Lean MonadOptions diff --git a/src/verso-blog/VersoBlog/LiterateModuleDocs.lean b/src/verso-blog/VersoBlog/LiterateModuleDocs.lean index 7a0beaf75..585c50521 100644 --- a/src/verso-blog/VersoBlog/LiterateModuleDocs.lean +++ b/src/verso-blog/VersoBlog/LiterateModuleDocs.lean @@ -3,13 +3,19 @@ Copyright (c) 2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ +module import SubVerso.Helper import SubVerso.Module -import VersoBlog.Basic +public import Verso.Doc.Concrete +public import Verso.Doc.Elab.Monad +public import VersoBlog.Basic import VersoBlog.LiterateLeanPage.Options import MD4Lean import VersoLiterate -import Lean.Compiler.LCNF.ConfigOptions +public import VersoLiterate.Module +public import VersoLiterate.Basic +public meta import Lean.Compiler.LCNF.ConfigOptions +public section set_option doc.verso true @@ -49,7 +55,7 @@ variable [Monad m] [MonadError m] [MonadQuotation m] open Verso Doc in open Lean Elab Command Term in open PartElabM in -def elabFromModuleDocs (x : Ident) (path : StrLit) (mod : Ident) (title : StrLit) (genre : Term) (metadata? : Option Term) : CommandElabM Unit := +meta def elabFromModuleDocs (x : Ident) (path : StrLit) (mod : Ident) (title : StrLit) (genre : Term) (metadata? : Option Term) : CommandElabM Unit := withTraceNode `verso.blog.literate (fun _ => pure m!"Literate '{title.getString}'") do let titleParts ← stringToInlines title diff --git a/src/verso-blog/VersoBlog/NameSuffixMap.lean b/src/verso-blog/VersoBlog/NameSuffixMap.lean new file mode 100644 index 000000000..2ec3253f2 --- /dev/null +++ b/src/verso-blog/VersoBlog/NameSuffixMap.lean @@ -0,0 +1,98 @@ +/- +Copyright (c) 2024-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +module +import Lean.Data.NameMap.Basic + +set_option linter.missingDocs true +set_option doc.verso true + +open Lean + +/-! +# Name Suffix Maps + +A map keyed by {lean}`Name` that supports lookup by suffix. When a key is inserted, only the last +component of the name is used as the index, so looking up a suffix like {lit}`foo` can match +{lit}`A.B.foo`. Among matches, longer suffix overlap is preferred, and ties are returned together, +sorted lexicographically. +-/ + +namespace Verso.Genre.Blog + +/-- +A map from {name}`Name` to {name}`α` that supports suffix-based lookup. + +Internally, entries are indexed by the last component of their key. Because name suffixes are +mostly unique, the per-bucket arrays are expected to be very small. +-/ +public structure NameSuffixMap (α : Type) : Type where + private contents : Lean.NameMap (Array (Name × α)) := {} + +/-- The empty {name}`NameSuffixMap`. -/ +public def NameSuffixMap.empty : NameSuffixMap α := {} + +/-- +The empty {name}`NameSuffixMap` can written “{lean (type := "NameSuffixMap α")}`∅`”. +-/ +public instance : EmptyCollection (NameSuffixMap α) := ⟨NameSuffixMap.empty⟩ + +public instance : Inhabited (NameSuffixMap α) := ⟨{}⟩ + +/-- Inserts a key-value pair, replacing any existing entry with the same key. -/ +public def NameSuffixMap.insert (map : NameSuffixMap α) (key : Name) (val : α) : NameSuffixMap α := Id.run do + let some last := key.components.getLast? + | map + let mut arr := map.contents.find? last |>.getD #[] + for h : i in [0:arr.size] do + have : i < arr.size := by get_elem_tactic + if arr[i].fst == key then + return { map with contents := map.contents.insert last (arr.set i (key, val)) } + return { map with contents := map.contents.insert last (arr.push (key, val)) } + +/-- Returns all entries as an array, sorted by key. -/ +public def NameSuffixMap.toArray (map : NameSuffixMap α) : Array (Name × α) := Id.run do + let mut arr := #[] + for (_, arr') in map.contents.toList do + arr := arr ++ arr' + arr.qsort (fun x y => x.fst.toString < y.fst.toString) + +/-- Returns all entries as a list, sorted by key. -/ +public def NameSuffixMap.toList (map : NameSuffixMap α) : List (Name × α) := map.toArray.toList + +/-- +Looks up entries whose key has {name}`key` as a suffix. Among candidates sharing the same last +component, those with the longest matching suffix (as determined by number of components in the +name, not string length) are returned. If multiple entries tie for the longest match, all of them +are returned, sorted lexicographically by key. +-/ +public def NameSuffixMap.get (map : NameSuffixMap α) (key : Name) : Array (Name × α) := Id.run do + let ks := key.componentsRev + let some k' := ks.head? + | #[] + let some candidates := map.contents.find? k' + | #[] + let mut result := none + for (n, c) in candidates do + match matchLength ks n.componentsRev, result with + | none, _ => continue + | some l, none => result := some (l, #[(n, c)]) + | some l, some (l', found) => + if l > l' then result := some (l, #[(n, c)]) + else if l == l' then result := some (l', found.push (n, c)) + else continue + let res := result.map Prod.snd |>.getD #[] + res.qsort (fun x y => x.fst.toString < y.fst.toString) +where + matchLength : List Name → List Name → Option Nat + | [], _ => some 0 + | _ :: _, [] => none + | x::xs, y::ys => + if x == y then + matchLength xs ys |>.map (· + 1) + else none + +public instance : GetElem (NameSuffixMap α) Name (Array (Name × α)) (fun _ _ => True) where + getElem map key _ := map.get key diff --git a/src/verso-blog/VersoBlog/Site.lean b/src/verso-blog/VersoBlog/Site.lean index 0c3b9ab48..b6e66f562 100644 --- a/src/verso-blog/VersoBlog/Site.lean +++ b/src/verso-blog/VersoBlog/Site.lean @@ -3,10 +3,12 @@ Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ - +module import Verso.Doc -import VersoBlog.Basic +import Verso.Method +public import VersoBlog.Basic import VersoBlog.Traverse +public section open Verso Doc diff --git a/src/verso-blog/VersoBlog/Site/Syntax.lean b/src/verso-blog/VersoBlog/Site/Syntax.lean index 3273b4dc3..c63f01930 100644 --- a/src/verso-blog/VersoBlog/Site/Syntax.lean +++ b/src/verso-blog/VersoBlog/Site/Syntax.lean @@ -3,9 +3,12 @@ Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ - +module +public import Lean.ResolveName import Verso.Doc.Concrete +public import Verso.Doc.DocName import VersoBlog.Site +public section open Lean Elab Macro Term diff --git a/src/verso-blog/VersoBlog/Template.lean b/src/verso-blog/VersoBlog/Template.lean index b14112874..fc18d42d7 100644 --- a/src/verso-blog/VersoBlog/Template.lean +++ b/src/verso-blog/VersoBlog/Template.lean @@ -3,19 +3,24 @@ Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ - +module import Std.Data.HashSet import SubVerso.Highlighting import Verso.Doc +public import Verso.Doc.DocName +import Verso.Method import Verso.Doc.Html +public import Verso.Instances import VersoBlog.Basic -import VersoBlog.Site -import VersoBlog.Component -import Verso.Output.Html +public import VersoBlog.Site +public import VersoBlog.Component +public import VersoBlog.LexedText +public import Verso.Output.Html import Verso.Output.Html.CssVars import Verso.Code +public section open Std (HashSet TreeMap) @@ -51,7 +56,7 @@ instance : Coe Html Template.Params.Val where | other => ⟨.mk other, #[]⟩ -def Params := TreeMap String Params.Val +@[expose] def Params := TreeMap String Params.Val instance : EmptyCollection Params := inferInstanceAs <| EmptyCollection (TreeMap _ _ _) @@ -271,7 +276,7 @@ def blogGenreHtml inline := bg.inline_eq ▸ inlineHtml g -private def mkHd (htmlId : Option String) (lvl : Nat) (contents : Html) : Html := +def mkHd (htmlId : Option String) (lvl : Nat) (contents : Html) : Html := mkPartHeader lvl contents (htmlId.map (fun x => #[("id", x)]) |>.getD #[]) instance : GenreHtml Page ComponentM := blogGenreHtml Page fun go metadata part => diff --git a/src/verso-blog/VersoBlog/Theme.lean b/src/verso-blog/VersoBlog/Theme.lean index 9604771e0..adfa45178 100644 --- a/src/verso-blog/VersoBlog/Theme.lean +++ b/src/verso-blog/VersoBlog/Theme.lean @@ -3,9 +3,10 @@ Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ - +module import VersoBlog.Site -import VersoBlog.Template +public import VersoBlog.Template +public section open Verso.Genre.Blog Template open Verso Doc Output Html diff --git a/src/verso-blog/VersoBlog/Traverse.lean b/src/verso-blog/VersoBlog/Traverse.lean index 6887791b4..a54d922bf 100644 --- a/src/verso-blog/VersoBlog/Traverse.lean +++ b/src/verso-blog/VersoBlog/Traverse.lean @@ -3,8 +3,11 @@ Copyright (c) 2023-2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ -import VersoBlog.Basic -import VersoBlog.Component +module +public import Verso.Code +public import VersoBlog.Basic +public import VersoBlog.Component +public section open Verso Code Highlighted WebAssets diff --git a/src/verso-literate/VersoLiterate/Module.lean b/src/verso-literate/VersoLiterate/Module.lean index 2507d7ba3..519b41345 100644 --- a/src/verso-literate/VersoLiterate/Module.lean +++ b/src/verso-literate/VersoLiterate/Module.lean @@ -40,7 +40,7 @@ def modToPage! [LoadLiterate g] (mod : LitMod) (title : Array (Inline g)) (title | .ok v => v open System in -def loadModuleJson +meta def loadModuleJson (leanProject : FilePath) (mod : String) (overrideToolchain : Option String := none) : IO String := do diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean index ab43b0b7d..52eaec608 100644 --- a/src/verso-manual/VersoManual.lean +++ b/src/verso-manual/VersoManual.lean @@ -3,11 +3,17 @@ Copyright (c) 2023-2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ - -import Verso.Doc -import Verso.Doc.Concrete +module +import Verso.CLI +public import Verso.Doc +public import Verso.Doc.ArgParse +public import Verso.Doc.Concrete +public meta import Verso.Doc.Elab.Block +public meta import Verso.Doc.Elab.Inline +public import Verso.Doc.Elab.Monad import Verso.Doc.TeX import Verso.Doc.Html +import Verso.Method import Verso.Output.TeX import Verso.Output.Html import Verso.Output.Html.CssVars @@ -16,32 +22,38 @@ import Verso.Output.Html.ElasticLunr import Verso.Doc.Lsp import Verso.Doc.Elab import Verso.FS +public meta import Verso.Linters import VersoSearch import MultiVerso -import VersoManual.Basic +public import VersoManual.Basic +public import VersoManual.DB import VersoManual.TeX -import VersoManual.TeX.Config +public import VersoManual.TeX.Config import VersoManual.Html -import VersoManual.Html.Style -import VersoManual.Draft -import VersoManual.Imports -import VersoManual.Index -import VersoManual.License -import VersoManual.Glossary -import VersoManual.Docstring +public import VersoManual.Html.Config +public import VersoManual.Html +public import VersoManual.Html.Style +public import VersoManual.Draft +public import VersoManual.Imports +public import VersoManual.Index +public import VersoManual.License +public import VersoManual.Glossary +public import VersoManual.Docstring import VersoManual.WebAssets import VersoManual.WordCount -import VersoManual.Linters +public import VersoManual.Linters import VersoManual.LocalContents -import VersoManual.InlineLean -import VersoManual.ExternalLean -import VersoManual.Literate -import VersoManual.Marginalia -import VersoManual.Bibliography -import VersoManual.Table +public import VersoManual.InlineLean +public import VersoManual.ExternalLean +public import VersoManual.Literate +public import VersoManual.Marginalia +public import VersoManual.Bibliography +public import VersoManual.Table +import VersoManual.DB +public section open Lean (Name NameMap Json ToJson FromJson quote) @@ -75,7 +87,7 @@ deriving BEq, ToJson, FromJson defmethod Part.htmlToc (part : Part Manual) : Bool := part.metadata.map (·.htmlToc) |>.getD true -inline_extension Inline.ref (canonicalName : String) (domain : Option Name) (remote : Option String) (resolvedDestination : Option Link := none) where +public inline_extension Inline.ref (canonicalName : String) (domain : Option Name) (remote : Option String) (resolvedDestination : Option Link := none) where data := ToJson.toJson (RefInfo.mk canonicalName domain remote resolvedDestination) traverse := fun _ info content => do match FromJson.fromJson? (α := RefInfo) info with @@ -149,7 +161,7 @@ structure RoleArgs where domain : Option Name remote : Option String := none -instance : FromArgs RoleArgs m where +meta instance : FromArgs RoleArgs m where fromArgs := RoleArgs.mk <$> .positional `canonicalName (ValDesc.string.as "canonical name (string literal)") <*> @@ -169,12 +181,12 @@ end Inserts a reference to the provided tag. -/ @[role] -def ref : RoleExpanderOf RoleArgs +meta def ref : RoleExpanderOf RoleArgs | {canonicalName, domain, remote}, content => do let content ← content.mapM elabInline ``(Inline.other (Inline.ref $(quote canonicalName) $(quote domain) $(quote remote)) #[$content,*]) -block_extension Block.paragraph where +public block_extension Block.paragraph where traverse := fun _ _ _ => pure none toTeX := some <| fun _ go _ _ content => do @@ -191,7 +203,7 @@ paragraph. In HTML output, they are rendered with less space between them, and L a single paragraph (e.g. without extraneous indentation). -/ @[directive] -def paragraph : DirectiveExpanderOf Unit +meta def paragraph : DirectiveExpanderOf Unit | (), stxs => do let args ← stxs.mapM elabBlock ``(Block.other Block.paragraph #[ $[ $args ],* ]) @@ -414,7 +426,8 @@ def emitTeX (logError : String → IO Unit) (config : Config) (text : Part Manua open Verso.Output (Html) -instance : Inhabited (StateT (State Html) (ReaderT ExtensionImpls IO) Html.Toc) where +open Verso.Genre.Manual.Html in +instance : Inhabited (StateT (State Html) (ReaderT ExtensionImpls IO) Toc) where default := fun _ => default diff --git a/src/verso-manual/VersoManual/Basic.lean b/src/verso-manual/VersoManual/Basic.lean index 6aa0b2698..98814922a 100644 --- a/src/verso-manual/VersoManual/Basic.lean +++ b/src/verso-manual/VersoManual/Basic.lean @@ -809,7 +809,7 @@ meta def extContents := structInstFields (sepByIndent Term.structInstField "; " Defines a new block extension. ``` -block_extension NAME PARAMS [via MIXINS,+] where +public block_extension NAME PARAMS [via MIXINS,+] where data := ... fields* ``` @@ -824,12 +824,12 @@ The remaining fields are used to define traversal and output generation for the block descriptor is then processed by `MIXINS`, from left to right, before being added to the block descriptor table. -/ -syntax "block_extension" ident (ppSpace bracketedBinder)* (&" via " ident,+)? ppIndent(ppSpace "where" extContents) : command +syntax (visibility)? "block_extension" ident (ppSpace bracketedBinder)* (&" via " ident,+)? ppIndent(ppSpace "where" extContents) : command /-- Defines a new inline extension. ``` -inline_extension NAME PARAMS [via MIXINS,+] where +public inline_extension NAME PARAMS [via MIXINS,+] where data := ... fields* ``` @@ -844,7 +844,7 @@ The remaining fields are used to define traversal and output generation for the resulting inline descriptor is then processed by `MIXINS`, from left to right, before being added to the inline descriptor table. -/ -syntax "inline_extension" ident (ppSpace bracketedBinder)* (&" via " ident,+)? ppIndent(ppSpace "where" extContents) : command +syntax (visibility)? "inline_extension" ident (ppSpace bracketedBinder)* (&" via " ident,+)? ppIndent(ppSpace "where" extContents) : command meta def isDataField : Lean.TSyntax ``Lean.Parser.Term.structInstField → Bool | `(Lean.Parser.Term.structInstField|data := $_) => true @@ -853,13 +853,13 @@ meta def isDataField : Lean.TSyntax ``Lean.Parser.Term.structInstField → Bool open Lean Elab Command in elab_rules : command - | `(block_extension $x $args* $[via $mixins,*]? where $contents;*) => do + | `($[$v]? block_extension $x $args* $[via $mixins,*]? where $contents;*) => do let (data, nonData) := (contents : Array _).partition isDataField if data.size > 1 then for x in data do logErrorAt x "Multiple 'data' fields found" let cmd1 ← - `(command| def $x $args* : Block where $data;*) + `(command| $[$v:visibility]? def $x $args* : Block where $data;*) let innerDescrName := x.getId ++ `descr.inner |> mkIdentFrom x let descrName := x.getId ++ `descr |> mkIdentFrom x let applyMixins (x : Term) : CommandElabM Term := @@ -878,13 +878,13 @@ elab_rules : command open Lean Elab Command in elab_rules : command - | `(inline_extension $x $args* $[via $mixins,*]? where $contents;*) => do + | `($[$v]? inline_extension $x $args* $[via $mixins,*]? where $contents;*) => do let (data, nonData) := (contents : Array _).partition isDataField if data.size > 1 then for x in data do logErrorAt x "Multiple 'data' fields found" let cmd1 ← - `(command| def $x $args* : Inline where $data;*) + `(command| $[$v:visibility]? def $x $args* : Inline where $data;*) let innerDescrName := x.getId ++ `descr.inner |> mkIdentFrom x let descrName := x.getId ++ `descr |> mkIdentFrom x let applyMixins (x : Term) : CommandElabM Term := diff --git a/src/verso-manual/VersoManual/Bibliography.lean b/src/verso-manual/VersoManual/Bibliography.lean index 950ed6f0d..1e28d27f4 100644 --- a/src/verso-manual/VersoManual/Bibliography.lean +++ b/src/verso-manual/VersoManual/Bibliography.lean @@ -3,17 +3,20 @@ Copyright (c) 2024 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ - +module import Lean.Data.Json import Lean.Elab.InfoTree.Types +public meta import Verso.Doc.Elab.Inline +public import Verso.Doc.Elab.Monad +public meta import Verso.Doc.Elab.Monad import Verso.Output.Html import Verso.Output.TeX import MultiVerso.Path import MultiVerso.Slug -import VersoManual.Basic -import VersoManual.Marginalia - +public import VersoManual.Basic +public import VersoManual.Marginalia +public section open Lean Elab open Verso Doc Elab Html @@ -352,7 +355,7 @@ private partial def cmpCite : Json → Json → Ordering (arrayOrd inst).compare a1 a2 -inline_extension Inline.cite (citations : List Citable) (style : Style := .parenthetical) where +public inline_extension Inline.cite (citations : List Citable) (style : Style := .parenthetical) where -- The nested bit here _should_ be a no-op, but it's to avoid deserialization overhead during the traverse pass data := ToJson.toJson (ToJson.toJson citations, style) traverse _ data _ := do @@ -390,19 +393,18 @@ inline_extension Inline.cite (citations : List Citable) (style : Style := .paren | .ok (v' : List Citable) => Citable.inlineHtml go v' v.2 -structure CiteConfig where +public structure CiteConfig where citations : List Name section variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] [MonadFileMap m] -partial def CiteConfig.parse : ArgParse m CiteConfig := - CiteConfig.mk <$> many1 (.positional `citation .resolvedName) +public meta instance : FromArgs CiteConfig m where + fromArgs := + CiteConfig.mk <$> many1 (.positional `citation .resolvedName) where many1 p := (· :: ·) <$> p <*> .many p -instance : FromArgs CiteConfig m where - fromArgs := CiteConfig.parse end @@ -413,19 +415,19 @@ export Verso.Genre.Manual.Bibliography (InProceedings Thesis ArXiv Article) open Bibliography @[role] -def citep : RoleExpanderOf CiteConfig +public meta def citep : RoleExpanderOf CiteConfig | config, extra => do let xs := config.citations.map mkIdent |>.toArray ``(Doc.Inline.other (Inline.cite ([$xs,*] : List Citable) Style.parenthetical) #[$(← extra.mapM elabInline),*]) @[role] -def citet : RoleExpanderOf CiteConfig +public meta def citet : RoleExpanderOf CiteConfig | config, extra => do let xs := config.citations.map mkIdent |>.toArray ``(Doc.Inline.other (Inline.cite ([$xs,*] : List Citable) Style.textual) #[$(← extra.mapM elabInline),*]) @[role] -def citehere : RoleExpanderOf CiteConfig +public meta def citehere : RoleExpanderOf CiteConfig | config, extra => do let xs := config.citations.map mkIdent |>.toArray ``(Doc.Inline.other (Inline.cite ([$xs,*] : List Citable) Style.here) #[$(← extra.mapM elabInline),*]) diff --git a/src/verso-manual/VersoManual/DB.lean b/src/verso-manual/VersoManual/DB.lean new file mode 100644 index 000000000..90e1e3615 --- /dev/null +++ b/src/verso-manual/VersoManual/DB.lean @@ -0,0 +1,10 @@ +/- +Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +module +import VersoManual.DB.Config +import VersoManual.DB.Convert +public meta import VersoManual.DB.Query +public import VersoManual.DB.Docstring diff --git a/src/verso-manual/VersoManual/DB/Analyze.lean b/src/verso-manual/VersoManual/DB/Analyze.lean new file mode 100644 index 000000000..4051b18dd --- /dev/null +++ b/src/verso-manual/VersoManual/DB/Analyze.lean @@ -0,0 +1,141 @@ +/- +Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +module +import DocGen4.DB + +import DocGen4.Load +import Lean.DocString +import Lean.Parser.Extension +import SQLite +import VersoManual.DB +import VersoManual.DB.Config + + + +public section + +/-! +# Documentation Extraction + +Executable that runs doc-gen4's analysis on pre-built `.olean` files and writes the results to a +SQLite database. Called by the `docSource` Lake package facet. + +Usage: `verso-docgen-analyze [--toml ] [ ...]` +-/ + +open DocGen4 Process +open Lean + +/-- +Collects conv tactics from the environment and writes them to the database. +-/ +private def saveConvTactics (env : Environment) (buildDir dbFile : String) : IO Unit := do + let dbPath : System.FilePath := buildDir / dbFile + let sqlite ← SQLite.open dbPath.toString + sqlite.exec + "CREATE TABLE IF NOT EXISTS conv_tactics ( + module_name TEXT NOT NULL, + internal_name TEXT NOT NULL, + user_name TEXT NOT NULL, + doc_string TEXT NOT NULL, + PRIMARY KEY (module_name, internal_name) + )" + let stmt ← sqlite.prepare + "INSERT OR IGNORE INTO conv_tactics (module_name, internal_name, user_name, doc_string) VALUES (?, ?, ?, ?)" + let some convs := (Parser.parserExtension.getState env).categories.find? `conv + | return + for ⟨kind, ()⟩ in convs.kinds do + let some modIdx := env.getModuleIdxFor? kind | continue + let moduleName := env.header.moduleNames[modIdx]! + let docString := (← findDocString? env kind).getD "" + let userName := kind.getString! + stmt.bind 1 moduleName.toString + stmt.bind 2 kind.toString + stmt.bind 3 userName + stmt.bind 4 docString + let _ ← stmt.step + stmt.reset + stmt.clearBindings + +/-- Flushes the write-ahead-log so the database file is self-contained. -/ +private def walCheckpoint (dbPath : System.FilePath) : IO Unit := do + let db ← SQLite.open dbPath.toString + db.exec "PRAGMA wal_checkpoint(TRUNCATE)" + db.exec "PRAGMA optimize" + +private structure Args where + /-- The Lake build directory containing `.olean` and `.ilean` files. -/ + buildDir : String + /-- Path to the SQLite database file to write. -/ + dbFile : String + /-- Optional path to a TOML configuration file for doc-source overrides. -/ + tomlPath : Option System.FilePath + /-- The list of root module names to analyze. -/ + modules : List Lean.Name +deriving Inhabited + +private def parseArgs : List String → IO Args + | buildDir :: dbFile :: rest => do + let mut tomlPath : Option System.FilePath := none + let mut moduleArgs : List String := [] + let mut remaining := rest + while !remaining.isEmpty do + match remaining with + | "--toml" :: path :: tail => + tomlPath := some ⟨path⟩ + remaining := tail + | arg :: tail => + moduleArgs := moduleArgs ++ [arg] + remaining := tail + | [] => break + pure { + buildDir, dbFile, tomlPath + modules := moduleArgs.map String.toName + } + | _ => throw <| .userError + "Usage: verso-docgen-analyze [--toml ] [ ...]" + +def main (args : List String) : IO UInt32 := do + let opts ← parseArgs args + + -- Read configuration from doc-sources.toml if provided + let config ← do + if let some tomlPath := opts.tomlPath then + Verso.Genre.Manual.DocSource.Config.load tomlPath + else + pure {} + let allModules := opts.modules ++ config.libraries.toList.map String.toName + + if allModules.isEmpty && !config.includeCore then + IO.eprintln "No modules to analyze. Provide module names or a --toml config." + return 1 + + -- Generate core documentation (Init, Std, Lake, Lean) + if config.includeCore then + for coreModule in [`Init, `Std, `Lake, `Lean] do + IO.println s!"Analyzing core module: {coreModule}" + let doc ← load <| .analyzePrefixModules coreModule + updateModuleDb DB.builtinDocstringValues doc opts.buildDir opts.dbFile none + + -- Generate documentation for specified modules (each as a prefix analysis) + for mod in allModules do + IO.println s!"Analyzing module prefix: {mod}" + let doc ← load <| .analyzePrefixModules mod + updateModuleDb DB.builtinDocstringValues doc opts.buildDir opts.dbFile none + + -- Collect and store conv tactics (not yet handled by doc-gen4) + let allPrefixes := (if config.includeCore then [`Init, `Std, `Lake, `Lean] else []) ++ allModules + if !allPrefixes.isEmpty then + IO.println "Collecting conv tactics..." + let env ← DocGen4.envOfImports allPrefixes.toArray + saveConvTactics env opts.buildDir opts.dbFile + + -- Flush WAL so the database file is self-contained for readers + let dbPath : System.FilePath := opts.buildDir / opts.dbFile + walCheckpoint dbPath + + IO.println s!"Documentation database ready at {dbPath}" + return 0 diff --git a/src/verso-manual/VersoManual/DB/Config.lean b/src/verso-manual/VersoManual/DB/Config.lean new file mode 100644 index 000000000..f31b3f958 --- /dev/null +++ b/src/verso-manual/VersoManual/DB/Config.lean @@ -0,0 +1,68 @@ +/- +Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +module +import Lake.Toml +public import Lake.Toml.Data.Value +public section + +/-! +# Document Source Configuration + +Parsing for `doc-sources.toml`, which declares which libraries' documentation should be built by +the `docSource` Lake package facet and thus made available in Verso documents. +-/ + +namespace Verso.Genre.Manual.DocSource + +open Lake.Toml + +/-- Parsed contents of a `doc-sources.toml` file. -/ +structure Config where + /-- Which library targets to process. -/ + libraries : Array String := #[] + /-- + Whether to include declarations from the Lean core libraries (`Init`, `Std`, `Lake`, `Lean`). + -/ + includeCore : Bool := true +deriving Repr, BEq, Inhabited + +/-- Extracts a `String` from a TOML `Value`, or throws if it's not a string. -/ +private def tomlString : Value → Except String String + | .string _ s => pure s + | v => throw s!"expected string, got {v}" + +/-- Extracts an `Array String` from a TOML array of strings. -/ +private def tomlStringArray : Value → Except String (Array String) + | .array _ vs => vs.mapM tomlString + | v => throw s!"expected array of strings, got {v}" + +/-- Extracts a `Bool` from a TOML `Value`, or throws if it's not a boolean. -/ +private def tomlBool : Value → Except String Bool + | .boolean _ b => pure b + | v => throw s!"expected boolean, got {v}" + +/-- Parses a `Config` from a TOML `Table`. -/ +def Config.ofToml (table : Table) : Except String Config := do + let libraries ← match table.find? `libraries with + | some v => tomlStringArray v + | none => pure #[] + let includeCore ← match table.find? `include_core with + | some v => tomlBool v + | none => pure true + pure { libraries, includeCore } + +/-- Loads and parses a `doc-sources.toml` file. -/ +def Config.load (filePath : System.FilePath) : IO Config := do + let input ← IO.FS.readFile filePath + let ictx := Lean.Parser.mkInputContext input filePath.toString + match (← Lake.Toml.loadToml ictx |>.toBaseIO) with + | .ok table => + match Config.ofToml table with + | .ok config => pure config + | .error e => throw <| .userError s!"Error parsing {filePath}: {e}" + | .error msgs => + let msgStrs ← msgs.toList.mapM fun msg => msg.data.toString + throw <| .userError s!"Error parsing {filePath}:\n{"\n".intercalate msgStrs}" diff --git a/src/verso-manual/VersoManual/DB/Convert.lean b/src/verso-manual/VersoManual/DB/Convert.lean new file mode 100644 index 000000000..776e08dfa --- /dev/null +++ b/src/verso-manual/VersoManual/DB/Convert.lean @@ -0,0 +1,138 @@ +/- +Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +module +public import DocGen4.RenderedCode +public import SubVerso.Highlighting.Highlighted +public section + +namespace Verso.Genre.Manual.DB + +open DocGen4 (RenderedCode FormatCode SortFormer) +open SubVerso.Highlighting (Highlighted Token) + +/-- Extracts plain text content from a `RenderedCode` tree, discarding all tags. -/ +partial def renderedCodeText : RenderedCode → String + | .text s => s + | .tag _ inner => renderedCodeText inner + | .append xs => String.join (xs.toList.map renderedCodeText) + +/-- +Converts a `RenderedCode` value to a `Highlighted` value (for Verso's rendering pipeline). + +The `localVars` parameter (from `FormatCode.localVars`) maps local variable indices to +`(userName, typeFormat?)`. When a `.localVar idx isBinder` tag is encountered, a +`Token.Kind.var` token is emitted with the variable's type rendered as plain text. + +The `constInfo` parameter provides hover data for known constants: a map from `Name` to +`(signature, docstring?)`. +-/ +partial def renderedCodeToHighlighted + (constInfo : Lean.NameMap (String × Option String) := {}) + (localVars : Array (Lean.Name × Option Lean.Format) := #[]) : + RenderedCode → Highlighted + | .text s => .text s + | .tag t inner => + let content := renderedCodeText inner + match t with + | .keyword => .token ⟨.keyword none none none, content⟩ + | .string => .token ⟨.str content, content⟩ + | .const name => + let (sig, doc?) := constInfo.find? name |>.getD ("", none) + .token ⟨.const name sig doc? false none, content⟩ + | .sort _former => .token ⟨.sort none, content⟩ + | .localVar idx _isBinder => + match localVars[idx]? with + | some (userName, typeFmt?) => + let typeStr := typeFmt?.map (·.pretty) |>.getD "" + -- Use the userName as FVarId since we don't have real FVarIds from the DB + .token ⟨.var ⟨userName⟩ typeStr none, content⟩ + | none => renderedCodeToHighlighted constInfo localVars inner + | .otherExpr => renderedCodeToHighlighted constInfo localVars inner + | .append xs => .seq (xs.map (renderedCodeToHighlighted constInfo localVars)) + +/-- Collects all constant names referenced in a `RenderedCode` tree. -/ +partial def renderedCodeConstNames (acc : Lean.NameSet := {}) : RenderedCode → Lean.NameSet + | .text _ => acc + | .tag (.const name) inner => renderedCodeConstNames (acc.insert name) inner + | .tag _ inner => renderedCodeConstNames acc inner + | .append xs => xs.foldl (init := acc) fun a x => renderedCodeConstNames a x + +/-- Extracts plain text from a `FormatCode` by rendering at the given width. -/ +def formatCodeText (fc : FormatCode) (width : Nat := Std.Format.defWidth) : String := + renderedCodeText (fc.render width) + +/-- +Converts a `FormatCode` to `Highlighted` by rendering at the given width. Local variable +tags are resolved using the `FormatCode.localVars` array for hover information. +-/ +def formatCodeToHighlighted (constInfo : Lean.NameMap (String × Option String) := {}) + (fc : FormatCode) (width : Nat := Std.Format.defWidth) : Highlighted := + renderedCodeToHighlighted constInfo fc.localVars (fc.render width) + +/-- Collects all constant names referenced in a `FormatCode`. -/ +def formatCodeConstNames (acc : Lean.NameSet := {}) (fc : FormatCode) : Lean.NameSet := + renderedCodeConstNames acc fc.render + +/-- Remaps all `Format.tag` indices by adding `offset`, as preparation for combining documents. -/ +private partial def offsetFormatTags (offset : Nat) : Lean.Format → Lean.Format + | .tag n f => .tag (n + offset) (offsetFormatTags offset f) + | .nest n f => .nest n (offsetFormatTags offset f) + | .append a b => .append (offsetFormatTags offset a) (offsetFormatTags offset b) + | .group f beh => .group (offsetFormatTags offset f) beh + | f => f + +/-- +Prepares to append a `FormatCode` to another one whose metadata is given by `tags` and `localVars`. +The resulting data contains both sets of metadata, with data in `tags` and `localVars` unchanged. +This allows the code associated with `tags` and `localVars` to be appended unmodified to the result +of this function. +-/ +private def prepareAppend (fc : FormatCode) + (tags : Array RenderedCode.Tag) (localVars : Array (Lean.Name × Option Lean.Format)) : + Lean.Format × Array RenderedCode.Tag × Array (Lean.Name × Option Lean.Format) := + let tagOff := tags.size + let lvOff := localVars.size + let fmt := offsetFormatTags tagOff fc.fmt + let newTags := fc.tags.map fun + | .localVar idx isBinder => .localVar (idx + lvOff) isBinder + | t => t + let newLVs := fc.localVars.map fun (n, tf?) => + (n, tf?.map (offsetFormatTags tagOff)) + (fmt, tags ++ newTags, localVars ++ newLVs) + +/-- +Builds a combined `FormatCode` for a full declaration signature: `name.{u, v} arg₁ arg₂ … : type`. +-/ +def buildSignatureFormatCode (name : Lean.Name) (levelParams : List Lean.Name) + (args : Array FormatCode) (type : FormatCode) + : FormatCode := Id.run do + -- Start with a const tag for the declaration name + let mut tags : Array RenderedCode.Tag := #[.const name] + let mut localVars : Array (Lean.Name × Option Lean.Format) := #[] + -- Name with universe parameters + let univSuffix := if levelParams.isEmpty then "" + else ".{" ++ ", ".intercalate (levelParams.map Lean.Name.toString) ++ "}" + let nameFmt : Lean.Format := .tag 0 (.text name.toString) ++ .text univSuffix + -- The name, each argument, and the return type are all pieces in a single fill group + -- with nest 2. The fill group packs greedily — fitting as many pieces per line as + -- possible. The " :" is glued to the last argument so the colon stays on the same + -- line, with a .line break before the return type. This gives results like: + -- ``` + -- foo.{u, v} (x : A) (y z : B) + -- (w : A) : + -- SuperLongReturnType + -- ``` + let mut body : Lean.Format := nameFmt + for arg in args do + let (fmt, tags', lvs') := prepareAppend arg tags localVars + tags := tags' + localVars := lvs' + body := body ++ .line ++ fmt + let (typeFmt, tags', lvs') := prepareAppend type tags localVars + tags := tags' + localVars := lvs' + let sigFmt := .group (.nest 2 (body ++ " :" ++ .line ++ typeFmt)) .fill + return { fmt := sigFmt, tags, localVars } diff --git a/src/verso-manual/VersoManual/DB/Docstring.lean b/src/verso-manual/VersoManual/DB/Docstring.lean new file mode 100644 index 000000000..8fdf5104b --- /dev/null +++ b/src/verso-manual/VersoManual/DB/Docstring.lean @@ -0,0 +1,248 @@ +/- +Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +module +public import Lean.CoreM +public import Lean.Data.Options +public import Lean.Environment + +import VersoManual.DB.Query +public meta import VersoManual.DB.Query +public import VersoManual.Docstring +import VersoManual.Markdown + +import Verso.Doc.Elab.Block +import Verso.Doc.Elab.Monad +public import Verso.Doc.ArgParse +import Verso.Doc.PointOfInterest + +import MD4Lean +public section + +/-! +# DocGen-Backed Docstring Command + +A `{docstring}` block command that reads documentation data from a `doc-gen4` SQLite database rather +than from the Lean environment. Produces the same `Block.docstring` output as the existing +environment-based `{docstring}` command, so the HTML/TeX rendering pipeline works unchanged. +-/ + +open Lean +open Verso.Doc.Elab PartElabM +open Verso.Code +open Verso.ArgParse +open SubVerso.Highlighting +open Verso.Genre.Manual hiding docstring tactic conv + +namespace Verso.Genre.Manual.DB + +/-- Cache for the database path, populated on first use by querying Lake. -/ +meta initialize dbPathCache : IO.Ref (Option System.FilePath) ← IO.mkRef none + +/-- +Locates the doc-gen4 database path by asking Lake for the `docSource` facet output. +Uses `--no-build` so that elaboration never triggers a long doc-gen4 build; if the database +is not up-to-date, the user is told to run `lake build` explicitly. +The result is cached so that `lake query` is invoked at most once per process. +-/ +private meta def getDbPath : IO System.FilePath := do + if let some path := (← dbPathCache.get) then + return path + let out ← IO.Process.output { cmd := "lake", args := #["query", "--no-build", "@:docSource"] } + if out.exitCode != 0 then + throw <| .userError s!"Documentation database is not up-to-date. Run `lake build` to generate it.\n\ + Make sure your lakefile includes `needs := #[`@:docSource]` on the library that uses DB docstrings.\n\ + Lake stderr:\n{out.stderr}" + let path : System.FilePath := ⟨out.stdout.trimAscii.copy⟩ + dbPathCache.set (some path) + return path + +private meta def getExtras (name : Name) (declType : Block.Docstring.DeclType) : + DocElabM (Array Term) := + match declType with + | .structure isClass constructor? _ fieldInfo parents _ => do + let ctorRow : Option Term ← constructor?.mapM fun constructor => do + let header := if isClass then "Instance Constructor" else "Constructor" + let sigDesc : Array Term ← + if let some docs := constructor.docstring? then + let some mdAst := MD4Lean.parse docs + | throwError "Failed to parse docstring as Markdown" + mdAst.blocks.mapM (Markdown.blockFromMarkdown · (handleHeaders := Markdown.strongEmphHeaders)) + else pure (#[] : Array Term) + let sig ← `(Verso.Doc.Block.other (Verso.Genre.Manual.Block.internalSignature $(quote constructor.hlName) none) #[$sigDesc,*]) + ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$sig]) + + let parentsRow : Option Term ← do + if parents.isEmpty then pure none + else + let header := "Extends" + let inh ← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.inheritance $(quote name) $(quote parents)) #[]) + some <$> ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$inh]) + + let fieldsRow : Option Term ← do + let header := if isClass then "Methods" else "Fields" + let fieldInfo := fieldInfo.filter (·.subobject?.isNone) + let fieldSigs : Array Term ← fieldInfo.mapM fun i => do + let inheritedFrom : Option Nat := + i.fieldFrom.head?.bind (fun n => parents.findIdx? (·.name == n.name)) + let sigDesc : Array Term ← + if let some docs := i.docString? then + let some mdAst := MD4Lean.parse docs + | throwError "Failed to parse docstring as Markdown" + mdAst.blocks.mapM (Markdown.blockFromMarkdown · (handleHeaders := Markdown.strongEmphHeaders)) + else + pure (#[] : Array Term) + ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.fieldSignature $(quote i.visibility) $(quote i.fieldName) $(quote i.type) $(quote inheritedFrom) $(quote <| parents.map (·.parent))) #[$sigDesc,*]) + if fieldSigs.isEmpty then pure none + else some <$> ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$fieldSigs,*]) + + pure <| ctorRow.toArray ++ parentsRow.toArray ++ fieldsRow.toArray + | .inductive ctors .. => do + let ctorSigs : Array Term ← + ctors.mapM fun c => do + let sigDesc ← + if let some docs := c.docstring? then + let some mdAst := MD4Lean.parse docs + | throwError "Failed to parse docstring as Markdown" + mdAst.blocks.mapM (Markdown.blockFromMarkdown · (handleHeaders := Markdown.strongEmphHeaders)) + else pure (#[] : Array Term) + ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.constructorSignature $(quote c.signature)) #[$sigDesc,*]) + pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection "Constructors") #[$ctorSigs,*])] + | _ => pure #[] + +end DB + +namespace DocGen +open DB + +open Verso.Genre.Manual.Markdown + +@[block_command] +public meta def docstring : BlockCommandOf DocstringConfig + | { name := (x, name), allowMissing, hideFields, hideStructureConstructor, label := customLabel } => do + let opts : Options → Options := + (verso.docstring.allowMissing.set · allowMissing) + withOptions opts do + Doc.PointOfInterest.save (← getRef) name.toString (detail? := some "Documentation") + + let dbPath ← getDbPath + unless ← dbPath.pathExists do + throwErrorAt x m!"Documentation database not found at '{dbPath}'. Run `lake build` to generate it." + + let some docInfo ← lookupDocInfo dbPath name + | throwErrorAt x m!"'{name}' not found in the documentation database." + + let info := docInfo.toInfo + let ci ← constInfoMap dbPath docInfo + + let blockStx ← do + match docStringOfDoc? info.doc with + | none => pure #[] + | some docs => + let some ast := MD4Lean.parse docs + | throwErrorAt x "Failed to parse docstring as Markdown" + ast.blocks.mapM (blockFromMarkdown · (handleHeaders := strongEmphHeaders)) + + let isDeprecated := info.attrs.any (·.startsWith "deprecated") + if !(← Docstring.getAllowDeprecated) && isDeprecated then + Lean.logError m!"'{name}' is deprecated.\n\nSet option 'verso.docstring.allowDeprecated' to 'true' to allow documentation for deprecated names." + + let declType := buildDeclType docInfo (hideFields := hideFields) (hideStructureConstructor := hideStructureConstructor) ci + + let levelParams := match (← getEnv).find? name with + | some ci => ci.levelParams + | none => [] + let signature := signatureOfInfo info ci (levelParams := levelParams) + + -- Find constructors and instance/structure fields + let extras ← getExtras name declType + + let altNames ← Lean.getStoredSuggestions name + + ``(Verso.Doc.Block.other + (Verso.Genre.Manual.Block.docstring $(quote name) $(quote declType) $(quote signature) $(quote customLabel) $(quote altNames.toArray)) + #[$(blockStx ++ extras),*]) + +open Lean Elab Tactic Doc in +@[directive] +public meta def tactic : DirectiveExpanderOf TacticDocsOptions + | { name, «show», replace, allowMissing }, more => do + let opts : Options → Options := + (verso.docstring.allowMissing.set · allowMissing) + withOptions opts do + let dbPath ← getDbPath + let blame : Syntax := name.elim TSyntax.raw TSyntax.raw + unless ← dbPath.pathExists do + throwErrorAt blame m!"Documentation database not found at '{dbPath}'. Run `lake build` to generate it." + + let results : Array TacticLookupResult ← match name with + | .inr ident => lookupTacticByName dbPath ident.getId + | .inl str => lookupTacticByUserName dbPath str.getString + if results.isEmpty then + let n : MessageData := match name with + | .inl x => x + | .inr x => x + throwErrorAt blame m!"Tactic not found in the documentation database: {n}" + + -- Prefer overloads with docstrings + let withDocs := results.filter (·.docString.isSome) + let result := + if h : withDocs.size > 0 then withDocs[0] + else results[0]! + if results.size > 1 then + logWarningAt blame s!"Found {results.size} overloads: {results.map (toString ·.internalName) |>.toList |> ", ".intercalate}" + + let tacticDoc : TacticDoc := { + internalName := result.internalName + userName := result.userName + tags := result.tags.foldl (init := {}) NameSet.insert + docString := result.docString + extensionDocs := #[] + } + + Doc.PointOfInterest.save (← getRef) tacticDoc.userName + if tacticDoc.userName == tacticDoc.internalName.toString && «show».isNone then + throwError "No `show` option provided, but the tactic has no user-facing token name" + + let contents ← + if replace then pure #[] + else + let some str := tacticDoc.docString + | throwError m!"Tactic {tacticDoc.userName} ({tacticDoc.internalName}) has no docstring" + let some mdAst := MD4Lean.parse str + | throwError m!"Failed to parse docstring as Markdown. Docstring contents:\n{repr str}" + mdAst.blocks.mapM (blockFromMarkdown · (handleHeaders := strongEmphHeaders)) + let userContents ← more.mapM elabBlock + ``(Verso.Doc.Block.other (Block.tactic $(quote tacticDoc) $(quote «show»)) #[$(contents ++ userContents),*]) + +@[directive] +public meta def conv : DirectiveExpanderOf TacticDocsOptions + | { name, «show», replace := _, allowMissing }, more => do + let opts : Options → Options := + (verso.docstring.allowMissing.set · allowMissing) + withOptions opts do + let dbPath ← getDbPath + let blame : Syntax := name.elim TSyntax.raw TSyntax.raw + unless ← dbPath.pathExists do + throwErrorAt blame m!"Documentation database not found at '{dbPath}'. Run `lake build` to generate it." + + -- Load all conv tactics and match by suffix + let convTactics ← lookupConvTactics dbPath + let nameToMatch : Name := match name with + | .inr ident => ident.getId + | .inl str => str.getString.toName + let some result := convTactics.find? (fun t => nameToMatch.isSuffixOf t.internalName) + | throwErrorAt blame m!"Conv tactic not found in the documentation database: {nameToMatch}" + + Doc.PointOfInterest.save (← getRef) result.internalName.toString + let contents ← if let some d := result.docString then + let some mdAst := MD4Lean.parse d + | throwError "Failed to parse docstring as Markdown" + mdAst.blocks.mapM (blockFromMarkdown · (handleHeaders := strongEmphHeaders)) + else pure #[] + let some toShow := «show» + | throwError "An explicit 'show' is mandatory for conv docs (for now)" + let userContents ← more.mapM elabBlock + ``(Verso.Doc.Block.other (Block.conv $(quote result.internalName) $(quote toShow) $(quote result.docString)) #[$(contents ++ userContents),*]) diff --git a/src/verso-manual/VersoManual/DB/Query.lean b/src/verso-manual/VersoManual/DB/Query.lean new file mode 100644 index 000000000..fc66a0c7c --- /dev/null +++ b/src/verso-manual/VersoManual/DB/Query.lean @@ -0,0 +1,454 @@ +/- +Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +module +public import Lean.DocString.Extension + +import DocGen4.DB +import DocGen4.DB.VersoDocString +public import DocGen4.Process.Base +import SQLite +public meta import SQLite + +import VersoManual.DB.Convert +import VersoManual.Docstring +public import VersoManual.Docstring.Basic +public import VersoManual.Docstring.DeclInfo +public import VersoManual.Docstring.DocName +public section + +/-! +High-level API for querying the `doc-gen4` database and converting the results into Verso's +documentation types (`DeclType`, `Signature`, `DocName`, `FieldInfo`, `ParentInfo`). +-/ + +namespace Verso.Genre.Manual.DB + +open Lean +open DocGen4 (FormatCode) +open DocGen4.Process (DocInfo NameInfo) +open DocGen4.DB (ReadDB openForReading builtinDocstringValues) +open SubVerso.Highlighting (Highlighted Token) +open Verso.Genre.Manual (Signature) +open Verso.Genre.Manual.Block.Docstring (DeclType DocName FieldInfo ParentInfo Visibility) + +/-- Extracts a Markdown docstring from a doc-gen4 `NameInfo.doc` field. -/ +def docStringOfDoc? (doc : Option (String ⊕ VersoDocString)) : Option String := + doc.bind fun + | .inl md => some md + | .inr v => some (DocGen4.Process.versoDocToMarkdown v) + +/-- +Builds a `DocName` from a doc-gen4 `NameInfo`. +When `showNamespace` is `true` (the default), the full qualified name is displayed. +When `false`, only the last component is shown (used for inductive constructors). +The `sigOverride` parameter allows providing a custom hover signature string (e.g., with named +parameters for structure constructors). +-/ +def docNameOfNameInfo (ni : NameInfo) + (constInfo : Lean.NameMap (String × Option String) := {}) + (showNamespace : Bool := true) + (sigOverride : Option String := none) : DocName where + name := ni.name + hlName := nameHl + signature := .seq #[nameHl, .text " : ", formatCodeToHighlighted constInfo ni.type] + docstring? +where + docstring? := docStringOfDoc? ni.doc + sigStr := sigOverride.getD s!"{ni.name} : {formatCodeText ni.type}" + displayName := if showNamespace then ni.name.toString else ni.name.getString! + nameHl := Highlighted.token ⟨.const ni.name sigStr docstring? false none, displayName⟩ + + +/-- +Builds a `Signature` from a doc-gen4 `Info`, including the declaration name. +Combines all `FormatCode` pieces (name, args, type) into a single `Format` document, +then renders at width 72 (wide) and 42 (narrow). +-/ +def signatureOfInfo (info : DocGen4.Process.Info) + (constInfo : Lean.NameMap (String × Option String) := {}) + (levelParams : List Name := []) : Signature where + wide := formatCodeToHighlighted constInfo sigFc 72 + narrow := formatCodeToHighlighted constInfo sigFc 42 +where + sigFc := buildSignatureFormatCode info.name levelParams (info.args.map (·.binder)) info.type + +/-- +Extracts the parent structure name from a `FormatCode` by rendering and finding the first +`.const` tag. Falls back to `.anonymous` if no constant reference is found. + +The database doesn't independently represent the name, just the full type. +-/ +private partial def parentNameOfFormatCode (fc : FormatCode) : Name := + go fc.render +where + go : DocGen4.RenderedCode → Name + | .text _ => .anonymous + | .tag (.const name) _ => name + | .tag _ inner => go inner + | .append xs => xs.foldl (init := .anonymous) fun acc x => + if acc != .anonymous then acc else go x + +/-- Converts `doc-gen4`'s `StructureParentInfo` array to Verso's `ParentInfo` array. -/ +def convertParents (parents : Array DocGen4.Process.StructureParentInfo) + (constInfo : Lean.NameMap (String × Option String) := {}) : Array ParentInfo := + parents.mapIdx fun i p => { + projFn := p.projFn + name := parentNameOfFormatCode p.type + parent := formatCodeToHighlighted constInfo p.type + index := i + } + +/-- +Converts a `doc-gen4` `Process.FieldInfo` to Verso's `Block.Docstring.FieldInfo`. + +Some fields are simplified because the database doesn't yet carry the full information: +- `subobject?` is always `none` +- `binderInfo` is always `BinderInfo.default` +- `autoParam` is always `false` +- `visibility` is always `.public` + +For inherited fields (`isDirect = false`), the `fieldFrom` list is populated by matching the +field's projection function name prefix against parent structure names. This enables the +"Inherited from" display and checkbox-based parent field filtering in the HTML output. +-/ +def convertFieldInfo (field : DocGen4.Process.FieldInfo) + (parents : Array ParentInfo) + (constInfo : Lean.NameMap (String × Option String) := {}) : FieldInfo := + let fieldNameStr := field.name.getString! + let docString? := docStringOfDoc? field.doc + let sigStr := s!"{field.name} : {formatCodeText field.type}" + let fieldName := + Highlighted.token ⟨.const field.name sigStr docString? true none, fieldNameStr⟩ + let fieldFrom : List DocName := + if field.isDirect then [] + else + -- For inherited fields, determine which parent owns this field by matching + -- the field's projection function name prefix against parent names. + -- E.g., field `Verso.Genre.Manual.HtmlAssets.extraCss` → parent `HtmlAssets` + let fieldPrefix := field.name.getPrefix + match parents.find? (·.name == fieldPrefix) with + | some parent => + let parentDocName : DocName := { + name := parent.name + hlName := .token ⟨.const parent.name "" none false none, parent.name.toString⟩ + signature := parent.parent + docstring? := none + } + [parentDocName] + | none => [] + { + fieldName, + fieldFrom, + type := formatCodeToHighlighted constInfo field.type, + projFn := field.name, + subobject? := none, + binderInfo := .default, + autoParam := false, + docString?, + visibility := .public, + } + +/-- +Builds a pretty constructor hover signature from a structure's fields, reconstructing it from the stored +type because the database does not yet include a rendered signature for structure constructors. +For example, it groups consecutive fields with the same type, e.g. `(shortTitle shortContextTitle : Option String)`. +Returns a string like `Struct.mk (field1 : Type1) (field2 field3 : Type2) : Struct`. +-/ +-- NOTE: This is a workaround because doc-gen4 currently stores the structure constructor as `NameInfo` +-- (without args). Once doc-gen4 is changed to store the constructor as `Info` (with pretty-printed +-- binder args), this function should be replaced by directly using the constructor's `args` field. +private def prettyCtorSig (ctorName : Name) (structName : Name) + (fields : Array DocGen4.Process.FieldInfo) : String := + let resultType := structName.toString + if fields.isEmpty then + s!"{ctorName} : {resultType}" + else Id.run do + -- Group consecutive fields with the same rendered type + let mut groups : Array (Array String × String) := #[] + for field in fields do + let typeStr := formatCodeText field.type + let fieldName := field.name.getString! + match groups.back? with + | some (names, t) => + if t == typeStr then + groups := groups.pop.push (names.push fieldName, t) + else + groups := groups.push (#[fieldName], typeStr) + | none => + groups := groups.push (#[fieldName], typeStr) + let params := groups.map fun (names, typeStr) => + let nameStr := " ".intercalate names.toList + s!"({nameStr} : {typeStr})" + let paramStr := "\n ".intercalate params.toList + s!"{ctorName} {paramStr} : {resultType}" + +private def buildStructureDeclType (isClass : Bool) (info : DocGen4.Process.StructureInfo) + (hideFields : Bool) (hideStructureConstructor : Bool) + (constInfo : Lean.NameMap (String × Option String) := {}) : DeclType := + let ctorSig := prettyCtorSig info.ctor.name info.toInfo.name info.fieldInfo + let ctor? := + if hideStructureConstructor then none + else some (docNameOfNameInfo info.ctor constInfo (sigOverride := some ctorSig)) + let fieldNames := + if hideFields then #[] + else info.fieldInfo.map (·.name) + let parents := convertParents info.parents constInfo + let fieldInfo := + if hideFields then #[] + else info.fieldInfo.map (convertFieldInfo · parents constInfo) + .structure isClass ctor? fieldNames fieldInfo parents #[] + +/-- +Reconstructs a `DeclType` from a doc-gen4 `DocInfo`: + +* For structures and classes, converts constructor, field, and parent information. +* For inductives, converts constructor `DocName` values. +* For definitions, opaque definitions, and axioms: extracts safety information. +-/ +def buildDeclType (docInfo : DocInfo) (hideFields : Bool) (hideStructureConstructor : Bool) + (constInfo : Lean.NameMap (String × Option String) := {}) : DeclType := + match docInfo with + | .axiomInfo info => + .axiom (if info.isUnsafe then .unsafe else .safe) + | .theoremInfo _ => + .theorem + | .opaqueInfo info => + .opaque info.definitionSafety + | .definitionInfo info => + .def (if info.isUnsafe then .unsafe else .safe) + | .instanceInfo info => + .def (if info.isUnsafe then .unsafe else .safe) + | .inductiveInfo info => + let ctors := info.ctors.toArray.map fun ctor => + docNameOfNameInfo ctor.toNameInfo constInfo (showNamespace := false) + .inductive ctors 0 false + | .structureInfo info => + buildStructureDeclType false info hideFields hideStructureConstructor constInfo + | .classInfo info => + buildStructureDeclType true info hideFields hideStructureConstructor constInfo + | .classInductiveInfo info => + let ctors := info.ctors.toArray.map fun ctor => + docNameOfNameInfo ctor.toNameInfo constInfo (showNamespace := false) + .inductive ctors 0 false + | .ctorInfo _info => + .other + +/-- +Builds a `NameMap` of hover data for constants directly referenced in a `DocInfo`, including the +declaration itself, its fields, constructors, etc. These are saved to be shown in hovers. + +The companion function `constInfoMap` then extends this with externally referenced constants (types +mentioned in signatures, etc.) by looking those up in the DB. This function avoids a DB round-trip +for those already in the `DocInfo` being processed. +-/ +private def localConstInfoMap (docInfo : DocInfo) : Lean.NameMap (String × Option String) := + let info := docInfo.toInfo + let sig := s!"{info.name} : {formatCodeText info.type}" + let m : Lean.NameMap (String × Option String) := + ({} : Lean.NameMap _).insert info.name (sig, docStringOfDoc? info.doc) + match docInfo with + | .inductiveInfo ind => + ind.ctors.foldl (init := m) fun m c => + m.insert c.name (s!"{c.name} : {formatCodeText c.type}", docStringOfDoc? c.doc) + | .structureInfo s => + let ctorSig := prettyCtorSig s.ctor.name info.name s.fieldInfo + let m := m.insert s.ctor.name (ctorSig, docStringOfDoc? s.ctor.doc) + s.fieldInfo.foldl (init := m) fun m f => + m.insert f.name (s!"{f.name} : {formatCodeText f.type}", docStringOfDoc? f.doc) + | .classInfo s => + let ctorSig := prettyCtorSig s.ctor.name info.name s.fieldInfo + let m := m.insert s.ctor.name (ctorSig, docStringOfDoc? s.ctor.doc) + s.fieldInfo.foldl (init := m) fun m f => + m.insert f.name (s!"{f.name} : {formatCodeText f.type}", docStringOfDoc? f.doc) + | _ => m + +/-- +Collects all `FormatCode` values from a `DocInfo` (type, args, fields, constructors, parents). +-/ +private def allFormatCodes (docInfo : DocInfo) : Array FormatCode := + let info := docInfo.toInfo + let codes := #[info.type] ++ info.args.map (·.binder) + match docInfo with + | .inductiveInfo ind => + codes ++ ind.ctors.toArray.map (·.type) + | .structureInfo s => + codes ++ #[s.ctor.type] ++ s.fieldInfo.map (·.type) ++ s.parents.map (·.type) + | .classInfo s => + codes ++ #[s.ctor.type] ++ s.fieldInfo.map (·.type) ++ s.parents.map (·.type) + | _ => codes + +/-- Collects all constant names referenced in any `FormatCode` of a `DocInfo`. -/ +private def referencedConstNames (docInfo : DocInfo) : NameSet := + (allFormatCodes docInfo).foldl (init := {}) fun acc fc => + formatCodeConstNames acc fc + +/-- +Queries the database for type and docstring hover data for a set of constant names. +Returns a `NameMap` of `(typeString, docstring?)` suitable for use as `constInfo`. +-/ +private def queryConstHoverData (dbPath : System.FilePath) (names : NameSet) : + IO (Lean.NameMap (String × Option String)) := do + let sqlite ← SQLite.openWith dbPath .readonly + let typeStmt ← sqlite.prepare + "SELECT type, module_name, position FROM name_info WHERE name = ?" + let mdDocStmt ← sqlite.prepare + "SELECT text FROM declaration_markdown_docstrings WHERE module_name = ? AND position = ?" + let versoDocStmt ← sqlite.prepare + "SELECT content FROM declaration_verso_docstrings WHERE module_name = ? AND position = ?" + let mut result : Lean.NameMap (String × Option String) := {} + -- TODO: Once doc-gen4 gets an extension mechanism for these, we'll need to use it here. + have : SQLite.Blob.FromBinary VersoDocString := DocGen4.DB.versoDocStringFromBinary builtinDocstringValues + for name in names do + typeStmt.bind 1 name.toString + if ← typeStmt.step then + let typeBlob ← typeStmt.columnBlob 0 + let moduleName ← typeStmt.columnText 1 + let position ← typeStmt.columnInt64 2 + -- Look up docstring: try markdown first, then verso + let mut doc? : Option String := none + mdDocStmt.bind 1 moduleName + mdDocStmt.bind 2 position + if ← mdDocStmt.step then + doc? := some (← mdDocStmt.columnText 0) + mdDocStmt.reset + mdDocStmt.clearBindings + if doc?.isNone then + versoDocStmt.bind 1 moduleName + versoDocStmt.bind 2 position + if ← versoDocStmt.step then + let blob ← versoDocStmt.columnBlob 0 + match SQLite.Blob.fromBinary (α := VersoDocString) blob with + | Except.ok vds => + doc? := some (DocGen4.Process.versoDocToMarkdown vds) + | Except.error _ => pure () + versoDocStmt.reset + versoDocStmt.clearBindings + match SQLite.Blob.fromBinary (α := FormatCode) typeBlob with + | Except.ok fc => + let sig := s!"{name} : {formatCodeText fc}" + result := result.insert name (sig, doc?) + | Except.error _ => + pure () + typeStmt.reset + typeStmt.clearBindings + return result + +/-- +Builds a complete `NameMap` of hover data for a `DocInfo`, including both locally-defined names +(the declaration, its fields/constructors) and externally-referenced constants (looked up in the DB). + +The values in the map pair signatures with optional Markdown docstrings. +-/ +def constInfoMap (dbPath : System.FilePath) (docInfo : DocInfo) : + IO (Lean.NameMap (String × Option String)) := do + let locallyAvailable := localConstInfoMap docInfo + let referenced := referencedConstNames docInfo + -- Only query the DB for names not already in the local map + let mut missing : Lean.NameSet := {} + for name in referenced do + unless locallyAvailable.contains name do + missing := missing.insert name + if missing.isEmpty then return locallyAvailable + let external ← queryConstHoverData dbPath missing + return external.foldl (init := locallyAvailable) fun m name val => + if m.contains name then m else m.insert name val + +/-- +Opens the `doc-gen4` database at the given path and looks up a declaration by name. + +Returns `none` if the name is not found. Throws on IO errors. +-/ +def lookupDocInfo (dbPath : System.FilePath) (name : Name) : + IO (Option DocInfo) := do + let db ← openForReading dbPath builtinDocstringValues + let moduleNames ← db.getModuleNames + let name2ModIdx ← db.buildName2ModIdx moduleNames + let some modIdx := name2ModIdx[name]? + | return none + let modName := moduleNames[modIdx.toNat]! + let mod ← db.loadModule modName + return mod.members.findSome? fun + | .docInfo di => if di.toInfo.name == name then some di else none + | _ => none + +/-- Result of looking up a tactic in the database. -/ +structure TacticLookupResult where + internalName : Name + userName : String + docString : Option String + tags : Array Name +deriving Inhabited + +/-- Result of looking up a conv tactic in the database. -/ +structure ConvTacticLookupResult where + internalName : Name + docString : Option String +deriving Inhabited + +private def readTacticRow (_sqlite : SQLite) (tacStmt tagStmt : SQLite.Stmt) : + IO TacticLookupResult := do + let internalName := (← tacStmt.columnText 0).toName + let userName ← tacStmt.columnText 1 + let docStr ← tacStmt.columnText 2 + let moduleName ← tacStmt.columnText 3 + -- Load tags + tagStmt.reset + tagStmt.clearBindings + tagStmt.bind 1 moduleName + tagStmt.bind 2 internalName.toString + let mut tags : Array Name := #[] + while (← tagStmt.step) do + tags := tags.push (← tagStmt.columnText 0).toName + return { + internalName + userName + docString := if docStr.isEmpty then none else some docStr + tags + } + +/-- Looks up tactics by internal name. -/ +def lookupTacticByName (dbPath : System.FilePath) (name : Name) : + IO (Array TacticLookupResult) := do + let sqlite ← SQLite.openWith dbPath .readonly + let tacStmt ← sqlite.prepare + "SELECT t.internal_name, t.user_name, t.doc_string, t.module_name FROM tactics t WHERE t.internal_name = ?" + let tagStmt ← sqlite.prepare + "SELECT tag FROM tactic_tags WHERE module_name = ? AND internal_name = ?" + tacStmt.bind 1 name.toString + let mut results := #[] + while (← tacStmt.step) do + results := results.push (← readTacticRow sqlite tacStmt tagStmt) + return results + +/-- Looks up tactics by user-facing name. -/ +def lookupTacticByUserName (dbPath : System.FilePath) (userName : String) : + IO (Array TacticLookupResult) := do + let sqlite ← SQLite.openWith dbPath .readonly + let tacStmt ← sqlite.prepare + "SELECT t.internal_name, t.user_name, t.doc_string, t.module_name FROM tactics t WHERE t.user_name = ?" + let tagStmt ← sqlite.prepare + "SELECT tag FROM tactic_tags WHERE module_name = ? AND internal_name = ?" + tacStmt.bind 1 userName + let mut results := #[] + while (← tacStmt.step) do + results := results.push (← readTacticRow sqlite tacStmt tagStmt) + return results + +/-- Loads all conv tactics from the `conv_tactics` table. -/ +def lookupConvTactics (dbPath : System.FilePath) : + IO (Array ConvTacticLookupResult) := do + let sqlite ← SQLite.openWith dbPath .readonly + let stmt ← sqlite.prepare + "SELECT internal_name, doc_string FROM conv_tactics" + let mut results := #[] + while (← stmt.step) do + let internalName := (← stmt.columnText 0).toName + let docStr ← stmt.columnText 1 + results := results.push { + internalName + docString := if docStr.isEmpty then none else some docStr + } + return results diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean index 80e523bee..0af0c3bf2 100644 --- a/src/verso-manual/VersoManual/Docstring.lean +++ b/src/verso-manual/VersoManual/Docstring.lean @@ -3,33 +3,47 @@ Copyright (c) 2024 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ +module import Lean.PrettyPrinter.Delaborator.Builtins import Lean.Elab.Term import Lean.DocString import Lean.Widget.TaggedText import Lean.Meta.Reduce +public import Lean.Data.Options +public import Lean.Environment +public import Lean.CoreM import Std.Data.HashSet -import VersoManual.Basic +public import VersoManual.Basic import VersoManual.HighlightedCode import VersoManual.Index import VersoManual.Markdown -import VersoManual.Docstring.Basic -import VersoManual.Docstring.Config -import VersoManual.Docstring.DocName -import VersoManual.Docstring.PrettyPrint +public meta import VersoManual.Markdown +public meta import VersoManual.Docstring.Basic +public import VersoManual.Docstring.Basic +public import VersoManual.Docstring.Config +public import VersoManual.Docstring.DeclInfo +public meta import VersoManual.Docstring.DeclInfo +public import VersoManual.Docstring.Show +public meta import VersoManual.Docstring.Show +public import VersoManual.Docstring.DocName +public import VersoManual.Docstring.PrettyPrint +meta import VersoManual.Docstring.PrettyPrint import VersoManual.Docstring.Progress import Verso.Instances import Verso.Code -import Verso.Doc.Elab.Block -import Verso.Doc.Elab.Monad -import Verso.Doc.ArgParse +public import Verso.Code.HighlightedToTex +public meta import Verso.Doc.Elab.Block +public meta import Verso.Doc.Elab.Monad +public import Verso.Doc.ArgParse import Verso.Doc.DocName +public meta import Verso.Doc.PointOfInterest import Verso.Doc.PointOfInterest -import Verso.Doc.Suggestion.Basic +public import Verso.Doc.Suggestion.Basic +public import MD4Lean import SubVerso.Highlighting @@ -57,7 +71,7 @@ open Verso.Doc.Suggestion variable {m} [Monad m] [MonadOptions m] [MonadEnv m] [MonadLiftT CoreM m] [MonadError m] [MonadLog m] [AddMessageContext m] [MonadInfoTree m] [MonadLiftT MetaM m] -def ValDesc.documentableName : ValDesc m (Ident × Name) where +meta def ValDesc.documentableName : ValDesc m (Ident × Name) where description := "a name with documentation" signature := .Ident get @@ -83,205 +97,8 @@ def ValDesc.documentableName : ValDesc m (Ident × Name) where end Verso.ArgParse -private def renderTaggedInMeta (code : Lean.Widget.CodeWithInfos) : MetaM Highlighted := do - let hlCtx : SubVerso.Highlighting.Context := ⟨{}, false, false, [], false, (← IO.mkRef {})⟩ - (renderTagged none code : ReaderT SubVerso.Highlighting.Context MetaM _) hlCtx - -namespace Verso.Genre.Manual.Block.Docstring - -inductive Visibility where - | «public» | «private» | «protected» -deriving Inhabited, Repr, ToJson, FromJson, DecidableEq, Ord, Quote - -def Visibility.of (env : Environment) (n : Name) : Visibility := - if isPrivateName n then .private else if isProtected env n then .protected else .public - -structure FieldInfo where - fieldName : Highlighted - /-- - What is the path by which the field was inherited? - [] if not inherited. - -/ - fieldFrom : List DocName - type : Highlighted - projFn : Name - /-- It is `some parentStructName` if it is a subobject, and `parentStructName` is the name of the parent structure -/ - subobject? : Option Name - binderInfo : BinderInfo - autoParam : Bool - docString? : Option String - visibility : Visibility -deriving Inhabited, Repr, ToJson, FromJson, Quote - - -structure ParentInfo where - projFn : Name - name : Name - parent : Highlighted - index : Nat -deriving ToJson, FromJson, Quote - -inductive DeclType where - /-- - A structure or class. The `constructor` field is `none` when the constructor is private. - -/ - | structure (isClass : Bool) (constructor : Option DocName) (fieldNames : Array Name) (fieldInfo : Array FieldInfo) (parents : Array ParentInfo) (ancestors : Array Name) - | def (safety : DefinitionSafety) - | opaque (safety : DefinitionSafety) - | inductive (constructors : Array DocName) (numArgs : Nat) (propOnly : Bool) - | axiom (safety : DefinitionSafety) - | theorem - | ctor (ofInductive : Name) (safety : DefinitionSafety) - | recursor (safety : DefinitionSafety) - | quotPrim (kind : QuotKind) - | other -deriving ToJson, FromJson, Quote - -def DeclType.label : DeclType → String - | .structure false .. => "structure" - | .structure true .. => "type class" - | .def .safe => "def" - | .def .unsafe => "unsafe def" - | .def .partial => "partial def" - | .opaque .unsafe => "unsafe opaque" - | .opaque _ => "opaque" - | .inductive _ _ false => "inductive type" - | .inductive _ 0 true => "inductive proposition" - | .inductive _ _ true => "inductive predicate" - | .axiom .unsafe => "axiom" - | .axiom _ => "axiom" - | .theorem => "theorem" - | .ctor n _ => s!"constructor of {n}" - | .quotPrim _ => "primitive" - | .recursor .unsafe => "unsafe recursor" - | .recursor _ => "recursor" - | .other => "" - - -partial def getStructurePathToBaseStructureAux (env : Environment) (baseStructName : Name) (structName : Name) (path : List Name) : Option (List Name) := - if baseStructName == structName then - some path.reverse - else - if let some info := getStructureInfo? env structName then - -- Prefer subobject projections - (info.fieldInfo.findSome? fun field => - match field.subobject? with - | none => none - | some parentStructName => getStructurePathToBaseStructureAux env baseStructName parentStructName (parentStructName :: path)) - -- Otherwise, consider other parents - <|> info.parentInfo.findSome? fun parent => - if parent.subobject then - none - else - getStructurePathToBaseStructureAux env baseStructName parent.structName (parent.structName :: path) - else none - -/-- -If `baseStructName` is an ancestor structure for `structName`, then return a sequence of projection functions -to go from `structName` to `baseStructName`. Returns `[]` if `baseStructName == structName`. --/ -def getStructurePathToBaseStructure? (env : Environment) (baseStructName : Name) (structName : Name) : Option (List Name) := - getStructurePathToBaseStructureAux env baseStructName structName [] - - -open Meta in -def DeclType.ofName (c : Name) - (hideFields : Bool := false) - (hideStructureConstructor : Bool := false) : - MetaM DeclType := do - let env ← getEnv - - let openDecls : List OpenDecl := - match c with - | .str _ s => [.explicit c.getPrefix s.toName] - | _ => [] - if let some info := env.find? c then - match info with - | .defnInfo di => return .def di.safety - | .inductInfo ii => - if let some info := getStructureInfo? env c then - let ctor := getStructureCtor env c - let parentProjFns := getStructureParentInfo env c |>.map (·.projFn) - let parents ← - forallTelescopeReducing ii.type fun params _ => - withLocalDeclD `self (mkAppN (mkConst c (ii.levelParams.map mkLevelParam)) params) fun s => do - let selfType ← inferType s >>= whnf - let .const _structName us := selfType.getAppFn - | pure #[] - let params := selfType.getAppArgs - - parentProjFns.mapIdxM fun i parentProj => do - let proj := mkApp (mkAppN (.const parentProj us) params) s - let type ← inferType proj >>= instantiateMVars - let projType ← withOptions (·.set `format.width (40 : Int) |>.setBool `pp.tagAppFns true) <| Widget.ppExprTagged type - if let .const parentName _ := type.getAppFn then - pure ⟨parentProj, parentName, ← renderTaggedInMeta projType, i⟩ - else - pure ⟨parentProj, .anonymous, ← renderTaggedInMeta projType, i⟩ - let ancestors ← getAllParentStructures c - let allFields := if hideFields then #[] else getStructureFieldsFlattened env c (includeSubobjectFields := true) - let fieldInfo ← - forallTelescopeReducing ii.type fun params _ => - withLocalDeclD `self (mkAppN (mkConst c (ii.levelParams.map mkLevelParam)) params) fun s => - allFields.filterMapM fun fieldName => do - let proj ← mkProjection s fieldName - let type ← inferType proj >>= instantiateMVars - let type' ← withOptions (·.set `format.width (40 : Int) |>.setBool `pp.tagAppFns true) <| (Widget.ppExprTagged type) - let projType ← withOptions (·.set `format.width (40 : Int) |>.setBool `pp.tagAppFns true) <| ppExpr type - let fieldFrom? := findField? env c fieldName - let fieldPath? := fieldFrom? >>= (getStructurePathToBaseStructure? env · c) - let fieldFrom ← fieldPath?.getD [] |>.mapM (DocName.ofName (showUniverses := false)) - let subobject? := isSubobjectField? env (fieldFrom?.getD c) fieldName - let fieldInfo? := getFieldInfo? env (fieldFrom?.getD c) fieldName - - let binderInfo := fieldInfo?.map (·.binderInfo) |>.getD BinderInfo.default - let autoParam := fieldInfo?.map (·.autoParam?.isSome) |>.getD false - - if let some projFn := getProjFnForField? env c fieldName then - if isPrivateName projFn then - pure none - else - let docString? ← - -- Don't complain about missing docstrings for subobject projections - if subobject?.isSome then findDocString? env projFn - else getDocString? env projFn - let visibility := Visibility.of env projFn - let fieldName' := Highlighted.token ⟨.const projFn projType.pretty docString? true none, fieldName.toString⟩ - - pure <| some { fieldName := fieldName', fieldFrom, type := ← renderTaggedInMeta type', subobject?, projFn, binderInfo, autoParam, docString?, visibility} - else - let fieldName' := Highlighted.token ⟨.unknown, fieldName.toString⟩ - pure <| some { fieldName := fieldName', fieldFrom, type := ← renderTaggedInMeta type' , subobject?, projFn := .anonymous, binderInfo, autoParam, docString? := none, visibility := .public} - - let ctor? ← - if hideStructureConstructor || isPrivateName ctor.name then pure none - else some <$> DocName.ofName (showNamespace := true) (checkDocstring := false) ctor.name - - return .structure (isClass env c) ctor? info.fieldNames fieldInfo parents ancestors - - else - let ctors ← ii.ctors.mapM (DocName.ofName (ppWidth := 60) (showNamespace := false) (openDecls := openDecls)) - let t ← inferType <| .const c (ii.levelParams.map .param) - let t' ← reduceAll t - return .inductive ctors.toArray (ii.numIndices + ii.numParams) (isPred t') - | .opaqueInfo oi => return .opaque (if oi.isUnsafe then .unsafe else .safe) - | .axiomInfo ai => return .axiom (if ai.isUnsafe then .unsafe else .safe) - | .thmInfo _ => return .theorem - | .recInfo ri => return .recursor (if ri.isUnsafe then .unsafe else .safe) - | .ctorInfo ci => return .ctor ci.induct (if ci.isUnsafe then .unsafe else .safe) - | .quotInfo qi => return .quotPrim qi.kind - else - return .other -where - isPred : Expr → Bool - | .sort u => u.isZero - | .forallE _ _ e _ => isPred e - | .mdata _ e => isPred e - | .letE _ _ _ e _ => isPred e - | _ => false - -end Docstring +namespace Verso.Genre.Manual.Block def docstring (name : Name) (declType : Docstring.DeclType) (signature : Signature) (customLabel : Option String) (altNamesToSuggest : Array Name) : Block where name := `Verso.Genre.Manual.Block.docstring @@ -311,31 +128,6 @@ def constructorSignature (signature : Highlighted) : Block where end Block -def Signature.forName [Monad m] [MonadWithOptions m] [MonadEnv m] [MonadMCtx m] [MonadOptions m] [MonadResolveName m] [MonadNameGenerator m] [MonadLiftT MetaM m] [MonadLiftT BaseIO m] [MonadLiftT IO m] [MonadFileMap m] [Alternative m] (name : Name) : m Signature := do - let (⟨fmt, infos⟩ : FormatWithInfos) ← withOptions (·.setBool `pp.tagAppFns true) <| Block.Docstring.ppSignature name (constantInfo := false) - - let ctx := { - env := (← getEnv) - mctx := (← getMCtx) - options := (← getOptions) - currNamespace := (← getCurrNamespace) - openDecls := (← getOpenDecls) - fileMap := default - ngen := (← getNGen) - } - - let ttNarrow := Lean.Widget.TaggedText.prettyTagged (w := 42) fmt - let sigNarrow ← Lean.Widget.tagCodeInfos ctx infos ttNarrow - - let ttWide := Lean.Widget.TaggedText.prettyTagged (w := 72) fmt - let sigWide ← Lean.Widget.tagCodeInfos ctx infos ttWide - - return { - wide := ← renderTaggedInMeta sigWide - narrow := ← renderTaggedInMeta sigNarrow - } - - instance [BEq α] [Hashable α] [FromJson α] : FromJson (HashSet α) where fromJson? v := do let xs ← v.getArr? @@ -569,7 +361,6 @@ def internalSignature.descr : BlockDescr where }} - @[block_extension Block.inheritance] def inheritance.descr : BlockDescr where traverse _ _ _ := pure none @@ -680,8 +471,9 @@ def constructorSignature.descr : BlockDescr where
}} + open Verso.Output Html in -def Signature.toHtml : Signature → HighlightHtmlM Manual Html +def Signature.toHtml : Signature → HighlightHtmlM Manual Html | {wide, narrow} => do return {{
{{← wide.toHtml}}
{{← narrow.toHtml}}
}} @@ -845,510 +637,6 @@ where open Verso.Doc.Elab -def leanFromMarkdown := () - -def Inline.leanFromMarkdown (hls : Highlighted) : Inline where - name := ``Verso.Genre.Manual.leanFromMarkdown - data := ToJson.toJson hls - -def Block.leanFromMarkdown (hls : Highlighted) : Block where - name := ``Verso.Genre.Manual.leanFromMarkdown - data := ToJson.toJson hls - - -@[inline_extension leanFromMarkdown] -def leanFromMarkdown.inlinedescr : InlineDescr := withHighlighting { - traverse _id _data _ := pure none - toTeX := some <| fun go _ _ content => content.mapM go - toHtml := - open Verso.Output Html in - open Verso.Doc.Html in - some <| fun _ _ data _ => do - match FromJson.fromJson? (α := Highlighted) data with - | .error err => - HtmlT.logError <| "Couldn't deserialize Lean code while rendering inline HTML: " ++ err - pure .empty - | .ok (hl : Highlighted) => - hl.inlineHtml (g := Manual) "docstring-examples" -} - -@[block_extension leanFromMarkdown] -def leanFromMarkdown.blockdescr : BlockDescr := withHighlighting { - traverse _id _data _ := pure none - toTeX := - some <| fun _goI goB _ _ content => do - pure <| .seq <| ← content.mapM fun b => do - pure <| .seq #[← goB b, .raw "\n"] - toHtml := - open Verso.Output Html in - open Verso.Doc.Html in - some <| fun _ _ _ data _ => do - match FromJson.fromJson? (α := Highlighted) data with - | .error err => - HtmlT.logError <| "Couldn't deserialize Lean code while rendering inline HTML: " ++ err - pure .empty - | .ok (hl : Highlighted) => - hl.blockHtml (g := Manual) "docstring-examples" -} - -open Lean Elab Term in -def tryElabCodeTermWith (mk : Highlighted → String → DocElabM α) (str : String) (ignoreElabErrors := false) (identOnly := false) : DocElabM α := do - let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos - let src := - if let some ⟨line, col⟩ := loc then s!"" - else s!"" - match Parser.runParserCategory (← getEnv) `term str src with - | .error e => throw (.error (← getRef) e) - | .ok stx => DocElabM.withFileMap (.ofString str) <| do - if stx.isIdent && (← readThe Term.Context).autoBoundImplicitContext.isSome then - throwError m!"Didn't elaborate {stx} as term to avoid spurious auto-implicits" - if identOnly && !stx.isIdent then - throwError m!"Didn't elaborate {stx} as term because only identifiers are wanted here" - let (newMsgs, tree, _e) ← do - let initMsgs ← Core.getMessageLog - try - Core.resetMessageLog - -- TODO open decls/current namespace - let (tree', e') ← do - let e ← Elab.Term.elabTerm (catchExPostpone := true) stx none - Term.synthesizeSyntheticMVarsNoPostponing - let e' ← Term.levelMVarToParam (← instantiateMVars e) - Term.synthesizeSyntheticMVarsNoPostponing - let e' ← instantiateMVars e' - let ctx := PartialContextInfo.commandCtx { - env := ← getEnv, fileMap := ← getFileMap, mctx := ← getMCtx, currNamespace := ← getCurrNamespace, - openDecls := ← getOpenDecls, options := ← getOptions, ngen := ← getNGen - } - pure (InfoTree.context ctx (.node (Info.ofCommandInfo ⟨`Verso.Genre.Manual.docstring, (← getRef)⟩) (← getInfoState).trees), e') - pure (← Core.getMessageLog, tree', e') - finally - Core.setMessageLog initMsgs - if newMsgs.hasErrors && !ignoreElabErrors then - for msg in newMsgs.errorsToWarnings.toArray do - logMessage msg - throwError m!"Didn't elaborate {stx} as term" - - let hls ← highlight stx #[] (PersistentArray.empty.push tree) - mk hls str - - -declare_syntax_cat doc_metavar -scoped syntax (name := docMetavar) term ":" term : doc_metavar - - -open Lean Elab Term in -def tryElabCodeMetavarTermWith (mk : Highlighted → String → DocElabM α) (str : String) (ignoreElabErrors := false) : DocElabM α := do - let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos - let src := - if let some ⟨line, col⟩ := loc then s!"" - else s!"" - match Parser.runParserCategory (← getEnv) `doc_metavar str src with - | .error e => throw (.error (← getRef) e) - | .ok stx => DocElabM.withFileMap (.ofString str) <| do - if let `(doc_metavar|$pat:term : $ty:term) := stx then - let (newMsgs, tree, _e') ← show TermElabM _ from do - let initMsgs ← Core.getMessageLog - try - Core.resetMessageLog - -- TODO open decls/current namespace - let (tree', e') ← do - let stx' : Term ← `(($pat : $ty)) - let e ← withReader ({· with autoBoundImplicitContext := some ⟨true, {}⟩}) <| elabTerm stx' none - Term.synthesizeSyntheticMVarsNoPostponing - let e' ← Term.levelMVarToParam (← instantiateMVars e) - Term.synthesizeSyntheticMVarsNoPostponing - let e' ← instantiateMVars e' - let ctx := PartialContextInfo.commandCtx { - env := ← getEnv, fileMap := ← getFileMap, mctx := ← getMCtx, currNamespace := ← getCurrNamespace, - openDecls := ← getOpenDecls, options := ← getOptions, ngen := ← getNGen - } - pure (InfoTree.context ctx (.node (Info.ofCommandInfo ⟨`Verso.Genre.Manual.docstring, stx⟩) (← getInfoState).trees), e') - pure (← Core.getMessageLog, tree', e') - finally - Core.setMessageLog initMsgs - if newMsgs.hasErrors && !ignoreElabErrors then - for msg in newMsgs.errorsToWarnings.toArray do - logMessage msg - throwError m!"Didn't elaborate {pat} : {ty} as term" - - let hls ← highlight stx #[] (PersistentArray.empty.push tree) - mk hls str - else - throwError "Not a doc metavar: {stx}" - -open Lean Elab Term in -def tryElabInlineCodeTerm (str : String) (ignoreElabErrors := false) (identOnly := false) : DocElabM Term := - tryElabCodeTermWith (ignoreElabErrors := ignoreElabErrors) (identOnly := identOnly) (fun hls str => - ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)])) - str - -open Lean Elab Term in -def tryElabInlineCodeMetavarTerm (str : String) (ignoreElabErrors := false) : DocElabM Term := - tryElabCodeMetavarTermWith (ignoreElabErrors := ignoreElabErrors) (fun hls str => - ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)])) - str - -open Lean Elab Term in -def tryElabBlockCodeTerm (str : String) (ignoreElabErrors := false) : DocElabM Term := - tryElabCodeTermWith (ignoreElabErrors := ignoreElabErrors) (fun hls str => - ``(Verso.Doc.Block.other (Block.leanFromMarkdown $(quote hls)) #[Verso.Doc.Block.code $(quote str)])) - str - -open Lean Elab Term in -def tryParseInlineCodeTactic (str : String) : DocElabM Term := do - let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos - let src := - if let some ⟨line, col⟩ := loc then s!"" - else s!"" - match Parser.runParserCategory (← getEnv) `tactic str src with - | .error e => throw (.error (← getRef) e) - | .ok stx => DocElabM.withFileMap (.ofString str) <| do - -- TODO try actually running the tactic - if the parameters are simple enough, then it may work - -- and give better highlights - let hls ← highlight stx #[] (PersistentArray.empty) - ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)]) - -open Lean Elab Term in -def tryInlineOption (str : String) : DocElabM Term := do - let optName := str.trimAscii.toName - let optDecl ← getOptionDecl optName - let hl : Highlighted := optTok optName optDecl.declName optDecl.descr - ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hl)) #[Verso.Doc.Inline.code $(quote str)]) -where - optTok (name declName : Name) (descr : String) : Highlighted := - .token ⟨.option name declName descr, name.toString⟩ - -open Lean Elab in -def tryTacticName (tactics : Array Tactic.Doc.TacticDoc) (str : String) : DocElabM Term := do - for t in tactics do - if t.userName == str then - let hl : Highlighted := tacToken t - return ← ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hl)) #[Verso.Doc.Inline.code $(quote str)]) - throwError "Not a tactic name: {str}" -where - tacToken (t : Lean.Elab.Tactic.Doc.TacticDoc) : Highlighted := - .token ⟨.keyword t.internalName none t.docString, str⟩ - -open Lean Elab Term in -open Lean.Parser in -def tryHighlightKeywords (extraKeywords : Array String) (str : String) : DocElabM Term := do - let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos - let src := - if let some ⟨line, col⟩ := loc then s!"" - else s!"" - let p : Parser := {fn := simpleFn} - match runParser extraKeywords (← getEnv) (← getOptions) p str src (prec := 0) with - | .error _e => throwError "Not keyword-highlightable" - | .ok stx => DocElabM.withFileMap (.ofString str) <| do - let hls ← highlight stx #[] (PersistentArray.empty) - ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)]) -where - - simpleFn := andthenFn whitespace <| nodeFn nullKind <| manyFn tokenFn - - runParser (extraKeywords : Array String) (env : Environment) (opts : Lean.Options) (p : Parser) (input : String) (fileName : String := "") (prec : Nat := 0) : Except (List (Position × String)) Syntax := - let ictx := mkInputContext input fileName - let p' := adaptCacheableContext ({· with prec}) p - let tokens := extraKeywords.foldl (init := getTokenTable env) (fun x tk => x.insert tk tk) - let s := p'.fn.run ictx { env, options := opts } tokens (mkParserState input) - if !s.allErrors.isEmpty then - Except.error (toErrorMsg ictx s) - else if ictx.atEnd s.pos then - Except.ok s.stxStack.back - else - Except.error (toErrorMsg ictx (s.mkError "end of input")) - - toErrorMsg (ctx : InputContext) (s : ParserState) : List (Position × String) := Id.run do - let mut errs := [] - for (pos, _stk, err) in s.allErrors do - let pos := ctx.fileMap.toPosition pos - errs := (pos, toString err) :: errs - errs.reverse - - -declare_syntax_cat braces_attr -syntax (name := plain) attr : braces_attr -syntax (name := bracketed) "[" attr "]" : braces_attr -syntax (name := atBracketed) "@[" attr "]" : braces_attr - -private def getAttr : Syntax → Syntax - | `(plain| $a) - | `(bracketed| [ $a ] ) - | `(atBracketed| @[ $a ]) => a - | _ => .missing - -open Lean Elab Term in -def tryParseInlineCodeAttribute (validate := true) (str : String) : DocElabM Term := do - let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos - let src := - if let some ⟨line, col⟩ := loc then s!"" - else s!"" - match Parser.runParserCategory (← getEnv) `braces_attr str src with - | .error e => throw (.error (← getRef) e) - | .ok stx => DocElabM.withFileMap (.ofString str) <| do - let inner := getAttr stx - if validate then - let attrName ← - match inner.getKind with - | `Lean.Parser.Attr.simple => pure inner[0].getId - | .str (.str (.str (.str .anonymous "Lean") "Parser") "Attr") k => pure k.toName - | other => - let allAttrs := attributeExtension.getState (← getEnv) |>.map |>.toArray |>.map (·.fst) |>.qsort (·.toString < ·.toString) - throwError "Failed to process attribute kind: {stx.getKind} {isAttribute (← getEnv) stx.getKind} {allAttrs |> repr}" - match getAttributeImpl (← getEnv) attrName with - | .error e => throwError e - | .ok _ => - let hls ← highlight stx #[] (PersistentArray.empty) - ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)]) - else - let hls ← highlight stx #[] (PersistentArray.empty) - ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)]) - - -private def indentColumn (str : String) : Nat := Id.run do - let mut i : Option Nat := none - for line in str.splitToList (· == '\n') do - let leading := line.takeWhile Char.isWhitespace - if leading == line.toSlice then continue - let leading := leading.copy - if let some i' := i then - if leading.length < i' then i := some leading.length - else i := some leading.length - return i.getD 0 - -/-- info: 0 -/ -#guard_msgs in -#eval indentColumn "" -/-- info: 0 -/ -#guard_msgs in -#eval indentColumn "abc" -/-- info: 3 -/ -#guard_msgs in -#eval indentColumn " abc" -/-- info: 3 -/ -#guard_msgs in -#eval indentColumn " abc\n\n def" -/-- info: 2 -/ -#guard_msgs in -#eval indentColumn " abc\n\n def" -/-- info: 2 -/ -#guard_msgs in -#eval indentColumn " abc\n\n def\n a" - -open Lean Elab Term in -def tryElabBlockCodeCommand (str : String) (ignoreElabErrors := false) : DocElabM Term := do - let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos - let src := - if let some ⟨line, col⟩ := loc then s!"" - else s!"" - - let ictx := Parser.mkInputContext str src - let cctx : Command.Context := { fileName := ← getFileName, fileMap := FileMap.ofString str, snap? := none, cancelTk? := none} - - let mut cmdState : Command.State := {env := ← getEnv, maxRecDepth := ← MonadRecDepth.getMaxRecDepth, scopes := [{header := ""}]} - let mut pstate := {pos := 0, recovering := false} - let mut cmds := #[] - - repeat - let scope := cmdState.scopes.head! - let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls } - let (cmd, ps', messages) := Parser.parseCommand ictx pmctx pstate cmdState.messages - cmds := cmds.push cmd - pstate := ps' - cmdState := {cmdState with messages := messages} - - cmdState ← withInfoTreeContext (mkInfoTree := pure ∘ InfoTree.node (.ofCommandInfo {elaborator := `Manual.Meta.lean, stx := cmd})) do - match (← liftM <| EIO.toIO' <| (Command.elabCommand cmd cctx).run cmdState) with - | Except.error e => - unless ignoreElabErrors do Lean.logError e.toMessageData - return cmdState - | Except.ok ((), s) => return s - - if Parser.isTerminalCommand cmd then break - - if cmdState.messages.hasErrors then - throwError "Errors found in command" - - let hls ← DocElabM.withFileMap (.ofString str) do - let mut hls := Highlighted.empty - for cmd in cmds do - hls := hls ++ (← highlight cmd cmdState.messages.toArray cmdState.infoState.trees) - pure <| hls.deIndent (indentColumn str) - - ``(Verso.Doc.Block.other (Block.leanFromMarkdown $(quote hls)) #[Verso.Doc.Block.code $(quote str)]) - - -open Lean Elab Term in -def tryElabInlineCodeName (str : String) : DocElabM Term := do - let str := str.trimAscii - let x := str.toName - if x.toString.toSlice == str then - let stx := mkIdent x - let n ← realizeGlobalConstNoOverload stx - let str := str.copy - let hl : Highlighted ← constTok n str - ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hl)) #[Verso.Doc.Inline.code $(quote str)]) - else - throwError "Not a name: '{str}'" -where - constTok {m} [Monad m] [MonadEnv m] [MonadLiftT MetaM m] [MonadLiftT IO m] - (name : Name) (str : String) : - m Highlighted := do - let docs ← findDocString? (← getEnv) name - let sig := toString (← (PrettyPrinter.ppSignature name)).1 - pure <| .token ⟨.const name sig docs false none, str⟩ - -open Lean Elab Term in -private def attempt (str : String) (xs : List (String → DocElabM α)) : DocElabM α := do - match xs with - | [] => throwError "No attempt succeeded" - | [x] => x str - | x::y::xs => - let info ← getInfoState - try - setInfoState {} - x str - catch e => - if isAutoBoundImplicitLocalException? e |>.isSome then - throw e - else attempt str (y::xs) - finally - setInfoState info - - -open Lean Elab Term in -def tryElabInlineCodeUsing (elabs : List (String → DocElabM Term)) - (priorWord : Option String) (str : String) : DocElabM Term := do - -- Don't try to show Lake commands as terms - if "lake ".isPrefixOf str then return (← ``(Verso.Doc.Inline.code $(quote str))) - try - attempt str <| wordElab priorWord ++ elabs - catch - | .error ref e => - logWarningAt ref e - ``(Verso.Doc.Inline.code $(quote str)) - | e => - if isAutoBoundImplicitLocalException? e |>.isSome then - throw e - else - logWarning m!"Internal exception uncaught: {e.toMessageData}" - ``(Verso.Doc.Inline.code $(quote str)) -where - wordElab - | some "attribute" => [tryParseInlineCodeAttribute (validate := false)] - | some "tactic" => [tryParseInlineCodeTactic] - | _ => [] - -open Elab in -def tryElabInlineCode (allTactics : Array Tactic.Doc.TacticDoc) (extraKeywords : Array String) - (priorWord : Option String) (str : String) : DocElabM Term := - tryElabInlineCodeUsing [ - tryElabInlineCodeName, - -- When identifiers have the same name as tactics, prefer the identifiers - tryElabInlineCodeTerm (identOnly := true), - tryParseInlineCodeTactic, - tryParseInlineCodeAttribute (validate := true), - tryInlineOption, - tryElabInlineCodeTerm, - tryElabInlineCodeMetavarTerm, - tryTacticName allTactics, - withTheReader Term.Context (fun ctx => {ctx with autoBoundImplicitContext := some ⟨true, {}⟩}) ∘ tryElabInlineCodeTerm, - tryElabInlineCodeTerm (ignoreElabErrors := true), - tryHighlightKeywords extraKeywords - ] priorWord str - -open Elab in -/-- -Like `tryElabInlineCode`, but prefers producing un-highlighted code blocks to -displaying metavariable-typed terms (e.g., through auto-bound implicits or -elaboration failures). --/ -def tryElabInlineCodeStrict (allTactics : Array Tactic.Doc.TacticDoc) (extraKeywords : Array String) - (priorWord : Option String) (str : String) : DocElabM Term := - tryElabInlineCodeUsing [ - tryElabInlineCodeName, - -- When identifiers have the same name as tactics, prefer the identifiers - tryElabInlineCodeTerm (identOnly := true), - tryParseInlineCodeTactic, - tryParseInlineCodeAttribute (validate := true), - tryInlineOption, - tryElabInlineCodeTerm, - tryElabInlineCodeMetavarTerm, - tryTacticName allTactics, - tryHighlightKeywords extraKeywords - ] priorWord str - -open Lean Elab Term in -def tryElabBlockCode (_info? _lang? : Option String) (str : String) : DocElabM Term := do - try - attempt str [ - tryElabBlockCodeCommand, - tryElabBlockCodeTerm, - tryElabBlockCodeCommand (ignoreElabErrors := true), - withTheReader Term.Context (fun ctx => {ctx with autoBoundImplicitContext := some ⟨true, {}⟩}) ∘ - tryElabBlockCodeTerm (ignoreElabErrors := true) - ] - catch - | .error ref e => - logWarningAt ref e - ``(Verso.Doc.Block.code $(quote str)) - | e => - if isAutoBoundImplicitLocalException? e |>.isSome then - throw e - else - logWarning m!"Internal exception uncaught: {e.toMessageData}" - ``(Verso.Doc.Block.code $(quote str)) - -open Lean Elab Term in -/-- -Heuristically elaborate Lean fragments in Markdown code. The provided names are used as signatures, -from left to right, with the names bound by the signature being available in the local scope in -which the Lean fragments are elaborated. --/ -def blockFromMarkdownWithLean (names : List Name) (b : MD4Lean.Block) : DocElabM Term := do - unless (← Docstring.getElabMarkdown) do - return (← Markdown.blockFromMarkdown b (handleHeaders := Markdown.strongEmphHeaders)) - let tactics ← Elab.Tactic.Doc.allTacticDocs - let keywords := tactics.map (·.userName) - try - match names with - | decl :: decls => - -- This brings the parameters into scope, so the term elaboration version catches them! - Meta.forallTelescopeReducing (← getConstInfo decl).type fun _ _ => - blockFromMarkdownWithLean decls b - | [] => - -- It'd be silly for some weird edge case to block on this feature... - let rec loop (max : Nat) (s : SavedState) : DocElabM Term := do - match max with - | k + 1 => - try - let res ← - Markdown.blockFromMarkdown b - (handleHeaders := Markdown.strongEmphHeaders) - (elabInlineCode := tryElabInlineCode tactics keywords) - (elabBlockCode := tryElabBlockCode) - synthesizeSyntheticMVarsUsingDefault - - discard <| addAutoBoundImplicits #[] (inlayHintPos? := none) - - return res - catch e => - if let some n := isAutoBoundImplicitLocalException? e then - s.restore (restoreInfo := true) - Meta.withLocalDecl n .implicit (← Meta.mkFreshTypeMVar) fun x => - withTheReader Term.Context (fun ctx => { ctx with autoBoundImplicitContext := ctx.autoBoundImplicitContext.map (fun c => {c with boundVariables := c.boundVariables.push x }) }) do - loop k (← (saveState : TermElabM _)) - else throw e - | 0 => throwError "Ran out of local name attempts" - let s ← (saveState : TermElabM _) - try - loop 40 s - finally - (s.restore : TermElabM _) - catch _ => - Markdown.blockFromMarkdown b - (handleHeaders := Markdown.strongEmphHeaders) - structure DocstringConfig where name : Ident × Name /-- @@ -1366,8 +654,9 @@ section variable [Monad m] [MonadOptions m] [MonadEnv m] [MonadLiftT CoreM m] [MonadLiftT MetaM m] [MonadError m] variable [MonadLog m] [AddMessageContext m] [Elab.MonadInfoTree m] -def DocstringConfig.parse : ArgParse m DocstringConfig := - DocstringConfig.mk <$> +meta instance : FromArgs DocstringConfig m where + fromArgs := + DocstringConfig.mk <$> .positional `name .documentableName <*> .flagM `allowMissing (verso.docstring.allowMissing.get <$> getOptions) "Warn instead of error on missing docstrings (defaults to value of option `verso.docstring.allowMissing)" <*> @@ -1375,12 +664,13 @@ def DocstringConfig.parse : ArgParse m DocstringConfig := .flag `hideStructureConstructor false <*> .named `label .string true -instance : FromArgs DocstringConfig m := ⟨DocstringConfig.parse⟩ - end +open Verso.Doc.Elab + +open Block.Docstring in @[block_command] -def docstring : BlockCommandOf DocstringConfig +meta def docstring : BlockCommandOf DocstringConfig | ⟨(x, name), allowMissing, hideFields, hideCtor, customLabel⟩ => do let opts : Options → Options := (verso.docstring.allowMissing.set · allowMissing) @@ -1471,16 +761,14 @@ structure IncludeDocstringOpts where name : Name elaborate : Bool -def IncludeDocstringOpts.parse : ArgParse m IncludeDocstringOpts := - IncludeDocstringOpts.mk <$> (.positional `name .documentableName <&> (·.2)) <*> .flag `elab true - -instance : FromArgs IncludeDocstringOpts m where - fromArgs := IncludeDocstringOpts.parse - +meta instance : FromArgs IncludeDocstringOpts m where + fromArgs := + IncludeDocstringOpts.mk <$> (.positional `name .documentableName <&> (·.2)) <*> .flag `elab true end +open Block.Docstring in @[block_command] -def includeDocstring : BlockCommandOf IncludeDocstringOpts +meta def includeDocstring : BlockCommandOf IncludeDocstringOpts | {name, elaborate} => do let fromMd := if elaborate then @@ -1518,15 +806,15 @@ elab "sig_for%" name:ident : term => do pure <| .lit <| .strVal tt.stripTags -def highlightDataValue (v : DataValue) : Highlighted := +meta def highlightDataValue (v : DataValue) : Highlighted := .token <| match v with | .ofString (v : String) => ⟨.str v, toString v⟩ | .ofBool b => if b then - ⟨.const ``true (sig_for% true) (some <| docs_for% true) false none, "true"⟩ + ⟨.const ``true (sig_for% true) (some <| "The Boolean value `true`") false none, "true"⟩ else - ⟨.const ``false (sig_for% false) (some <| docs_for% false) false none, "false"⟩ + ⟨.const ``false (sig_for% false) (some <| "The Boolean value `false`") false none, "false"⟩ | .ofName (v : Name) => ⟨.unknown, v.toString⟩ | .ofNat (v : Nat) => ⟨.unknown, toString v⟩ | .ofInt (v : Int) => ⟨.unknown, toString v⟩ @@ -1534,10 +822,11 @@ def highlightDataValue (v : DataValue) : Highlighted := @[expose] def optionDocs.Args := Ident -instance : FromArgs optionDocs.Args DocElabM := ⟨.positional `name .ident "The option name"⟩ +meta instance : FromArgs optionDocs.Args DocElabM := ⟨.positional `name .ident "The option name"⟩ +open Block.Docstring in @[block_command] -def optionDocs : BlockCommandOf optionDocs.Args +meta def optionDocs : BlockCommandOf optionDocs.Args | x => do let optDecl ← getOptionDecl x.getId Doc.PointOfInterest.save x.raw optDecl.declName.toString @@ -1615,13 +904,14 @@ section variable [Monad m] [MonadError m] [MonadLiftT CoreM m] [MonadOptions m] -def TacticDocsOptions.parse : ArgParse m TacticDocsOptions := - TacticDocsOptions.mk <$> - .positional `name strOrName <*> - .named `show .string true <*> - .flag `replace false <*> - .flagM `allowMissing (verso.docstring.allowMissing.get <$> getOptions) - "Warn instead of error on missing docstrings (defaults to value of option `verso.docstring.allowMissing)" +meta instance : FromArgs TacticDocsOptions m where + fromArgs := + TacticDocsOptions.mk <$> + .positional `name strOrName <*> + .named `show .string true <*> + .flag `replace false <*> + .flagM `allowMissing (verso.docstring.allowMissing.get <$> getOptions) + "Warn instead of error on missing docstrings (defaults to value of option `verso.docstring.allowMissing)" where strOrName : ValDesc m (StrLit ⊕ Ident) := { description := "First token in tactic, or canonical parser name" @@ -1632,8 +922,6 @@ where | .num n => throwErrorAt n "Expected tactic name (either first token as string, or internal parser name)" } -instance : FromArgs TacticDocsOptions m := ⟨TacticDocsOptions.parse⟩ - end open Lean Elab Term Parser Tactic Doc in @@ -1651,7 +939,7 @@ private def getTactic (name : StrLit ⊕ Ident) : TermElabM TacticDoc := do open Lean Elab Term Parser Tactic Doc in -private def getTacticOverloads (name : StrLit ⊕ Ident) : TermElabM (Array TacticDoc) := do +private meta def getTacticOverloads (name : StrLit ⊕ Ident) : TermElabM (Array TacticDoc) := do let mut out := #[] for t in ← allTacticDocs do match name with @@ -1668,14 +956,15 @@ private def getTacticOverloads (name : StrLit ⊕ Ident) : TermElabM (Array Tact open Lean Elab Term Parser Tactic Doc in -private def getTactic? (name : String ⊕ Name) : TermElabM (Option TacticDoc) := do +private meta def getTactic? (name : String ⊕ Name) : TermElabM (Option TacticDoc) := do for t in ← allTacticDocs do if .inr t.internalName == name || .inl t.userName == name then return some t return none +open Block.Docstring in @[directive] -def tactic : DirectiveExpanderOf TacticDocsOptions +meta def tactic : DirectiveExpanderOf TacticDocsOptions | opts, more => do let tactics ← getTacticOverloads opts.name let blame : Syntax := opts.name.elim TSyntax.raw TSyntax.raw @@ -1775,15 +1064,13 @@ structure TacticInlineOptions where section variable [Monad m] [MonadError m] -def TacticInlineOptions.parse : ArgParse m TacticInlineOptions := - TacticInlineOptions.mk <$> .named `show .string true - -instance : FromArgs TacticInlineOptions m where - fromArgs := TacticInlineOptions.parse +meta instance : FromArgs TacticInlineOptions m where + fromArgs := + TacticInlineOptions.mk <$> .named `show .string true end @[role tactic] -def tacticInline : RoleExpanderOf TacticInlineOptions +meta def tacticInline : RoleExpanderOf TacticInlineOptions | {«show»}, inlines => do let #[arg] := inlines | throwError "Expected exactly one argument" @@ -1832,8 +1119,8 @@ structure ConvTacticDoc where docs? : Option String open Lean Elab Term Parser Tactic Doc in -def getConvTactic (name : StrLit ⊕ Ident) (allowMissing : Option Bool) : TermElabM ConvTacticDoc := - withOptions (allowMissing.map (fun b opts => verso.docstring.allowMissing.set opts b) |>.getD id) do +meta def getConvTactic (name : StrLit ⊕ Ident) (allowMissing : Option Bool) : TermElabM ConvTacticDoc := + withOptions (allowMissing.map (fun b opts => verso.docstring.allowMissing.set opts b) |>.getD (·)) do let .inr kind := name | throwError "Strings not yet supported here" let parserState := parserExtension.getState (← getEnv) @@ -1844,8 +1131,9 @@ def getConvTactic (name : StrLit ⊕ Ident) (allowMissing : Option Bool) : TermE return ⟨k, ← getDocString? (← getEnv) k⟩ throwError m!"Conv tactic not found: {kind}" +open Block.Docstring in @[directive] -def conv : DirectiveExpanderOf TacticDocsOptions +meta def conv : DirectiveExpanderOf TacticDocsOptions | opts, more => do let tactic ← getConvTactic opts.name opts.allowMissing Doc.PointOfInterest.save (← getRef) tactic.name.toString @@ -1921,7 +1209,7 @@ def conv.descr : BlockDescr := withHighlighting { extraCss := [docstringStyle] } -inline_extension Inline.conv (hl : Highlighted) via withHighlighting where +public inline_extension Inline.conv (hl : Highlighted) via withHighlighting where data := ToJson.toJson hl traverse _ _ _ := pure none toTeX := @@ -1940,7 +1228,7 @@ inline_extension Inline.conv (hl : Highlighted) via withHighlighting where hl.inlineHtml (g := Manual) "examples" @[role_expander conv] -def convInline : RoleExpander +meta def convInline : RoleExpander | _args, inlines => do let #[arg] := inlines | throwError "Expected exactly one argument" diff --git a/src/verso-manual/VersoManual/Docstring/DeclInfo.lean b/src/verso-manual/VersoManual/Docstring/DeclInfo.lean new file mode 100644 index 000000000..65e22b752 --- /dev/null +++ b/src/verso-manual/VersoManual/Docstring/DeclInfo.lean @@ -0,0 +1,248 @@ +/- +Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +module +meta import Verso.Instances.Deriving +public import Verso.Instances +import Lean.Data.Json.FromToJson.Basic +import Lean.PrivateName +import Lean.Modifiers +import Lean.Meta.Reduce +import Lean.Widget.InteractiveCode +import SubVerso.Highlighting.Highlighted +public import VersoManual.Docstring.Basic +public import VersoManual.Docstring.DocName +public import VersoManual.Docstring.PrettyPrint + +open Lean +open SubVerso.Highlighting + +private def renderTaggedInMeta (code : Lean.Widget.CodeWithInfos) : MetaM Highlighted := do + let hlCtx : SubVerso.Highlighting.Context := ⟨{}, false, false, [], false, (← IO.mkRef {})⟩ + (renderTagged none code : ReaderT SubVerso.Highlighting.Context MetaM _) hlCtx + + +namespace Verso.Genre.Manual.Block.Docstring + + +public inductive Visibility where + | «public» | «private» | «protected» +deriving Inhabited, Repr, ToJson, FromJson, DecidableEq, Ord, Quote + +public def Visibility.of (env : Environment) (n : Name) : Visibility := + if isPrivateName n then .private else if isProtected env n then .protected else .public + +public structure FieldInfo where + fieldName : Highlighted + /-- + What is the path by which the field was inherited? + [] if not inherited. + -/ + fieldFrom : List DocName + type : Highlighted + projFn : Name + /-- + It is `some parentStructName` if it is a subobject, and `parentStructName` is the name of + the parent structure. + -/ + subobject? : Option Name + binderInfo : BinderInfo + autoParam : Bool + docString? : Option String + visibility : Visibility +deriving Inhabited, Repr, ToJson, FromJson, Quote + + +public structure ParentInfo where + projFn : Name + name : Name + parent : Highlighted + index : Nat +deriving ToJson, FromJson, Quote + +public inductive DeclType where + /-- + A structure or class. The `constructor` field is `none` when the constructor is private. + -/ + | structure (isClass : Bool) (constructor : Option DocName) (fieldNames : Array Name) (fieldInfo : Array FieldInfo) (parents : Array ParentInfo) (ancestors : Array Name) + | def (safety : DefinitionSafety) + | opaque (safety : DefinitionSafety) + | inductive (constructors : Array DocName) (numArgs : Nat) (propOnly : Bool) + | axiom (safety : DefinitionSafety) + | theorem + | ctor (ofInductive : Name) (safety : DefinitionSafety) + | recursor (safety : DefinitionSafety) + | quotPrim (kind : QuotKind) + | other +deriving ToJson, FromJson, Quote + +public def DeclType.label : DeclType → String + | .structure false .. => "structure" + | .structure true .. => "type class" + | .def .safe => "def" + | .def .unsafe => "unsafe def" + | .def .partial => "partial def" + | .opaque .unsafe => "unsafe opaque" + | .opaque _ => "opaque" + | .inductive _ _ false => "inductive type" + | .inductive _ 0 true => "inductive proposition" + | .inductive _ _ true => "inductive predicate" + | .axiom .unsafe => "axiom" + | .axiom _ => "axiom" + | .theorem => "theorem" + | .ctor n _ => s!"constructor of {n}" + | .quotPrim _ => "primitive" + | .recursor .unsafe => "unsafe recursor" + | .recursor _ => "recursor" + | .other => "" + + +private partial def getStructurePathToBaseStructureAux (env : Environment) (baseStructName : Name) (structName : Name) (path : List Name) : Option (List Name) := + if baseStructName == structName then + some path.reverse + else + if let some info := getStructureInfo? env structName then + -- Prefer subobject projections + (info.fieldInfo.findSome? fun field => + match field.subobject? with + | none => none + | some parentStructName => getStructurePathToBaseStructureAux env baseStructName parentStructName (parentStructName :: path)) + -- Otherwise, consider other parents + <|> info.parentInfo.findSome? fun parent => + if parent.subobject then + none + else + getStructurePathToBaseStructureAux env baseStructName parent.structName (parent.structName :: path) + else none + +/-- +If `baseStructName` is an ancestor structure for `structName`, then return a sequence of projection functions +to go from `structName` to `baseStructName`. Returns `[]` if `baseStructName == structName`. +-/ +public def getStructurePathToBaseStructure? (env : Environment) (baseStructName : Name) (structName : Name) : Option (List Name) := + getStructurePathToBaseStructureAux env baseStructName structName [] + + +open Meta in +public def DeclType.ofName (c : Name) + (hideFields : Bool := false) + (hideStructureConstructor : Bool := false) : + MetaM DeclType := do + let env ← getEnv + + let openDecls : List OpenDecl := + match c with + | .str _ s => [.explicit c.getPrefix s.toName] + | _ => [] + if let some info := env.find? c then + match info with + | .defnInfo di => return .def di.safety + | .inductInfo ii => + if let some info := getStructureInfo? env c then + let ctor := getStructureCtor env c + let parentProjFns := getStructureParentInfo env c |>.map (·.projFn) + let parents ← + forallTelescopeReducing ii.type fun params _ => + withLocalDeclD `self (mkAppN (mkConst c (ii.levelParams.map mkLevelParam)) params) fun s => do + let selfType ← inferType s >>= whnf + let .const _structName us := selfType.getAppFn + | pure #[] + let params := selfType.getAppArgs + + parentProjFns.mapIdxM fun i parentProj => do + let proj := mkApp (mkAppN (.const parentProj us) params) s + let type ← inferType proj >>= instantiateMVars + let projType ← withOptions (·.set `format.width (40 : Int) |>.setBool `pp.tagAppFns true) <| Widget.ppExprTagged type + if let .const parentName _ := type.getAppFn then + pure ⟨parentProj, parentName, ← renderTaggedInMeta projType, i⟩ + else + pure ⟨parentProj, .anonymous, ← renderTaggedInMeta projType, i⟩ + let ancestors ← getAllParentStructures c + let allFields := if hideFields then #[] else getStructureFieldsFlattened env c (includeSubobjectFields := true) + let fieldInfo ← + forallTelescopeReducing ii.type fun params _ => + withLocalDeclD `self (mkAppN (mkConst c (ii.levelParams.map mkLevelParam)) params) fun s => + allFields.filterMapM fun fieldName => do + let proj ← mkProjection s fieldName + let type ← inferType proj >>= instantiateMVars + let type' ← withOptions (·.set `format.width (40 : Int) |>.setBool `pp.tagAppFns true) <| (Widget.ppExprTagged type) + let projType ← withOptions (·.set `format.width (40 : Int) |>.setBool `pp.tagAppFns true) <| ppExpr type + let fieldFrom? := findField? env c fieldName + let fieldPath? := fieldFrom? >>= (getStructurePathToBaseStructure? env · c) + let fieldFrom ← fieldPath?.getD [] |>.mapM (DocName.ofName (showUniverses := false)) + let subobject? := isSubobjectField? env (fieldFrom?.getD c) fieldName + let fieldInfo? := getFieldInfo? env (fieldFrom?.getD c) fieldName + + let binderInfo := fieldInfo?.map (·.binderInfo) |>.getD BinderInfo.default + let autoParam := fieldInfo?.map (·.autoParam?.isSome) |>.getD false + + if let some projFn := getProjFnForField? env c fieldName then + if isPrivateName projFn then + pure none + else + let docString? ← + -- Don't complain about missing docstrings for subobject projections + if subobject?.isSome then findDocString? env projFn + else getDocString? env projFn + let visibility := Visibility.of env projFn + let fieldName' := Highlighted.token ⟨.const projFn projType.pretty docString? true none, fieldName.toString⟩ + + pure <| some { fieldName := fieldName', fieldFrom, type := ← renderTaggedInMeta type', subobject?, projFn, binderInfo, autoParam, docString?, visibility} + else + let fieldName' := Highlighted.token ⟨.unknown, fieldName.toString⟩ + pure <| some { fieldName := fieldName', fieldFrom, type := ← renderTaggedInMeta type' , subobject?, projFn := .anonymous, binderInfo, autoParam, docString? := none, visibility := .public} + + let ctor? ← + if hideStructureConstructor || isPrivateName ctor.name then pure none + else some <$> DocName.ofName (showNamespace := true) (checkDocstring := false) ctor.name + + return .structure (isClass env c) ctor? info.fieldNames fieldInfo parents ancestors + + else + let ctors ← ii.ctors.mapM (DocName.ofName (ppWidth := 60) (showNamespace := false) (openDecls := openDecls)) + let t ← inferType <| .const c (ii.levelParams.map .param) + let t' ← reduceAll t + return .inductive ctors.toArray (ii.numIndices + ii.numParams) (isPred t') + | .opaqueInfo oi => return .opaque (if oi.isUnsafe then .unsafe else .safe) + | .axiomInfo ai => return .axiom (if ai.isUnsafe then .unsafe else .safe) + | .thmInfo _ => return .theorem + | .recInfo ri => return .recursor (if ri.isUnsafe then .unsafe else .safe) + | .ctorInfo ci => return .ctor ci.induct (if ci.isUnsafe then .unsafe else .safe) + | .quotInfo qi => return .quotPrim qi.kind + else + return .other +where + isPred : Expr → Bool + | .sort u => u.isZero + | .forallE _ _ e _ => isPred e + | .mdata _ e => isPred e + | .letE _ _ _ e _ => isPred e + | _ => false + +end Block.Docstring + +public def Signature.forName [Monad m] [MonadWithOptions m] [MonadEnv m] [MonadMCtx m] [MonadOptions m] [MonadResolveName m] [MonadNameGenerator m] [MonadLiftT MetaM m] [MonadLiftT BaseIO m] [MonadLiftT IO m] [MonadFileMap m] [Alternative m] (name : Name) : m Signature := do + let (⟨fmt, infos⟩ : FormatWithInfos) ← withOptions (·.setBool `pp.tagAppFns true) <| Block.Docstring.ppSignature name (constantInfo := false) + + let ctx := { + env := (← getEnv) + mctx := (← getMCtx) + options := (← getOptions) + currNamespace := (← getCurrNamespace) + openDecls := (← getOpenDecls) + fileMap := default + ngen := (← getNGen) + } + + let ttNarrow := Lean.Widget.TaggedText.prettyTagged (w := 42) fmt + let sigNarrow ← Lean.Widget.tagCodeInfos ctx infos ttNarrow + + let ttWide := Lean.Widget.TaggedText.prettyTagged (w := 72) fmt + let sigWide ← Lean.Widget.tagCodeInfos ctx infos ttWide + + return { + wide := ← renderTaggedInMeta sigWide + narrow := ← renderTaggedInMeta sigNarrow + } diff --git a/src/verso-manual/VersoManual/Docstring/Progress.lean b/src/verso-manual/VersoManual/Docstring/Progress.lean index 0234019a6..9309eef0a 100644 --- a/src/verso-manual/VersoManual/Docstring/Progress.lean +++ b/src/verso-manual/VersoManual/Docstring/Progress.lean @@ -35,7 +35,7 @@ public def Block.progress name := `Verso.Genre.Manual.Block.progress data := toJson (namespaces, exceptions, present, tactics) -private def ignore [Monad m] [MonadLiftT CoreM m] [MonadEnv m] (x : Name) : m Bool := do +private meta def ignore [Monad m] [MonadLiftT CoreM m] [MonadEnv m] (x : Name) : m Bool := do if (← Meta.Simp.isSimproc x) then return true let env ← getEnv return isPrivateName x || @@ -63,7 +63,7 @@ run_cmd do elabCommand <| ← `(private def $(mkIdent `allRootNames) : Array Name := #[$(names.map (quote · : Name → Term)),*]) @[directive] -public def progress : DirectiveExpanderOf Unit +public meta def progress : DirectiveExpanderOf Unit | (), blocks => do let mut namespaces : NameSet := {} let mut exceptions : NameSet := {} diff --git a/src/verso-manual/VersoManual/Docstring/Show.lean b/src/verso-manual/VersoManual/Docstring/Show.lean new file mode 100644 index 000000000..e0dde1dc9 --- /dev/null +++ b/src/verso-manual/VersoManual/Docstring/Show.lean @@ -0,0 +1,518 @@ +/- +Copyright (c) 2023-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +module + +public import MD4Lean +public import Verso.Doc.Elab.Monad +import VersoManual.Docstring.Config +import VersoManual.HighlightedCode +import VersoManual.Markdown +public import VersoManual.Basic +import SubVerso.Highlighting +import Verso.Code.Highlighted +import Lean.Data.Json.FromToJson.Basic +import Lean.DocString +import Lean.Elab.Tactic.Doc +import Verso.Doc.DocName + +public section + +open Verso.Doc.Elab +open SubVerso.Highlighting +open Lean + +namespace Verso.Genre.Manual + +/-- Finds the minimum indentation column across non-blank lines in a string. -/ +def indentColumn (str : String) : Nat := Id.run do + let mut i : Option Nat := none + for line in str.splitToList (· == '\n') do + let leading := line.takeWhile Char.isWhitespace + if leading == line.toSlice then continue + let leading := leading.copy + if let some i' := i then + if leading.length < i' then i := some leading.length + else i := some leading.length + return i.getD 0 + +def leanFromMarkdown := () + +def Inline.leanFromMarkdown (hls : Highlighted) : Inline where + name := ``Verso.Genre.Manual.leanFromMarkdown + data := ToJson.toJson hls + +def Block.leanFromMarkdown (hls : Highlighted) : Block where + name := ``Verso.Genre.Manual.leanFromMarkdown + data := ToJson.toJson hls + + +@[inline_extension leanFromMarkdown] +def leanFromMarkdown.inlinedescr : InlineDescr := withHighlighting { + traverse _id _data _ := pure none + toTeX := some <| fun go _ _ content => content.mapM go + toHtml := + open Verso.Output Html in + open Verso.Doc.Html in + some <| fun _ _ data _ => do + match FromJson.fromJson? (α := Highlighted) data with + | .error err => + HtmlT.logError <| "Couldn't deserialize Lean code while rendering inline HTML: " ++ err + pure .empty + | .ok (hl : Highlighted) => + hl.inlineHtml (g := Manual) "docstring-examples" +} + +@[block_extension leanFromMarkdown] +def leanFromMarkdown.blockdescr : BlockDescr := withHighlighting { + traverse _id _data _ := pure none + toTeX := + some <| fun _goI goB _ _ content => do + pure <| .seq <| ← content.mapM fun b => do + pure <| .seq #[← goB b, .raw "\n"] + toHtml := + open Verso.Output Html in + open Verso.Doc.Html in + some <| fun _ _ _ data _ => do + match FromJson.fromJson? (α := Highlighted) data with + | .error err => + HtmlT.logError <| "Couldn't deserialize Lean code while rendering inline HTML: " ++ err + pure .empty + | .ok (hl : Highlighted) => + hl.blockHtml (g := Manual) "docstring-examples" +} + +namespace Block.Docstring + + +open Lean Elab Term in +def tryElabBlockCodeCommand (str : String) (ignoreElabErrors := false) : DocElabM Term := do + let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos + let src := + if let some ⟨line, col⟩ := loc then s!"" + else s!"" + + let ictx := Parser.mkInputContext str src + let cctx : Command.Context := { fileName := ← getFileName, fileMap := FileMap.ofString str, snap? := none, cancelTk? := none} + + let mut cmdState : Command.State := {env := ← getEnv, maxRecDepth := ← MonadRecDepth.getMaxRecDepth, scopes := [{header := ""}]} + let mut pstate := {pos := 0, recovering := false} + let mut cmds := #[] + + repeat + let scope := cmdState.scopes.head! + let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls } + let (cmd, ps', messages) := Parser.parseCommand ictx pmctx pstate cmdState.messages + cmds := cmds.push cmd + pstate := ps' + cmdState := {cmdState with messages := messages} + + cmdState ← withInfoTreeContext (mkInfoTree := pure ∘ InfoTree.node (.ofCommandInfo {elaborator := `Manual.Meta.lean, stx := cmd})) do + match (← liftM <| EIO.toIO' <| (Command.elabCommand cmd cctx).run cmdState) with + | Except.error e => + unless ignoreElabErrors do Lean.logError e.toMessageData + return cmdState + | Except.ok ((), s) => return s + + if Parser.isTerminalCommand cmd then break + + if cmdState.messages.hasErrors then + throwError "Errors found in command" + + let hls ← DocElabM.withFileMap (.ofString str) do + let mut hls := Highlighted.empty + for cmd in cmds do + hls := hls ++ (← highlight cmd cmdState.messages.toArray cmdState.infoState.trees) + pure <| hls.deIndent (indentColumn str) + + ``(Verso.Doc.Block.other (Block.leanFromMarkdown $(quote hls)) #[Verso.Doc.Block.code $(quote str)]) + + +open Lean Elab Term in +def tryElabInlineCodeName (str : String) : DocElabM Term := do + let str := str.trimAscii + let x := str.toName + if x.toString.toSlice == str then + let stx := mkIdent x + let n ← realizeGlobalConstNoOverload stx + let str := str.copy + let hl : Highlighted ← constTok n str + ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hl)) #[Verso.Doc.Inline.code $(quote str)]) + else + throwError "Not a name: '{str}'" +where + constTok {m} [Monad m] [MonadEnv m] [MonadLiftT MetaM m] [MonadLiftT IO m] + (name : Name) (str : String) : + m Highlighted := do + let docs ← findDocString? (← getEnv) name + let sig := toString (← (PrettyPrinter.ppSignature name)).1 + pure <| .token ⟨.const name sig docs false none, str⟩ + +open Lean Elab Term in +private def attempt (str : String) (xs : List (String → DocElabM α)) : DocElabM α := do + match xs with + | [] => throwError "No attempt succeeded" + | [x] => x str + | x::y::xs => + let info ← getInfoState + try + setInfoState {} + x str + catch e => + if isAutoBoundImplicitLocalException? e |>.isSome then + throw e + else attempt str (y::xs) + finally + setInfoState info + +open Lean Elab Term in +def tryParseInlineCodeTactic (str : String) : DocElabM Term := do + let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos + let src := + if let some ⟨line, col⟩ := loc then s!"" + else s!"" + match Parser.runParserCategory (← getEnv) `tactic str src with + | .error e => throw (.error (← getRef) e) + | .ok stx => DocElabM.withFileMap (.ofString str) <| do + -- TODO try actually running the tactic - if the parameters are simple enough, then it may work + -- and give better highlights + let hls ← highlight stx #[] (PersistentArray.empty) + ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)]) + +open Lean Elab Term in +def tryInlineOption (str : String) : DocElabM Term := do + let optName := str.trimAscii.toName + let optDecl ← getOptionDecl optName + let hl : Highlighted := optTok optName optDecl.declName optDecl.descr + ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hl)) #[Verso.Doc.Inline.code $(quote str)]) +where + optTok (name declName : Name) (descr : String) : Highlighted := + .token ⟨.option name declName descr, name.toString⟩ + +open Lean Elab in +def tryTacticName (tactics : Array Tactic.Doc.TacticDoc) (str : String) : DocElabM Term := do + for t in tactics do + if t.userName == str then + let hl : Highlighted := tacToken t + return ← ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hl)) #[Verso.Doc.Inline.code $(quote str)]) + throwError "Not a tactic name: {str}" +where + tacToken (t : Lean.Elab.Tactic.Doc.TacticDoc) : Highlighted := + .token ⟨.keyword t.internalName none t.docString, str⟩ + +open Lean Elab Term in +open Lean.Parser in +def tryHighlightKeywords (extraKeywords : Array String) (str : String) : DocElabM Term := do + let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos + let src := + if let some ⟨line, col⟩ := loc then s!"" + else s!"" + let p : Parser := {fn := simpleFn} + match runParser extraKeywords (← getEnv) (← getOptions) p str src (prec := 0) with + | .error _e => throwError "Not keyword-highlightable" + | .ok stx => DocElabM.withFileMap (.ofString str) <| do + let hls ← highlight stx #[] (PersistentArray.empty) + ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)]) +where + + simpleFn := andthenFn whitespace <| nodeFn nullKind <| manyFn tokenFn + + runParser (extraKeywords : Array String) (env : Environment) (opts : Lean.Options) (p : Parser) (input : String) (fileName : String := "") (prec : Nat := 0) : Except (List (Position × String)) Syntax := + let ictx := mkInputContext input fileName + let p' := adaptCacheableContext ({· with prec}) p + let tokens := extraKeywords.foldl (init := getTokenTable env) (fun x tk => x.insert tk tk) + let s := p'.fn.run ictx { env, options := opts } tokens (mkParserState input) + if !s.allErrors.isEmpty then + Except.error (toErrorMsg ictx s) + else if ictx.atEnd s.pos then + Except.ok s.stxStack.back + else + Except.error (toErrorMsg ictx (s.mkError "end of input")) + + toErrorMsg (ctx : InputContext) (s : ParserState) : List (Position × String) := Id.run do + let mut errs := [] + for (pos, _stk, err) in s.allErrors do + let pos := ctx.fileMap.toPosition pos + errs := (pos, toString err) :: errs + errs.reverse + + +declare_syntax_cat braces_attr +syntax (name := plain) attr : braces_attr +syntax (name := bracketed) "[" attr "]" : braces_attr +syntax (name := atBracketed) "@[" attr "]" : braces_attr + +private def getAttr : Syntax → Syntax + | `(plain| $a) + | `(bracketed| [ $a ] ) + | `(atBracketed| @[ $a ]) => a + | _ => .missing + +open Lean Elab Term in +def tryParseInlineCodeAttribute (validate := true) (str : String) : DocElabM Term := do + let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos + let src := + if let some ⟨line, col⟩ := loc then s!"" + else s!"" + match Parser.runParserCategory (← getEnv) `braces_attr str src with + | .error e => throw (.error (← getRef) e) + | .ok stx => DocElabM.withFileMap (.ofString str) <| do + let inner := getAttr stx + if validate then + let attrName ← + match inner.getKind with + | `Lean.Parser.Attr.simple => pure inner[0].getId + | .str (.str (.str (.str .anonymous "Lean") "Parser") "Attr") k => pure k.toName + | other => + let allAttrs := attributeExtension.getState (← getEnv) |>.map |>.toArray |>.map (·.fst) |>.qsort (·.toString < ·.toString) + throwError "Failed to process attribute kind: {stx.getKind} {isAttribute (← getEnv) stx.getKind} {allAttrs |> repr}" + match getAttributeImpl (← getEnv) attrName with + | .error e => throwError e + | .ok _ => + let hls ← highlight stx #[] (PersistentArray.empty) + ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)]) + else + let hls ← highlight stx #[] (PersistentArray.empty) + ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)]) + +open Lean Elab Term in +def tryElabInlineCodeUsing (elabs : List (String → DocElabM Term)) + (priorWord : Option String) (str : String) : DocElabM Term := do + -- Don't try to show Lake commands as terms + if "lake ".isPrefixOf str then return (← ``(Verso.Doc.Inline.code $(quote str))) + try + attempt str <| wordElab priorWord ++ elabs + catch + | .error ref e => + logWarningAt ref e + ``(Verso.Doc.Inline.code $(quote str)) + | e => + if isAutoBoundImplicitLocalException? e |>.isSome then + throw e + else + logWarning m!"Internal exception uncaught: {e.toMessageData}" + ``(Verso.Doc.Inline.code $(quote str)) +where + wordElab + | some "attribute" => [tryParseInlineCodeAttribute (validate := false)] + | some "tactic" => [tryParseInlineCodeTactic] + | _ => [] + +open Lean Elab Term in +def tryElabCodeTermWith (mk : Highlighted → String → DocElabM α) (str : String) (ignoreElabErrors := false) (identOnly := false) : DocElabM α := do + let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos + let src := + if let some ⟨line, col⟩ := loc then s!"" + else s!"" + match Parser.runParserCategory (← getEnv) `term str src with + | .error e => throw (.error (← getRef) e) + | .ok stx => DocElabM.withFileMap (.ofString str) <| do + if stx.isIdent && (← readThe Term.Context).autoBoundImplicitContext.isSome then + throwError m!"Didn't elaborate {stx} as term to avoid spurious auto-implicits" + if identOnly && !stx.isIdent then + throwError m!"Didn't elaborate {stx} as term because only identifiers are wanted here" + let (newMsgs, tree, _e) ← do + let initMsgs ← Core.getMessageLog + try + Core.resetMessageLog + -- TODO open decls/current namespace + let (tree', e') ← do + let e ← Elab.Term.elabTerm (catchExPostpone := true) stx none + Term.synthesizeSyntheticMVarsNoPostponing + let e' ← Term.levelMVarToParam (← instantiateMVars e) + Term.synthesizeSyntheticMVarsNoPostponing + let e' ← instantiateMVars e' + let ctx := PartialContextInfo.commandCtx { + env := ← getEnv, fileMap := ← getFileMap, mctx := ← getMCtx, currNamespace := ← getCurrNamespace, + openDecls := ← getOpenDecls, options := ← getOptions, ngen := ← getNGen + } + pure (InfoTree.context ctx (.node (Info.ofCommandInfo ⟨`Verso.Genre.Manual.docstring, (← getRef)⟩) (← getInfoState).trees), e') + pure (← Core.getMessageLog, tree', e') + finally + Core.setMessageLog initMsgs + if newMsgs.hasErrors && !ignoreElabErrors then + for msg in newMsgs.errorsToWarnings.toArray do + logMessage msg + throwError m!"Didn't elaborate {stx} as term" + + let hls ← highlight stx #[] (PersistentArray.empty.push tree) + mk hls str + + +declare_syntax_cat doc_metavar +syntax (name := docMetavar) term ":" term : doc_metavar + + +open Lean Elab Term in +def tryElabCodeMetavarTermWith (mk : Highlighted → String → DocElabM α) (str : String) (ignoreElabErrors := false) : DocElabM α := do + let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos + let src := + if let some ⟨line, col⟩ := loc then s!"" + else s!"" + match Parser.runParserCategory (← getEnv) `doc_metavar str src with + | .error e => throw (.error (← getRef) e) + | .ok stx => DocElabM.withFileMap (.ofString str) <| do + if let `(doc_metavar|$pat:term : $ty:term) := stx then + let (newMsgs, tree, _e') ← show TermElabM _ from do + let initMsgs ← Core.getMessageLog + try + Core.resetMessageLog + -- TODO open decls/current namespace + let (tree', e') ← do + let stx' : Term ← `(($pat : $ty)) + let e ← withReader ({· with autoBoundImplicitContext := some ⟨true, {}⟩}) <| elabTerm stx' none + Term.synthesizeSyntheticMVarsNoPostponing + let e' ← Term.levelMVarToParam (← instantiateMVars e) + Term.synthesizeSyntheticMVarsNoPostponing + let e' ← instantiateMVars e' + let ctx := PartialContextInfo.commandCtx { + env := ← getEnv, fileMap := ← getFileMap, mctx := ← getMCtx, currNamespace := ← getCurrNamespace, + openDecls := ← getOpenDecls, options := ← getOptions, ngen := ← getNGen + } + pure (InfoTree.context ctx (.node (Info.ofCommandInfo ⟨`Verso.Genre.Manual.docstring, stx⟩) (← getInfoState).trees), e') + pure (← Core.getMessageLog, tree', e') + finally + Core.setMessageLog initMsgs + if newMsgs.hasErrors && !ignoreElabErrors then + for msg in newMsgs.errorsToWarnings.toArray do + logMessage msg + throwError m!"Didn't elaborate {pat} : {ty} as term" + + let hls ← highlight stx #[] (PersistentArray.empty.push tree) + mk hls str + else + throwError "Not a doc metavar: {stx}" + +open Lean Elab Term in +def tryElabInlineCodeTerm (str : String) (ignoreElabErrors := false) (identOnly := false) : DocElabM Term := + tryElabCodeTermWith (ignoreElabErrors := ignoreElabErrors) (identOnly := identOnly) (fun hls str => + ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)])) + str + +open Lean Elab Term in +def tryElabInlineCodeMetavarTerm (str : String) (ignoreElabErrors := false) : DocElabM Term := + tryElabCodeMetavarTermWith (ignoreElabErrors := ignoreElabErrors) (fun hls str => + ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)])) + str + +open Lean Elab Term in +def tryElabBlockCodeTerm (str : String) (ignoreElabErrors := false) : DocElabM Term := + tryElabCodeTermWith (ignoreElabErrors := ignoreElabErrors) (fun hls str => + ``(Verso.Doc.Block.other (Block.leanFromMarkdown $(quote hls)) #[Verso.Doc.Block.code $(quote str)])) + str + + +open Elab in +/-- +Like `tryElabInlineCode`, but prefers producing un-highlighted code blocks to +displaying metavariable-typed terms (e.g., through auto-bound implicits or +elaboration failures). +-/ +def tryElabInlineCodeStrict (allTactics : Array Tactic.Doc.TacticDoc) (extraKeywords : Array String) + (priorWord : Option String) (str : String) : DocElabM Term := + tryElabInlineCodeUsing [ + tryElabInlineCodeName, + -- When identifiers have the same name as tactics, prefer the identifiers + tryElabInlineCodeTerm (identOnly := true), + tryParseInlineCodeTactic, + tryParseInlineCodeAttribute (validate := true), + tryInlineOption, + tryElabInlineCodeTerm, + tryElabInlineCodeMetavarTerm, + tryTacticName allTactics, + tryHighlightKeywords extraKeywords + ] priorWord str + +open Lean Elab Term in +def tryElabBlockCode (_info? _lang? : Option String) (str : String) : DocElabM Term := do + try + attempt str [ + tryElabBlockCodeCommand, + tryElabBlockCodeTerm, + tryElabBlockCodeCommand (ignoreElabErrors := true), + withTheReader Term.Context (fun ctx => {ctx with autoBoundImplicitContext := some ⟨true, {}⟩}) ∘ + tryElabBlockCodeTerm (ignoreElabErrors := true) + ] + catch + | .error ref e => + logWarningAt ref e + ``(Verso.Doc.Block.code $(quote str)) + | e => + if isAutoBoundImplicitLocalException? e |>.isSome then + throw e + else + logWarning m!"Internal exception uncaught: {e.toMessageData}" + ``(Verso.Doc.Block.code $(quote str)) + + + +open Elab in +def tryElabInlineCode (allTactics : Array Tactic.Doc.TacticDoc) (extraKeywords : Array String) + (priorWord : Option String) (str : String) : DocElabM Term := + tryElabInlineCodeUsing [ + tryElabInlineCodeName, + -- When identifiers have the same name as tactics, prefer the identifiers + tryElabInlineCodeTerm (identOnly := true), + tryParseInlineCodeTactic, + tryParseInlineCodeAttribute (validate := true), + tryInlineOption, + tryElabInlineCodeTerm, + tryElabInlineCodeMetavarTerm, + tryTacticName allTactics, + withTheReader Term.Context (fun ctx => {ctx with autoBoundImplicitContext := some ⟨true, {}⟩}) ∘ tryElabInlineCodeTerm, + tryElabInlineCodeTerm (ignoreElabErrors := true), + tryHighlightKeywords extraKeywords + ] priorWord str + + +open Lean Elab Term in +/-- +Heuristically elaborate Lean fragments in Markdown code. The provided names are used as signatures, +from left to right, with the names bound by the signature being available in the local scope in +which the Lean fragments are elaborated. +-/ +public def blockFromMarkdownWithLean (names : List Name) (b : MD4Lean.Block) : DocElabM Term := do + unless (← Docstring.getElabMarkdown) do + return (← Markdown.blockFromMarkdown b (handleHeaders := Markdown.strongEmphHeaders)) + let tactics ← Elab.Tactic.Doc.allTacticDocs + let keywords := tactics.map (·.userName) + try + match names with + | decl :: decls => + -- This brings the parameters into scope, so the term elaboration version catches them! + Meta.forallTelescopeReducing (← getConstInfo decl).type fun _ _ => + blockFromMarkdownWithLean decls b + | [] => + -- It'd be silly for some weird edge case to block on this feature... + let rec loop (max : Nat) (s : SavedState) : DocElabM Term := do + match max with + | k + 1 => + try + let res ← + Markdown.blockFromMarkdown b + (handleHeaders := Markdown.strongEmphHeaders) + (elabInlineCode := tryElabInlineCode tactics keywords) + (elabBlockCode := tryElabBlockCode) + synthesizeSyntheticMVarsUsingDefault + + discard <| addAutoBoundImplicits #[] (inlayHintPos? := none) + + return res + catch e => + if let some n := isAutoBoundImplicitLocalException? e then + s.restore (restoreInfo := true) + Meta.withLocalDecl n .implicit (← Meta.mkFreshTypeMVar) fun x => + withTheReader Term.Context (fun ctx => { ctx with autoBoundImplicitContext := ctx.autoBoundImplicitContext.map (fun c => {c with boundVariables := c.boundVariables.push x }) }) do + loop k (← (saveState : TermElabM _)) + else throw e + | 0 => throwError "Ran out of local name attempts" + let s ← (saveState : TermElabM _) + try + loop 40 s + finally + (s.restore : TermElabM _) + catch _ => + Markdown.blockFromMarkdown b + (handleHeaders := Markdown.strongEmphHeaders) diff --git a/src/verso-manual/VersoManual/Draft.lean b/src/verso-manual/VersoManual/Draft.lean index 1198b1680..1205fb479 100644 --- a/src/verso-manual/VersoManual/Draft.lean +++ b/src/verso-manual/VersoManual/Draft.lean @@ -11,6 +11,8 @@ import Std.Data.HashSet import Verso.Doc.ArgParse import Verso.Doc.Elab +public meta import Verso.Doc.Elab.Block +public meta import Verso.Doc.Elab.Inline public import Verso.Doc.Elab.Monad meta import Verso.Doc.Elab.Monad public import VersoManual.Basic @@ -25,7 +27,7 @@ public section namespace Verso.Genre.Manual -inline_extension Inline.draft where +public inline_extension Inline.draft where traverse _id _data _contents := do if (← isDraft) then pure none @@ -39,7 +41,7 @@ inline_extension Inline.draft where some <| fun go _ _ content => do content.mapM go -block_extension Block.draft where +public block_extension Block.draft where traverse _id _data _contents := do if (← isDraft) then pure none @@ -55,12 +57,12 @@ block_extension Block.draft where /-- Hide draft-only content when in not in draft mode -/ @[role] -def draft : RoleExpanderOf Unit +meta def draft : RoleExpanderOf Unit | (), contents => do ``(Verso.Doc.Inline.other Inline.draft #[$[$(← contents.mapM elabInline)],*]) /-- Hide draft-only content when in not in draft mode -/ @[directive draft] -def draftBlock : DirectiveExpanderOf Unit +meta def draftBlock : DirectiveExpanderOf Unit | (), contents => do ``(Verso.Doc.Block.other Block.draft #[$[$(← contents.mapM elabBlock)],*]) diff --git a/src/verso-manual/VersoManual/ExternalLean.lean b/src/verso-manual/VersoManual/ExternalLean.lean index 2a96b16b4..792a55cdd 100644 --- a/src/verso-manual/VersoManual/ExternalLean.lean +++ b/src/verso-manual/VersoManual/ExternalLean.lean @@ -3,13 +3,15 @@ Copyright (c) 2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ - +module import Verso -import VersoManual.Basic +public import VersoManual.Basic import VersoManual.HighlightedCode -import Verso.Code.External +public import Verso.Code.External import Verso.Code.HighlightedToTex -import SubVerso.Examples.Messages +public import SubVerso.Examples.Messages + +public section set_option linter.missingDocs true @@ -18,15 +20,14 @@ open Lean.Meta.Hint open Verso Log Doc Elab ArgParse Genre.Manual Code Output Html Highlighted WebAssets open SubVerso.Highlighting -open SubVerso.Examples.Messages + open Std open Verso.Code.External namespace Verso.Genre.Manual - -block_extension Block.lean (hls : Highlighted) (cfg : CodeConfig) via withHighlighting where +public block_extension Block.lean (hls : Highlighted) (cfg : CodeConfig) via withHighlighting where init st := st.addQuickJumpMapper exampleDomain exampleDomainMapper data := @@ -87,7 +88,7 @@ block_extension Block.lean (hls : Highlighted) (cfg : CodeConfig) via withHighli withReader ({ · with codeOptions.inlineProofStates := cfg.showProofStates, codeOptions.definitionsAsTargets := cfg.defSite.getD true }) <| hl.blockHtml (g := Manual) "examples" -inline_extension Inline.lean (hls : Highlighted) (cfg : CodeConfig) via withHighlighting where +public inline_extension Inline.lean (hls : Highlighted) (cfg : CodeConfig) via withHighlighting where data := let defined := definedNames hls Json.arr #[ToJson.toJson cfg, ToJson.toJson hls, ToJson.toJson defined] @@ -148,7 +149,7 @@ inline_extension Inline.lean (hls : Highlighted) (cfg : CodeConfig) via withHigh codeOptions.inlineProofStates := cfg.showProofStates, codeOptions.definitionsAsTargets := cfg.defSite.getD false }) <| hl.inlineHtml (g := Manual) "examples" -block_extension Block.leanOutput +public block_extension Block.leanOutput (message : Highlighted.Message) (summarize : Bool := false) (expandTraces : List Name := []) via withHighlighting where data := ToJson.toJson (message, summarize, expandTraces) @@ -175,7 +176,7 @@ block_extension Block.leanOutput msg.blockHtml summarize expandTraces (g := Manual) -inline_extension Inline.leanOutput +public inline_extension Inline.leanOutput (message : Highlighted.Message) (plain : Bool) (expandTraces : List Name) via withHighlighting where data := ToJson.toJson (message, plain, expandTraces) @@ -206,7 +207,7 @@ inline_extension Inline.leanOutput open Verso.Code.External -instance : ExternalCode Manual where +public instance : ExternalCode Manual where leanInline hl cfg := .other (Inline.lean hl cfg) #[] leanBlock hl cfg := diff --git a/src/verso-manual/VersoManual/Glossary.lean b/src/verso-manual/VersoManual/Glossary.lean index 4807039e1..aab704b64 100644 --- a/src/verso-manual/VersoManual/Glossary.lean +++ b/src/verso-manual/VersoManual/Glossary.lean @@ -8,9 +8,12 @@ import Lean.Data.Json import Lean.Data.Json.FromToJson import Verso.Doc.Elab -import Verso.Doc.PointOfInterest +public meta import Verso.Doc.PointOfInterest public import VersoManual.Basic +public import VersoManual.Glossary.Norm +public meta import VersoManual.Glossary.Norm public import Verso.Doc.Elab.Monad +public meta import Verso.Doc.Elab.Inline open Verso Genre Manual ArgParse open Verso.Doc.Elab @@ -29,17 +32,11 @@ public structure TechArgs extends DefTechArgs where section variable [Monad m] [Lean.MonadError m] [MonadLiftT Lean.CoreM m] -def DefTechArgs.parse : ArgParse m DefTechArgs := - DefTechArgs.mk <$> .named `key .string true <*> .flag `normalize true +public meta instance : FromArgs DefTechArgs m where + fromArgs := DefTechArgs.mk <$> .named `key .string true <*> .flag `normalize true -public instance : FromArgs DefTechArgs m where - fromArgs := private DefTechArgs.parse - -def TechArgs.parse : ArgParse m TechArgs := - TechArgs.mk <$> fromArgs <*> .named `remote .string true - -public instance : FromArgs TechArgs m where - fromArgs := private TechArgs.parse +public meta instance : FromArgs TechArgs m where + fromArgs := TechArgs.mk <$> fromArgs <*> .named `remote .string true end @@ -50,7 +47,7 @@ private theorem glossaryState.isPublic : NameMap.isPublic glossaryState := by gr public def Inline.deftech : Inline where name := `Verso.Genre.Manual.deftech -private partial def techString (text : Doc.Inline Manual) : String := +public partial def techString (text : Doc.Inline Manual) : String := match text with | .code str | .math _ str | .text str | .linebreak str => str | .image .. | .footnote .. => "" @@ -60,17 +57,6 @@ private partial def techString (text : Doc.Inline Manual) : String := | .emph txt | .link txt _href => String.join <| txt.toList.map techString --- Implements the normalization procedure used in Scribble -private partial def normString (term : String) : String := Id.run do - let mut str := term.toLower - if str.endsWith "ies" then - str := (str.dropEnd 3).copy ++ "y" - if str.endsWith "s" then - str := str.dropEnd 1 |>.copy - str := str.replace "‑" "-" - String.intercalate " " (str.splitToList (fun c => c.isWhitespace || c == '-') |>.filter (!·.isEmpty)) - - open Lean in /-- Defines a technical term. @@ -88,7 +74,7 @@ of the automatically-derived key. Uses of `tech` use the same process to derive a key, and the key is matched against the `deftech` table. -/ @[role] -public def deftech : RoleExpanderOf DefTechArgs +public meta def deftech : RoleExpanderOf DefTechArgs | {key, normalize}, content => do -- Heuristically guess at the string and key (usually works) @@ -185,7 +171,7 @@ Call with `(normalize := false)` to disable normalization, and `(key := some k)` of the automatically-derived key. -/ @[role] -public def tech : RoleExpanderOf TechArgs +public meta def tech : RoleExpanderOf TechArgs | {key, normalize, remote}, content => do -- Heuristically guess at the string and key (usually works) diff --git a/src/verso-manual/VersoManual/Glossary/Norm.lean b/src/verso-manual/VersoManual/Glossary/Norm.lean new file mode 100644 index 000000000..fc282edb9 --- /dev/null +++ b/src/verso-manual/VersoManual/Glossary/Norm.lean @@ -0,0 +1,17 @@ +/- +Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +module +namespace Verso.Genre.Manual + +-- Implements the normalization procedure used in Scribble +public partial def normString (term : String) : String := Id.run do + let mut str := term.toLower + if str.endsWith "ies" then + str := (str.dropEnd 3).copy ++ "y" + if str.endsWith "s" then + str := str.dropEnd 1 |>.copy + str := str.replace "‑" "-" + String.intercalate " " (str.splitToList (fun c => c.isWhitespace || c == '-') |>.filter (!·.isEmpty)) diff --git a/src/verso-manual/VersoManual/Imports.lean b/src/verso-manual/VersoManual/Imports.lean index 3e89cdd61..2c39ab743 100644 --- a/src/verso-manual/VersoManual/Imports.lean +++ b/src/verso-manual/VersoManual/Imports.lean @@ -3,11 +3,12 @@ Copyright (c) 2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ - +module import Verso.Doc.ArgParse import Verso.Doc.Elab import SubVerso.Highlighting.Code import VersoManual.ExternalLean +public import Verso.Doc.Elab.Monad open scoped Lean.Doc.Syntax @@ -19,17 +20,17 @@ open ArgParse namespace Verso.Genre.Manual -structure ImportsParams where +public structure ImportsParams where «show» : Bool := true -instance : FromArgs ImportsParams m where +public meta instance : FromArgs ImportsParams m where fromArgs := ImportsParams.mk <$> .flag `show true (some "Whether to show the import header") /-- Parses, but does not validate, a module header. -/ @[code_block] -def imports : CodeBlockExpanderOf ImportsParams +public meta def imports : CodeBlockExpanderOf ImportsParams | { «show» } , str => do let altStr ← parserInputString str let p := Parser.whitespace >> Parser.Module.header.fn diff --git a/src/verso-manual/VersoManual/InlineLean.lean b/src/verso-manual/VersoManual/InlineLean.lean index 3e6a4c1ab..f4254015a 100644 --- a/src/verso-manual/VersoManual/InlineLean.lean +++ b/src/verso-manual/VersoManual/InlineLean.lean @@ -3,22 +3,34 @@ Copyright (c) 2024-2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ - +module import Lean.Elab.Command +import Lean.Elab.GuardMsgs import Lean.Elab.InfoTree -import SubVerso.Highlighting -import SubVerso.Examples +public import SubVerso.Highlighting +public import SubVerso.Examples.Messages.NormalizeMetavars +public meta import SubVerso.Examples.Messages import Verso -import VersoManual.Basic +public import Verso.Doc.Elab.Monad +public import Verso.Doc.Elab.Block +public meta import Verso.Doc.Helpers +public meta import Verso.Doc.PointOfInterest +public meta import Verso.Hint +public meta import Verso.Log +public meta import Verso.WithoutAsync +public import VersoManual.Basic import VersoManual.HighlightedCode -import VersoManual.InlineLean.Block +public import VersoManual.InlineLean.Block import VersoManual.InlineLean.IO -import VersoManual.InlineLean.LongLines +public meta import VersoManual.InlineLean.LongLines +public import VersoManual.InlineLean.LongLines import VersoManual.InlineLean.Option import VersoManual.InlineLean.Outputs +public meta import VersoManual.InlineLean.Outputs +public meta import VersoManual.InlineLean.Scopes import VersoManual.InlineLean.Scopes import VersoManual.InlineLean.Signature import VersoManual.InlineLean.SyntaxError @@ -35,7 +47,7 @@ open Lean.Elab.Tactic.GuardMsgs namespace Verso.Genre.Manual.InlineLean -inline_extension Inline.lean (hls : Highlighted) via withHighlighting where +public inline_extension Inline.lean (hls : Highlighted) via withHighlighting where data := let defined := definedNames hls Json.arr #[ToJson.toJson hls, ToJson.toJson defined] @@ -77,26 +89,26 @@ section Config variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] -structure LeanBlockConfig where +public structure LeanBlockConfig where «show» : Bool keep : Bool name : Option Name error : Bool fresh : Bool -def LeanBlockConfig.parse : ArgParse m LeanBlockConfig := - LeanBlockConfig.mk <$> .flag `show true <*> .flag `keep true <*> .named `name .name true <*> .flag `error false <*> .flag `fresh false - -instance : FromArgs LeanBlockConfig m := ⟨LeanBlockConfig.parse⟩ +public meta instance : FromArgs LeanBlockConfig m where + fromArgs := + LeanBlockConfig.mk <$> .flag `show true <*> .flag `keep true <*> .named `name .name true <*> .flag `error false <*> .flag `fresh false -structure LeanInlineConfig extends LeanBlockConfig where +public structure LeanInlineConfig extends LeanBlockConfig where /-- The expected type of the term -/ type : Option StrLit /-- Universe variables allowed in the term -/ universes : Option StrLit -def LeanInlineConfig.parse : ArgParse m LeanInlineConfig := - LeanInlineConfig.mk <$> LeanBlockConfig.parse <*> .named `type strLit true <*> .named `universes strLit true +public meta instance : FromArgs LeanInlineConfig m where + fromArgs := + LeanInlineConfig.mk <$> fromArgs <*> .named `type strLit true <*> .named `universes strLit true where strLit : ValDesc m StrLit := { description := "string literal containing an expected type", @@ -106,19 +118,17 @@ where | other => throwError "Expected string, got {repr other}" } -instance : FromArgs LeanInlineConfig m := ⟨LeanInlineConfig.parse⟩ - end Config open Verso.Genre.Manual.InlineLean.Scopes (getScopes setScopes runWithOpenDecls runWithVariables) -private def abbrevFirstLine (width : Nat) (str : String) : String := +private meta def abbrevFirstLine (width : Nat) (str : String) : String := let str := str.trimAsciiStart let short := str.take width |>.replace "\n" "⏎" if short.toSlice == str then short else short ++ "…" -def LeanBlockConfig.outlineMeta : LeanBlockConfig → String +meta def LeanBlockConfig.outlineMeta : LeanBlockConfig → String | {«show», error, ..} => match «show», error with | true, true => " (error)" @@ -126,7 +136,7 @@ def LeanBlockConfig.outlineMeta : LeanBlockConfig → String | false, false => " (hidden)" | _, _ => " " -def firstToken? (stx : Syntax) : Option Syntax := +meta def firstToken? (stx : Syntax) : Option Syntax := stx.find? fun | .ident info .. => usable info | .atom info .. => usable info @@ -147,7 +157,7 @@ is `some false`, then the author expected no errors; in this case, messages are `none` case and an additional error is thrown. If it is `some true`, then errors are downgraded to warnings and all messages are logged silently. -/ -def reportMessages {m} [Monad m] [MonadLog m] [MonadError m] +public meta def reportMessages {m} [Monad m] [MonadLog m] [MonadError m] (errorExpected : Option Bool) (blame : Syntax) (messages : MessageLog) : m Unit := do match errorExpected with @@ -168,7 +178,7 @@ def reportMessages {m} [Monad m] [MonadLog m] [MonadError m] if messages.hasErrors then throwErrorAt blame "No error expected in code block, one occurred" -def reconstructHighlight (docReconst : DocReconstruction) (key : Export.Key) := +public def reconstructHighlight (docReconst : DocReconstruction) (key : Export.Key) := match docReconst.highlightDeduplication.toHighlighted key with | .error msg => panic! s!"Unable to export key {key}: {msg}" | .ok v => v @@ -179,7 +189,7 @@ within the DocElabM monad, `← quoteHighlightViaSerialization hls` will result represents the same highlight as `quote hls`, but will hopefully produce smaller code because of quoting a compressed version of the highlighted code. -/ -private def quoteHighlightViaSerialization (hls : Highlighted) : DocElabM Term := do +private meta def quoteHighlightViaSerialization (hls : Highlighted) : DocElabM Term := do match (( ← readThe DocElabContext).docReconstructionPlaceholder, (← getThe DocElabM.State).highlightDeduplicationTable) with | (.some placeholder, .some exportTable) => let (key, exportTable) := hls.export.run exportTable @@ -193,7 +203,7 @@ private def quoteHighlightViaSerialization (hls : Highlighted) : DocElabM Term : De-indents and returns (syntax of) a Block representation containing highlighted Lean code. The argument `hls` must be a highlighting of the parsed string `str`. -/ -private def toHighlightedLeanBlock (shouldShow : Bool) (hls : Highlighted) (str: StrLit) : DocElabM Term := do +private meta def toHighlightedLeanBlock (shouldShow : Bool) (hls : Highlighted) (str: StrLit) : DocElabM Term := do if !shouldShow then return ← ``(Block.concat #[]) @@ -212,7 +222,7 @@ private def toHighlightedLeanBlock (shouldShow : Bool) (hls : Highlighted) (str: Returns (syntax of) an Inline representation containing highlighted Lean code. The argument `hls` must be a highlighting of the parsed string `str`. -/ -private def toHighlightedLeanInline (shouldShow : Bool) (hls : Highlighted) (str : StrLit) : DocElabM Term := do +private meta def toHighlightedLeanInline (shouldShow : Bool) (hls : Highlighted) (str : StrLit) : DocElabM Term := do if !shouldShow then return ← ``(Inline.concat #[]) @@ -229,7 +239,7 @@ needs to run, so that its warnings are accurately recorded. But the linter also document, at which time it can inspect the info trees left behind by the embedded Lean and generate spurious warnings. Turning it off before saving info trees works around this issue. -/ -private partial def disableUnusedVarLinterInInfoTree : InfoTree → InfoTree +private meta partial def disableUnusedVarLinterInInfoTree : InfoTree → InfoTree | .context (.commandCtx ci) child => .context (.commandCtx { ci with options := Lean.Linter.linter.unusedVariables.set ci.options false }) (disableUnusedVarLinterInInfoTree child) @@ -239,7 +249,7 @@ private partial def disableUnusedVarLinterInInfoTree : InfoTree → InfoTree .node info (children.map disableUnusedVarLinterInInfoTree) | .hole id => .hole id -def elabCommands (config : LeanBlockConfig) (str : StrLit) +public meta def elabCommands (config : LeanBlockConfig) (str : StrLit) (toHighlightedLeanContent : (shouldShow : Bool) → (hls : Highlighted) → (str: StrLit) → DocElabM Term) (minCommands : Option Nat := none) (maxCommands : Option Nat := none) : @@ -359,11 +369,11 @@ where Elaborates the provided Lean command in the context of the current Verso module. -/ @[code_block] -def lean : CodeBlockExpanderOf LeanBlockConfig +public meta def lean : CodeBlockExpanderOf LeanBlockConfig | config, str => elabCommands config str toHighlightedLeanBlock @[role] -def leanCommand : RoleExpanderOf LeanBlockConfig +public meta def leanCommand : RoleExpanderOf LeanBlockConfig | config, inls => do if let some str ← oneCodeStr? inls then elabCommands config str toHighlightedLeanInline (minCommands := some 1) (maxCommands := some 1) @@ -375,7 +385,7 @@ def leanCommand : RoleExpanderOf LeanBlockConfig Elaborates the provided Lean term in the context of the current Verso module. -/ @[code_block] -def leanTerm : CodeBlockExpanderOf LeanInlineConfig +public meta def leanTerm : CodeBlockExpanderOf LeanInlineConfig | config, str => withoutAsync <| do let altStr ← parserInputString str @@ -454,7 +464,7 @@ def leanTerm : CodeBlockExpanderOf LeanInlineConfig Elaborates the provided Lean term in the context of the current Verso module. -/ @[role lean] -def leanInline : RoleExpanderOf LeanInlineConfig +public meta def leanInline : RoleExpanderOf LeanInlineConfig -- Async elab is turned off to make sure that info trees and messages are available when highlighting | config, inlines => withoutAsync do let #[arg] := inlines @@ -551,7 +561,7 @@ def leanInline : RoleExpanderOf LeanInlineConfig Elaborates the provided term in the current Verso context, then ensures that it's a type class that has an instance. -/ @[role] -def inst : RoleExpanderOf LeanBlockConfig +public meta def inst : RoleExpanderOf LeanBlockConfig | config, inlines => withoutAsync <| do let #[arg] := inlines | throwError "Expected exactly one argument" @@ -609,7 +619,7 @@ def inst : RoleExpanderOf LeanBlockConfig Elaborates the contained document in a new section. -/ @[directive_expander leanSection] -def leanSection : DirectiveExpander +public meta def leanSection : DirectiveExpander | args, contents => do let name? ← ArgParse.run ((some <$> .positional `name .string) <|> pure none) args let arg ← `(doc_arg| -«show») @@ -624,7 +634,7 @@ private def getClass : MessageSeverity → String | .information => "information" | .warning => "warning" -block_extension Block.leanOutput via withHighlighting where +public block_extension Block.leanOutput via withHighlighting where traverse _ _ _ := do pure none toTeX := @@ -647,7 +657,7 @@ block_extension Block.leanOutput via withHighlighting where msg.blockHtml summarize (expandTraces := expandTraces) (g := Manual) -structure LeanOutputConfig where +public structure LeanOutputConfig where name : Ident «show» : Bool := true severity : Option MessageSeverity @@ -662,18 +672,19 @@ structure LeanOutputConfig where section variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] -def LeanOutputConfig.parser : ArgParse m LeanOutputConfig := - LeanOutputConfig.mk <$> - .positional `name output <*> - .flag `show true <*> - .named `severity .messageSeverity true <*> - .flag `summarize false <*> - .namedD `whitespace .whitespaceMode .exact <*> - .flag `normalizeMetas true <*> - .namedD `allowDiff .nat 0 <*> - .many (.named `expandTrace .name false) <*> - .named `startAt .string true <*> - .named `stopAt .string true +public meta instance : FromArgs LeanOutputConfig m where + fromArgs := + LeanOutputConfig.mk <$> + .positional `name output <*> + .flag `show true <*> + .named `severity .messageSeverity true <*> + .flag `summarize false <*> + .namedD `whitespace .whitespaceMode .exact <*> + .flag `normalizeMetas true <*> + .namedD `allowDiff .nat 0 <*> + .many (.named `expandTrace .name false) <*> + .named `startAt .string true <*> + .named `stopAt .string true where output : ValDesc m Ident := { description := "output name", @@ -682,17 +693,14 @@ where | .name x => pure x | other => throwError "Expected output name, got {repr other}" } - -instance : FromArgs LeanOutputConfig m := ⟨LeanOutputConfig.parser⟩ - end -private def withNl (s : String) : String := +private meta def withNl (s : String) : String := if s.endsWith "\n" then s else s ++ "\n" open SubVerso.Examples.Messages in @[code_block] -def leanOutput : CodeBlockExpanderOf LeanOutputConfig +public meta def leanOutput : CodeBlockExpanderOf LeanOutputConfig | config, str => do PointOfInterest.save (← getRef) (config.name.getId.toString) @@ -797,7 +805,7 @@ where (insDel.size, Diff.linesToString d) -inline_extension Inline.name via withHighlighting where +public inline_extension Inline.name via withHighlighting where traverse _ _ _ := do pure none toTeX := some <| fun go _ _ content => content.mapM go @@ -811,14 +819,14 @@ inline_extension Inline.name via withHighlighting where | .ok (hl : Highlighted) => hl.inlineHtml (g := Manual) "examples" -structure NameConfig where +public structure NameConfig where full : Option Name section variable [Monad m] [MonadError m] [MonadLiftT CoreM m] [MonadLiftT TermElabM m] -def NameConfig.parse : ArgParse m NameConfig := - NameConfig.mk <$> ((fun _ => none) <$> .done <|> .positional `name ref) +public meta instance : FromArgs NameConfig m where + fromArgs := NameConfig.mk <$> ((fun _ => none) <$> .done <|> .positional `name ref) where ref : ValDesc m (Option Name) := { description := "reference name" @@ -833,11 +841,9 @@ where | _ => return none | other => throwError "Expected reference name, got {repr other}" } - -instance : FromArgs NameConfig m := ⟨NameConfig.parse⟩ end -def constTok [Monad m] [MonadEnv m] [MonadLiftT MetaM m] [MonadLiftT IO m] +public meta def constTok [Monad m] [MonadEnv m] [MonadLiftT MetaM m] [MonadLiftT IO m] (name : Name) (str : String) : m Highlighted := do let docs ← findDocString? (← getEnv) name @@ -845,7 +851,7 @@ def constTok [Monad m] [MonadEnv m] [MonadLiftT MetaM m] [MonadLiftT IO m] pure <| .token ⟨.const name sig docs false none, str⟩ @[role] -def name : RoleExpanderOf NameConfig +public meta def name : RoleExpanderOf NameConfig | cfg, #[arg] => do let `(inline|code( $name:str )) := arg | throwErrorAt arg "Expected code literal with the example name" @@ -873,7 +879,7 @@ def name : RoleExpanderOf NameConfig -- Placeholder for module names (eventually hyperlinking these will be important, so better to tag them now) @[role] -def module : RoleExpanderOf Unit +public meta def module : RoleExpanderOf Unit | (), #[arg] => do let `(inline|code( $name:str )) := arg | throwErrorAt arg "Expected code literal with the module's name" diff --git a/src/verso-manual/VersoManual/InlineLean/Block.lean b/src/verso-manual/VersoManual/InlineLean/Block.lean index 379aacfff..14970768b 100644 --- a/src/verso-manual/VersoManual/InlineLean/Block.lean +++ b/src/verso-manual/VersoManual/InlineLean/Block.lean @@ -3,15 +3,17 @@ Copyright (c) 2024-2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ - +module import Lean.Data.Json.Basic -import VersoManual.Basic +public import VersoManual.Basic import VersoManual.HighlightedCode import Verso.Code.Highlighted.WebAssets import Verso.Code.HighlightedToTex import SubVerso.Highlighting +public section + open Verso Genre Manual open Verso Code Highlighted WebAssets open Verso Doc Output Html @@ -20,7 +22,7 @@ open SubVerso.Highlighting namespace Verso.Genre.Manual.InlineLean -block_extension Block.lean +public block_extension Block.lean (hls : Highlighted) (file : Option System.FilePath := none) (range : Option Lsp.Range := none) via withHighlighting where init s := s.addQuickJumpMapper exampleDomain exampleDomainMapper diff --git a/src/verso-manual/VersoManual/InlineLean/IO.lean b/src/verso-manual/VersoManual/InlineLean/IO.lean index 67e4129d1..50d7fa815 100644 --- a/src/verso-manual/VersoManual/InlineLean/IO.lean +++ b/src/verso-manual/VersoManual/InlineLean/IO.lean @@ -3,22 +3,30 @@ Copyright (c) 2024-2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ - +module import Lean.Elab.Command import Lean.Elab.InfoTree import Verso import Verso.FS import Verso.Doc.ArgParse -import Verso.Doc.Elab.Monad +public import Verso.Doc.Elab.Monad +public meta import Verso.Doc.Elab.Block +public meta import Verso.Doc.Suggestion.Basic import Verso.Code import Verso.Instances import SubVerso.Highlighting import SubVerso.Examples +public meta import SubVerso.Module +public import VersoManual.Basic +import VersoManual.HighlightedCode import VersoManual.InlineLean.Scopes -import VersoManual.InlineLean.IO.Context +public import VersoManual.InlineLean.IO.Context +meta import VersoManual.InlineLean.IO.Context +import VersoManual.InlineLean.IO.Data +public meta import VersoManual.InlineLean.IO.Data import VersoManual.InlineLean.Block @@ -34,29 +42,23 @@ open Verso.Genre.Manual.InlineLean.IOExample namespace Verso.Genre.Manual.InlineLean -inductive FileType where - | stdin | stdout | stderr - | input (file : System.FilePath) - | output (file : System.FilePath) - | other (file : System.FilePath) -deriving ToJson, FromJson, Repr, BEq, DecidableEq, Quote -def Block.exampleFile (type : FileType) : Block where +public def Block.exampleFile (type : FileType) : Block where data := ToJson.toJson type -structure ExampleFileConfig where +public structure ExampleFileConfig where type : FileType «show» : Bool := true -def FileType.parse [Monad m] [MonadError m] : ArgParse m FileType := - (.positional `type (literally `stdin) *> pure .stdin) <|> - (.positional `type (literally `stdout) *> pure .stdout) <|> - (.positional `type (literally `stderr) *> pure .stderr) <|> - (.positional `type (literally `stderr) *> pure .stderr) <|> - (FileType.input <$> (.positional `type (literally `input) *> .positional `filename path)) <|> - (FileType.output <$> (.positional `type (literally `output) *> .positional `filename path)) <|> - (FileType.other <$> (.positional `type (literally `other) *> .positional `filename path)) +public meta def FileType.parse [Monad m] [MonadError m] : ArgParse m FileType := + (.positional `type (literally `stdin) *> pure .stdin) <|> + (.positional `type (literally `stdout) *> pure .stdout) <|> + (.positional `type (literally `stderr) *> pure .stderr) <|> + (.positional `type (literally `stderr) *> pure .stderr) <|> + (FileType.input <$> (.positional `type (literally `input) *> .positional `filename path)) <|> + (FileType.output <$> (.positional `type (literally `output) *> .positional `filename path)) <|> + (FileType.other <$> (.positional `type (literally `other) *> .positional `filename path)) where path : ValDesc m System.FilePath := Coe.coe <$> ValDesc.string @@ -72,18 +74,17 @@ section variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] -def ExampleFileConfig.parse : ArgParse m ExampleFileConfig := - ExampleFileConfig.mk <$> FileType.parse <*> (.flag `show true) -def IOExample.exampleFileSyntax [Monad m] [MonadQuotation m] (type : FileType) (contents : String) : m Term := do +meta def IOExample.exampleFileSyntax [Monad m] [MonadQuotation m] (type : FileType) (contents : String) : m Term := do ``(Block.other (Block.exampleFile $(quote type)) #[Block.code $(quote contents)]) -instance : FromArgs ExampleFileConfig m := ⟨ExampleFileConfig.parse⟩ +public meta instance : FromArgs ExampleFileConfig m where + fromArgs := ExampleFileConfig.mk <$> FileType.parse <*> (.flag `show true) end @[code_block] -def exampleFile : CodeBlockExpanderOf ExampleFileConfig +public meta def exampleFile : CodeBlockExpanderOf ExampleFileConfig | config, str => do let s := str.getString if config.show then @@ -178,7 +179,7 @@ where if lines.back? == some "" then lines.pop else lines end -block_extension Block.exampleLeanFile (filename : String) where +public block_extension Block.exampleLeanFile (filename : String) where data := .str filename traverse _ _ _ := pure none toTeX := @@ -280,7 +281,7 @@ private def getSubversoDir : IO System.FilePath := do throw <| IO.userError s!"SubVerso directory {p} not found" -def startExample [Monad m] [MonadEnv m] [MonadError m] [MonadQuotation m] [MonadRef m] : m Unit := do +meta def startExample [Monad m] [MonadEnv m] [MonadError m] [MonadQuotation m] [MonadRef m] : m Unit := do match ioExampleCtx.getState (← getEnv) with | some _ => throwError "Can't initialize - already in a context" | none => @@ -288,7 +289,7 @@ def startExample [Monad m] [MonadEnv m] [MonadError m] [MonadQuotation m] [Monad modifyEnv fun env => ioExampleCtx.setState env (some {leanCodeName}) -def saveLeanCode (src : StrLit) : DocElabM Ident := do +meta def saveLeanCode (src : StrLit) : DocElabM Ident := do match ioExampleCtx.getState (← getEnv) with | none => throwError "Can't set Lean code - not in an IO example" | some st => @@ -298,20 +299,19 @@ def saveLeanCode (src : StrLit) : DocElabM Ident := do return st.leanCodeName else throwError "Code already specified" - -def saveInputFile [Monad m] [MonadEnv m] [MonadError m] (name : System.FilePath) (contents : StrLit) : m Unit := do +meta def saveInputFile [Monad m] [MonadEnv m] [MonadError m] (name : System.FilePath) (contents : StrLit) : m Unit := do match ioExampleCtx.getState (← getEnv) with | none => throwError "Can't save file - not in an IO example" | some st => modifyEnv fun env => ioExampleCtx.setState env (some {st with inputFiles := st.inputFiles.push (name, contents)}) -def saveOutputFile [Monad m] [MonadEnv m] [MonadError m] (name : System.FilePath) (contents : StrLit) : m Unit := do +meta def saveOutputFile [Monad m] [MonadEnv m] [MonadError m] (name : System.FilePath) (contents : StrLit) : m Unit := do match ioExampleCtx.getState (← getEnv) with | none => throwError "Can't save file - not in an IO example" | some st => modifyEnv fun env => ioExampleCtx.setState env (some {st with outputFiles := st.outputFiles.push (name, contents)}) -def saveStdin [Monad m] [MonadEnv m] [MonadError m] (contents : StrLit) : m Unit := do +meta def saveStdin [Monad m] [MonadEnv m] [MonadError m] (contents : StrLit) : m Unit := do match ioExampleCtx.getState (← getEnv) with | none => throwError "Can't save stdin - not in an IO example" | some st => @@ -319,7 +319,7 @@ def saveStdin [Monad m] [MonadEnv m] [MonadError m] (contents : StrLit) : m Unit | none => modifyEnv fun env => ioExampleCtx.setState env (some {st with stdin := some contents}) | some _ => throwError "stdin already specified" -def saveStdout [Monad m] [MonadEnv m] [MonadError m] (contents : StrLit) : m Unit := do +meta def saveStdout [Monad m] [MonadEnv m] [MonadError m] (contents : StrLit) : m Unit := do match ioExampleCtx.getState (← getEnv) with | none => throwError "Can't save stdout - not in an IO example" | some st => @@ -327,7 +327,7 @@ def saveStdout [Monad m] [MonadEnv m] [MonadError m] (contents : StrLit) : m Uni | none => modifyEnv fun env => ioExampleCtx.setState env (some {st with stdout := some contents}) | some _ => throwError "stdout already specified" -def saveStderr [Monad m] [MonadEnv m] [MonadError m] (contents : StrLit) : m Unit := do +meta def saveStderr [Monad m] [MonadEnv m] [MonadError m] (contents : StrLit) : m Unit := do match ioExampleCtx.getState (← getEnv) with | none => throwError "Can't save stderr - not in an IO example" | some st => @@ -336,7 +336,7 @@ def saveStderr [Monad m] [MonadEnv m] [MonadError m] (contents : StrLit) : m Uni | some _ => throwError "stderr already specified" -def check +meta def check (leanCode : StrLit) (leanCodeName : Name) (inputFiles outputFiles : Array (System.FilePath × StrLit)) (stdin stdout stderr : Option StrLit) : DocElabM Highlighted := @@ -437,7 +437,7 @@ where shorten (str : String) : String := if str.length < 30 then str else (str.take 30).copy ++ "…" -def endExample (body : TSyntax `term) : DocElabM (TSyntax `term) := do +meta def endExample (body : TSyntax `term) : DocElabM (TSyntax `term) := do match ioExampleCtx.getState (← getEnv) with | none => throwErrorAt body "Can't end example - never started" | some {code, leanCodeName, inputFiles, outputFiles, stdin, stdout, stderr} => do @@ -455,22 +455,18 @@ def endExample (body : TSyntax `term) : DocElabM (TSyntax `term) := do section variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] -structure Config where +public structure Config where tag : Option String := none «show» : Bool := true -def Config.parse : ArgParse m Config := - Config.mk <$> .named `tag .string true <*> (.flag `show true) - -instance : FromArgs Config m := ⟨Config.parse⟩ +public meta instance : FromArgs Config m where + fromArgs := Config.mk <$> .named `tag .string true <*> (.flag `show true) -structure FileConfig extends Config where +public structure FileConfig extends Config where name : String -def FileConfig.parse : ArgParse m FileConfig := - FileConfig.mk <$> Config.parse <*> .positional `name .string - -instance : FromArgs FileConfig m := ⟨FileConfig.parse⟩ +public meta instance : FromArgs FileConfig m where + fromArgs := FileConfig.mk <$> fromArgs <*> .positional `name .string end @@ -478,7 +474,7 @@ end IOExample open IOExample in @[code_block] -def inputFile : CodeBlockExpanderOf FileConfig +public meta def inputFile : CodeBlockExpanderOf FileConfig | opts, str => do saveInputFile opts.name str -- The quote step here is to prevent the editor from showing document AST internals when the @@ -490,7 +486,7 @@ def inputFile : CodeBlockExpanderOf FileConfig open IOExample in @[code_block] -def outputFile : CodeBlockExpanderOf FileConfig +public meta def outputFile : CodeBlockExpanderOf FileConfig | opts, str => do saveOutputFile opts.name str -- The quote step here is to prevent the editor from showing document AST internals when the @@ -502,7 +498,7 @@ def outputFile : CodeBlockExpanderOf FileConfig open IOExample in @[code_block] -def stdin : CodeBlockExpanderOf Config +public meta def stdin : CodeBlockExpanderOf Config | opts, str => do saveStdin str -- The quote step here is to prevent the editor from showing document AST internals when the @@ -514,7 +510,7 @@ def stdin : CodeBlockExpanderOf Config open IOExample in @[code_block] -def stdout : CodeBlockExpanderOf Config +public meta def stdout : CodeBlockExpanderOf Config | opts, str => do saveStdout str -- The quote step here is to prevent the editor from showing document AST internals when the @@ -526,7 +522,7 @@ def stdout : CodeBlockExpanderOf Config open IOExample in @[code_block] -def stderr : CodeBlockExpanderOf Config +public meta def stderr : CodeBlockExpanderOf Config | opts, str => do saveStderr str -- The quote step here is to prevent the editor from showing document AST internals when the @@ -536,10 +532,9 @@ def stderr : CodeBlockExpanderOf Config else ``(Block.concat #[]) - open IOExample in @[code_block] -def ioLean : CodeBlockExpanderOf Config +public meta def ioLean : CodeBlockExpanderOf Config | opts, str => do let x ← saveLeanCode str if opts.show then @@ -551,7 +546,7 @@ def ioLean : CodeBlockExpanderOf Config open IOExample in @[directive ioExample] -def ioExample : DirectiveExpanderOf Unit +public meta def ioExample : DirectiveExpanderOf Unit | (), blocks => do startExample let body ← blocks.mapM elabBlock diff --git a/src/verso-manual/VersoManual/InlineLean/IO/Context.lean b/src/verso-manual/VersoManual/InlineLean/IO/Context.lean index 73052ed35..7f303a2eb 100644 --- a/src/verso-manual/VersoManual/InlineLean/IO/Context.lean +++ b/src/verso-manual/VersoManual/InlineLean/IO/Context.lean @@ -3,14 +3,14 @@ Copyright (c) 2024-2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ - -import Lean.Environment +module +public import Lean.Environment namespace Verso.Genre.Manual.InlineLean.IOExample open Lean -structure IOExampleContext where +public structure IOExampleContext where leanCodeName : Ident code : Option StrLit := none inputFiles : Array (System.FilePath × StrLit) := #[] @@ -20,5 +20,5 @@ structure IOExampleContext where stderr : Option StrLit := none deriving Repr -initialize ioExampleCtx : EnvExtension (Option IOExampleContext) ← +public initialize ioExampleCtx : EnvExtension (Option IOExampleContext) ← Lean.registerEnvExtension (pure none) diff --git a/src/verso-manual/VersoManual/InlineLean/IO/Data.lean b/src/verso-manual/VersoManual/InlineLean/IO/Data.lean new file mode 100644 index 000000000..63090c790 --- /dev/null +++ b/src/verso-manual/VersoManual/InlineLean/IO/Data.lean @@ -0,0 +1,20 @@ +/- +Copyright (c) 2025-2026 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ +module +public import Lean.Data.Json.FromToJson.Basic +public import Verso.Instances +meta import Verso.Instances.Deriving + +open Lean + +namespace Verso.Genre.Manual.InlineLean + +public inductive FileType where + | stdin | stdout | stderr + | input (file : System.FilePath) + | output (file : System.FilePath) + | other (file : System.FilePath) +deriving ToJson, FromJson, Repr, BEq, DecidableEq, Quote diff --git a/src/verso-manual/VersoManual/InlineLean/LongLines.lean b/src/verso-manual/VersoManual/InlineLean/LongLines.lean index 618297555..e312839f5 100644 --- a/src/verso-manual/VersoManual/InlineLean/LongLines.lean +++ b/src/verso-manual/VersoManual/InlineLean/LongLines.lean @@ -3,14 +3,15 @@ Copyright (c) 2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ -import Lean.Data.Lsp.Utf16 -import Lean.Data.Options -import Lean.Data.Position -import Lean.Log +module +public import Lean.Data.Lsp.Utf16 +public import Lean.Data.Options +public import Lean.Data.Position +public import Lean.Log open Lean MonadOptions -register_option verso.code.warnLineLength : Nat := { +public register_option verso.code.warnLineLength : Nat := { defValue := 60 descr := "The example code line length at which to issue warnings. Set to 0 for no warnings." } @@ -21,7 +22,7 @@ def getWarnLineLength [Monad m] [MonadOptions m] : m (Option Nat) := do let val := (← getOptions).get verso.code.warnLineLength.name verso.code.warnLineLength.defValue if val = 0 then return none else return some val -def warnLongLines [Monad m] [MonadFileMap m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (indent? : Option Nat) (str : StrLit) : m Unit := do +public def warnLongLines [Monad m] [MonadFileMap m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (indent? : Option Nat) (str : StrLit) : m Unit := do let some maxCodeColumns ← getWarnLineLength | pure () let fileMap ← getFileMap diff --git a/src/verso-manual/VersoManual/InlineLean/Option.lean b/src/verso-manual/VersoManual/InlineLean/Option.lean index a88de81d3..638d623ad 100644 --- a/src/verso-manual/VersoManual/InlineLean/Option.lean +++ b/src/verso-manual/VersoManual/InlineLean/Option.lean @@ -3,9 +3,12 @@ Copyright (c) 2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ +module import Verso -import VersoManual.Basic +public meta import Verso.WithoutAsync +public import VersoManual.Basic import VersoManual.HighlightedCode +public import Verso.Doc.Elab.Monad open SubVerso.Highlighting @@ -20,7 +23,7 @@ namespace Verso.Genre.Manual.InlineLean def Inline.option : Inline where @[role] -def option : RoleExpanderOf Unit +public meta def option : RoleExpanderOf Unit | (), inlines => withoutAsync do let #[arg] := inlines | throwError "Expected exactly one argument" diff --git a/src/verso-manual/VersoManual/InlineLean/Outputs.lean b/src/verso-manual/VersoManual/InlineLean/Outputs.lean index 92aa157d0..db00a7599 100644 --- a/src/verso-manual/VersoManual/InlineLean/Outputs.lean +++ b/src/verso-manual/VersoManual/InlineLean/Outputs.lean @@ -3,10 +3,13 @@ Copyright (c) 2024-2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ -import Lean.Environment -import Lean.Message -import Lean.Exception -import Verso +module +import Lean.Data.EditDistance +public import Lean.Environment +public import Lean.Message +public import Lean.Exception +public import SubVerso.Highlighting.Highlighted +public import Verso.Doc.Suggestion.Basic open Lean open SubVerso.Highlighting @@ -19,11 +22,11 @@ initialize leanOutputs : EnvExtension (NameMap (List Highlighted.Message)) ← variable [Monad m] [MonadEnv m] [Elab.MonadInfoTree m] [MonadError m] /-- -Save the output of a Lean block. +Saves the output of a Lean block. `name` is the name the author assigned to the block. -/ -def saveOutputs (name : Name) (msgs : List Highlighted.Message) : m Unit := +public def saveOutputs (name : Name) (msgs : List Highlighted.Message) : m Unit := modifyEnv (leanOutputs.modifyState · (·.insert name msgs)) def getOrSuggest (key : Ident) (map : NameMap α) : m α := do @@ -46,5 +49,5 @@ where else if l < 10 then 2 else 3 -def getOutputs (name : Ident) : m (List Highlighted.Message):= do +public def getOutputs (name : Ident) : m (List Highlighted.Message):= do leanOutputs.getState (← getEnv) |> getOrSuggest name diff --git a/src/verso-manual/VersoManual/InlineLean/Scopes.lean b/src/verso-manual/VersoManual/InlineLean/Scopes.lean index ec60a9994..ca3fc2e41 100644 --- a/src/verso-manual/VersoManual/InlineLean/Scopes.lean +++ b/src/verso-manual/VersoManual/InlineLean/Scopes.lean @@ -3,9 +3,11 @@ Copyright (c) 2024-2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ - +module import Lean.Elab.Command -import Lean.Environment +public import Lean.Environment +public import Lean.Elab.Command.Scope +public import Lean.Elab.Term.TermElabM open Lean Elab Command @@ -25,18 +27,18 @@ def initScopes [Monad m] [MonadEnv m] [MonadOptions m] [MonadResolveName m] : m } modifyEnv (leanSampleScopes.setState · [basicSc]) -def getScopes [Monad m] [MonadEnv m] [MonadOptions m] [MonadResolveName m] : m (List Scope) := do +public def getScopes [Monad m] [MonadEnv m] [MonadOptions m] [MonadResolveName m] : m (List Scope) := do initScopes return leanSampleScopes.getState (← getEnv) -def setScopes [Monad m] [MonadEnv m] (scopes : List Scope) : m Unit := do +public def setScopes [Monad m] [MonadEnv m] (scopes : List Scope) : m Unit := do modifyEnv (leanSampleScopes.setState · scopes) /-- Runs an elaborator action with the current namespace and open declarations that have been found via inline Lean blocks. -/ -def runWithOpenDecls (act : TermElabM α) : TermElabM α := do +public def runWithOpenDecls (act : TermElabM α) : TermElabM α := do let scope := (← getScopes).head! withTheReader Core.Context ({· with currNamespace := scope.currNamespace, openDecls := scope.openDecls}) do let initNames := (← getThe Term.State).levelNames @@ -51,7 +53,7 @@ Runs an elaborator action with the section variables that have been established This is a version of `Lean.Elab.Command.runTermElabM`. -/ -def runWithVariables (elabFn : Array Expr → TermElabM α) : TermElabM α := do +public def runWithVariables (elabFn : Array Expr → TermElabM α) : TermElabM α := do let scope := (← getScopes).head! Term.withAutoBoundImplicit do let msgLog ← Core.getMessageLog diff --git a/src/verso-manual/VersoManual/InlineLean/Signature.lean b/src/verso-manual/VersoManual/InlineLean/Signature.lean index 243c882f4..031b6506e 100644 --- a/src/verso-manual/VersoManual/InlineLean/Signature.lean +++ b/src/verso-manual/VersoManual/InlineLean/Signature.lean @@ -3,12 +3,18 @@ Copyright (c) 2024-2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ +module import Lean.Elab.InfoTree.Types import Verso -import VersoManual.Basic +public meta import Verso.WithoutAsync +public meta import Verso.Code.Highlighted +public import VersoManual.Basic import VersoManual.HighlightedCode -import SubVerso.Examples +public import SubVerso.Examples +public import Verso.Doc.Elab.Monad +public meta import Verso.Doc.PointOfInterest +public meta import Verso.Doc.Suggestion.Basic open SubVerso.Highlighting @@ -20,7 +26,7 @@ open Lean Elab namespace Verso.Genre.Manual.InlineLean -block_extension Block.signature via withHighlighting where +public block_extension Block.signature via withHighlighting where traverse _ _ _ := do pure none toTeX := @@ -41,23 +47,19 @@ block_extension Block.signature via withHighlighting where declare_syntax_cat signature_spec syntax ("def" <|> "theorem")? declId declSig : signature_spec -structure SignatureConfig where +public structure SignatureConfig where «show» : Bool := true section variable [Monad m] [MonadError m] [MonadLiftT CoreM m] -def SignatureConfig.parse : ArgParse m SignatureConfig := - SignatureConfig.mk <$> - (.flag `show true) - -instance : FromArgs SignatureConfig m where - fromArgs := SignatureConfig.parse +public meta instance : FromArgs SignatureConfig m where + fromArgs := SignatureConfig.mk <$> .flag `show true end @[code_block] -def signature : CodeBlockExpanderOf SignatureConfig +public meta def signature : CodeBlockExpanderOf SignatureConfig | {«show»}, str => withoutAsync do let altStr ← parserInputString str let col? := (← getRef).getPos? |>.map (← getFileMap).utf8PosToLspPos |>.map (·.character) diff --git a/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean b/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean index 7fffb414b..f0f8c9915 100644 --- a/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean +++ b/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean @@ -3,13 +3,17 @@ Copyright (c) 2024-2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ +module import Lean.Elab.InfoTree.Types import Verso -import VersoManual.Basic +public meta import Verso.WithoutAsync +public import VersoManual.Basic import VersoManual.HighlightedCode -import VersoManual.InlineLean.Outputs +public meta import VersoManual.InlineLean.Outputs import SubVerso.Examples +public import Verso.Doc.Elab.Monad +public meta import Verso.Doc.PointOfInterest open SubVerso.Highlighting @@ -22,7 +26,7 @@ open Lean Elab namespace Verso.Genre.Manual.InlineLean -block_extension Block.syntaxError via withHighlighting where +public block_extension Block.syntaxError via withHighlighting where traverse _ _ _ := pure none toTeX := some <| fun _ go _ _ content => do @@ -110,7 +114,7 @@ block_extension Block.syntaxError via withHighlighting where pure {{
{{out}}
}} -structure SyntaxErrorConfig where +public structure SyntaxErrorConfig where name : Name «show» : Bool := true category : Name := `command @@ -119,20 +123,19 @@ structure SyntaxErrorConfig where section variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] -def SyntaxErrorConfig.parse : ArgParse m SyntaxErrorConfig := - SyntaxErrorConfig.mk <$> - .positional `name (ValDesc.name.as "name for later reference") <*> - .flag `show true <*> - .namedD `category (ValDesc.name.as "syntax category (default `command`)") `command <*> - .namedD `precedence .nat 0 - -instance : FromArgs SyntaxErrorConfig m := ⟨SyntaxErrorConfig.parse⟩ +public meta instance : FromArgs SyntaxErrorConfig m where + fromArgs := + SyntaxErrorConfig.mk <$> + .positional `name (ValDesc.name.as "name for later reference") <*> + .flag `show true <*> + .namedD `category (ValDesc.name.as "syntax category (default `command`)") `command <*> + .namedD `precedence .nat 0 end open Lean.Parser in @[code_block] -def syntaxError : CodeBlockExpanderOf SyntaxErrorConfig +public meta def syntaxError : CodeBlockExpanderOf SyntaxErrorConfig | config, str => withoutAsync do PointOfInterest.save (← getRef) config.name.toString diff --git a/src/verso-manual/VersoManual/License.lean b/src/verso-manual/VersoManual/License.lean index 41460ad56..77917c6f1 100644 --- a/src/verso-manual/VersoManual/License.lean +++ b/src/verso-manual/VersoManual/License.lean @@ -63,7 +63,7 @@ where public section -block_extension Block.licenseInfo where +public block_extension Block.licenseInfo where traverse _ _ _ := do pure none /- The TeX output is intentionally empty. As we are not distributing code in the PDF, we don't believe diff --git a/src/verso-manual/VersoManual/Linters.lean b/src/verso-manual/VersoManual/Linters.lean index 713a563b1..893f295fb 100644 --- a/src/verso-manual/VersoManual/Linters.lean +++ b/src/verso-manual/VersoManual/Linters.lean @@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ +module +public import Lean.Data.Options import Lean.Linter.Basic import Lean.Meta.Hint import Verso.Doc.Concrete diff --git a/src/verso-manual/VersoManual/Literate.lean b/src/verso-manual/VersoManual/Literate.lean index 412eb429f..f81eba844 100644 --- a/src/verso-manual/VersoManual/Literate.lean +++ b/src/verso-manual/VersoManual/Literate.lean @@ -3,11 +3,21 @@ Copyright (c) 2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ -import VersoManual.Basic -import VersoManual.ExternalLean +module +public import Verso.Code.External +import Verso.Doc.Concrete +public import VersoManual.Basic +public import VersoManual.ExternalLean import VersoLiterate +public import VersoLiterate.Basic +public import VersoLiterate.Module +public meta import Verso.Parser import Lean.Data.Json -import Lean.Compiler.LCNF.ConfigOptions +public meta import Lean.Compiler.LCNF.ConfigOptions +public meta import Verso.Doc.Elab.Inline +public import Verso.Doc.Elab + +public section namespace Verso.Genre.Manual @@ -17,14 +27,14 @@ open Verso.Output Html open Verso.Doc.Html open Lean -block_extension Block.literateDocstring where +public block_extension Block.literateDocstring where traverse _ _ _ _ := pure none toHtml := some fun _goI goB _id _data contents => do pure {{
{{← contents.mapM goB}}
}} toTeX := some fun _goI goB _id _data contents => do contents.mapM goB -block_extension Block.literateDocstringPart (level : Nat) where +public block_extension Block.literateDocstringPart (level : Nat) where data := level traverse _ _ _ _ := pure none toHtml := some fun goI goB _id data contents => do @@ -67,7 +77,7 @@ block_extension Block.literateDocstringPart (level : Nat) where let sectionHeader ← Doc.TeX.headerLevel title level none pure <| (sectionHeader ++ (← contents.mapM goB)) -instance : LoadLiterate Manual where +public instance : LoadLiterate Manual where inline goI | .highlighted hl, _ => ExternalCode.leanInline hl {} | .data .., content => .concat <| content.map goI @@ -86,7 +96,7 @@ open Verso.Doc Elab Concrete open Lean.Elab Command Term open PartElabM -def getModuleWithDocs (path : StrLit) (mod : Ident) (title : StrLit) (metadata? : Option Term) (genre : Syntax := mkIdent ``Manual) : TermElabM Name := +meta def getModuleWithDocs (path : StrLit) (mod : Ident) (title : StrLit) (metadata? : Option Term) (genre : Syntax := mkIdent ``Manual) : TermElabM Name := withTraceNode `verso.blog.literate (fun _ => pure m!"Literate '{title.getString}'") do let titleParts ← stringToInlines title @@ -139,19 +149,19 @@ open ArgParse variable [Monad m] [MonadError m] [MonadLiftT CoreM m] -structure IncludeLiterateConfig where +meta structure IncludeLiterateConfig where path : StrLit level : Option NumLit modName : Ident title : StrLit -instance : FromArgs IncludeLiterateConfig m where +meta instance : FromArgs IncludeLiterateConfig m where fromArgs := IncludeLiterateConfig.mk <$> .positional' `path <*> .named' `level true <*> .positional' `name <*> .positional' `title @[part_command Lean.Doc.Syntax.command] -def includeLiterateSection : PartCommand +meta def includeLiterateSection : PartCommand | `(block|command{includeLiterate $args* }) => do let {path, level, modName, title} ← parseThe IncludeLiterateConfig (← parseArgs args) let ref ← getRef diff --git a/src/verso-manual/VersoManual/LocalContents.lean b/src/verso-manual/VersoManual/LocalContents.lean index 5813b0ab4..4e51a5407 100644 --- a/src/verso-manual/VersoManual/LocalContents.lean +++ b/src/verso-manual/VersoManual/LocalContents.lean @@ -3,10 +3,14 @@ Copyright (c) 2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ +module import Verso +public import Verso.Doc.Html import MultiVerso.Slug -import VersoManual.Basic +public import VersoManual.Basic +public import Lean.Attributes +public import Lean.Elab.Term.TermElabM open Lean open Verso.Multi @@ -22,10 +26,10 @@ def LocalContentItemRecognizer.failure : LocalContentItemRecognizer := fun _ => def LocalContentItemRecognizer.orElse (r1 r2 : LocalContentItemRecognizer) : LocalContentItemRecognizer := fun b => r1 b <|> r2 b -initialize localContentAttr : TagAttribute ← +meta initialize localContentAttr : TagAttribute ← registerTagAttribute `local_content_list "Functions that recognize items for the page-local table of contents" -private def localContentRecognizers [Monad m] [MonadLiftT MetaM m] [MonadOptions m] [MonadEnv m] [MonadError m] : m (Array Name) := do +private meta def localContentRecognizers [Monad m] [MonadLiftT MetaM m] [MonadOptions m] [MonadEnv m] [MonadError m] : m (Array Name) := do let st := localContentAttr.ext.toEnvExtension.getState (← getEnv) let st' := st.importedEntries.flatten ++ st.state.toArray @@ -46,13 +50,13 @@ scoped elab "local_content_recognizer_fun" : term => do stx ← `($(mkIdent f) <|> $stx) elabTerm stx none -structure HeaderStatus where +public structure HeaderStatus where level : Nat numbering : Option String deriving Repr open Verso.Output in -structure LocalContentItem where +public structure LocalContentItem where header? : Option HeaderStatus dest : String linkTexts : Array (String × Html) @@ -86,7 +90,7 @@ partial def toNone : Doc.Inline Manual → Doc.Inline Genre.none open Verso.Output Html -def LocalContentItem.toHtml (item : LocalContentItem) : Html := +public def LocalContentItem.toHtml (item : LocalContentItem) : Html := have := item.linkTexts_nonempty let txt := {{{{item.linkTexts[0].2}}}} if let some ⟨level, numbering⟩ := item.header? then @@ -191,7 +195,7 @@ def uniquifyLocalItems (items : Array LocalContentItem) : Array LocalContentItem /-- How far down the tree should be traversed when collecting local items? -/ -inductive SubpartSpec where +public inductive SubpartSpec where /-- Include only the part itself, as a header. -/ | none /-- Include `n` levels of content below the current header. -/ @@ -200,7 +204,7 @@ inductive SubpartSpec where | all deriving DecidableEq, Repr -instance : Ord SubpartSpec where +public instance : Ord SubpartSpec where compare | .none, .none => .eq | .none, _ => .lt @@ -259,7 +263,7 @@ where withoutPrefix (str : String) (prefix? : Option String) : String := prefix?.bind (str.dropPrefix? · |>.map String.Slice.copy) |>.getD str -def localContents [Monad m] [ToHtml Manual m (Doc.Inline Manual)] [MonadReaderOf ExtensionImpls m] +public def localContents [Monad m] [ToHtml Manual m (Doc.Inline Manual)] [MonadReaderOf ExtensionImpls m] (opts : Html.Options m) (ctxt : TraverseContext) (xref : TraverseState) (p : Part Manual) (sectionNumPrefix : Option String := none) diff --git a/src/verso-manual/VersoManual/Marginalia.lean b/src/verso-manual/VersoManual/Marginalia.lean index baf819f51..a54c7057f 100644 --- a/src/verso-manual/VersoManual/Marginalia.lean +++ b/src/verso-manual/VersoManual/Marginalia.lean @@ -3,12 +3,14 @@ Copyright (c) 2024 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ - +module import Verso import Verso.Doc.ArgParse -import Verso.Doc.Elab.Monad +public import Verso.Doc.Elab.Inline +public import Verso.Doc.Elab.Monad import Verso.Code -import VersoManual.Basic +public import VersoManual.Basic + namespace Verso.Genre.Manual @@ -16,7 +18,7 @@ open Lean Elab open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets open SubVerso.Highlighting Highlighted -def Marginalia.css := r#" +public def Marginalia.css := r#" .marginalia .note { position: relative; padding: 0.5rem; @@ -92,7 +94,7 @@ body { "# open Verso.Output Html in -def Marginalia.html (content : Html) : Html := +public def Marginalia.html (content : Html) : Html := {{{{content}}}} /- @@ -105,10 +107,10 @@ stylistic sense to render them as footnotes in a fundamentally paginated format. -/ open Verso.Output TeX in -def Marginalia.TeX (content : TeX) : TeX := +public def Marginalia.TeX (content : TeX) : TeX := \TeX{ \footnote{ \Lean{ content } } } -inline_extension Inline.margin where +public inline_extension Inline.margin where traverse _ _ _ := do pure none toTeX := @@ -122,7 +124,7 @@ inline_extension Inline.margin where Marginalia.html <$> content.mapM goI @[role] -def margin : RoleExpanderOf Unit +public meta def margin : RoleExpanderOf Unit | (), inlines => do let content ← inlines.mapM elabInline ``(Doc.Inline.other Inline.margin #[$content,*]) diff --git a/src/verso-manual/VersoManual/Table.lean b/src/verso-manual/VersoManual/Table.lean index 7f6f2ba0c..69f2cfae8 100644 --- a/src/verso-manual/VersoManual/Table.lean +++ b/src/verso-manual/VersoManual/Table.lean @@ -3,10 +3,12 @@ Copyright (c) 2024-2025 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ - -import VersoManual.Basic +module +public import VersoManual.Basic import Verso.Doc.ArgParse import Verso.Doc.Elab +public meta import Verso.Doc.Elab.Block +public import Verso.Doc.Elab.Monad open Verso Doc Elab open Verso.Genre Manual @@ -19,13 +21,13 @@ set_option pp.rawOnError true namespace Verso.Genre.Manual -inductive TableConfig.Alignment where +public inductive TableConfig.Alignment where | left | right | center deriving ToJson, FromJson, DecidableEq, Repr, Ord open Syntax in open TableConfig.Alignment in -instance : Quote TableConfig.Alignment where +meta instance : Quote TableConfig.Alignment where quote | .left => mkCApp ``left #[] | .center => mkCApp ``center #[] @@ -42,14 +44,14 @@ def Alignment.htmlClass : Alignment → String end TableConfig -structure TableConfig where +public structure TableConfig where /-- Name for refs -/ name : Option String := none header : Bool := false /-- Alignment in the text (`none` means defer to stylesheet default) -/ alignment : Option TableConfig.Alignment := none -block_extension Block.table (columns : Nat) (header : Bool) (tag : Option String) (alignment : Option TableConfig.Alignment) (assignedTag : Option Tag := none) where +public block_extension Block.table (columns : Nat) (header : Bool) (tag : Option String) (alignment : Option TableConfig.Alignment) (assignedTag : Option Tag := none) where data := ToJson.toJson (columns, header, tag, assignedTag, alignment) traverse id data contents := do @@ -164,8 +166,9 @@ table.tabular td > p:last-child, table.tabular th > p:first-child { section variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] [MonadFileMap m] -def TableConfig.parse : ArgParse m TableConfig := - TableConfig.mk <$> .named `tag .string true <*> .flag `header true <*> .named `align alignment true +public meta instance : FromArgs TableConfig m where + fromArgs := + TableConfig.mk <$> .named `tag .string true <*> .flag `header true <*> .named `align alignment true where alignment := { description := "Alignment of the table ('left', 'right', or 'center')" @@ -179,13 +182,10 @@ where | _ => throwErrorAt x "Expected 'left', 'right', or 'center'" | .num x | .str x => throwErrorAt x "Expected 'left', 'right', or 'center'" } - -instance : FromArgs TableConfig m := ⟨TableConfig.parse⟩ - end @[directive] -def table : DirectiveExpanderOf TableConfig +public meta def table : DirectiveExpanderOf TableConfig | cfg, contents => do -- The table should be a list of lists. Extract them! let #[oneBlock] := contents diff --git a/src/verso-tutorial/VersoTutorial/Basic.lean b/src/verso-tutorial/VersoTutorial/Basic.lean index 1fecb8596..9d1c428cc 100644 --- a/src/verso-tutorial/VersoTutorial/Basic.lean +++ b/src/verso-tutorial/VersoTutorial/Basic.lean @@ -144,7 +144,7 @@ def savePartXref (slug : Slug) (id : InternalId) (part : Part Tutorial) : Manual "sectionNum": null }) -block_extension Block.displayOnly where +public block_extension Block.displayOnly where traverse _ _ _ _ := pure none toHtml := some <| fun _ goB _ _ content => content.mapM goB toTeX := some <| fun _ goB _ _ content => content.mapM goB @@ -155,7 +155,7 @@ def displayOnly : Elab.DirectiveExpanderOf Unit | (), contents => do ``(Block.other Block.displayOnly #[$(← contents.mapM Elab.elabBlock),*]) -block_extension Block.codeOnly where +public block_extension Block.codeOnly where traverse _ _ _ _ := pure none toHtml := some <| fun _ _ _ _ _ => pure .empty toTeX := some <| fun _ _ _ _ _ => pure .empty diff --git a/src/verso/Verso/Doc/Concrete.lean b/src/verso/Verso/Doc/Concrete.lean index 7fc944ec4..ed803eb12 100644 --- a/src/verso/Verso/Doc/Concrete.lean +++ b/src/verso/Verso/Doc/Concrete.lean @@ -354,7 +354,7 @@ private meta def finishDoc : Command.CommandElabM Unit:= do let doc ← Command.runTermElabM fun _ => finished.toVersoDoc versoEnv.genreSyntax versoEnv.ctx versoEnv.docState versoEnv.partState let ty ← ``(VersoDoc $versoEnv.genreSyntax) - Command.elabCommand (← `(def $n : $ty := $doc)) + Command.elabCommand (← `(public def $n : $ty := $doc)) syntax (name := replaceDoc) "#doc " "(" term ") " str " =>" : command elab_rules : command diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean index 92db53922..4d52136a6 100644 --- a/src/verso/Verso/Doc/Elab/Monad.lean +++ b/src/verso/Verso/Doc/Elab/Monad.lean @@ -664,6 +664,8 @@ unsafe initialize registerBuiltinAttribute { | `(attr|role $x) => realizeGlobalConstNoOverloadWithInfo x | _ => throwError "Invalid `role` attribute" + ensureAttrDeclIsMeta `role declName k + let n ← mkFreshUserName <| declName ++ `role let ((e, t), _) ← Meta.MetaM.run (ctx := {}) (s := {}) do @@ -678,7 +680,7 @@ unsafe initialize registerBuiltinAttribute { pure (e, t) - addAndCompile <| .defnDecl { + let decl := Declaration.defnDecl { name := n, levelParams := [], type := t, @@ -686,6 +688,12 @@ unsafe initialize registerBuiltinAttribute { hints := .opaque, safety := .safe } + addDecl decl + + if (← getEnv).header.isModule then + modifyEnv (markMeta · n) + + compileDecl decl addDocStringCore' n (← findSimpleDocString? (← getEnv) declName) @@ -735,6 +743,8 @@ unsafe initialize registerBuiltinAttribute { | `(attr|code_block $x) => realizeGlobalConstNoOverloadWithInfo x | _ => throwError "Invalid `code_block` attribute" + ensureAttrDeclIsMeta `code_block declName k + let n ← mkFreshUserName <| declName ++ `code_block let ((e, t), _) ← Meta.MetaM.run (ctx := {}) (s := {}) do @@ -749,7 +759,7 @@ unsafe initialize registerBuiltinAttribute { pure (e, t) - addAndCompile <| .defnDecl { + let decl := Declaration.defnDecl { name := n, levelParams := [], type := t, @@ -757,6 +767,12 @@ unsafe initialize registerBuiltinAttribute { hints := .opaque, safety := .safe } + addDecl decl + + if (← getEnv).header.isModule then + modifyEnv (markMeta · n) + + compileDecl decl addDocStringCore' n (← findSimpleDocString? (← getEnv) declName) @@ -823,6 +839,8 @@ unsafe initialize registerBuiltinAttribute { | `(attr|directive $x) => realizeGlobalConstNoOverloadWithInfo x | _ => throwError "Invalid `directive` attribute" + ensureAttrDeclIsMeta `directive declName k + let n ← mkFreshUserName <| declName ++ `directive let ((e, t), _) ← Meta.MetaM.run (ctx := {}) (s := {}) do @@ -837,7 +855,7 @@ unsafe initialize registerBuiltinAttribute { pure (e, t) - addAndCompile <| .defnDecl { + let decl := Declaration.defnDecl { name := n, levelParams := [], type := t, @@ -845,6 +863,12 @@ unsafe initialize registerBuiltinAttribute { hints := .opaque, safety := .safe } + addDecl decl + + if (← getEnv).header.isModule then + modifyEnv (markMeta · n) + + compileDecl decl addDocStringCore' n (← findSimpleDocString? (← getEnv) declName) @@ -911,6 +935,8 @@ unsafe initialize registerBuiltinAttribute { | `(attr|block_command $x) => realizeGlobalConstNoOverloadWithInfo x | _ => throwError "Invalid `block_command` attribute" + ensureAttrDeclIsMeta `block_command declName k + let n ← mkFreshUserName <| declName ++ `block_command let ((e, t), _) ← Meta.MetaM.run (ctx := {}) (s := {}) do @@ -924,7 +950,7 @@ unsafe initialize registerBuiltinAttribute { pure (e, t) - addAndCompile <| .defnDecl { + let decl := Declaration.defnDecl { name := n, levelParams := [], type := t, @@ -932,6 +958,12 @@ unsafe initialize registerBuiltinAttribute { hints := .opaque, safety := .safe } + addDecl decl + + if (← getEnv).header.isModule then + modifyEnv (markMeta · n) + + compileDecl decl addDocStringCore' n (← findSimpleDocString? (← getEnv) declName) diff --git a/test-projects/literate-config/lake-manifest.json b/test-projects/literate-config/lake-manifest.json index cf9a80b56..792f01ed2 100644 --- a/test-projects/literate-config/lake-manifest.json +++ b/test-projects/literate-config/lake-manifest.json @@ -8,6 +8,16 @@ "inherited": false, "dir": "../..", "configFile": "lakefile.lean"}, + {"url": "https://github.com/david-christiansen/doc-gen4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "1bec291d9b93db694d25887e9695f5e277102e79", + "name": "«doc-gen4»", + "manifestFile": "lake-manifest.json", + "inputRev": "pp-db", + "inherited": true, + "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, @@ -37,6 +47,46 @@ "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}], + "configFile": "lakefile.lean"}, + {"url": "https://github.com/kim-em/leansqlite", + "type": "git", + "subDir": null, + "scope": "", + "rev": "d14544c72b593af6a66131bc34cdab16bf7c0940", + "name": "leansqlite", + "manifestFile": "lake-manifest.json", + "inputRev": "suppress-reducibility-warning", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "", + "rev": "61cd682f2a25175996bc1b9e8d8231e76cded866", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "scope": "", + "rev": "629254926fb54ef83d582bd41a0b9eb72b934015", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "nightly-testing", + "inherited": true, + "configFile": "lakefile.toml"}], "name": "«literate-config-test»", "lakeDir": ".lake"} diff --git a/test-projects/literate-multi-root/lake-manifest.json b/test-projects/literate-multi-root/lake-manifest.json index 2c2f40bee..5f064478c 100644 --- a/test-projects/literate-multi-root/lake-manifest.json +++ b/test-projects/literate-multi-root/lake-manifest.json @@ -8,6 +8,16 @@ "inherited": false, "dir": "../..", "configFile": "lakefile.lean"}, + {"url": "https://github.com/david-christiansen/doc-gen4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "1bec291d9b93db694d25887e9695f5e277102e79", + "name": "«doc-gen4»", + "manifestFile": "lake-manifest.json", + "inputRev": "pp-db", + "inherited": true, + "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, @@ -37,6 +47,46 @@ "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}], + "configFile": "lakefile.lean"}, + {"url": "https://github.com/kim-em/leansqlite", + "type": "git", + "subDir": null, + "scope": "", + "rev": "d14544c72b593af6a66131bc34cdab16bf7c0940", + "name": "leansqlite", + "manifestFile": "lake-manifest.json", + "inputRev": "suppress-reducibility-warning", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "", + "rev": "61cd682f2a25175996bc1b9e8d8231e76cded866", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "scope": "", + "rev": "629254926fb54ef83d582bd41a0b9eb72b934015", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "nightly-testing", + "inherited": true, + "configFile": "lakefile.toml"}], "name": "«literate-multi-root-test»", "lakeDir": ".lake"} diff --git a/test-projects/textbook/DemoTextbook/Meta/Lean.lean b/test-projects/textbook/DemoTextbook/Meta/Lean.lean index ef6ccc517..e445c7923 100644 --- a/test-projects/textbook/DemoTextbook/Meta/Lean.lean +++ b/test-projects/textbook/DemoTextbook/Meta/Lean.lean @@ -13,7 +13,7 @@ open Lean namespace DemoTextbook -block_extension Block.savedLean (file : String) (source : String) where +public block_extension Block.savedLean (file : String) (source : String) where data := .arr #[.str file, .str source] traverse _ _ _ := pure none @@ -22,7 +22,7 @@ block_extension Block.savedLean (file : String) (source : String) where toHtml := some fun _ goB _ _ contents => contents.mapM goB -block_extension Block.savedImport (file : String) (source : String) where +public block_extension Block.savedImport (file : String) (source : String) where data := .arr #[.str file, .str source] traverse _ _ _ := pure none