From c63d2daccb30340c3df5e5e27e96c57268952660 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 12 Nov 2025 16:19:21 +0100 Subject: [PATCH 01/45] wip: tutorials --- Main.lean | 6 +- Manual.lean | 3 - Manual/Grind/ExtendedExamples.lean | 7 +- Manual/Meta.lean | 1 - Manual/Meta/Example.lean | 1 - Manual/Meta/Imports.lean | 38 --------- Manual/Meta/ParserAlias.lean | 2 +- Manual/Meta/Syntax.lean | 8 +- Tutorial.lean | 2 + .../Grind}/IndexMap.lean | 79 +++++++++++++++++-- {Manual => Tutorial}/VCGen.lean | 35 +++++--- TutorialMain.lean | 52 ++++++++++++ extended-examples/IndexMapGrind.lean | 15 +++- lakefile.lean | 9 ++- 14 files changed, 186 insertions(+), 72 deletions(-) delete mode 100644 Manual/Meta/Imports.lean create mode 100644 Tutorial.lean rename {Manual/Grind/ExtendedExamples => Tutorial/Grind}/IndexMap.lean (94%) rename {Manual => Tutorial}/VCGen.lean (97%) create mode 100644 TutorialMain.lean diff --git a/Main.lean b/Main.lean index ffc473b9c..101e07047 100644 --- a/Main.lean +++ b/Main.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2024 Lean FRO LLC. All rights reserved. +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 -/ @@ -36,11 +36,11 @@ def staticCss := {{ def main := manualMain (%doc Manual) (config := config) (extraSteps := [extractExamples]) where - config := Config.addSearch <| Config.addKaTeX { + config := { extraFiles := [("static", "static")], extraHead := #[plausible, staticJs, staticCss], emitTeX := false, - emitHtmlSingle := true, -- for proofreading + emitHtmlSingle := .immediately, -- 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", diff --git a/Manual.lean b/Manual.lean index 4e9144e6c..2952c6a7c 100644 --- a/Manual.lean +++ b/Manual.lean @@ -18,7 +18,6 @@ import Manual.ErrorExplanations import Manual.Tactics import Manual.Simp import Manual.Grind -import Manual.VCGen import Manual.BasicTypes import Manual.BasicProps import Manual.NotationsMacros @@ -100,8 +99,6 @@ Thus, this reference manual does not draw a barrier between the two aspects, but {include 0 Manual.Grind} -{include 0 Manual.VCGen} - {include 0 Manual.BasicProps} {include 0 Manual.BasicTypes} diff --git a/Manual/Grind/ExtendedExamples.lean b/Manual/Grind/ExtendedExamples.lean index 7ac200443..bc880375c 100644 --- a/Manual/Grind/ExtendedExamples.lean +++ b/Manual/Grind/ExtendedExamples.lean @@ -12,7 +12,6 @@ import Manual.Meta import Manual.Grind.ExtendedExamples.Integration import Manual.Grind.ExtendedExamples.IfElseNorm -import Manual.Grind.ExtendedExamples.IndexMap open Verso.Genre Manual open Verso.Genre.Manual.InlineLean @@ -27,8 +26,10 @@ open Lean.Grind tag := "grind-bigger-examples" %%% +:::TODO +Properly link to tutorial section +::: + {include 1 Manual.Grind.ExtendedExamples.Integration} {include 1 Manual.Grind.ExtendedExamples.IfElseNorm} - -{include 1 Manual.Grind.ExtendedExamples.IndexMap} diff --git a/Manual/Meta.lean b/Manual/Meta.lean index ec3b04891..c78713da8 100644 --- a/Manual/Meta.lean +++ b/Manual/Meta.lean @@ -33,7 +33,6 @@ import Manual.Meta.Syntax import Manual.Meta.Tactics import Manual.Meta.SpliceContents import Manual.Meta.Markdown -import Manual.Meta.Imports import Manual.Meta.Namespace diff --git a/Manual/Meta/Example.lean b/Manual/Meta/Example.lean index 882346526..e6d299242 100644 --- a/Manual/Meta/Example.lean +++ b/Manual/Meta/Example.lean @@ -6,7 +6,6 @@ Author: David Thrane Christiansen import VersoManual import Manual.Meta.Figure -import Manual.Meta.Imports import Manual.Meta.LzCompress import Lean.Elab.InfoTree.Types diff --git a/Manual/Meta/Imports.lean b/Manual/Meta/Imports.lean deleted file mode 100644 index 47df4bcaf..000000000 --- a/Manual/Meta/Imports.lean +++ /dev/null @@ -1,38 +0,0 @@ -/- -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 -import Lean.Elab.InfoTree.Types -import SubVerso.Highlighting.Code - -open scoped Lean.Doc.Syntax - -open Verso Doc Elab -open Lean Elab -open Verso.Genre.Manual InlineLean Scopes -open Verso.SyntaxUtils -open SubVerso.Highlighting -open ArgParse - -namespace Manual - -structure ImportsParams where - «show» : Bool := true - -instance : FromArgs ImportsParams m where - fromArgs := ImportsParams.mk <$> .flag `show true (some "Whether to show the import header") - -@[code_block] -def imports : CodeBlockExpanderOf ImportsParams - | { «show» } , str => do - let altStr ← parserInputString str - let p := Parser.whitespace >> Parser.Module.header.fn - let headerStx ← p.parseString altStr - let hl ← highlight headerStx #[] {} - if «show» then - ``(Block.other (Block.lean $(quote hl) {}) #[Block.code $(quote str.getString)]) - else - ``(Block.empty) diff --git a/Manual/Meta/ParserAlias.lean b/Manual/Meta/ParserAlias.lean index 882558c69..bcc4ee9b2 100644 --- a/Manual/Meta/ParserAlias.lean +++ b/Manual/Meta/ParserAlias.lean @@ -69,7 +69,7 @@ def parserAlias : DirectiveExpander pure #[← ``(Verso.Doc.Block.other (Block.parserAlias $(quote opts.name) $(quote declName) $(quote opts.show) $(quote stackSz?) $(quote autoGroupArgs) $(quote docs?) $(quote argCount)) #[$(contents ++ userContents),*])] @[inline] -private def getFromJson {α} [Inhabited α] [FromJson α] (v : Json) : HtmlT Genre.Manual (ReaderT ExtensionImpls IO) α:= +private def getFromJson {α} [Monad m] [Inhabited α] [FromJson α] (v : Json) : HtmlT Genre.Manual m α:= match FromJson.fromJson? (α := α) v with | .error e => do Verso.Doc.Html.HtmlT.logError diff --git a/Manual/Meta/Syntax.lean b/Manual/Meta/Syntax.lean index b96b58215..810b6f6c1 100644 --- a/Manual/Meta/Syntax.lean +++ b/Manual/Meta/Syntax.lean @@ -830,7 +830,7 @@ where return bar ++ .nest 2 (← production which stx |>.run' {}) def testGetBnf (config : FreeSyntaxConfig) (isFirst : Bool) (stxs : List Syntax) : TermElabM String := do - let (tagged, _) ← getBnf config isFirst stxs |>.run (← moduleGenreElabContext) {} {partContext := ⟨⟨default, default, default, default, default⟩, default⟩} + let (tagged, _) ← getBnf config isFirst stxs |>.run ⟨← ``(Manual), mkConst ``Manual, .always, none⟩ {} {partContext := ⟨⟨default, default, default, default, default⟩, default⟩} pure tagged.stripTags namespace Tests @@ -1352,7 +1352,7 @@ window.addEventListener("load", () => { "# open Verso.Output Html HtmlT in -private def nonTermHtmlOf (kind : Name) (doc? : Option String) (rendered : Html) : HtmlT Manual (ReaderT ExtensionImpls IO) Html := do +private def nonTermHtmlOf (kind : Name) (doc? : Option String) (rendered : Html) : HtmlT Manual (ReaderT Multi.AllRemotes (ReaderT ExtensionImpls IO)) Html := do let xref ← match (← state).resolveDomainObject syntaxKindDomain kind.toString with | .error _ => pure none @@ -1398,7 +1398,7 @@ def noLook (ctx : GrammarHtmlContext) : GrammarHtmlContext := end GrammarHtmlContext open Verso.Output Html in -abbrev GrammarHtmlM := ReaderT GrammarHtmlContext (HtmlT Manual (ReaderT ExtensionImpls IO)) +abbrev GrammarHtmlM := ReaderT GrammarHtmlContext (HtmlT Manual (ReaderT Multi.AllRemotes (ReaderT ExtensionImpls IO))) private def lookingAt (k : Name) : GrammarHtmlM α → GrammarHtmlM α := withReader (·.look k) @@ -1492,7 +1492,7 @@ where let inner ← go if let some k := (← read).lookingAt then unless k == nullKind do - if let some tgt := ((← HtmlT.state (genre := Manual) (m := ReaderT ExtensionImpls IO)).localTargets.keyword k none)[0]? then + if let some tgt := ((← HtmlT.state (genre := Manual) (m := ReaderT Multi.AllRemotes (ReaderT ExtensionImpls IO))).localTargets.keyword k none)[0]? then return {{{{inner}}}} return {{{{inner}}}} | .nonterminal k doc? => do diff --git a/Tutorial.lean b/Tutorial.lean new file mode 100644 index 000000000..9d2f83520 --- /dev/null +++ b/Tutorial.lean @@ -0,0 +1,2 @@ +import Tutorial.VCGen +import Tutorial.Grind.IndexMap diff --git a/Manual/Grind/ExtendedExamples/IndexMap.lean b/Tutorial/Grind/IndexMap.lean similarity index 94% rename from Manual/Grind/ExtendedExamples/IndexMap.lean rename to Tutorial/Grind/IndexMap.lean index f03d31a47..b8eacaca2 100644 --- a/Manual/Grind/ExtendedExamples/IndexMap.lean +++ b/Tutorial/Grind/IndexMap.lean @@ -5,13 +5,14 @@ Author: Leo de Moura, Kim Morrison -/ import VersoManual +import VersoTutorial import Lean.Parser.Term import Manual.Meta -open Verso.Genre Manual +open Verso.Genre Manual Tutorial open Verso.Genre.Manual.InlineLean hiding module open Verso.Doc.Elab (CodeBlockExpander) open Verso.Code.External @@ -30,8 +31,12 @@ set_option verso.exampleProject "." set_option verso.exampleModule "IndexMapGrind" -#doc (Manual) "`IndexMap`" => - +#doc (Tutorial) "`IndexMap`" => +%%% +slug := "grind-index-map" +summary := "A walkthrough of ..." +exampleStyle := .inlineLean `IndexMap +%%% In this section we'll build an example of a new data structure and basic API for it, illustrating the use of {tactic}`grind`. The example will be derived from Rust's [`indexmap`](https://docs.rs/indexmap/latest/indexmap/) data structure. @@ -60,6 +65,18 @@ Our goals will be: Ideally, we don't even need to see the proofs; they should mostly be handled invisibly by {tactic}`grind`. + +:::paragraph +The first step is to import the necessary data structures: +```anchor imports +import Std.Data.HashMap +``` +::: + +# Skeleton + +:::displayOnly + To begin with, we'll write out a skeleton of what we want to achieve, liberally using {lean}`sorry` as a placeholder for all proofs. In particular, this version makes no use of {tactic}`grind`. @@ -212,6 +229,9 @@ theorem findIdx_insert_self end IndexMap ``` +::: + +# Header 2 Let's get started. We'll aspire to never writing a proof by hand, and the first step of that is to install auto-parameters for the `size_keys` and `WF` field, @@ -219,6 +239,8 @@ so we can omit these fields whenever `grind` can prove them. While we're modifying the definition of `IndexMap` itself, lets make all the fields private, since we're planning on having complete encapsulation. ```anchor IndexMap +open Std + structure IndexMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where private indices : HashMap α Nat @@ -229,6 +251,14 @@ structure IndexMap keys[i]? = some a ↔ indices[a]? = some i := by grind ``` +For the rest of this tutorial, the following namespace and variable declarations are in effect: +```anchor variables +namespace IndexMap + +variable {α : Type u} {β : Type v} [BEq α] [Hashable α] +variable {m : IndexMap α β} {a : α} {b : β} {i : Nat} +``` + Let's give {tactic}`grind` access to the definition of `size`, and `size_keys` private field: ```anchor size @[inline] def size (m : IndexMap α β) : Nat := @@ -250,6 +280,21 @@ def emptyWithCapacity (capacity := 8) : IndexMap α β where ``` ::: +:::codeOnly +```anchor Membership +@[inline] def contains (m : IndexMap α β) + (a : α) : Bool := + m.indices.contains a + +instance : Membership α (IndexMap α β) where + mem m a := a ∈ m.indices + +instance {m : IndexMap α β} {a : α} : Decidable (a ∈ m) := + inferInstanceAs (Decidable (a ∈ m.indices)) +``` +::: + +:::displayOnly Our next task is to deal with the {lean}`sorry` in our construction of the original {anchorTerm GetElem?}`GetElem?` instance: ```anchor GetElem? (module := IndexMap) instance : @@ -261,6 +306,7 @@ instance : getElem! m a := m.indices[a]?.bind (m.values[·]?) |>.getD default ``` +::: The goal at this sorry is ``` @@ -331,7 +377,7 @@ However this proof is going to work, we know the following: * It must use the well-formedness condition of the map. * It can't do so without relating `m.indices[a]` and `m.indices[a]?` (because the later is what appears in the well-formedness condition). * The expected relationship there doesn't even hold unless the map `m.indices` satisfies {lean}`LawfulGetElem`, - for which we need {tech}[instances] of {lean}`LawfulBEq α` and {lean}`LawfulHashable α`. + for which we need {tech (remote:="reference")}[instances] of {lean}`LawfulBEq α` and {lean}`LawfulHashable α`. ::: :::TODO @@ -401,7 +447,13 @@ macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| grind) ::: :::paragraph -We can now return to constructing our {anchorName GetElem?}`GetElem?` instance, and simply write: +We can now return to constructing our {anchorName GetElem?}`GetElem?` instance. +In order to use the well-formedness condition, {tactic}`grind` must be able to unfold {anchorName size}`size`: +```anchor local_grind_size +attribute [local grind] size +``` +The {anchorTerm local_grind_size}`local` modifier restricts this unfolding to the current file. +With this in place, we can simply write: ```anchor GetElem? instance : GetElem? (IndexMap α β) α β (fun m a => a ∈ m) where getElem m a h := @@ -626,6 +678,23 @@ Trying again with {anchorName eraseSwap}`eraseSwap`, everything goes through cle | none => m ``` +:::codeOnly +```anchor getFindIdx +@[inline] def findIdx? (m : IndexMap α β) (a : α) : Option Nat := + m.indices[a]? + +@[inline] def findIdx (m : IndexMap α β) (a : α) + (h : a ∈ m := by get_elem_tactic) : Nat := + m.indices[a] + +@[inline] def getIdx? (m : IndexMap α β) (i : Nat) : Option β := + m.values[i]? + +@[inline] def getIdx (m : IndexMap α β) (i : Nat) + (h : i < m.size := by get_elem_tactic) : β := + m.values[i] +``` +::: Finally we turn to the verification theorems about the basic operations, relating {anchorName Verification}`getIdx`, {anchorName Verification}`findIdx`, and {anchorName Verification}`insert`. By adding a {anchorTerm Verification}`local grind` annotation allowing {tactic}`grind` to unfold the definitions of these operations, diff --git a/Manual/VCGen.lean b/Tutorial/VCGen.lean similarity index 97% rename from Manual/VCGen.lean rename to Tutorial/VCGen.lean index fe7788140..941ed915a 100644 --- a/Manual/VCGen.lean +++ b/Tutorial/VCGen.lean @@ -5,6 +5,7 @@ Author: Sebastian Graf -/ import VersoManual +import VersoTutorial import Manual.Meta import Manual.Papers @@ -24,14 +25,14 @@ set_option linter.unusedVariables false set_option linter.typography.quotes true set_option linter.typography.dashes true -set_option mvcgen.warning false - open Manual (comment) -#doc (Manual) "The `mvcgen` tactic" => +#doc (Tutorial) "The `mvcgen` tactic" => %%% tag := "mvcgen-tactic" -htmlSplit := .never +slug := "mvcgen" +summary := "summary here" +exampleStyle := .inlineLean `MVCGenTutorial %%% The {tactic}`mvcgen` tactic implements a _monadic verification condition generator_: @@ -43,15 +44,27 @@ In order to use the {tactic}`mvcgen` tactic, {module}`Std.Tactic.Do` must be imp # Verifying Imperative Programs Using `mvcgen` +:::paragraph This section is a tutorial that introduces the most important concepts of {tactic}`mvcgen` top-down. -Recall that you need to import {module}`Std.Tactic.Do` and open {namespace}`Std.Do` to run these examples: - +A little preparation is required. +Recall that you need to import {module}`Std.Tactic.Do` to use the tactic: ```imports import Std.Tactic.Do ``` +The code also makes use of hash sets from the standard library: +```imports +import Std.Data.HashSet +``` +Because {tactic}`mvcgen` is presently an experimental feature, a warning is issued when it is used. +The warning can be disabled as follows: +```lean +set_option mvcgen.warning false +``` +Finally, the namespace {namespace}`Std.Do` must be opened in order to run these examples: ```lean open Std.Do ``` +::: ## Preconditions and Postconditions @@ -69,7 +82,7 @@ This means that the postcondition holds no matter what. ## Loops and Invariants :::leanFirst -As a first example of {tactic}`mvcgen`, the function {name}`mySum` computes the sum of an array using {ref "let-mut"}[local mutable state] and a {keywordOf Lean.Parser.Term.doFor}`for` loop: +As a first example of {tactic}`mvcgen`, the function {name}`mySum` computes the sum of an array using {ref "let-mut" (remote:="reference")}[local mutable state] and a {keywordOf Lean.Parser.Term.doFor}`for` loop: ```lean def mySum (l : Array Nat) : Nat := Id.run do @@ -241,7 +254,7 @@ axiom onExcept : ExceptConds PostShape.pure ``` The proof has the same succinct structure as for the initial {name}`mySum` example, because we again offload all proofs to {tactic}`grind` and its existing automation around {name}`List.Nodup`. Therefore, the only difference is in the {tech}[loop invariant]. -Since our loop has an {ref "early-return"}[early return], we construct the invariant using the helper function {lean}`Invariant.withEarlyReturn`. +Since our loop has an {ref "early-return" (remote:="reference")}[early return], we construct the invariant using the helper function {lean}`Invariant.withEarlyReturn`. This function allows us to specify the invariant in three parts: * {lean}`onReturn ret seen` holds after the loop was left through an early return with value {lean}`ret`. @@ -296,7 +309,7 @@ Some observations: * The proof is even shorter than the one with {tactic}`mvcgen`. * The use of {tactic}`generalize` to generalize the accumulator relies on there being exactly one occurrence of {lean (type := "Std.HashSet Int")}`∅` to generalize. If that were not the case, we would have to copy parts of the program into the proof. This is a no-go for larger functions. * {tactic}`grind` splits along the control flow of the function and reasons about {name}`Id`, given the right lemmas. - While this works for {name}`Id.run_pure` and {name}`Id.run_bind`, it would not work for {name}`Id.run_seq`, for example, because that lemma is not {tech (key := "E-matching")}[E-matchable]. + While this works for {name}`Id.run_pure` and {name}`Id.run_bind`, it would not work for {name}`Id.run_seq`, for example, because that lemma is not {tech (key := "E-matching") (remote := "reference")}[E-matchable]. If {tactic}`grind` would fail, we would be forced to do all the control flow splitting and monadic reasoning by hand until {tactic}`grind` could pick up again. ::: @@ -570,7 +583,7 @@ Hypotheses in the Lean context are part of the immutable {deftech}_frame_ of the ## Monad Transformers and Lifting -Real-world programs often use monads that are built from multiple {tech}[monad transformers], with operations being frequently {ref "lifting-monads"}[lifted] from one monad to another. +Real-world programs often use monads that are built from multiple {tech (remote := "reference")}[monad transformers], with operations being frequently {ref "lifting-monads" (remote:="reference")}[lifted] from one monad to another. Verification of these programs requires taking this into account. We can tweak the previous example to demonstrate this. @@ -1026,6 +1039,6 @@ A common case for when a VC of the form {lean}`H ⊢ₛ T` is left behind is whe In this case, the proof will depend on a {lean}`WP m ps` instance which governs the translation into the {name}`Assertion` language, but the exact correspondence to `σs : List (Type u)` is yet unknown. To successfully discharge such a VC, `mvcgen` comes with an entire proof mode that is inspired by that of the Iris concurrent separation logic. (In fact, the proof mode was adapted in large part from its Lean clone, [`iris-lean`](https://github.com/leanprover-community/iris-lean).) -The {ref "tactic-ref-spred"}[tactic reference] contains a list of all proof mode tactics. +The {ref "tactic-ref-spred" (remote:="reference")}[tactic reference] contains a list of all proof mode tactics. ::: diff --git a/TutorialMain.lean b/TutorialMain.lean new file mode 100644 index 000000000..e1eac3294 --- /dev/null +++ b/TutorialMain.lean @@ -0,0 +1,52 @@ +/- +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 +-/ + +import VersoTutorial +import Tutorial + +open Verso.Genre.Manual +open Verso.Genre.Tutorial + +open Verso.Output.Html in +def plausible := {{ + + }} + +open Verso.Output.Html in +def staticJs := {{ + + + }} + +open Verso.Output.Html in +def staticCss := {{ + + + + + + + + }} + +open Verso.Doc Concrete in +def tutorials : Tutorials where + content := + (verso (.none) "foo" + ::::::: + abc + :::::::).toPart + + topics := #[ + { title := "Tactics" + description := #[blocks!"..."] + tutorials := #[%doc Tutorial.VCGen, %doc Tutorial.Grind.IndexMap] + } + + ] + +def main := + tutorialsMain tutorials (config := {remoteConfigFile := "tutorial-remotes.json", destination := "_tutorial-out"}) diff --git a/extended-examples/IndexMapGrind.lean b/extended-examples/IndexMapGrind.lean index 5639e86f4..5e972c6a7 100644 --- a/extended-examples/IndexMapGrind.lean +++ b/extended-examples/IndexMapGrind.lean @@ -1,4 +1,6 @@ +--ANCHOR: imports import Std.Data.HashMap +--ANCHOR_END: imports import IndexMapGrind.CheckMsgs open Std in @@ -19,9 +21,11 @@ example (m : HashMap Nat Nat) : (m.insert 1 2).size ≤ m.size + 1 := by get_elem_tactic -open Std + -- ANCHOR: IndexMap +open Std + structure IndexMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where private indices : HashMap α Nat @@ -32,10 +36,13 @@ structure IndexMap keys[i]? = some a ↔ indices[a]? = some i := by grind -- ANCHOR_END: IndexMap + +-- ANCHOR: variables namespace IndexMap variable {α : Type u} {β : Type v} [BEq α] [Hashable α] variable {m : IndexMap α β} {a : α} {b : β} {i : Nat} +-- ANCHOR_END: variables -- ANCHOR: size @[inline] def size (m : IndexMap α β) : Nat := @@ -58,6 +65,7 @@ instance : EmptyCollection (IndexMap α β) where instance : Inhabited (IndexMap α β) where default := ∅ +-- ANCHOR: Membership @[inline] def contains (m : IndexMap α β) (a : α) : Bool := m.indices.contains a @@ -67,6 +75,7 @@ instance : Membership α (IndexMap α β) where instance {m : IndexMap α β} {a : α} : Decidable (a ∈ m) := inferInstanceAs (Decidable (a ∈ m.indices)) +-- ANCHOR_END: Membership discarding /-- @@ -110,6 +119,7 @@ stop discarding a ∈ m ↔ a ∈ m.indices := Iff.rfl -- ANCHOR_END: mem_indices_of_mem +-- ANCHOR: getFindIdx @[inline] def findIdx? (m : IndexMap α β) (a : α) : Option Nat := m.indices[a]? @@ -123,6 +133,7 @@ stop discarding @[inline] def getIdx (m : IndexMap α β) (i : Nat) (h : i < m.size := by get_elem_tactic) : β := m.values[i] +-- ANCHOR_END: getFindIdx -- ANCHOR: Lawfuls variable [LawfulBEq α] [LawfulHashable α] @@ -153,7 +164,9 @@ end grind_pattern getElem_indices_lt => m.indices[a] -- ANCHOR_END: getElem_indices_lt_pattern +-- ANCHOR: local_grind_size attribute [local grind] size +-- ANCHOR_END: local_grind_size -- ANCHOR: GetElem? instance : GetElem? (IndexMap α β) α β (fun m a => a ∈ m) where diff --git a/lakefile.lean b/lakefile.lean index 5fc864600..0ee2dafd7 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -8,7 +8,7 @@ import Lake open Lake DSL open System (FilePath) -require verso from git "https://github.com/leanprover/verso.git"@"main" +require verso from "../leandoc" -- git "https://github.com/leanprover/verso.git"@"tutorials" package "verso-manual" where -- building the C code cost much more than the optimizations save @@ -283,3 +283,10 @@ end ExplanationPreprocessing lean_exe "generate-manual" where needs := #[`@/figures, `@/subversoExtractMod] root := `Main + +@[default_target] +lean_lib Tutorial where + +@[default_target] +lean_exe "generate-tutorials" where + root := `TutorialMain From 9610596149c1de156f7c273d5f38dcd25857a010 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 17 Nov 2025 19:08:26 +0100 Subject: [PATCH 02/45] wip: tutorials --- Main.lean | 2 +- lakefile.lean | 24 ++++++++++++++++++++++++ 2 files changed, 25 insertions(+), 1 deletion(-) diff --git a/Main.lean b/Main.lean index 101e07047..b26a41c45 100644 --- a/Main.lean +++ b/Main.lean @@ -40,7 +40,7 @@ where extraFiles := [("static", "static")], extraHead := #[plausible, staticJs, staticCss], emitTeX := false, - emitHtmlSingle := .immediately, -- for proofreading + emitHtmlSingle := .no, logo := some "/static/lean_logo.svg", sourceLink := some "https://github.com/leanprover/reference-manual", issueLink := some "https://github.com/leanprover/reference-manual/issues", diff --git a/lakefile.lean b/lakefile.lean index 0ee2dafd7..0649ff7fe 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -290,3 +290,27 @@ lean_lib Tutorial where @[default_target] lean_exe "generate-tutorials" where root := `TutorialMain + +def lakeExe (prog : String) (args : Array String) : IO Unit := do + IO.println s!"Running {prog} with args {args}" + -- Using spawn and wait here causes the process to inherit stdio streams from Lake, so output is immediately visible + let code ← IO.Process.Child.wait <| (← IO.Process.spawn { cmd := "lake", args := #["--quiet", "exe", prog] ++ args }) + if code ≠ 0 then + let code' := code.toUInt8 + let code := if code' ≠ 0 then code' else 1 + IO.eprintln s!"Failed to run {prog} with args {args}" + IO.Process.exit code + + +script generate args := do + if !args.isEmpty then + IO.eprintln "No args expected" + return 1 + + lakeExe "generate-manual" #["--depth", "2", "--verbose", "--delay-html-multi", "multi.json"] + lakeExe "generate-tutorials" #["--verbose", "--delay", "tutorials.json"] + lakeExe "generate-manual" #["--resume-html-multi", "multi.json"] + lakeExe "generate-tutorials" #["--resume", "tutorials.json"] + + + return 0 From a2f6505c9673e2c1dea9467b0a011b8379cd6b5b Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 10 Dec 2025 10:46:49 +0100 Subject: [PATCH 03/45] bump --- lake-manifest.json | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 680981665..1849d4690 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,21 +1,18 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/verso.git", - "type": "git", - "subDir": null, + [{"type": "path", "scope": "", - "rev": "795bc01672b6f616aeaa24a7c7c4b32b20fe9c04", "name": "verso", "manifestFile": "lake-manifest.json", - "inputRev": "main", "inherited": false, + "dir": "../leandoc", "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "", - "rev": "ec4a54b5308c1f46b4b52a9c62fb67d193aa0972", + "rev": "74835c84b38e4070b8240a063c6417c767e551ae", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +32,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "519b262cfc93634f904c9fb0992a45377ee49a9d", + "rev": "eb77622e97e942ba2cfe02f60637705fc2d9481b", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", From 2304fe9afb3f00ba50616bd98cf81301422f7ed3 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 10 Dec 2025 16:38:12 +0100 Subject: [PATCH 04/45] Fix ambiguous tech terms --- Manual.lean | 2 +- Manual/BuildTools/Lake/CLI.lean | 2 +- Manual/Defs.lean | 2 +- Manual/Elaboration.lean | 6 +++--- Manual/Grind/EMatching.lean | 2 +- Manual/IO/Threads.lean | 6 +++--- Manual/Interaction.lean | 4 ++-- Manual/Language/Namespaces.lean | 2 +- Manual/NotationsMacros.lean | 2 +- Manual/NotationsMacros/SyntaxDef.lean | 2 +- Manual/SourceFiles.lean | 6 +++--- Manual/Terms.lean | 4 ++-- Manual/Types.lean | 2 +- lake-manifest.json | 7 +++++-- lakefile.lean | 2 +- 15 files changed, 27 insertions(+), 24 deletions(-) diff --git a/Manual.lean b/Manual.lean index 88a3fbde1..0b2e30ac3 100644 --- a/Manual.lean +++ b/Manual.lean @@ -57,7 +57,7 @@ Along with many other parts of Lean, the tactic language is user-extensible, so Tactics are written in Lean itself, and can be used immediately upon definition; rebuilding the prover or loading external modules is not required. Lean is also a pure *functional programming language*, with features such as a run-time system based on reference counting that can efficiently work with packed array structures, multi-threading, and monadic {name}`IO`. -As befits a programming language, Lean is primarily implemented in itself, including the language server, build tool, {tech}[elaborator], and tactic system. +As befits a programming language, Lean is primarily implemented in itself, including the language server, build tool, {tech (key := "Lean elaborator") -normalize}[elaborator], and tactic system. This very book is written in [Verso](https://github.com/leanprover/verso), a documentation authoring tool written in Lean. Familiarity with Lean's programming features is valuable even for users whose primary interest is in writing proofs, because Lean programs are used to implement new tactics and proof automation. diff --git a/Manual/BuildTools/Lake/CLI.lean b/Manual/BuildTools/Lake/CLI.lean index 3a0ca23a4..6ccad489b 100644 --- a/Manual/BuildTools/Lake/CLI.lean +++ b/Manual/BuildTools/Lake/CLI.lean @@ -308,7 +308,7 @@ Single-character flags cannot be combined; `-HR` is not equivalent to `-H -R`. : {lakeOptDef flag}`--reconfigure` or {lakeOptDef flag}`-R` - Normally, the {tech}[package configuration] file is {tech (key := "elaborator")}[elaborated] when a package is first configured, with the result cached to a {tech}[`.olean` file] that is used for future invocations until the package configuration + Normally, the {tech}[package configuration] file is {tech (key := "elaborator") -normalize}[elaborated] when a package is first configured, with the result cached to a {tech}[`.olean` file] that is used for future invocations until the package configuration Providing this flag causes the configuration file to be re-elaborated. : {lakeOptDef flag}`--keep-toolchain` diff --git a/Manual/Defs.lean b/Manual/Defs.lean index 61a7addbc..47534097e 100644 --- a/Manual/Defs.lean +++ b/Manual/Defs.lean @@ -30,7 +30,7 @@ The following commands in Lean are definition-like: {TODO}[Render commands as th * {keyword}`theorem` * {keyword}`opaque` -All of these commands cause Lean to {tech (key := "elaborator")}[elaborate] a term based on a {tech}[signature]. +All of these commands cause Lean to {tech (key := "elaborator") -normalize}[elaborate] a term based on a {tech}[signature]. With the exception of {keywordOf Lean.Parser.Command.example}`example`, which discards the result, the resulting expression in Lean's core language is saved for future use in the environment. The {keywordOf Lean.Parser.Command.declaration}`instance` command is described in the {ref "instance-declarations"}[section on instance declarations]. diff --git a/Manual/Elaboration.lean b/Manual/Elaboration.lean index b4bafb8d5..9f88f13bf 100644 --- a/Manual/Elaboration.lean +++ b/Manual/Elaboration.lean @@ -37,7 +37,7 @@ Roughly speaking, Lean's processing of a source file can be divided into the fol : Elaboration - {deftech (key := "elaborator")}[Elaboration] is the process of transforming Lean's user-facing syntax into its core type theory. + {deftech (key := "Lean elaborator") -normalize}[Elaboration] is the process of transforming Lean's user-facing syntax into its core type theory. This core theory is much simpler, enabling the trusted kernel to be very small. Elaboration additionally produces metadata, such as proof states or the types of expressions, used for Lean's interactive features, storing them in a side table. @@ -103,7 +103,7 @@ tag := "macro-and-elab" %%% Having parsed a command, the next step is to elaborate it. -The precise meaning of {deftech}_elaboration_ depends on what is being elaborated: elaborating a command effects a change in the state of Lean, while elaborating a term results in a term in Lean's core type theory. +The precise meaning of {deftech -normalize}_elaboration_ depends on what is being elaborated: elaborating a command effects a change in the state of Lean, while elaborating a term results in a term in Lean's core type theory. Elaboration of both commands and terms may be recursive, both because of command combinators such as {keywordOf Lean.Parser.Command.in}`in` and because terms may contain other terms. Command and term elaboration have different capabilities. @@ -290,7 +290,7 @@ The compiler stores an intermediate representation in an environment extension. For straightforwardly structurally recursive functions, the translation will use the type's recursor. These functions tend to be relatively efficient when run in the kernel, their defining equations hold definitionally, and they are easy to understand. -Functions that use other patterns of recursion that cannot be captured by the type's recursor are translated using {deftech}[well-founded recursion], which is structural recursion on a proof that some {deftech}_measure_ decreases at each recursive call, or using {ref "partial-fixpoint"}[partial fixpoints], which logically capture at least part of a function's specification by appealing to domain-theoretic constructions. +Functions that use other patterns of recursion that cannot be captured by the type's recursor are translated using {tech}[well-founded recursion], which is structural recursion on a proof that some {tech}[measure] decreases at each recursive call, or using {ref "partial-fixpoint"}[partial fixpoints], which logically capture at least part of a function's specification by appealing to domain-theoretic constructions. Lean can automatically derive many of these termination proofs, but some require manual proofs. Well-founded recursion is more flexible, but the resulting functions are often slower to execute in the kernel due to the proof terms that show that a measure decreases, and their defining equations may hold only propositionally. To provide a uniform interface to functions defined via structural and well-founded recursion and to check its own correctness, the elaborator proves {deftech}[equational lemmas] that relate the function to its original definition. diff --git a/Manual/Grind/EMatching.lean b/Manual/Grind/EMatching.lean index b1ae2e31a..849eeec2c 100644 --- a/Manual/Grind/EMatching.lean +++ b/Manual/Grind/EMatching.lean @@ -31,7 +31,7 @@ Each fact added to the whiteboard by E-matching is referred to as an {deftech (k Annotating theorems for E-matching, thus adding them to the index, is essential for enabling {tactic}`grind` to make effective use of a library. In addition to user-specified theorems, {tactic}`grind` uses automatically generated equations for {keywordOf Lean.Parser.Term.match}`match`-expressions as E-matching theorems. -Behind the scenes, the {tech}[elaborator] generates auxiliary functions that implement pattern matches, along with equational theorems that specify their behavior. +Behind the scenes, the {tech (key := "Lean elaborator")}[elaborator] generates auxiliary functions that implement pattern matches, along with equational theorems that specify their behavior. Using these equations with E-matching enables {tactic}`grind` to reduce these instances of pattern matching. diff --git a/Manual/IO/Threads.lean b/Manual/IO/Threads.lean index e0429d443..3e726f8ae 100644 --- a/Manual/IO/Threads.lean +++ b/Manual/IO/Threads.lean @@ -30,7 +30,7 @@ variable {α : Type u} ``` {deftech}_Tasks_ are the fundamental primitive for writing multi-threaded code. -A {lean}`Task α` represents a computation that, at some point, will {deftech}_resolve_ to a value of type `α`; it may be computed on a separate thread. +A {lean}`Task α` represents a computation that, at some point, will {tech (key := "resolve promise")}_resolve_ to a value of type `α`; it may be computed on a separate thread. When a task has resolved, its value can be read; attempting to get the value of a task before it resolves causes the current thread to block until the task has resolved. Tasks are similar to promises in JavaScript, `JoinHandle` in Rust, and `Future` in Scala. @@ -52,7 +52,7 @@ Tasks may be explicitly cancelled using {name}`IO.cancel`. The Lean runtime maintains a thread pool for running tasks. The size of the thread pool is determined by the environment variable {envVar +def}`LEAN_NUM_THREADS` if it is set, or by the number of logical processors on the current machine otherwise. The size of the thread pool is not a hard limit; in certain situations it may be exceeded to avoid deadlocks. -By default, these threads are used to run tasks; each task has a {deftech}_priority_ ({name}`Task.Priority`), and higher-priority tasks take precedence over lower-priority tasks. +By default, these threads are used to run tasks; each task has a {deftech (key := "task priority")}_priority_ ({name}`Task.Priority`), and higher-priority tasks take precedence over lower-priority tasks. Tasks may also be assigned to dedicated threads by spawning them with a sufficiently high priority. {docstring Task (label := "type") +hideStructureConstructor +hideFields} @@ -162,7 +162,7 @@ Pure tasks are terminated automatically upon cancellation. # Promises Promises represent a value that will be supplied in the future. -Supplying the value is called {deftech (key := "resolve")}_resolving_ the promise. +Supplying the value is called {deftech (key := "resolve promise")}_resolving_ the promise. Once created, a promise can be stored in a data structure or passed around like any other value, and attempts to read from it will block until it is resolved. diff --git a/Manual/Interaction.lean b/Manual/Interaction.lean index 5eacac46b..2ee3d92ac 100644 --- a/Manual/Interaction.lean +++ b/Manual/Interaction.lean @@ -28,7 +28,7 @@ Lean's interactive features are based on a different paradigm. Rather than a separate command prompt outside of the program, Lean provides {tech}[commands] for accomplishing the same tasks in the context of a source file. By convention, commands that are intended for interactive use rather than as part of a durable code artifact are prefixed with {keyword}`#`. -Information from Lean commands is available in the {deftech}_message log_, which accumulates output from the {tech}[elaborator]. +Information from Lean commands is available in the {deftech}_message log_, which accumulates output from the {tech (key := "Lean elaborator")}[elaborator]. Each entry in the message log is associated with a specific source range and has a {deftech}_severity_. There are three severities: {lean (type := "Lean.MessageSeverity")}`information` is used for messages that do not indicate a problem, {lean (type := "Lean.MessageSeverity")}`warning` indicates a potential problem, and {lean (type := "Lean.MessageSeverity")}`error` indicates a definite problem. For interactive commands, results are typically returned as informational messages that are associated with the command's leading keyword. @@ -56,7 +56,7 @@ Use {keywordOf Lean.reduceCmd}`#reduce` to instead reduce terms using the reduct ::: -{keywordOf Lean.Parser.Command.eval}`#eval` always {tech (key := "elaborator")}[elaborates] and compiles the provided term. +{keywordOf Lean.Parser.Command.eval}`#eval` always {tech (key := "Lean elaborator")}[elaborates] and compiles the provided term. It then checks whether the term transitively depends on any uses of {lean}`sorry`, in which case evaluation is terminated unless the command was invoked as {keywordOf Lean.Parser.Command.eval}`#eval!`. This is because compiled code may rely on compile-time invariants (such as array lookups being in-bounds) that are ensured by proofs of suitable statements, and running code that contains incomplete proofs (or uses of {lean}`sorry` that “prove” incorrect statements) can cause Lean itself to crash. diff --git a/Manual/Language/Namespaces.lean b/Manual/Language/Namespaces.lean index 1831c8e0f..ddc50f86e 100644 --- a/Manual/Language/Namespaces.lean +++ b/Manual/Language/Namespaces.lean @@ -65,7 +65,7 @@ end Forest # Namespaces and Section Scopes -Every {tech}[section scope] has a {deftech}_current namespace_, which is determined by the {keywordOf Lean.Parser.Command.namespace}`namespace` command.{margin}[The {keywordOf Lean.Parser.Command.namespace}`namespace` command is described in the {ref "scope-commands"}[section on commands that introduce section scopes].] +Every {tech}[section scope] has a {tech}[current namespace], which is determined by the {keywordOf Lean.Parser.Command.namespace}`namespace` command.{margin}[The {keywordOf Lean.Parser.Command.namespace}`namespace` command is described in the {ref "scope-commands"}[section on commands that introduce section scopes].] Names that are declared within the section scope are added to the current namespace. If the declared name has more than one component, then its namespace is nested within the current namespace; the body of the declaration's current namespace is the nested namespace. Section scopes also include a set of {deftech}_opened namespaces_, which are namespaces whose contents are in scope without additional qualification. diff --git a/Manual/NotationsMacros.lean b/Manual/NotationsMacros.lean index 1d9ef44f2..b382745a6 100644 --- a/Manual/NotationsMacros.lean +++ b/Manual/NotationsMacros.lean @@ -62,7 +62,7 @@ They can be combined flexibly to achieve the necessary results: tag := "macros" %%% -{deftech}_Macros_ are transformations from {name Lean.Syntax}`Syntax` to {name Lean.Syntax}`Syntax` that occur during {tech (key := "elaborator")}[elaboration] and during {ref "tactic-macros"}[tactic execution]. +{deftech}_Macros_ are transformations from {name Lean.Syntax}`Syntax` to {name Lean.Syntax}`Syntax` that occur during {tech (key := "elaborator") -normalize}[elaboration] and during {ref "tactic-macros"}[tactic execution]. Replacing syntax with the result of transforming it with a macro is called {deftech}_macro expansion_. Multiple macros may be associated with a single {tech}[syntax kind], and they are attempted in order of definition. Macros are run in a {tech}[monad] that has access to some compile-time metadata and has the ability to either emit an error message or to delegate to subsequent macros, but the macro monad is much less powerful than the elaboration monads. diff --git a/Manual/NotationsMacros/SyntaxDef.lean b/Manual/NotationsMacros/SyntaxDef.lean index ac0254495..a49070594 100644 --- a/Manual/NotationsMacros/SyntaxDef.lean +++ b/Manual/NotationsMacros/SyntaxDef.lean @@ -718,7 +718,7 @@ A variant of list literals that requires double square brackets and allows a tra syntax "[[" term,*,? "]]" : term ``` -Adding a {deftech}[macro] that describes how to translate it into an ordinary list literal allows it to be used in tests. +Adding a {tech}[macro] that describes how to translate it into an ordinary list literal allows it to be used in tests. ```lean macro_rules | `(term|[[$e:term,*]]) => `([$e,*]) diff --git a/Manual/SourceFiles.lean b/Manual/SourceFiles.lean index 42bb62c3f..6b9a5425c 100644 --- a/Manual/SourceFiles.lean +++ b/Manual/SourceFiles.lean @@ -17,7 +17,7 @@ tag := "files" htmlSplit := .never %%% -The smallest unit of compilation in Lean is a single {deftech}[source file]. +The smallest unit of compilation in Lean is a single {tech}[source file]. Source files may import other source files based on their file names. In other words, the names and folder structures of files are significant in Lean code. @@ -642,7 +642,7 @@ tag := "meta-phase" Definitions in Lean result in both a representation in the type theory that is designed for formal reasoning and a compiled representation that is designed for execution. This compiled representation is used to generate machine code, but it can also be executed directly using an interpreter. -The code runs during {tech}[elaboration], such as {ref "tactics"}[tactics] or {ref "macros"}[macros], is the compiled form of definitions. +The code runs during {tech -normalize}[elaboration], such as {ref "tactics"}[tactics] or {ref "macros"}[macros], is the compiled form of definitions. If this compiled representation changes, then any code created by it may no longer be up to date, and it must be re-run. Because the compiler performs non-trivial optimizations, changes to any definition in the transitive dependency chain of a function could in principle invalidate its compiled representation. This means that metaprograms exported by modules induce a much stronger coupling than ordinary definitions. @@ -863,7 +863,7 @@ tag := "code-distribution" %%% -Lean modules are organized into {deftech}_packages_, which are units of code distribution. +Lean modules are organized into {tech}_packages_, which are units of code distribution. A {tech}[package] may contain multiple libraries or executables. Code in a package that is intended for use by other Lean packages is organized into {deftech (key:="library")}[libraries]. diff --git a/Manual/Terms.lean b/Manual/Terms.lean index ba511755a..9958d3e94 100644 --- a/Manual/Terms.lean +++ b/Manual/Terms.lean @@ -28,7 +28,7 @@ tag := "terms" {deftech}_Terms_ are the principal means of writing mathematics and programs in Lean. -The {tech}[elaborator] translates them to Lean's minimal core language, which is then checked by the kernel and compiled for execution. +The {deftech (key := "Lean elaborator")}[elaborator] translates them to Lean's minimal core language, which is then checked by the kernel and compiled for execution. The syntax of terms is {ref "syntax-ext"}[arbitrarily extensible]; this chapter documents the term syntax that Lean provides out-of-the-box. # Identifiers @@ -410,7 +410,7 @@ Implicit parameters come in three varieties: : Instance implicit parameters - Arguments for {deftech}_instance implicit_ parameters are found via {ref "instance-synth"}[type class synthesis]. + Arguments for {tech}_instance implicit_ parameters are found via {ref "instance-synth"}[type class synthesis]. Instance implicit parameters are written in square brackets (`[` and `]`). Unlike the other kinds of implicit parameter, instance implicit parameters that are written without a `:` specify the parameter's type rather than providing a name. Furthermore, only a single name is allowed. diff --git a/Manual/Types.lean b/Manual/Types.lean index 1c1b49ccb..6939b5f99 100644 --- a/Manual/Types.lean +++ b/Manual/Types.lean @@ -24,7 +24,7 @@ shortContextTitle := "Type System" %%% {deftech}_Terms_, also known as {deftech}_expressions_, are the fundamental units of meaning in Lean's core language. -They are produced from user-written syntax by the {tech}[elaborator]. +They are produced from user-written syntax by the {tech (key := "Lean elaborator")}[elaborator]. Lean's type system relates terms to their _types_, which are also themselves terms. Types can be thought of as denoting sets, while terms denote individual elements of these sets. A term is {deftech}_well-typed_ if it has a type under the rules of Lean's type theory. diff --git a/lake-manifest.json b/lake-manifest.json index 1849d4690..c079a12ad 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,12 +1,15 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"type": "path", + [{"url": "https://github.com/leanprover/verso.git", + "type": "git", + "subDir": null, "scope": "", + "rev": "bcc253c7f2bfa288acfcb1617ffb3b1511bb98e2", "name": "verso", "manifestFile": "lake-manifest.json", + "inputRev": "tutorials", "inherited": false, - "dir": "../leandoc", "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", diff --git a/lakefile.lean b/lakefile.lean index 0649ff7fe..1760605d3 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -8,7 +8,7 @@ import Lake open Lake DSL open System (FilePath) -require verso from "../leandoc" -- git "https://github.com/leanprover/verso.git"@"tutorials" +require verso from git "https://github.com/leanprover/verso.git"@"tutorials" package "verso-manual" where -- building the C code cost much more than the optimizations save From 95c690a90cc2cc14b1ab72db58e6a97f8f3b7f7c Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 12 Dec 2025 11:55:55 +0100 Subject: [PATCH 05/45] progress --- TutorialMain.lean | 2 +- lake-manifest.json | 2 +- lakefile.lean | 16 +++++++++++----- 3 files changed, 13 insertions(+), 7 deletions(-) diff --git a/TutorialMain.lean b/TutorialMain.lean index e1eac3294..ffd388e65 100644 --- a/TutorialMain.lean +++ b/TutorialMain.lean @@ -49,4 +49,4 @@ def tutorials : Tutorials where ] def main := - tutorialsMain tutorials (config := {remoteConfigFile := "tutorial-remotes.json", destination := "_tutorial-out"}) + tutorialsMain tutorials (config := {destination := "_tutorial-out"}) diff --git a/lake-manifest.json b/lake-manifest.json index c079a12ad..c8c897ab5 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "bcc253c7f2bfa288acfcb1617ffb3b1511bb98e2", + "rev": "26224a9fda56c34bff3a63ecc82e8ee754c5ac86", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "tutorials", diff --git a/lakefile.lean b/lakefile.lean index 1760605d3..1369e9c50 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -306,11 +306,17 @@ script generate args := do if !args.isEmpty then IO.eprintln "No args expected" return 1 - - lakeExe "generate-manual" #["--depth", "2", "--verbose", "--delay-html-multi", "multi.json"] - lakeExe "generate-tutorials" #["--verbose", "--delay", "tutorials.json"] - lakeExe "generate-manual" #["--resume-html-multi", "multi.json"] - lakeExe "generate-tutorials" #["--resume", "tutorials.json"] + let outDir : FilePath := "_out" + let siteDir := outDir / "site" + + lakeExe "generate-manual" #["--depth", "2", "--verbose", "--delay-html-multi", "multi.json", "--remote-config", "verso-sources.json"] + lakeExe "generate-tutorials" #["--verbose", "--delay", "tutorials.json", "--remote-config", "verso-sources.json"] + lakeExe "generate-manual" #["--verbose", "--resume-html-multi", "multi.json", "--remote-config", "verso-sources.json"] + lakeExe "generate-tutorials" #["--verbose", "--resume", "tutorials.json", "--remote-config", "verso-sources.json"] + IO.FS.createDirAll siteDir + IO.FS.writeFile (siteDir / "index.html") (← IO.FS.readFile (("test-data" : FilePath) / "index.html")) + discard <| IO.Process.run { cmd := "cp", args := #["-r", "_out/html-multi", (siteDir / "reference").toString] } + discard <| IO.Process.run { cmd := "cp", args := #["-r", "_tutorial-out", (siteDir / "tutorials").toString] } return 0 From f0536aefe36a620562d0dbba6f60eeb59f0ec4a4 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 12 Dec 2025 15:04:57 +0100 Subject: [PATCH 06/45] Working cross-links --- lake-manifest.json | 2 +- lakefile.lean | 14 ++++++++------ reference-remotes.json | 12 ++++++++++++ tutorial-remotes.json | 12 ++++++++++++ 4 files changed, 33 insertions(+), 7 deletions(-) create mode 100644 reference-remotes.json create mode 100644 tutorial-remotes.json diff --git a/lake-manifest.json b/lake-manifest.json index c8c897ab5..716e9e338 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "26224a9fda56c34bff3a63ecc82e8ee754c5ac86", + "rev": "5834aca69fd494cdc0d0dee4b12649ad321ef537", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "tutorials", diff --git a/lakefile.lean b/lakefile.lean index 1369e9c50..3128d6a04 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -309,14 +309,16 @@ script generate args := do let outDir : FilePath := "_out" let siteDir := outDir / "site" - lakeExe "generate-manual" #["--depth", "2", "--verbose", "--delay-html-multi", "multi.json", "--remote-config", "verso-sources.json"] - lakeExe "generate-tutorials" #["--verbose", "--delay", "tutorials.json", "--remote-config", "verso-sources.json"] - lakeExe "generate-manual" #["--verbose", "--resume-html-multi", "multi.json", "--remote-config", "verso-sources.json"] - lakeExe "generate-tutorials" #["--verbose", "--resume", "tutorials.json", "--remote-config", "verso-sources.json"] + lakeExe "generate-manual" #["--depth", "2", "--verbose", "--delay-html-multi", "multi.json", "--remote-config", "reference-remotes.json"] + lakeExe "generate-tutorials" #["--verbose", "--delay", "tutorials.json", "--remote-config", "tutorial-remotes.json"] + lakeExe "generate-manual" #["--verbose", "--resume-html-multi", "multi.json", "--remote-config", "reference-remotes.json"] + lakeExe "generate-tutorials" #["--verbose", "--resume", "tutorials.json", "--remote-config", "tutorial-remotes.json"] IO.FS.createDirAll siteDir + IO.FS.createDirAll <| siteDir / "reference" + IO.FS.createDirAll <| siteDir / "tutorials" IO.FS.writeFile (siteDir / "index.html") (← IO.FS.readFile (("test-data" : FilePath) / "index.html")) - discard <| IO.Process.run { cmd := "cp", args := #["-r", "_out/html-multi", (siteDir / "reference").toString] } - discard <| IO.Process.run { cmd := "cp", args := #["-r", "_tutorial-out", (siteDir / "tutorials").toString] } + discard <| IO.Process.run { cmd := "cp", args := #["-r", "_out/html-multi/", (siteDir / "reference/").toString] } + discard <| IO.Process.run { cmd := "cp", args := #["-r", "_tutorial-out/", (siteDir / "tutorials/").toString] } return 0 diff --git a/reference-remotes.json b/reference-remotes.json new file mode 100644 index 000000000..cf78b67f8 --- /dev/null +++ b/reference-remotes.json @@ -0,0 +1,12 @@ +{ + "version": 0, + "sources": { + "tutorials": { + "root": "/tutorials", + "shortName": "tutorials", + "longName": "Lean Tutorials", + "updateFrequency": "always", + "sources": [{"local": "_tutorial-out/xref.json"}] + } + } +} diff --git a/tutorial-remotes.json b/tutorial-remotes.json new file mode 100644 index 000000000..414b63692 --- /dev/null +++ b/tutorial-remotes.json @@ -0,0 +1,12 @@ +{ + "version": 0, + "sources": { + "reference": { + "root": "/reference", + "updateFrequency": "always", + "shortName": "ref", + "longName": "Lean Language Reference", + "sources": [{"local": "_out/html-multi/xref.json"}, "default"] + } + } +} From f3356610983b28e746a40a13993913ece1e33320 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 12 Dec 2025 16:54:09 +0100 Subject: [PATCH 07/45] Better deploy for PRs --- lake-manifest.json | 2 +- lakefile.lean | 22 ---- test-data/index.html | 103 ++++++++++++++++++ .../reference-remotes.json | 0 .../tutorial-remotes.json | 0 5 files changed, 104 insertions(+), 23 deletions(-) create mode 100644 test-data/index.html rename reference-remotes.json => test-data/reference-remotes.json (100%) rename tutorial-remotes.json => test-data/tutorial-remotes.json (100%) diff --git a/lake-manifest.json b/lake-manifest.json index 716e9e338..504ce4f19 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "5834aca69fd494cdc0d0dee4b12649ad321ef537", + "rev": "e195c57713a2736fcaf7aa7caeed8d7c1e5f3050", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "tutorials", diff --git a/lakefile.lean b/lakefile.lean index 3128d6a04..09bc01a4c 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -300,25 +300,3 @@ def lakeExe (prog : String) (args : Array String) : IO Unit := do let code := if code' ≠ 0 then code' else 1 IO.eprintln s!"Failed to run {prog} with args {args}" IO.Process.exit code - - -script generate args := do - if !args.isEmpty then - IO.eprintln "No args expected" - return 1 - let outDir : FilePath := "_out" - let siteDir := outDir / "site" - - lakeExe "generate-manual" #["--depth", "2", "--verbose", "--delay-html-multi", "multi.json", "--remote-config", "reference-remotes.json"] - lakeExe "generate-tutorials" #["--verbose", "--delay", "tutorials.json", "--remote-config", "tutorial-remotes.json"] - lakeExe "generate-manual" #["--verbose", "--resume-html-multi", "multi.json", "--remote-config", "reference-remotes.json"] - lakeExe "generate-tutorials" #["--verbose", "--resume", "tutorials.json", "--remote-config", "tutorial-remotes.json"] - IO.FS.createDirAll siteDir - IO.FS.createDirAll <| siteDir / "reference" - IO.FS.createDirAll <| siteDir / "tutorials" - IO.FS.writeFile (siteDir / "index.html") (← IO.FS.readFile (("test-data" : FilePath) / "index.html")) - discard <| IO.Process.run { cmd := "cp", args := #["-r", "_out/html-multi/", (siteDir / "reference/").toString] } - discard <| IO.Process.run { cmd := "cp", args := #["-r", "_tutorial-out/", (siteDir / "tutorials/").toString] } - - - return 0 diff --git a/test-data/index.html b/test-data/index.html new file mode 100644 index 000000000..f303f728c --- /dev/null +++ b/test-data/index.html @@ -0,0 +1,103 @@ + + + + + + Lean Manual + + + + +
+

Lean Manual Testing

+

Preview Version

+
+ Reference Manual + Tutorials +
+
+ + diff --git a/reference-remotes.json b/test-data/reference-remotes.json similarity index 100% rename from reference-remotes.json rename to test-data/reference-remotes.json diff --git a/tutorial-remotes.json b/test-data/tutorial-remotes.json similarity index 100% rename from tutorial-remotes.json rename to test-data/tutorial-remotes.json From 10fe3ab76da995255ee263403a25f57ad8e27c9e Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 15 Dec 2025 12:34:54 +0100 Subject: [PATCH 08/45] Missing header --- Tutorial.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Tutorial.lean b/Tutorial.lean index 9d2f83520..6f892783b 100644 --- a/Tutorial.lean +++ b/Tutorial.lean @@ -1,2 +1,7 @@ +/- +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 Tutorial.VCGen import Tutorial.Grind.IndexMap From a458c50fd43d94439b20372a01d5f6543e9a4e7b Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 15 Dec 2025 14:09:58 +0100 Subject: [PATCH 09/45] Add sources --- verso-sources.json | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 verso-sources.json diff --git a/verso-sources.json b/verso-sources.json new file mode 100644 index 000000000..226486252 --- /dev/null +++ b/verso-sources.json @@ -0,0 +1,19 @@ +{ + "version": 0, + "sources": { + "reference": { + "root": "/reference", + "shortName": "reference", + "longName": "The Lean Language Reference", + "updateFrequency": "always", + "sources": [{"local": "_out/html-multi/xref.json"}] + }, + "tutorials": { + "root": "/tutorials", + "shortName": "tutorials", + "longName": "Lean Tutorials", + "updateFrequency": "always", + "sources": [{"local": "_tutorial-out/xref.json"}] + } + } +} From 0ab8f066048c2759afe9e8b4d2eb3fb9ddc3e7b8 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 15 Dec 2025 17:28:28 +0100 Subject: [PATCH 10/45] Update scripts --- .github/workflows/ci.yml | 11 ++- ...production-remotes-reference.json.template | 12 +++ ...production-remotes-tutorials.json.template | 12 +++ generate.sh | 94 +++++++++++++++++++ 4 files changed, 124 insertions(+), 5 deletions(-) create mode 100644 config/production-remotes-reference.json.template create mode 100644 config/production-remotes-tutorials.json.template create mode 100755 generate.sh diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 62be29763..1fc7dc533 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -155,12 +155,13 @@ jobs: - name: Generate HTML (non-release) if: github.event_name != 'release' run: | - lake --quiet exe generate-manual --depth 2 --with-word-count "words.txt" --verbose --without-html-single + ./generate.sh --mode preview - name: Generate HTML (release) if: github.event_name == 'release' run: | - lake --quiet exe generate-manual --depth 2 --with-word-count "words.txt" --verbose --without-html-single + VERSION=${GITHUB_REF#refs/tags/v} + ./generate.sh --mode production --version "$VERSION" - name: Check Manual Examples are Isolated run: | @@ -170,7 +171,7 @@ jobs: if: github.event_name == 'pull_request' id: generate run: | - lake --quiet exe generate-manual --depth 2 --verbose --draft --without-html-single --output "_out/draft" + ./generate.sh --mode preview --draft --output "_out/draft-site" - name: Report status to Lean PR if: always() && github.repository == 'leanprover/reference-manual' @@ -222,7 +223,7 @@ jobs: - name: Run LinkChecker (local links only) if: github.event_name == 'push' || github.event_name == 'pull_request' run: | - linkchecker --config=.linkchecker/linkcheckerrc './_out/html-multi/' + linkchecker --config=.linkchecker/linkcheckerrc './_out/site/' # This saved number is used by a workflow_run trigger. It # manages labels that indicate the status of the built HTML. @@ -282,7 +283,7 @@ jobs: uses: nwtgck/actions-netlify@v2.0 if: github.event_name == 'release' with: - publish-dir: _out/html-multi + publish-dir: _out/site/reference production-branch: main production-deploy: true github-token: ${{ secrets.GITHUB_TOKEN }} diff --git a/config/production-remotes-reference.json.template b/config/production-remotes-reference.json.template new file mode 100644 index 000000000..8aef1ccdf --- /dev/null +++ b/config/production-remotes-reference.json.template @@ -0,0 +1,12 @@ +{ + "version": 0, + "sources": { + "tutorials": { + "root": "/doc/tutorials/__VERSION__", + "shortName": "tutorials", + "longName": "Lean Tutorials", + "updateFrequency": "always", + "sources": [{"local": "_tutorial-out/xref.json"}] + } + } +} diff --git a/config/production-remotes-tutorials.json.template b/config/production-remotes-tutorials.json.template new file mode 100644 index 000000000..1f03aa81e --- /dev/null +++ b/config/production-remotes-tutorials.json.template @@ -0,0 +1,12 @@ +{ + "version": 0, + "sources": { + "reference": { + "root": "/doc/reference/__VERSION__", + "updateFrequency": "always", + "shortName": "ref", + "longName": "Lean Language Reference", + "sources": [{"local": "_out/html-multi/xref.json"}, "default"] + } + } +} diff --git a/generate.sh b/generate.sh new file mode 100755 index 000000000..66455762b --- /dev/null +++ b/generate.sh @@ -0,0 +1,94 @@ +#!/usr/bin/env bash +set -euo pipefail + +# Generate the manual and tutorials with support for preview and production modes + +# Default values +MODE="preview" +VERSION="" +OUTPUT="_out/site" +DRAFT_FLAG="" + +# Parse arguments +while [[ $# -gt 0 ]]; do + case $1 in + --mode) + MODE="$2" + shift 2 + ;; + --version) + VERSION="$2" + shift 2 + ;; + --output) + OUTPUT="$2" + shift 2 + ;; + --draft) + DRAFT_FLAG="--draft" + shift + ;; + *) + echo "Unknown option: $1" + echo "Usage: $0 [--mode preview|production] [--version VERSION] [--output DIR] [--draft]" + exit 1 + ;; + esac +done + +# Validate production mode requirements +if [ "$MODE" = "production" ]; then + if [ -z "$VERSION" ]; then + echo "Error: --version required for production mode" + exit 1 + fi + if [ -n "$DRAFT_FLAG" ]; then + echo "Error: --draft not supported in production mode" + exit 1 + fi +fi + +# Set up remote configs based on mode +if [ "$MODE" = "preview" ]; then + REF_REMOTE_CONFIG="test-data/reference-remotes.json" + TUT_REMOTE_CONFIG="test-data/tutorial-remotes.json" +else + # Production mode: generate temporary configs from templates + REF_REMOTE_CONFIG="_build/production-remotes-reference.json" + TUT_REMOTE_CONFIG="_build/production-remotes-tutorials.json" + + # Replace __VERSION__ in templates and write to temporary files + mkdir -p _build + sed "s/__VERSION__/$VERSION/g" config/production-remotes-reference.json.template > "$REF_REMOTE_CONFIG" + sed "s/__VERSION__/$VERSION/g" config/production-remotes-tutorials.json.template > "$TUT_REMOTE_CONFIG" + + echo "Generated production configs with version $VERSION" +fi + +# Generate the manual and tutorials +echo "Running generate-manual with args --depth 2 --verbose --delay-html-multi multi.json --remote-config $REF_REMOTE_CONFIG --with-word-count words.txt $DRAFT_FLAG" +lake --quiet exe generate-manual --depth 2 --verbose --delay-html-multi multi.json --remote-config "$REF_REMOTE_CONFIG" --with-word-count "words.txt" $DRAFT_FLAG + +echo "Running generate-tutorials with args --verbose --delay tutorials.json --remote-config $TUT_REMOTE_CONFIG $DRAFT_FLAG" +lake --quiet exe generate-tutorials --verbose --delay tutorials.json --remote-config "$TUT_REMOTE_CONFIG" $DRAFT_FLAG + +echo "Running generate-manual with args --verbose --resume-html-multi multi.json --remote-config $REF_REMOTE_CONFIG $DRAFT_FLAG" +lake --quiet exe generate-manual --verbose --resume-html-multi multi.json --remote-config "$REF_REMOTE_CONFIG" $DRAFT_FLAG + +echo "Running generate-tutorials with args --verbose --resume tutorials.json --remote-config $TUT_REMOTE_CONFIG $DRAFT_FLAG" +lake --quiet exe generate-tutorials --verbose --resume tutorials.json --remote-config "$TUT_REMOTE_CONFIG" $DRAFT_FLAG + +# Set up output directories +echo "Setting up output directories" +mkdir -p "$OUTPUT/reference" +mkdir -p "$OUTPUT/tutorials" + +# Copy files +echo "Copying files to site directory" +if [ "$MODE" = "preview" ]; then + cp test-data/index.html "$OUTPUT/index.html" +fi +cp -r _out/html-multi/ "$OUTPUT/reference/" +cp -r _tutorial-out/ "$OUTPUT/tutorials/" + +echo "Done! Site generated at $OUTPUT/" From 0d8f23e7ae25beb6853f0b3c6d8171f0f0068410 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 15 Dec 2025 17:36:06 +0100 Subject: [PATCH 11/45] No draft flag for tutorials --- generate.sh | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/generate.sh b/generate.sh index 66455762b..f44d272fa 100755 --- a/generate.sh +++ b/generate.sh @@ -69,14 +69,14 @@ fi echo "Running generate-manual with args --depth 2 --verbose --delay-html-multi multi.json --remote-config $REF_REMOTE_CONFIG --with-word-count words.txt $DRAFT_FLAG" lake --quiet exe generate-manual --depth 2 --verbose --delay-html-multi multi.json --remote-config "$REF_REMOTE_CONFIG" --with-word-count "words.txt" $DRAFT_FLAG -echo "Running generate-tutorials with args --verbose --delay tutorials.json --remote-config $TUT_REMOTE_CONFIG $DRAFT_FLAG" -lake --quiet exe generate-tutorials --verbose --delay tutorials.json --remote-config "$TUT_REMOTE_CONFIG" $DRAFT_FLAG +echo "Running generate-tutorials with args --verbose --delay tutorials.json --remote-config $TUT_REMOTE_CONFIG" +lake --quiet exe generate-tutorials --verbose --delay tutorials.json --remote-config "$TUT_REMOTE_CONFIG" echo "Running generate-manual with args --verbose --resume-html-multi multi.json --remote-config $REF_REMOTE_CONFIG $DRAFT_FLAG" lake --quiet exe generate-manual --verbose --resume-html-multi multi.json --remote-config "$REF_REMOTE_CONFIG" $DRAFT_FLAG -echo "Running generate-tutorials with args --verbose --resume tutorials.json --remote-config $TUT_REMOTE_CONFIG $DRAFT_FLAG" -lake --quiet exe generate-tutorials --verbose --resume tutorials.json --remote-config "$TUT_REMOTE_CONFIG" $DRAFT_FLAG +echo "Running generate-tutorials with args --verbose --resume tutorials.json --remote-config $TUT_REMOTE_CONFIG" +lake --quiet exe generate-tutorials --verbose --resume tutorials.json --remote-config "$TUT_REMOTE_CONFIG" # Set up output directories echo "Setting up output directories" From 378192bad49b94316a2910464a3d9f74115db51a Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 15 Dec 2025 17:53:45 +0100 Subject: [PATCH 12/45] Try checking links with server --- .github/workflows/ci.yml | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1fc7dc533..56f8c612e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -223,7 +223,20 @@ jobs: - name: Run LinkChecker (local links only) if: github.event_name == 'push' || github.event_name == 'pull_request' run: | - linkchecker --config=.linkchecker/linkcheckerrc './_out/site/' + # Start a local web server in the background for link checking + cd _out/site + python3 -m http.server 8877 & + SERVER_PID=$! + cd ../.. + + # Wait for server to start + sleep 2 + + # Run linkchecker against the local server + linkchecker --config=.linkchecker/linkcheckerrc 'http://localhost:8877/' + + # Stop the server + kill $SERVER_PID || true # This saved number is used by a workflow_run trigger. It # manages labels that indicate the status of the built HTML. From 388bb04a421591cb47ba2c8ad712fb058618cb60 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 15 Dec 2025 18:03:50 +0100 Subject: [PATCH 13/45] fixes --- .github/workflows/ci.yml | 3 ++- generate.sh | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 56f8c612e..9d102e7f8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -224,8 +224,9 @@ jobs: if: github.event_name == 'push' || github.event_name == 'pull_request' run: | # Start a local web server in the background for link checking + # Suppress server errors (connection resets from parallel requests) cd _out/site - python3 -m http.server 8877 & + python3 -m http.server 8877 2>/dev/null & SERVER_PID=$! cd ../.. diff --git a/generate.sh b/generate.sh index f44d272fa..7fa824583 100755 --- a/generate.sh +++ b/generate.sh @@ -88,7 +88,7 @@ echo "Copying files to site directory" if [ "$MODE" = "preview" ]; then cp test-data/index.html "$OUTPUT/index.html" fi -cp -r _out/html-multi/ "$OUTPUT/reference/" -cp -r _tutorial-out/ "$OUTPUT/tutorials/" +cp -r _out/html-multi/* "$OUTPUT/reference/" +cp -r _tutorial-out/* "$OUTPUT/tutorials/" echo "Done! Site generated at $OUTPUT/" From 2ce693522eaae8ab7a25c905cb965335909da381 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 15 Dec 2025 22:33:53 +0100 Subject: [PATCH 14/45] bump --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 2d8e667cf..7dc538ccd 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "84fecb1face7e417cd3da73aba6a3e36907c7fa2", + "rev": "42dcc7abf0af1572c951bdfc3c152d79ebcb0f71", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "tutorials", From c80268351af40d9ab969a269fdf0822ad81e3e9b Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 15 Dec 2025 22:55:11 +0100 Subject: [PATCH 15/45] bump --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 7dc538ccd..e754a1e7c 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "42dcc7abf0af1572c951bdfc3c152d79ebcb0f71", + "rev": "2af0a3aa6f193b4baa8d4b91ec5a51e2bc1e8813", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "tutorials", From c30023da5dd7acdf528a1f3cb4675eaab12de1e8 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 16 Dec 2025 05:53:41 +0100 Subject: [PATCH 16/45] trailing slashes --- test-data/index.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test-data/index.html b/test-data/index.html index f303f728c..dde409989 100644 --- a/test-data/index.html +++ b/test-data/index.html @@ -95,8 +95,8 @@

Lean Manual Testing

Preview Version

- Reference Manual - Tutorials + Reference Manual + Tutorials
From 3189ef1832c5c2fefdf9a1c900f9e726ffac051e Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 16 Dec 2025 06:16:50 +0100 Subject: [PATCH 17/45] See if more threads makes linkchecker faster against local server --- .github/workflows/ci.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 9d102e7f8..64678c973 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -233,8 +233,8 @@ jobs: # Wait for server to start sleep 2 - # Run linkchecker against the local server - linkchecker --config=.linkchecker/linkcheckerrc 'http://localhost:8877/' + # Run linkchecker + linkchecker --config=.linkchecker/linkcheckerrc --threads=30 'http://localhost:8877/' # Stop the server kill $SERVER_PID || true From d507a197fb1cfbb1ad3a711b25a45f9bb676c636 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 16 Dec 2025 06:35:20 +0100 Subject: [PATCH 18/45] Output locations and proselint --- generate.sh | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/generate.sh b/generate.sh index 7fa824583..87e1f432a 100755 --- a/generate.sh +++ b/generate.sh @@ -65,15 +65,24 @@ else echo "Generated production configs with version $VERSION" fi +# Set up output locations based on draft mode +if [ -n "$DRAFT_FLAG" ]; then + MANUAL_OUTPUT_FLAG="--output _out/draft" + REF_SOURCE="_out/draft/html-multi" +else + MANUAL_OUTPUT_FLAG="" + REF_SOURCE="_out/html-multi" +fi + # Generate the manual and tutorials -echo "Running generate-manual with args --depth 2 --verbose --delay-html-multi multi.json --remote-config $REF_REMOTE_CONFIG --with-word-count words.txt $DRAFT_FLAG" -lake --quiet exe generate-manual --depth 2 --verbose --delay-html-multi multi.json --remote-config "$REF_REMOTE_CONFIG" --with-word-count "words.txt" $DRAFT_FLAG +echo "Running generate-manual with args --depth 2 --verbose --delay-html-multi multi.json --remote-config $REF_REMOTE_CONFIG --with-word-count words.txt $MANUAL_OUTPUT_FLAG $DRAFT_FLAG" +lake --quiet exe generate-manual --depth 2 --verbose --delay-html-multi multi.json --remote-config "$REF_REMOTE_CONFIG" --with-word-count "words.txt" $MANUAL_OUTPUT_FLAG $DRAFT_FLAG echo "Running generate-tutorials with args --verbose --delay tutorials.json --remote-config $TUT_REMOTE_CONFIG" lake --quiet exe generate-tutorials --verbose --delay tutorials.json --remote-config "$TUT_REMOTE_CONFIG" -echo "Running generate-manual with args --verbose --resume-html-multi multi.json --remote-config $REF_REMOTE_CONFIG $DRAFT_FLAG" -lake --quiet exe generate-manual --verbose --resume-html-multi multi.json --remote-config "$REF_REMOTE_CONFIG" $DRAFT_FLAG +echo "Running generate-manual with args --verbose --resume-html-multi multi.json --remote-config $REF_REMOTE_CONFIG $MANUAL_OUTPUT_FLAG $DRAFT_FLAG" +lake --quiet exe generate-manual --verbose --resume-html-multi multi.json --remote-config "$REF_REMOTE_CONFIG" $MANUAL_OUTPUT_FLAG $DRAFT_FLAG echo "Running generate-tutorials with args --verbose --resume tutorials.json --remote-config $TUT_REMOTE_CONFIG" lake --quiet exe generate-tutorials --verbose --resume tutorials.json --remote-config "$TUT_REMOTE_CONFIG" @@ -88,7 +97,7 @@ echo "Copying files to site directory" if [ "$MODE" = "preview" ]; then cp test-data/index.html "$OUTPUT/index.html" fi -cp -r _out/html-multi/* "$OUTPUT/reference/" +cp -r "$REF_SOURCE"/* "$OUTPUT/reference/" cp -r _tutorial-out/* "$OUTPUT/tutorials/" echo "Done! Site generated at $OUTPUT/" From 160762f491ad52d547f14f4d5cd56c3426f50bdc Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 16 Dec 2025 08:56:37 +0100 Subject: [PATCH 19/45] Better text --- test-data/index.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test-data/index.html b/test-data/index.html index dde409989..20f8ce60c 100644 --- a/test-data/index.html +++ b/test-data/index.html @@ -92,7 +92,7 @@
-

Lean Manual Testing

+

Lean Reference Manual and Tutorials

Preview Version

Reference Manual From a8fcee8fb7ef35c2ba6a66db6016e63ed95225fb Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 16 Dec 2025 08:56:42 +0100 Subject: [PATCH 20/45] Try to speed up server --- .github/workflows/ci.yml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 64678c973..f746d671a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -223,15 +223,16 @@ jobs: - name: Run LinkChecker (local links only) if: github.event_name == 'push' || github.event_name == 'pull_request' run: | - # Start a local web server in the background for link checking - # Suppress server errors (connection resets from parallel requests) - cd _out/site - python3 -m http.server 8877 2>/dev/null & + # Download miniserve (fast Rust-based static file server) + curl -sL https://github.com/svenstaro/miniserve/releases/download/v0.27.1/miniserve-0.27.1-x86_64-unknown-linux-gnu -o miniserve + chmod +x miniserve + + # Start miniserve in the background + ./miniserve _out/site --port 8877 --index index.html 2>/dev/null & SERVER_PID=$! - cd ../.. # Wait for server to start - sleep 2 + sleep 1 # Run linkchecker linkchecker --config=.linkchecker/linkcheckerrc --threads=30 'http://localhost:8877/' From 2025eadc59c83486ae4f43839453cf07546db8fc Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 16 Dec 2025 10:32:22 +0100 Subject: [PATCH 21/45] Try other link checker now that there's a server --- .github/workflows/ci.yml | 67 ++++++++++++++++++++------------------ .linkchecker/linkcheckerrc | 4 +++ 2 files changed, 39 insertions(+), 32 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f746d671a..4cfbf6dd6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -208,38 +208,6 @@ jobs: cat words.txt >> $GITHUB_STEP_SUMMARY echo "\`\`\`" >> $GITHUB_STEP_SUMMARY - - name: Set up Python for link checker - if: github.event_name == 'push' || github.event_name == 'pull_request' - uses: actions/setup-python@v4 - with: - python-version: '3.10' - - - name: Install LinkChecker - if: github.event_name == 'push' || github.event_name == 'pull_request' - run: | - python -m pip install --upgrade pip - pip install linkchecker - - - name: Run LinkChecker (local links only) - if: github.event_name == 'push' || github.event_name == 'pull_request' - run: | - # Download miniserve (fast Rust-based static file server) - curl -sL https://github.com/svenstaro/miniserve/releases/download/v0.27.1/miniserve-0.27.1-x86_64-unknown-linux-gnu -o miniserve - chmod +x miniserve - - # Start miniserve in the background - ./miniserve _out/site --port 8877 --index index.html 2>/dev/null & - SERVER_PID=$! - - # Wait for server to start - sleep 1 - - # Run linkchecker - linkchecker --config=.linkchecker/linkcheckerrc --threads=30 'http://localhost:8877/' - - # Stop the server - kill $SERVER_PID || true - # This saved number is used by a workflow_run trigger. It # manages labels that indicate the status of the built HTML. - name: Save PR number @@ -413,3 +381,38 @@ jobs: run: | cd _out/html-multi/-verso-search tsc --noEmit -p jsconfig.json + + link-check: + name: Check local links + runs-on: ubuntu-latest + needs: [build] + if: github.event_name == 'push' || github.event_name == 'pull_request' + steps: + - uses: actions/checkout@v4 + + - name: Get generated HTML from artifact storage + uses: actions/download-artifact@v4 + with: + name: 'html' + path: '_out/' + + - name: Start HTTP server + run: | + # Start HTTP server in the background + python3 -m http.server 8877 --directory _out/site 2>/dev/null & + echo $! > server.pid + + # Wait for server to start + sleep 2 + + - name: Run linkcheck + uses: filiph/linkcheck@2.0.23 + with: + arguments: http://localhost:8877/ + + - name: Stop HTTP server + if: always() + run: | + if [ -f server.pid ]; then + kill $(cat server.pid) || true + fi diff --git a/.linkchecker/linkcheckerrc b/.linkchecker/linkcheckerrc index 0cd632270..00cfc342b 100644 --- a/.linkchecker/linkcheckerrc +++ b/.linkchecker/linkcheckerrc @@ -1,2 +1,6 @@ [filtering] ignorewarnings=url-content-too-large,url-too-long + +[checking] +# No rate limiting for localhost +maxrequestspersecond=0 From c93a4c3a940b7d87842e466aab5396c3f0ef7e09 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 16 Dec 2025 10:41:55 +0100 Subject: [PATCH 22/45] context --- .github/workflows/ci.yml | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4cfbf6dd6..00e7da18d 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -396,23 +396,24 @@ jobs: name: 'html' path: '_out/' - - name: Start HTTP server + - name: Set up Dart + uses: dart-lang/setup-dart@v1 + + - name: Install linkcheck + run: dart pub global activate linkcheck + + - name: Run linkcheck run: | # Start HTTP server in the background python3 -m http.server 8877 --directory _out/site 2>/dev/null & - echo $! > server.pid + SERVER_PID=$! # Wait for server to start sleep 2 - - name: Run linkcheck - uses: filiph/linkcheck@2.0.23 - with: - arguments: http://localhost:8877/ + # Run linkcheck as a CLI tool instead of using filiph/linkcheck action + # because the action runs in isolation and can't reach our local HTTP server + linkcheck http://localhost:8877/ - - name: Stop HTTP server - if: always() - run: | - if [ -f server.pid ]; then - kill $(cat server.pid) || true - fi + # Stop the server + kill $SERVER_PID || true From a0bf5c71099071aa44e4120ac5b2e4bebeb3e93c Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 16 Dec 2025 10:49:28 +0100 Subject: [PATCH 23/45] cleanup differently --- .github/workflows/ci.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 00e7da18d..082fc3ca1 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -408,12 +408,12 @@ jobs: python3 -m http.server 8877 --directory _out/site 2>/dev/null & SERVER_PID=$! + # Ensure server is stopped on exit + trap "kill $SERVER_PID 2>/dev/null || true" EXIT + # Wait for server to start sleep 2 # Run linkcheck as a CLI tool instead of using filiph/linkcheck action # because the action runs in isolation and can't reach our local HTTP server linkcheck http://localhost:8877/ - - # Stop the server - kill $SERVER_PID || true From 21f1c27f3ae40af522fbcbc913ebf0234df9e987 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 16 Dec 2025 10:50:49 +0100 Subject: [PATCH 24/45] No cleanup needed --- .github/workflows/ci.yml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 082fc3ca1..62f2597e6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -406,10 +406,6 @@ jobs: run: | # Start HTTP server in the background python3 -m http.server 8877 --directory _out/site 2>/dev/null & - SERVER_PID=$! - - # Ensure server is stopped on exit - trap "kill $SERVER_PID 2>/dev/null || true" EXIT # Wait for server to start sleep 2 @@ -417,3 +413,5 @@ jobs: # Run linkcheck as a CLI tool instead of using filiph/linkcheck action # because the action runs in isolation and can't reach our local HTTP server linkcheck http://localhost:8877/ + + # GitHub Actions will automatically clean up the background server when this step completes From a78a7d87378dabb7160a2a1e964fedbda993df79 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 16 Dec 2025 11:18:25 +0100 Subject: [PATCH 25/45] Try linkchecker again --- .github/workflows/ci.yml | 28 ++++++++++++++++------------ .linkchecker/linkcheckerrc | 4 ++-- 2 files changed, 18 insertions(+), 14 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 62f2597e6..606e4cec6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -389,6 +389,9 @@ jobs: if: github.event_name == 'push' || github.event_name == 'pull_request' steps: - uses: actions/checkout@v4 + with: + sparse-checkout: | + .linkchecker - name: Get generated HTML from artifact storage uses: actions/download-artifact@v4 @@ -396,22 +399,23 @@ jobs: name: 'html' path: '_out/' - - name: Set up Dart - uses: dart-lang/setup-dart@v1 + - name: Set up Python + uses: actions/setup-python@v4 + with: + python-version: '3.10' - - name: Install linkcheck - run: dart pub global activate linkcheck + - name: Install LinkChecker + run: | + python -m pip install --upgrade pip + pip install linkchecker - - name: Run linkcheck + - name: Run LinkChecker (local links only) run: | - # Start HTTP server in the background - python3 -m http.server 8877 --directory _out/site 2>/dev/null & + # Start custom HTTP server that sends LinkChecker header to bypass rate limiting + python3 .linkchecker/server.py 8877 _out/site 2>/dev/null & # Wait for server to start sleep 2 - # Run linkcheck as a CLI tool instead of using filiph/linkcheck action - # because the action runs in isolation and can't reach our local HTTP server - linkcheck http://localhost:8877/ - - # GitHub Actions will automatically clean up the background server when this step completes + # Run linkchecker with high rate limit (enabled by LinkChecker header) + linkchecker --config=.linkchecker/linkcheckerrc --threads=30 'http://localhost:8877/' diff --git a/.linkchecker/linkcheckerrc b/.linkchecker/linkcheckerrc index 00cfc342b..3510f13ed 100644 --- a/.linkchecker/linkcheckerrc +++ b/.linkchecker/linkcheckerrc @@ -2,5 +2,5 @@ ignorewarnings=url-content-too-large,url-too-long [checking] -# No rate limiting for localhost -maxrequestspersecond=0 +# High rate limit enabled by LinkChecker response header from server +maxrequestspersecond=100 From fc6f48bfd2c924998cac3b40740686b34188eb1e Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 16 Dec 2025 11:25:50 +0100 Subject: [PATCH 26/45] server dbg --- .github/workflows/ci.yml | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 606e4cec6..023e115ca 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -412,10 +412,22 @@ jobs: - name: Run LinkChecker (local links only) run: | # Start custom HTTP server that sends LinkChecker header to bypass rate limiting - python3 .linkchecker/server.py 8877 _out/site 2>/dev/null & - - # Wait for server to start - sleep 2 + python3 .linkchecker/server.py 8877 _out/site & + SERVER_PID=$! + + # Wait for server to start and verify it's responding + echo "Waiting for server to start..." + for i in {1..10}; do + if curl -s http://localhost:8877/ > /dev/null 2>&1; then + echo "Server is ready" + break + fi + if [ $i -eq 10 ]; then + echo "Server failed to start" + exit 1 + fi + sleep 1 + done # Run linkchecker with high rate limit (enabled by LinkChecker header) linkchecker --config=.linkchecker/linkcheckerrc --threads=30 'http://localhost:8877/' From 6f5d9dc0646dd4e8644e7b7b4f3d271596d9ead7 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 16 Dec 2025 11:31:02 +0100 Subject: [PATCH 27/45] Missing server --- .linkchecker/server.py | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 .linkchecker/server.py diff --git a/.linkchecker/server.py b/.linkchecker/server.py new file mode 100644 index 000000000..f50e8ae8b --- /dev/null +++ b/.linkchecker/server.py @@ -0,0 +1,23 @@ +#!/usr/bin/env python3 +""" +Simple HTTP server that adds a LinkChecker header to allow unlimited request rate. +""" +import http.server +import sys + +class LinkCheckerHTTPRequestHandler(http.server.SimpleHTTPRequestHandler): + def end_headers(self): + # Add LinkChecker header to allow maxrequestspersecond > 10 + self.send_header('LinkChecker', 'allowed') + super().end_headers() + +if __name__ == '__main__': + port = int(sys.argv[1]) if len(sys.argv) > 1 else 8877 + directory = sys.argv[2] if len(sys.argv) > 2 else '.' + + import os + os.chdir(directory) + + with http.server.HTTPServer(('', port), LinkCheckerHTTPRequestHandler) as httpd: + print(f"Serving at port {port} with LinkChecker header enabled") + httpd.serve_forever() From b8e94967ad911b82bd96775ee348ecedadd952ac Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 16 Dec 2025 11:38:45 +0100 Subject: [PATCH 28/45] No more junk on console --- .github/workflows/ci.yml | 20 ++++---------------- 1 file changed, 4 insertions(+), 16 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 023e115ca..606e4cec6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -412,22 +412,10 @@ jobs: - name: Run LinkChecker (local links only) run: | # Start custom HTTP server that sends LinkChecker header to bypass rate limiting - python3 .linkchecker/server.py 8877 _out/site & - SERVER_PID=$! - - # Wait for server to start and verify it's responding - echo "Waiting for server to start..." - for i in {1..10}; do - if curl -s http://localhost:8877/ > /dev/null 2>&1; then - echo "Server is ready" - break - fi - if [ $i -eq 10 ]; then - echo "Server failed to start" - exit 1 - fi - sleep 1 - done + python3 .linkchecker/server.py 8877 _out/site 2>/dev/null & + + # Wait for server to start + sleep 2 # Run linkchecker with high rate limit (enabled by LinkChecker header) linkchecker --config=.linkchecker/linkcheckerrc --threads=30 'http://localhost:8877/' From 7b22ddd5f126db6f22fcc4991e4ca2403b8f80d3 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 16 Dec 2025 11:41:08 +0100 Subject: [PATCH 29/45] don't overwhelm dev server --- .github/workflows/ci.yml | 4 ++-- .linkchecker/linkcheckerrc | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 606e4cec6..41530f076 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -417,5 +417,5 @@ jobs: # Wait for server to start sleep 2 - # Run linkchecker with high rate limit (enabled by LinkChecker header) - linkchecker --config=.linkchecker/linkcheckerrc --threads=30 'http://localhost:8877/' + # Run linkchecker with moderate concurrency to avoid overwhelming Python's simple HTTP server + linkchecker --config=.linkchecker/linkcheckerrc --threads=10 'http://localhost:8877/' diff --git a/.linkchecker/linkcheckerrc b/.linkchecker/linkcheckerrc index 3510f13ed..0e8d40256 100644 --- a/.linkchecker/linkcheckerrc +++ b/.linkchecker/linkcheckerrc @@ -2,5 +2,5 @@ ignorewarnings=url-content-too-large,url-too-long [checking] -# High rate limit enabled by LinkChecker response header from server -maxrequestspersecond=100 +# Moderate rate limit for localhost - higher values overwhelm Python's simple HTTP server +maxrequestspersecond=30 From 410b9da70ab85b2d68039a49d30ebd52519a5625 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 16 Dec 2025 11:52:34 +0100 Subject: [PATCH 30/45] Less thread --- .github/workflows/ci.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 41530f076..6d8c1f921 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -417,5 +417,5 @@ jobs: # Wait for server to start sleep 2 - # Run linkchecker with moderate concurrency to avoid overwhelming Python's simple HTTP server - linkchecker --config=.linkchecker/linkcheckerrc --threads=10 'http://localhost:8877/' + # Run linkchecker with low concurrency to avoid overwhelming Python's single-threaded HTTP server + linkchecker --config=.linkchecker/linkcheckerrc --threads=5 'http://localhost:8877/' From 34ce921f39ab66af127e358d168958db71fcd572 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 17 Dec 2025 16:16:59 +0100 Subject: [PATCH 31/45] working lean-lang CSS --- Tutorial/Meta/Theme.lean | 366 +++++++++++++++++++++++++++++++++++++++ TutorialMain.lean | 195 ++++++++++++++++++++- lake-manifest.json | 34 ++-- lakefile.lean | 2 + 4 files changed, 581 insertions(+), 16 deletions(-) create mode 100644 Tutorial/Meta/Theme.lean diff --git a/Tutorial/Meta/Theme.lean b/Tutorial/Meta/Theme.lean new file mode 100644 index 000000000..e1668d10a --- /dev/null +++ b/Tutorial/Meta/Theme.lean @@ -0,0 +1,366 @@ +import VersoBlog +import VersoWeb.Theme + +import VersoWeb.Components.Footer +import VersoWeb.Components.NavBar + +open Verso Genre Blog Output Html Multi +open Web Components Theme + +namespace LeanLangOrg + +/-- +Default footer configuration with all standard links +-/ +def footer : FooterConfig := { + columns := #[ + -- Get Started column + { + heading := "Get Started" + headingId := some "get-started" + ariaLabel := some "LEAN" + items := #[ + { title := "Install", url := "/install" }, + { title := "Learn", url := "/learn" }, + { title := "Community", url := "/community" }, + { title := "Reservoir", url := "https://reservoir.lean-lang.org/", blank := true } + ] + }, + -- Documentation column + { + heading := "Documentation" + headingId := some "documentation" + ariaLabel := some "Documentation" + items := #[ + { title := "Language reference", url := "/doc/reference/latest/" }, + { title := "Lean API", url := "/doc/api/" }, + { title := "Use cases", url := "/use-cases" }, + { title := "Cite Lean", url := "/learn#how-to-cite-lean" } + ] + }, + -- Resources column + { + heading := "Resources" + headingId := some "resources" + ariaLabel := some "Resources" + items := #[ + { title := "Lean playground", url := "https://live.lean-lang.org/?from=lean", blank := true }, + { title := "VS Code extension", url := "https://marketplace.visualstudio.com/items?itemName=leanprover.lean4", blank := true }, + { title := "Loogle", url := "https://loogle.lean-lang.org/", blank := true }, + { title := "Mathlib", url := "https://github.com/leanprover-community/mathlib4", blank := true } + ] + }, + -- FRO column + { + heading := "FRO" + headingId := some "fro" + ariaLabel := some "FRO" + items := #[ + { title := "Vision", url := "/fro" }, + { title := "Team", url := "/fro/team" }, + { title := "Roadmap", url := "/fro/roadmap/y3" }, + { title := "Contact", url := "/fro/contact" } + ] + }, + -- Policies column + { + heading := "Policies" + headingId := some "policies" + ariaLabel := some "Policies" + items := #[ + { title := "Privacy Policy", url := "/privacy" }, + { title := "Terms of Use", url := "/terms" }, + { title := "Lean Trademark Policy", url := "/trademark-policy" } + ] + } + ] + socialLinks := #[ + { url := "https://bsky.app/profile/lean-lang.org", icon := Icon.blueskyLogo, ariaLabel := some "Bluesky" }, + { url := "https://www.linkedin.com/company/lean-fro", icon := Icon.linkedinLogo, ariaLabel := some "LinkedIn" }, + { url := "https://functional.cafe/@leanprover", icon := Icon.mastodonLogo, ariaLabel := some "Mastodon" }, + { url := "https://x.com/leanprover", icon := Icon.xLogo, ariaLabel := some "X (Twitter)" }, + { url := "https://leanprover.zulipchat.com/", icon := Icon.zulipLogo, ariaLabel := some "Zulip" }, + { url := "https://github.com/leanprover/", icon := Icon.githubLogo, ariaLabel := some "GitHub" } + ] + copyrightText := "© 2025 Lean FRO. All rights reserved." + showThemeSwitcher := true +} + +/-- +Helper to create FRO home navigation item +-/ +def navFroItem (path : Path) : NavBarItem := + { title := .text false "Home" + , url := some "/fro" + , active := path == #["fro"] } + +/-- +Function to get all the items that redirect to pages. +-/ +def getPageItems : TemplateM (Array NavBarItem) := do + let links ← Verso.Web.Util.getDirLinks + return links.map fun (active, url, title) => { title, url, active } + +def isFro (path : Path) : Bool := path[0]?.isEqSome "fro" + +/-- +Build NavBarConfig for FRO section +-/ +def buildFroNavBarConfig : TemplateM NavBarConfig := do + let leftItems ← getPageItems + let path ← currentPath + + let froPathItems (path : Path) : Array NavBarItem := #[ + { title := .text false "About", url := some "/fro/about", active := path == #["fro", "about"] }, + { title := .text false "Team", url := some "/fro/team", active := path == #["fro", "team"] }, + { title := .text false "Roadmap", url := some "/fro/roadmap", active := path == #["fro", "roadmap"] }, + { title := .text false "Contact", url := some "/fro/contact", active := path == #["fro", "contact"] } + ] + + let externalLinks : Array NavBarItem := #[ + { title := .text false "Playground", url := some "https://live.lean-lang.org/?from=lean", blank := true }, + { title := .text false "Reservoir", url := some "https://reservoir.lean-lang.org/", blank := true } + ] + + let rightItems : Array NavBarItem := #[ + { title := Icon.moon, alt := some "Change Theme", classes := some "change-theme" }, + { title := Icon.github, alt := some "Github", url := some "https://github.com/leanprover/lean4", blank := true } + ] + + let menuItems := #[navFroItem path] ++ froPathItems path + + return { + leftItems := leftItems + rightItems := rightItems + menuItems := menuItems + externalLinks := externalLinks + subNavBar := if isFro path then some (SubNavBarConfig.mk (froPathItems path)) else none + } + +def socialMeta : SocialMeta := + { title := "Lean Programming Language", + description := "Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code.", + image := "https://lean-lang.org/static/png/banner.png", + url := "https://lean-lang.org", + siteName := "Lean Language", + alt := "Lean Programming Language", + articleCreator := "@leanprover", + } + +def headConfig : HeadConfig := + { description := socialMeta.description, + faviconWhite := "https://lean-lang.org/static/favicon-light.ico", + faviconDark := "https://lean-lang.org/static/favicon-dark.ico", + appleTouchIcon := "https://lean-lang.org/static/apple-touch-icon.png", + color := "#3D6AC9" + } + +/-- +Default theme configuration with all design tokens +-/ +def colorTheme : ThemeConfig := { + variables := [ + -- Typography + { name := "font-primary", value := "'Open Sans', Arial, sans-serif" }, + { name := "font-secondary", value := "'Oranienbaum', serif" }, + { name := "fs-xs", value := "0.75rem" }, + { name := "fs-sm", value := "0.875rem" }, + { name := "fs-base", value := "1rem" }, + { name := "fs-md", value := "17px" }, + { name := "fs-lg", value := "1.25rem" }, + { name := "fs-xl", value := "2rem" }, + { name := "fs-2xl", value := "3.3rem" }, + + -- Spacing + { name := "space-1", value := "0.25rem" }, + { name := "space-2", value := "0.5rem" }, + { name := "space-3", value := "0.75rem" }, + { name := "space-4", value := "1rem" }, + { name := "space-5", value := "1.25rem" }, + { name := "space-6", value := "1.5rem" }, + { name := "space-8", value := "2rem" }, + { name := "space-10", value := "2.5rem" }, + { name := "space-12", value := "3rem" }, + { name := "space-13", value := "3.5rem" }, + { name := "space-14", value := "4rem" }, + { name := "space-16", value := "5rem" }, + + -- Semantic spacing + { name := "gap-sm", value := "var(--space-2)" }, + { name := "gap-md", value := "10px" }, + { name := "gap-lg", value := "30px" }, + { name := "gap-xl", value := "100px" }, + + -- Section padding + { name := "section-padding", value := "var(--space-10)" }, + { name := "section-padding-top", value := "var(--space-16)" }, + + -- Border Radius + { name := "radius-sm", value := "0.25rem" }, + { name := "radius-md", value := "0.5rem" }, + { name := "radius-lg", value := "1rem" }, + { name := "radius-pill", value := "9999px" }, + + -- Sizes + { name := "container-width", value := "1240px" }, + { name := "logo-size", value := "1.25rem" }, + { name := "logo-footer-size", value := "60px" }, + { name := "icon-size", value := "64px" }, + + -- Layout + { name := "nav-padding-y", value := "var(--space-6)" }, + { name := "nav-padding-x", value := "10vw" }, + { name := "nav-height", value := "calc(var(--nav-padding-y) * 2 + 2em)" }, + + -- Transitions + { name := "transition-fast", value := "0.2s" }, + { name := "transition-base", value := "0.3s" }, + { name := "transition-slow", value := "0.6s" }, + { name := "transition-delay-none", value := "0s" }, + { name := "transition-delay-small", value := "0.05s" }, + { name := "transition-delay-medium", value := "0.1s" }, + { name := "transition-delay-large", value := "0.15s" }, + + -- Animation + { name := "animation-delay", value := "10000ms" }, + + -- Z-Index + { name := "z-below", value := "-1" }, + { name := "z-normal", value := "0" }, + { name := "z-above", value := "1" }, + { name := "z-header", value := "1000" }, + + -- Colors + { name := "color-surface", value := "#fff" }, + { name := "color-primary", value := "#386EE0" }, + { name := "color-primary-focus", value := "#1D4ED8" }, + { name := "color-primary-light", value := "#4a90e2" }, + { name := "color-secondary", value := "#607D8B" }, + { name := "color-text", value := "#333" }, + { name := "color-text-contrast", value := "white" }, + { name := "color-text-light", value := "#64748b" }, + { name := "color-muted", value := "#607D8B" }, + { name := "color-bg", value := "#F9FBFD" }, + { name := "color-bg-translucent", value := "rgba(249, 251, 253, 0.81)" }, + { name := "color-white", value := "#fff" }, + { name := "color-border", value := "#E4EBF3" }, + { name := "color-border-nav", value := "#E4EBF3" }, + { name := "color-border-light", value := "#D1D9E2" }, + { name := "color-hover", value := "rgba(56, 110, 224, 0.08)" }, + { name := "color-link-hover", value := "#0073e6" }, + { name := "color-shadow", value := "rgba(35, 55, 139, 0.1)" }, + + -- Components + { name := "btn-bg", value := "var(--color-primary)" }, + { name := "btn-text", value := "var(--color-white)" }, + { name := "btn-font", value := "var(--font-primary)" }, + { name := "btn-radius", value := "var(--radius-md)" }, + + -- Card specific + { name := "card-bg", value := "var(--color-white)" }, + { name := "card-border", value := "var(--color-border-light)" }, + + -- Testimonial specific + { name := "testimonial-bg", value := "var(--color-primary)" }, + { name := "testimonial-text", value := "var(--color-white)" } + ], + + darkVariables := [ + + -- Dark theme color overrides + { name := "color-surface", value := "#121212" }, + { name := "color-primary", value := "#3b94ff" }, + { name := "color-primary-focus", value := "#669df6" }, + { name := "color-primary-light", value := "#6aadfe" }, + { name := "color-secondary", value := "#aabfc9" }, + { name := "color-text", value := "#eee" }, + { name := "color-text-light", value := "#bbb" }, + { name := "color-text-contrast", value := "white" }, + { name := "color-muted", value := "#90a4ae" }, + { name := "color-bg", value := "#181818" }, + { name := "color-bg-translucent", value := "rgba(24, 24, 24, 0.85)" }, + { name := "color-white", value := "#1e1e1e" }, + { name := "color-border", value := "#333" }, + { name := "color-border-nav", value := "#333" }, + { name := "color-border-light", value := "#444" }, + { name := "color-hover", value := "rgba(255, 255, 255, 0.08)" }, + { name := "color-link-hover", value := "#4d9efc" }, + { name := "color-shadow", value := "rgba(0, 0, 0, 0.5)" }, + + -- Component overrides + { name := "btn-bg", value := "var(--color-primary)" }, + { name := "btn-text", value := "var(--color-white)" }, + { name := "card-bg", value := "#1f1f1f" }, + { name := "card-border", value := "#2a2a2a" }, + { name := "testimonial-bg", value := "#2e3a59" }, + { name := "testimonial-text", value := "#fff" } + ] +} + +/-- +Lean-specific page type detection functions. +-/ + +def isMarkdownPage : Path → Bool + | #[] | #["fro"] | #["404"] => false + | _ => true + +def indexPage : Path → Bool + | _ => false + +def needsTitle : Path → Bool + | #["learn"] | #["install"] | #["404"] => false + | _ => true + +def isInstallPage (path : Path) : Bool := + path[0]?.isEqSome "install" + +def isUseCases : Path → Bool + | #["use-cases"] => true + | _ => false + +def isRoadmap : Path → Bool + | #["fro", "roadmap"] => true + | _ => false + +def isPagePost : Path → Bool + | #["use-cases", _] | #["fro", "roadmap", _] => true + | _ => false + + +/-- +Lean-specific post configuration. +-/ +def postConfig : PostConfig := + { hasSpecialStyling := fun path => if isFro path then some "fro" else none } + +/-- +Lean website layout configuration. +-/ +def layoutConfig : LayoutConfig := + { isMarkdownPage := isMarkdownPage, + isIndexPage := indexPage, + needsTitle := needsTitle, + isPagePost := isPagePost, + postConfig := postConfig, + hasSpecialStyling := fun path => if isFro path then some "fro" else none, + renderPostList := fun path html => + if isUseCases path then + {{
{{ html }}
}} + else + html + } + +def theme : Theme := + Verso.Web.theme + { siteName := "Lean Lang", rootTitle := "Lean enables correct, maintainable, and formally verified code", socialMeta, headConfig, variables := colorTheme } + layoutConfig + buildFroNavBarConfig + {{ + + + }} + (pure footer) diff --git a/TutorialMain.lean b/TutorialMain.lean index ffd388e65..326699515 100644 --- a/TutorialMain.lean +++ b/TutorialMain.lean @@ -5,10 +5,14 @@ Author: David Thrane Christiansen -/ import VersoTutorial +import VersoBlog import Tutorial +import Tutorial.Meta.Theme +import VersoWeb.Theme open Verso.Genre.Manual open Verso.Genre.Tutorial +open Verso.Genre.Blog (Page) open Verso.Output.Html in def plausible := {{ @@ -32,21 +36,204 @@ def staticCss := {{ }} +def version (_content : Array (Verso.Doc.Inline g)) : Verso.Doc.Inline g := .text Lean.versionString + open Verso.Doc Concrete in def tutorials : Tutorials where content := - (verso (.none) "foo" + (verso (Page) "Tutorials" ::::::: - abc + These tutorials are written for version {version}[] of Lean. :::::::).toPart topics := #[ - { title := "Tactics" + { title := #[inlines!"Tactics"], + titleString := "Tactics" description := #[blocks!"..."] tutorials := #[%doc Tutorial.VCGen, %doc Tutorial.Grind.IndexMap] } ] +open Verso.Genre.Blog Site.Syntax in +open Verso.Doc in +def leanSite : Site := + site home / + "install" install + "learn" learn + "community" community + "use-cases" «use-cases» + "fro" fro +where + placeholder title : Part Page := { title := #[.text title], titleString := title, metadata := none, content := #[], subParts := #[] } + home : VersoDoc Page := { construct := fun _ => placeholder "Lean" } + install : VersoDoc Page := { construct := fun _ => placeholder "Install" } + learn : VersoDoc Page := { construct := fun _ => placeholder "Learn" } + community : VersoDoc Page := { construct := fun _ => placeholder "Community" } + «use-cases» : VersoDoc Page := { construct := fun _ => placeholder "Use Cases" } + «trademark-policy» : VersoDoc Page := { construct := fun _ => placeholder "Trademark Policy" } + privacy : VersoDoc Page := { construct := fun _ => placeholder "Privacy" } + terms : VersoDoc Page := { construct := fun _ => placeholder "Terms" } + logos : VersoDoc Page := { construct := fun _ => placeholder "Logos" } + fro : VersoDoc Page := { construct := fun _ => placeholder "FRO" } + documentation : VersoDoc Page := { construct := fun _ => placeholder "Documentation" } + examples : VersoDoc Page :={ construct := fun _ => placeholder "Examples" } + publications : VersoDoc Page := { construct := fun _ => placeholder "Publications" } + links : VersoDoc Page := { construct := fun _ => placeholder "Links" } + people : VersoDoc Page := { construct := fun _ => placeholder "People" } + +-- open Verso.Output.Html in +-- def theme : Theme where +-- page content := do +-- let config := { logError := fun _ => pure () } +-- let ctxt := { +-- site := leanSite, +-- ctxt := { +-- config, +-- components := {}, +-- path := #["doc", "tutorials"] +-- }, +-- xref := { remoteContent := {} }, +-- linkTargets := {}, +-- dir := "", +-- config, +-- header := "" +-- } +-- let pageContent := {{
{{content.content}}
}} +-- let mut params : Verso.Genre.Blog.Template.Params := {} +-- params := params.insert "title" content.title +-- params := params.insert "content" pageContent +-- let ((html, st'), y) ← Verso.Genre.Blog.Template.renderMany [LeanLangOrg.theme.pageTemplate, LeanLangOrg.theme.primaryTemplate] params ctxt {} {} +-- pure html +-- topic := Theme.default.topic +-- tutorialToC := Theme.default.tutorialToC +-- cssFiles := Verso.Web.Theme.Static.allCSS.map fun (filename, contents) => +-- { filename := s!"theme/style/{filename}", contents } + + +def codeColors := r#" +:root { + --verso-code-color: var(--color-text) !important; +} +"# + +def localToCStyle := r#" +nav.local-toc { + position: fixed; + top: calc(var(--nav-height) + 1rem + 60px); + right: calc((100vw - var(--container-width)) / 2 - 15rem - 2rem); + width: 15rem; + font-size: 0.875rem; + max-height: calc(100vh - 2rem - var(--nav-height) - 60px); + overflow-y: auto; +} + +nav.local-toc h1 { + display: none; +} + +nav.local-toc ol { + list-style: none; + margin: 0; + padding: 0; +} + +nav.local-toc li { + margin: 0.5rem 0; +} + +nav.local-toc a { + color: var(--verso-text-color); + text-decoration: none; +} + +nav.local-toc a:hover { + color: var(--color-accent); +} + +/* On smaller screens, display normally */ +@media (max-width: 90rem) { + nav.local-toc { + position: static; + right: auto; + width: auto; + max-height: none; + border-left: 3px solid var(--color-border); + padding-left: 1rem; + margin-bottom: 1rem; + } +} + +nav.local-toc ol ol { + padding-left: 1rem; + margin-top: 0.25rem; +} + +nav.local-toc ol ol li { + margin: 0.25rem 0; +} + +/*******/ +nav.local-toc > div:first-child { + margin-bottom: 1rem; +} + +nav.local-toc h1 { + font-size: 1rem; + margin: 0 0 0.5rem 0; + font-weight: 600; +} + +nav.local-toc .code-links { + display: flex; + gap: 0.5rem; + flex-wrap: wrap; +} + +nav.local-toc .code-link { + font-size: 0.8125rem; + padding: 0.25rem 0.5rem; + border: 1px solid var(--color-border); + border-radius: 6px; + color: var(--verso-text-color); + text-decoration: none; + display: inline-block; +} + +nav.local-toc .code-link:hover { + background: var(--verso-selected-color); + border-color: var(--color-accent); +} + +nav.local-toc .code-link code { + background: none; + padding: 0; + font-size: inherit; +} + +nav.local-toc .code-link.live::before { + content: "↪ "; + margin-right: 0.25rem; +} + +nav.local-toc .code-link.download::before { + content: "📦 "; + margin-right: 0.25rem; +} +"# + + +open Verso.Genre.Blog.Template in +open Verso.Output Html in +def theme := + { LeanLangOrg.theme with + pageTemplate := do + let tutorialNav : Option Html ← param? "tutorialNav" + let content : Html ← param "content" + let content := tutorialNav.getD .empty ++ content + withTheReader Context (fun ρ => { ρ with params := ρ.params.insert "content" content }) LeanLangOrg.theme.pageTemplate + cssFiles := LeanLangOrg.theme.cssFiles.push ("code-colors.css", codeColors) |>.push ("local-toc.css", localToCStyle) + } + def main := - tutorialsMain tutorials (config := {destination := "_tutorial-out"}) + tutorialsMain tutorials (config := {destination := "_tutorial-out"}) (theme := theme) (navSite := leanSite) diff --git a/lake-manifest.json b/lake-manifest.json index e754a1e7c..fe175e6f1 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,16 +1,36 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/verso.git", + [{"url": "https://github.com/leanprover/verso-web-components", "type": "git", "subDir": null, "scope": "", - "rev": "2af0a3aa6f193b4baa8d4b91ec5a51e2bc1e8813", + "rev": "9b7146809fc91975b210eb388c43d9e09ddfb01e", + "name": "versowebcomponents", + "manifestFile": "lake-manifest.json", + "inputRev": "tutorials", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/verso.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "525de870d337366103ec48316d6c190fcbc576c7", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "tutorials", "inherited": false, "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/subverso", + "type": "git", + "subDir": null, + "scope": "", + "rev": "eb77622e97e942ba2cfe02f60637705fc2d9481b", + "name": "subverso", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, @@ -30,16 +50,6 @@ "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/subverso", - "type": "git", - "subDir": null, - "scope": "", - "rev": "eb77622e97e942ba2cfe02f60637705fc2d9481b", - "name": "subverso", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, "configFile": "lakefile.lean"}], "name": "«verso-manual»", "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index 026bcef03..cd028a861 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -9,6 +9,8 @@ open Lake DSL open System (FilePath) require verso from git "https://github.com/leanprover/verso.git"@"tutorials" +require versowebcomponents from git "https://github.com/leanprover/verso-web-components"@"tutorials" + package "verso-manual" where -- building the C code cost much more than the optimizations save From 6a3a2e60a7fe883b0562636e26d53ae5bc1581d8 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 18 Dec 2025 02:05:43 +0100 Subject: [PATCH 32/45] headers --- Tutorial/Meta/Theme.lean | 5 +++++ TutorialMain.lean | 2 +- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/Tutorial/Meta/Theme.lean b/Tutorial/Meta/Theme.lean index e1668d10a..c6a9d4175 100644 --- a/Tutorial/Meta/Theme.lean +++ b/Tutorial/Meta/Theme.lean @@ -1,3 +1,8 @@ +/- +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 VersoBlog import VersoWeb.Theme diff --git a/TutorialMain.lean b/TutorialMain.lean index 326699515..cfa888e3b 100644 --- a/TutorialMain.lean +++ b/TutorialMain.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2024 Lean FRO LLC. All rights reserved. +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 -/ From f674113d0a66f8acd034a6cc30fbb86246113a89 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 18 Dec 2025 02:07:29 +0100 Subject: [PATCH 33/45] prettier --- .github/workflows/ci.yml | 2 +- test-data/index.html | 178 ++++++++++++++++--------------- test-data/reference-remotes.json | 18 ++-- test-data/tutorial-remotes.json | 2 +- verso-sources.json | 32 +++--- 5 files changed, 117 insertions(+), 115 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a3ce7ebae..6bb8b5442 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -161,7 +161,7 @@ jobs: - name: Generate HTML (non-release) if: github.event_name != 'release' run: | - ./generate.sh --mode preview + ./generate.sh --mode preview - name: Generate HTML (release) if: github.event_name == 'release' diff --git a/test-data/index.html b/test-data/index.html index 20f8ce60c..e9eb32a31 100644 --- a/test-data/index.html +++ b/test-data/index.html @@ -1,103 +1,105 @@ - + - - - - Lean Manual - - - - -
-

Lean Reference Manual and Tutorials

-

Preview Version

-
- Reference Manual - Tutorials + + + +
+

Lean Reference Manual and Tutorials

+

Preview Version

+
+ Reference Manual + Tutorials +
-
- + diff --git a/test-data/reference-remotes.json b/test-data/reference-remotes.json index cf78b67f8..9d01e354e 100644 --- a/test-data/reference-remotes.json +++ b/test-data/reference-remotes.json @@ -1,12 +1,12 @@ { - "version": 0, - "sources": { - "tutorials": { - "root": "/tutorials", - "shortName": "tutorials", - "longName": "Lean Tutorials", - "updateFrequency": "always", - "sources": [{"local": "_tutorial-out/xref.json"}] + "version": 0, + "sources": { + "tutorials": { + "root": "/tutorials", + "shortName": "tutorials", + "longName": "Lean Tutorials", + "updateFrequency": "always", + "sources": [{ "local": "_tutorial-out/xref.json" }] + } } - } } diff --git a/test-data/tutorial-remotes.json b/test-data/tutorial-remotes.json index 414b63692..91f701473 100644 --- a/test-data/tutorial-remotes.json +++ b/test-data/tutorial-remotes.json @@ -6,7 +6,7 @@ "updateFrequency": "always", "shortName": "ref", "longName": "Lean Language Reference", - "sources": [{"local": "_out/html-multi/xref.json"}, "default"] + "sources": [{ "local": "_out/html-multi/xref.json" }, "default"] } } } diff --git a/verso-sources.json b/verso-sources.json index 226486252..ddae7b82d 100644 --- a/verso-sources.json +++ b/verso-sources.json @@ -1,19 +1,19 @@ { - "version": 0, - "sources": { - "reference": { - "root": "/reference", - "shortName": "reference", - "longName": "The Lean Language Reference", - "updateFrequency": "always", - "sources": [{"local": "_out/html-multi/xref.json"}] - }, - "tutorials": { - "root": "/tutorials", - "shortName": "tutorials", - "longName": "Lean Tutorials", - "updateFrequency": "always", - "sources": [{"local": "_tutorial-out/xref.json"}] + "version": 0, + "sources": { + "reference": { + "root": "/reference", + "shortName": "reference", + "longName": "The Lean Language Reference", + "updateFrequency": "always", + "sources": [{ "local": "_out/html-multi/xref.json" }] + }, + "tutorials": { + "root": "/tutorials", + "shortName": "tutorials", + "longName": "Lean Tutorials", + "updateFrequency": "always", + "sources": [{ "local": "_tutorial-out/xref.json" }] + } } - } } From d6c91f89acfa66da80b89f448a9992b40ad5f4ca Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 19 Dec 2025 19:14:39 +0100 Subject: [PATCH 34/45] details --- Manual/Meta.lean | 9 +++++++ Tutorial/Grind/IndexMap.lean | 4 +-- Tutorial/Meta/Theme.lean | 3 +-- Tutorial/VCGen.lean | 14 +++++----- TutorialMain.lean | 52 +++++------------------------------- lake-manifest.json | 4 +-- 6 files changed, 27 insertions(+), 59 deletions(-) diff --git a/Manual/Meta.lean b/Manual/Meta.lean index 9ecb4f9f7..ed2b72eca 100644 --- a/Manual/Meta.lean +++ b/Manual/Meta.lean @@ -390,6 +390,15 @@ def ffi.descr : BlockDescr where toTeX := some <| fun _goI goB _ _ contents => contents.mapM goB -- TODO +open Verso.Output.Html in +inline_extension Inline.multiCode where + traverse _ _ _ := pure none + toHtml := some <| fun goI _id _data contents => do return {{{{← contents.mapM goI}}}} + toTeX := none + +@[role] +def multiCode : RoleExpanderOf Unit + | (), contents => do ``(Inline.other Inline.multiCode #[$(← contents.mapM elabInline),*]) structure LeanSectionConfig where diff --git a/Tutorial/Grind/IndexMap.lean b/Tutorial/Grind/IndexMap.lean index 79a80bf36..e7b450787 100644 --- a/Tutorial/Grind/IndexMap.lean +++ b/Tutorial/Grind/IndexMap.lean @@ -31,10 +31,10 @@ set_option verso.exampleProject "." set_option verso.exampleModule "IndexMapGrind" -#doc (Tutorial) "`IndexMap`" => +#doc (Tutorial) "Using `grind` for Ordered Maps" => %%% slug := "grind-index-map" -summary := "A walkthrough of ..." +summary := "A demonstration of how to use `grind` to automate essentially all proofs in a new data structure, with an interface that finds proofs automatically." exampleStyle := .inlineLean `IndexMap %%% diff --git a/Tutorial/Meta/Theme.lean b/Tutorial/Meta/Theme.lean index c6a9d4175..6070f94bd 100644 --- a/Tutorial/Meta/Theme.lean +++ b/Tutorial/Meta/Theme.lean @@ -307,7 +307,6 @@ Lean-specific page type detection functions. -/ def isMarkdownPage : Path → Bool - | #[] | #["fro"] | #["404"] => false | _ => true def indexPage : Path → Bool @@ -348,7 +347,7 @@ def layoutConfig : LayoutConfig := needsTitle := needsTitle, isPagePost := isPagePost, postConfig := postConfig, - hasSpecialStyling := fun path => if isFro path then some "fro" else none, + hasSpecialStyling := fun path => if isFro path then some "fro" else if path.isEmpty then "tutorials" else none, renderPostList := fun path html => if isUseCases path then {{
{{ html }}
}} diff --git a/Tutorial/VCGen.lean b/Tutorial/VCGen.lean index d0b41085e..9a46063e6 100644 --- a/Tutorial/VCGen.lean +++ b/Tutorial/VCGen.lean @@ -31,7 +31,7 @@ set_option mvcgen.warning false %%% tag := "mvcgen-tactic-tutorial" slug := "mvcgen" -summary := "summary here" +summary := "A demonstration of how to use Lean's verification condition generator to conveniently and compositionally prove properties of monadic programs." exampleStyle := .inlineLean `MVCGenTutorial %%% @@ -145,8 +145,8 @@ theorem mySum_correct_shorter (l : Array Nat) : mySum l = l.sum := by · ⇓⟨xs, out⟩ => ⌜xs.prefix.sum = out⌝ with grind ``` -The {keyword}`mvcgen invariants `{lit}`...`{keyword}` with `{lit}`...` is an abbreviation for the -tactic sequence {keyword}`mvcgen; case`{lit}` inv1 => ...`{keyword}`; all_goals mleave; grind` +The {multiCode}[{keyword}`mvcgen invariants `{lit}`...`{keyword}` with `{lit}`...`] is an abbreviation for the +tactic sequence {multiCode}[{keyword}`mvcgen; case`{lit}` inv1 => ...`{keyword}`; all_goals mleave; grind`] above. It is the form that we will be using from now on. ::: @@ -305,7 +305,7 @@ Furthermore, an {tactic}`mvcgen`-powered proof will never need to copy any part variable (M : Type u → Type v) [Monad M] (α : Type u) axiom M.run : M α → β → α ``` -The previous examples reasoned about functions defined using {lean}`Id.run`{lit}` `{keywordOf Lean.Parser.Term.do}`do`{lit}` ` to make use of local mutability and early return in {lit}``. +The previous examples reasoned about functions defined using {multiCode}[{lean}`Id.run`{lit}` `{keywordOf Lean.Parser.Term.do}`do`{lit}` `] to make use of local mutability and early return in {lit}``. However, real-world programs often use {keywordOf Lean.Parser.Term.do}`do` notation and monads {lean}`M` to hide away state and failure conditions as implicit “effects”. In this use case, functions usually omit the {name}`M.run`. Instead they have a monadic return type {lean}`M α` and compose well with other functions of that return type. @@ -481,7 +481,7 @@ Pure, stateful hypotheses may be freely moved into the regular Lean context and ## Composing Specifications -Nested unfolding of definitions as in {tactic}`mvcgen`{lit}` [`{name}`mkFreshN`{lit}`, `{name}`mkFresh`{lit}`]` is quite blunt but effective for small programs. +Nested unfolding of definitions as in {multiCode}[{tactic}`mvcgen`{lit}` [`{name}`mkFreshN`{lit}`, `{name}`mkFresh`{lit}`]`] is quite blunt but effective for small programs. A more compositional way is to develop individual {tech (remote := "reference")}_specification lemmas_ for each monadic function. A specification lemma is a Hoare triple that is automatically used during {tech (remote := "reference")}[verification condition] generation to obtain the pre- and postconditions of each statement in a {keywordOf Lean.Parser.Term.do}`do`-block. When the system cannot automatically prove that the postcondition of one statement implies the precondition of the next, then this missing reasoning step becomes a verification condition. @@ -945,8 +945,8 @@ variable {σs : List (Type u)} {H T : SPred σs} ``` It is a priority of {tactic}`mvcgen` to break down monadic programs into {tech (remote := "reference")}[verification conditions] that are straightforward to understand. -For example, when the monad is monomorphic and all loop invariants have been instantiated, an invocation of {tactic}`all_goals`{lit}` `{tactic}`mleave` should simplify away any {name}`Std.Do.SPred`-specific constructs and leave behind a goal that is easily understood by humans and {tactic}`grind`. -This {tactic}`all_goals`{lit}` `{tactic}`mleave` step is carried out automatically by {tactic}`mvcgen` after loop invariants have been instantiated. +For example, when the monad is monomorphic and all loop invariants have been instantiated, an invocation of {multiCode}[{tactic}`all_goals`{lit}` `{tactic}`mleave`] should simplify away any {name}`Std.Do.SPred`-specific constructs and leave behind a goal that is easily understood by humans and {tactic}`grind`. +This {multiCode}[{tactic}`all_goals`{lit}` `{tactic}`mleave`]step is carried out automatically by {tactic}`mvcgen` after loop invariants have been instantiated. However, there are times when {tactic}`mleave` will be unable to remove all {name}`Std.Do.SPred` constructs. In this case, verification conditions of the form {lean}`H ⊢ₛ T` will be left behind. diff --git a/TutorialMain.lean b/TutorialMain.lean index cfa888e3b..ef21c6f2d 100644 --- a/TutorialMain.lean +++ b/TutorialMain.lean @@ -19,37 +19,25 @@ def plausible := {{ }} -open Verso.Output.Html in -def staticJs := {{ - - - }} - -open Verso.Output.Html in -def staticCss := {{ - - - - - - - - }} def version (_content : Array (Verso.Doc.Inline g)) : Verso.Doc.Inline g := .text Lean.versionString +def manualLink (args : Array (Verso.Doc.Inline g)) : Verso.Doc.Inline g:= + Verso.Doc.Inline.link args Lean.manualRoot + open Verso.Doc Concrete in def tutorials : Tutorials where content := (verso (Page) "Tutorials" ::::::: - These tutorials are written for version {version}[] of Lean. + These tutorials cover version {version}[] of Lean. + While the {manualLink}[reference manual] describes the system and its features in detail, these tutorials introduce one specific aspect. :::::::).toPart topics := #[ { title := #[inlines!"Tactics"], titleString := "Tactics" - description := #[blocks!"..."] + description := #[blocks!"These tutorials demonstrate Lean's advanced proof automation."] tutorials := #[%doc Tutorial.VCGen, %doc Tutorial.Grind.IndexMap] } @@ -82,34 +70,6 @@ where links : VersoDoc Page := { construct := fun _ => placeholder "Links" } people : VersoDoc Page := { construct := fun _ => placeholder "People" } --- open Verso.Output.Html in --- def theme : Theme where --- page content := do --- let config := { logError := fun _ => pure () } --- let ctxt := { --- site := leanSite, --- ctxt := { --- config, --- components := {}, --- path := #["doc", "tutorials"] --- }, --- xref := { remoteContent := {} }, --- linkTargets := {}, --- dir := "", --- config, --- header := "" --- } --- let pageContent := {{
{{content.content}}
}} --- let mut params : Verso.Genre.Blog.Template.Params := {} --- params := params.insert "title" content.title --- params := params.insert "content" pageContent --- let ((html, st'), y) ← Verso.Genre.Blog.Template.renderMany [LeanLangOrg.theme.pageTemplate, LeanLangOrg.theme.primaryTemplate] params ctxt {} {} --- pure html --- topic := Theme.default.topic --- tutorialToC := Theme.default.tutorialToC --- cssFiles := Verso.Web.Theme.Static.allCSS.map fun (filename, contents) => --- { filename := s!"theme/style/{filename}", contents } - def codeColors := r#" :root { diff --git a/lake-manifest.json b/lake-manifest.json index fe175e6f1..7a6b39b1b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "9b7146809fc91975b210eb388c43d9e09ddfb01e", + "rev": "bb53f1e61444637f3b5951e892b446da05dd8e81", "name": "versowebcomponents", "manifestFile": "lake-manifest.json", "inputRev": "tutorials", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "525de870d337366103ec48316d6c190fcbc576c7", + "rev": "2f95678da15b0705a97645f07b239d01ab8f8598", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "tutorials", From 8e272474c506b28e642d36e44aa8e4989c93d7d3 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 19 Dec 2025 20:03:54 +0100 Subject: [PATCH 35/45] example code appearance --- Tutorial/VCGen.lean | 68 ++++++++++++++++++++++++++++++++------------- TutorialMain.lean | 5 ++++ lake-manifest.json | 2 +- 3 files changed, 54 insertions(+), 21 deletions(-) diff --git a/Tutorial/VCGen.lean b/Tutorial/VCGen.lean index 9a46063e6..bede6d693 100644 --- a/Tutorial/VCGen.lean +++ b/Tutorial/VCGen.lean @@ -15,6 +15,7 @@ import Std.Tactic.Do open Verso.Genre Manual open Verso.Genre.Manual.InlineLean open Verso.Code.External (lit) +open Verso.Genre.Tutorial set_option pp.rawOnError true @@ -38,6 +39,12 @@ exampleStyle := .inlineLean `MVCGenTutorial This section is a tutorial that introduces the most important concepts of {tactic}`mvcgen` top-down. Recall that you need to import {module}`Std.Tactic.Do` and open {namespace}`Std.Do` to run these examples: +:::codeOnly +```imports +import Std.Data.HashMap +import Std.Data.HashSet +``` +::: ```imports import Std.Tactic.Do ``` @@ -367,7 +374,7 @@ theorem mkFreshN_correct (n : Nat) : ((mkFreshN n).run' s).Nodup := by ## Hoare Triples -:::::leanSection +::::::leanSection ```lean -show universe u v variable {m : Type u → Type v} {ps : PostShape.{u}} [Monad m] [WP m ps] {α σ ε : Type u} {P : Assertion ps} {Q : PostCond α ps} {prog : m α} {c : Nat} @@ -387,8 +394,9 @@ Given {lean}`⦃P⦄ stmt1 ⦃Q⦄` and {lean}`⦃P'⦄ stmt2 ⦃Q'⦄`, if {lea Just as proofs about ordinary functions can rely on lemmas about the functions that they call, proofs about monadic programs can use lemmas that are specified in terms of Hoare triples. ::: -::::paragraph +:::::paragraph One suitable specification for {name}`mkFresh` as a Hoare triple is this translation of {name}`mkFreshN_correct`: +::::displayOnly :::leanSection ```lean -show variable {n : Nat} @@ -397,16 +405,18 @@ variable {n : Nat} ⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ ``` ::: +:::: ```lean -show variable {p : Prop} ``` Corner brackets embed propositions into the monadic assertion language, so {lean}`⌜p⌝` is the assertion of the proposition {lean}`p`. The precondition {lean}`⌜True⌝` asserts that {lean}`True` is true; this trivial precondition is used to state that the specification imposes no requirements on the state in which it is called. The postcondition states that the result value is a list with no duplicate elements. -:::: +::::: -::::paragraph +:::::paragraph A specification for the single-step {name}`mkFresh` describes its effects on the monad's state: +::::displayOnly :::leanSection ```lean -show variable {n : Nat} @@ -428,6 +438,7 @@ Note that this specification is lossy: {name}`mkFresh` could increment its state This is good, because specifications may _abstract over_ uninteresting implementation details, ensuring resilient and small proofs. ::: :::: +::::: :::paragraph @@ -477,7 +488,7 @@ for some {lean}`p`. Pure, stateful hypotheses may be freely moved into the regular Lean context and back. (This can be done manually with the {tactic}`mpure` tactic.) -::::: +:::::: ## Composing Specifications @@ -529,19 +540,26 @@ The specification lemma {name}`mkFreshN_spec` is automatically used by {tactic}` This subsection is a bit of a digression and can be skipped on first reading. -:::leanSection -```lean -show +::::leanSection + +:::codeOnly +```lean axiom M : Type → Type variable {x y : UInt8} [Monad M] [WP M .pure] def addQ (x y : UInt8) : M UInt8 := pure (x + y) local infix:1023 " +? " => addQ +``` +```lean -show axiom dots {α} : α local notation "…" => dots ``` +::: + Say the specification for some [`Aeneas`](https://github.com/AeneasVerif/aeneas)-inspired monadic addition function {typed}`x +? y : M UInt8` has the requirement that the addition won't overflow, that is, `h : x.toNat + y.toNat ≤ UInt8.size`. Should this requirement be encoded as a regular Lean hypothesis of the specification (`add_spec_hyp`) or should this requirement be encoded as a pure precondition of the Hoare triple, using `⌜·⌝` notation (`add_spec_pre`)? +:::displayOnly ```lean theorem add_spec_hyp (x y : UInt8) (h : x.toNat + y.toNat ≤ UInt8.size) : @@ -552,9 +570,10 @@ theorem add_spec_pre (x y : UInt8) : x +? y ⦃⇓ r => ⌜r.toNat = x.toNat + y.toNat⌝⦄ := … ``` - ::: +:::: + The first approach is advisable, although it should not make a difference in practice. The VC generator will move pure hypotheses from the stateful context into the regular Lean context, so the second form turns effectively into the first form. This is referred to as {deftech}_framing_ hypotheses (cf. the {tactic}`mpure` and {tactic}`mframe` tactics). @@ -566,11 +585,15 @@ Real-world programs often use monads that are built from multiple {tech (remote Verification of these programs requires taking this into account. We can tweak the previous example to demonstrate this. -```lean -show +:::codeOnly +```lean namespace Transformers +``` +```lean -show variable {m : Type → Type} {α : Type} {ps : PostShape.{0}} attribute [-instance] Lake.instMonadLiftTOfMonadLift_lake ``` +::: ::::paragraph :::leanFirst @@ -610,8 +633,7 @@ theorem mkFresh_spec (c : Nat) : ⦃fun state => ⌜state.counter = c⌝⦄ mkFresh ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄ := by - --TODO: mvcgen [mkFresh] with grind - sorry + mvcgen [mkFresh] with grind @[spec] theorem mkFreshN_spec (n : Nat) : @@ -636,9 +658,11 @@ However, under the radar of the user the proof builds on a cascade of specificat ::: -```lean -show +:::codeOnly +```lean end Transformers ``` +::: # Exceptions @@ -675,9 +699,11 @@ The notion of postconditions {name}`PostCond` in `Std.Do` supports this spectrum :::: -```lean -show +:::codeOnly +```lean namespace Exceptions ``` +::: For example, suppose that our {name}`Supply` of fresh numbers is bounded and we want to throw an exception if the supply is exhausted. @@ -755,9 +781,11 @@ theorem mkFreshN_correct (n : Nat) : ``` ::: -```lean -show +:::codeOnly +```lean end Exceptions ``` +::: :::leanSection ```lean -show @@ -790,8 +818,8 @@ The {name}`WP` instance defines the weakest precondition interpretation of a mon and the matching {name}`WPMonad` instance asserts that this translation distributes over the {name}`Monad` operations. ::: -::::paragraph -:::leanFirst +:::::paragraph +::::leanFirst Suppose one wants to use `mvcgen` to generate verification conditions for programs generated by [`Aeneas`](https://github.com/AeneasVerif/aeneas). `Aeneas` translates Rust programs into Lean programs in the following {name}`Result` monad: @@ -805,7 +833,8 @@ inductive Result (α : Type u) where | fail (e: Error): Result α | div ``` -```lean -show +:::codeOnly +```lean instance Result.instMonad : Monad Result where pure x := .ok x bind x f := match x with @@ -814,12 +843,11 @@ instance Result.instMonad : Monad Result where | .div => .div instance Result.instLawfulMonad : LawfulMonad Result := by - -- TODO: Replace sorry with grind when it no longer introduces section - -- variables - apply LawfulMonad.mk' <;> (simp only [Result.instMonad]; sorry) + apply LawfulMonad.mk' <;> (simp only [Result.instMonad]; grind) ``` ::: :::: +::::: :::paragraph There are both {inst}`Monad Result` and {inst}`LawfulMonad Result` instances. diff --git a/TutorialMain.lean b/TutorialMain.lean index ef21c6f2d..586e18f70 100644 --- a/TutorialMain.lean +++ b/TutorialMain.lean @@ -78,6 +78,7 @@ def codeColors := r#" "# def localToCStyle := r#" +/* nav.local-toc { position: fixed; top: calc(var(--nav-height) + 1rem + 60px); @@ -87,6 +88,7 @@ nav.local-toc { max-height: calc(100vh - 2rem - var(--nav-height) - 60px); overflow-y: auto; } +*/ nav.local-toc h1 { display: none; @@ -96,6 +98,7 @@ nav.local-toc ol { list-style: none; margin: 0; padding: 0; + display: none; } nav.local-toc li { @@ -112,6 +115,7 @@ nav.local-toc a:hover { } /* On smaller screens, display normally */ +/* @media (max-width: 90rem) { nav.local-toc { position: static; @@ -123,6 +127,7 @@ nav.local-toc a:hover { margin-bottom: 1rem; } } +*/ nav.local-toc ol ol { padding-left: 1rem; diff --git a/lake-manifest.json b/lake-manifest.json index 7a6b39b1b..b597db92d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "bb53f1e61444637f3b5951e892b446da05dd8e81", + "rev": "19e7248895e65c5ea0817c258d865d27bde6c991", "name": "versowebcomponents", "manifestFile": "lake-manifest.json", "inputRev": "tutorials", From ab8b665f4b5ceec31b6378a3a8d3319231a37b81 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 15 Jan 2026 14:38:39 +0100 Subject: [PATCH 36/45] fix: use generate script for preview drafts --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6bb8b5442..85def2ba8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -176,7 +176,7 @@ jobs: if: github.event_name == 'pull_request' id: generate run: | - lake --quiet exe generate-manual --depth 2 --verbose --draft --without-html-single --output "_out/draft" + ./generate.sh --mode preview --draft --output _out/draft-site - name: Report status to Lean PR if: always() && github.repository == 'leanprover/reference-manual' From 5e3700f93a113ae044eaa72cd9a8108531c65014 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 15 Jan 2026 16:19:39 +0100 Subject: [PATCH 37/45] fix: compatibility with upstream verso --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 5545c19e6..6710043e3 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "e4c1b91a20c85d310c2eed60447c2a4e2eeefe20", + "rev": "845fadc0cbb156e0f4ded4da2749531a7f913f7c", "name": "versowebcomponents", "manifestFile": "lake-manifest.json", "inputRev": "main", From e441d0ab0eb0725b88c76ab783d8c0e075464a4f Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 15 Jan 2026 17:16:31 +0100 Subject: [PATCH 38/45] fix: trailing slash fix in Verso for tutorial links --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 6710043e3..a02d6e4b2 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "142f6c8177be7b0a63fb3a9431b1587c6368020b", + "rev": "82eba5d89a5f21aea934d8a57c40e275c5ec3651", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "main", From d591f95b99f098461872f7eba83459aea2ee6705 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 15 Jan 2026 17:56:09 +0100 Subject: [PATCH 39/45] fix: JS from themes in Verso --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index a02d6e4b2..1ca28207f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "82eba5d89a5f21aea934d8a57c40e275c5ec3651", + "rev": "d46ba7b5429e54864e7061205908d6bdf6e9ab19", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "main", From 57188295f4d8a340f7a20b8e078ed05658e0dcb2 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 15 Jan 2026 19:20:23 +0100 Subject: [PATCH 40/45] chore: check tutorial example projects in CI --- .github/workflows/ci.yml | 5 ++++ scripts/check-tutorial-zips.sh | 51 ++++++++++++++++++++++++++++++++++ 2 files changed, 56 insertions(+) create mode 100755 scripts/check-tutorial-zips.sh diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 85def2ba8..f16f6cada 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -172,6 +172,11 @@ jobs: run: | scripts/check-examples-isolated.sh + - name: Verify tutorial project zip files build + if: github.event_name != 'release' + run: | + scripts/check-tutorial-zips.sh + - name: Generate proofreading HTML if: github.event_name == 'pull_request' id: generate diff --git a/scripts/check-tutorial-zips.sh b/scripts/check-tutorial-zips.sh new file mode 100755 index 000000000..26e4cdad2 --- /dev/null +++ b/scripts/check-tutorial-zips.sh @@ -0,0 +1,51 @@ +#!/usr/bin/env bash + +# Verify that tutorial project zip files can be unpacked and built with lake + +# First check that we actually found some zip files +zip_count=$(find _out/site/tutorials -name "*.zip" 2>/dev/null | wc -l) +if [ "$zip_count" -eq 0 ]; then + echo "Error: No tutorial zip files found in _out/site/tutorials" + echo "If the output structure changed, update this script." + exit 1 +fi + +successes=0 +failures=0 + +while IFS= read -r zip; do + echo "=== Testing: $zip" + tmpdir=$(mktemp -d) + unzip -q "$zip" -d "$tmpdir" + + # Find the project directory (may be nested inside the zip) + project_dir=$(find "$tmpdir" -name "lakefile.lean" -o -name "lakefile.toml" | head -1 | xargs dirname 2>/dev/null) + + if [ -z "$project_dir" ]; then + echo "Warning: No lakefile found in $zip" + ((failures++)) + else + pushd "$project_dir" > /dev/null + if lake build 2>&1; then + echo "Build succeeded" + ((successes++)) + else + echo "Build failed" + ((failures++)) + fi + popd > /dev/null + fi + + rm -rf "$tmpdir" +done < <(find _out/site/tutorials -name "*.zip" 2>/dev/null) + +echo +echo "Summary:" +echo " Succeeded: $successes" +echo " Failed: $failures" + +if [ $failures -ne 0 ]; then + exit 1 +else + exit 0 +fi From 72ac58c9b66cf6b133266654dfcbf65d3850527d Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 15 Jan 2026 22:25:29 +0100 Subject: [PATCH 41/45] chore: prepare CI infrastructure for tutorials release --- .github/workflows/ci.yml | 4 +- .github/workflows/overlay.yml | 22 +++++------ .github/workflows/release-tag.yml | 10 +++-- .github/workflows/upload-snapshots.yml | 55 +++++++++++++------------- deploy/generate.sh | 10 ++++- deploy/overlay.py | 5 +++ generate.sh => generate-html.sh | 0 7 files changed, 59 insertions(+), 47 deletions(-) rename generate.sh => generate-html.sh (100%) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f16f6cada..dc953e178 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -161,7 +161,7 @@ jobs: - name: Generate HTML (non-release) if: github.event_name != 'release' run: | - ./generate.sh --mode preview + ./generate-html.sh --mode preview - name: Generate HTML (release) if: github.event_name == 'release' @@ -181,7 +181,7 @@ jobs: if: github.event_name == 'pull_request' id: generate run: | - ./generate.sh --mode preview --draft --output _out/draft-site + ./generate-html.sh --mode preview --draft --output _out/draft-site - name: Report status to Lean PR if: always() && github.repository == 'leanprover/reference-manual' diff --git a/.github/workflows/overlay.yml b/.github/workflows/overlay.yml index b304c9ae9..da5a9f737 100644 --- a/.github/workflows/overlay.yml +++ b/.github/workflows/overlay.yml @@ -34,9 +34,8 @@ jobs: git config --global user.email "41898282+github-actions[bot]@users.noreply.github.com" git fetch origin deploy:deploy git fetch origin postdeploy:postdeploy - # TODO: Fetch tutorials branches when ready for production deployment: - # git fetch origin deploy-tutorials:deploy-tutorials - # git fetch origin postdeploy-tutorials:postdeploy-tutorials + git fetch origin deploy-tutorials:deploy-tutorials + git fetch origin postdeploy-tutorials:postdeploy-tutorials - name: Run overlay script run: | @@ -49,12 +48,11 @@ jobs: run: | git push origin postdeploy - # TODO: Add these steps when tutorials are ready for production deployment: - # - name: Run overlay script for tutorials - # run: | - # echo "Adding overlays to tutorials predeploy" - # python -B deploy/overlay.py . deploy-tutorials postdeploy-tutorials --site-dir tutorials - # - # - name: Push tutorials deploy branch - # run: | - # git push origin postdeploy-tutorials + - name: Run overlay script for tutorials + run: | + echo "Adding overlays to tutorials predeploy" + python -B deploy/overlay.py . deploy-tutorials postdeploy-tutorials --site-dir tutorials + + - name: Push tutorials deploy branch + run: | + git push origin postdeploy-tutorials diff --git a/.github/workflows/release-tag.yml b/.github/workflows/release-tag.yml index ad54bce36..a1ea3a105 100644 --- a/.github/workflows/release-tag.yml +++ b/.github/workflows/release-tag.yml @@ -134,11 +134,13 @@ jobs: echo "Making deployment from tag: '$TAG_NAME'" python deploy/release.py ${{ steps.detect-structure.outputs.reference_dir }} "$VERSION" deploy - # TODO: Add tutorials deployment when ready for production (requires new structure): - # python deploy/release.py html/site/tutorials "$VERSION" deploy-tutorials + if [ "${{ steps.detect-structure.outputs.structure }}" = "new" ]; then + python deploy/release.py html/site/tutorials "$VERSION" deploy-tutorials + fi - name: Push deploy branch run: | git push origin deploy - # TODO: Push tutorials branch when ready for production: - # git push origin deploy-tutorials + if [ "${{ steps.detect-structure.outputs.structure }}" = "new" ]; then + git push origin deploy-tutorials + fi diff --git a/.github/workflows/upload-snapshots.yml b/.github/workflows/upload-snapshots.yml index f3467832f..f8a423b96 100644 --- a/.github/workflows/upload-snapshots.yml +++ b/.github/workflows/upload-snapshots.yml @@ -42,31 +42,30 @@ jobs: # This is the site called 'lean-reference-manual-versions' NETLIFY_SITE_ID: "91dc33ef-6016-4ac7-bac1-d574e2254405" - # TODO: Add parallel job for tutorials when ready for production deployment: - # deploy-tutorials: - # name: Deploy tutorials release branch to hosting - # runs-on: ubuntu-latest - # if: - # ${{ github.event_name != 'workflow_run' || github.event.workflow_run.conclusion == - # 'success' }} - # steps: - # - name: Checkout postdeploy-tutorials branch - # uses: actions/checkout@v4 - # with: - # ref: "postdeploy-tutorials" - # - # - name: Upload the current state of the postdeploy-tutorials branch - # uses: nwtgck/actions-netlify@v2.0 - # with: - # publish-dir: "." - # production-branch: postdeploy-tutorials - # production-deploy: true - # github-token: ${{ secrets.GITHUB_TOKEN }} - # deploy-message: | - # Deploy tutorials from ${{ github.ref }} - # enable-commit-comment: false - # enable-pull-request-comment: false - # fails-without-credentials: true - # env: - # NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }} - # NETLIFY_SITE_ID: "e76b4246-fee7-491e-91ef-a87fffff6ce1" + deploy-tutorials: + name: Deploy tutorials release branch to hosting + runs-on: ubuntu-latest + if: + ${{ github.event_name != 'workflow_run' || github.event.workflow_run.conclusion == + 'success' }} + steps: + - name: Checkout postdeploy-tutorials branch + uses: actions/checkout@v4 + with: + ref: "postdeploy-tutorials" + + - name: Upload the current state of the postdeploy-tutorials branch + uses: nwtgck/actions-netlify@v2.0 + with: + publish-dir: "." + production-branch: postdeploy-tutorials + production-deploy: true + github-token: ${{ secrets.GITHUB_TOKEN }} + deploy-message: | + Deploy tutorials from ${{ github.ref }} + enable-commit-comment: false + enable-pull-request-comment: false + fails-without-credentials: true + env: + NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }} + NETLIFY_SITE_ID: "e76b4246-fee7-491e-91ef-a87fffff6ce1" diff --git a/deploy/generate.sh b/deploy/generate.sh index 21fe62ac7..6cd7f8963 100755 --- a/deploy/generate.sh +++ b/deploy/generate.sh @@ -1,3 +1,11 @@ #!/usr/bin/env bash +set -euo pipefail -lake --quiet exe generate-manual --depth 2 --verbose --without-html-single --output "html" +# VERSION is set by release-tag.yml from the git tag +if [ -z "${VERSION:-}" ]; then + echo "Error: VERSION environment variable must be set" + exit 1 +fi + +# Build both manual and tutorials using the combined generate script +./generate-html.sh --mode production --version "$VERSION" --output "html/site" diff --git a/deploy/overlay.py b/deploy/overlay.py index 9829be465..ed08bba7f 100644 --- a/deploy/overlay.py +++ b/deploy/overlay.py @@ -93,6 +93,11 @@ def deploy_overlays(deploy_dir, src_branch, tgt_branch, site_dir): if is_git_ancestor(tgt_branch, src_branch): raise Exception(f"Git merge will have bad behavior if {tgt_branch} is an ancestor of {src_branch}, try creating a vacuous commit on {tgt_branch} first.") run_git_command(["git", "switch", src_branch]) + + if find_latest_version(deploy_dir) is None: + print(f"No version directories found on {src_branch}, nothing to overlay") + return + print(f"Applying overlays...") apply_overlays(deploy_dir, site_dir) print(f"Creating merge commit...") diff --git a/generate.sh b/generate-html.sh similarity index 100% rename from generate.sh rename to generate-html.sh From 50230680911d405c9e57bb0c2d33859af9ad8522 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 15 Jan 2026 22:56:22 +0100 Subject: [PATCH 42/45] chore: update README for new deployment and fix bug in YAML --- .github/workflows/overlay.yml | 7 +++ README.md | 111 ++++++++++++++++++++-------------- 2 files changed, 73 insertions(+), 45 deletions(-) diff --git a/.github/workflows/overlay.yml b/.github/workflows/overlay.yml index da5a9f737..25c19e88d 100644 --- a/.github/workflows/overlay.yml +++ b/.github/workflows/overlay.yml @@ -9,6 +9,7 @@ on: push: branches: - "deploy" + - "deploy-tutorials" workflow_dispatch: @@ -37,7 +38,9 @@ jobs: git fetch origin deploy-tutorials:deploy-tutorials git fetch origin postdeploy-tutorials:postdeploy-tutorials + # Run reference overlay if triggered by workflow_run, workflow_dispatch, or push to deploy - name: Run overlay script + if: github.event_name != 'push' || github.ref == 'refs/heads/deploy' run: | echo "Adding overlays to predeploy" # -B to prevent creation of __pycache__ directory @@ -45,14 +48,18 @@ jobs: python -B deploy/overlay.py . deploy postdeploy --site-dir reference - name: Push deploy branch + if: github.event_name != 'push' || github.ref == 'refs/heads/deploy' run: | git push origin postdeploy + # Run tutorials overlay if triggered by workflow_run, workflow_dispatch, or push to deploy-tutorials - name: Run overlay script for tutorials + if: github.event_name != 'push' || github.ref == 'refs/heads/deploy-tutorials' run: | echo "Adding overlays to tutorials predeploy" python -B deploy/overlay.py . deploy-tutorials postdeploy-tutorials --site-dir tutorials - name: Push tutorials deploy branch + if: github.event_name != 'push' || github.ref == 'refs/heads/deploy-tutorials' run: | git push origin postdeploy-tutorials diff --git a/README.md b/README.md index fbb5e08ed..34e0e27d4 100644 --- a/README.md +++ b/README.md @@ -110,15 +110,15 @@ Please see [CONTRIBUTING.md](CONTRIBUTING.md) for more information. TL;DR: push a tag of the form `vX.Y.Z` onto the commit that should be released as the manual for that version, and the rest is automatic. -This directory contains the deployment infrastructure for the -reference manual. Deployment happens in GitHub Actions, in response to -certain tags being pushed. Because the latest version of the GH action -file will always be used, and we want to be able to mutate tags to -re-deploy old manual versions (e.g. to update CSS for consistent look -and feel while keeping content version-accurate, or add a "THIS IS -OBSOLETE" banner in a few years). Thus, the steps of the workflow that -might change are captured in scripts that are versioned along with the -code. +This repository contains the deployment infrastructure for both the +reference manual and the tutorials site. Deployment happens in GitHub +Actions, in response to certain tags being pushed. Because the latest +version of the GH action file will always be used, and we want to be +able to mutate tags to re-deploy old manual versions (e.g. to update +CSS for consistent look and feel while keeping content +version-accurate, or add a "THIS IS OBSOLETE" banner in a few years), +the steps of the workflow that might change are captured in scripts +that are versioned along with the code. The files are: @@ -128,19 +128,22 @@ The files are: - `build.sh` is used to build the executable that generates the manual. -- `generate.sh` actually generates release-ready HTML, saving it in - `/html` in the root of this repository. +- `generate.sh` builds both the reference manual and tutorials, + saving them in `/html/site/reference` and `/html/site/tutorials`. - `release.py` puts the generated HTML in the right place on a new - commit on the branch `deploy` + commit on a deployment branch (`deploy` for the reference manual, + `deploy-tutorials` for tutorials). Everything above is what needs to happen specifically to the single version of the documentation that is being updated in the course of the deploy. There is one further step, which is computing the desired -state of the final `postdeploy` branch from the state in the branch -`deploy`. This is done by the script `overlay.py`, which is triggered -by pushes to `deploy`, and therefore runs at branch `main` rather than -at the tag being pushed. +state of the final `postdeploy` branches from the state in the +`deploy` branches. This is done by the script `overlay.py`, which is +triggered by pushes to `deploy`, and therefore runs at branch `main` +rather than at the tag being pushed. It processes both the reference +manual (`deploy` → `postdeploy`) and tutorials (`deploy-tutorials` → +`postdeploy-tutorials`). We might have named the two branches `predeploy` and `deploy`, but chose instead `deploy` and `postdeploy` so that we cold leave @@ -149,24 +152,34 @@ still have workflows that emit commits to `deploy`. ## Deployment Overview -The goal is to have versioned snapshots of the manual, with a -structure like: +The goal is to have versioned snapshots of both the reference manual +and tutorials, with a structure like: -- `https://lean-lang.org/doc/reference/latest/`- latest version -- `https://lean-lang.org/doc/reference/4.19.0/` - manual for v4.19.0 -- `https://lean-lang.org/doc/reference/4.20.0/` - manual for v4.19.0 +- `https://lean-lang.org/doc/reference/latest/` - latest version +- `https://lean-lang.org/doc/reference/stable/` - latest stable version +- `https://lean-lang.org/doc/reference/4.19.0/` - reference for v4.19.0 +- `https://lean-lang.org/doc/reference/4.20.0/` - reference for v4.20.0 +- `https://lean-lang.org/doc/tutorials/latest/` - latest tutorials +- `https://lean-lang.org/doc/tutorials/stable/` - latest stable tutorials +- `https://lean-lang.org/doc/tutorials/4.19.0/` - tutorials for v4.19.0 +- `https://lean-lang.org/doc/tutorials/4.20.0/` - tutorials for v4.20.0 -and so forth. `https://lean-lang.org/doc/reference/` should redirect -to `latest`. It's important to be able to edit past deployments as -well. +and so forth. The base URLs should redirect to `latest`. It's +important to be able to edit past deployments as well. -An orphan branch, called `deploy`, should at all times contain this -structure. With the three URLs above, the branch would contain three -directories: +Orphan branches `deploy` and `deploy-tutorials` contain the versioned +content for each site. For example, the `deploy` branch might contain: -- `/4.20.0/` - built HTML served for 4.20.0 -- `/4.19.0/` - built HTML served for 4.19.0 -- `/latest` - symlink to `/4.20.0` +- `/4.25.0-rc1/` - built HTML for 4.25.0-rc1 +- `/4.24.0/` - built HTML for 4.24.0 +- `/4.23.0/` - built HTML for 4.23.0 +- `/latest/` - copy of `/4.25.0-rc1/` (the most recent version) +- `/stable/` - copy of `/4.24.0/` (the most recent non-RC version) + +The `latest` and `stable` directories are full copies rather than +symlinks because Netlify deployment doesn't support symlinks. + +The `deploy-tutorials` branch has the same structure for tutorials. The `release.py` script is responsible for updating this structure. It takes the generated HTML directory, the version number, and the @@ -174,31 +187,34 @@ deployment branch name as arguments, and then does the following: 1. It copies the HTML to the branch (deleting an existing directory first if needed). -2. It updates the `latest` symlink to point at the most recent +2. It updates the `latest` directory to be a copy of the most recent version, with all numbered releases being considered more recent than any nightly and real releases being more recent than their RCs. -3. It commits the changes to the branch `deploy`, then switches back +3. It updates the `stable` directory to be a copy of the most recent + non-RC version. +4. It commits the changes to the deployment branch, then switches back to the original branch. -A successful push to deploy in this way triggers a GH action that runs -the `overlay.py` script, which is then responsible for creating a new -commit to `postdeploy`, based on `deploy`. This commit includes all -desired overlays. At time of writing, this is just a single file -`static/metadata.js` in each version of the reference manual that +A successful push to `deploy` triggers a GH action that runs the +`overlay.py` script, which creates commits to `postdeploy` (based on +`deploy`) and `postdeploy-tutorials` (based on `deploy-tutorials`). +These commits include all desired overlays. At time of writing, this +is just a single file `static/metadata.js` in each version that contains information about whether the version is in fact stable or latest. -A successful push to `postdeploy` in this way triggers a GH Action -which actually publishes the content to netlify. +A successful push to `postdeploy` or `postdeploy-tutorials` triggers a +GH Action which publishes the content to Netlify. ## Overlays The script `overlay.py` computes `postdeploy` from `deploy` any time -`deploy` changes. Its purpose is to add metadata or make in-place -changes to `deploy` content that is best thought of as a unified -overlay on top of the data that exists at the historical tags -`4.19.0`, `4.20.0`, etc. +`deploy` changes, and `postdeploy-tutorials` from `deploy-tutorials` +any time `deploy-tutorials` changes. Its purpose is to add metadata or +make in-place changes to deployed content that is best thought of as +a unified overlay on top of the data that exists at the historical +version tags. Examples of the sorts of things we might like to achieve with this overlay mechanism are: @@ -233,7 +249,7 @@ Therefore we can be careful on both sides: To test `overlay.py` locally before pushing, do the following. -- Ensure branches `deploy` and `postdeploy` exist locally. +- Ensure the deployment branches exist locally. - You'll probably want to do ``` @@ -242,6 +258,10 @@ git checkout deploy git reset --hard remotes/upstream/deploy git checkout postdeploy git reset --hard remotes/upstream/postdeploy +git checkout deploy-tutorials +git reset --hard remotes/upstream/deploy-tutorials +git checkout postdeploy-tutorials +git reset --hard remotes/upstream/postdeploy-tutorials ``` - From the `reference-manual` checkout directory, on branch `main`, @@ -249,7 +269,8 @@ git reset --hard remotes/upstream/postdeploy you've made) run ```shell -python3 -B deploy/overlay.py . deploy postdeploy +python3 -B deploy/overlay.py . deploy postdeploy --site-dir reference +python3 -B deploy/overlay.py . deploy-tutorials postdeploy-tutorials --site-dir tutorials ``` - Inspect whatever `postdeploy` results you're interested in, e.g. From bd55e8dc97893795c31801d5b411cd7fdb950553 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 15 Jan 2026 23:42:18 +0100 Subject: [PATCH 43/45] fix: overlay.py compatibility with tutorials deply/overlay.py previously identified version directories by the presence of static/ underneath, but tutorials have a different structure. Now it checks for static/ or theme/ to match both. --- deploy/overlay.py | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/deploy/overlay.py b/deploy/overlay.py index ed08bba7f..431247e47 100644 --- a/deploy/overlay.py +++ b/deploy/overlay.py @@ -60,16 +60,18 @@ def apply_overlays(deploy_dir, site_dir): print (f"overlay.py: the latest stable lean version is {latest_stable_version}") header = "// This file was automatically generated by reference-manual/deploy/overlay.py" for inner in Path(deploy_dir).iterdir(): - if inner.is_dir() and (inner / "static").is_dir(): - # Generate some version metadata - filename = inner / "static" / "metadata.js" - content = f"{header}\nwindow.metadata = {{versionString: \"{inner}\"}};\n" - if str(inner) == latest_version or str(inner) == "latest": - content += f"window.metadata.latest = true;\n" - if str(inner) == latest_stable_version or str(inner) == "stable": - content += f"window.metadata.stable = true;\n" - with open(filename, 'a') as file: - file.write(content) + # Check for index.html to identify version directories + if inner.is_dir() and (inner / "index.html").is_file(): + # Generate metadata.js only for reference manual (it has static/) + if site_dir == "reference" and (inner / "static").is_dir(): + filename = inner / "static" / "metadata.js" + content = f"{header}\nwindow.metadata = {{versionString: \"{inner}\"}};\n" + if str(inner) == latest_version or str(inner) == "latest": + content += f"window.metadata.latest = true;\n" + if str(inner) == latest_stable_version or str(inner) == "stable": + content += f"window.metadata.stable = true;\n" + with open(filename, 'a') as file: + file.write(content) # Add appropriate metadata to every file at every version add_metadata(inner, str(inner), site_dir) From 02c9f457c84ec191da339f4a1fc31271b8210aac Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 16 Jan 2026 10:25:37 +0100 Subject: [PATCH 44/45] chore: comments based on workflow audit --- .github/workflows/overlay.yml | 7 +++++++ .github/workflows/release-tag.yml | 6 +++++- 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/.github/workflows/overlay.yml b/.github/workflows/overlay.yml index 25c19e88d..d1edfb37c 100644 --- a/.github/workflows/overlay.yml +++ b/.github/workflows/overlay.yml @@ -1,5 +1,12 @@ name: Apply Overlays +# This workflow applies HTML overlays (canonical URLs, robots noindex, metadata.js) to +# deployed content and pushes to the postdeploy branches. +# +# In normal operation, the workflow_run trigger fires when release-tag.yml completes. +# Pushes made by release-tag.yml using GITHUB_TOKEN do NOT trigger the push events +# (GitHub prevents this to avoid infinite loops). + on: workflow_run: workflows: ["Deploy Tagged Version"] diff --git a/.github/workflows/release-tag.yml b/.github/workflows/release-tag.yml index a1ea3a105..2fd5f8666 100644 --- a/.github/workflows/release-tag.yml +++ b/.github/workflows/release-tag.yml @@ -115,7 +115,11 @@ jobs: - name: Detect deployment structure id: detect-structure run: | - # Check if we have the new combined site structure or old single-site structure + # Check if we have the new combined site structure or old single-site structure. + # The single-site structure is used for older builds that don't have tutorials. + # Because this workflow runs on tag push, it runs in the context of the tagged + # commit; after tutorial deployments are confirmed working, we can get rid of this + # conditional and just assume the new structure in this workflow. if [ -d "html/site/reference" ]; then STRUCTURE="new" REFERENCE_DIR="html/site/reference" From b4b44787f1a5e89baee7b044ce3a62add0ecf775 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 16 Jan 2026 10:27:27 +0100 Subject: [PATCH 45/45] chore: prettier for README --- README.md | 30 ++++++++++++++++++------------ 1 file changed, 18 insertions(+), 12 deletions(-) diff --git a/README.md b/README.md index 34e0e27d4..472c5ab9b 100644 --- a/README.md +++ b/README.md @@ -128,8 +128,8 @@ The files are: - `build.sh` is used to build the executable that generates the manual. -- `generate.sh` builds both the reference manual and tutorials, - saving them in `/html/site/reference` and `/html/site/tutorials`. +- `generate.sh` builds both the reference manual and tutorials, saving + them in `/html/site/reference` and `/html/site/tutorials`. - `release.py` puts the generated HTML in the right place on a new commit on a deployment branch (`deploy` for the reference manual, @@ -156,13 +156,19 @@ The goal is to have versioned snapshots of both the reference manual and tutorials, with a structure like: - `https://lean-lang.org/doc/reference/latest/` - latest version -- `https://lean-lang.org/doc/reference/stable/` - latest stable version -- `https://lean-lang.org/doc/reference/4.19.0/` - reference for v4.19.0 -- `https://lean-lang.org/doc/reference/4.20.0/` - reference for v4.20.0 +- `https://lean-lang.org/doc/reference/stable/` - latest stable + version +- `https://lean-lang.org/doc/reference/4.19.0/` - reference for + v4.19.0 +- `https://lean-lang.org/doc/reference/4.20.0/` - reference for + v4.20.0 - `https://lean-lang.org/doc/tutorials/latest/` - latest tutorials -- `https://lean-lang.org/doc/tutorials/stable/` - latest stable tutorials -- `https://lean-lang.org/doc/tutorials/4.19.0/` - tutorials for v4.19.0 -- `https://lean-lang.org/doc/tutorials/4.20.0/` - tutorials for v4.20.0 +- `https://lean-lang.org/doc/tutorials/stable/` - latest stable + tutorials +- `https://lean-lang.org/doc/tutorials/4.19.0/` - tutorials for + v4.19.0 +- `https://lean-lang.org/doc/tutorials/4.20.0/` - tutorials for + v4.20.0 and so forth. The base URLs should redirect to `latest`. It's important to be able to edit past deployments as well. @@ -193,8 +199,8 @@ deployment branch name as arguments, and then does the following: RCs. 3. It updates the `stable` directory to be a copy of the most recent non-RC version. -4. It commits the changes to the deployment branch, then switches back - to the original branch. +4. It commits the changes to the deployment branch, then switches + back to the original branch. A successful push to `deploy` triggers a GH action that runs the `overlay.py` script, which creates commits to `postdeploy` (based on @@ -212,8 +218,8 @@ GH Action which publishes the content to Netlify. The script `overlay.py` computes `postdeploy` from `deploy` any time `deploy` changes, and `postdeploy-tutorials` from `deploy-tutorials` any time `deploy-tutorials` changes. Its purpose is to add metadata or -make in-place changes to deployed content that is best thought of as -a unified overlay on top of the data that exists at the historical +make in-place changes to deployed content that is best thought of as a +unified overlay on top of the data that exists at the historical version tags. Examples of the sorts of things we might like to achieve with this