chore: update toolchain 10-20 (#86)

DocGen4/LeanInk/Process.lean

@@ -27,20 +27,20 @@ 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 { 
+  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
 
-@[implementedBy enableInitializersExecution]
+@[implemented_by enableInitializersExecution]
 private def enableInitializersExecutionWrapper : IO Unit := pure ()
 
 def runInk (sourceFilePath : System.FilePath) : HtmlT IO Unit := do
   let contents ← IO.FS.readFile sourceFilePath
-  let config := { 
+  let config := {
     inputFilePath := sourceFilePath
     inputFileContents := contents
     lakeFile := none

DocGen4/Output/DocString.lean

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

DocGen4/Output/Inductive.lean

@@ -16,7 +16,7 @@ def instancesForToHtml (typeName : Name) : HtmlM Html := do
     </details>
 
 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
   if let some doc := c.doc then
     let renderedDoc ← docStringToHtml doc

DocGen4/Output/Module.lean

@@ -30,8 +30,6 @@ def argToHtml (arg : Arg) : HtmlM Html := do
   | BinderInfo.implicit => ("{", "}", true)
   | BinderInfo.strictImplicit => ("⦃", "⦄", 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} : "]
   nodes := nodes.append (←infoFormatToHtml arg.type)
   nodes := nodes.push r
@@ -146,7 +144,7 @@ Rendering a module doc string, that is the ones with an ! after the opener
 as HTML.
 -/
 def modDocToHtml (mdoc : ModuleDoc) : HtmlM Html := do
-  pure 
+  pure
     <div class="mod_doc">
       [←docStringToHtml mdoc.doc]
     </div>

DocGen4/Output/Structure.lean

@@ -12,7 +12,7 @@ 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.components'.head!.toString
+  let shortName := f.name.componentsRev.head!.toString
   let name := f.name.toString
   if let some doc := f.doc then
     let renderedDoc ← docStringToHtml doc
@@ -37,7 +37,7 @@ def structureToHtml (i : Process.StructureInfo) : HtmlM (Array Html) := do
         [←i.fieldInfo.mapM fieldToHtml]
       </ul>)
     else
-      let ctorShortName := i.ctor.name.components'.head!.toString
+      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">

DocGen4/Output/ToHtmlFormat.lean

@@ -78,8 +78,8 @@ def jsxText : Parser :=
       let s := takeWhile1Fn (not ∘ "[{<>}]$".contains) "expected JSX text" c s
       mkNodeToken `jsxText startPos c s }
 
-@[combinatorFormatter DocGen4.Jsx.jsxText] def jsxText.formatter : Formatter := pure ()
-@[combinatorParenthesizer DocGen4.Jsx.jsxText] def jsxText.parenthesizer : Parenthesizer := pure ()
+@[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 "}")

DocGen4/Process/Attributes.lean

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

DocGen4/Process/Hierarchy.lean

@@ -14,7 +14,7 @@ namespace DocGen4
 open Lean 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
 
 inductive Hierarchy where

lakefile.lean

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

lean-toolchain

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