diff --git a/Main.lean b/Main.lean index 50016c4e..929207c2 100644 --- a/Main.lean +++ b/Main.lean @@ -6,6 +6,7 @@ Author: David Thrane Christiansen import Manual import Manual.Meta import VersoManual +import Manual.ExtractExamples open Verso.Genre.Manual open Verso.Genre.Manual.InlineLean @@ -32,7 +33,7 @@ def staticCss := {{ }} def main := - manualMain (%doc Manual) (config := config) + manualMain (%doc Manual) (config := config) (extraSteps := [extractExamples]) where config := Config.addSearch <| Config.addKaTeX { extraFiles := [("static", "static")], diff --git a/Manual/ExtractExamples.lean b/Manual/ExtractExamples.lean new file mode 100644 index 00000000..d61f21b3 --- /dev/null +++ b/Manual/ExtractExamples.lean @@ -0,0 +1,60 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Jason Reed +-/ + +import Manual.Meta.Example +import VersoManual +open Lean +open Verso Doc Multi +open Verso.Genre Manual +open Std (HashMap) + +/-- +A monad for traversing all example directives in a document, and +extracting them into individual files in a directory structured as the +document is structured. In the `Array (Array String × String)`, the +first string is the path to the example file we're writing, and the +second is the body of the example. +-/ +abbrev ExtractM := ReaderT (Array String) (StateT (Array (Array String × String)) IO) + +partial def extractExamples (_mode : Mode) (logError : String → IO Unit) (cfg : Manual.Config) (_state : TraverseState) (text : Part Manual) : IO Unit := do + + let code := (← part text |>.run #[] |>.run #[]).snd + let dest := cfg.destination / "extracted-examples" + for (ctx, content) in code do + + let filename := ctx.map (Slug.toString ∘ String.sluggify) + |>.foldl (init := dest) (· / ·) + |>.withExtension "lean" + filename.parent.forM IO.FS.createDirAll + IO.FS.writeFile filename content + +where + part : Part Manual → ExtractM Unit + | .mk _ titleString _ intro subParts => withReader (·.push titleString) do + for b in intro do block b + for p in subParts do part p + block : Block Manual → ExtractM Unit + | .other which contents => do + if which.name == `Manual.example then + match FromJson.fromJson? which.data (α := Manual.ExampleBlockJson) with + | .error e => logError s!"Error deserializing example data: {e}" + | .ok (descrString, _, _, _, liveText) => + let context ← read + let some txt := liveText + | return () + modify fun saved => + saved.push (context.push descrString, txt) + for b in contents do block b + | .concat bs | .blockquote bs => + for b in bs do block b + | .ol _ lis | .ul lis => + for li in lis do + for b in li.contents do block b + | .dl dis => + for di in dis do + for b in di.desc do block b + | .para .. | .code .. => pure () diff --git a/Manual/Meta/Example.lean b/Manual/Meta/Example.lean index bf0e134e..21154b51 100644 --- a/Manual/Meta/Example.lean +++ b/Manual/Meta/Example.lean @@ -6,6 +6,7 @@ Author: David Thrane Christiansen import VersoManual import Manual.Meta.Figure +import Manual.Meta.LzCompress import Lean.Elab.InfoTree.Types open Verso Doc Elab @@ -17,11 +18,15 @@ open Lean Elab namespace Manual -def Block.example (descriptionString : String) (name : Option String) (opened : Bool) : Block where +def Block.example (descriptionString : String) (name : Option String) (opened : Bool) (liveText : Option String := none) : Block where + -- FIXME: This should be a double-backtickable name name := `Manual.example - data := ToJson.toJson (descriptionString, name, opened, (none : Option Tag)) + data := ToJson.toJson (descriptionString, name, opened, (none : Option Tag), liveText) properties := .empty |>.insert `Verso.Genre.Manual.exampleDefContext descriptionString +/-- The type of the Json stored with Block.example -/ +abbrev ExampleBlockJson := String × Option String × Bool × Option Tag × Option String + structure ExampleConfig where description : FileMap × TSyntaxArray `inline /-- Name for refs -/ @@ -58,10 +63,27 @@ def prioritizedElab [Monad m] (prioritize : α → m Bool) (act : α → m β) def isLeanBlock : TSyntax `block → CoreM Bool | `(block|```$nameStx:ident $_args*|$_contents:str```) => do - let name ← realizeGlobalConstNoOverloadWithInfo nameStx + let name ← realizeGlobalConstNoOverload nameStx return name == ``Verso.Genre.Manual.InlineLean.lean | _ => pure false +inductive LeanBlockContent where + | content : String → LeanBlockContent + | elabWithoutKeep : LeanBlockContent + | nonLeanBlock : LeanBlockContent + +def getLeanBlockContents? : TSyntax `block → DocElabM (LeanBlockContent) + | `(block|```$nameStx:ident $args*|$contents:str```) => do + let name ← realizeGlobalConstNoOverload nameStx + if name != ``Verso.Genre.Manual.InlineLean.lean then + return .nonLeanBlock + let args ← Verso.Doc.Elab.parseArgs args + let args ← parseThe InlineLean.LeanBlockConfig args + if !args.keep || args.error then + return .elabWithoutKeep + pure <| .content (contents.getString) + | _ => pure .nonLeanBlock + /-- Elaborates all Lean blocks first, enabling local forward references -/ @@ -73,6 +95,14 @@ def leanFirst : DirectiveExpander -- Elaborate Lean blocks first, so inlines in prior blocks can refer to them prioritizedElab (isLeanBlock ·) elabBlock contents +/-- Turn a list of lean blocks into one string with the appropriate amount of whitespace -/ +def renderExampleContent (exampleBlocks : List String) : String := + "\n\n".intercalate <| exampleBlocks.map (·.trim) + +/-- info: "a\n\nb\n\nc" -/ +#guard_msgs in +#eval renderExampleContent ["\n \na\n", "\n b", "c "] + /-- A domain for named examples -/ def examples : Domain := {} @@ -89,31 +119,44 @@ def «example» : DirectiveExpander (selectionRange := mkNullNode cfg.description.2) (kind := Lsp.SymbolKind.interface) (detail? := some "Example") + + let accumulate (b : TSyntax `block) : StateT (List String) DocElabM Bool := do + match ← getLeanBlockContents? b with + | LeanBlockContent.elabWithoutKeep => pure true + | LeanBlockContent.nonLeanBlock => pure false + | LeanBlockContent.content x => + modify (· ++ [x]) + pure true + -- Elaborate Lean blocks first, so inlines in prior blocks can refer to them - let blocks ← - if cfg.keep then - prioritizedElab (isLeanBlock ·) elabBlock contents - else - withoutModifyingEnv <| prioritizedElab (isLeanBlock ·) elabBlock contents + -- Also accumulate text of lean blocks. + let exampleCode := prioritizedElab accumulate (elabBlock ·) contents + |>.run [] + let (blocks, acc) ← + if cfg.keep then exampleCode + else withoutModifyingEnv <| exampleCode + let liveLinkContent := if acc = [] then none else some (renderExampleContent acc) -- Examples are represented using the first block to hold the description. Storing it in the JSON -- entails repeated (de)serialization. - pure #[← ``(Block.other (Block.example $(quote descriptionString) $(quote cfg.tag) (opened := $(quote cfg.opened))) + pure #[← ``(Block.other (Block.example $(quote descriptionString) $(quote cfg.tag) (opened := $(quote cfg.opened)) $(quote liveLinkContent)) #[Block.para #[$description,*], $blocks,*])] @[block_extension «example»] def example.descr : BlockDescr where traverse id data contents := do - match FromJson.fromJson? data (α := String × Option String × Bool × Option Tag) with + match FromJson.fromJson? data (α := ExampleBlockJson) with | .error e => logError s!"Error deserializing example tag: {e}"; pure none - | .ok (descrString, none, _, _) => do + | .ok (descrString, none, _, _, _) => do modify (·.saveDomainObject ``examples descrString id) pure none - | .ok (descrString, some x, opened, none) => + | .ok (descrString, some x, opened, none, liveText) => modify (·.saveDomainObject ``examples descrString id) let path ← (·.path) <$> read let tag ← Verso.Genre.Manual.externalTag id path x - pure <| some <| Block.other {Block.example descrString none false with id := some id, data := toJson (some x, opened, some tag)} contents - | .ok (descrString, some _, _, some _) => + pure <| some <| Block.other {Block.example descrString none false liveText with + id := some id, + data := toJson (some x, opened, some tag)} contents -- Is this line reachable? + | .ok (descrString, some _, _, some _, liveText) => modify (·.saveDomainObject ``examples descrString id) pure none toTeX := @@ -130,21 +173,37 @@ def example.descr : BlockDescr where else let .para description := blocks[0] | HtmlT.logError "Malformed example - description not paragraph"; pure .empty - let (descrString, opened) ← - match FromJson.fromJson? data (α := String × Option String × Bool × Option Tag) with - | .error e => HtmlT.logError s!"Error deserializing example data: {e}"; pure ("", false) - | .ok (descrString, _, opened, _) => pure (descrString, opened) + let (descrString, opened, liveText) ← + match FromJson.fromJson? data (α := ExampleBlockJson) with + | .error e => HtmlT.logError s!"Error deserializing example data {data}: {e}"; pure ("", false, none) + | .ok (descrString, _, opened, _, liveText) => pure (descrString, opened, liveText) let xref ← HtmlT.state let ctxt ← HtmlT.context let mut attrs := xref.htmlId id if opened then attrs := attrs.push ("open", "") withReader (fun ρ => { ρ with definitionIds := xref.definitionIds ctxt, codeOptions.definitionsAsTargets := true}) do + let liveLink := match liveText with + | .none => Output.Html.empty + | .some content => + let href := "https://live.lean-lang.org/#codez=" ++ lzCompress content + {{
"Live ↪"
}} + -- TODO(https://github.com/leanprover/verso/issues/569): + -- We compute but do not yet add the liveLink inside + -- the div.example-content below. That is, we consider this + -- "feature-flagged off". + -- + -- We should actually add the link when mechanisms are in place to + -- ensure that + -- * all reference manual examples yield correct code + -- that can be run in a fresh copy of lean + -- * we don't produce stale links pure {{
{{← description.mapM goI}}
{{← blocks.extract 1 blocks.size |>.mapM goB}} + -- {{liveLink}}
}} @@ -214,6 +273,7 @@ r#".example { } .example-content { padding: 0 var(--verso--box-padding) var(--verso--box-padding); + position: relative; } .example-content > :first-child { margin-top: 0; @@ -224,6 +284,20 @@ r#".example { .example .hl.lean.block { overflow-x: auto; } +.live-link { + font-family: var(--verso-structure-font-family); + position: absolute; + bottom: 0px; + right: 0px; + padding: 0.5rem; + border-top: 1px solid #98B2C0; + border-left: 1px solid #98B2C0; + border-top-left-radius: 0.5rem; +} +.live-link a { + text-decoration: none; + color: var(--lean-blue); +} "# ] diff --git a/Manual/Meta/LzCompress.lean b/Manual/Meta/LzCompress.lean new file mode 100644 index 00000000..063dc075 --- /dev/null +++ b/Manual/Meta/LzCompress.lean @@ -0,0 +1,236 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Jason Reed +-/ +import Std.Data.HashMap + +def keyStrBase64 := "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/=" + +def getCharFromInt (n : Nat) : Char := keyStrBase64.get ⟨n⟩ + +open Std + +/-! +This code was adapted from https://github.com/pieroxy/lz-string +which was distributed under the MIT License as given below. + +In its current state it is quite imperative and not particularly +idiomatic lean. The reason for using this code at all is to match the +compressed strings that lean4web uses. + +MIT License + +Copyright (c) 2013 Pieroxy pieroxy@pieroxy.net + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + +-/ +def compress (uncompressed : String) + (bitsPerChar : Nat) + (getCharFromInt : Nat → Char) : String := Id.run do + if uncompressed.isEmpty then + return "" + + let mut dictionary : HashMap String Nat := {} + let mut dictionaryToCreate : HashMap String Bool := {} + + let mut wc : String := "" + let mut w : String := "" + let mut enlargeIn : Nat := 2 + let mut dictSize : Nat := 3 + let mut numBits : Nat := 2 + let mut data : Array Char := #[] + let mut data_val : Nat := 0 + let mut data_position : Nat := 0 + + for c in uncompressed.toList.map toString do + if !dictionary.contains c then + dictionary := dictionary.insert c dictSize + dictSize := dictSize + 1 + dictionaryToCreate := dictionaryToCreate.insert c true + wc := w ++ c + if dictionary.contains wc then + w := wc + else + if dictionaryToCreate.contains w then + let code := w.get! 0 |>.toNat + if code < 256 then + for _ in [:numBits] do + data_val := data_val <<< 1 + if data_position == bitsPerChar - 1 then + data := data.push (getCharFromInt data_val) + data_position := 0 + data_val := 0 + else + data_position := data_position + 1 + let mut value := code + for _ in [0:8] do + data_val := (data_val <<< 1) ||| (value &&& 1) + if data_position == bitsPerChar - 1 then + data := data.push (getCharFromInt data_val) + data_position := 0 + data_val := 0 + else + data_position := data_position + 1 + value := value >>> 1 + else + let mut value := 1 + for _ in [:numBits] do + data_val := (data_val <<< 1) ||| value + if data_position == bitsPerChar - 1 then + data := data.push (getCharFromInt data_val) + data_position := 0 + data_val := 0 + else + data_position := data_position + 1 + value := 0 + let mut value' := w.get! 0 |> Char.toNat + for _ in [0:16] do + data_val := (data_val <<< 1) ||| (value' &&& 1) + if data_position == bitsPerChar - 1 then + data := data.push (getCharFromInt data_val) + data_position := 0 + data_val := 0 + else + data_position := data_position + 1 + value' := value' >>> 1 + enlargeIn := enlargeIn - 1 + if enlargeIn == 0 then + enlargeIn := Nat.pow 2 numBits + numBits := numBits + 1 + dictionaryToCreate := dictionaryToCreate.erase w + else + let mut value := dictionary.get! w + for _ in [:numBits] do + data_val := (data_val <<< 1) ||| (value &&& 1) + if data_position == bitsPerChar - 1 then + data := data.push (getCharFromInt data_val) + data_position := 0 + data_val := 0 + else + data_position := data_position + 1 + value := value >>> 1 + enlargeIn := enlargeIn - 1 + if enlargeIn == 0 then + enlargeIn := Nat.pow 2 numBits + numBits := numBits + 1 + dictionary := dictionary.insert wc dictSize + dictSize := dictSize + 1 + w := c + + -- Output the code for _w if not empty + if !w.isEmpty then + if dictionaryToCreate.contains w then + let code := w.get! 0 |>.toNat + if code < 256 then + for _ in [:numBits] do + data_val := data_val <<< 1 + if data_position == bitsPerChar - 1 then + data := data.push (getCharFromInt data_val) + data_position := 0 + data_val := 0 + else + data_position := data_position + 1 + let mut value := code + for _ in [0:8] do + data_val := (data_val <<< 1) ||| (value &&& 1) + if data_position == bitsPerChar - 1 then + data := data.push (getCharFromInt data_val) + data_position := 0 + data_val := 0 + else + data_position := data_position + 1 + value := value >>> 1 + else + let mut value := 1 + for _ in [:numBits] do + data_val := (data_val <<< 1) ||| value + if data_position == bitsPerChar - 1 then + data := data.push (getCharFromInt data_val) + data_position := 0 + data_val := 0 + else + data_position := data_position + 1 + value := 0 + let mut value' := code + for _ in [0:16] do + data_val := (data_val <<< 1) ||| (value' &&& 1) + if data_position == bitsPerChar - 1 then + data := data.push (getCharFromInt data_val) + data_position := 0 + data_val := 0 + else + data_position := data_position + 1 + value' := value' >>> 1 + enlargeIn := enlargeIn - 1 + if enlargeIn == 0 then + enlargeIn := Nat.pow 2 numBits + numBits := numBits + 1 + dictionaryToCreate := dictionaryToCreate.erase w + else + let mut value := dictionary.get! w + for _ in [:numBits] do + data_val := (data_val <<< 1) ||| (value &&& 1) + if data_position == bitsPerChar - 1 then + data := data.push (getCharFromInt data_val) + data_position := 0 + data_val := 0 + else + data_position := data_position + 1 + value := value >>> 1 + enlargeIn := enlargeIn - 1 + if enlargeIn == 0 then + enlargeIn := Nat.pow 2 numBits + numBits := numBits + 1 + + -- End of stream marker + let mut value := 2 + for _ in [:numBits] do + data_val := (data_val <<< 1) ||| (value &&& 1) + if data_position == bitsPerChar - 1 then + data := data.push (getCharFromInt data_val) + data_position := 0 + data_val := 0 + else + data_position := data_position + 1 + value := value >>> 1 + + -- Flush last char + let mut loop := true + while loop do + data_val := data_val <<< 1 + if data_position == bitsPerChar - 1 then + data := data.push (getCharFromInt data_val) + loop := false + else + data_position := data_position + 1 + + return String.mk data.toList + +def lzCompress (uncompressed : String) := compress uncompressed 6 getCharFromInt + +/-- +info: "JYWwDg9gTgLgBAWQIYwBYBtgCMB0AZCAc2AGMcAhJAZ1LgFo64traAzJEmKuYAOznRFSAKAZw0AU2gSQ3PnDwSkvAOTcQKVDJSlumLFCRQAnsNGNF8AApxlAEzgBFJhPFQArhLrt0VV1RgUGQleLmEANyNgJCx0VwAKG2cALjgrKAgwAEozMQAVLThWCHRBAHc+Qh5uJCYWEjgoCSp3dHh5QWISYQkADyRwOLhUgBq4RLhAciInLLhAFMI4MZtACiJFp2GAXiZTOHpGYC44MAyIVmrbdCakO2MefkVlNTgNSRfdAWxDE2Fdvo54XgQGAAfXswOguUYAAkJE1zsogVooHUaA0mi02ncBEJun9Bq5RuMVjN5msbNMxiktlgdrYwGB0MYAPx7OBlVwkZRwPxGEioIrQcSFY4QU5YyQfAxGWlidlwTn8JC+CCNCQMjiuAAGSHpjKZmrZB35B24EHcMDA5uEQA" +-/ +#guard_msgs in +#eval lzCompress r#"import Mathlib.Logic.Basic -- basic facts in logic +-- theorems in Lean's mathematics library + +-- Let P and Q be true-false statements +variable (P Q : Prop) + +-- The following is a basic result in logic +example : ¬ (P ∧ Q) ↔ ¬ P ∨ ¬ Q := by + -- its proof is already in Lean's mathematics library + exact not_and_or + +-- Here is another basic result in logic +example : ¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q := by + apply? -- we can search for the proof in the library + -- we can also replace `apply?` with its output +"# diff --git a/Manual/Monads.lean b/Manual/Monads.lean index f7ded578..8cbad4f9 100644 --- a/Manual/Monads.lean +++ b/Manual/Monads.lean @@ -134,11 +134,11 @@ def LenList.diagonal (square : LenList n (LenList n α)) : LenList n α := lengthOk := by simp } ``` +:::: ```lean -show end ``` -:::: :::::