Compare commits

..

2 Commits

Author SHA1 Message Date
Joshua Potter 870a01c6eb Polish further. 2023-11-12 19:19:56 -07:00
Joshua Potter a371cbb6f4 Embed latex proof for finite domain and range size. 2023-11-12 18:29:40 -07:00
80 changed files with 7177 additions and 425 deletions

3
.envrc
View File

@ -1,3 +0,0 @@
#!/usr/bin/env bash
use flake

7
.gitignore vendored
View File

@ -4,7 +4,6 @@ lakefile.olean
lake-packages
_target
leanpkg.path
.lake/
# TeX
*.aux
@ -22,9 +21,3 @@ leanpkg.path
*.synctex.gz
*.toc
.*.lb
# direnv
.direnv/
# nix
result

View File

@ -50,7 +50,7 @@ theorem exercise_4c (x y : )
: ⌊x + y⌋ = ⌊x⌋ + ⌊y⌋ ⌊x + y⌋ = ⌊x⌋ + ⌊y⌋ + 1 := by
have hx : x = Int.floor x + Int.fract x := Eq.symm (add_eq_of_eq_sub' rfl)
have hy : y = Int.floor y + Int.fract y := Eq.symm (add_eq_of_eq_sub' rfl)
by_cases h : Int.fract x + Int.fract y < 1
by_cases Int.fract x + Int.fract y < 1
· refine Or.inl ?_
rw [Int.floor_eq_iff]
simp only [Int.cast_add]

View File

@ -1,5 +1,5 @@
import Common.Set
import Mathlib.Data.Real.Archimedean
import Mathlib.Data.Real.Basic
/-! # Apostol.Chapter_I_03

View File

@ -481,7 +481,7 @@ theorem exercise_1_2_2b_iii {k : } (h : Odd k)
exact absurd hr hk
unfold σ
rw [hn₁]
simp only [Nat.add_eq, add_zero, imp_false, not_not]
simp only [Nat.add_eq, add_zero, not_forall, exists_prop, and_true]
exact exercise_1_2_2b_i False Q hn₂
end Exercise_1_2_2

View File

@ -616,7 +616,7 @@ lemma right_diff_eq_insert_one_three : A \ (B \ C) = {1, 3} := by
rw [hy] at hz
unfold Membership.mem Set.instMembershipSet Set.Mem at hz
unfold singleton Set.instSingletonSet Set.singleton setOf at hz
simp at hz
simp only at hz
· intro hy
refine ⟨Or.inr (Or.inr hy), ?_⟩
intro hz

View File

@ -542,7 +542,7 @@ theorem exercise_3_1 {x y z u v w : }
· rw [hx, hy, hz, hu, hv, hw]
simp
· rw [hy, hv]
simp
simp only
/-- ### Exercise 3.2a

View File

@ -702,7 +702,7 @@ theorem exercise_4_17 (m n p : )
| zero => calc m ^ (n + 0)
_ = m ^ n := rfl
_ = m ^ n * 1 := by rw [right_mul_id]
_ = m ^ n * m ^ 0 := by rfl
_ = m ^ n * m ^ 0 := rfl
| succ p ih => calc m ^ (n + p.succ)
_ = m ^ (n + p).succ := rfl
_ = m ^ (n + p) * m := rfl

View File

@ -512,7 +512,7 @@ theorem corollary_6d_b
]
refine ⟨1, ?_⟩
intro x nx
simp only [mul_eq_one, OfNat.ofNat_ne_one, false_and] at nx
simp only [mul_eq_one, false_and] at nx
/-- ### Corollary 6E
@ -935,23 +935,76 @@ natural numbers `m, n ∈ ω` such that `dom f ≈ m`, `ran f ≈ n`, and `m ≥
theorem finite_dom_ran_size [Nonempty α] {A B : Set α}
(hA : Set.Finite A) (hB : Set.Finite B) (hf : Set.MapsTo f A B)
: ∃ m n : , A ≈ Set.Iio m ∧ f '' A ≈ Set.Iio n ∧ m ≥ n := by
/-
> Let `A` and `B` be finite sets and `f : A → B` be a function. By definition of
> finite sets, there exists natural numbers `m, p ∈ ω` such that `A ≈ m` and
> `B ≈ p`. By definition of the domain of a function, `dom f = A`. Thus
> `dom f ≈ m`.
-/
have ⟨m, hm⟩ := Set.finite_iff_equinumerous_nat.mp hA
have ⟨p, hp⟩ := Set.finite_iff_equinumerous_nat.mp hB
/-
> By *Theorem 6A*, there exists a one-to-one correspondence `g` between `m` and
> `dom f = A`.
-/
have ⟨g, hg⟩ := Set.equinumerous_symm hm
/-
> For all `y ∈ ran f`, consider `f⁻¹⟦{y}⟧`. Let
>
> `A_y = {x ∈ m | f(g(x)) = y}`.
-/
let A_y y := { x ∈ Set.Iio m | f (g x) = y }
have hA₁ : ∀ y ∈ B, A_y y ≈ f ⁻¹' {y} := by
/-
> Since `g` is a one-to-one correspondence, it follows that `A_y ≈ f⁻¹⟦{y}⟧`.
-/
have hA₁ : ∀ y, y ∈ f '' A → A_y y ≈ A ∩ f ⁻¹' {y} := by
intro y hy
refine ⟨fun x => g x, ?_, ?_, ?_⟩
· -- `Set.MapsTo`
intro x hx
simp only [Set.mem_Iio, Set.mem_setOf_eq, Set.mem_preimage, Set.mem_singleton_iff] at hx ⊢
exact ⟨hg.left hx.left, hx.right⟩
· -- `Set.InjOn`
intro x₁ hx₁ x₂ hx₂ hf
exact hg.right.left hx₁.left hx₂.left hf
· -- `Set.SurjOn`
unfold Set.SurjOn Set.preimage Set.image
rw [Set.subset_def]
simp only [Set.mem_singleton_iff, Set.mem_inter_iff, Set.mem_setOf_eq, Set.mem_Iio]
intro x ⟨hx₁, hx₂⟩
have hx₃ := hg.right.right hx₁
simp only [Set.mem_image, Set.mem_Iio] at hx₃
have ⟨z, hz⟩ := hx₃
exact ⟨z, ⟨hz.left, hz.right ▸ hx₂⟩, hz.right⟩
/-
> Since `A_y` is a nonempty subset of natural numbers, the
> *Well Ordering of `ω`* implies there exists a least element, say `q_y`.
-/
have hA₂ : ∀ y, y ∈ f '' A → Set.Nonempty (A_y y) := by
intro y hy
unfold Set.Nonempty
simp only [Set.mem_image, Set.mem_Iio, Set.mem_setOf_eq] at hy ⊢
have ⟨x, hx⟩ := hy
have ⟨z, hz⟩ := hg.right.right hx.left
simp only [Set.mem_Iio] at hz
exact ⟨z, hz.left, hz.right ▸ hx.right⟩
have hA₃ : ∀ y, y ∈ f '' A → ∃ q, q ∈ A_y y ∧ ∀ p ∈ A_y y, q ≤ p := by
sorry
have hA₂ : ∀ y ∈ B, Set.Nonempty (A_y y) := by
sorry
have hA₃ : ∀ y ∈ B, ∃ q : , ∀ p ∈ A_y y, q ≤ p := by
sorry
let C := { q | ∃ y ∈ B, ∀ p ∈ A_y y, q ≤ p }
/-
> Define `C = {q_y | y ∈ ran f}`.
-/
let C := { q | ∃ y, y ∈ f '' A ∧ (∀ p ∈ A_y y, q ≤ p) }
/-
> Thus `h : C → ran f` given by `h(x) = f(g(x))` is a one-to-on ecorrespondence
> between `C` and `ran f` by construction. That is, `C ≈ ran f`.
-/
let h x := f (g x)
have hh : C ≈ f '' A := by
sorry
/-
> By *Lemma 6F*, there exists some `n ≤ m` such that `C ≈ n`. By *Theorem 6A*,
> `n ≈ ran f`.
-/
sorry
/-- ### Set Difference Size
@ -992,7 +1045,7 @@ lemma sdiff_size_aux [DecidableEq α] [Nonempty α]
simp only [Set.diff_empty]
exact hA
rw [this]
refine ⟨by simp, hB', Set.equinumerous_emptyset_emptyset⟩
refine ⟨trivial, hB', Set.equinumerous_emptyset_emptyset⟩
| succ m ih =>
/-
> #### (ii)

View File

@ -162,7 +162,7 @@ theorem length_zipWith_self_tail_eq_length_sub_one
rw [length_zipWith]
simp only [length_cons, ge_iff_le, min_eq_right_iff]
show length as ≤ length as + 1
simp only [le_add_iff_nonneg_right, zero_le]
simp only [le_add_iff_nonneg_right]
/--
The output `List` of a `zipWith` is nonempty **iff** both of its inputs are

View File

@ -9,4 +9,23 @@ If `n < m⁺`, then `n < m` or `n = m`.
theorem lt_or_eq_of_lt {n m : Nat} (h : n < m.succ) : n < m n = m :=
lt_or_eq_of_le (lt_succ.mp h)
end Nat
/--
The following cancellation law holds for `m`, `n`, and `p` in `ω`:
```
m ⬝ p = n ⬝ p ∧ p ≠ 0 → m = n
```
-/
theorem mul_right_cancel (m n p : ) (hp : 0 < p) : m * p = n * p → m = n := by
intro hmn
match @trichotomous LT.lt _ m n with
| Or.inl h =>
have : m * p < n * p := Nat.mul_lt_mul_of_pos_right h hp
rw [hmn] at this
simp at this
| Or.inr (Or.inl h) => exact h
| Or.inr (Or.inr h) =>
have : n * p < m * p := Nat.mul_lt_mul_of_pos_right h hp
rw [hmn] at this
simp at this
end Nat

View File

@ -1,5 +1,6 @@
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Real.Archimedean
import Mathlib.Data.Real.Basic
import Mathlib.Data.Finset.Basic
/-! # Common.Real.Floor
@ -144,4 +145,4 @@ theorem floor_mul_eq_sum_range_floor_add_index_div (n : ) (x : )
-- Close out goal by showing left- and right-hand side equal a common value.
rw [hlhs, hrhs]
end Real.Floor
end Real.Floor

9
DocGen4.lean Normal file
View File

@ -0,0 +1,9 @@
/-
Copyright (c) 2021 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import DocGen4.Process
import DocGen4.Load
import DocGen4.Output
import DocGen4.LeanInk

7
DocGen4/LeanInk.lean Normal file
View File

@ -0,0 +1,7 @@
/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import DocGen4.LeanInk.Process
import DocGen4.LeanInk.Output

215
DocGen4/LeanInk/Output.lean Normal file
View File

@ -0,0 +1,215 @@
/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving, Xubai Wang
-/
import DocGen4.Output.Base
import DocGen4.Output.ToHtmlFormat
import Lean.Data.Json
import LeanInk.Annotation.Alectryon
namespace LeanInk.Annotation.Alectryon
open DocGen4 Output
open scoped DocGen4.Jsx
structure AlectryonContext where
counter : Nat
abbrev AlectryonT := StateT AlectryonContext
abbrev AlectryonM := AlectryonT HtmlM
def getNextButtonLabel : AlectryonM String := do
let val ← get
let newCounter := val.counter + 1
set { val with counter := newCounter }
return s!"plain-lean4-lean-chk{val.counter}"
def TypeInfo.toHtml (tyi : TypeInfo) : AlectryonM Html := do
pure
<div class="alectryon-type-info-wrapper">
<small class="alectryon-type-info">
<div class="alectryon-goals">
<blockquote class="alectryon-goal">
<div class="goal-hyps">
<span class="hyp-type">
<var>{tyi.name}</var>
<b>: </b>
<span>[← DocGen4.Output.infoFormatToHtml tyi.type.fst]</span>
</span>
</div>
</blockquote>
</div>
</small>
</div>
def Token.processSemantic (t : Token) : Html :=
match t.semanticType with
| some "Name.Attribute" => <span class="na">{t.raw}</span>
| some "Name.Variable" => <span class="nv">{t.raw}</span>
| some "Keyword" => <span class="k">{t.raw}</span>
| _ => Html.text t.raw
def Token.toHtml (t : Token) : AlectryonM Html := do
-- Right now t.link is always none from LeanInk, ignore it
-- TODO: render docstring
let mut parts := #[]
if let some tyi := t.typeinfo then
parts := parts.push <| ← tyi.toHtml
parts := parts.push t.processSemantic
pure
-- TODO: Show rest of token
<span class="alectryon-token">
[parts]
</span>
def Contents.toHtml : Contents → AlectryonM Html
| .string value =>
pure
<span class="alectryon-wsp">
{value}
</span>
| .experimentalTokens values => do
let values ← values.mapM Token.toHtml
pure
<span class="alectryon-wsp">
[values]
</span>
def Hypothesis.toHtml (h : Hypothesis) : AlectryonM Html := do
let mut hypParts := #[<var>[h.names.intersperse ", " |>.map Html.text |>.toArray]</var>]
if h.body.snd != "" then
hypParts := hypParts.push
<span class="hyp-body">
<b>:= </b>
<span>[← infoFormatToHtml h.body.fst]</span>
</span>
hypParts := hypParts.push
<span class="hyp-type">
<b>: </b>
<span >[← infoFormatToHtml h.type.fst]</span>
</span>
pure
<span>
[hypParts]
</span>
def Goal.toHtml (g : Goal) : AlectryonM Html := do
let mut hypotheses := #[]
for hyp in g.hypotheses do
let rendered ← hyp.toHtml
hypotheses := hypotheses.push rendered
hypotheses := hypotheses.push <br/>
let conclusionHtml ←
match g.conclusion with
| .typed info _ => infoFormatToHtml info
| .untyped str => pure #[Html.text str]
pure
<blockquote class="alectryon-goal">
<div class="goal-hyps">
[hypotheses]
</div>
<span class="goal-separator">
<hr><span class="goal-name">{g.name}</span></hr>
</span>
<div class="goal-conclusion">
[conclusionHtml]
</div>
</blockquote>
def Message.toHtml (m : Message) : AlectryonM Html := do
pure
<blockquote class="alectryon-message">
-- TODO: This might have to be done in a fancier way
{m.contents}
</blockquote>
def Sentence.toHtml (s : Sentence) : AlectryonM Html := do
let messages :=
if s.messages.size > 0 then
#[
<div class="alectryon-messages">
[← s.messages.mapM Message.toHtml]
</div>
]
else
#[]
let goals :=
if s.goals.size > 0 then
-- TODO: Alectryon has a "alectryon-extra-goals" here, implement it
#[
<div class="alectryon-goals">
[← s.goals.mapM Goal.toHtml]
</div>
]
else
#[]
let buttonLabel ← getNextButtonLabel
pure
<span class="alectryon-sentence">
<input class="alectryon-toggle" id={buttonLabel} style="display: none" type="checkbox"/>
<label class="alectryon-input" for={buttonLabel}>
{← s.contents.toHtml}
</label>
<small class="alectryon-output">
[messages]
[goals]
</small>
</span>
def Text.toHtml (t : Text) : AlectryonM Html := t.contents.toHtml
def Fragment.toHtml : Fragment → AlectryonM Html
| .text value => value.toHtml
| .sentence value => value.toHtml
def baseHtml (content : Array Html) : AlectryonM Html := do
let banner :=
<div «class»="alectryon-banner">
Built with <a href="https://github.com/leanprover/doc-gen4">doc-gen4</a>, running Lean4.
Bubbles (<span class="alectryon-bubble"></span>) indicate interactive fragments: hover for details, tap to reveal contents.
Use <kbd>Ctrl+↑</kbd> <kbd>Ctrl+↓</kbd> to navigate, <kbd>Ctrl+🖱️</kbd> to focus.
On Mac, use <kbd>Cmd</kbd> instead of <kbd>Ctrl</kbd>.
</div>
pure
<html lang="en" class="alectryon-standalone">
<head>
<meta charset="UTF-8"/>
<meta name="viewport" content="width=device-width, initial-scale=1"/>
<link rel="stylesheet" href={s!"{← getRoot}src/alectryon.css"}/>
<link rel="stylesheet" href={s!"{← getRoot}src/pygments.css"}/>
<link rel="stylesheet" href={s!"{← getRoot}src/docutils_basic.css"}/>
<link rel="shortcut icon" href={s!"{← getRoot}favicon.ico"}/>
<script defer="true" src={s!"{← getRoot}src/alectryon.js"}></script>
</head>
<body>
<article class="alectryon-root alectryon-centered">
{banner}
<pre class="alectryon-io highlight">
[content]
</pre>
</article>
</body>
</html>
def annotationsToFragments (as : List Annotation.Annotation) : AnalysisM (List Fragment) := do
let config ← read
annotateFileWithCompounds [] config.inputFileContents as
-- TODO: rework monad mess
def renderAnnotations (as : List Annotation.Annotation) : HtmlT AnalysisM Html := do
let fs ← annotationsToFragments as
let (html, _) ← fs.mapM Fragment.toHtml >>= (baseHtml ∘ List.toArray) |>.run { counter := 0 }
return html
end LeanInk.Annotation.Alectryon

View File

@ -0,0 +1,57 @@
/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
import LeanInk.Analysis
import LeanInk.Annotation
import DocGen4.LeanInk.Output
import DocGen4.Output.Base
namespace DocGen4.Process.LeanInk
open Lean
open DocGen4.Output
def docGenOutput (as : List LeanInk.Annotation.Annotation) : HtmlT LeanInk.AnalysisM UInt32 := do
let some modName ← getCurrentName | unreachable!
let srcHtml ← LeanInk.Annotation.Alectryon.renderAnnotations as
let srcDir := moduleNameToDirectory srcBasePath modName
let srcPath := moduleNameToFile srcBasePath modName
IO.FS.createDirAll srcDir
IO.FS.writeFile srcPath srcHtml.toString
return 0
def execAuxM : HtmlT LeanInk.AnalysisM UInt32 := do
let ctx ← readThe SiteContext
let baseCtx ← readThe SiteBaseContext
let outputFn := (docGenOutput · |>.run ctx baseCtx)
return ← LeanInk.Analysis.runAnalysis {
name := "doc-gen4"
genOutput := outputFn
}
def execAux (config : LeanInk.Configuration) : HtmlT IO UInt32 := do
execAuxM.run (← readThe SiteContext) (← readThe SiteBaseContext) |>.run config
@[implemented_by enableInitializersExecution]
private def enableInitializersExecutionWrapper : IO Unit := return ()
def runInk (sourceFilePath : System.FilePath) : HtmlT IO Unit := do
let contents ← IO.FS.readFile sourceFilePath
let config := {
inputFilePath := sourceFilePath
inputFileContents := contents
lakeFile := none
verbose := false
prettifyOutput := true
experimentalTypeInfo := true
experimentalDocString := true
experimentalSemanticType := true
}
enableInitializersExecutionWrapper
if (← execAux config) != 0 then
throw <| IO.userError s!"Analysis for \"{sourceFilePath}\" failed!"
end DocGen4.Process.LeanInk

43
DocGen4/Load.lean Normal file
View File

@ -0,0 +1,43 @@
/-
Copyright (c) 2021 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
import DocGen4.Process
import Lean.Data.HashMap
namespace DocGen4
open Lean System IO
def envOfImports (imports : Array Name) : IO Environment := do
importModules (imports.map (Import.mk · false)) Options.empty
def loadInit (imports : Array Name) : IO Hierarchy := do
let env ← envOfImports imports
pure <| Hierarchy.fromArray env.header.moduleNames
/--
Load a list of modules from the current Lean search path into an `Environment`
to process for documentation.
-/
def load (task : Process.AnalyzeTask) : IO (Process.AnalyzerResult × Hierarchy) := do
initSearchPath (← findSysroot)
let env ← envOfImports task.getLoad
let config := {
-- TODO: parameterize maxHeartbeats
maxHeartbeats := 100000000,
options := ⟨[(`pp.tagAppFns, true)]⟩,
-- TODO: Figure out whether this could cause some bugs
fileName := default,
fileMap := default,
}
Prod.fst <$> Meta.MetaM.toIO (Process.process task) config { env := env } {} {}
def loadCore : IO (Process.AnalyzerResult × Hierarchy) := do
load <| .loadAll #[`Init, `Lean, `Lake]
end DocGen4

152
DocGen4/Output.lean Normal file
View File

@ -0,0 +1,152 @@
/-
Copyright (c) 2021 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
import DocGen4.Process
import DocGen4.Output.Base
import DocGen4.Output.Index
import DocGen4.Output.Module
import DocGen4.Output.NotFound
import DocGen4.Output.Find
import DocGen4.Output.SourceLinker
import DocGen4.Output.Search
import DocGen4.Output.ToJson
import DocGen4.Output.FoundationalTypes
import DocGen4.LeanInk.Process
import Lean.Data.HashMap
namespace DocGen4
open Lean IO System Output Process
def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
let findBasePath := basePath / "find"
-- Base structure
FS.createDirAll basePath
FS.createDirAll findBasePath
FS.createDirAll srcBasePath
FS.createDirAll declarationsBasePath
-- All the doc-gen static stuff
let indexHtml := ReaderT.run index config |>.toString
let notFoundHtml := ReaderT.run notFound config |>.toString
let foundationalTypesHtml := ReaderT.run foundationalTypes config |>.toString
let navbarHtml := ReaderT.run navbar config |>.toString
let searchHtml := ReaderT.run search config |>.toString
let docGenStatic := #[
("style.css", styleCss),
("declaration-data.js", declarationDataCenterJs),
("color-scheme.js", colorSchemeJs),
("nav.js", navJs),
("jump-src.js", jumpSrcJs),
("expand-nav.js", expandNavJs),
("how-about.js", howAboutJs),
("search.html", searchHtml),
("search.js", searchJs),
("mathjax-config.js", mathjaxConfigJs),
("instances.js", instancesJs),
("importedBy.js", importedByJs),
("index.html", indexHtml),
("foundational_types.html", foundationalTypesHtml),
("404.html", notFoundHtml),
("navbar.html", navbarHtml)
]
for (fileName, content) in docGenStatic do
FS.writeFile (basePath / fileName) content
let findHtml := ReaderT.run find { config with depthToRoot := 1 } |>.toString
let findStatic := #[
("index.html", findHtml),
("find.js", findJs)
]
for (fileName, content) in findStatic do
FS.writeFile (findBasePath / fileName) content
let alectryonStatic := #[
("alectryon.css", alectryonCss),
("alectryon.js", alectryonJs),
("docutils_basic.css", docUtilsCss),
("pygments.css", pygmentsCss)
]
for (fileName, content) in alectryonStatic do
FS.writeFile (srcBasePath / fileName) content
def htmlOutputDeclarationDatas (result : AnalyzerResult) : HtmlT IO Unit := do
for (_, mod) in result.moduleInfo.toArray do
let jsonDecls ← Module.toJson mod
FS.writeFile (declarationsBasePath / s!"declaration-data-{mod.name}.bmp") (toJson jsonDecls).compress
def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (gitUrl? : Option String) (ink : Bool) : IO Unit := do
let config : SiteContext := {
result := result,
sourceLinker := ← SourceLinker.sourceLinker gitUrl?
leanInkEnabled := ink
}
FS.createDirAll basePath
FS.createDirAll declarationsBasePath
let some p := (← IO.getEnv "LEAN_SRC_PATH") | throw <| IO.userError "LEAN_SRC_PATH not found in env"
let sourceSearchPath := System.SearchPath.parse p
discard <| htmlOutputDeclarationDatas result |>.run config baseConfig
for (modName, module) in result.moduleInfo.toArray do
let fileDir := moduleNameToDirectory basePath modName
let filePath := moduleNameToFile basePath modName
-- path: 'basePath/module/components/till/last.html'
-- The last component is the file name, so we drop it from the depth to root.
let baseConfig := { baseConfig with
depthToRoot := modName.components.dropLast.length
currentName := some modName
}
let moduleHtml := moduleToHtml module |>.run config baseConfig
FS.createDirAll fileDir
FS.writeFile filePath moduleHtml.toString
if ink then
if let some inputPath ← Lean.SearchPath.findModuleWithExt sourceSearchPath "lean" module.name then
-- path: 'basePath/src/module/components/till/last.html'
-- The last component is the file name, however we are in src/ here so dont drop it this time
let baseConfig := {baseConfig with depthToRoot := modName.components.length }
Process.LeanInk.runInk inputPath |>.run config baseConfig
def getSimpleBaseContext (hierarchy : Hierarchy) : IO SiteBaseContext := do
return {
depthToRoot := 0,
currentName := none,
hierarchy
}
def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
htmlOutputSetup baseConfig
let mut index : JsonIndex := {}
let mut headerIndex : JsonHeaderIndex := {}
for entry in ← System.FilePath.readDir declarationsBasePath do
if entry.fileName.startsWith "declaration-data-" && entry.fileName.endsWith ".bmp" then
let fileContent ← FS.readFile entry.path
let .ok jsonContent := Json.parse fileContent | unreachable!
let .ok (module : JsonModule) := fromJson? jsonContent | unreachable!
index := index.addModule module |>.run baseConfig
headerIndex := headerIndex.addModule module
let finalJson := toJson index
let finalHeaderJson := toJson headerIndex
-- The root JSON for find
FS.writeFile (declarationsBasePath / "declaration-data.bmp") finalJson.compress
FS.writeFile (declarationsBasePath / "header-data.bmp") finalHeaderJson.compress
/--
The main entrypoint for outputting the documentation HTML based on an
`AnalyzerResult`.
-/
def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (gitUrl? : Option String) (ink : Bool) : IO Unit := do
let baseConfig ← getSimpleBaseContext hierarchy
htmlOutputResults baseConfig result gitUrl? ink
htmlOutputIndex baseConfig
end DocGen4

278
DocGen4/Output/Base.lean Normal file
View File

