chore: toolchain upgrade (#82)

Halleluja!

.github/workflows/build.yml

@@ -4,6 +4,8 @@ on:
   schedule:
     - cron: '0 */2 * * *' # every 2 hours
   push:
+    branches:
+      - "main"
   pull_request:
 
 jobs:
@@ -12,7 +14,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
 
       - name: install elan
         run: |
@@ -32,6 +34,7 @@ jobs:
         run: |
           if [ "$github_repo" = "leanprover/doc-gen4" ] && [ "$github_ref" = "refs/heads/main" ]; then
             deploy="true"
+            DOC_GEN_REF="main"
           else
             deploy="false"
           fi
@@ -39,5 +42,4 @@ jobs:
           ./doc-gen4/deploy_docs.sh "mathlib4" "doc-gen4" "$deploy" "LeanInk"
         env:
           MATHLIB4_DOCS_KEY: ${{ secrets.MATHLIB4_DOCS_KEY }}
-          github_repo: ${{ github.repository }}
+          DOC_GEN_REF: ${{ github.event.pull_request.head.sha }}
-          github_ref: ${{ github.ref }}

DocGen4/Load.lean

@@ -8,11 +8,11 @@ import Lean
 import Lake
 import Lake.CLI.Main
 import DocGen4.Process
-import Std.Data.HashMap
+import Lean.Data.HashMap
 
 namespace DocGen4
 
-open Lean System Std IO
+open Lean System IO
 
 /--
 Sets up a lake workspace for the current project. Furthermore initialize
@@ -56,6 +56,6 @@ def load (task : Process.AnalyzeTask) : IO (Process.AnalyzerResult × Hierarchy)
   Prod.fst <$> Meta.MetaM.toIO (Process.process task) config { env := env } {} {}
 
 def loadCore : IO (Process.AnalyzerResult × Hierarchy) := do
-  load <| .loadAll [`Init, `Std, `Lean]
+  load <| .loadAll [`Init, `Lean]
 
 end DocGen4

DocGen4/Output.lean

@@ -14,11 +14,11 @@ import DocGen4.Output.Find
 import DocGen4.Output.SourceLinker
 import DocGen4.Output.ToJson
 import DocGen4.LeanInk.Process
-import Std.Data.HashMap
+import Lean.Data.HashMap
 
 namespace DocGen4
 
-open Lean IO System Output Process Std
+open Lean IO System Output Process
 
 def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
   let findBasePath := basePath / "find"

DocGen4/Output/DocString.lean

@@ -27,7 +27,7 @@ namespace Output
 -/
 def splitAround (s : String) (p : Char → Bool) : List String := splitAroundAux s p 0 0 []
 
-instance : Inhabited Element := ⟨"", Std.RBMap.empty, #[]⟩
+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
@@ -119,7 +119,7 @@ def addHeadingAttributes (el : Element) (modifyElement : Element → HtmlM Eleme
   match el with
   | Element.Element name attrs contents => do
     let id := xmlGetHeadingId el
-    let anchorAttributes := Std.RBMap.empty
+    let anchorAttributes := Lean.RBMap.empty
       |>.insert "class" "hover-link"
       |>.insert "href" s!"#{id}"
     let anchor := Element.Element "a" anchorAttributes #[Content.Character "#"]
@@ -159,7 +159,7 @@ def autoLink (el : Element) : HtmlM Element := do
       let link? ← nameToLink? s
       match link? with
       | some link => 
-        let attributes := Std.RBMap.empty.insert "href" 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 ≠ '.')
@@ -167,7 +167,7 @@ def autoLink (el : Element) : HtmlM Element := do
         let link'? ← nameToLink? sTail
         match link'? with
         | some link' => 
-          let attributes := Std.RBMap.empty.insert "href" link'
+          let attributes := Lean.RBMap.empty.insert "href" link'
           pure [
             Content.Character sHead,
             Content.Element <| Element.Element "a" attributes #[Content.Character sTail]

DocGen4/Output/SourceLinker.lean

@@ -57,7 +57,7 @@ declarations into (optionally positional) Github URLs.
 def sourceLinker (ws : Lake.Workspace) : IO (Name → Option DeclarationRange → String) := do
   let leanHash := ws.lakeEnv.lean.githash
   -- Compute a map from package names to source URL
-  let mut gitMap := Std.mkHashMap
+  let mut gitMap := Lean.mkHashMap
   let projectBaseUrl := getGithubBaseUrl (←getProjectGithubUrl)
   let projectCommit ← getProjectCommit
   gitMap := gitMap.insert ws.root.name (projectBaseUrl, projectCommit)
@@ -72,7 +72,7 @@ def sourceLinker (ws : Lake.Workspace) : IO (Name → Option DeclarationRange
     let parts := module.components.map Name.toString
     let path := (parts.intersperse "/").foldl (· ++ ·) ""
     let root := module.getRoot
-    let basic := if root == `Lean ∨ root == `Init ∨ root == `Std then
+    let basic := if root == `Lean ∨ root == `Init then
       s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean"
     else
       match ws.packageArray.find? (·.isLocalModule module) with

DocGen4/Output/ToHtmlFormat.lean

@@ -121,7 +121,7 @@ private def htmlHelper (n : Syntax) (children : Array Syntax) (m : Syntax) : Mac
   let mut cs ← `(#[])
   for child in children do
     cs ← match child with
-    | `(jsxChild|$t:jsxText)    => `(($cs).push (Html.text $(quote t.raw[0].getAtomVal!)))
+    | `(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))

DocGen4/Output/ToJson.lean

@@ -1,11 +1,11 @@
 import Lean
 import DocGen4.Process
 import DocGen4.Output.Base
-import Std.Data.RBMap
+import Lean.Data.RBMap
 
 namespace DocGen4.Output
 
-open Lean Std
+open Lean
 
 structure JsonDeclaration where
   name : String

DocGen4/Process/Analyze.lean

@@ -5,8 +5,8 @@ Authors: Henrik Böving
 -/
 
 import Lean
-import Std.Data.HashMap
+import Lean.Data.HashMap
-import Std.Data.HashSet
+import Lean.Data.HashSet
 
 import DocGen4.Process.Base
 import DocGen4.Process.Hierarchy
@@ -14,7 +14,7 @@ import DocGen4.Process.DocInfo
 
 namespace DocGen4.Process
 
-open Lean Meta Std
+open Lean Meta
 
 /--
 Member of a module, either a declaration or some module doc string.

DocGen4/Process/Attributes.lean

@@ -77,7 +77,7 @@ instance : ToString SpecializeAttributeKind where
 /--
 The list of all enum based attributes doc-gen knows about and can recover.
 -/
-def enumAttributes : Array EnumAttrWrapper := #[⟨Compiler.inlineAttrs⟩, ⟨Compiler.specializeAttrs⟩]
+def enumAttributes : Array EnumAttrWrapper := #[⟨Compiler.inlineAttrs⟩]
 
 instance : ToString ExternEntry where
   toString entry :=
@@ -97,7 +97,7 @@ instance : ToString ExternAttrData where
 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⟩]
