diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 8bdf61b..71f9f50 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -21,10 +21,6 @@ jobs: ~/.elan/bin/lean --version echo "$HOME/.elan/bin" >> $GITHUB_PATH - - name: Compile doc-gen4 - run: | - lake build - - name: Checkout and compile std4 run: | cd ../ diff --git a/lake-manifest.json b/lake-manifest.json index 60dd202..f607b57 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -7,6 +7,12 @@ "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77", "name": "CMark", "inputRev?": "main"}}, + {"git": + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "subDir?": null, + "rev": "f09250282cea3ed8c010f430264d9e8e50d7bc32", + "name": "lean4-unicode-basic", + "inputRev?": "main"}}, {"git": {"url": "https://github.com/mhuisi/lean4-cli", "subDir?": null, @@ -18,10 +24,4 @@ "subDir?": null, "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1", "name": "leanInk", - "inputRev?": "doc-gen"}}, - {"git": - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "subDir?": null, - "rev": "f09250282cea3ed8c010f430264d9e8e50d7bc32", - "name": "UnicodeBasic", - "inputRev?": "main"}}]} + "inputRev?": "doc-gen"}}]} diff --git a/lakefile.lean b/lakefile.lean index 0362a70..48530a7 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -14,7 +14,7 @@ lean_exe «doc-gen4» { require CMark from git "https://github.com/xubaiw/CMark.lean" @ "main" -require UnicodeBasic from git +require «lean4-unicode-basic» from git "https://github.com/fgdorais/lean4-unicode-basic" @ "main" require Cli from git diff --git a/lean-toolchain b/lean-toolchain index e183d2c..dc4c3b8 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2023-07-30 +leanprover/lean4:nightly-2023-08-03 diff --git a/test_docs.sh b/test_docs.sh index 8a2579d..387af03 100755 --- a/test_docs.sh +++ b/test_docs.sh @@ -5,10 +5,6 @@ set -e set -x -# carry the already built doc-gen4 over -mkdir -p "$1"/lake-packages -rsync -av --exclude=".*" "$2"/lake-packages/* "$1"/lake-packages - # generate the docs cd "$1" sed -i "s|from git \"https://github.com/leanprover/doc-gen4\" @ \"main\"| from \"..\" / \"doc-gen4\" with NameMap.empty|" lakefile.lean