[Don't merge] Make infoview tabbed

Projects/MathlibDemo/MathlibDemo.lean

@@ -6,3 +6,9 @@ import MathlibDemo.Bijection
 import MathlibDemo.Logic
 import MathlibDemo.Rational
 import MathlibDemo.Ring
+
+import Verso
+import VersoBlog
+import VersoManual
+import VersoUtil
+import VersoSearch

Projects/MathlibDemo/build.sh

@@ -3,19 +3,6 @@
 # Operate in the directory where this file is located
 cd $(dirname $0)
 
-# Updating Mathlib: We follow the instructions at
-# https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4
-
-# Note: we had once problems with the `lake-manifest` when a new dependency got added
-# to `mathlib`, we may need to add `rm lake-manifest.json` again if that's still a problem.
-
-# currently the mathlib post-update-hook is not good enough to update the lean-toolchain.
-# things break if the new lakefile is not valid in the old lean version
-curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
-
-# note: mathlib has now a post-update hook that modifies the `lean-toolchain`
-# and calls `lake exe cache get`.
-
 lake update -R
 lake build
 lake build Batteries

Projects/MathlibDemo/lake-manifest.json

@@ -1,31 +1,61 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/mathlib4",
+ [{"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bfd79bd53242ce07c2f41264531699b721cd209d",
+   "rev": "9137d010a277cd29e0989a65445805c292caf01e",
+   "name": "verso",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.27.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.27.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "1603151ac0db4e822908e18094f16acc250acaff",
+   "scope": "",
+   "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "38ac5945d744903ffcc473ce1030223991b11cf6",
+   "name": "MD4Lean",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/subverso",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "1e55697c44a646f8a22e2a91878efc4496aa5743",
+   "name": "subverso",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
+   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e25fe66cf13e902ba550533ef681cc35a9f18dc2",
+   "rev": "8f497d55985a189cea8020d9dc51260af1e41ad2",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +75,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6980f6ca164de593cb77cd03d8eac549cc444156",
+   "rev": "c04225ee7c0585effbd933662b3151f01b600e40",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.62",
+   "inputRev": "v0.0.85",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c3a19fa17982c5c1413fea335f371869b8b12e1d",
+   "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e1d2994e0acdee2f0c03c9d84d28a5df34aa0020",
+   "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5e6a77528fb6cace1f0adf2563e4e1bc1da541ae",
+   "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +115,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "a0abd472348dd725adbb26732e79b26e7e220913",
+   "rev": "55c37290ff6186e2e965d68cf853a57c0702db82",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.27.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "MathlibDemo",

Projects/MathlibDemo/lakefile.toml

@@ -7,7 +7,12 @@ pp.unicode.fun = true
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "master"
+rev = "v4.27.0"
+
+[[require]]
+name = "verso"
+git = "https://github.com/leanprover/verso"
+rev = "v4.27.0"
 
 [[lean_lib]]
 name = "MathlibDemo"

Projects/MathlibDemo/lean-toolchain

@@ -1 +1,2 @@
-leanprover/lean4:v4.21.0-rc3
+leanprover/lean4:v4.27.0
+

Projects/Stable/Stable.lean

@@ -0,0 +1,5 @@
+import Verso
+import VersoBlog
+import VersoManual
+import VersoUtil
+import VersoSearch

Projects/Stable/Stable/SampleDoc.lean

@@ -0,0 +1,24 @@
+import VersoManual
+open Verso Doc
+open Verso.Genre Manual
+open Verso.Genre.Manual.InlineLean
+
+#doc (Manual) "My Document" =>
+
+This is a Verso document.
+
+It can include inline math, like this: $`x + 4 = -3`.
+
+It can also include block math, like
+$$`\int_\mathsf{this}^\mathtt{orthis} \mathit{or{\ldots}maybe{\ldots}this}`
+
+We also support inline lean, like this: {lean}`Nat.add_assoc`.
+
+We also support block lean, like this:
+
+```lean
+/-- The name we will be greeting -/
+def theName := "Jimothy"
+
+#eval s!"Hello {theName}"
+```

Projects/Stable/build.sh

@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+
+# Operate in the directory where this file is located
+cd $(dirname $0)
+
+lake update -R
+lake build

Projects/Stable/lake-manifest.json

@@ -0,0 +1,45 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/verso",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "9137d010a277cd29e0989a65445805c292caf01e",
+   "name": "verso",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.27.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "38ac5945d744903ffcc473ce1030223991b11cf6",
+   "name": "MD4Lean",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/subverso",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "1e55697c44a646f8a22e2a91878efc4496aa5743",
+   "name": "subverso",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"}],
+ "name": "Stable",
+ "lakeDir": ".lake"}

Projects/Stable/lakefile.toml

@@ -0,0 +1,13 @@
+name = "Stable"
+defaultTargets = ["Stable"]
+
+[leanOptions]
+pp.unicode.fun = true
+
+[[require]]
+name = "verso"
+git = "https://github.com/leanprover/verso"
+rev = "v4.27.0"
+
+[[lean_lib]]
+name = "Stable"

Projects/Stable/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.27.0