@ -0,0 +1,278 @@
/-
Copyright (c) 2021 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import DocGen4.Process
import DocGen4.Output.ToHtmlFormat
namespace DocGen4.Output
open scoped DocGen4.Jsx
open Lean System Widget Elab Process
def basePath := FilePath.mk "." / "build" / "doc"
def srcBasePath := basePath / "src"
def declarationsBasePath := basePath / "declarations"
/--
The context used in the `BaseHtmlM` monad for HTML templating.
-/
structure SiteBaseContext where
/--
The module hierarchy as a tree structure.
-/
hierarchy : Hierarchy
/--
How far away we are from the page root, used for relative links to the root.
-/
depthToRoot: Nat
/--
The name of the current module if there is one, there exist a few
pages that don't have a module name.
-/
currentName : Option Name
/--
The context used in the `HtmlM` monad for HTML templating.
-/
structure SiteContext where
/--
The full analysis result from the Process module.
-/
result : AnalyzerResult
/--
A function to link declaration names to their source URLs, usually Github ones.
-/
sourceLinker : Name → Option DeclarationRange → String
/--
Whether LeanInk is enabled
-/
leanInkEnabled : Bool
def setCurrentName (name : Name) (ctx : SiteBaseContext) := {ctx with currentName := some name}
abbrev BaseHtmlT := ReaderT SiteBaseContext
abbrev BaseHtmlM := BaseHtmlT Id
abbrev HtmlT (m) := ReaderT SiteContext (BaseHtmlT m)
abbrev HtmlM := HtmlT Id
def HtmlT.run (x : HtmlT m α) (ctx : SiteContext) (baseCtx : SiteBaseContext) : m α :=
ReaderT.run x ctx |>.run baseCtx
def HtmlM.run (x : HtmlM α) (ctx : SiteContext) (baseCtx : SiteBaseContext) : α :=
ReaderT.run x ctx |>.run baseCtx |>.run
instance [Monad m] : MonadLift HtmlM (HtmlT m) where
monadLift x := do return x.run (← readThe SiteContext) (← readThe SiteBaseContext)
instance [Monad m] : MonadLift BaseHtmlM (BaseHtmlT m) where
monadLift x := do return x.run (← readThe SiteBaseContext)
/--
Obtains the root URL as a relative one to the current depth.
-/
def getRoot : BaseHtmlM String := do
let rec go: Nat -> String
| 0 => "./"
| Nat.succ n' => "../" ++ go n'
let d <- SiteBaseContext.depthToRoot <$> read
return (go d)
def getHierarchy : BaseHtmlM Hierarchy := do return (← read).hierarchy
def getCurrentName : BaseHtmlM (Option Name) := do return (← read).currentName
def getResult : HtmlM AnalyzerResult := do return (← read).result
def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do return (← read).sourceLinker module range
def leanInkEnabled? : HtmlM Bool := do return (← read).leanInkEnabled
/--
If a template is meant to be extended because it for example only provides the
header but no real content this is the way to fill the template with content.
This is untyped so HtmlM and BaseHtmlM can be mixed.
-/
def templateExtends {α β} {m} [Bind m] (base : α → m β) (new : m α) : m β :=
new >>= base
def templateLiftExtends {α β} {m n} [Bind m] [MonadLift n m] (base : α → n β) (new : m α) : m β :=
new >>= (monadLift ∘ base)
/-
Returns the doc-gen4 link to a module `NameExt`.
-/
def moduleNameExtToLink (n : NameExt) : BaseHtmlM String := do
let parts := n.name.components.map Name.toString
return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ "." ++ n.ext.toString
/--
Returns the doc-gen4 link to a module name.
-/
def moduleNameToHtmlLink (n : Name) : BaseHtmlM String :=
moduleNameExtToLink ⟨n, .html⟩
/--
Returns the HTML doc-gen4 link to a module name.
-/
def moduleToHtmlLink (module : Name) : BaseHtmlM Html := do
return <a href={← moduleNameToHtmlLink module}>{module.toString}</a>
/--
Returns the LeanInk link to a module name.
-/
def moduleNameToInkLink (n : Name) : BaseHtmlM String := do
let parts := "src" :: n.components.map Name.toString
return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
/--
Returns the path to the HTML file that contains information about a module.
-/
def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath :=
let parts := n.components.map Name.toString
FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html"
/--
Returns the directory of the HTML file that contains information about a module.
-/
def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
let parts := n.components.dropLast.map Name.toString
basePath / parts.foldl (· / ·) (FilePath.mk ".")
section Static
/-!
The following section contains all the statically included files that
are used in documentation generation, notably JS and CSS ones.
-/
def styleCss : String := include_str "../../static/style.css"
def declarationDataCenterJs : String := include_str "../../static/declaration-data.js"
def colorSchemeJs : String := include_str "../../static/color-scheme.js"
def jumpSrcJs : String := include_str "../../static/jump-src.js"
def navJs : String := include_str "../../static/nav.js"
def expandNavJs : String := include_str "../../static/expand-nav.js"
def howAboutJs : String := include_str "../../static/how-about.js"
def searchJs : String := include_str "../../static/search.js"
def instancesJs : String := include_str "../../static/instances.js"
def importedByJs : String := include_str "../../static/importedBy.js"
def findJs : String := include_str "../../static/find/find.js"
def mathjaxConfigJs : String := include_str "../../static/mathjax-config.js"
def alectryonCss : String := include_str "../../static/alectryon/alectryon.css"
def alectryonJs : String := include_str "../../static/alectryon/alectryon.js"
def docUtilsCss : String := include_str "../../static/alectryon/docutils_basic.css"
def pygmentsCss : String := include_str "../../static/alectryon/pygments.css"
end Static
/--
Returns the doc-gen4 link to a declaration name.
-/
def declNameToLink (name : Name) : HtmlM String := do
let res ← getResult
let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]!
return (← moduleNameToHtmlLink module) ++ "#" ++ name.toString
/--
Returns the HTML doc-gen4 link to a declaration name.
-/
def declNameToHtmlLink (name : Name) : HtmlM Html := do
return <a href={← declNameToLink name}>{name.toString}</a>
/--
Returns the LeanInk link to a declaration name.
-/
def declNameToInkLink (name : Name) : HtmlM String := do
let res ← getResult
let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]!
return (← moduleNameToInkLink module) ++ "#" ++ name.toString
/--
Returns a name splitted into parts.
Together with "break_within" CSS class this helps browser to break a name
nicely.
-/
def breakWithin (name: String) : (Array Html) :=
name.splitOn "."
|> .map (fun (s: String) => <span class="name">{s}</span>)
|> .intersperse "."
|> List.toArray
/--
Returns the HTML doc-gen4 link to a declaration name with "break_within"
set as class.
-/
def declNameToHtmlBreakWithinLink (name : Name) : HtmlM Html := do
return <a class="break_within" href={← declNameToLink name}>
[breakWithin name.toString]
</a>
/--
In Lean syntax declarations the following pattern is quite common:
```
syntax term " + " term : term
```
that is, we place spaces around the operator in the middle. When the
`InfoTree` framework provides us with information about what source token
corresponds to which identifier it will thus say that `" + "` corresponds to
`HAdd.hadd`. This is however not the way we want this to be linked, in the HTML
only `+` should be linked, taking care of this is what this function is
responsible for.
-/
def splitWhitespaces (s : String) : (String × String × String) := Id.run do
let front := "".pushn ' ' <| s.offsetOfPos (s.find (!Char.isWhitespace ·))
let mut s := s.trimLeft
let back := "".pushn ' ' (s.length - s.offsetOfPos (s.find Char.isWhitespace))
s := s.trimRight
(front, s, back)
/--
Turns a `CodeWithInfos` object, that is basically a Lean syntax tree with
information about what the identifiers mean, into an HTML object that links
to as much information as possible.
-/
partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
match i with
| .text t => return #[Html.escape t]
| .append tt => tt.foldlM (fun acc t => do return acc ++ (← infoFormatToHtml t)) #[]
| .tag a t =>
match a.info.val.info with
| Info.ofTermInfo i =>
let cleanExpr := i.expr.consumeMData
match cleanExpr with
| .const name _ =>
-- TODO: this is some very primitive blacklisting but real Blacklisting needs MetaM
-- find a better solution
if (← getResult).name2ModIdx.contains name then
match t with
| .text t =>
let (front, t, back) := splitWhitespaces <| Html.escape t
let elem := <a href={← declNameToLink name}>{t}</a>
return #[Html.text front, elem, Html.text back]
| _ =>
return #[<a href={← declNameToLink name}>[← infoFormatToHtml t]</a>]
else
return #[<span class="fn">[← infoFormatToHtml t]</span>]
| .sort _ =>
match t with
| .text t =>
let sortPrefix :: rest := t.splitOn " " | unreachable!
let sortLink := <a href={s!"{← getRoot}foundational_types.html"}>{sortPrefix}</a>
let mut restStr := String.intercalate " " rest
if restStr.length != 0 then
restStr := " " ++ restStr
return #[sortLink, Html.text restStr]
| _ =>
return #[<a href={s!"{← getRoot}foundational_types.html"}>[← infoFormatToHtml t]</a>]
| _ =>
return #[<span class="fn">[← infoFormatToHtml t]</span>]
| _ => return #[<span class="fn">[← infoFormatToHtml t]</span>]
def baseHtmlHeadDeclarations : BaseHtmlM (Array Html) := do
return #[
<meta charset="UTF-8"/>,
<meta name="viewport" content="width=device-width, initial-scale=1"/>,
<link rel="stylesheet" href={s!"{← getRoot}style.css"}/>,
<link rel="stylesheet" href={s!"{← getRoot}src/pygments.css"}/>,
<link rel="shortcut icon" href={s!"{← getRoot}favicon.ico"}/>,
<link rel="prefetch" href={s!"{← getRoot}/declarations/declaration-data.bmp"} as="image"/>
]
end DocGen4.Output

22
DocGen4/Output/Class.lean Normal file
View File

@ -0,0 +1,22 @@
import DocGen4.Output.Template
import DocGen4.Output.Structure
import DocGen4.Process
namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
open Lean
def classInstancesToHtml (className : Name) : HtmlM Html := do
pure
<details «class»="instances">
<summary>Instances</summary>
<ul id={s!"instances-list-{className}"} class="instances-list"></ul>
</details>
def classToHtml (i : Process.ClassInfo) : HtmlM (Array Html) := do
structureToHtml i
end Output
end DocGen4

View File

@ -0,0 +1,14 @@
import DocGen4.Output.Template
import DocGen4.Output.Class
import DocGen4.Output.Inductive
import DocGen4.Process
namespace DocGen4
namespace Output
def classInductiveToHtml (i : Process.ClassInductiveInfo) : HtmlM (Array Html) := do
inductiveToHtml i
end Output
end DocGen4

View File

@ -0,0 +1,51 @@
import DocGen4.Output.Template
import DocGen4.Output.DocString
import DocGen4.Process
namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
open Lean Widget
/-- This is basically an arbitrary number that seems to work okay. -/
def equationLimit : Nat := 200
def equationToHtml (c : CodeWithInfos) : HtmlM Html := do
return <li class="equation">[← infoFormatToHtml c]</li>
/--
Attempt to render all `simp` equations for this definition. At a size
defined in `equationLimit` we stop trying since they:
- are too ugly to read most of the time
- take too long
-/
def equationsToHtml (i : Process.DefinitionInfo) : HtmlM (Array Html) := do
if let some eqs := i.equations then
let equationsHtml ← eqs.mapM equationToHtml
let filteredEquationsHtml := equationsHtml.filter (·.textLength < equationLimit)
if equationsHtml.size ≠ filteredEquationsHtml.size then
return #[
<details>
<summary>Equations</summary>
<ul class="equations">
<li class="equation">One or more equations did not get rendered due to their size.</li>
[filteredEquationsHtml]
</ul>
</details>
]
else
return #[
<details>
<summary>Equations</summary>
<ul class="equations">
[filteredEquationsHtml]
</ul>
</details>
]
else
return #[]
end Output
end DocGen4

View File

