chore: update toolchain 10-20 (#86)

main
Mario Carneiro 2022-10-20 19:51:26 +02:00 committed by GitHub
parent 153982f982
commit 9aef28b16e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
10 changed files with 32 additions and 33 deletions

View File

@ -27,20 +27,20 @@ def execAuxM : HtmlT LeanInk.AnalysisM UInt32 := do
let ctx ← readThe SiteContext let ctx ← readThe SiteContext
let baseCtx ← readThe SiteBaseContext let baseCtx ← readThe SiteBaseContext
let outputFn := (docGenOutput · |>.run ctx baseCtx) let outputFn := (docGenOutput · |>.run ctx baseCtx)
return ← LeanInk.Analysis.runAnalysis { return ← LeanInk.Analysis.runAnalysis {
name := "doc-gen4" name := "doc-gen4"
genOutput := outputFn genOutput := outputFn
} }
def execAux (config : LeanInk.Configuration) : HtmlT IO UInt32 := do def execAux (config : LeanInk.Configuration) : HtmlT IO UInt32 := do
execAuxM.run (←readThe SiteContext) (←readThe SiteBaseContext) |>.run config execAuxM.run (←readThe SiteContext) (←readThe SiteBaseContext) |>.run config
@[implementedBy enableInitializersExecution] @[implemented_by enableInitializersExecution]
private def enableInitializersExecutionWrapper : IO Unit := pure () private def enableInitializersExecutionWrapper : IO Unit := pure ()
def runInk (sourceFilePath : System.FilePath) : HtmlT IO Unit := do def runInk (sourceFilePath : System.FilePath) : HtmlT IO Unit := do
let contents ← IO.FS.readFile sourceFilePath let contents ← IO.FS.readFile sourceFilePath
let config := { let config := {
inputFilePath := sourceFilePath inputFilePath := sourceFilePath
inputFileContents := contents inputFileContents := contents
lakeFile := none lakeFile := none

View File

@ -43,8 +43,8 @@ def manyDocument : Parsec (Array Element) := many (prolog *> element <* many Mis
partial def xmlGetHeadingId (el : Xml.Element) : String := partial def xmlGetHeadingId (el : Xml.Element) : String :=
elementToPlainText el |> replaceCharSeq unicodeToDrop "-" elementToPlainText el |> replaceCharSeq unicodeToDrop "-"
where where
elementToPlainText el := match el with elementToPlainText el := match el with
| (Element.Element _ _ contents) => | (Element.Element _ _ contents) =>
"".intercalate (contents.toList.map contentToPlainText) "".intercalate (contents.toList.map contentToPlainText)
contentToPlainText c := match c with contentToPlainText c := match c with
| Content.Element el => elementToPlainText el | Content.Element el => elementToPlainText el
@ -54,10 +54,10 @@ partial def xmlGetHeadingId (el : Xml.Element) : String :=
s.split pattern s.split pattern
|>.filter (!·.isEmpty) |>.filter (!·.isEmpty)
|> replacement.intercalate |> replacement.intercalate
unicodeToDrop (c : Char) : Bool := unicodeToDrop (c : Char) : Bool :=
charInGeneralCategory c GeneralCategory.punctuation || charInGeneralCategory c GeneralCategory.punctuation ||
charInGeneralCategory c GeneralCategory.separator || charInGeneralCategory c GeneralCategory.separator ||
charInGeneralCategory c GeneralCategory.other charInGeneralCategory c GeneralCategory.other
/-- /--
This function try to find the given name, both globally and in current module. This function try to find the given name, both globally and in current module.
@ -79,7 +79,7 @@ def nameToLink? (s : String) : HtmlM (Option String) := do
match (← getCurrentName) with match (← getCurrentName) with
| some currentName => | some currentName =>
match res.moduleInfo.find! currentName |>.members |> filterMapDocInfo |>.find? (sameEnd ·.getName name) with match res.moduleInfo.find! currentName |>.members |> filterMapDocInfo |>.find? (sameEnd ·.getName name) with
| some info => | some info =>
declNameToLink info.getName declNameToLink info.getName
| _ => pure none | _ => pure none
| _ => pure none | _ => pure none
@ -88,7 +88,7 @@ def nameToLink? (s : String) : HtmlM (Option String) := do
where where
-- check if two names have the same ending components -- check if two names have the same ending components
sameEnd n1 n2 := sameEnd n1 n2 :=
List.zip n1.components' n2.components' List.zip n1.componentsRev n2.componentsRev
|>.all λ ⟨a, b⟩ => a == b |>.all λ ⟨a, b⟩ => a == b
/-- /--
@ -106,11 +106,11 @@ def extendLink (s : String) : HtmlM String := do
pure link pure link
else else
panic! s!"Cannot find {s.drop 2}, only full name and abbrev in current module is supported" panic! s!"Cannot find {s.drop 2}, only full name and abbrev in current module is supported"
-- for id -- for id
else if s.startsWith "#" then else if s.startsWith "#" then
pure s pure s
-- for absolute and relative urls -- for absolute and relative urls
else if s.startsWith "http" then else if s.startsWith "http" then
pure s pure s
else pure ((←getRoot) ++ s) else pure ((←getRoot) ++ s)
@ -126,13 +126,13 @@ def addHeadingAttributes (el : Element) (modifyElement : Element → HtmlM Eleme
let newAttrs := attrs let newAttrs := attrs
|>.insert "id" id |>.insert "id" id
|>.insert "class" "markdown-heading" |>.insert "class" "markdown-heading"
let newContents := (← let newContents := (←
contents.mapM (λ c => match c with contents.mapM (λ c => match c with
| Content.Element e => return Content.Element (← modifyElement e) | Content.Element e => return Content.Element (← modifyElement e)
| _ => pure c)) | _ => pure c))
|>.push (Content.Character " ") |>.push (Content.Character " ")
|>.push (Content.Element anchor) |>.push (Content.Element anchor)
pure ⟨ name, newAttrs, newContents⟩ pure ⟨ name, newAttrs, newContents⟩
/-- Extend anchor links. -/ /-- Extend anchor links. -/
def extendAnchor (el : Element) : HtmlM Element := do def extendAnchor (el : Element) : HtmlM Element := do
@ -158,7 +158,7 @@ def autoLink (el : Element) : HtmlM Element := do
linkify s := do linkify s := do
let link? ← nameToLink? s let link? ← nameToLink? s
match link? with match link? with
| some link => | some link =>
let attributes := Lean.RBMap.empty.insert "href" link let attributes := Lean.RBMap.empty.insert "href" link
pure [Content.Element <| Element.Element "a" attributes #[Content.Character s]] pure [Content.Element <| Element.Element "a" attributes #[Content.Character s]]
| none => | none =>
@ -166,7 +166,7 @@ def autoLink (el : Element) : HtmlM Element := do
let sTail := s.takeRightWhile (λ c => c ≠ '.') let sTail := s.takeRightWhile (λ c => c ≠ '.')
let link'? ← nameToLink? sTail let link'? ← nameToLink? sTail
match link'? with match link'? with
| some link' => | some link' =>
let attributes := Lean.RBMap.empty.insert "href" link' let attributes := Lean.RBMap.empty.insert "href" link'
pure [ pure [
Content.Character sHead, Content.Character sHead,
@ -174,9 +174,9 @@ def autoLink (el : Element) : HtmlM Element := do
] ]
| none => | none =>
pure [Content.Character s] pure [Content.Character s]
unicodeToSplit (c : Char) : Bool := unicodeToSplit (c : Char) : Bool :=
charInGeneralCategory c GeneralCategory.separator || charInGeneralCategory c GeneralCategory.separator ||
charInGeneralCategory c GeneralCategory.other charInGeneralCategory c GeneralCategory.other
/-- Core function of modifying the cmark rendered docstring html. -/ /-- Core function of modifying the cmark rendered docstring html. -/
partial def modifyElement (element : Element) : HtmlM Element := partial def modifyElement (element : Element) : HtmlM Element :=
match element with match element with
@ -195,13 +195,13 @@ partial def modifyElement (element : Element) : HtmlM Element :=
let newContents ← contents.mapM λ c => match c with let newContents ← contents.mapM λ c => match c with
| Content.Element e => return Content.Element (← modifyElement e) | Content.Element e => return Content.Element (← modifyElement e)
| _ => pure c | _ => pure c
pure ⟨ name, attrs, newContents ⟩ pure ⟨ name, attrs, newContents ⟩
/-- Convert docstring to Html. -/ /-- Convert docstring to Html. -/
def docStringToHtml (s : String) : HtmlM (Array Html) := do def docStringToHtml (s : String) : HtmlM (Array Html) := do
let rendered := CMark.renderHtml s let rendered := CMark.renderHtml s
match manyDocument rendered.mkIterator with match manyDocument rendered.mkIterator with
| Parsec.ParseResult.success _ res => | Parsec.ParseResult.success _ res =>
res.mapM λ x => do res.mapM λ x => do
pure (Html.text <| toString (← modifyElement x)) pure (Html.text <| toString (← modifyElement x))
| _ => pure #[Html.text rendered] | _ => pure #[Html.text rendered]

View File

@ -16,7 +16,7 @@ def instancesForToHtml (typeName : Name) : HtmlM Html := do
</details> </details>
def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do
let shortName := c.name.components'.head!.toString let shortName := c.name.componentsRev.head!.toString
let name := c.name.toString let name := c.name.toString
if let some doc := c.doc then if let some doc := c.doc then
let renderedDoc ← docStringToHtml doc let renderedDoc ← docStringToHtml doc

View File

@ -30,8 +30,6 @@ def argToHtml (arg : Arg) : HtmlM Html := do
| BinderInfo.implicit => ("{", "}", true) | BinderInfo.implicit => ("{", "}", true)
| BinderInfo.strictImplicit => ("⦃", "⦄", true) | BinderInfo.strictImplicit => ("⦃", "⦄", true)
| BinderInfo.instImplicit => ("[", "]", true) | BinderInfo.instImplicit => ("[", "]", true)
-- TODO: Can this ever be reached here? What does it mean?
| BinderInfo.auxDecl => unreachable!
let mut nodes := #[Html.text s!"{l}{arg.name.toString} : "] let mut nodes := #[Html.text s!"{l}{arg.name.toString} : "]
nodes := nodes.append (←infoFormatToHtml arg.type) nodes := nodes.append (←infoFormatToHtml arg.type)
nodes := nodes.push r nodes := nodes.push r
@ -146,7 +144,7 @@ Rendering a module doc string, that is the ones with an ! after the opener
as HTML. as HTML.
-/ -/
def modDocToHtml (mdoc : ModuleDoc) : HtmlM Html := do def modDocToHtml (mdoc : ModuleDoc) : HtmlM Html := do
pure pure
<div class="mod_doc"> <div class="mod_doc">
[←docStringToHtml mdoc.doc] [←docStringToHtml mdoc.doc]
</div> </div>

View File

@ -12,7 +12,7 @@ open Lean
Render a single field consisting of its documentation, its name and its type as HTML. Render a single field consisting of its documentation, its name and its type as HTML.
-/ -/
def fieldToHtml (f : Process.NameInfo) : HtmlM Html := do def fieldToHtml (f : Process.NameInfo) : HtmlM Html := do
let shortName := f.name.components'.head!.toString let shortName := f.name.componentsRev.head!.toString
let name := f.name.toString let name := f.name.toString
if let some doc := f.doc then if let some doc := f.doc then
let renderedDoc ← docStringToHtml doc let renderedDoc ← docStringToHtml doc
@ -37,7 +37,7 @@ def structureToHtml (i : Process.StructureInfo) : HtmlM (Array Html) := do
[←i.fieldInfo.mapM fieldToHtml] [←i.fieldInfo.mapM fieldToHtml]
</ul>) </ul>)
else else
let ctorShortName := i.ctor.name.components'.head!.toString let ctorShortName := i.ctor.name.componentsRev.head!.toString
(<ul class="structure_ext"> (<ul class="structure_ext">
<li id={i.ctor.name.toString} class="structure_ext_ctor">{s!"{ctorShortName} "} :: (</li> <li id={i.ctor.name.toString} class="structure_ext_ctor">{s!"{ctorShortName} "} :: (</li>
<ul class="structure_ext_fields"> <ul class="structure_ext_fields">

View File

@ -78,8 +78,8 @@ def jsxText : Parser :=
let s := takeWhile1Fn (not ∘ "[{<>}]$".contains) "expected JSX text" c s let s := takeWhile1Fn (not ∘ "[{<>}]$".contains) "expected JSX text" c s
mkNodeToken `jsxText startPos c s } mkNodeToken `jsxText startPos c s }
@[combinatorFormatter DocGen4.Jsx.jsxText] def jsxText.formatter : Formatter := pure () @[combinator_formatter DocGen4.Jsx.jsxText] def jsxText.formatter : Formatter := pure ()
@[combinatorParenthesizer DocGen4.Jsx.jsxText] def jsxText.parenthesizer : Parenthesizer := pure () @[combinator_parenthesizer DocGen4.Jsx.jsxText] def jsxText.parenthesizer : Parenthesizer := pure ()
syntax jsxAttrName := rawIdent <|> str syntax jsxAttrName := rawIdent <|> str
syntax jsxAttrVal := str <|> group("{" term "}") syntax jsxAttrVal := str <|> group("{" term "}")

View File

@ -64,8 +64,9 @@ instance : ToString InlineAttributeKind where
match kind with match kind with
| InlineAttributeKind.inline => "inline" | InlineAttributeKind.inline => "inline"
| InlineAttributeKind.noinline => "noinline" | InlineAttributeKind.noinline => "noinline"
| InlineAttributeKind.macroInline => "macroInline" | InlineAttributeKind.macroInline => "macro_inline"
| InlineAttributeKind.inlineIfReduce => "inlineIfReduce" | InlineAttributeKind.inlineIfReduce => "inline_if_reduce"
| InlineAttributeKind.alwaysInline => "always_inline"
open Compiler in open Compiler in
instance : ToString SpecializeAttributeKind where instance : ToString SpecializeAttributeKind where

View File

@ -14,7 +14,7 @@ namespace DocGen4
open Lean Name open Lean Name
def getNLevels (name : Name) (levels: Nat) : Name := def getNLevels (name : Name) (levels: Nat) : Name :=
let components := name.components' let components := name.componentsRev
(components.drop (components.length - levels)).reverse.foldl (· ++ ·) Name.anonymous (components.drop (components.length - levels)).reverse.foldl (· ++ ·) Name.anonymous
inductive Hierarchy where inductive Hierarchy where

View File

@ -5,7 +5,7 @@ package «doc-gen4»
lean_lib DocGen4 lean_lib DocGen4
@[defaultTarget] @[default_target]
lean_exe «doc-gen4» { lean_exe «doc-gen4» {
root := `Main root := `Main
supportInterpreter := true supportInterpreter := true

View File

@ -1 +1 @@
leanprover/lean4:nightly-2022-10-03 leanprover/lean4:nightly-2022-10-20