Minimal working Verso

.gitignore

@@ -14,3 +14,4 @@ tla/*.tex
 tla/*.pdf
 tla/states
 
+lean4-verso-xp/_out

lean4-verso-xp/Main.lean

@@ -0,0 +1,18 @@
+import VersoXp
+
+open Verso.Genre.Manual
+
+
+def main :=
+  manualMain (%doc VersoXp) (config := config)
+where
+  config := {
+    -- extraFiles := [("static", "static")],
+    -- extraCss := ["/static/colors.css", "/static/theme.css", "/static/print.css", "/static/fonts/source-serif/source-serif-text.css", "/static/fonts/source-code-pro/source-code-pro.css", "/static/katex/katex.min.css"],
+    -- extraJs := ["/static/katex/katex.min.js", "/static/math.js", "/static/print.js"],
+    emitTeX := false,
+    emitHtmlSingle := true, -- for proofreading
+    -- logo := some "/static/lean_logo.svg",
+    -- sourceLink := some "https://github.com/leanprover/reference-manual",
+    -- issueLink := some "https://github.com/leanprover/reference-manual/issues"
+  }

lean4-verso-xp/VersoXp.lean

@@ -1,3 +1,10 @@
-import Mathlib
-import Verso
-import VersoXp.Basic
+import VersoManual
+
+open Verso.Genre Manual
+
+set_option pp.rawOnError true
+
+#doc (Manual) "The Verso exploration" =>
+%%%
+tag := "verso-xp"
+%%%

lean4-verso-xp/VersoXp/Basic.lean

@@ -1 +1 @@
-def hello := "world"
+import Mathlib.Tactic.Basic

lean4-verso-xp/lake-manifest.json

@@ -1,154 +1,34 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
-   "name": "batteries",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/quote4",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
-   "name": "Qq",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "28fa80508edc97d96ed6342c9a771a67189e0baa",
-   "name": "aesop",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/ProofWidgets4",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
-   "name": "proofwidgets",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.42",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
+ [{"url": "https://github.com/leanprover/subverso.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/import-graph",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1",
-   "name": "importGraph",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/LeanSearchClient",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
-   "name": "LeanSearchClient",
+   "rev": "d0b2c57577661d7d558828929a2180ccd67ae1c4",
+   "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/mathlib4",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "809c3fb3b5c8f5d7dace56e200b426187516535a",
-   "name": "mathlib",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.12.0",
-   "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/acmepjz/md4lean",
+  {"url": "https://github.com/david-christiansen/md4lean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
+   "rev": "2b381ee8dceba3b934d3d4aea4a2702a61e5664f",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "6d2e06515f1ed1f74208d5a1da3a9cc26c60a7a0",
-   "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": "85e1e7143dd4cfa2b551826c27867bada60858e8",
-   "name": "BibtexQuery",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/doc-gen4",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "5119580cd7510a440d54f67834c9024cc03a3e32",
-   "name": "«doc-gen4»",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.12.0",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/HEPLean/HepLean",
-   "type": "git",
-   "subDir": null,
-   "scope": "HEPLean",
-   "rev": "4279302bfec42b6bf9ae26e624d3e8bc765b1814",
-   "name": "hep_lean",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "4279302bfec42b6bf9ae26e624d3e8bc765b1814",
-   "inherited": false,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover/subverso.git",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "f567482f2dcadd1858a5f85421c94a14f468a159",
-   "name": "subverso",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "parser",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "33b0ed5626cf5494a96d3a51efe376bdadf9cf63",
+   "rev": "f323aacf146f5c49f3b36810918a14c6c1fe662e",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.12.0",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "VersoXp",

lean4-verso-xp/lakefile.toml

@@ -2,23 +2,28 @@ name = "VersoXp"
 
 defaultTargets = ["VersoXp"]
 
-[[require]]
-name = "mathlib"
-scope = "leanprover-community"
-rev = "v4.12.0"
+# [[require]]
+# name = "mathlib"
+# scope = "leanprover-community"
+# rev = "v4.12.0"
 
-[[require]]
-name = "hep_lean"
-scope = "HEPLean"
-rev = "4279302bfec42b6bf9ae26e624d3e8bc765b1814"
+# [[require]]
+# name = "hep_lean"
+# scope = "HEPLean"
+# rev = "4279302bfec42b6bf9ae26e624d3e8bc765b1814"
 
 [[require]]
 name = "verso"
 scope = "leanprover"
-rev = "v4.12.0"
+rev = "main"
+# rev = "v4.12.0"
 
 [[lean_lib]]
 name = "VersoXp"
 
+[[lean_exe]]
+name = "mkVersoDoc"
+root = "Main"
+
 # see https://github.com/HEPLean/HepLean/blob/master/lakefile.toml for
 # an example of other configs

lean4-verso-xp/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:nightly-2024-10-14