@ -0,0 +1,220 @@
import CMark
import DocGen4.Output.Template
import Lean.Data.Parsec
import UnicodeBasic
open Lean Xml Parser Parsec DocGen4.Process
namespace DocGen4
namespace Output
/-- Auxiliary function for `splitAround`. -/
@[specialize] partial def splitAroundAux (s : String) (p : Char → Bool) (b i : String.Pos) (r : List String) : List String :=
if s.atEnd i then
let r := (s.extract b i)::r
r.reverse
else
let c := s.get i
if p c then
let i := s.next i
splitAroundAux s p i i (c.toString::s.extract b (i-⟨1⟩)::r)
else
splitAroundAux s p b (s.next i) r
/--
Similar to `String.split` in Lean core, but keeps the separater.
e.g. `splitAround "a,b,c" (fun c => c = ',') = ["a", ",", "b", ",", "c"]`
-/
def splitAround (s : String) (p : Char → Bool) : List String := splitAroundAux s p 0 0 []
instance : Inhabited Element := ⟨"", Lean.RBMap.empty, #[]⟩
/-- Parse an array of Xml/Html document from String. -/
def manyDocument : Parsec (Array Element) := many (prolog *> element <* many Misc) <* eof
/--
Generate id for heading elements, with the following rules:
1. Characters in `letter`, `mark`, `number` and `symbol` unicode categories are preserved.
2. Any sequences of Characters in `punctuation`, `separator` and `other` categories are replaced by a single dash.
3. Cases (upper and lower) are preserved.
4. Xml/Html tags are ignored.
-/
partial def xmlGetHeadingId (el : Xml.Element) : String :=
elementToPlainText el |> replaceCharSeq unicodeToDrop "-"
where
elementToPlainText el := match el with
| (Element.Element _ _ contents) =>
"".intercalate (contents.toList.map contentToPlainText)
contentToPlainText c := match c with
| Content.Element el => elementToPlainText el
| Content.Comment _ => ""
| Content.Character s => s
replaceCharSeq pattern replacement s :=
s.split pattern
|>.filter (!·.isEmpty)
|> replacement.intercalate
unicodeToDrop (c : Char) : Bool :=
let cats := [
Unicode.GeneralCategory.P, -- punctuation
Unicode.GeneralCategory.Z, -- separator
Unicode.GeneralCategory.C -- other
]
cats.any (Unicode.isInGeneralCategory c)
/--
This function try to find the given name, both globally and in current module.
For global search, a precise name is need. If the global search fails, the function
tries to find a local one that ends with the given search name.
-/
def nameToLink? (s : String) : HtmlM (Option String) := do
let res ← getResult
if s.endsWith ".lean" && s.contains '/' then
return (← getRoot) ++ s.dropRight 5 ++ ".html"
else if let some name := Lean.Syntax.decodeNameLit ("`" ++ s) then
-- with exactly the same name
if res.name2ModIdx.contains name then
declNameToLink name
-- module name
else if res.moduleNames.contains name then
moduleNameToHtmlLink name
-- find similar name in the same module
else
match (← getCurrentName) with
| some currentName =>
match res.moduleInfo.find! currentName |>.members |> filterDocInfo |>.find? (sameEnd ·.getName name) with
| some info =>
declNameToLink info.getName
| _ => return none
| _ => return none
else
return none
where
-- check if two names have the same ending components
sameEnd n1 n2 :=
List.zip n1.componentsRev n2.componentsRev
|>.all fun ⟨a, b⟩ => a == b
/--
Extend links with following rules:
1. if the link starts with `##`, a name search is used and will panic if not found
2. if the link starts with `#`, it's treated as id link, no modification
3. if the link starts with `http`, it's an absolute one, no modification
4. otherwise it's a relative link, extend it with base url
-/
def extendLink (s : String) : HtmlM String := do
-- for intra doc links
if s.startsWith "##" then
if let some link ← nameToLink? (s.drop 2) then
return link
else
panic! s!"Cannot find {s.drop 2}, only full name and abbrev in current module is supported"
-- for id
else if s.startsWith "#" then
return s
-- for absolute and relative urls
else if s.startsWith "http" then
return s
else return ((← getRoot) ++ s)
/-- Add attributes for heading. -/
def addHeadingAttributes (el : Element) (modifyElement : Element → HtmlM Element) : HtmlM Element := do
match el with
| Element.Element name attrs contents => do
let id := xmlGetHeadingId el
let anchorAttributes := Lean.RBMap.empty
|>.insert "class" "hover-link"
|>.insert "href" s!"#{id}"
let anchor := Element.Element "a" anchorAttributes #[Content.Character "#"]
let newAttrs := attrs
|>.insert "id" id
|>.insert "class" "markdown-heading"
let newContents := (←
contents.mapM (fun c => match c with
| Content.Element e => return Content.Element (← modifyElement e)
| _ => pure c))
|>.push (Content.Character " ")
|>.push (Content.Element anchor)
return ⟨ name, newAttrs, newContents⟩
/-- Extend anchor links. -/
def extendAnchor (el : Element) : HtmlM Element := do
match el with
| Element.Element name attrs contents =>
let newAttrs ← match attrs.find? "href" with
| some href => pure (attrs.insert "href" (← extendLink href))
| none => pure attrs
return ⟨ name, newAttrs, contents⟩
/-- Automatically add intra documentation link for inline code span. -/
def autoLink (el : Element) : HtmlM Element := do
match el with
| Element.Element name attrs contents =>
let mut newContents := #[]
for c in contents do
match c with
| Content.Character s =>
newContents := newContents ++ (← splitAround s unicodeToSplit |>.mapM linkify).join
| _ => newContents := newContents.push c
return ⟨ name, attrs, newContents ⟩
where
linkify s := do
let link? ← nameToLink? s
match link? with
| some link =>
let attributes := Lean.RBMap.empty.insert "href" link
return [Content.Element <| Element.Element "a" attributes #[Content.Character s]]
| none =>
let sHead := s.dropRightWhile (· != '.')
let sTail := s.takeRightWhile (· != '.')
let link'? ← nameToLink? sTail
match link'? with
| some link' =>
let attributes := Lean.RBMap.empty.insert "href" link'
return [
Content.Character sHead,
Content.Element <| Element.Element "a" attributes #[Content.Character sTail]
]
| none =>
return [Content.Character s]
unicodeToSplit (c : Char) : Bool :=
let cats := [
Unicode.GeneralCategory.Z, -- separator
Unicode.GeneralCategory.C -- other
]
cats.any (Unicode.isInGeneralCategory c)
/-- Core function of modifying the cmark rendered docstring html. -/
partial def modifyElement (element : Element) : HtmlM Element :=
match element with
| el@(Element.Element name attrs contents) => do
-- add id and class to <h_></h_>
if name = "h1" name = "h2" name = "h3" name = "h4" name = "h5" name = "h6" then
addHeadingAttributes el modifyElement
-- extend relative href for <a></a>
else if name = "a" then
extendAnchor el
-- auto link for inline <code></code>
else if name = "code" ∧
-- don't linkify code blocks explicitly tagged with a language other than lean
(((attrs.find? "class").getD "").splitOn.all (fun s => s == "language-lean" || !s.startsWith "language-")) then
autoLink el
-- recursively modify
else
let newContents ← contents.mapM fun c => match c with
| Content.Element e => return Content.Element (← modifyElement e)
| _ => pure c
return ⟨ name, attrs, newContents ⟩
/-- Convert docstring to Html. -/
def docStringToHtml (s : String) : HtmlM (Array Html) := do
let rendered := CMark.renderHtml (Html.escape s)
match manyDocument rendered.mkIterator with
| Parsec.ParseResult.success _ res =>
res.mapM fun x => do return Html.text <| toString (← modifyElement x)
| _ => return #[Html.text rendered]
end Output
end DocGen4

22
DocGen4/Output/Find.lean Normal file
View File

@ -0,0 +1,22 @@
import DocGen4.Output.Template
namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
open Lean
def find : BaseHtmlM Html := do
pure
<html lang="en">
<head>
<link rel="preload" href={s!"{← getRoot}/declarations/declaration-data.bmp"} as="image"/>
<script>{s!"const SITE_ROOT={String.quote (← getRoot)};"}</script>
<script type="module" async="true" src="./find.js"></script>
</head>
<body></body>
</html>
end Output
end DocGen4

View File

@ -0,0 +1,51 @@
import DocGen4.Output.Template
import DocGen4.Output.Inductive
namespace DocGen4.Output
open scoped DocGen4.Jsx
def foundationalTypes : BaseHtmlM Html := templateLiftExtends (baseHtml "Foundational Types") do
pure <|
<main>
<a id="top"></a>
<h1>Foundational Types</h1>
<p>Some of Lean's types are not defined in any Lean source files (even the <code>prelude</code>) since they come from its foundational type theory. This page provides basic documentation for these types.</p>
<p>For a more in-depth explanation of Lean's type theory, refer to
<a href="https://leanprover.github.io/theorem_proving_in_lean4/dependent_type_theory.html">TPiL</a>.</p>
<h2 id="codesort-ucode"><code>Sort u</code></h2>
<p><code>Sort u</code> is the type of types in Lean, and <code>Sort u : Sort (u + 1)</code>.</p>
{← instancesForToHtml `_builtin_sortu}
<h2 id="codetype-ucode"><code>Type u</code></h2>
<p><code>Type u</code> is notation for <code>Sort (u + 1)</code>.</p>
{← instancesForToHtml `_builtin_typeu}
<h2 id="codepropcode"><code>Prop</code></h2>
<p><code>Prop</code> is notation for <code>Sort 0</code>.</p>
{← instancesForToHtml `_builtin_prop}
<h2 id="pi-types-codeπ-a--α-β-acode">Pi types, <code>{"(a : α) → β a"}</code></h2>
<p>The type of dependent functions is known as a pi type.
Non-dependent functions and implications are a special case.</p>
<p>Note that these can also be written with the alternative notations:</p>
<ul>
<li><code>∀ a : α, β a</code>, conventionally used where <code>β a : Prop</code>.</li>
<li><code>(a : α) → β a</code></li>
<li><code>αγ</code>, possible only if <code>β a = γ</code> for all <code>a</code>.</li>
</ul>
<p>Lean also permits ASCII-only spellings of the three variants:</p>
<ul>
<li><code>forall a : A, B a</code> for <code>{"∀ a : α, β a"}</code></li>
<li><code>(a : A) -&gt; B a</code>, for <code>(a : α) → β a</code></li>
<li><code>A -&gt; B</code>, for <code>α → β</code></li>
</ul>
<p>Note that despite not itself being a function, <code>(→)</code> is available as infix notation for
<code>{"fun α β, α → β"}</code>.</p>
-- TODO: instances for pi types
</main>
end DocGen4.Output

84
DocGen4/Output/Index.lean Normal file
View File

@ -0,0 +1,84 @@
/-
Copyright (c) 2021 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import DocGen4.Output.ToHtmlFormat
import DocGen4.Output.Template
namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
pure <|
<main>
<a id="top"></a>
<h1>Bookshelf</h1>
<p>
A study of the books listed below. Most proofs are conducted in LaTeX.
Where feasible, theorems are also formally proven in
<a target="_blank" href="https://leanprover.github.io/">Lean</a>.
</p>
<h2>In Progress</h2>
<ul>
<li><a href={s!"{← getRoot}Bookshelf/Apostol.html"}>Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an Introduction to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.</a></li>
<li><a href={s!"{← getRoot}Bookshelf/Enderton/Logic.html"}>Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: Harcourt/Academic Press, 2001.</a></li>
<li><a href={s!"{← getRoot}Bookshelf/Enderton/Set.html"}>Enderton, Herbert B. Elements of Set Theory. New York: Academic Press, 1977.</a></li>
<li><a href={s!"{← getRoot}Bookshelf/Fraleigh.html"}>Fraleigh, John B. A First Course in Abstract Algebra, n.d.</a></li>
</ul>
<h2>Complete</h2>
<ul>
<li><a href={s!"{← getRoot}Bookshelf/Avigad.html"}>Avigad, Jeremy. Theorem Proving in Lean, n.d.</a></li>
</ul>
<h2>Pending</h2>
<ul>
<li>Axler, Sheldon. Linear Algebra Done Right. Undergraduate Texts in Mathematics. Cham: Springer International Publishing, 2015.</li>
<li>Cormen, Thomas H., Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms. 3rd ed. Cambridge, Mass: MIT Press, 2009.</li>
<li>Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.</li>
<li>Gustedt, Jens. Modern C. Shelter Island, NY: Manning Publications Co, 2020.</li>
<li>Ross, Sheldon. A First Course in Probability Theory. 8th ed. Pearson Prentice Hall, n.d.</li>
<li>Smullyan, Raymond M. To Mock a Mockingbird: And Other Logic Puzzles Including an Amazing Adventure in Combinatory Logic. Oxford: Oxford university press, 2000.</li>
</ul>
<h2>Legend</h2>
<p>
A color/symbol code is used on generated PDF headers to indicate their
status:
<ul>
<li>
<span style="color:darkgray">Dark gray statements </span> are
reserved for definitions and axioms that have been encoded in LaTeX.
A reference to a definition in Lean may also be provided.
</li>
<li>
<span style="color:teal">Teal statements </span> are reserved for
statements, theorems, lemmas, etc. that have been proven in LaTeX
and have a corresponding proof in Lean.
</li>
<li>
<span style="color:olive">Olive statements </span> are reserved for
statements, theorems, lemmas, etc. that have been proven in LaTeX.
A reference to a statement in Lean may also be provided.
</li>
<li>
<span style="color:fuchsia">Fuchsia statements </span> are reserved
for statements, theorems, lemmas, etc. that have been proven in
LaTeX and <i>will </i> have a corresponding proof in Lean.
</li>
<li>
<span style="color:maroon">Maroon </span> serves as a catch-all for
statements that don't fit the above categorizations. Incomplete
definitions, statements without proof, etc. belong here.
</li>
</ul>
</p>
<p>This was built using Lean 4 at commit <a href={s!"https://github.com/leanprover/lean4/tree/{Lean.githash}"}>{Lean.githash}</a></p>
</main>
end Output
end DocGen4

View File

@ -0,0 +1,39 @@
import DocGen4.Output.Template
import DocGen4.Output.DocString
import DocGen4.Process
namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
open Lean
def instancesForToHtml (typeName : Name) : BaseHtmlM Html := do
pure
<details «class»="instances">
<summary>Instances For</summary>
<ul id={s!"instances-for-list-{typeName}"} class="instances-for-list"></ul>
</details>
def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do
let shortName := c.name.componentsRev.head!.toString
let name := c.name.toString
if let some doc := c.doc then
let renderedDoc ← docStringToHtml doc
pure
<li class="constructor" id={name}>
{shortName} : [← infoFormatToHtml c.type]
<div class="inductive_ctor_doc">[renderedDoc]</div>
</li>
else
pure
<li class="constructor" id={name}>
{shortName} : [← infoFormatToHtml c.type]
</li>
def inductiveToHtml (i : Process.InductiveInfo) : HtmlM (Array Html) := do
let constructorsHtml := <ul class="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>
return #[constructorsHtml]
end Output
end DocGen4

View File

@ -0,0 +1,8 @@
import DocGen4.Output.Template
import DocGen4.Output.Definition
namespace DocGen4
namespace Output
end Output
end DocGen4

219
DocGen4/Output/Module.lean Normal file
View File

@ -0,0 +1,219 @@
/-
Copyright (c) 2021 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import DocGen4.Output.Template
import DocGen4.Output.Inductive
import DocGen4.Output.Structure
import DocGen4.Output.Class
import DocGen4.Output.Definition
import DocGen4.Output.Instance
import DocGen4.Output.ClassInductive
import DocGen4.Output.DocString
import DocGen4.Process
import Lean.Data.Xml.Parser
namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
open Lean Process
/--
Render an `Arg` as HTML, adding opacity effects etc. depending on what
type of binder it has.
-/
def argToHtml (arg : Arg) : HtmlM Html := do
let (l, r, implicit) := match arg.binderInfo with
| BinderInfo.default => ("(", ")", false)
| BinderInfo.implicit => ("{", "}", true)
| BinderInfo.strictImplicit => ("⦃", "⦄", true)
| BinderInfo.instImplicit => ("[", "]", true)
let mut nodes :=
match arg.name with
| some name => #[Html.text s!"{l}{name.toString} : "]
| none => #[Html.text s!"{l}"]
nodes := nodes.append (← infoFormatToHtml arg.type)
nodes := nodes.push r
let inner := <span class="fn">[nodes]</span>
let html := Html.element "span" false #[("class", "decl_args")] #[inner]
if implicit then
return <span class="impl_arg">{html}</span>
else
return html
/--
Render the structures this structure extends from as HTML so it can be
added to the top level.
-/
def structureInfoHeader (s : Process.StructureInfo) : HtmlM (Array Html) := do
let mut nodes := #[]
if s.parents.size > 0 then
nodes := nodes.push <span class="decl_extends">extends</span>
let mut parents := #[]
for parent in s.parents do
let link ← declNameToHtmlBreakWithinLink parent
let inner := <span class="fn">{link}</span>
let html:= Html.element "span" false #[("class", "decl_parent")] #[inner]
parents := parents.push html
nodes := nodes.append (parents.toList.intersperse (Html.text ", ")).toArray
return nodes
/--
Render the general header of a declaration containing its declaration type
and name.
-/
def docInfoHeader (doc : DocInfo) : HtmlM Html := do
let mut nodes := #[]
nodes := nodes.push <| Html.element "span" false #[("class", "decl_kind")] #[doc.getKindDescription]
nodes := nodes.push
<span class="decl_name">
{← declNameToHtmlBreakWithinLink doc.getName}
</span>
for arg in doc.getArgs do
nodes := nodes.push (← argToHtml arg)
match doc with
| DocInfo.structureInfo i => nodes := nodes.append (← structureInfoHeader i)
| DocInfo.classInfo i => nodes := nodes.append (← structureInfoHeader i)
| _ => nodes := nodes
nodes := nodes.push <| Html.element "span" true #[("class", "decl_args")] #[" :"]
nodes := nodes.push <div class="decl_type">[← infoFormatToHtml doc.getType]</div>
return <div class="decl_header"> [nodes] </div>
/--
The main entry point for rendering a single declaration inside a given module.
-/
def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
-- basic info like headers, types, structure fields, etc.
let docInfoHtml ← match doc with
| DocInfo.inductiveInfo i => inductiveToHtml i
| DocInfo.structureInfo i => structureToHtml i
| DocInfo.classInfo i => classToHtml i
| DocInfo.classInductiveInfo i => classInductiveToHtml i
| _ => pure #[]
-- rendered doc stirng
let docStringHtml ← match doc.getDocString with
| some s => docStringToHtml s
| none => pure #[]
-- extra information like equations and instances
let extraInfoHtml ← match doc with
| DocInfo.classInfo i => pure #[← classInstancesToHtml i.name]
| DocInfo.definitionInfo i => pure ((← equationsToHtml i) ++ #[← instancesForToHtml i.name])
| DocInfo.instanceInfo i => equationsToHtml i.toDefinitionInfo
| DocInfo.classInductiveInfo i => pure #[← classInstancesToHtml i.name]
| DocInfo.inductiveInfo i => pure #[← instancesForToHtml i.name]
| DocInfo.structureInfo i => pure #[← instancesForToHtml i.name]
| _ => pure #[]
let attrs := doc.getAttrs
let attrsHtml :=
if attrs.size > 0 then
let attrStr := "@[" ++ String.intercalate ", " doc.getAttrs.toList ++ "]"
#[Html.element "div" false #[("class", "attributes")] #[attrStr]]
else
#[]
let leanInkHtml :=
if ← leanInkEnabled? then
#[
<div class="ink_link">
<a href={← declNameToInkLink doc.getName}>ink</a>
</div>
]
else
#[]
pure
<div class="decl" id={doc.getName.toString}>
<div class={doc.getKind}>
<div class="gh_link">
<a href={← getSourceUrl module doc.getDeclarationRange}>source</a>
</div>
[leanInkHtml]
[attrsHtml]
{← docInfoHeader doc}
[docInfoHtml]
[docStringHtml]
[extraInfoHtml]
</div>
</div>
/--
Rendering a module doc string, that is the ones with an ! after the opener
as HTML.
-/
def modDocToHtml (mdoc : ModuleDoc) : HtmlM Html := do
pure
<div class="mod_doc">
[← docStringToHtml mdoc.doc]
</div>
/--
Render a module member, that is either a module doc string or a declaration
as HTML.
-/
def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := do
match member with
| ModuleMember.docInfo d => docInfoToHtml module d
| ModuleMember.modDoc d => modDocToHtml d
def declarationToNavLink (module : Name) : Html :=
<div class="nav_link">
<a class="break_within" href={s!"#{module.toString}"}>
[breakWithin module.toString]
</a>
</div>
/--
Returns the list of all imports this module does.
-/
def getImports (module : Name) : HtmlM (Array Name) := do
let res ← getResult
return res.moduleInfo.find! module |>.imports
/--
Sort the list of all modules this one is importing, linkify it
and return the HTML.
-/
def importsHtml (moduleName : Name) : HtmlM (Array Html) := do
let imports := (← getImports moduleName).qsort Name.lt
imports.mapM (fun i => do return <li>{← moduleToHtmlLink i}</li>)
/--
Render the internal nav bar (the thing on the right on all module pages).
-/
def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
pure
<nav class="internal_nav">
<h3><a class="break_within" href="#top">[breakWithin moduleName.toString]</a></h3>
<p class="gh_nav_link"><a href={← getSourceUrl moduleName none}>source</a></p>
<div class="imports">
<details>
<summary>Imports</summary>
<ul>
[← importsHtml moduleName]
</ul>
</details>
<details>
<summary>Imported by</summary>
<ul id={s!"imported-by-{moduleName}"} class="imported-by-list"> </ul>
</details>
</div>
[members.map declarationToNavLink]
</nav>
/--
The main entry point to rendering the HTML for an entire module.
-/
def moduleToHtml (module : Process.Module) : HtmlM Html := withTheReader SiteBaseContext (setCurrentName module.name) do
let relevantMembers := module.members.filter Process.ModuleMember.shouldRender
let memberDocs ← relevantMembers.mapM (moduleMemberToHtml module.name)
let memberNames := filterDocInfo relevantMembers |>.map DocInfo.getName
templateLiftExtends (baseHtmlGenerator module.name.toString) <| pure #[
← internalNav memberNames module.name,
Html.element "main" false #[] memberDocs
]
end Output
end DocGen4

111
DocGen4/Output/Navbar.lean Normal file
View File

@ -0,0 +1,111 @@
/-
Copyright (c) 2021 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
import DocGen4.Output.ToHtmlFormat
import DocGen4.Output.Base
namespace DocGen4
namespace Output
open Lean
open scoped DocGen4.Jsx
def moduleListFile (file : NameExt) : BaseHtmlM Html := do
let contents :=
if file.ext == .pdf then
<span>{s!"🗎 {file.getString!} (<a class=\"pdf\" target=\"_blank\" href={← moduleNameExtToLink file}>pdf</a>)"}</span>
else
<a href={← moduleNameExtToLink file}>{file.getString!}</a>
return <div class={if (← getCurrentName) == file.name then "nav_link visible" else "nav_link"}>
{contents}
</div>
/--
Build the HTML tree representing the module hierarchy.
-/
partial def moduleListDir (h : Hierarchy) : BaseHtmlM Html := do
let children := Array.mk (h.getChildren.toList.map Prod.snd)
let nodes ← children.mapM (fun c =>
if c.getChildren.toList.length != 0 then
moduleListDir c
else if Hierarchy.isFile c && c.getChildren.toList.length = 0 then
moduleListFile (Hierarchy.getNameExt c)
else
pure ""
)
let moduleLink ← moduleNameToHtmlLink h.getName
let summary :=
if h.isFile then
<summary>{s!"{h.getName.getString!} ({<a href={← moduleNameToHtmlLink h.getName}>file</a>})"} </summary>
else
<summary>{h.getName.getString!}</summary>
pure
<details class="nav_sect" "data-path"={moduleLink} [if (← getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]>
{summary}
[nodes]
</details>
/--
Return a list of top level modules, linkified and rendered as HTML
-/
def moduleList : BaseHtmlM Html := do
let hierarchy ← getHierarchy
let mut list := Array.empty
for (_, cs) in hierarchy.getChildren do
list := list.push <| ← moduleListDir cs
return <div class="module_list">[list]</div>
/--
The main entry point to rendering the navbar on the left hand side.
-/
def navbar : BaseHtmlM Html := do
pure
<html lang="en">
<head>
[← baseHtmlHeadDeclarations]
<script type="module" src={s!"{← getRoot}nav.js"}></script>
<script type="module" src={s!"{← getRoot}color-scheme.js"}></script>
<base target="_parent" />
</head>
<body>
<div class="navframe">
<nav class="nav">
<h3>General documentation</h3>
<div class="nav_link"><a href={s!"{← getRoot}"}>index</a></div>
<div class="nav_link"><a href={s!"{← getRoot}foundational_types.html"}>foundational types</a></div>
/-
TODO: Add these in later
<div class="nav_link"><a href={s!"{← getRoot}tactics.html"}>tactics</a></div>
<div class="nav_link"><a href={s!"{← getRoot}commands.html"}>commands</a></div>
<div class="nav_link"><a href={s!"{← getRoot}hole_commands.html"}>hole commands</a></div>
<div class="nav_link"><a href={s!"{← getRoot}attributes.html"}>attributes</a></div>
<div class="nav_link"><a href={s!"{← getRoot}notes.html"}>notes</a></div>
<div class="nav_link"><a href={s!"{← getRoot}references.html"}>references</a></div>
-/
<h3>Library</h3>
{← moduleList}
<div id="settings" hidden="hidden">
-- `input` is a void tag, but can be self-closed to make parsing easier.
<h3>Color scheme</h3>
<form id="color-theme-switcher">
<label for="color-theme-dark">
<input type="radio" name="color_theme" id="color-theme-dark" value="dark" autocomplete="off"/>dark</label>
<label for="color-theme-system" title="Match system theme settings">
<input type="radio" name="color_theme" id="color-theme-system" value="system" autocomplete="off"/>system</label>
<label for="color-theme-light">
<input type="radio" name="color_theme" id="color-theme-light" value="light" autocomplete="off"/>light</label>
</form>
</div>
</nav>
</div>
</body>
</html>
end Output
end DocGen4

View File

@ -0,0 +1,26 @@
/-
Copyright (c) 2021 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import DocGen4.Output.ToHtmlFormat
import DocGen4.Output.Template
namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
/--
Render the 404 page.
-/
def notFound : BaseHtmlM Html := do templateExtends (baseHtml "404") <|
pure <|
<main>
<h1>404 Not Found</h1>
<p> Unfortunately, the page you were looking for is no longer here. </p>
<div id="howabout"></div>
</main>
end Output
end DocGen4

View File

@ -0,0 +1,48 @@
/-
Copyright (c) 2023 Jeremy Salwen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Salwen
-/
import DocGen4.Output.ToHtmlFormat
import DocGen4.Output.Template
namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
def search : BaseHtmlM Html := do templateExtends (baseHtml "Search") <|
pure <|
<main>
<h1> Search Results </h1>
<label for="search_page_query">Query:</label>
<input id="search_page_query" />
<div id="kinds">
Allowed Kinds:
<input type="checkbox" id="def_checkbox" class="kind_checkbox" value="def" checked="checked" />
<label for="def_checkbox">def</label>
<input type="checkbox" id="theorem_checkbox" class="kind_checkbox" value="theorem" checked="checked" />
<label for="theorem_checkbox">theorem</label>
<input type="checkbox" id="inductive_checkbox" class="kind_checkbox" value="inductive" checked="checked" />
<label for="inductive_checkbox">inductive</label>
<input type="checkbox" id="structure_checkbox" class="kind_checkbox" value="structure" checked="checked" />
<label for="structure_checkbox">structure</label>
<input type="checkbox" id="class_checkbox" class="kind_checkbox" value="class" checked="checked" />
<label for="class_checkbox">class</label>
<input type="checkbox" id="instance_checkbox" class="kind_checkbox" value="instance" checked="checked" />
<label for="instance_checkbox">instance</label>
<input type="checkbox" id="axiom_checkbox" class="axiom_checkbox" value="axiom" checked="checked" />
<label for="axiom_checkbox">axiom</label>
<input type="checkbox" id="opaque_checkbox" class="kind_checkbox" value="opaque" checked="checked" />
<label for="opaque_checkbox">opaque</label>
</div>
<script>
document.getElementById("search_page_query").value = new URL(window.location.href).searchParams.get("q")
</script>
<div id="search_results">
</div>
</main>
end Output
end DocGen4

View File

@ -0,0 +1,37 @@
/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
namespace DocGen4.Output.SourceLinker
open Lean
/--
Given a lake workspace with all the dependencies as well as the hash of the
compiler release to work with this provides a function to turn names of
declarations into (optionally positional) Github URLs.
-/
def sourceLinker (gitUrl? : Option String) : IO (Name → Option DeclarationRange → String) := do
-- TOOD: Refactor this, we don't need to pass in the module into the returned closure
-- since we have one sourceLinker per module
return fun module range =>
let parts := module.components.map Name.toString
let path := String.intercalate "/" parts
let root := module.getRoot
let leanHash := Lean.githash
let basic := if root == `Lean root == `Init then
s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean"
else if root == `Lake then
s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/lake/{path}.lean"
else
gitUrl?.get!
match range with
| some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}"
| none => basic
end DocGen4.Output.SourceLinker

View File

@ -0,0 +1,51 @@
import DocGen4.Output.Template
import DocGen4.Output.DocString
import DocGen4.Process
namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
open Lean
/--
Render a single field consisting of its documentation, its name and its type as HTML.
-/
def fieldToHtml (f : Process.NameInfo) : HtmlM Html := do
let shortName := f.name.componentsRev.head!.toString
let name := f.name.toString
if let some doc := f.doc then
let renderedDoc ← docStringToHtml doc
pure
<li id={name} class="structure_field">
<div class="structure_field_info">{s!"{shortName} "} : [← infoFormatToHtml f.type]</div>
<div class="structure_field_doc">[renderedDoc]</div>
</li>
else
pure
<li id={name} class="structure_field">
<div class="structure_field_info">{s!"{shortName} "} : [← infoFormatToHtml f.type]</div>
</li>
/--
Render all information about a structure as HTML.
-/
def structureToHtml (i : Process.StructureInfo) : HtmlM (Array Html) := do
let structureHtml :=
if Name.isSuffixOf `mk i.ctor.name then
(<ul class="structure_fields" id={i.ctor.name.toString}>
[← i.fieldInfo.mapM fieldToHtml]
</ul>)
else
let ctorShortName := i.ctor.name.componentsRev.head!.toString
(<ul class="structure_ext">
<li id={i.ctor.name.toString} class="structure_ext_ctor">{s!"{ctorShortName} "} :: (</li>
<ul class="structure_ext_fields">
[← i.fieldInfo.mapM fieldToHtml]
</ul>
<li class="structure_ext_ctor">)</li>
</ul>)
return #[structureHtml]
end Output
end DocGen4

View File

@ -0,0 +1,72 @@
/-
Copyright (c) 2021 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import DocGen4.Output.ToHtmlFormat
import DocGen4.Output.Navbar
namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
/--
The HTML template used for all pages.
-/
def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := do
let moduleConstant :=
if let some module := ← getCurrentName then
#[<script>{s!"const MODULE_NAME={String.quote module.toString};"}</script>]
else
#[]
pure
<html lang="en">
<head>
[← baseHtmlHeadDeclarations]
<title>{title}</title>
<script defer="true" src={s!"{← getRoot}mathjax-config.js"}></script>
<script defer="true" src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
<script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
<script>{s!"const SITE_ROOT={String.quote (← getRoot)};"}</script>
[moduleConstant]
<script type="module" src={s!"{← getRoot}jump-src.js"}></script>
<script type="module" src={s!"{← getRoot}search.js"}></script>
<script type="module" src={s!"{← getRoot}expand-nav.js"}></script>
<script type="module" src={s!"{← getRoot}how-about.js"}></script>
<script type="module" src={s!"{← getRoot}instances.js"}></script>
<script type="module" src={s!"{← getRoot}importedBy.js"}></script>
</head>
<body>
<input id="nav_toggle" type="checkbox"/>
<header>
<h1><label for="nav_toggle"></label>Documentation</h1>
<p class="header_filename break_within">[breakWithin title]</p>
<form action="https://google.com/search" method="get" id="search_form">
<input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib4_docs"/>
<input type="text" name="q" autocomplete="off"/>&#32;
<button id="search_button" onclick={s!"javascript: form.action='{← getRoot}search.html';"}>Search</button>
<button>Google site search</button>
</form>
</header>
[site]
<nav class="nav">
<iframe src={s!"{← getRoot}navbar.html"} class="navframe" frameBorder="0"></iframe>
</nav>
</body>
</html>
/--
A comfortability wrapper around `baseHtmlGenerator`.
-/
def baseHtml (title : String) (site : Html) : BaseHtmlM Html := baseHtmlGenerator title #[site]
end Output
end DocGen4

View File

@ -0,0 +1,149 @@
/-
Copyright (c) 2021 Wojciech Nawrocki. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Wojciech Nawrocki, Sebastian Ullrich, Henrik Böving
-/
import Lean.Data.Json
import Lean.Parser
/-! This module defines:
- a representation of HTML trees
- together with a JSX-like DSL for writing them
- and widget support for visualizing any type as HTML. -/
namespace DocGen4
open Lean
inductive Html where
-- TODO(WN): it's nameless for shorter JSON; re-add names when we have deriving strategies for From/ToJson
-- element (tag : String) (flatten : Bool) (attrs : Array HtmlAttribute) (children : Array Html)
| element : String → Bool → Array (String × String) → Array Html → Html
| text : String → Html
deriving Repr, BEq, Inhabited, FromJson, ToJson
instance : Coe String Html :=
⟨Html.text⟩
namespace Html
def attributesToString (attrs : Array (String × String)) :String :=
attrs.foldl (fun acc (k, v) => acc ++ " " ++ k ++ "=\"" ++ v ++ "\"") ""
-- TODO: Termination proof
partial def toStringAux : Html → String
| element tag false attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}</{tag}>\n"
| element tag false attrs #[child] => s!"<{tag}{attributesToString attrs}>\n{child.toStringAux}</{tag}>\n"
| element tag false attrs children => s!"<{tag}{attributesToString attrs}>\n{children.foldl (· ++ toStringAux ·) ""}</{tag}>\n"
| element tag true attrs children => s!"<{tag}{attributesToString attrs}>{children.foldl (· ++ toStringAux ·) ""}</{tag}>"
| text s => s
def toString (html : Html) : String :=
html.toStringAux.trimRight
instance : ToString Html :=
⟨toString⟩
partial def textLength : Html → Nat
| text s => s.length
| element _ _ _ children =>
let lengths := children.map textLength
lengths.foldl Nat.add 0
def escapePairs : Array (String × String) :=
#[
("&", "&amp;"),
("<", "&lt;"),
(">", "&gt;"),
("\"", "&quot;")
]
def escape (s : String) : String :=
escapePairs.foldl (fun acc (o, r) => acc.replace o r) s
end Html
namespace Jsx
open Parser PrettyPrinter
declare_syntax_cat jsxElement
declare_syntax_cat jsxChild
-- JSXTextCharacter : SourceCharacter but not one of {, <, > or }
def jsxText : Parser :=
withAntiquot (mkAntiquot "jsxText" `jsxText) {
fn := fun c s =>
let startPos := s.pos
let s := takeWhile1Fn (not ∘ "[{<>}]$".contains) "expected JSX text" c s
mkNodeToken `jsxText startPos c s }
@[combinator_formatter DocGen4.Jsx.jsxText] def jsxText.formatter : Formatter := pure ()
@[combinator_parenthesizer DocGen4.Jsx.jsxText] def jsxText.parenthesizer : Parenthesizer := pure ()
syntax jsxAttrName := rawIdent <|> str
syntax jsxAttrVal := str <|> group("{" term "}")
syntax jsxSimpleAttr := jsxAttrName "=" jsxAttrVal
syntax jsxAttrSpread := "[" term "]"
syntax jsxAttr := jsxSimpleAttr <|> jsxAttrSpread
syntax "<" rawIdent jsxAttr* "/>" : jsxElement
syntax "<" rawIdent jsxAttr* ">" jsxChild* "</" rawIdent ">" : jsxElement
syntax jsxText : jsxChild
syntax "{" term "}" : jsxChild
syntax "[" term "]" : jsxChild
syntax jsxElement : jsxChild
scoped syntax:max jsxElement : term
def translateAttrs (attrs : Array (TSyntax `DocGen4.Jsx.jsxAttr)) : MacroM (TSyntax `term) := do
let mut as ← `(#[])
for attr in attrs.map TSyntax.raw do
as ← match attr with
| `(jsxAttr| $n:jsxAttrName=$v:jsxAttrVal) =>
let n ← match n with
| `(jsxAttrName| $n:str) => pure n
| `(jsxAttrName| $n:ident) => pure <| quote (toString n.getId)
| _ => Macro.throwUnsupported
let v ← match v with
| `(jsxAttrVal| {$v}) => pure v
| `(jsxAttrVal| $v:str) => pure v
| _ => Macro.throwUnsupported
`(($as).push ($n, ($v : String)))
| `(jsxAttr| [$t]) => `($as ++ ($t : Array (String × String)))
| _ => Macro.throwUnsupported
return as
private def htmlHelper (n : Syntax) (children : Array Syntax) (m : Syntax) : MacroM (String × (TSyntax `term)):= do
unless n.getId == m.getId do
withRef m <| Macro.throwError s!"Leading and trailing part of tags don't match: '{n}', '{m}'"
let mut cs ← `(#[])
for child in children do
cs ← match child with
| `(jsxChild|$t:jsxText) => `(($cs).push (Html.text $(quote t.raw[0]!.getAtomVal)))
-- TODO(WN): elab as list of children if type is `t Html` where `Foldable t`
| `(jsxChild|{$t}) => `(($cs).push ($t : Html))
| `(jsxChild|[$t]) => `($cs ++ ($t : Array Html))
| `(jsxChild|$e:jsxElement) => `(($cs).push ($e:jsxElement : Html))
| _ => Macro.throwUnsupported
let tag := toString n.getId
pure <| (tag, cs)
macro_rules
| `(<$n $attrs* />) => do
let kind := quote (toString n.getId)
let attrs ← translateAttrs attrs
`(Html.element $kind true $attrs #[])
| `(<$n $attrs* >$children*</$m>) => do
let (tag, children) ← htmlHelper n children m
`(Html.element $(quote tag) true $(← translateAttrs attrs) $children)
end Jsx
/-- A type which implements `ToHtmlFormat` will be visualized
as the resulting HTML in editors which support it. -/
class ToHtmlFormat (α : Type u) where
formatHtml : α → Html
end DocGen4

134
DocGen4/Output/ToJson.lean Normal file
View File

@ -0,0 +1,134 @@
import Lean
import DocGen4.Process
import DocGen4.Output.Base
import DocGen4.Output.Module
import Lean.Data.RBMap
namespace DocGen4.Output
open Lean
structure JsonDeclarationInfo where
name : String
kind : String
doc : String
docLink : String
sourceLink : String
line : Nat
deriving FromJson, ToJson
structure JsonDeclaration where
info : JsonDeclarationInfo
header : String
deriving FromJson, ToJson
structure JsonInstance where
name : String
className : String
typeNames : Array String
deriving FromJson, ToJson
structure JsonModule where
name : String
declarations : List JsonDeclaration
instances : Array JsonInstance
imports : Array String
deriving FromJson, ToJson
structure JsonHeaderIndex where
declarations : List (String × JsonDeclaration) := []
structure JsonIndexedDeclarationInfo where
kind : String
docLink : String
deriving FromJson, ToJson
structure JsonIndex where
declarations : List (String × JsonIndexedDeclarationInfo) := []
instances : HashMap String (RBTree String Ord.compare) := .empty
importedBy : HashMap String (Array String) := .empty
modules : List (String × String) := []
instancesFor : HashMap String (RBTree String Ord.compare) := .empty
instance : ToJson JsonHeaderIndex where
toJson idx := Json.mkObj <| idx.declarations.map (fun (k, v) => (k, toJson v))
instance : ToJson JsonIndex where
toJson idx := Id.run do
let jsonDecls := Json.mkObj <| idx.declarations.map (fun (k, v) => (k, toJson v))
let jsonInstances := Json.mkObj <| idx.instances.toList.map (fun (k, v) => (k, toJson v.toArray))
let jsonImportedBy := Json.mkObj <| idx.importedBy.toList.map (fun (k, v) => (k, toJson v))
let jsonModules := Json.mkObj <| idx.modules.map (fun (k, v) => (k, toJson v))
let jsonInstancesFor := Json.mkObj <| idx.instancesFor.toList.map (fun (k, v) => (k, toJson v.toArray))
let finalJson := Json.mkObj [
("declarations", jsonDecls),
("instances", jsonInstances),
("importedBy", jsonImportedBy),
("modules", jsonModules),
("instancesFor", jsonInstancesFor)
]
return finalJson
def JsonHeaderIndex.addModule (index : JsonHeaderIndex) (module : JsonModule) : JsonHeaderIndex :=
let merge idx decl := { idx with declarations := (decl.info.name, decl) :: idx.declarations }
module.declarations.foldl merge index
def JsonIndex.addModule (index : JsonIndex) (module : JsonModule) : BaseHtmlM JsonIndex := do
let mut index := index
let newModule := (module.name, ← moduleNameToHtmlLink (String.toName module.name))
let newDecls := module.declarations.map (fun d => (d.info.name, {
kind := d.info.kind,
docLink := d.info.docLink,
}))
index := { index with
modules := newModule :: index.modules
declarations := newDecls ++ index.declarations
}
-- TODO: In theory one could sort instances and imports by name and batch the writes
for inst in module.instances do
let mut insts := index.instances.findD inst.className {}
insts := insts.insert inst.name
index := { index with instances := index.instances.insert inst.className insts }
for typeName in inst.typeNames do
let mut instsFor := index.instancesFor.findD typeName {}
instsFor := instsFor.insert inst.name
index := { index with instancesFor := index.instancesFor.insert typeName instsFor }
for imp in module.imports do
let mut impBy := index.importedBy.findD imp #[]
impBy := impBy.push module.name
index := { index with importedBy := index.importedBy.insert imp impBy }
return index
def DocInfo.toJson (module : Name) (info : Process.DocInfo) : HtmlM JsonDeclaration := do
let name := info.getName.toString
let kind := info.getKind
let doc := info.getDocString.getD ""
let docLink ← declNameToLink info.getName
let sourceLink ← getSourceUrl module info.getDeclarationRange
let line := info.getDeclarationRange.pos.line
let header := (← docInfoHeader info).toString
let info := { name, kind, doc, docLink, sourceLink, line }
return { info, header }
def Process.Module.toJson (module : Process.Module) : HtmlM Json := do
let mut jsonDecls := []
let mut instances := #[]
let declInfo := Process.filterDocInfo module.members
for decl in declInfo do
jsonDecls := (← DocInfo.toJson module.name decl) :: jsonDecls
if let .instanceInfo i := decl then
instances := instances.push {
name := i.name.toString,
className := i.className.toString
typeNames := i.typeNames.map Name.toString
}
let jsonMod : JsonModule := {
name := module.name.toString,
declarations := jsonDecls,
instances,
imports := module.imports.map Name.toString
}
return ToJson.toJson jsonMod
end DocGen4.Output

21
DocGen4/Process.lean Normal file
View File

@ -0,0 +1,21 @@
/-
Copyright (c) 2021 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import DocGen4.Process.Analyze
import DocGen4.Process.Attributes
import DocGen4.Process.AxiomInfo
import DocGen4.Process.Base
import DocGen4.Process.ClassInfo
import DocGen4.Process.DefinitionInfo
import DocGen4.Process.DocInfo
import DocGen4.Process.Hierarchy
import DocGen4.Process.InductiveInfo
import DocGen4.Process.InstanceInfo
import DocGen4.Process.NameExt
import DocGen4.Process.NameInfo
import DocGen4.Process.OpaqueInfo
import DocGen4.Process.StructureInfo
import DocGen4.Process.TheoremInfo

View File

@ -0,0 +1,162 @@
/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
import Lean.Data.HashMap
import Lean.Data.HashSet
import DocGen4.Process.Base
import DocGen4.Process.Hierarchy
import DocGen4.Process.DocInfo
namespace DocGen4.Process
open Lean Meta
/--
Member of a module, either a declaration or some module doc string.
-/
inductive ModuleMember where
| docInfo (info : DocInfo) : ModuleMember
| modDoc (doc : ModuleDoc) : ModuleMember
deriving Inhabited
/--
A Lean module.
-/
structure Module where
/--
Name of the module.
-/
name : Name
/--
All members of the module, sorted according to their line numbers.
-/
members : Array ModuleMember
imports : Array Name
deriving Inhabited
/--
The result of running a full doc-gen analysis on a project.
-/
structure AnalyzerResult where
/--
The map from module names to indices of the `moduleNames` array.
-/
name2ModIdx : HashMap Name ModuleIdx
/--
The list of all modules, accessible nicely via `name2ModIdx`.
-/
moduleNames : Array Name
/--
A map from module names to information about these modules.
-/
moduleInfo : HashMap Name Module
deriving Inhabited
namespace ModuleMember
def getDeclarationRange : ModuleMember → DeclarationRange
| docInfo i => i.getDeclarationRange
| modDoc i => i.declarationRange
/--
An order for module members, based on their declaration range.
-/
def order (l r : ModuleMember) : Bool :=
Position.lt l.getDeclarationRange.pos r.getDeclarationRange.pos
def getName : ModuleMember → Name
| docInfo i => i.getName
| modDoc _ => Name.anonymous
def getDocString : ModuleMember → Option String
| docInfo i => i.getDocString
| modDoc i => i.doc
def shouldRender : ModuleMember → Bool
| docInfo i => i.shouldRender
| modDoc _ => true
end ModuleMember
inductive AnalyzeTask where
| loadAll (load : Array Name) : AnalyzeTask
| loadAllLimitAnalysis (analyze : Array Name) : AnalyzeTask
def AnalyzeTask.getLoad : AnalyzeTask → Array Name
| loadAll load => load
| loadAllLimitAnalysis load => load
def getAllModuleDocs (relevantModules : Array Name) : MetaM (HashMap Name Module) := do
let env ← getEnv
let mut res := mkHashMap relevantModules.size
for module in relevantModules do
let modDocs := getModuleDoc? env module |>.getD #[] |>.map .modDoc
let some modIdx := env.getModuleIdx? module | unreachable!
let moduleData := env.header.moduleData.get! modIdx
let imports := moduleData.imports.map Import.module
res := res.insert module <| Module.mk module modDocs imports
return res
/--
Run the doc-gen analysis on all modules that are loaded into the `Environment`
of this `MetaM` run and mentioned by the `AnalyzeTask`.
-/
def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do
let env ← getEnv
let relevantModules := match task with
| .loadAll _ => HashSet.fromArray env.header.moduleNames
| .loadAllLimitAnalysis analysis => HashSet.fromArray analysis
let allModules := env.header.moduleNames
let mut res ← getAllModuleDocs relevantModules.toArray
for (name, cinfo) in env.constants.toList do
let some modidx := env.getModuleIdxFor? name | unreachable!
let moduleName := env.allImportedModuleNames.get! modidx
if !relevantModules.contains moduleName then
continue
try
let config := {
maxHeartbeats := 5000000,
options := ← getOptions,
fileName := ← getFileName,
fileMap := ← getFileMap
}
let analysis ← Prod.fst <$> Meta.MetaM.toIO (DocInfo.ofConstant (name, cinfo)) config { env := env } {} {}
if let some dinfo := analysis then
let moduleName := env.allImportedModuleNames.get! modidx
let module := res.find! moduleName
res := res.insert moduleName {module with members := module.members.push (ModuleMember.docInfo dinfo)}
catch e =>
if let some pos := e.getRef.getPos? then
let pos := (← getFileMap).toPosition pos
IO.println s!"WARNING: Failed to obtain information in file: {pos}, for: {name}, {← e.toMessageData.toString}"
else
IO.println s!"WARNING: Failed to obtain information for: {name}: {← e.toMessageData.toString}"
-- TODO: This could probably be faster if we did sorted insert above instead
for (moduleName, module) in res.toArray do
res := res.insert moduleName {module with members := module.members.qsort ModuleMember.order}
let hierarchy := Hierarchy.fromArray allModules
let analysis := {
name2ModIdx := env.const2ModIdx,
moduleNames := allModules,
moduleInfo := res,
}
return (analysis, hierarchy)
def filterDocInfo (ms : Array ModuleMember) : Array DocInfo :=
ms.filterMap filter
where
filter : ModuleMember → Option DocInfo
| ModuleMember.docInfo i => some i
| _ => none
end DocGen4.Process

View File

@ -0,0 +1,182 @@
import Lean
namespace DocGen4
open Lean Meta
-- The following is probably completely overengineered but I love it
/--
Captures the notion of a value based attributes, `attrKind` is things like
`EnumAttributes`.
-/
class ValueAttr (attrKind : Type → Type) where
/--
Given a certain value based attribute, an `Environment` and the `Name` of
a declaration returns the value of the attribute on this declaration if present.
-/
getValue {α : Type} [Inhabited α] [ToString α] : attrKind α → Environment → Name → Option String
/--
Contains a specific attribute declaration of a certain attribute kind (enum based, parametric etc.).
-/
structure ValueAttrWrapper (attrKind : Type → Type) [ValueAttr attrKind] where
{α : Type}
attr : attrKind α
[str : ToString α]
[inhab : Inhabited α]
/--
Obtain the value of an enum attribute for a certain name.
-/
def enumGetValue {α : Type} [Inhabited α] [ToString α] (attr : EnumAttributes α) (env : Environment) (decl : Name) : Option String := do
let val ← EnumAttributes.getValue attr env decl
some (toString val)
instance : ValueAttr EnumAttributes where
getValue := enumGetValue
/--
Obtain the value of a parametric attribute for a certain name.
-/
def parametricGetValue {α : Type} [Inhabited α] [ToString α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option String := do
let val ← ParametricAttribute.getParam? attr env decl
some (attr.attr.name.toString ++ " " ++ toString val)
instance : ValueAttr ParametricAttribute where
getValue := parametricGetValue
abbrev EnumAttrWrapper := ValueAttrWrapper EnumAttributes
abbrev ParametricAttrWrapper := ValueAttrWrapper ParametricAttribute
/--
The list of all tag based attributes doc-gen knows about and can recover.
-/
def tagAttributes : Array TagAttribute :=
#[IR.UnboxResult.unboxAttr, neverExtractAttr,
Elab.Term.elabWithoutExpectedTypeAttr, matchPatternAttr]
deriving instance Repr for Compiler.InlineAttributeKind
deriving instance Repr for Compiler.SpecializeAttributeKind
open Compiler in
instance : ToString InlineAttributeKind where
toString kind :=
match kind with
| .inline => "inline"
| .noinline => "noinline"
| .macroInline => "macro_inline"
| .inlineIfReduce => "inline_if_reduce"
| .alwaysInline => "always_inline"
open Compiler in
instance : ToString SpecializeAttributeKind where
toString kind :=
match kind with
| .specialize => "specialize"
| .nospecialize => "nospecialize"
instance : ToString ReducibilityStatus where
toString kind :=
match kind with
| .reducible => "reducible"
| .semireducible => "semireducible"
| .irreducible => "irreducible"
/--
The list of all enum based attributes doc-gen knows about and can recover.
-/
@[reducible]
def enumAttributes : Array EnumAttrWrapper := #[⟨Compiler.inlineAttrs⟩, ⟨reducibilityAttrs⟩]
instance : ToString ExternEntry where
toString entry :=
match entry with
| .adhoc `all => ""
| .adhoc backend => s!"{backend} adhoc"
| .standard `all fn => fn
| .standard backend fn => s!"{backend} {fn}"
| .inline backend pattern => s!"{backend} inline {String.quote pattern}"
-- TODO: The docs in the module dont specific how to render this
| .foreign backend fn => s!"{backend} foreign {fn}"
instance : ToString ExternAttrData where
toString data := (data.arity?.map toString |>.getD "") ++ " " ++ String.intercalate " " (data.entries.map toString)
/--
The list of all parametric attributes (that is, attributes with any kind of information attached)
doc-gen knows about and can recover.
-/
def parametricAttributes : Array ParametricAttrWrapper := #[⟨externAttr⟩, ⟨Compiler.implementedByAttr⟩, ⟨exportAttr⟩, ⟨Compiler.specializeAttr⟩]
def getTags (decl : Name) : MetaM (Array String) := do
let env ← getEnv
return tagAttributes.filter (TagAttribute.hasTag · env decl) |>.map (·.attr.name.toString)
def getValuesAux {α : Type} {attrKind : Type → Type} [va : ValueAttr attrKind] [Inhabited α] [ToString α] (decl : Name) (attr : attrKind α) : MetaM (Option String) := do
let env ← getEnv
return va.getValue attr env decl
def getValues {attrKind : Type → Type} [ValueAttr attrKind] (decl : Name) (attrs : Array (ValueAttrWrapper attrKind)) : MetaM (Array String) := do
let mut res := #[]
for attr in attrs do
if let some val ← @getValuesAux attr.α attrKind _ attr.inhab attr.str decl attr.attr then
res := res.push val
return res
def getEnumValues (decl : Name) : MetaM (Array String) := getValues decl enumAttributes
def getParametricValues (decl : Name) : MetaM (Array String) := do
let mut uniform ← getValues decl parametricAttributes
-- This attribute contains an `Option Name` but we would like to pretty print it better
if let some depTag := Linter.deprecatedAttr.getParam? (← getEnv) decl then
let str := match depTag with
| some alt => s!"deprecated {alt.toString}"
| none => "deprecated"
uniform := uniform.push str
return uniform
def getDefaultInstance (decl : Name) (className : Name) : MetaM (Option String) := do
let insts ← getDefaultInstances className
for (inst, prio) in insts do
if inst == decl then
return some s!"defaultInstance {prio}"
return none
def hasSimp (decl : Name) : MetaM (Option String) := do
let thms ← simpExtension.getTheorems
if thms.isLemma (.decl decl) then
return "simp"
else
return none
def hasCsimp (decl : Name) : MetaM (Option String) := do
let env ← getEnv
if Compiler.hasCSimpAttribute env decl then
return some "csimp"
else
return none
/--
The list of custom attributes, that don't fit in the parametric or enum
attribute kinds, doc-gen konws about and can recover.
-/
def customAttrs := #[hasSimp, hasCsimp]
def getCustomAttrs (decl : Name) : MetaM (Array String) := do
let mut values := #[]
for attr in customAttrs do
if let some value ← attr decl then
values := values.push value
return values
/--
The main entry point for recovering all attribute values for a given
declaration.
-/
def getAllAttributes (decl : Name) : MetaM (Array String) := do
let tags ← getTags decl
let enums ← getEnumValues decl
let parametric ← getParametricValues decl
let customs ← getCustomAttrs decl
return customs ++ tags ++ enums ++ parametric
end DocGen4

View File

@ -0,0 +1,22 @@
/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
import DocGen4.Process.Base
import DocGen4.Process.NameInfo
namespace DocGen4.Process
open Lean Meta
def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do
let info ← Info.ofConstantVal v.toConstantVal
return {
toInfo := info,
isUnsafe := v.isUnsafe
}
end DocGen4.Process

198
DocGen4/Process/Base.lean Normal file
View File

@ -0,0 +1,198 @@
/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
namespace DocGen4.Process
open Lean Widget Meta
/--
Stores information about a typed name.
-/
structure NameInfo where
/--
The name that has this info attached.
-/
name : Name
/--
The pretty printed type of this name.
-/
type : CodeWithInfos
/--
The doc string of the name if it exists.
-/
doc : Option String
deriving Inhabited
/--
An argument to a declaration, e.g. the `(x : Nat)` in `def foo (x : Nat) := x`.
-/
structure Arg where
/--
The name of the argument. For auto generated argument names like `[Monad α]`
this is none
-/
name : Option Name
/--
The pretty printed type of the argument.
-/
type : CodeWithInfos
/--
What kind of binder was used for the argument.
-/
binderInfo : BinderInfo
/--
A base structure for information about a declaration.
-/
structure Info extends NameInfo where
/--
The list of arguments to the declaration.
-/
args : Array Arg
/--
In which lines the declaration was created.
-/
declarationRange : DeclarationRange
/--
A list of (known) attributes that are attached to the declaration.
-/
attrs : Array String
/--
Whether this info item should be rendered
-/
render : Bool := true
deriving Inhabited
/--
Information about an `axiom` declaration.
-/
structure AxiomInfo extends Info where
isUnsafe : Bool
deriving Inhabited
/--
Information about a `theorem` declaration.
-/
structure TheoremInfo extends Info
deriving Inhabited
/--
Information about an `opaque` declaration.
-/
structure OpaqueInfo extends Info where
/--
The pretty printed value of the declaration.
-/
value : CodeWithInfos
/--
A value of partial is interpreted as this opaque being part of a partial def
since the actual definition for a partial def is hidden behind an inaccessible value.
-/
definitionSafety : DefinitionSafety
deriving Inhabited
/--
Information about a `def` declaration, note that partial defs are handled by `OpaqueInfo`.
-/
structure DefinitionInfo extends Info where
isUnsafe : Bool
hints : ReducibilityHints
equations : Option (Array CodeWithInfos)
isNonComputable : Bool
deriving Inhabited
/--
Information about an `instance` declaration.
-/
structure InstanceInfo extends DefinitionInfo where
className : Name
typeNames : Array Name
deriving Inhabited
/--
Information about an `inductive` declaration
-/
structure InductiveInfo extends Info where
/--
List of all constructors of this inductive type.
-/
ctors : List NameInfo
isUnsafe : Bool
deriving Inhabited
/--
Information about a `structure` declaration.
-/
structure StructureInfo extends Info where
/--
Information about all the fields of the structure.
-/
fieldInfo : Array NameInfo
/--
All the structures this one inherited from.
-/
parents : Array Name
/--
The constructor of the structure.
-/
ctor : NameInfo
deriving Inhabited
/--
Information about a `class` declaration.
-/
abbrev ClassInfo := StructureInfo
/--
Information about a `class inductive` declaration.
-/
abbrev ClassInductiveInfo := InductiveInfo
/--
Information about a constructor of an inductive type
-/
abbrev ConstructorInfo := Info
/--
A general type for informations about declarations.
-/
inductive DocInfo where
| axiomInfo (info : AxiomInfo) : DocInfo
| theoremInfo (info : TheoremInfo) : DocInfo
| opaqueInfo (info : OpaqueInfo) : DocInfo
| definitionInfo (info : DefinitionInfo) : DocInfo
| instanceInfo (info : InstanceInfo) : DocInfo
| inductiveInfo (info : InductiveInfo) : DocInfo
| structureInfo (info : StructureInfo) : DocInfo
| classInfo (info : ClassInfo) : DocInfo
| classInductiveInfo (info : ClassInductiveInfo) : DocInfo
| ctorInfo (info : ConstructorInfo) : DocInfo
deriving Inhabited
/--
Turns an `Expr` into a pretty printed `CodeWithInfos`.
-/
def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do
let ⟨fmt, infos⟩ ← PrettyPrinter.ppExprWithInfos expr
let tt := TaggedText.prettyTagged fmt
let ctx := {
env := ← getEnv
mctx := ← getMCtx
options := ← getOptions
currNamespace := ← getCurrNamespace
openDecls := ← getOpenDecls
fileMap := default,
ngen := ← getNGen
}
return tagCodeInfos ctx infos tt
def isInstance (declName : Name) : MetaM Bool := do
return (instanceExtension.getState (← getEnv)).instanceNames.contains declName
end DocGen4.Process

View File

@ -0,0 +1,24 @@
/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
import DocGen4.Process.Base
import DocGen4.Process.NameInfo
import DocGen4.Process.StructureInfo
import DocGen4.Process.InductiveInfo
namespace DocGen4.Process
open Lean Meta
def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
StructureInfo.ofInductiveVal v
def ClassInductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInductiveInfo := do
InductiveInfo.ofInductiveVal v
end DocGen4.Process

View File

@ -0,0 +1,72 @@
/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
import DocGen4.Process.Base
import DocGen4.Process.NameInfo
namespace DocGen4.Process
open Lean Meta Widget
partial def stripArgs (e : Expr) (k : Expr → MetaM α) : MetaM α :=
match e.consumeMData with
| Expr.forallE name type body bi =>
let name := name.eraseMacroScopes
Meta.withLocalDecl name bi type fun fvar => do
stripArgs (Expr.instantiate1 body fvar) k
| _ => k e
def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do
withOptions (tactic.hygienic.set . false) do
lambdaTelescope v.value fun xs body => do
let us := v.levelParams.map mkLevelParam
let type ← mkEq (mkAppN (Lean.mkConst v.name us) xs) body
let type ← mkForallFVars xs type
return type
def processEq (eq : Name) : MetaM CodeWithInfos := do
let type ← (mkConstWithFreshMVarLevels eq >>= inferType)
stripArgs type prettyPrintTerm
def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
let info ← Info.ofConstantVal v.toConstantVal
let isUnsafe := v.safety == DefinitionSafety.unsafe
let isNonComputable := isNoncomputable (← getEnv) v.name
try
let eqs? ← getEqnsFor? v.name
match eqs? with
| some eqs =>
let equations ← eqs.mapM processEq
return {
toInfo := info,
isUnsafe,
hints := v.hints,
equations,
isNonComputable
}
| none =>
let equations := #[← stripArgs (← valueToEq v) prettyPrintTerm]
return {
toInfo := info,
isUnsafe,
hints := v.hints,
equations,
isNonComputable
}
catch err =>
IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {← err.toMessageData.toString}"
return {
toInfo := info,
isUnsafe,
hints := v.hints,
equations := none,
isNonComputable
}
end DocGen4.Process

View File

@ -0,0 +1,223 @@
/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
import DocGen4.Process.Base
import DocGen4.Process.AxiomInfo
import DocGen4.Process.TheoremInfo
import DocGen4.Process.OpaqueInfo
import DocGen4.Process.InstanceInfo
import DocGen4.Process.DefinitionInfo
import DocGen4.Process.ClassInfo
import DocGen4.Process.StructureInfo
import DocGen4.Process.InductiveInfo
namespace DocGen4.Process
namespace DocInfo
open Lean Meta Widget
def getDeclarationRange : DocInfo → DeclarationRange
| axiomInfo i => i.declarationRange
| theoremInfo i => i.declarationRange
| opaqueInfo i => i.declarationRange
| definitionInfo i => i.declarationRange
| instanceInfo i => i.declarationRange
| inductiveInfo i => i.declarationRange
| structureInfo i => i.declarationRange
| classInfo i => i.declarationRange
| classInductiveInfo i => i.declarationRange
| ctorInfo i => i.declarationRange
def getName : DocInfo → Name
| axiomInfo i => i.name
| theoremInfo i => i.name
| opaqueInfo i => i.name
| definitionInfo i => i.name
| instanceInfo i => i.name
| inductiveInfo i => i.name
| structureInfo i => i.name
| classInfo i => i.name
| classInductiveInfo i => i.name
| ctorInfo i => i.name
def getKind : DocInfo → String
| axiomInfo _ => "axiom"
| theoremInfo _ => "theorem"
| opaqueInfo _ => "opaque"
| definitionInfo _ => "def"
| instanceInfo _ => "instance"
| inductiveInfo _ => "inductive"
| structureInfo _ => "structure"
| classInfo _ => "class"
| classInductiveInfo _ => "class"
| ctorInfo _ => "ctor" -- TODO: kind ctor support in js
def getType : DocInfo → CodeWithInfos
| axiomInfo i => i.type
| theoremInfo i => i.type
| opaqueInfo i => i.type
| definitionInfo i => i.type
| instanceInfo i => i.type
| inductiveInfo i => i.type
| structureInfo i => i.type
| classInfo i => i.type
| classInductiveInfo i => i.type
| ctorInfo i => i.type
def getArgs : DocInfo → Array Arg
| axiomInfo i => i.args
| theoremInfo i => i.args
| opaqueInfo i => i.args
| definitionInfo i => i.args
| instanceInfo i => i.args
| inductiveInfo i => i.args
| structureInfo i => i.args
| classInfo i => i.args
| classInductiveInfo i => i.args
| ctorInfo i => i.args
def getAttrs : DocInfo → Array String
| axiomInfo i => i.attrs
| theoremInfo i => i.attrs
| opaqueInfo i => i.attrs
| definitionInfo i => i.attrs
| instanceInfo i => i.attrs
| inductiveInfo i => i.attrs
| structureInfo i => i.attrs
| classInfo i => i.attrs
| classInductiveInfo i => i.attrs
| ctorInfo i => i.attrs
def getDocString : DocInfo → Option String
| axiomInfo i => i.doc
| theoremInfo i => i.doc
| opaqueInfo i => i.doc
| definitionInfo i => i.doc
| instanceInfo i => i.doc
| inductiveInfo i => i.doc
| structureInfo i => i.doc
| classInfo i => i.doc
| classInductiveInfo i => i.doc
| ctorInfo i => i.doc
def shouldRender : DocInfo → Bool
| axiomInfo i => i.render
| theoremInfo i => i.render
| opaqueInfo i => i.render
| definitionInfo i => i.render
| instanceInfo i => i.render
| inductiveInfo i => i.render
| structureInfo i => i.render
| classInfo i => i.render
| classInductiveInfo i => i.render
| ctorInfo i => i.render
def isBlackListed (declName : Name) : MetaM Bool := do
match ← findDeclarationRanges? declName with
| some _ =>
let env ← getEnv
pure (declName.isInternal)
<||> (pure <| isAuxRecursor env declName)
<||> (pure <| isNoConfusion env declName)
<||> isRec declName
<||> isMatcher declName
-- TODO: Evaluate whether filtering out declarations without range is sensible
| none => return true
-- TODO: Is this actually the best way?
def isProjFn (declName : Name) : MetaM Bool := do
let env ← getEnv
match declName with
| Name.str parent name =>
if isStructure env parent then
match getStructureInfo? env parent with
| some i =>
match i.fieldNames.find? (· == name) with
| some _ => return true
| none => return false
| none => panic! s!"{parent} is not a structure"
else
return false
| _ => return false
def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := fun (name, info) => do
if ← isBlackListed name then
return none
match info with
| ConstantInfo.axiomInfo i => return some <| axiomInfo (← AxiomInfo.ofAxiomVal i)
| ConstantInfo.thmInfo i => return some <| theoremInfo (← TheoremInfo.ofTheoremVal i)
| ConstantInfo.opaqueInfo i => return some <| opaqueInfo (← OpaqueInfo.ofOpaqueVal i)
| ConstantInfo.defnInfo i =>
if ← isProjFn i.name then
let info ← DefinitionInfo.ofDefinitionVal i
return some <| definitionInfo { info with render := false }
else
if ← isInstance i.name then
let info ← InstanceInfo.ofDefinitionVal i
return some <| instanceInfo info
else
let info ← DefinitionInfo.ofDefinitionVal i
return some <| definitionInfo info
| ConstantInfo.inductInfo i =>
let env ← getEnv
if isStructure env i.name then
if isClass env i.name then
return some <| classInfo (← ClassInfo.ofInductiveVal i)
else
return some <| structureInfo (← StructureInfo.ofInductiveVal i)
else
if isClass env i.name then
return some <| classInductiveInfo (← ClassInductiveInfo.ofInductiveVal i)
else
return some <| inductiveInfo (← InductiveInfo.ofInductiveVal i)
| ConstantInfo.ctorInfo i =>
let info ← Info.ofConstantVal i.toConstantVal
return some <| ctorInfo { info with render := false }
-- we ignore these for now
| ConstantInfo.recInfo _ | ConstantInfo.quotInfo _ => return none
def getKindDescription : DocInfo → String
| axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom"
| theoremInfo _ => "theorem"
| opaqueInfo i =>
match i.definitionSafety with
| DefinitionSafety.safe => "opaque"
| DefinitionSafety.unsafe => "unsafe opaque"
| DefinitionSafety.partial => "partial def"
| definitionInfo i => Id.run do
let mut modifiers := #[]
if i.isUnsafe then
modifiers := modifiers.push "unsafe"
if i.isNonComputable then
modifiers := modifiers.push "noncomputable"
let defKind :=
if i.hints.isAbbrev then
"abbrev"
else
"def"
modifiers := modifiers.push defKind
return String.intercalate " " modifiers.toList
| instanceInfo i => Id.run do
let mut modifiers := #[]
if i.isUnsafe then
modifiers := modifiers.push "unsafe"
if i.isNonComputable then
modifiers := modifiers.push "noncomputable"
modifiers := modifiers.push "instance"
return String.intercalate " " modifiers.toList
| inductiveInfo i => if i.isUnsafe then "unsafe inductive" else "inductive"
| structureInfo _ => "structure"
| classInfo _ => "class"
| classInductiveInfo _ => "class inductive"
| ctorInfo _ => "constructor"
end DocInfo
end DocGen4.Process

View File

@ -0,0 +1,138 @@
/-
Copyright (c) 2021 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
import Lean.Data.HashMap
import DocGen4.Process.NameExt
def Lean.HashSet.fromArray [BEq α] [Hashable α] (xs : Array α) : Lean.HashSet α :=
xs.foldr (flip .insert) .empty
namespace DocGen4
open Lean Name
def getNLevels (name : Name) (levels: Nat) : Name :=
let components := name.componentsRev
(components.drop (components.length - levels)).reverse.foldl (· ++ ·) Name.anonymous
inductive Hierarchy where
| node (name : NameExt) (isFile : Bool) (children : RBNode NameExt (fun _ => Hierarchy)) : Hierarchy
instance : Inhabited Hierarchy := ⟨Hierarchy.node ⟨.anonymous, .html⟩ false RBNode.leaf⟩
abbrev HierarchyMap := RBNode NameExt (fun _ => Hierarchy)
-- Everything in this namespace is adapted from stdlib's RBNode
namespace HierarchyMap
def toList : HierarchyMap → List (NameExt × Hierarchy)
| t => t.revFold (fun ps k v => (k, v)::ps) []
def toArray : HierarchyMap → Array (NameExt × Hierarchy)
| t => t.fold (fun ps k v => ps ++ #[(k, v)] ) #[]
def hForIn [Monad m] (t : HierarchyMap) (init : σ) (f : (NameExt × Hierarchy) → σ → m (ForInStep σ)) : m σ :=
t.forIn init (fun a b acc => f (a, b) acc)
instance : ForIn m HierarchyMap (NameExt × Hierarchy) where
forIn := HierarchyMap.hForIn
end HierarchyMap
namespace Hierarchy
def empty (n : NameExt) (isFile : Bool) : Hierarchy :=
node n isFile RBNode.leaf
def getName : Hierarchy → Name
| node n _ _ => n.name
def getNameExt : Hierarchy → NameExt
| node n _ _ => n
def getChildren : Hierarchy → HierarchyMap
| node _ _ c => c
def isFile : Hierarchy → Bool
| node _ f _ => f
partial def insert! (h : Hierarchy) (n : NameExt) : Hierarchy := Id.run do
let hn := h.getNameExt
let mut cs := h.getChildren
if getNumParts hn.name + 1 == getNumParts n.name then
match cs.find NameExt.cmp n with
| none =>
node hn h.isFile (cs.insert NameExt.cmp n <| empty n true)
| some (node _ true _) => h
| some (node _ false ccs) =>
cs := cs.erase NameExt.cmp n
node hn h.isFile (cs.insert NameExt.cmp n <| node n true ccs)
else
let leveled := ⟨getNLevels n.name (getNumParts hn.name + 1), .html⟩
match cs.find NameExt.cmp leveled with
| some nextLevel =>
cs := cs.erase NameExt.cmp leveled
-- BUG?
node hn h.isFile <| cs.insert NameExt.cmp leveled (nextLevel.insert! n)
| none =>
let child := (insert! (empty leveled false) n)
node hn h.isFile <| cs.insert NameExt.cmp leveled child
partial def fromArray (names : Array Name) : Hierarchy :=
(names.map (fun n => NameExt.mk n .html)).foldl insert! (empty ⟨anonymous, .html⟩ false)
partial def fromArrayExt (names : Array NameExt) : Hierarchy :=
names.foldl insert! (empty ⟨anonymous, .html⟩ false)
def baseDirBlackList : HashSet String :=
HashSet.fromArray #[
"404.html",
"color-scheme.js",
"declaration-data.js",
"declarations",
"expand-nav.js",
"find",
"foundational_types.html",
"how-about.js",
"index.html",
"jump-src.js",
"mathjax-config.js",
"navbar.html",
"nav.js",
"search.html",
"search.js",
"src",
"style.css"
]
partial def fromDirectoryAux (dir : System.FilePath) (previous : Name) : IO (Array NameExt) := do
let mut children := #[]
for entry in ← System.FilePath.readDir dir do
if ← entry.path.isDir then
children := children ++ (← fromDirectoryAux entry.path (.str previous entry.fileName))
else if entry.path.extension = some "html" then
children := children.push <| ⟨.str previous (entry.fileName.dropRight ".html".length), .html⟩
else if entry.path.extension = some "pdf" then
children := children.push <| ⟨.str previous (entry.fileName.dropRight ".pdf".length), .pdf⟩
return children
def fromDirectory (dir : System.FilePath) : IO Hierarchy := do
let mut children := #[]
for entry in ← System.FilePath.readDir dir do
if baseDirBlackList.contains entry.fileName then
continue
else if ← entry.path.isDir then
children := children ++ (← fromDirectoryAux entry.path (.mkSimple entry.fileName))
else if entry.path.extension = some "html" then
children := children.push <| ⟨.mkSimple (entry.fileName.dropRight ".html".length), .html⟩
else if entry.path.extension = some "pdf" then
children := children.push <| ⟨.mkSimple (entry.fileName.dropRight ".pdf".length), .pdf⟩
return Hierarchy.fromArrayExt children
end Hierarchy
end DocGen4

View File

@ -0,0 +1,30 @@
/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
import DocGen4.Process.Base
import DocGen4.Process.NameInfo
namespace DocGen4.Process
open Lean Meta
def getConstructorType (ctor : Name) : MetaM Expr := do
let env ← getEnv
match env.find? ctor with
| some (ConstantInfo.ctorInfo i) => pure i.type
| _ => panic! s!"Constructor {ctor} was requested but does not exist"
def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do
let info ← Info.ofConstantVal v.toConstantVal
let ctors ← v.ctors.mapM (fun name => do NameInfo.ofTypedName name (← getConstructorType name))
return {
toInfo := info,
ctors,
isUnsafe := v.isUnsafe
}
end DocGen4.Process

View File

@ -0,0 +1,45 @@
/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
import DocGen4.Process.Base
import DocGen4.Process.NameInfo
import DocGen4.Process.DefinitionInfo
namespace DocGen4.Process
open Lean Meta
def getInstanceTypes (typ : Expr) : MetaM (Array Name) := do
let (_, _, tail) ← forallMetaTelescopeReducing typ
let args := tail.getAppArgs
let (_, bis, _) ← forallMetaTelescopeReducing (← inferType tail.getAppFn)
let (_, names) ← (bis.zip args).mapM findName |>.run .empty
return names
where
findName : BinderInfo × Expr → StateRefT (Array Name) MetaM Unit
| (.default, .sort .zero) => modify (·.push "_builtin_prop")
| (.default, .sort (.succ _)) => modify (·.push "_builtin_typeu")
| (.default, .sort _) => modify (·.push "_builtin_sortu")
| (.default, e) =>
match e.getAppFn with
| .const name .. => modify (·.push name)
| _ => return ()
| _ => return ()
def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do
let mut info ← DefinitionInfo.ofDefinitionVal v
let some className ← isClass? v.type | panic! s!"isClass? on {v.name} returned none"
if let some instAttr ← getDefaultInstance v.name className then
info := { info with attrs := info.attrs.push instAttr }
let typeNames ← getInstanceTypes v.type
return {
toDefinitionInfo := info,
className,
typeNames
}
end DocGen4.Process

View File

@ -0,0 +1,48 @@
/-
A generalization of `Lean.Name` that includes a file extension.
-/
import Lean
open Lean Name
inductive Extension where
| html
| pdf
deriving Repr
namespace Extension
def cmp : Extension → Extension → Ordering
| html, html => Ordering.eq
| html, _ => Ordering.lt
| pdf, pdf => Ordering.eq
| pdf, _ => Ordering.gt
instance : BEq Extension where
beq e1 e2 :=
match cmp e1 e2 with
| Ordering.eq => true
| _ => false
def toString : Extension → String
| html => "html"
| pdf => "pdf"
end Extension
structure NameExt where
name : Name
ext : Extension
namespace NameExt
def cmp (n₁ n₂ : NameExt) : Ordering :=
match Name.cmp n₁.name n₂.name with
| Ordering.eq => Extension.cmp n₁.ext n₂.ext
| ord => ord
def getString! : NameExt → String
| ⟨str _ s, _⟩ => s
| _ => unreachable!
end NameExt

View File

@ -0,0 +1,56 @@
/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
import DocGen4.Process.Base
import DocGen4.Process.Attributes
namespace DocGen4.Process
open Lean Meta
def NameInfo.ofTypedName (n : Name) (t : Expr) : MetaM NameInfo := do
let env ← getEnv
return { name := n, type := ← prettyPrintTerm t, doc := ← findDocString? env n}
partial def argTypeTelescope {α : Type} (e : Expr) (k : Array ((Option Name) × Expr × BinderInfo) → Expr → MetaM α) : MetaM α :=
go e #[]
where
go (e : Expr) (args : Array ((Option Name) × Expr × BinderInfo)) : MetaM α := do
let helper := fun name type body bi =>
-- Once we hit a name with a macro scope we stop traversing the expression
-- and print what is left after the : instead. The only exception
-- to this is instances since these almost never have a name
-- but should still be printed as arguments instead of after the :.
if bi.isInstImplicit && name.hasMacroScopes then
let arg := (none, type, bi)
Meta.withLocalDecl name bi type fun fvar => do
go (Expr.instantiate1 body fvar) (args.push arg)
else if name.hasMacroScopes then
k args e
else
let arg := (some name, type, bi)
Meta.withLocalDecl name bi type fun fvar => do
go (Expr.instantiate1 body fvar) (args.push arg)
match e.consumeMData with
| Expr.forallE name type body binderInfo => helper name type body binderInfo
| _ => k args e
def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
argTypeTelescope v.type fun args type => do
let args ← args.mapM (fun (n, e, b) => do return Arg.mk n (← prettyPrintTerm e) b)
let nameInfo ← NameInfo.ofTypedName v.name type
match ← findDeclarationRanges? v.name with
-- TODO: Maybe selection range is more relevant? Figure this out in the future
| some range =>
return {
toNameInfo := nameInfo,
args,
declarationRange := range.range,
attrs := ← getAllAttributes v.name
}
| none => panic! s!"{v.name} is a declaration without position"
end DocGen4.Process

View File

@ -0,0 +1,33 @@
/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
import DocGen4.Process.Base
import DocGen4.Process.NameInfo
namespace DocGen4.Process
open Lean Meta
def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do
let info ← Info.ofConstantVal v.toConstantVal
let value ← prettyPrintTerm v.value
let env ← getEnv
let isPartial := env.find? (Compiler.mkUnsafeRecName v.name) |>.isSome
let definitionSafety :=
if isPartial then
DefinitionSafety.partial
else if v.isUnsafe then
DefinitionSafety.unsafe
else
DefinitionSafety.safe
return {
toInfo := info,
value,
definitionSafety
}
end DocGen4.Process

View File

@ -0,0 +1,58 @@
/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
import DocGen4.Process.Base
import DocGen4.Process.NameInfo
namespace DocGen4.Process
open Lean Meta
/--
Execute `k` with an array containing pairs `(fieldName, fieldType)`.
`k` is executed in an updated local context which contains local declarations for the `structName` parameters.
-/
def withFields (info : InductiveVal) (k : Array (Name × Expr) → MetaM α) (includeSubobjectFields : Bool := false) : MetaM α := do
let structName := info.name
let us := info.levelParams.map mkLevelParam
forallTelescopeReducing info.type fun params _ =>
withLocalDeclD `s (mkAppN (mkConst structName us) params) fun s => do
let mut info := #[]
for fieldName in getStructureFieldsFlattened (← getEnv) structName includeSubobjectFields do
let proj ← mkProjection s fieldName
info := info.push (fieldName, (← inferType proj))
k info
def getFieldTypes (v : InductiveVal) : MetaM (Array NameInfo) := do
withFields v fun fields =>
fields.foldlM (init := #[]) (fun acc (name, type) => do return acc.push (← NameInfo.ofTypedName (v.name.append name) type))
def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
let info ← Info.ofConstantVal v.toConstantVal
let env ← getEnv
let parents := getParentStructures env v.name
let ctorVal := getStructureCtor env v.name
let ctor ← NameInfo.ofTypedName ctorVal.name ctorVal.type
match getStructureInfo? env v.name with
| some i =>
if i.fieldNames.size - parents.size > 0 then
return {
toInfo := info,
fieldInfo := ← getFieldTypes v,
parents,
ctor
}
else
return {
toInfo := info,
fieldInfo := #[],
parents,
ctor
}
| none => panic! s!"{v.name} is not a structure"
end DocGen4.Process

View File

@ -0,0 +1,19 @@
/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
import DocGen4.Process.Base
import DocGen4.Process.NameInfo
namespace DocGen4.Process
open Lean Meta
def TheoremInfo.ofTheoremVal (v : TheoremVal) : MetaM TheoremInfo := do
let info ← Info.ofConstantVal v.toConstantVal
return { toInfo := info }
end DocGen4.Process

14
Makefile Normal file
View File

@ -0,0 +1,14 @@
all:
@echo "Please specify a build target."
docs:
-ls build/doc | \
grep -v -E 'Init|Lean|Mathlib' | \
xargs -I {} rm -r "build/doc/{}"
-./scripts/run_pdflatex.sh build > /dev/null
lake build Bookshelf:docs
docs!:
-rm -r build/doc
-./scripts/run_pdflatex.sh build > /dev/null
lake build Bookshelf:docs

View File

@ -1,11 +1,7 @@
# bookshelf
A study of the books listed below.
## Overview
Most proofs are conducted in LaTeX. Where feasible, theorems are also formally
proven in [Lean](https://leanprover.github.io/).
A study of the books listed below. Most proofs are conducted in LaTeX. Where
feasible, theorems are also formally proven in [Lean](https://leanprover.github.io/).
- [ ] Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an Introduction to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.
- [x] Avigad, Jeremy. Theorem Proving in Lean, n.d.
@ -18,21 +14,23 @@ proven in [Lean](https://leanprover.github.io/).
- [ ] Ross, Sheldon. A First Course in Probability Theory. 8th ed. Pearson Prentice Hall, n.d.
- [ ] Smullyan, Raymond M. To Mock a Mockingbird: And Other Logic Puzzles Including an Amazing Adventure in Combinatory Logic. Oxford: Oxford university press, 2000.
## Building
## Documentation
This project has absorbed [doc-gen4](https://github.com/leanprover/doc-gen4) to
ease customization. In particular, the `DocGen4` module found in this project
allows generating PDFs and including them in the navbar. To generate
documentation and serve files locally, run the following:
[direnv](https://direnv.net/) can be used to launch a dev shell upon entering
this directory (refer to `.envrc`). Otherwise run via:
```bash
$ nix develop
> make docs[!]
> lake run server
```
If you prefer not to use `nix`, you can also use the [elan](https://github.com/leanprover/elan)
package manager like normal. Afterward, build the project by running
```bash
$ lake build
```
Optionally build documentation by running:
```bash
$ lake build Bookshelf:docs
```
Afterward, you can view the generated files by running `python3 -m http.server`
from within the `.lake/build/doc` directory.
The `docs` build target avoids cleaning files that are expected to not change
often (e.g. `Lean`, `Init`, and `Mathlib` related content). If you've upgraded
Lean or Mathlib, run `make docs!` instead to generate documentation from
scratch.
Both assume you have `pdflatex` and `python3` available in your `$PATH`. To
change how the server behaves, refer to the `.env` file located in the root
directory of this project.

View File

@ -1,76 +0,0 @@
{
"nodes": {
"flake-compat": {
"locked": {
"lastModified": 1696426674,
"narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=",
"rev": "0f9255e01c2351cc7d116c072cb317785dd33b33",
"revCount": 57,
"type": "tarball",
"url": "https://api.flakehub.com/f/pinned/edolstra/flake-compat/1.0.1/018afb31-abd1-7bff-a5e4-cff7e18efb7a/source.tar.gz"
},
"original": {
"type": "tarball",
"url": "https://flakehub.com/f/edolstra/flake-compat/1.tar.gz"
}
},
"flake-utils": {
"inputs": {
"systems": "systems"
},
"locked": {
"lastModified": 1701680307,
"narHash": "sha256-kAuep2h5ajznlPMD9rnQyffWG8EM/C73lejGofXvdM8=",
"owner": "numtide",
"repo": "flake-utils",
"rev": "4022d587cbbfd70fe950c1e2083a02621806a725",
"type": "github"
},
"original": {
"owner": "numtide",
"repo": "flake-utils",
"type": "github"
}
},
"nixpkgs": {
"locked": {
"lastModified": 1702312524,
"narHash": "sha256-gkZJRDBUCpTPBvQk25G0B7vfbpEYM5s5OZqghkjZsnE=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "a9bf124c46ef298113270b1f84a164865987a91c",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixos-unstable",
"repo": "nixpkgs",
"type": "github"
}
},
"root": {
"inputs": {
"flake-compat": "flake-compat",
"flake-utils": "flake-utils",
"nixpkgs": "nixpkgs"
}
},
"systems": {
"locked": {
"lastModified": 1681028828,
"narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
"owner": "nix-systems",
"repo": "default",
"rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
"type": "github"
},
"original": {
"owner": "nix-systems",
"repo": "default",
"type": "github"
}
}
},
"root": "root",
"version": 7
}

View File

@ -1,79 +0,0 @@
{
description = "";
inputs = {
flake-compat.url = "https://flakehub.com/f/edolstra/flake-compat/1.tar.gz";
flake-utils.url = "github:numtide/flake-utils";
nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
};
outputs = { self, nixpkgs, flake-utils, ... }:
flake-utils.lib.eachDefaultSystem (system:
let
pkgs = nixpkgs.legacyPackages.${system};
manifest = import ./lake-manifest.nix { inherit pkgs; };
scheme-custom = with pkgs; (texlive.combine {
inherit (texlive) scheme-basic
bigfoot
comment
enumitem
environ
etoolbox
fontawesome5
jknapltx
mathabx
mathabx-type1
metafont
ncctools
pgf
rsfs
soul
stmaryrd
tcolorbox
xcolor;
});
in
{
packages = {
app = pkgs.stdenv.mkDerivation {
pname = "bookshelf";
version = "0.1.0";
src = ./.;
nativeBuildInputs = with pkgs; [
git
lean4
scheme-custom
];
buildPhase = ''
mkdir -p .lake/packages
${pkgs.lib.foldlAttrs (s: key: val: s + ''
cp -a ${val}/src .lake/packages/${key}
chmod 755 .lake/packages/${key}/{,.git}
'') "" manifest}
export GIT_ORIGIN_URL="https://github.com/jrpotter/bookshelf.git"
export GIT_REVISION="${self.rev or "dirty"}"
lake build Bookshelf:docs
find .lake/build/doc \
\( -name "*.html.trace" -o -name "*.html.hash" \) \
-exec rm {} +
'';
installPhase = ''
mkdir $out
cp -a .lake/build/doc/* $out
'';
};
default = self.packages.${system}.app;
};
devShells.default = pkgs.mkShell {
packages = with pkgs; [
lean4
python3
scheme-custom
];
};
});
}

View File

@ -1,95 +1,76 @@
{"version": 7,
"packagesDir": ".lake/packages",
{"version": 6,
"packagesDir": "lake-packages",
"packages":
[{"url": "https://github.com/leanprover/std4.git",
"type": "git",
"subDir": null,
"rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
"name": "std",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.3.0",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/quote4",
"type": "git",
"subDir": null,
"rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755",
"name": "Qq",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
"rev": "c7cff4551258d31c0d2d453b3f9cbca757d445f1",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/ProofWidgets4",
"type": "git",
"subDir": null,
"rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749",
"name": "proofwidgets",
"manifestFile": "lake-manifest.json",
"inputRev": "v0.0.23",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/lean4-cli",
"type": "git",
"subDir": null,
"rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
"name": "Cli",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git",
"subDir": null,
"rev": "f04afed5ac9fea0e1355bc6f6bee2bd01f4a888d",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.3.0",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/xubaiw/CMark.lean",
"type": "git",
"subDir": null,
"rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
"name": "CMark",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
"type": "git",
"subDir": null,
"rev": "dc62b29a26fcc3da545472ab8ad2c98ef3433634",
"name": "UnicodeBasic",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/hargonix/LeanInk",
"type": "git",
"subDir": null,
"rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
"name": "leanInk",
"manifestFile": "lake-manifest.json",
"inputRev": "doc-gen",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/jrpotter/bookshelf-doc",
"type": "git",
"subDir": null,
"rev": "9bd217dc37ea79a3f118a313583f539cdbc762e6",
"name": "«doc-gen4»",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": false,
"configFile": "lakefile.lean"}],
"name": "bookshelf",
"lakeDir": ".lake"}
[{"git":
{"url": "https://github.com/mhuisi/lean4-cli",
"subDir?": null,
"rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
"opts": {},
"name": "Cli",
"inputRev?": "nightly",
"inherited": false}},
{"git":
{"url": "https://github.com/xubaiw/CMark.lean",
"subDir?": null,
"rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
"opts": {},
"name": "CMark",
"inputRev?": "main",
"inherited": false}},
{"git":
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
"subDir?": null,
"rev": "280d75fdfe7be8eb337be7f1bf8479b4aac09f71",
"opts": {},
"name": "UnicodeBasic",
"inputRev?": "main",
"inherited": false}},
{"git":
{"url": "https://github.com/hargonix/LeanInk",
"subDir?": null,
"rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
"opts": {},
"name": "leanInk",
"inputRev?": "doc-gen",
"inherited": false}},
{"git":
{"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null,
"rev": "c97b9b00802c2ed343d9ac73e59be287428dbcf0",
"opts": {},
"name": "mathlib",
"inputRev?": "master",
"inherited": false}},
{"git":
{"url": "https://github.com/leanprover/std4.git",
"subDir?": null,
"rev": "87b0742b01e45c6cc53cd3043fe3c7cdbf87a56f",
"opts": {},
"name": "std",
"inputRev?": "main",
"inherited": false}},
{"git":
{"url": "https://github.com/leanprover-community/quote4",
"subDir?": null,
"rev": "511eb96eca98a7474683b8ae55193a7e7c51bc39",
"opts": {},
"name": "Qq",
"inputRev?": "master",
"inherited": true}},
{"git":
{"url": "https://github.com/leanprover-community/aesop",
"subDir?": null,
"rev": "cb87803274405db79ec578fc07c4730c093efb90",
"opts": {},
"name": "aesop",
"inputRev?": "master",
"inherited": true}},
{"git":
{"url": "https://github.com/leanprover-community/ProofWidgets4",
"subDir?": null,
"rev": "f1a5c7808b001305ba07d8626f45ee054282f589",
"opts": {},
"name": "proofwidgets",
"inputRev?": "v0.0.21",
"inherited": true}}],
"name": "bookshelf"}

View File

@ -1,119 +0,0 @@
{ pkgs }:
let
fetchGitPackage = { pname, version, owner, repo, rev, hash }:
pkgs.stdenv.mkDerivation {
inherit pname version;
src = pkgs.fetchgit {
inherit rev hash;
url = "https://github.com/${owner}/${repo}";
# We need to keep this attribute enabled to prevent Lake from trying to
# update the package. This attribute ensures the specified commit is
# accessible at HEAD:
# https://github.com/leanprover/lean4/blob/cddc8089bc736a1532d6092f69476bd2d205a9eb/src/lake/Lake/Load/Materialize.lean#L22
leaveDotGit = true;
};
nativeBuildInputs = with pkgs; [ git ];
# Lake will perform a compulsory check that `git remote get-url origin`
# returns the value we set here:
# https://github.com/leanprover/lean4/blob/cddc8089bc736a1532d6092f69476bd2d205a9eb/src/lake/Lake/Load/Materialize.lean#L54
buildPhase = ''
git remote add origin https://github.com/${owner}/${repo}
'';
installPhase = ''
shopt -s dotglob
mkdir -p $out/src
cp -a . $out/src
'';
};
in
{
CMark = fetchGitPackage {
pname = "CMark";
version = "main";
owner = "xubaiw";
repo = "CMark.lean";
rev = "0077cbbaa92abf855fc1c0413e158ffd8195ec77";
hash = "sha256-ge+9V4IsMdPwjhYu66zUUN6CK70K2BdMT98BzBV3a4c=";
};
Cli = fetchGitPackage {
pname = "Cli";
version = "main";
owner = "leanprover";
repo = "lean4-cli";
rev = "a751d21d4b68c999accb6fc5d960538af26ad5ec";
hash = "sha256-n+6x7ZhyKKiIMZ9cH9VV8zay3oTUlJojtxcLYsUwQPU=";
};
Qq = fetchGitPackage {
pname = "Qq";
version = "master";
owner = "leanprover-community";
repo = "quote4";
rev = "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755";
hash = "sha256-l+X+Mi4khC/xdwQmESz8Qzto6noYqhYN4UqC+TVt3cs=";
};
UnicodeBasic = fetchGitPackage {
pname = "UnicodeBasic";
version = "main";
owner = "fgdorais";
repo = "lean4-unicode-basic";
rev = "dc62b29a26fcc3da545472ab8ad2c98ef3433634";
hash = "sha256-EimohrYMr01CnGx8xCg4q4XX663QuxKfpTDNnDnosO4=";
};
aesop = fetchGitPackage {
pname = "aesop";
version = "master";
owner = "leanprover-community";
repo = "aesop";
rev = "c7cff4551258d31c0d2d453b3f9cbca757d445f1";
hash = "sha256-uzkxE9XJ4y3WMtmiNQn2Je1hNkQ2FgE1/0vqz8f98cw=";
};
doc-gen4 = fetchGitPackage {
pname = "doc-gen4";
version = "main";
owner = "jrpotter";
repo = "bookshelf-doc";
rev = "9bd217dc37ea79a3f118a313583f539cdbc762e6";
hash = "sha256-L7Uca5hJV19/WHYG+MkFWX6BwXDInfSYsOrnZdM9ejY=";
};
leanInk = fetchGitPackage {
pname = "leanInk";
version = "doc-gen";
owner = "hargonix";
repo = "LeanInk";
rev = "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1";
hash = "sha256-asHVaa1uOxpz5arCvfllIrJmMC9VDm1F+bufsu3XwN0=";
};
mathlib = fetchGitPackage {
pname = "mathlib";
version = "v4.3.0";
owner = "leanprover-community";
repo = "mathlib4.git";
rev = "f04afed5ac9fea0e1355bc6f6bee2bd01f4a888d";
hash = "sha256-B0pZ7HwJwOrEXTMMyJSzMLLyh66Bcs/CqNwC3EKZ60I=";
};
proofwidgets = fetchGitPackage {
pname = "proofwidgets";
version = "v0.0.23";
owner = "leanprover-community";
repo = "ProofWidgets4";
rev = "909febc72b4f64628f8d35cd0554f8a90b6e0749";
hash = "sha256-twXXKXXONQpfzG+YLoXYY+3kTU0F40Tsv2+SKfF2Qsc=";
};
std = fetchGitPackage {
pname = "std";
version = "v4.3.0";
owner = "leanprover";
repo = "std4";
rev = "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087";
hash = "sha256-agWcsRIEJbHSjIdiA6z/HQHLZkb72ASW9SPnIM0voeo=";
};
}

View File

@ -4,17 +4,232 @@ open System Lake DSL
package «bookshelf»
-- ========================================
-- Imports
-- ========================================
require Cli from git
"https://github.com/mhuisi/lean4-cli" @
"nightly"
require CMark from git
"https://github.com/xubaiw/CMark.lean" @
"main"
require UnicodeBasic from git
"https://github.com/fgdorais/lean4-unicode-basic" @
"main"
require leanInk from git
"https://github.com/hargonix/LeanInk" @
"doc-gen"
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git" @
"v4.3.0"
"master"
require std from git
"https://github.com/leanprover/std4.git" @
"v4.3.0"
require «doc-gen4» from git
"https://github.com/jrpotter/bookshelf-doc" @
"main"
-- ========================================
-- Documentation Generator
-- ========================================
lean_lib DocGen4
lean_exe «doc-gen4» {
root := `Main
supportInterpreter := true
}
/--
Turns a Github git remote URL into an HTTPS Github URL.
Three link types from git supported:
- https://github.com/org/repo
- https://github.com/org/repo.git
- git@github.com:org/repo.git
TODO: This function is quite brittle and very Github specific, we can
probably do better.
-/
def getGithubBaseUrl (gitUrl : String) : String := Id.run do
let mut url := gitUrl
if url.startsWith "git@" then
url := url.drop 15
url := url.dropRight 4
return s!"https://github.com/{url}"
else if url.endsWith ".git" then
return url.dropRight 4
else
return url
/--
Obtain the Github URL of a project by parsing the origin remote.
-/
def getProjectGithubUrl (directory : System.FilePath := "." ) : IO String := do
let out ← IO.Process.output {
cmd := "git",
args := #["remote", "get-url", "origin"],
cwd := directory
}
if out.exitCode != 0 then
throw <| IO.userError <| s!"git exited with code {out.exitCode} while looking for the git remote in {directory}"
return out.stdout.trimRight
/--
Obtain the git commit hash of the project that is currently getting analyzed.
-/
def getProjectCommit (directory : System.FilePath := "." ) : IO String := do
let out ← IO.Process.output {
cmd := "git",
args := #["rev-parse", "HEAD"]
cwd := directory
}
if out.exitCode != 0 then
throw <| IO.userError <| s!"git exited with code {out.exitCode} while looking for the current commit in {directory}"
return out.stdout.trimRight
def getGitUrl (pkg : Package) (lib : LeanLibConfig) (mod : Module) : IO String := do
let baseUrl := getGithubBaseUrl (← getProjectGithubUrl pkg.dir)
let commit ← getProjectCommit pkg.dir
let parts := mod.name.components.map toString
let path := String.intercalate "/" parts
let libPath := pkg.config.srcDir / lib.srcDir
let basePath := String.intercalate "/" (libPath.components.filter (· != "."))
let url := s!"{baseUrl}/blob/{commit}/{basePath}/{path}.lean"
return url
module_facet docs (mod) : FilePath := do
let some docGen4 ← findLeanExe? `«doc-gen4»
| error "no doc-gen4 executable configuration found in workspace"
let exeJob ← docGen4.exe.fetch
let modJob ← mod.leanArts.fetch
let ws ← getWorkspace
let pkg ← ws.packages.find? (·.isLocalModule mod.name)
let libConfig ← pkg.leanLibConfigs.toArray.find? (·.isLocalModule mod.name)
-- Build all documentation imported modules
let imports ← mod.imports.fetch
let depDocJobs ← BuildJob.mixArray <| ← imports.mapM fun mod => fetch <| mod.facet `docs
let gitUrl ← getGitUrl pkg libConfig mod
let buildDir := ws.root.buildDir
let docFile := mod.filePath (buildDir / "doc") "html"
depDocJobs.bindAsync fun _ depDocTrace => do
exeJob.bindAsync fun exeFile exeTrace => do
modJob.bindSync fun _ modTrace => do
let depTrace := mixTraceArray #[exeTrace, modTrace, depDocTrace]
let trace ← buildFileUnlessUpToDate docFile depTrace do
logStep s!"Documenting module: {mod.name}"
proc {
cmd := exeFile.toString
args := #["single", mod.name.toString, gitUrl]
env := ← getAugmentedEnv
}
return (docFile, trace)
-- TODO: technically speaking this facet does not show all file dependencies
target coreDocs : FilePath := do
let some docGen4 ← findLeanExe? `«doc-gen4»
| error "no doc-gen4 executable configuration found in workspace"
let exeJob ← docGen4.exe.fetch
let basePath := (←getWorkspace).root.buildDir / "doc"
let dataFile := basePath / "declarations" / "declaration-data-Lean.bmp"
exeJob.bindSync fun exeFile exeTrace => do
let trace ← buildFileUnlessUpToDate dataFile exeTrace do
logStep "Documenting Lean core: Init and Lean"
proc {
cmd := exeFile.toString
args := #["genCore"]
env := ← getAugmentedEnv
}
return (dataFile, trace)
library_facet docs (lib) : FilePath := do
-- Ordering is important. The index file is generated by walking through the
-- filesystem directory. Files copied from the shell scripts need to exist
-- prior to this.
let mods ← lib.modules.fetch
let moduleJobs ← BuildJob.mixArray <| ← mods.mapM (fetch <| ·.facet `docs)
let coreJob : BuildJob FilePath ← coreDocs.fetch
let exeJob ← «doc-gen4».fetch
-- Shared with DocGen4.Output
let basePath := (←getWorkspace).root.buildDir / "doc"
let dataFile := basePath / "declarations" / "declaration-data.bmp"
let staticFiles := #[
basePath / "style.css",
basePath / "declaration-data.js",
basePath / "color-scheme.js",
basePath / "nav.js",
basePath / "jump-src.js",
basePath / "expand-nav.js",
basePath / "how-about.js",
basePath / "search.js",
basePath / "mathjax-config.js",
basePath / "instances.js",
basePath / "importedBy.js",
basePath / "index.html",
basePath / "404.html",
basePath / "navbar.html",
basePath / "search.html",
basePath / "find" / "index.html",
basePath / "find" / "find.js",
basePath / "src" / "alectryon.css",
basePath / "src" / "alectryon.js",
basePath / "src" / "docutils_basic.css",
basePath / "src" / "pygments.css"
]
coreJob.bindAsync fun _ coreInputTrace => do
exeJob.bindAsync fun exeFile exeTrace => do
moduleJobs.bindSync fun _ inputTrace => do
let depTrace := mixTraceArray #[inputTrace, exeTrace, coreInputTrace]
let trace ← buildFileUnlessUpToDate dataFile depTrace do
logInfo "Documentation indexing"
proc {
cmd := exeFile.toString
args := #["index"]
}
let traces ← staticFiles.mapM computeTrace
let indexTrace := mixTraceArray traces
return (dataFile, trace.mix indexTrace)
-- ========================================
-- Bookshelf
-- ========================================
@[default_target]
lean_lib «Bookshelf» {
roots := #[`Bookshelf, `Common]
}
/--
The contents of our `.env` file.
-/
structure Config where
port : Nat := 5555
/--
Read in the `.env` file into an in-memory structure.
-/
private def readConfig : StateT Config ScriptM Unit := do
let env <- IO.FS.readFile ".env"
for line in env.trim.split (fun c => c == '\n') do
match line.split (fun c => c == '=') with
| ["PORT", port] => modify (fun c => { c with port := String.toNat! port })
| _ => error "Malformed `.env` file."
return ()
/--
Start an HTTP server for locally serving documentation. It is expected the
documentation has already been generated prior via
```bash
> lake build Bookshelf:docs
```
USAGE:
lake run server
-/
script server (_args) do
let ((), config) <- StateT.run readConfig {}
IO.println s!"Running Lean on `http://localhost:{config.port}`"
_ <- IO.Process.run {
cmd := "python3",
args := #["-m", "http.server", toString config.port, "-d", "build/doc"],
}
return 0

View File

@ -1 +1 @@
leanprover/lean4:v4.3.0
leanprover/lean4:v4.3.0-rc1

26
scripts/run_pdflatex.sh Executable file
View File

@ -0,0 +1,26 @@
#!/usr/bin/env bash
if ! command -v pdflatex > /dev/null; then
>&2 echo 'pdflatex was not found in the current $PATH.'
exit 1
fi
BUILD_DIR="$1"
function process_file () {
REL_DIR=$(dirname "$1")
REL_BASE=$(basename -s ".tex" "$1")
mkdir -p "$BUILD_DIR/doc/$REL_DIR"
(cd "$REL_DIR" && pdflatex "$REL_BASE.tex")
cp "$REL_DIR/$REL_BASE.pdf" "$BUILD_DIR/doc/$REL_DIR/"
}
export BUILD_DIR
export -f process_file
# We run this command twice to allow any cross-references to resolve correctly.
# https://tex.stackexchange.com/questions/41539/does-hyperref-work-between-two-files
for _ in {1..2}; do
find ./* \( -path build -o -path lake-packages \) -prune -o -name "*.tex" -print0 \
| xargs -0 -I{} bash -c "process_file {}"
done

View File

@ -0,0 +1,777 @@
@charset "UTF-8";
/*
Copyright © 2019 Clément Pit-Claudel
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.
*/
/*******************************/
/* CSS reset for .alectryon-io */
/*******************************/
.alectryon-io blockquote {
line-height: inherit;
}
.alectryon-io blockquote:after {
display: none;
}
.alectryon-io label {
display: inline;
font-size: inherit;
margin: 0;
}
.alectryon-io a {
text-decoration: none !important;
font-style: oblique !important;
color: unset;
}
/* Undo <small> and <blockquote>, added to improve RSS rendering. */
.alectryon-io small.alectryon-output,
.alectryon-io small.alectryon-type-info {
font-size: inherit;
}
.alectryon-io blockquote.alectryon-goal,
.alectryon-io blockquote.alectryon-message {
font-weight: normal;
font-size: inherit;
}
/***************/
/* Main styles */
/***************/
.alectryon-coqdoc .doc .code,
.alectryon-coqdoc .doc .comment,
.alectryon-coqdoc .doc .inlinecode,
.alectryon-mref,
.alectryon-block, .alectryon-io,
.alectryon-toggle-label, .alectryon-banner {
font-family: "Source Code Pro", Consolas, "Ubuntu Mono", Menlo, "DejaVu Sans Mono", monospace, monospace !important;
font-size: 0.875em;
font-feature-settings: "COQX" 1 /* Coq ligatures */, "XV00" 1 /* Legacy */, "calt" 1 /* Fallback */;
line-height: initial;
}
.alectryon-io, .alectryon-block, .alectryon-toggle-label, .alectryon-banner {
overflow: visible;
overflow-wrap: break-word;
position: relative;
white-space: pre-wrap;
}
/*
CoqIDE doesn't turn off the unicode bidirectional algorithm (and PG simply
respects the user's `bidi-display-reordering` setting), so don't turn it off
here either. But beware unexpected results like `Definition test_אב := 0.`
.alectryon-io span {
direction: ltr;
unicode-bidi: bidi-override;
}
In any case, make an exception for comments:
.highlight .c {
direction: embed;
unicode-bidi: initial;
}
*/
.alectryon-mref,
.alectryon-mref-marker {
align-self: center;
box-sizing: border-box;
display: inline-block;
font-size: 80%;
font-weight: bold;
line-height: 1;
box-shadow: 0 0 0 1pt black;
padding: 1pt 0.3em;
text-decoration: none;
}
.alectryon-block .alectryon-mref-marker,
.alectryon-io .alectryon-mref-marker {
user-select: none;
margin: -0.25em 0 -0.25em 0.5em;
}
.alectryon-inline .alectryon-mref-marker {
margin: -0.25em 0.15em -0.25em 0.625em; /* 625 = 0.5em / 80% */
}
.alectryon-mref {
color: inherit;
margin: -0.5em 0.25em;
}
.alectryon-goal:target .goal-separator .alectryon-mref-marker,
:target > .alectryon-mref-marker {
animation: blink 0.2s step-start 0s 3 normal none;
background-color: #fcaf3e;
position: relative;
}
@keyframes blink {
50% {
box-shadow: 0 0 0 3pt #fcaf3e, 0 0 0 4pt black;
z-index: 10;
}
}
.alectryon-toggle,
.alectryon-io .alectryon-extra-goal-toggle {
display: none;
}
.alectryon-bubble,
.alectryon-io label,
.alectryon-toggle-label {
cursor: pointer;
}
.alectryon-toggle-label {
display: block;
font-size: 0.8em;
}
.alectryon-io .alectryon-input {
padding: 0.1em 0; /* Enlarge the hitbox slightly to fill interline gaps */
}
.alectryon-io .alectryon-token {
white-space: pre-wrap;
display: inline;
}
.alectryon-io .alectryon-sentence.alectryon-target .alectryon-input {
/* FIXME if keywords were bolder we wouldn't need !important */
font-weight: bold !important; /* Use !important to avoid a * selector */
}
.alectryon-bubble:before,
.alectryon-toggle-label:before,
.alectryon-io label.alectryon-input:after,
.alectryon-io .alectryon-goal > label:before {
border: 1px solid #babdb6;
border-radius: 1em;
box-sizing: border-box;
content: '';
display: inline-block;
font-weight: bold;
height: 0.25em;
margin-bottom: 0.15em;
vertical-align: middle;
width: 0.75em;
}
.alectryon-toggle-label:before,
.alectryon-io .alectryon-goal > label:before {
margin-right: 0.25em;
}
.alectryon-io .alectryon-goal > label:before {
margin-top: 0.125em;
}
.alectryon-io label.alectryon-input {
padding-right: 1em; /* Prevent line wraps before the checkbox bubble */
}
.alectryon-io label.alectryon-input:after {
margin-left: 0.25em;
margin-right: -1em; /* Compensate for the anti-wrapping space */
}
.alectryon-failed {
/* Underlines are broken in Chrome (they reset at each element boundary)… */
/* text-decoration: red wavy underline; */
/* … but it isn't too noticeable with dots */
text-decoration: red dotted underline;
text-decoration-skip-ink: none;
/* Chrome prints background images in low resolution, yielding a blurry underline */
/* background: bottom / 0.3em auto repeat-x url(data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAyLjY0NiAxLjg1MiIgaGVpZ2h0PSI4IiB3aWR0aD0iMTAiPjxwYXRoIGQ9Ik0wIC4yNjVjLjc5NCAwIC41MyAxLjMyMiAxLjMyMyAxLjMyMi43OTQgMCAuNTMtMS4zMjIgMS4zMjMtMS4zMjIiIGZpbGw9Im5vbmUiIHN0cm9rZT0icmVkIiBzdHJva2Utd2lkdGg9Ii41MjkiLz48L3N2Zz4=); */
}
/* Wrapping :hover rules in a media query ensures that tapping a Coq sentence
doesn't trigger its :hover state (otherwise, on mobile, tapping a sentence to
hide its output causes it to remain visible (its :hover state gets triggered.
We only do it for the default style though, since other styles don't put the
output over the main text, so showing too much is not an issue. */
@media (any-hover: hover) {
.alectryon-bubble:hover:before,
.alectryon-toggle-label:hover:before,
.alectryon-io label.alectryon-input:hover:after {
background: #eeeeec;
}
.alectryon-io label.alectryon-input:hover {
text-decoration: underline dotted #babdb6;
text-shadow: 0 0 1px rgb(46, 52, 54, 0.3); /* #2e3436 + opacity */
}
.alectryon-io .alectryon-sentence:hover .alectryon-output,
.alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper,
.alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper {
z-index: 2; /* Place hovered goals above .alectryon-sentence.alectryon-target ones */
}
}
.alectryon-toggle:checked + .alectryon-toggle-label:before,
.alectryon-io .alectryon-sentence > .alectryon-toggle:checked + label.alectryon-input:after,
.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal > label:before {
background-color: #babdb6;
border-color: #babdb6;
}
/* Disable clicks on sentences when the document-wide toggle is set. */
.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input {
cursor: unset;
pointer-events: none;
}
/* Hide individual checkboxes when the document-wide toggle is set. */
.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input:after {
display: none;
}
/* .alectryon-output is displayed by toggles, :hover, and .alectryon-target rules */
.alectryon-io .alectryon-output {
box-sizing: border-box;
display: none;
left: 0;
right: 0;
position: absolute;
padding: 0.25em 0;
overflow: visible; /* Let box-shadows overflow */
z-index: 1; /* Default to an index lower than that used by :hover */
}
.alectryon-io .alectryon-type-info-wrapper {
position: absolute;
display: inline-block;
width: 100%;
}
.alectryon-io .alectryon-type-info-wrapper.full-width {
left: 0;
min-width: 100%;
max-width: 100%;
}
.alectryon-io .alectryon-type-info .goal-separator {
height: unset;
margin-top: 0em;
}
.alectryon-io .alectryon-type-info-wrapper .alectryon-type-info {
box-sizing: border-box;
bottom: 100%;
position: absolute;
/*padding: 0.25em 0;*/
visibility: hidden;
overflow: visible; /* Let box-shadows overflow */
z-index: 1; /* Default to an index lower than that used by :hover */
white-space: pre-wrap !important;
}
.alectryon-io .alectryon-type-info-wrapper .alectryon-type-info .alectryon-goal.alectryon-docstring {
white-space: pre-wrap !important;
}
@media (any-hover: hover) { /* See note above about this @media query */
.alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) {
display: block;
}
.alectryon-io.output-hidden .alectryon-sentence:hover .alectryon-output:not(:hover) {
display: none !important;
}
.alectryon-io.type-info-hidden .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info,
.alectryon-io.type-info-hidden .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
/*visibility: hidden !important;*/
}
.alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info,
.alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
visibility: visible;
transition-delay: 0.5s;
}
}
.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output {
display: block;
}
/* Indicate active (hovered or targeted) goals with a shadow. */
.alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-messages,
.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .alectryon-messages,
.alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-goals,
.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .alectryon-goals,
.alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
box-shadow: 2px 2px 2px gray;
}
.alectryon-io .alectryon-extra-goals .alectryon-goal .goal-hyps {
display: none;
}
.alectryon-io .alectryon-extra-goals .alectryon-extra-goal-toggle:not(:checked) + .alectryon-goal label.goal-separator hr {
/* Dashes indicate that the hypotheses are hidden */
border-top-style: dashed;
}
/* Show just a small preview of the other goals; this is undone by the
"extra-goal" toggle and by :hover and .alectryon-target in windowed mode. */
.alectryon-io .alectryon-extra-goals .alectryon-goal .goal-conclusion {
max-height: 5.2em;
overflow-y: auto;
/* Combining overflow-y: auto with display: inline-block causes extra space
to be added below the box. vertical-align: middle gets rid of it. */
vertical-align: middle;
}
.alectryon-io .alectryon-goals,
.alectryon-io .alectryon-messages {
background: #f6f7f6;
/*border: thin solid #d3d7cf; /* Convenient when pre's background is already #EEE */
display: block;
padding: 0.25em;
}
.alectryon-message::before {
content: '';
float: right;
/* etc/svg/square-bubble-xl.svg */
background: url("data:image/svg+xml,%3Csvg width='14' height='14' viewBox='0 0 3.704 3.704' xmlns='http://www.w3.org/2000/svg'%3E%3Cg fill-rule='evenodd' stroke='%23000' stroke-width='.264'%3E%3Cpath d='M.794.934h2.115M.794 1.463h1.455M.794 1.992h1.852'/%3E%3C/g%3E%3Cpath d='M.132.14v2.646h.794v.661l.926-.661h1.72V.14z' fill='none' stroke='%23000' stroke-width='.265'/%3E%3C/svg%3E") top right no-repeat;
height: 14px;
width: 14px;
}
.alectryon-toggle:checked + label + .alectryon-container {
width: unset;
}
/* Show goals when a toggle is set */
.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input + .alectryon-output,
.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output {
display: block;
position: static;
width: unset;
background: unset; /* Override the backgrounds set in floating in windowed mode */
padding: 0.25em 0; /* Re-assert so that later :hover rules don't override this padding */
}
.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input + .alectryon-output .goal-hyps,
.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output .goal-hyps {
/* Overridden back in windowed style */
flex-flow: row wrap;
justify-content: flex-start;
}
.alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence .alectryon-output > div,
.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output > div {
display: block;
}
.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-hyps {
display: flex;
}
.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-conclusion {
max-height: unset;
overflow-y: unset;
}
.alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence > .alectryon-toggle ~ .alectryon-wsp,
.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-wsp {
display: none;
}
.alectryon-io .alectryon-messages,
.alectryon-io .alectryon-message,
.alectryon-io .alectryon-goals,
.alectryon-io .alectryon-goal,
.alectryon-io .goal-hyps > span,
.alectryon-io .goal-conclusion {
border-radius: 0.15em;
}
.alectryon-io .alectryon-goal,
.alectryon-io .alectryon-message {
align-items: center;
background: #f6f7f6;
border: 0em;
display: block;
flex-direction: column;
margin: 0.25em;
padding: 0.5em;
position: relative;
}
.alectryon-io .goal-hyps {
align-content: space-around;
align-items: baseline;
display: flex;
flex-flow: column nowrap; /* re-stated in windowed mode */
justify-content: space-around;
/* LATER use a gap property instead of margins once supported */
margin: -0.15em -0.25em; /* -0.15em to cancel the item spacing */
padding-bottom: 0.35em; /* 0.5em-0.15em to cancel the 0.5em of .goal-separator */
}
.alectryon-io .goal-hyps > br {
display: none; /* Only for RSS readers */
}
.alectryon-io .goal-hyps > span,
.alectryon-io .goal-conclusion {
/*background: #eeeeec;*/
display: inline-block;
padding: 0.15em 0.35em;
}
.alectryon-io .goal-hyps > span {
align-items: baseline;
display: inline-flex;
margin: 0.15em 0.25em;
}
.alectryon-block var,
.alectryon-inline var,
.alectryon-io .goal-hyps > span > var {
font-weight: 600;
font-style: unset;
}
.alectryon-io .goal-hyps > span > var {
/* Shrink the list of names, but let it grow as long as space is available. */
flex-basis: min-content;
flex-grow: 1;
}
.alectryon-io .goal-hyps > span b {
font-weight: 600;
margin: 0 0 0 0.5em;
white-space: pre;
}
.alectryon-io .hyp-body,
.alectryon-io .hyp-type {
display: flex;
align-items: baseline;
}
.alectryon-io .goal-separator {
align-items: center;
display: flex;
flex-direction: row;
height: 1em; /* Fixed height to ignore goal name and markers */
margin-top: -0.5em; /* Compensated in .goal-hyps when shown */
}
.alectryon-io .goal-separator hr {
border: none;
border-top: thin solid #555753;
display: block;
flex-grow: 1;
margin: 0;
}
.alectryon-io .goal-separator .goal-name {
font-size: 0.75em;
margin-left: 0.5em;
}
/**********/
/* Banner */
/**********/
.alectryon-banner {
background: #eeeeec;
border: 1px solid #babcbd;
font-size: 0.75em;
padding: 0.25em;
text-align: center;
margin: 1em 0;
}
.alectryon-banner a {
cursor: pointer;
text-decoration: underline;
}
.alectryon-banner kbd {
background: #d3d7cf;
border-radius: 0.15em;
border: 1px solid #babdb6;
box-sizing: border-box;
display: inline-block;
font-family: inherit;
font-size: 0.9em;
height: 1.3em;
line-height: 1.2em;
margin: -0.25em 0;
padding: 0 0.25em;
vertical-align: middle;
}
/**********/
/* Toggle */
/**********/
.alectryon-toggle-label {
margin: 1rem 0;
}
/******************/
/* Floating style */
/******************/
/* If there's space, display goals to the right of the code, not below it. */
@media (min-width: 80rem) {
/* Unlike the windowed case, we don't want to move output blocks to the side
when they are both :checked and -targeted, since it gets confusing as
things jump around; hence the commented-output part of the selector,
which would otherwise increase specificity */
.alectryon-floating .alectryon-sentence.alectryon-target /* > .alectryon-toggle ~ */ .alectryon-output,
.alectryon-floating .alectryon-sentence:hover .alectryon-output {
top: 0;
left: 100%;
right: -100%;
padding: 0 0.5em;
position: absolute;
}
.alectryon-floating .alectryon-output {
min-height: 100%;
}
.alectryon-floating .alectryon-sentence:hover .alectryon-output {
background: white; /* Ensure that short goals hide long ones */
}
/* This odd margin-bottom property prevents the sticky div from bumping
against the bottom of its container (.alectryon-output). The alternative
would be enlarging .alectryon-output, but that would cause overflows,
enlarging scrollbars and yielding scrolling towards the bottom of the
page. Doing things this way instead makes it possible to restrict
.alectryon-output to a reasonable size (100%, through top = bottom = 0).
See also https://stackoverflow.com/questions/43909940/. */
/* See note on specificity above */
.alectryon-floating .alectryon-sentence.alectryon-target /* > .alectryon-toggle ~ */ .alectryon-output > div,
.alectryon-floating .alectryon-sentence:hover .alectryon-output > div {
margin-bottom: -200%;
position: sticky;
top: 0;
}
.alectryon-floating .alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence .alectryon-output > div,
.alectryon-floating .alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output > div {
margin-bottom: unset; /* Undo the margin */
}
/* Float underneath the current fragment
@media (max-width: 80rem) {
.alectryon-floating .alectryon-output {
top: 100%;
}
} */
}
/********************/
/* Multi-pane style */
/********************/
.alectryon-windowed {
border: 0 solid #2e3436;
box-sizing: border-box;
}
.alectryon-windowed .alectryon-sentence:hover .alectryon-output {
background: white; /* Ensure that short goals hide long ones */
}
.alectryon-windowed .alectryon-output {
position: fixed; /* Overwritten by the :checked rules */
}
/* See note about specificity below */
.alectryon-windowed .alectryon-sentence:hover .alectryon-output,
.alectryon-windowed .alectryon-sentence.alectryon-target > .alectryon-toggle ~ .alectryon-output {
padding: 0.5em;
overflow-y: auto; /* Windowed contents may need to scroll */
}
.alectryon-windowed .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-messages,
.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .alectryon-messages,
.alectryon-windowed .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-goals,
.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .alectryon-goals {
box-shadow: none; /* A shadow is unnecessary here and incompatible with overflow-y set to auto */
}
.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .goal-hyps {
/* Restated to override the :checked style */
flex-flow: column nowrap;
justify-content: space-around;
}
.alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-extra-goals .alectryon-goal .goal-conclusion
/* Like .alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-conclusion */ {
max-height: unset;
overflow-y: unset;
}
.alectryon-windowed .alectryon-output > div {
display: flex; /* Put messages after goals */
flex-direction: column-reverse;
}
/*********************/
/* Standalone styles */
/*********************/
.alectryon-standalone {
font-family: 'IBM Plex Serif', 'PT Serif', 'Merriweather', 'DejaVu Serif', serif;
line-height: 1.5;
}
@media screen and (min-width: 50rem) {
html.alectryon-standalone {
/* Prevent flickering when hovering a block causes scrollbars to appear. */
margin-left: calc(100vw - 100%);
margin-right: 0;
}
}
/* Coqdoc */
.alectryon-coqdoc .doc .code,
.alectryon-coqdoc .doc .inlinecode,
.alectryon-coqdoc .doc .comment {
display: inline;
}
.alectryon-coqdoc .doc .comment {
color: #eeeeec;
}
.alectryon-coqdoc .doc .paragraph {
height: 0.75em;
}
/* Centered, Floating */
.alectryon-standalone .alectryon-centered,
.alectryon-standalone .alectryon-floating {
max-width: 50rem;
margin: auto;
}
@media (min-width: 80rem) {
.alectryon-standalone .alectryon-floating {
max-width: 80rem;
}
.alectryon-standalone .alectryon-floating > * {
width: 50%;
margin-left: 0;
}
}
/* Windowed */
.alectryon-standalone .alectryon-windowed {
display: block;
margin: 0;
overflow-y: auto;
position: absolute;
padding: 0 1em;
}
.alectryon-standalone .alectryon-windowed > * {
/* Override properties of docutils_basic.css */
margin-left: 0;
max-width: unset;
}
.alectryon-standalone .alectryon-windowed .alectryon-io {
box-sizing: border-box;
width: 100%;
}
/* No need to predicate the :hover rules below on :not(:checked), since left,
right, top, and bottom will be inactived by the :checked rules setting
position to static */
/* Specificity: We want the output to stay inline when hovered while unfolded
(:checked), but we want it to move when it's targeted (i.e. when the user
is browsing goals one by one using the keyboard, in which case we want to
goals to appear in consistent locations). The selectors below ensure
that :hover < :checked < -targeted in terms of specificity. */
/* LATER: Reimplement this stuff with CSS variables */
.alectryon-windowed .alectryon-sentence.alectryon-target > .alectryon-toggle ~ .alectryon-output {
position: fixed;
}
@media screen and (min-width: 60rem) {
.alectryon-standalone .alectryon-windowed {
border-right-width: thin;
bottom: 0;
left: 0;
right: 50%;
top: 0;
}
.alectryon-standalone .alectryon-windowed .alectryon-sentence:hover .alectryon-output,
.alectryon-standalone .alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-output {
bottom: 0;
left: 50%;
right: 0;
top: 0;
}
}
@media screen and (max-width: 60rem) {
.alectryon-standalone .alectryon-windowed {
border-bottom-width: 1px;
bottom: 40%;
left: 0;
right: 0;
top: 0;
}
.alectryon-standalone .alectryon-windowed .alectryon-sentence:hover .alectryon-output,
.alectryon-standalone .alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-output {
bottom: 0;
left: 0;
right: 0;
top: 60%;
}
}

