Merge pull request #225 from leanprover/bump_to_v4.13.0

chore: bump toolchain to v4.13.0

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6d2e06515f1ed1f74208d5a1da3a9cc26c60a7a0",
+   "rev": "107e98b3e7603628d9bfd817b4704488d8a25e96",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "85e1e7143dd4cfa2b551826c27867bada60858e8",
+   "rev": "bdc2fc30b1e834b294759a5d391d83020a90058e",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bf066c328bcff19aa93adf4d24c4e896c0d4eaca",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "«doc-gen4»",

lakefile.lean

@@ -21,7 +21,7 @@ require «UnicodeBasic» from git
   "https://github.com/fgdorais/lean4-unicode-basic" @ "main"
 
 require Cli from git
-  "https://github.com/mhuisi/lean4-cli" @ "nightly"
+  "https://github.com/mhuisi/lean4-cli" @ "main"
 
 /--
 Obtain the Github URL of a project by parsing the origin remote.

lean-toolchain

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

test_docs.sh

@@ -1,13 +1,16 @@
 # Arguments:
 # $1 : path to batteries from working directory
-# $2 : path to doc-gen4 from working directory
 
 set -e
 set -x
 
 # generate the docs
 cd "$1"
-echo 'require «doc-gen4» from ".." / "doc-gen4"' >> lakefile.lean
+cat >> lakefile.toml << 'EOL'
+[[require]]
+name = "«doc-gen4»"
+path = "../doc-gen4"
+EOL
 
 lake update doc-gen4
 lake build Batteries:docs