Add index for DuperXp

utensil · Oct 23, 2024 · 55daa9e · 55daa9e
1 parent 70cce06
commit 55daa9e
Show file tree

Hide file tree

Showing 5 changed files with 36 additions and 18 deletions.
diff --git a/README.md b/README.md
@@ -9,8 +9,10 @@ My monorepo for formalization.
 I explore with the following formalization systems, and do interactive [literate programming](https://en.wikipedia.org/wiki/Literate_programming) when supported, because then one can interact with the formalization and inspect intermediate (goal) states just from a Web browser.
 
 - [Lean 4](./lean4/README.md)
-  - [examples](https://utensil.github.io/formal-land/lean4/) annotated by [alectryon](https://github.com/cpitclaudel/alectryon)
-- [Aya](./aya/README.md)
+    - annotated by [alectryon](https://github.com/cpitclaudel/alectryon)
+    - [Lean 4 Playground examples](https://utensil.github.io/formal-land/lean4/)
+    - [Duper explorations](https://utensil.github.io/formal-land/lean4-duper-xp/)
+  - [Aya](./aya/README.md)
   - [haskeller-tutorial](https://utensil.github.io/formal-land/aya/haskeller-tutorial.html)
   - [prover-tutorial](https://utensil.github.io/formal-land/aya/prover-tutorial.html)
   - [literate](https://utensil.github.io/formal-land/aya/literate.html)

diff --git a/lean4-duper-xp/DuperXp/index.lean b/lean4-duper-xp/DuperXp/index.lean
@@ -0,0 +1,19 @@
+/-!
+
+# Duper explorations
+
+- [Basic.lean](./Basic.html)
+- [CliffordAlgebra.lean](./CliffordAlgebra.html)
+
+-/
+
+#eval Lean.versionString
+
+#eval Lean.versionStringCore
+
+#eval Lean.toolchain
+
+#eval Lean.origin
+
+#eval Lean.githash
+
diff --git a/lean4-xp-kit/scripts/annotate.lean b/lean4-xp-kit/scripts/annotate.lean
@@ -35,7 +35,7 @@ def main (args : List String) : IO Unit := do
   let positionalArgs := args.erase "--toc" |>.erase "--verbose"
 
   if positionalArgs.isEmpty then
-    IO.eprintln "Usage: lake exe annotate [--verbose] [--toc] libraryName testFileName"
+    IO.eprintln "Usage: lake exe annotate [--verbose] [--toc] libraryName [targetFileName]"
     exit 1
 
   let libraryName := positionalArgs.head!

diff --git a/lean4-xp-kit/scripts/test.lean b/lean4-xp-kit/scripts/test.lean
@@ -36,7 +36,7 @@ def main (args : List String) : IO Unit := do
   let positionalArgs := args.erase "--no-noisy" |>.erase "--verbose"
 
   if positionalArgs.isEmpty then
-    IO.eprintln "Usage: lake exe test [--verbose] [--no-noisy] libraryName testFileName"
+    IO.eprintln "Usage: lake exe test [--verbose] [--no-noisy] libraryName [targetFileName]"
     exit 1
 
   let libraryName := positionalArgs.head!

diff --git a/lean4/Playground/index.lean b/lean4/Playground/index.lean
@@ -2,20 +2,6 @@
 
 # Lean 4 Playground
 
--/
-
-#eval Lean.versionString
-
-#eval Lean.versionStringCore
-
-#eval Lean.toolchain
-
-#eval Lean.origin
-
-#eval Lean.githash
-
-/-!
-
 ## Examples
 
 ### Literate reStructuredText (RST)
@@ -67,3 +53,14 @@
 - [Zulip/WithLog.lean](./Zulip/WithLog.html)
 
 -/
+
+#eval Lean.versionString
+
+#eval Lean.versionStringCore
+
+#eval Lean.toolchain
+
+#eval Lean.origin
+
+#eval Lean.githash
+