View File

@ -0,0 +1,172 @@
var Alectryon;
(function(Alectryon) {
(function (slideshow) {
function anchor(sentence) { return "#" + sentence.id; }
function current_sentence() { return slideshow.sentences[slideshow.pos]; }
function unhighlight() {
var sentence = current_sentence();
if (sentence) sentence.classList.remove("alectryon-target");
slideshow.pos = -1;
}
function highlight(sentence) {
sentence.classList.add("alectryon-target");
}
function scroll(sentence) {
// Put the top of the current fragment close to the top of the
// screen, but scroll it out of view if showing it requires pushing
// the sentence past half of the screen. If sentence is already in
// a reasonable position, don't move.
var parent = sentence.parentElement;
/* We want to scroll the whole document, so start at root… */
while (parent && !parent.classList.contains("alectryon-root"))
parent = parent.parentElement;
/* and work up from there to find a scrollable element.
parent.scrollHeight can be greater than parent.clientHeight
without showing scrollbars, so we add a 10px buffer. */
while (parent && parent.scrollHeight <= parent.clientHeight + 10)
parent = parent.parentElement;
/* <body> and <html> elements can have their client rect overflow
* the window if their height is unset, so scroll the window
* instead */
if (parent && (parent.nodeName == "BODY" || parent.nodeName == "HTML"))
parent = null;
var rect = function(e) { return e.getBoundingClientRect(); };
var parent_box = parent ? rect(parent) : { y: 0, height: window.innerHeight },
sentence_y = rect(sentence).y - parent_box.y,
fragment_y = rect(sentence.parentElement).y - parent_box.y;
// The assertion below sometimes fails for the first element in a block.
// console.assert(sentence_y >= fragment_y);
if (sentence_y < 0.1 * parent_box.height ||
sentence_y > 0.7 * parent_box.height) {
(parent || window).scrollBy(
0, Math.max(sentence_y - 0.5 * parent_box.height,
fragment_y - 0.1 * parent_box.height));
}
}
function highlighted(pos) {
return slideshow.pos == pos;
}
function navigate(pos, inhibitScroll) {
unhighlight();
slideshow.pos = Math.min(Math.max(pos, 0), slideshow.sentences.length - 1);
var sentence = current_sentence();
highlight(sentence);
if (!inhibitScroll)
scroll(sentence);
}
var keys = {
PAGE_UP: 33,
PAGE_DOWN: 34,
ARROW_UP: 38,
ARROW_DOWN: 40,
h: 72, l: 76, p: 80, n: 78
};
function onkeydown(e) {
e = e || window.event;
if (e.ctrlKey || e.metaKey) {
if (e.keyCode == keys.ARROW_UP)
slideshow.previous();
else if (e.keyCode == keys.ARROW_DOWN)
slideshow.next();
else
return;
} else {
// if (e.keyCode == keys.PAGE_UP || e.keyCode == keys.p || e.keyCode == keys.h)
// slideshow.previous();
// else if (e.keyCode == keys.PAGE_DOWN || e.keyCode == keys.n || e.keyCode == keys.l)
// slideshow.next();
// else
return;
}
e.preventDefault();
}
function start() {
slideshow.navigate(0);
}
function toggleHighlight(idx) {
if (highlighted(idx))
unhighlight();
else
navigate(idx, true);
}
function handleClick(evt) {
if (evt.ctrlKey || evt.metaKey) {
var sentence = evt.currentTarget;
// Ensure that the goal is shown on the side, not inline
var checkbox = sentence.getElementsByClassName("alectryon-toggle")[0];
if (checkbox)
checkbox.checked = false;
toggleHighlight(sentence.alectryon_index);
evt.preventDefault();
}
}
function init() {
document.onkeydown = onkeydown;
slideshow.pos = -1;
slideshow.sentences = Array.from(document.getElementsByClassName("alectryon-sentence"));
slideshow.sentences.forEach(function (s, idx) {
s.addEventListener('click', handleClick, false);
s.alectryon_index = idx;
});
}
slideshow.start = start;
slideshow.end = unhighlight;
slideshow.navigate = navigate;
slideshow.next = function() { navigate(slideshow.pos + 1); };
slideshow.previous = function() { navigate(slideshow.pos + -1); };
window.addEventListener('DOMContentLoaded', init);
})(Alectryon.slideshow || (Alectryon.slideshow = {}));
(function (styles) {
var styleNames = ["centered", "floating", "windowed"];
function className(style) {
return "alectryon-" + style;
}
function setStyle(style) {
var root = document.getElementsByClassName("alectryon-root")[0];
styleNames.forEach(function (s) {
root.classList.remove(className(s)); });
root.classList.add(className(style));
}
function init() {
var banner = document.getElementsByClassName("alectryon-banner")[0];
if (banner) {
banner.append(" Style: ");
styleNames.forEach(function (styleName, idx) {
var s = styleName;
var a = document.createElement("a");
a.onclick = function() { setStyle(s); };
a.append(styleName);
if (idx > 0) banner.append("; ");
banner.appendChild(a);
});
banner.append(".");
}
}
window.addEventListener('DOMContentLoaded', init);
styles.setStyle = setStyle;
})(Alectryon.styles || (Alectryon.styles = {}));
})(Alectryon || (Alectryon = {}));