+def parametricAttributes : Array ParametricAttrWrapper := #[⟨externAttr⟩, ⟨Compiler.implementedByAttr⟩, ⟨exportAttr⟩, ⟨Compiler.specializeAttr⟩]
 
 def getTags (decl : Name) : MetaM (Array String) := do
   let env ← getEnv
@@ -127,7 +127,7 @@ def getDefaultInstance (decl : Name) (className : Name) : MetaM (Option String)
 def hasSimp (decl : Name) : MetaM (Option String) := do
   let thms ← simpExtension.getTheorems
   pure <|
-    if thms.isLemma decl then
+    if thms.isLemma (.decl decl) then
       some "simp"
     else
       none

DocGen4/Process/Hierarchy.lean

@@ -4,11 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 import Lean
-import Std.Data.HashMap
+import Lean.Data.HashMap
 
-open Std
+def Lean.HashSet.fromArray [BEq α] [Hashable α] (xs : Array α) : Lean.HashSet α :=
-
-def HashSet.fromArray [BEq α] [Hashable α] (xs : Array α) : HashSet α :=
   xs.foldr (flip .insert) .empty
 
 namespace DocGen4

Main.lean

@@ -64,7 +64,7 @@ def indexCmd := `[Cli|
 
 def genCoreCmd := `[Cli|
   genCore VIA runGenCoreCmd;
-  "Generate documentation for the core Lean modules: Init, Std and Lean since they are not Lake projects"
+  "Generate documentation for the core Lean modules: Init and Lean since they are not Lake projects"
 ]
 
 def docGenCmd : Cmd := `[Cli|

deploy_docs.sh

@@ -10,21 +10,23 @@ cd $1
 mathlib_short_git_hash="$(git log -1 --pretty=format:%h)"
 
 cd ../$2
-docgen_git_hash="$(git log -1 --pretty=format:%h)"
+DOC_GEN_URL="$GITHUB_SERVER_URL/$GITHUB_REPOSITORY"
 
 cd ../
 
 git clone "https://github.com/leanprover-community/mathlib4_docs.git" mathlib4_docs
 
 # skip if docs for this commit have already been generated
-if [ "$(cd mathlib4_docs && git log -1 --pretty=format:%s)" == "automatic update to mathlib4 $mathlib_short_git_hash using doc-gen4 $docgen_git_hash" ]; then
+if [ "$(cd mathlib4_docs && git log -1 --pretty=format:%s)" == "automatic update to mathlib4 $mathlib_short_git_hash using doc-gen4 $DOC_GEN_REF" ]; then
   exit 0
 fi
 
 # generate the docs
 cd $1
-sed -i "s/git \"https:\/\/github.com\/leanprover\/doc-gen4\" @ \"main\"/\"..\" \/ \"$2\" with NameMap.empty/" lakefile.lean
+sed -i "s|\"https://github.com/leanprover/doc-gen4\" @ \"main\"|\"$DOC_GEN_URL\" @ \"$DOC_GEN_REF\"|" lakefile.lean
-lake -Kdoc=on build Mathlib:docs --verbose
+rm -rf lean_packages/manifest.json
+lake -Kdoc=on update
+lake -Kdoc=on build Mathlib:docs Std:docs --verbose
 
 if [ "$3" = "true" ]; then
   cd ..
@@ -39,6 +41,6 @@ if [ "$3" = "true" ]; then
   git config user.name "leanprover-community-bot"
   git add -A .
   git checkout --orphan master2
-  git commit -m "automatic update to mathlib4 $mathlib_short_git_hash using doc-gen4 $docgen_git_hash"
+  git commit -m "automatic update to mathlib4 $mathlib_short_git_hash using doc-gen4 $DOC_GEN_REF"
   git push -f origin HEAD:master
 fi

lakefile.lean

@@ -54,7 +54,7 @@ target coreDocs : FilePath := do
   let dataFile := basePath / "declarations" / "declaration-data-Lean.bmp"
   exeJob.bindSync fun exeFile exeTrace => do
     let trace ← buildFileUnlessUpToDate dataFile exeTrace do
-      logInfo "Documenting Lean core: Init, Std, Lean"
+      logInfo "Documenting Lean core: Init and Lean"
       proc {
         cmd := exeFile.toString
         args := #["genCore"]

lean-toolchain

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

lean_packages/manifest.json

@@ -1,20 +1,22 @@
 {"version": 2,
  "packages":
  [{"url": "https://github.com/mhuisi/lean4-cli",
-   "rev": "112b35fc348a4a18d2111ac2c6586163330b4941",
+   "rev": "80b783a8905a4e8a29ced841abb64f710bc86f06",
-   "name": "Cli"},
+   "name": "Cli",
+   "inputRev": "nightly"},
   {"url": "https://github.com/hargonix/LeanInk",
    "rev": "439303af06465824588a486f5f9c023ca69979f3",
-   "name": "leanInk"},
+   "name": "leanInk",
+   "inputRev": "doc-gen"},
   {"url": "https://github.com/xubaiw/Unicode.lean",
-   "rev": "25b32ef69fd6d8ae34300d51dc0b9403ffb1fd29",
+   "rev": "3a74ad4a69a3720ad8bd5f50a3233fe393f3f38e",
-   "name": "Unicode"},
+   "name": "Unicode",
-  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "inputRev": "main"},
-   "rev": "ecd37441047e490ff2ad339e16f45bb8b58591bd",
-   "name": "mathlib"},
   {"url": "https://github.com/leanprover/lake",
-   "rev": "6cfb4e3fd7ff700ace8c2cfdb85056d59f321920",
+   "rev": "2cc00e4e08473939842d823fd753dcac891ab709",
-   "name": "lake"},
+   "name": "lake",
+   "inputRev": "master"},
   {"url": "https://github.com/xubaiw/CMark.lean",
    "rev": "8c0f9c1b16ee8047813f43b1f92de471782114ff",
-   "name": "CMark"}]}
+   "name": "CMark",
+   "inputRev": "main"}]}