CI changes coming from add-combi

* Replace `lakefile.toml` by `lakefile.lean`
* Acquire `scripts/build_docs.sh`
* Drop `scripts/bump.sh`
* Rename `docs/` to `website/`

Author: YaelDillies

.github/workflows/push.yml

@@ -1,3 +1,5 @@
+name: Build Lean project
+
 on:
   push:
     branches:
@@ -29,94 +31,85 @@ jobs:
     name: Build project
     steps:
       - name: Checkout project
-        uses: actions/checkout@v2
-        with:
-          fetch-depth: 0
+        uses: actions/checkout@v4
 
-      - name: Print files to upstream
-        run: |
-          grep -r --files-without-match 'import PersistentDecomp' PersistentDecomp | sort > 1.txt
-          grep -r --files-with-match 'sorry' PersistentDecomp | sort > 2.txt
-          mkdir -p docs/_includes
-          comm -23 1.txt 2.txt | sed -e 's/^\(.*\)$/- [`\1`](https:\/\/github.com\/Paul-Lez\/PersistentDecomp\/blob\/master\/\1)/' > docs/_includes/files_to_upstream.md
-          rm 1.txt 2.txt
+      - name: Copy README.md to website/index.md
+        run: cp README.md website/index.md
 
-      - name: Count sorries
-        run: python scripts/count_sorry.py
+      - name: Check PersistentDecomp.Mathlib only imports from Mathlib or PersistentDecomp.Mathlib
+        run: python3 scripts/check_mathlib_imports.py
+
+      - name: Upstreaming dashboard
+        run: |
+          mkdir -p website/_includes
+          python3 scripts/upstreaming_dashboard.py
 
       - name: Install elan
-        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.5.0
+        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.15.0
 
       - name: Get cache
         run: ~/.elan/bin/lake exe cache get || true
 
       - name: Build project
         run: ~/.elan/bin/lake build PersistentDecomp
 
-      - name: Cache mathlib docs
-        uses: actions/cache@v3
+      - name: File dependencies
+        run: |
+          sudo apt-get update
+          sudo apt install graphviz -y
+          ~/.elan/bin/lake exe graph website/file_deps.pdf
+
+      - name: Cache documentation
+        uses: actions/cache@v4
         with:
-          path: |
-            .lake/build/doc/Init
-            .lake/build/doc/Lake
-            .lake/build/doc/Lean
-            .lake/build/doc/Std
-            .lake/build/doc/Mathlib
-            .lake/build/doc/declarations
+          path: website/docs
           key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
-          restore-keys: |
-            MathlibDoc-
+          restore-keys: MathlibDoc-
 
       - name: Build documentation
-        run: ~/.elan/bin/lake -R -Kenv=dev build PersistentDecomp:docs
+        run: scripts/build_docs.sh
 
-      # - name: Build blueprint and copy to `docs/blueprint`
+      # - name: Build blueprint and copy to `website/blueprint`
       #   uses: xu-cheng/texlive-action@v2
       #   with:
-      #     docker_image: ghcr.io/xu-cheng/texlive-full:20231201
+      #     scheme: full
       #     run: |
       #       apk update
       #       apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
       #       git config --global --add safe.directory $GITHUB_WORKSPACE
       #       git config --global --add safe.directory `pwd`
-      #       python3 -m venv env
-      #       source env/bin/activate
-      #       pip install --upgrade pip requests wheel
-      #       pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
-      #       pip install leanblueprint
-      #       leanblueprint pdf
-      #       cp blueprint/print/print.pdf docs/blueprint.pdf
-      #       leanblueprint web
-      #       cp -r blueprint/web docs/blueprint
-
-      - name: Move documentation to `docs/docs`
+      #       python3 -m pip install --upgrade pip requests wheel
+      #       python3 -m pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
+      #       pip install -r blueprint/requirements.txt
+      #       python3 -m pip install invoke
+      #       inv all
+
+      - name: Copy documentation to `website/docs`
         run: |
-          mv .lake/build/doc docs/docs
+          mkdir -p website/docs
+          mv docs/build website/docs
 
       - name: Bundle dependencies
         uses: ruby/setup-ruby@v1
         with:
-          working-directory: docs
-          ruby-version: "3.0"  # Specify Ruby version
-          bundler-cache: true  # Enable caching for bundler
+          working-directory: website
+          ruby-version: "3.0" # Not needed with a .ruby-version file
+          bundler-cache: true # runs 'bundle install' and caches installed gems automatically
 
-      - name: Build website using Jekyll
-        working-directory: docs
-        run: JEKYLL_ENV=production bundle exec jekyll build  # Note this will also copy the blueprint and API doc into docs/_site
+      - name: Bundle website
+        working-directory: website
+        run: JEKYLL_ENV=production bundle exec jekyll build
 
       - name: Upload docs & blueprint artifact
-        uses: actions/upload-pages-artifact@v1
+        uses: actions/upload-pages-artifact@v3
         with:
-          path: docs/_site
+          path: website/_site
 
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v1
-
-      # - name: Check declarations
-      #   run: |
-      #       ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
+        uses: actions/deploy-pages@v4
 
       - name: Make sure the cache works
         run: |
-          mv docs/docs .lake/build/doc
+          mkdir -p docbuild/.lake/build/doc
+          mv website/docs docbuild/.lake/build/doc

docs/index.md

@@ -0,0 +1,52 @@
+# Build HTML documentation for add-combi
+# The output will be located in docs/build
+
+# Template lakefile.toml
+template() {
+  cat <<EOF
+name = "docbuild"
+reservoir = false
+version = "0.1.0"
+packagesDir = "../.lake/packages"
+
+[[require]]
+name = "PersistentDecomp"
+path = "../"
+
+[[require]]
+scope = "leanprover"
+name = "doc-gen4"
+rev = "TOOLCHAIN"
+EOF
+}
+
+# Create a temporary docbuild folder
+mkdir -p docbuild
+
+# Equip docbuild with the template lakefile.toml
+template > docbuild/lakefile.toml
+
+# Substitute the toolchain from lean-toolchain into docbuild/lakefile.toml
+sed -i s/TOOLCHAIN/`grep -oP 'v4\..*' lean-toolchain`/ docbuild/lakefile.toml
+
+# Fetch the docs cache if it exists
+mkdir -p website/docs
+mkdir -p docbuild/.lake/build/doc
+mv website/docs docbuild/.lake/build/doc
+
+# Initialise docbuild as a Lean project
+cd docbuild
+MATHLIB_NO_CACHE_ON_UPDATE=1 # Disable an error message due to a non-blocking bug. See Zulip
+~/.elan/bin/lake update PersistentDecomp
+~/.elan/bin/lake exe cache get
+
+# Build the docs
+~/.elan/bin/lake build PersistentDecomp:docs
+
+# Move them out of docbuild
+cd ../
+mkdir -p docs/build
+mv docbuild/.lake/build/doc docs/build
+
+# Clean up after ourselves
+rm -rf docbuild

scripts/build_docs.sh

@@ -0,0 +1,29 @@
+import os
+
+def list_files_by_type_recursive(folder_path, file_extension):
+    """Recursively lists all files in a folder and subfolders with the specified file extension."""
+    matching_files = []
+    for root, _, files in os.walk(folder_path):
+        matching_files.extend(os.path.join(root, f) for f in files if f.endswith(file_extension))
+    return matching_files
+
+folder = "PersistentDecomp/Mathlib"
+extension = ".lean"
+files = list_files_by_type_recursive(folder, extension)
+
+for file in files:
+    code = None
+    with open(file, "r") as reader:
+        code = reader.read()
+    lines = code.split("\n")
+    header = [line for line in lines if line.lstrip().startswith("import")]
+
+    for imp in header:
+        imp_file = imp.lstrip()[len("import"):].strip()
+        if (not imp_file.startswith("Mathlib.")) and \
+            (not imp_file.startswith("PersistentDecomp.Mathlib")):
+            raise OSError(f"""
+MathlibImportError: A file in PersistentDecomp.Mathlib imports a file not in Mathlib or PersistentDecomp.Mathlib
+\tImporting file: {file}
+\tImported file: {imp_file}
+""")