View File

@ -0,0 +1,593 @@
/******************************************************************************
The MIT License (MIT)
Copyright (c) 2014 Matthias Eisen
Further changes Copyright (c) 2020, 2021 Clément Pit-Claudel
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.
******************************************************************************/
kbd,
pre,
samp,
tt,
body code, /* Increase specificity to override IBM's stylesheet */
body code.highlight,
.docutils.literal {
font-family: 'Iosevka Slab Web', 'Iosevka Web', 'Iosevka Slab', 'Iosevka', 'Fira Code', monospace;
font-feature-settings: "COQX" 1 /* Coq ligatures */, "XV00" 1 /* Legacy */, "calt" 1 /* Fallback */;
}
body {
color: #111;
font-family: 'IBM Plex Serif', 'PT Serif', 'Merriweather', 'DejaVu Serif', serif;
line-height: 1.5;
}
main, div.document {
margin: 0 auto;
max-width: 720px;
}
/* ========== Headings ========== */
h1, h2, h3, h4, h5, h6 {
font-weight: normal;
margin-top: 1.5em;
}
h1.section-subtitle,
h2.section-subtitle,
h3.section-subtitle,
h4.section-subtitle,
h5.section-subtitle,
h6.section-subtitle {
margin-top: 0.4em;
}
h1.title {
text-align: center;
}
h2.subtitle {
text-align: center;
}
span.section-subtitle {
font-size: 80%,
}
/* //-------- Headings ---------- */
/* ========== Images ========== */
img,
.figure,
object {
display: block;
margin-left: auto;
margin-right: auto;
}
div.figure {
margin-left: 2em;
margin-right: 2em;
}
img.align-left, .figure.align-left, object.align-left {
clear: left;
float: left;
margin-right: 1em;
}
img.align-right, .figure.align-right, object.align-right {
clear: right;
float: right;
margin-left: 1em;
}
img.align-center, .figure.align-center, object.align-center {
display: block;
margin-left: auto;
margin-right: auto;
}
/* reset inner alignment in figures */
div.align-right {
text-align: inherit;
}
object[type="image/svg+xml"],
object[type="application/x-shockwave-flash"] {
overflow: hidden;
}
/* //-------- Images ---------- */
/* ========== Literal Blocks ========== */
.docutils.literal {
background-color: #eee;
padding: 0 0.2em;
border-radius: 0.1em;
}
pre.address {
margin-bottom: 0;
margin-top: 0;
font: inherit;
}
pre.literal-block {
border-left: solid 5px #ccc;
padding: 1em;
}
pre.literal-block, pre.doctest-block, pre.math, pre.code {
}
span.interpreted {
}
span.pre {
white-space: pre;
}
pre.code .ln {
color: grey;
}
pre.code, code {
border-style: none;
/* ! padding: 1em 0; */ /* Removed because that large hitbox bleeds over links on other lines */
}
pre.code .comment, code .comment {
color: #888;
}
pre.code .keyword, code .keyword {
font-weight: bold;
color: #080;
}
pre.code .literal.string, code .literal.string {
color: #d20;
background-color: #fff0f0;
}
pre.code .literal.number, code .literal.number {
color: #00d;
}
pre.code .name.builtin, code .name.builtin {
color: #038;
color: #820;
}
pre.code .name.namespace, code .name.namespace {
color: #b06;
}
pre.code .deleted, code .deleted {
background-color: #fdd;
}
pre.code .inserted, code .inserted {
background-color: #dfd;
}
/* //-------- Literal Blocks --------- */
/* ========== Tables ========== */
table {
border-spacing: 0;
border-collapse: collapse;
border-style: none;
border-top: solid thin #111;
border-bottom: solid thin #111;
}
td,
th {
border: none;
padding: 0.5em;
vertical-align: top;
}
th {
border-top: solid thin #111;
border-bottom: solid thin #111;
background-color: #ddd;
}
table.field-list,
table.footnote,
table.citation,
table.option-list {
border: none;
}
table.docinfo {
margin: 2em 4em;
}
table.docutils {
margin: 1em 0;
}
table.docutils th.field-name,
table.docinfo th.docinfo-name {
border: none;
background: none;
font-weight: bold ;
text-align: left ;
white-space: nowrap ;
padding-left: 0;
vertical-align: middle;
}
table.docutils.booktabs {
border: none;
border-top: medium solid;
border-bottom: medium solid;
border-collapse: collapse;
}
table.docutils.booktabs * {
border: none;
}
table.docutils.booktabs th {
border-bottom: thin solid;
text-align: left;
}
span.option {
white-space: nowrap;
}
table caption {
margin-bottom: 2px;
}
/* //-------- Tables ---------- */
/* ========== Lists ========== */
ol.simple, ul.simple {
margin-bottom: 1em;
}
ol.arabic {
list-style: decimal;
}
ol.loweralpha {
list-style: lower-alpha;
}
ol.upperalpha {
list-style: upper-alpha;
}
ol.lowerroman {
list-style: lower-roman;
}
ol.upperroman {
list-style: upper-roman;
}
dl.docutils dd {
margin-bottom: 0.5em;
}
dl.docutils dt {
font-weight: bold;
}
/* //-------- Lists ---------- */
/* ========== Sidebar ========== */
div.sidebar {
margin: 0 0 0.5em 1em ;
border-left: solid medium #111;
padding: 1em ;
width: 40% ;
float: right ;
clear: right;
}
div.sidebar {
font-size: 0.9rem;
}
p.sidebar-title {
font-size: 1rem;
font-weight: bold ;
}
p.sidebar-subtitle {
font-weight: bold;
}
/* //-------- Sidebar ---------- */
/* ========== Topic ========== */
div.topic {
border-left: thin solid #111;
padding-left: 1em;
}
div.topic p {
padding: 0;
}
p.topic-title {
font-weight: bold;
}
/* //-------- Topic ---------- */
/* ========== Header ========== */
div.header {
font-family: "Century Gothic", CenturyGothic, Geneva, AppleGothic, sans-serif;
font-size: 0.9rem;
margin: 2em auto 4em auto;
max-width: 960px;
clear: both;
}
hr.header {
border: 0;
height: 1px;
margin-top: 1em;
background-color: #111;
}
/* //-------- Header ---------- */
/* ========== Footer ========== */
div.footer {
font-family: "Century Gothic", CenturyGothic, Geneva, AppleGothic, sans-serif;
font-size: 0.9rem;
margin: 6em auto 2em auto;
max-width: 960px;
clear: both;
text-align: center;
}
hr.footer {
border: 0;
height: 1px;
margin-bottom: 2em;
background-color: #111;
}
/* //-------- Footer ---------- */
/* ========== Admonitions ========== */
div.admonition,
div.attention,
div.caution,
div.danger,
div.error,
div.hint,
div.important,
div.note,
div.tip,
div.warning {
border: solid thin #111;
padding: 0 1em;
}
div.error,
div.danger {
border-color: #a94442;
background-color: #f2dede;
}
div.hint,
div.tip {
border-color: #31708f;
background-color: #d9edf7;
}
div.attention,
div.caution,
div.warning {
border-color: #8a6d3b;
background-color: #fcf8e3;
}
div.hint p.admonition-title,
div.tip p.admonition-title {
color: #31708f;
font-weight: bold ;
}
div.note p.admonition-title,
div.admonition p.admonition-title,
div.important p.admonition-title {
font-weight: bold ;
}
div.attention p.admonition-title,
div.caution p.admonition-title,
div.warning p.admonition-title {
color: #8a6d3b;
font-weight: bold ;
}
div.danger p.admonition-title,
div.error p.admonition-title,
.code .error {
color: #a94442;
font-weight: bold ;
}
/* //-------- Admonitions ---------- */
/* ========== Table of Contents ========== */
div.contents {
margin: 2em 0;
border: none;
}
ul.auto-toc {
list-style-type: none;
}
a.toc-backref {
text-decoration: none ;
color: #111;
}
/* //-------- Table of Contents ---------- */
/* ========== Line Blocks========== */
div.line-block {
display: block ;
margin-top: 1em ;
margin-bottom: 1em;
}
div.line-block div.line-block {
margin-top: 0 ;
margin-bottom: 0 ;
margin-left: 1.5em;
}
/* //-------- Line Blocks---------- */
/* ========== System Messages ========== */
div.system-messages {
margin: 5em;
}
div.system-messages h1 {
color: red;
}
div.system-message {
border: medium outset ;
padding: 1em;
}
div.system-message p.system-message-title {
color: red ;
font-weight: bold;
}
/* //-------- System Messages---------- */
/* ========== Helpers ========== */
.hidden {
display: none;
}
.align-left {
text-align: left;
}
.align-center {
clear: both ;
text-align: center;
}
.align-right {
text-align: right;
}
/* //-------- Helpers---------- */
p.caption {
font-style: italic;
text-align: center;
}
p.credits {
font-style: italic ;
font-size: smaller }
p.label {
white-space: nowrap }
p.rubric {
font-weight: bold ;
font-size: larger ;
color: maroon ;
text-align: center }
p.attribution {
text-align: right ;
margin-left: 50% }
blockquote.epigraph {
margin: 2em 5em;
}
div.abstract {
margin: 2em 5em }
div.abstract {
font-weight: bold ;
text-align: center }
div.dedication {
margin: 2em 5em ;
text-align: center ;
font-style: italic }
div.dedication {
font-weight: bold ;
font-style: normal }
span.classifier {
font-style: oblique }
span.classifier-delimiter {
font-weight: bold }
span.problematic {
color: red }

