Verso doc

.gitignore

@@ -1,4 +1,5 @@
 .lake/
 docbuild/lake-manifest.json
 docbuild/lean-toolchain
-html/
+html/
+/KernelHomManual.lean

KernelHom/Tactic/Hom/KernelDiagram.lean

@@ -60,10 +60,6 @@ def Node.toPenroseVar_kernel (n : Node) : MetaM PenroseVar := do
       pure n.e
   return ⟨"E", [n.vPos, n.hPosSrc, n.hPosTar], expr⟩
 
-def Strand.toPenroseVar_kernel (s : Strand) : MetaM PenroseVar := do
-  let expr := Expr.const ``True []
-  return ⟨"f", [s.vPos, s.hPos], expr ⟩
-
 open scoped Jsx in
 /-- Construct a kernelized string diagram from a Penrose `sub`stance program and
 expressions `embeds` to display as labels in the diagram. -/
@@ -88,7 +84,7 @@ def mkKernelDiagram (nodes : List (List Node)) (strands : List (List Strand)) :
   /- Add 1-morphisms as strings. -/
   for l in strands do
     for s in l do
-      StringDiagram.addConstructor "Mor1" (← s.toPenroseVar_kernel)
+      StringDiagram.addConstructor "Mor1" s.toPenroseVar
         "MakeString" [← s.startPoint.toPenroseVar_kernel, ← s.endPoint.toPenroseVar_kernel]
 
 end Mathlib.Tactic.Widget.StringDiagram

Verso/KernelHomManual/Tools/VersoKernelDiagram.lean → KernelHomManual/Tools/VersoKernelDiagram.lean

@@ -111,7 +111,7 @@ block_extension Block.stringDiagramWidget (payload : StringDiagramPayload) where
         match FromJson.fromJson? (α := StringDiagramPayload) data with
         | .ok payload => pure payload
         | .error err =>
-          Verso.Doc.Html.HtmlT.logError s!"Could not deserialize string diagram payload: {err}"
+          Verso.reportError s!"Could not deserialize string diagram payload: {err}"
           pure {
             html := Json.null,
             diagramHash := 0,

build_manual.sh

@@ -1,9 +1,9 @@
 set -x -e
 
-rm -rf _out html
+rm -rf _out html KernelHomManual.lean
 lake exe manual
 mkdir html
 mv _out/html-multi/* html/
 rm -rf _out
 mkdir -p html/static
-cp Verso/static_files/* html/static
+cp verso_static_files/* html/static

lakefile.toml

@@ -27,10 +27,9 @@ globs = ["KernelHomTests.+"]
 
 [[lean_lib]]
 name = "KernelHomManual"
-srcDir = "Verso/"
-root = "KernelHomManual"
+globs = ["KernelHomManual.+"]
 
 [[lean_exe]]
 name = "manual"
-srcDir = "Verso/"
-root = "KernelHomManual"
+srcDir = "KernelHomManual/"
+root = "Manual"