View File

@ -0,0 +1,82 @@
/* Pygments stylesheet generated by Alectryon (style=None) */
/* Most of the following are unused as of now */
td.linenos .normal { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }
span.linenos { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }
td.linenos .special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }
span.linenos.special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }
.highlight .hll, .code .hll { background-color: #ffffcc }
.highlight .c, .code .c { color: #555753; font-style: italic } /* Comment */
.highlight .err, .code .err { color: #a40000; border: 1px solid #cc0000 } /* Error */
.highlight .g, .code .g { color: #000000 } /* Generic */
.highlight .k, .code .k { color: #8f5902 } /* Keyword */
.highlight .l, .code .l { color: #2e3436 } /* Literal */
.highlight .n, .code .n { color: #000000 } /* Name */
.highlight .o, .code .o { color: #000000 } /* Operator */
.highlight .x, .code .x { color: #2e3436 } /* Other */
.highlight .p, .code .p { color: #000000 } /* Punctuation */
.highlight .ch, .code .ch { color: #555753; font-weight: bold; font-style: italic } /* Comment.Hashbang */
.highlight .cm, .code .cm { color: #555753; font-style: italic } /* Comment.Multiline */
.highlight .cp, .code .cp { color: #3465a4; font-style: italic } /* Comment.Preproc */
.highlight .cpf, .code .cpf { color: #555753; font-style: italic } /* Comment.PreprocFile */
.highlight .c1, .code .c1 { color: #555753; font-style: italic } /* Comment.Single */
.highlight .cs, .code .cs { color: #3465a4; font-weight: bold; font-style: italic } /* Comment.Special */
.highlight .gd, .code .gd { color: #a40000 } /* Generic.Deleted */
.highlight .ge, .code .ge { color: #000000; font-style: italic } /* Generic.Emph */
.highlight .gr, .code .gr { color: #a40000 } /* Generic.Error */
.highlight .gh, .code .gh { color: #a40000; font-weight: bold } /* Generic.Heading */
.highlight .gi, .code .gi { color: #4e9a06 } /* Generic.Inserted */
.highlight .go, .code .go { color: #000000; font-style: italic } /* Generic.Output */
.highlight .gp, .code .gp { color: #8f5902 } /* Generic.Prompt */
.highlight .gs, .code .gs { color: #000000; font-weight: bold } /* Generic.Strong */
.highlight .gu, .code .gu { color: #000000; font-weight: bold } /* Generic.Subheading */
.highlight .gt, .code .gt { color: #000000; font-style: italic } /* Generic.Traceback */
.highlight .kc, .code .kc { color: #204a87; font-weight: bold } /* Keyword.Constant */
.highlight .kd, .code .kd { color: #4e9a06; font-weight: bold } /* Keyword.Declaration */
.highlight .kn, .code .kn { color: #4e9a06; font-weight: bold } /* Keyword.Namespace */
.highlight .kp, .code .kp { color: #204a87 } /* Keyword.Pseudo */
.highlight .kr, .code .kr { color: #8f5902 } /* Keyword.Reserved */
.highlight .kt, .code .kt { color: #204a87 } /* Keyword.Type */
.highlight .ld, .code .ld { color: #2e3436 } /* Literal.Date */
.highlight .m, .code .m { color: #2e3436 } /* Literal.Number */
.highlight .s, .code .s { color: #ad7fa8 } /* Literal.String */
.highlight .na, .code .na { color: #c4a000 } /* Name.Attribute */
.highlight .nb, .code .nb { color: #75507b } /* Name.Builtin */
.highlight .nc, .code .nc { color: #204a87 } /* Name.Class */
.highlight .no, .code .no { color: #ce5c00 } /* Name.Constant */
.highlight .nd, .code .nd { color: #3465a4; font-weight: bold } /* Name.Decorator */
.highlight .ni, .code .ni { color: #c4a000; text-decoration: underline } /* Name.Entity */
.highlight .ne, .code .ne { color: #cc0000 } /* Name.Exception */
.highlight .nf, .code .nf { color: #a40000 } /* Name.Function */
.highlight .nl, .code .nl { color: #3465a4; font-weight: bold } /* Name.Label */
.highlight .nn, .code .nn { color: #000000 } /* Name.Namespace */
.highlight .nx, .code .nx { color: #000000 } /* Name.Other */
.highlight .py, .code .py { color: #000000 } /* Name.Property */
.highlight .nt, .code .nt { color: #a40000 } /* Name.Tag */
.highlight .nv, .code .nv { color: #ce5c00 } /* Name.Variable */
.highlight .ow, .code .ow { color: #8f5902 } /* Operator.Word */
.highlight .w, .code .w { color: #d3d7cf; text-decoration: underline } /* Text.Whitespace */
.highlight .mb, .code .mb { color: #2e3436 } /* Literal.Number.Bin */
.highlight .mf, .code .mf { color: #2e3436 } /* Literal.Number.Float */
.highlight .mh, .code .mh { color: #2e3436 } /* Literal.Number.Hex */
.highlight .mi, .code .mi { color: #2e3436 } /* Literal.Number.Integer */
.highlight .mo, .code .mo { color: #2e3436 } /* Literal.Number.Oct */
.highlight .sa, .code .sa { color: #ad7fa8 } /* Literal.String.Affix */
.highlight .sb, .code .sb { color: #ad7fa8 } /* Literal.String.Backtick */
.highlight .sc, .code .sc { color: #ad7fa8; font-weight: bold } /* Literal.String.Char */
.highlight .dl, .code .dl { color: #ad7fa8 } /* Literal.String.Delimiter */
.highlight .sd, .code .sd { color: #ad7fa8 } /* Literal.String.Doc */
.highlight .s2, .code .s2 { color: #ad7fa8 } /* Literal.String.Double */
.highlight .se, .code .se { color: #ad7fa8; font-weight: bold } /* Literal.String.Escape */
.highlight .sh, .code .sh { color: #ad7fa8; text-decoration: underline } /* Literal.String.Heredoc */
.highlight .si, .code .si { color: #ce5c00 } /* Literal.String.Interpol */
.highlight .sx, .code .sx { color: #ad7fa8 } /* Literal.String.Other */
.highlight .sr, .code .sr { color: #ad7fa8 } /* Literal.String.Regex */
.highlight .s1, .code .s1 { color: #ad7fa8 } /* Literal.String.Single */
.highlight .ss, .code .ss { color: #8f5902 } /* Literal.String.Symbol */
.highlight .bp, .code .bp { color: #5c35cc } /* Name.Builtin.Pseudo */
.highlight .fm, .code .fm { color: #a40000 } /* Name.Function.Magic */
.highlight .vc, .code .vc { color: #ce5c00 } /* Name.Variable.Class */
.highlight .vg, .code .vg { color: #ce5c00; text-decoration: underline } /* Name.Variable.Global */
.highlight .vi, .code .vi { color: #ce5c00 } /* Name.Variable.Instance */
.highlight .vm, .code .vm { color: #ce5c00 } /* Name.Variable.Magic */
.highlight .il, .code .il { color: #2e3436 } /* Literal.Number.Integer.Long */

33
static/color-scheme.js Normal file
View File

@ -0,0 +1,33 @@
function getTheme() {
return localStorage.getItem("theme") || "system";
}
function setTheme(themeName) {
localStorage.setItem('theme', themeName);
if (themeName == "system") {
themeName = parent.matchMedia("(prefers-color-scheme: dark)").matches ? "dark" : "light";
}
// the navbar is in an iframe, so we need to set this variable in the parent document
for (const win of [window, parent]) {
win.document.documentElement.setAttribute('data-theme', themeName);
}
}
setTheme(getTheme())
document.addEventListener("DOMContentLoaded", function() {
document.querySelectorAll("#color-theme-switcher input").forEach((input) => {
if (input.value == getTheme()) {
input.checked = true;
}
input.addEventListener('change', e => setTheme(e.target.value));
});
// also check to see if the user changes their theme settings while the page is loaded.
parent.matchMedia('(prefers-color-scheme: dark)').addEventListener('change', event => {
setTheme(getTheme());
})
});
// un-hide the colorscheme picker
document.querySelector("#settings").removeAttribute('hidden');

272
static/declaration-data.js Normal file
View File

@ -0,0 +1,272 @@
/**
* This module is a wrapper that facilitates manipulating the declaration data.
*
* Please see {@link DeclarationDataCenter} for more information.
*/
const CACHE_DB_NAME = "declaration-data";
const CACHE_DB_VERSION = 1;
const CACHE_DB_KEY = "DECLARATIONS_KEY";
/**
* The DeclarationDataCenter is used for declaration searching.
*
* For usage, see the {@link init} and {@link search} methods.
*/
export class DeclarationDataCenter {
/**
* The declaration data. Users should not interact directly with this field.
*
* *NOTE:* This is not made private to support legacy browsers.
*/
declarationData = null;
/**
* Used to implement the singleton, in case we need to fetch data mutiple times in the same page.
*/
static requestSingleton = null;
/**
* Construct a DeclarationDataCenter with given data.
*
* Please use {@link DeclarationDataCenter.init} instead, which automates the data fetching process.
* @param {*} declarationData
*/
constructor(declarationData) {
this.declarationData = declarationData;
}
/**
* The actual constructor of DeclarationDataCenter
* @returns {Promise<DeclarationDataCenter>}
*/
static async init() {
if (DeclarationDataCenter.requestSingleton === null) {
DeclarationDataCenter.requestSingleton = DeclarationDataCenter.getData();
}
return await DeclarationDataCenter.requestSingleton;
}
static async getData() {
const dataListUrl = new URL(
`${SITE_ROOT}/declarations/declaration-data.bmp`,
window.location
);
// try to use cache first
// TODO: This API is not thought 100% through. If we have a DB cached
// already it will not even ask the remote for a new one so we end up
// with outdated declaration-data. This has to have some form of cache
// invalidation: https://github.com/leanprover/doc-gen4/issues/133
// const data = await fetchCachedDeclarationData().catch(_e => null);
const data = null;
if (data) {
// if data is defined, use the cached one.
return new DeclarationDataCenter(data);
} else {
// undefined. then fetch the data from the server.
const dataListRes = await fetch(dataListUrl);
const data = await dataListRes.json();
// TODO https://github.com/leanprover/doc-gen4/issues/133
// await cacheDeclarationData(data);
return new DeclarationDataCenter(data);
}
}
/**
* Search for a declaration.
* @returns {Array<any>}
*/
search(pattern, strict = true, allowedKinds = undefined, maxResults = undefined) {
if (!pattern) {
return [];
}
if (strict) {
let decl = this.declarationData.declarations[pattern];
return decl ? [decl] : [];
} else {
return getMatches(this.declarationData.declarations, pattern, allowedKinds, maxResults);
}
}
/**
* Search for all instances of a certain typeclass
* @returns {Array<String>}
*/
instancesForClass(className) {
const instances = this.declarationData.instances[className];
if (!instances) {
return [];
} else {
return instances;
}
}
/**
* Search for all instances that involve a certain type
* @returns {Array<String>}
*/
instancesForType(typeName) {
const instances = this.declarationData.instancesFor[typeName];
if (!instances) {
return [];
} else {
return instances;
}
}
/**
* Analogous to Lean declNameToLink
* @returns {String}
*/
declNameToLink(declName) {
return this.declarationData.declarations[declName].docLink;
}
/**
* Find all modules that imported the given one.
* @returns {Array<String>}
*/
moduleImportedBy(moduleName) {
return this.declarationData.importedBy[moduleName];
}
/**
* Analogous to Lean moduleNameToLink
* @returns {String}
*/
moduleNameToLink(moduleName) {
return this.declarationData.modules[moduleName];
}
}
function isSeparator(char) {
return char === "." || char === "_";
}
// HACK: the fuzzy matching is quite hacky
function matchCaseSensitive(declName, lowerDeclName, pattern) {
let i = 0,
j = 0,
err = 0,
lastMatch = 0;
while (i < declName.length && j < pattern.length) {
if (pattern[j] === declName[i] || pattern[j] === lowerDeclName[i]) {
err += (isSeparator(pattern[j]) ? 0.125 : 1) * (i - lastMatch);
if (pattern[j] !== declName[i]) err += 0.5;
lastMatch = i + 1;
j++;
} else if (isSeparator(declName[i])) {
err += 0.125 * (i + 1 - lastMatch);
lastMatch = i + 1;
}
i++;
}
err += 0.125 * (declName.length - lastMatch);
if (j === pattern.length) {
return err;
}
}
function getMatches(declarations, pattern, allowedKinds = undefined, maxResults = undefined) {
const lowerPats = pattern.toLowerCase().split(/\s/g);
const patNoSpaces = pattern.replace(/\s/g, "");
const results = [];
for (const [name, {
kind,
docLink,
}] of Object.entries(declarations)) {
// Apply "kind" filter
if (allowedKinds !== undefined) {
if (!allowedKinds.has(kind)) {
continue;
}
}
const lowerName = name.toLowerCase();
let err = matchCaseSensitive(name, lowerName, patNoSpaces);
if (err !== undefined) {
results.push({
name,
kind,
err,
lowerName,
docLink,
});
}
}
return results.sort(({ err: a }, { err: b }) => a - b).slice(0, maxResults);
}
// TODO: refactor the indexedDB part to be more robust
/**
* Get the indexedDB database, automatically initialized.
* @returns {Promise<IDBDatabase>}
*/
async function getDeclarationDatabase() {
return new Promise((resolve, reject) => {
const request = indexedDB.open(CACHE_DB_NAME, CACHE_DB_VERSION);
request.onerror = function (event) {
reject(
new Error(
`fail to open indexedDB ${CACHE_DB_NAME} of version ${CACHE_DB_VERSION}`
)
);
};
request.onupgradeneeded = function (event) {
let db = event.target.result;
// We only need to store one object, so no key path or increment is needed.
db.createObjectStore("declaration");
};
request.onsuccess = function (event) {
resolve(event.target.result);
};
});
}
/**
* Store data in indexedDB object store.
* @param {Map<string, any>} data
*/
async function cacheDeclarationData(data) {
let db = await getDeclarationDatabase();
let store = db
.transaction("declaration", "readwrite")
.objectStore("declaration");
return new Promise((resolve, reject) => {
let clearRequest = store.clear();
let addRequest = store.add(data, CACHE_DB_KEY);
addRequest.onsuccess = function (event) {
resolve();
};
addRequest.onerror = function (event) {
reject(new Error(`fail to store declaration data`));
};
clearRequest.onerror = function (event) {
reject(new Error("fail to clear object store"));
};
});
}
/**
* Retrieve data from indexedDB database.
* @returns {Promise<Map<string, any>|undefined>}
*/
async function fetchCachedDeclarationData() {
let db = await getDeclarationDatabase();
let store = db
.transaction("declaration", "readonly")
.objectStore("declaration");
return new Promise((resolve, reject) => {
let transactionRequest = store.get(CACHE_DB_KEY);
transactionRequest.onsuccess = function (event) {
resolve(event.target.result);
};
transactionRequest.onerror = function (event) {
reject(new Error(`fail to store declaration data`));
};
});
}

24
static/expand-nav.js Normal file
View File

@ -0,0 +1,24 @@
document.querySelector('.navframe').addEventListener('load', function() {
// Get the current page URL without the suffix after #
var currentPageURL = window.location.href.split('#')[0];
// Get all anchor tags
var as = document.querySelector('.navframe').contentWindow.document.body.querySelectorAll('a');
for (const a of as) {
if (a.href) {
var href = a.href.split('#')[0];
// find the one with the current url
if (href === currentPageURL) {
a.style.fontStyle = 'italic';
// open all detail tags above the current
var el = a.parentNode.closest('details');
while (el) {
el.open = true;
el = el.parentNode.closest('details');
}
}
// seeing as we found the link we were looking for, stop
break;
}
}
});

94
static/find/find.js Normal file
View File

@ -0,0 +1,94 @@
/**
* This module is used for the `/find` endpoint.
*
* Two basic kinds of search syntax are supported:
*
* 1. Query-Fragment syntax: `/find?pattern=Nat.add#doc` for documentation and `/find?pattern=Nat.add#src` for source code.
* 2. Fragment-Only syntax:`/find/#doc/Nat.add` for documentation and `/find/#src/Nat.add` for source code.
*
* Though both of them are valid, the first one is highly recommended, and the second one is for compatibility and taste.
*
* There are some extended usage for the QF syntax. For example, appending `strict=false` to the query part
* (`/find?pattern=Nat.add&strict=false#doc`) will allow you to use the fuzzy search, rather than strict match.
* Also, the fragment is extensible as well. For now only `#doc` and `#src` are implement, and the plain query without
* hash (`/find?pattern=Nat.add`) is used for computer-friendly data (semantic web is great! :P), while all other fragments
* fallback to the `#doc` view.
*/
import { DeclarationDataCenter } from "../declaration-data.js";
function leanFriendlyRegExp(c) {
try {
return new RegExp("(?<!«[^»]*)" + c);
} catch (e) {
if (e instanceof SyntaxError) {
// Lookbehind is not implemented yet in WebKit: https://bugs.webkit.org/show_bug.cgi?id=174931
// Fall back to less friendly regex.
return new RegExp(c);
}
throw e;
}
}
/**
* We don't use browser's default hash and searchParams in case Lean declaration name
* can be like `«#»`, rather we manually handle the `window.location.href` with regex.
*/
const LEAN_FRIENDLY_URL_REGEX = /^[^?#]+(?:\?((?:[^«#»]|«.*»)*))?(?:#(.*))?$/;
const LEAN_FRIENDLY_AND_SEPARATOR = leanFriendlyRegExp("&");
const LEAN_FRIENDLY_EQUAL_SEPARATOR = leanFriendlyRegExp("=");
const LEAN_FRIENDLY_SLASH_SEPARATOR = leanFriendlyRegExp("/");
const [_, query, fragment] = LEAN_FRIENDLY_URL_REGEX.exec(window.location.href);
const queryParams = new Map(
query
?.split(LEAN_FRIENDLY_AND_SEPARATOR)
?.map((p) => p.split(LEAN_FRIENDLY_EQUAL_SEPARATOR))
?.filter((l) => l.length == 2 && l[0].length > 0)
);
const fragmentPaths = fragment?.split(LEAN_FRIENDLY_SLASH_SEPARATOR) ?? [];
const encodedPattern = queryParams.get("pattern") ?? fragmentPaths[1]; // if first fail then second, may be undefined
const pattern = encodedPattern && decodeURIComponent(encodedPattern);
const strict = (queryParams.get("strict") ?? "true") === "true"; // default to true
const view = fragmentPaths[0];
findAndRedirect(pattern, strict, view);
/**
* Find the result and redirect to the result page.
* @param {string} pattern the pattern to search for
* @param {string} view the view of the find result (`"doc"` or `"src"` for now)
*/
async function findAndRedirect(pattern, strict, view) {
// if no pattern provided, directly redirect to the 404 page
if (!pattern) {
window.location.replace(`${SITE_ROOT}404.html`);
}
// search for result
try {
const dataCenter = await DeclarationDataCenter.init();
let result = (dataCenter.search(pattern, strict) ?? [])[0]; // in case return non array
// if no result found, redirect to the 404 page
if (!result) {
// TODO: better url semantic for 404, current implementation will lead to duplicate search for fuzzy match if not found.
window.location.replace(`${SITE_ROOT}404.html#${pattern ?? ""}`);
} else {
result.docLink = SITE_ROOT + result.docLink;
// success, redirect to doc or source page, or to the semantic rdf.
if (!view) {
window.location.replace(result.link);
} else if (view == "doc") {
window.location.replace(result.docLink);
} else if (view == "src") {
const [module, decl] = result.docLink.split("#", 2);
window.location.replace(`${module}?jump=src#${decl}`);
} else {
// fallback to doc page
window.location.replace(result.docLink);
}
}
} catch (e) {
document.write(`Cannot fetch data, please check your network connection.\n${e}`);
}
}

39
static/how-about.js Normal file
View File

@ -0,0 +1,39 @@
/**
* This module implements the `howabout` functionality in the 404 page.
*/
import { DeclarationDataCenter } from "./declaration-data.js";
const HOW_ABOUT = document.querySelector("#howabout");
// Show url of the missing page
if (HOW_ABOUT) {
HOW_ABOUT.parentNode
.insertBefore(document.createElement("pre"), HOW_ABOUT)
.appendChild(document.createElement("code")).innerText =
window.location.href.replace(/[/]/g, "/\u200b");
// TODO: add how about functionality for similar page as well.
const pattern = window.location.hash.replace("#", "");
// try to search for similar declarations
if (pattern) {
HOW_ABOUT.innerText = "Please wait a second. I'll try to help you.";
DeclarationDataCenter.init().then((dataCenter) => {
let results = dataCenter.search(pattern, false);
if (results.length > 0) {
HOW_ABOUT.innerText = "How about one of these instead:";
const ul = HOW_ABOUT.appendChild(document.createElement("ul"));
for (const { name, docLink } of results) {
const li = ul.appendChild(document.createElement("li"));
const a = li.appendChild(document.createElement("a"));
a.href = docLink;
a.appendChild(document.createElement("code")).innerText = name;
}
} else {
HOW_ABOUT.innerText =
"Sorry, I cannot find any similar declarations. Check the link or use the module navigation to find what you want :P";
}
});
}
}

19
static/importedBy.js Normal file
View File

@ -0,0 +1,19 @@
import { DeclarationDataCenter } from "./declaration-data.js";
fillImportedBy();
async function fillImportedBy() {
if (typeof(MODULE_NAME) == "undefined") {
return;
}
const dataCenter = await DeclarationDataCenter.init();
const moduleName = MODULE_NAME;
const importedByList = document.querySelector(".imported-by-list");
const importedBy = dataCenter.moduleImportedBy(moduleName);
var innerHTML = "";
for(var module of importedBy) {
const moduleLink = dataCenter.moduleNameToLink(module);
innerHTML += `<li><a href="${SITE_ROOT}${moduleLink}">${module}</a></li>`
}
importedByList.innerHTML = innerHTML;
}

36
static/instances.js Normal file
View File

@ -0,0 +1,36 @@
import { DeclarationDataCenter } from "./declaration-data.js";
annotateInstances();
annotateInstancesFor()
async function annotateInstances() {
const dataCenter = await DeclarationDataCenter.init();
const instanceForLists = [...(document.querySelectorAll(".instances-list"))];
for (const instanceForList of instanceForLists) {
const className = instanceForList.id.slice("instances-list-".length);
const instances = dataCenter.instancesForClass(className);
var innerHTML = "";
for(var instance of instances) {
const instanceLink = dataCenter.declNameToLink(instance);
innerHTML += `<li><a href="${SITE_ROOT}${instanceLink}">${instance}</a></li>`
}
instanceForList.innerHTML = innerHTML;
}
}
async function annotateInstancesFor() {
const dataCenter = await DeclarationDataCenter.init();
const instanceForLists = [...(document.querySelectorAll(".instances-for-list"))];
for (const instanceForList of instanceForLists) {
const typeName = instanceForList.id.slice("instances-for-list-".length);
const instances = dataCenter.instancesForType(typeName);
var innerHTML = "";
for(var instance of instances) {
const instanceLink = dataCenter.declNameToLink(instance);
innerHTML += `<li><a href="${SITE_ROOT}${instanceLink}">${instance}</a></li>`
}
instanceForList.innerHTML = innerHTML;
}
}

10
static/jump-src.js Normal file
View File

@ -0,0 +1,10 @@
document.addEventListener("DOMContentLoaded", () => {
const hash = document.location.hash.substring(1);
const tgt = new URLSearchParams(document.location.search).get("jump");
if (tgt === "src" && hash) {
const target = document.getElementById(hash)
?.querySelector(".gh_link a")
?.getAttribute("href");
if (target) window.location.replace(target);
}
})

41
static/mathjax-config.js Normal file
View File

@ -0,0 +1,41 @@
/*
* This file is for configing MathJax behavior.
* See https://docs.mathjax.org/en/latest/web/configuration.html
*
* This configuration is copied from old doc-gen3
* https://github.com/leanprover-community/doc-gen
*/
MathJax = {
tex: {
inlineMath: [["$", "$"]],
displayMath: [["$$", "$$"]],
},
options: {
skipHtmlTags: [
"script",
"noscript",
"style",
"textarea",
"pre",
"code",
"annotation",
"annotation-xml",
"decl",
"decl_meta",
"attributes",
"decl_args",
"decl_header",
"decl_name",
"decl_type",
"equation",
"equations",
"structure_field",
"structure_fields",
"constructor",
"constructors",
"instances",
],
ignoreHtmlClass: "tex2jax_ignore",
processHtmlClass: "tex2jax_process",
},
};

43
static/nav.js Normal file
View File

@ -0,0 +1,43 @@
/**
* This module is used to implement persistent navbar expansion.
*/
// The variable to store the expansion information.
let expanded = {};
// Load expansion information from sessionStorage.
for (const e of (sessionStorage.getItem("expanded") || "").split(",")) {
if (e !== "") {
expanded[e] = true;
}
}
/**
* Save expansion information to sessionStorage.
*/
function saveExpanded() {
sessionStorage.setItem(
"expanded",
Object.getOwnPropertyNames(expanded)
.filter((e) => expanded[e])
.join(",")
);
}
// save expansion information when user change the expansion.
for (const elem of document.getElementsByClassName("nav_sect")) {
const id = elem.getAttribute("data-path");
if (!id) continue;
if (expanded[id]) {
elem.open = true;
}
elem.addEventListener("toggle", () => {
expanded[id] = elem.open;
saveExpanded();
});
}
// Scroll to center.
for (const currentFileLink of document.getElementsByClassName("visible")) {
currentFileLink.scrollIntoView({ block: "center" });
}

164
static/search.js Normal file
View File

@ -0,0 +1,164 @@
/**
* This module is used to handle user's interaction with the search form.
*/
import { DeclarationDataCenter } from "./declaration-data.js";
// Search form and input in the upper right toolbar
const SEARCH_FORM = document.querySelector("#search_form");
const SEARCH_INPUT = SEARCH_FORM.querySelector("input[name=q]");
// Search form on the /search.html_page. These may be null.
const SEARCH_PAGE_INPUT = document.querySelector("#search_page_query")
const SEARCH_RESULTS = document.querySelector("#search_results")
// Max results to show for autocomplete or /search.html page.
const AC_MAX_RESULTS = 30
const SEARCH_PAGE_MAX_RESULTS = undefined
// Create an `div#autocomplete_results` to hold all autocomplete results.
let ac_results = document.createElement("div");
ac_results.id = "autocomplete_results";
SEARCH_FORM.appendChild(ac_results);
/**
* Attach `selected` class to the the selected autocomplete result.
*/
function handleSearchCursorUpDown(down) {
const sel = ac_results.querySelector(`.selected`);
if (sel) {
sel.classList.remove("selected");
const toSelect = down
? sel.nextSibling
: sel.previousSibling;
toSelect && toSelect.classList.add("selected");
} else {
const toSelect = down ? ac_results.firstChild : ac_results.lastChild;
toSelect && toSelect.classList.add("selected");
}
}
/**
* Perform search (when enter is pressed).
*/
function handleSearchEnter() {
const sel = ac_results.querySelector(`.selected .result_link a`) || document.querySelector(`#search_button`);
sel.click();
}
/**
* Allow user to navigate autocomplete results with up/down arrow keys, and choose with enter.
*/
SEARCH_INPUT.addEventListener("keydown", (ev) => {
switch (ev.key) {
case "Down":
case "ArrowDown":
ev.preventDefault();
handleSearchCursorUpDown(true);
break;
case "Up":
case "ArrowUp":
ev.preventDefault();
handleSearchCursorUpDown(false);
break;
case "Enter":
ev.preventDefault();
handleSearchEnter();
break;
}
});
/**
* Remove all children of a DOM node.
*/
function removeAllChildren(node) {
while (node.firstChild) {
node.removeChild(node.lastChild);
}
}
/**
* Handle user input and perform search.
*/
function handleSearch(dataCenter, err, ev, sr, maxResults, autocomplete) {
const text = ev.target.value;
// If no input clear all.
if (!text) {
sr.removeAttribute("state");
removeAllChildren(sr);
return;
}
// searching
sr.setAttribute("state", "loading");
if (dataCenter) {
var allowedKinds;
if (!autocomplete) {
allowedKinds = new Set();
document.querySelectorAll(".kind_checkbox").forEach((checkbox) =>
{
if (checkbox.checked) {
allowedKinds.add(checkbox.value);
}
}
);
}
const result = dataCenter.search(text, false, allowedKinds, maxResults);
// in case user has updated the input.
if (ev.target.value != text) return;
// update autocomplete results
removeAllChildren(sr);
for (const { name, kind, docLink } of result) {
const row = sr.appendChild(document.createElement("div"));
row.classList.add("search_result")
const linkdiv = row.appendChild(document.createElement("div"))
linkdiv.classList.add("result_link")
const link = linkdiv.appendChild(document.createElement("a"));
link.innerText = name;
link.title = name;
link.href = SITE_ROOT + docLink;
}
}
// handle error
else {
removeAllChildren(sr);
const d = sr.appendChild(document.createElement("a"));
d.innerText = `Cannot fetch data, please check your network connection.\n${err}`;
}
sr.setAttribute("state", "done");
}
// https://www.joshwcomeau.com/snippets/javascript/debounce/
const debounce = (callback, wait) => {
let timeoutId = null;
return (...args) => {
window.clearTimeout(timeoutId);
timeoutId = window.setTimeout(() => {
callback.apply(null, args);
}, wait);
};
}
DeclarationDataCenter.init()
.then((dataCenter) => {
// Search autocompletion.
SEARCH_INPUT.addEventListener("input", debounce(ev => handleSearch(dataCenter, null, ev, ac_results, AC_MAX_RESULTS, true), 300));
if(SEARCH_PAGE_INPUT) {
SEARCH_PAGE_INPUT.addEventListener("input", ev => handleSearch(dataCenter, null, ev, SEARCH_RESULTS, SEARCH_PAGE_MAX_RESULTS, false))
document.querySelectorAll(".kind_checkbox").forEach((checkbox) =>
checkbox.addEventListener("input", ev => SEARCH_PAGE_INPUT.dispatchEvent(new Event("input")))
);
SEARCH_PAGE_INPUT.dispatchEvent(new Event("input"))
};
SEARCH_INPUT.dispatchEvent(new Event("input"))
})
.catch(e => {
SEARCH_INPUT.addEventListener("input", debounce(ev => handleSearch(null, e, ev, ac_results, AC_MAX_RESULTS, true), 300));
if(SEARCH_PAGE_INPUT) {
SEARCH_PAGE_INPUT.addEventListener("input", ev => handleSearch(null, e, ev, SEARCH_RESULTS, SEARCH_PAGE_MAX_RESULTS, false));
}
});

4
static/site-root.js Normal file
View File

@ -0,0 +1,4 @@
/**
* Get the site root, {siteRoot} is to be replaced by doc-gen4.
*/
export const SITE_ROOT = "{siteRoot}";

815
static/style.css Normal file
View File

@ -0,0 +1,815 @@
@import url('https://fonts.googleapis.com/css2?family=Merriweather&family=Open+Sans&family=Source+Code+Pro&family=Source+Code+Pro:wght@600&display=swap');
* {
box-sizing: border-box;
}
body {
font-family: 'Open Sans', sans-serif;
color: var(--text-color);
background: var(--body-bg);
}
a {
color: var(--link-color);
}
a.pdf {
color: var(--link-pdf-color);
}
h1, h2, h3, h4, h5, h6 {
font-family: 'Merriweather', serif;
}
body { line-height: 1.5; }
nav { line-height: normal; }
:root {
--header-height: 3em;
--fragment-offset: calc(var(--header-height) + 1em);
--content-width: 55vw;
--header-bg: #f8f8f8;
--body-bg: white;
--code-bg: #f3f3f3;
--text-color: black;
--link-color: hsl(210, 100%, 30%);
--link-pdf-color: hsl(272, 61%, 34%);
--implicit-arg-text-color: var(--text-color);
--def-color: #92dce5;
--def-color-hsl-angle: 187;
--theorem-color: #8fe388;
--theorem-color-hsl-angle: 115;
--axiom-and-constant-color: #f44708;
--axiom-and-constant-color-hsl-angle: 16;
--structure-and-inductive-color: #f0a202;
--structure-and-inductive-color-hsl-angle: 40;
--starting-percentage: 100;
--hamburger-bg-color: #eee;
--hamburger-active-color: white;
--hamburger-border-color: #ccc;
--tags-border-color: #555;
--fragment-offset: calc(var(--header-height) + 1em);
--content-width: 55vw;
}
/* automatic dark theme if no javascript */
@media (prefers-color-scheme: dark) {
:root {
--header-bg: #111010;
--body-bg: #171717;
--code-bg: #363333;
--text-color: #eee;
--link-color: #58a6ff;
--link-pdf-color: #9d58fd;
--implicit-arg-text-color: var(--text-color);
--def-color: #1F497F;
--def-color-hsl-angle: 214;
--theorem-color: #134E2D;
--theorem-color-hsl-angle: 146;
--axiom-and-constant-color: #6B1B1A;
--axiom-and-constant-color-hsl-angle: 1;
--structure-and-inductive-color: #73461C;
--structure-and-inductive-color-hsl-angle: 29;
--starting-percentage: 30;
--hamburger-bg-color: #2d2c2c;
--hamburger-active-color: black;
--hamburger-border-color: #717171;
--tags-border-color: #AAA;
}
}
[data-theme="light"] {
color-scheme: light;
--header-height: 3em;
--fragment-offset: calc(var(--header-height) + 1em);
--content-width: 55vw;
--header-bg: #f8f8f8;
--body-bg: white;
--code-bg: #f3f3f3;
--text-color: black;
--link-color: hsl(210, 100%, 30%);
--link-pdf-color: hsl(272, 61%, 34%);
--implicit-arg-text-color: var(--text-color);
--def-color: #92dce5;
--def-color-hsl-angle: 187;
--theorem-color: #8fe388;
--theorem-color-hsl-angle: 115;
--axiom-and-constant-color: #f44708;
--axiom-and-constant-color-hsl-angle: 16;
--structure-and-inductive-color: #f0a202;
--structure-and-inductive-color-hsl-angle: 40;
--starting-percentage: 100;
--hamburger-bg-color: #eee;
--hamburger-active-color: white;
--hamburger-border-color: #ccc;
--tags-border-color: #555;
--fragment-offset: calc(var(--header-height) + 1em);
--content-width: 55vw;
}
[data-theme="dark"] {
color-scheme: dark;
--header-bg: #111010;
--body-bg: #171717;
--code-bg: #363333;
--text-color: #eee;
--link-color: #58a6ff;
--link-pdf-color: #9d58fd;
--implicit-arg-text-color: var(--text-color);
--def-color: #1F497F;
--def-color-hsl-angle: 214;
--theorem-color: #134E2D;
--theorem-color-hsl-angle: 146;
--axiom-and-constant-color: #6B1B1A;
--axiom-and-constant-color-hsl-angle: 1;
--structure-and-inductive-color: #73461C;
--structure-and-inductive-color-hsl-angle: 29;
--starting-percentage: 30;
--hamburger-bg-color: #2d2c2c;
--hamburger-active-color: black;
--hamburger-border-color: #717171;
--tags-border-color: #AAA;
}
@supports (width: min(10px, 5vw)) {
:root {
--content-width: clamp(20em, 55vw, 60em);
}
}
#nav_toggle {
display: none;
}
label[for="nav_toggle"] {
display: none;
}
header {
height: var(--header-height);
float: left;
position: fixed;
width: 100vw;
max-width: 100%;
left: 0;
right: 0;
top: 0;
--header-side-padding: 2em;
padding: 0 var(--header-side-padding);
background: var(--header-bg);
z-index: 1;
display: flex;
align-items: center;
justify-content: space-between;
}
@supports (width: min(10px, 5vw)) {
header {
--header-side-padding: calc(max(2em, (100vw - var(--content-width) - 30em) / 2));
}
}
@media screen and (max-width: 1000px) {
:root {
--content-width: 100vw;
}
.internal_nav {
display: none;
}
body .nav {
width: 100vw;
max-width: 100vw;
margin-left: 1em;
z-index: 1;
}
body main {
width: unset;
max-width: unset;
margin-left: unset;
margin-right: unset;
}
body .decl > div {
overflow-x: unset;
}
#nav_toggle:not(:checked) ~ .nav {
display: none;
}
#nav_toggle:checked ~ main {
visibility: hidden;
}
label[for="nav_toggle"]::before {
content: '≡';
}
label[for="nav_toggle"] {
display: inline-block;
margin-right: 1em;
border: 1px solid var(--hamburger-border-color);
padding: 0.5ex 1ex;
cursor: pointer;
background: var(--hamburger-bg-color);
}
#nav_toggle:checked ~ * label[for="nav_toggle"] {
background: var(--hamburger-active-color);
}
body header h1 {
font-size: 100%;
}
header {
--header-side-padding: 1ex;
}
}
@media screen and (max-width: 700px) {
header h1 span { display: none; }
:root { --header-side-padding: 1ex; }
#search_form button { display: none; }
#search_form input { width: 100%; }
header #autocomplete_results {
left: 1ex;
right: 1ex;
width: inherit;
}
body header > * { margin: 0; }
}
header > * {
display: inline-block;
padding: 0;
margin: 0 1em;
vertical-align: middle;
}
header h1 {
font-weight: normal;
font-size: 160%;
}
header header_filename {
font-size: 150%;
}
@media (max-width: 80em) {
.header .header_filename {
display: none;
}
}
/* inserted by nav.js */
#autocomplete_results {
position: absolute;
top: var(--header-height);
right: calc(var(--header-side-padding));
width: calc(20em + 4em);
z-index: 1;
background: var(--header-bg);
border: 1px solid #aaa;
border-top: none;
overflow-x: hidden;
overflow-y: auto;
max-height: calc(100vh - var(--header-height));
}
#autocomplete_results:empty {
display: none;
}
#autocomplete_results[state="loading"]:empty {
display: block;
cursor: progress;
}
#autocomplete_results[state="loading"]:empty::before {
display: block;
content: ' 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 ';
padding: 1ex;
animation: marquee 10s linear infinite;
}
@keyframes marquee {
0% { transform: translate(100%, 0); }
100% { transform: translate(-100%, 0); }
}
#autocomplete_results[state="done"]:empty {
display: block;
text-align: center;
padding: 1ex;
}
#autocomplete_results[state="done"]:empty::before {
content: '(no results)';
font-style: italic;
}
#autocomplete_results a {
display: block;
color: inherit;
padding: 1ex;
border-left: 0.5ex solid transparent;
padding-left: 0.5ex;
cursor: pointer;
}
#autocomplete_results .selected .result_link a {
background: var(--body-bg);
border-color: var(--structure-and-inductive-color);
}
#search_results {
display: table;
width: 100%;
}
#search_results[state="done"]:empty::before {
content: '(no results)';
font-style: italic;
}
#search_results .result_link, #search_results .result_doc {
border-bottom: 1px solid rgba(0, 0, 0, 0.8);
}
.search_result {
display: table-row;
}
.result_link, .result_doc {
display: table-cell;
overflow: hidden;
word-break: break-word;
}
main, nav {
margin-top: calc(var(--header-height) + 1em);
}
/* extra space for scrolling things to the top */
main {
margin-bottom: 90vh;
}
main {
max-width: var(--content-width);
/* center it: */
margin-left: auto;
margin-right: auto;
}
nav {
float: left;
height: calc(100vh - var(--header-height) - 1em);
position: fixed;
top: 0;
overflow: auto;
scrollbar-width: thin;
scrollbar-color: transparent transparent;
}
nav:hover {
scrollbar-color: gray transparent;
}
nav {
--column-available-space: calc((100vw - var(--content-width) - 5em)/2);
--column-width: calc(var(--column-available-space) - 1ex);
--dist-to-edge: 1ex;
width: var(--content-width);
max-width: var(--column-width);
}
@supports (width: min(10px, 5vw)) {
.nav { --desired-column-width: 20em; }
.internal_nav { --desired-column-width: 30em; }
nav {
--column-available-space: calc(max(0px, (100vw - var(--content-width) - 5em)/2));
--column-width: calc(clamp(0px, var(--column-available-space) - 1ex, var(--desired-column-width)));
--dist-to-edge: calc(max(1ex, var(--column-available-space) - var(--column-width)));
}
}
.nav { left: var(--dist-to-edge); }
.internal_nav { right: var(--dist-to-edge); }
.internal_nav .nav_link, .taclink {
/* indent everything but first line by 2ex */
text-indent: -2ex; padding-left: 2ex;
}
.navframe {
height: 100%;
width: 100%;
}
.navframe .nav {
position: absolute;
left: 0;
margin-left: 0;
}
.internal_nav .imports {
margin-bottom: 1rem;
}
.tagfilter-div {
margin-bottom: 1em;
}
.tagfilter-div > summary {
margin-bottom: 1ex;
}
/* top-level modules in left navbar */
.nav .module_list > details {
margin-top: 1ex;
}
.nav details > * {
padding-left: 2ex;
}
.nav summary {
cursor: pointer;
padding-left: 0;
}
.nav summary::marker {
font-size: 85%;
}
.nav .nav_file {
display: inline-block;
}
.nav h3 {
margin-block-end: 4px;
}
/* People use way too long declaration names. */
.internal_nav, .decl_name {
overflow-wrap: break-word;
}
/* Add a linebreak after a declaration name. */
.decl_name::after {
content: "\A";
white-space: pre;
}
.nav_link {
overflow-wrap: break-word;
}
.navframe {
--header-height: 0;
}
#settings {
margin-top: 5em;
}
#settings h3 {
font-size: inherit;
}
#color-theme-switcher {
display: flex;
justify-content: space-between;
padding: 0 2ex;
flex-flow: row wrap;
}
/* custom radio buttons for dark/light switch */
#color-theme-switcher input {
-webkit-appearance: none;
-moz-appearance: none;
appearance: none;
display: inline-block;
box-sizing: content-box;
height: 1em;
width: 1em;
background-clip: content-box;
padding: 2px;
border: 2px solid transparent;
margin-bottom: -4px;
border-radius: 50%;
}
#color-theme-dark { background-color: #444; }
#color-theme-light { background-color: #ccc; }
#color-theme-system {
background-image: linear-gradient(60deg, #444, #444 50%, #CCC 50%, #CCC);
}
#color-theme-switcher input:checked {
border-color: var(--text-color);
}
.decl > div, .mod_doc {
padding-left: 8px;
padding-right: 8px;
}
.decl {
margin-top: 20px;
margin-bottom: 20px;
}
.decl > div {
/* sometimes declarations arguments are way too long
and would continue into the right column,
so put a scroll bar there: */
overflow-x: auto;
}
/* Make `#id` links appear below header. */
.decl, h1[id], h2[id], h3[id], h4[id], h5[id], h6[id] {
scroll-margin-top: var(--fragment-offset);
}
/* don't need as much vertical space for these
inline elements */
a[id], li[id] {
scroll-margin-top: var(--header-height);
}
/* HACK: Safari doesn't support scroll-margin-top for
fragment links (yet?)
https://caniuse.com/mdn-css_properties_scroll-margin-top
https://bugs.webkit.org/show_bug.cgi?id=189265
*/
@supports not (scroll-margin-top: var(--fragment-offset)) {
.decl::before, h1[id]::before, h2[id]::before, h3[id]::before,
h4[id]::before, h5[id]::before, h6[id]::before,
a[id]::before, li[id]::before {
content: "";
display: block;
height: var(--fragment-offset);
margin-top: calc(-1 * var(--fragment-offset));
box-sizing: inherit;
visibility: hidden;
width: 1px;
}
}
/* hide # after markdown headings except on hover */
.markdown-heading:not(:hover) > .hover-link {
visibility: hidden;
}
main h2, main h3, main h4, main h5, main h6 {
margin-top: 2rem;
}
.decl + .mod_doc > h2,
.decl + .mod_doc > h3,
.decl + .mod_doc > h4,
.decl + .mod_doc > h5,
.decl + .mod_doc > h6 {
margin-top: 4rem;
}
.def, .instance {
border-left: 10px solid var(--text-color);
border-top: 2px solid var(--text-color);
}
.theorem {
border-left: 10px solid var(--theorem-color);
border-top: 2px solid var(--theorem-color);
}
.axiom, .opaque {
border-left: 10px solid var(--axiom-and-constant-color);
border-top: 2px solid var(--axiom-and-constant-color);
}
.structure, .inductive, .class {
border-left: 10px solid var(--structure-and-inductive-color);
border-top: 2px solid var(--structure-and-inductive-color);
}
.fn {
display: inline-block;
/* border: 1px dashed red; */
text-indent: -1ex;
padding-left: 1ex;
white-space: pre-wrap;
vertical-align: top;
}
.fn { --fn: 1; }
.fn .fn { --fn: 2; }
.fn .fn .fn { --fn: 3; }
.fn .fn .fn .fn { --fn: 4; }
.fn .fn .fn .fn .fn { --fn: 5; }
.fn .fn .fn .fn .fn .fn { --fn: 6; }
.fn .fn .fn .fn .fn .fn .fn { --fn: 7; }
.fn .fn .fn .fn .fn .fn .fn .fn { --fn: 8; }
.fn {
transition: background-color 100ms ease-in-out;
}
.def .fn:hover, .instance .fn:hover {
background-color: hsla(var(--def-color-hsl-angle), 61%, calc(var(--starting-percentage) - 5%*var(--fn)));
box-shadow: 0 0 0 1px hsla(var(--def-color-hsl-angle), 61%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1)));
border-radius: 5px;
}
.theorem .fn:hover {
background-color: hsla(var(--theorem-color-hsl-angle), 62%, calc(var(--starting-percentage) - 5%*var(--fn)));
box-shadow: 0 0 0 1px hsla(var(--theorem-color-hsl-angle), 62%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1)));
border-radius: 5px;
}
.axiom .fn:hover, .opaque .fn:hover {
background-color: hsla(var(--axiom-and-constant-color-hsl-angle), 94%, calc(var(--starting-percentage) - 5%*var(--fn)));
box-shadow: 0 0 0 1px hsla(var(--axiom-and-constant-color-hsl-angle), 94%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1)));
border-radius: 5px;
}
.structure .fn:hover, .inductive .fn:hover, .class .fn:hover {
background-color: hsla(var(--structure-and-inductive-color-hsl-angle), 98%, calc(var(--starting-percentage) - 5%*var(--fn)));
box-shadow: 0 0 0 1px hsla(var(--structure-and-inductive-color-hsl-angle), 98%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1)));
border-radius: 5px;
}
.decl_args, .decl_type .decl_parent {
font-weight: normal;
}
.implicits, .impl_arg {
color: var(--text-color);
white-space: normal;
}
.decl_kind, .decl_name, .decl_extends {
font-weight: bold;
}
/* break long declaration names at periods where possible */
.break_within {
word-break: break-all;
}
.break_within .name {
word-break: normal;
}
.decl_header {
/* indent everything but first line twice as much as decl_type */
text-indent: -8ex; padding-left: 8ex;
}
.decl_type {
margin-top: 2px;
margin-left: 4ex; /* extra indentation */
}
.imports li, code, .decl_header, .attributes, .structure_field_info,
.constructor, .instances li, .equation, .result_link, .structure_ext_ctor {
font-family: 'Source Code Pro', monospace;
}
pre {
white-space: break-spaces;
}
code, pre { background: var(--code-bg); }
code, pre { border-radius: 5px; }
code { padding: 1px 3px; }
pre { padding: 1ex; }
pre code { padding: 0 0; }
#howabout code { background: inherit; }
#howabout li { margin-bottom: 0.5ex; }
.structure_fields, .constructors {
display: block;
padding-inline-start: 0;
margin-top: 1ex;
text-indent: -2ex; padding-left: 2ex;
}
.structure_field {
display: block;
margin-left: 2ex;
}
.inductive_ctor_doc {
text-indent: 2ex;
font-family: 'Open Sans', sans-serif;
}
.structure_field_doc {
text-indent: 0;
font-family: 'Open Sans', sans-serif;
}
.structure_ext_fields {
display: block;
padding-inline-start: 0;
margin-top: 1ex;
text-indent: -2ex; padding-left: 2ex;
}
.structure_ext_fields .structure_field {
margin-left: -1ex !important;
}
.structure_ext_ctor {
display: block;
text-indent: -3ex;
}
.constructor {
display: block;
}
.constructor:before {
content: '| ';
color: gray;
}
/** Don't show underline on types, to prevent the ≤ vs < confusion. **/
a:link, a:visited, a:active {
color:var(--link-color);
text-decoration: none;
}
a.pdf:link, a.pdf:visited, a.pdf:active {
color:var(--link-pdf-color);
}
/** Show it on hover though. **/
a:hover {
text-decoration: underline;
}
.impl_arg {
font-style: italic;
transition: opacity 300ms ease-in;
}
.decl_header:not(:hover) .impl_arg {
opacity: 30%;
transition: opacity 1000ms ease-out;
}
.gh_link {
float: right;
margin-left: 10px;
}
.ink_link {
float: right;
margin-left: 20px;
}
.docfile h2, .note h2 {
margin-block-start: 3px;
margin-block-end: 0px;
}
.docfile h2 a {
color: var(--text-color);
}
.tags {
margin-bottom: 1ex;
}
.tags ul {
display: inline;
padding: 0;
}
.tags li {
border: 1px solid var(--tags-border-color);
border-radius: 4px;
list-style-type: none;
padding: 1px 3px;
margin-left: 1ex;
display: inline-block;
}
/* used by nav.js */
.hide { display: none; }
.tactic, .note {
border-top: 3px solid #0479c7;
padding-top: 2em;
margin-top: 2em;
margin-bottom: 2em;
}

61
static/tactic.js Normal file
View File

@ -0,0 +1,61 @@
// TODO: The tactic part seem to be unimplemented now.
function filterSelectionClass(tagNames, classname) {
if (tagNames.length == 0) {
for (const elem of document.getElementsByClassName(classname)) {
elem.classList.remove("hide");
}
} else {
// Add the "show" class (display:block) to the filtered elements, and remove the "show" class from the elements that are not selected
for (const elem of document.getElementsByClassName(classname)) {
elem.classList.add("hide");
for (const tagName of tagNames) {
if (elem.classList.contains(tagName)) {
elem.classList.remove("hide");
}
}
}
}
}
function filterSelection(c) {
filterSelectionClass(c, "tactic");
filterSelectionClass(c, "taclink");
}
var filterBoxes = document.getElementsByClassName("tagfilter");
function updateDisplay() {
filterSelection(getSelectValues());
}
function getSelectValues() {
var result = [];
for (const opt of filterBoxes) {
if (opt.checked) {
result.push(opt.value);
}
}
return result;
}
function setSelectVal(val) {
for (const opt of filterBoxes) {
opt.checked = val;
}
}
updateDisplay();
for (const opt of filterBoxes) {
opt.addEventListener("change", updateDisplay);
}
const tse = document.getElementById("tagfilter-selectall");
if (tse != null) {
tse.addEventListener("change", function () {
setSelectVal(this.checked);
updateDisplay();
});
}