Upgrade blueprint to support Lean 4 (#2)

Per our discussion on [zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.204.20project.20blueprint/near/397963523), this PR upgrades blueprint to support Lean 4.

CI passed and blueprint and doc are published to https://utensil.github.io/LeanAPAP/.

Links to [Blueprint](https://utensil.github.io/LeanAPAP/blueprint/) or [Documentation](https://utensil.github.io/LeanAPAP/docs/) are working, and jumping from blueprint/depgragh to doc is also working (for theorems, because their names are all in lower case, unchanged from Lean 3 to Lean 4).

.github/workflows/push.yml

@@ -3,6 +3,12 @@ on:
     branches:
       - master
 
+# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
 jobs:
   build_project:
     runs-on: ubuntu-latest
@@ -11,6 +17,22 @@ jobs:
       group: ${{ github.workflow }}-${{ github.ref }}
       cancel-in-progress: true
     steps:
+      - name: Free Disk Space (Ubuntu)
+        uses: jlumbroso/free-disk-space@main
+        with:
+          # this might remove tools that are actually needed,
+          # if set to "true" but frees about 6 GB
+          tool-cache: false
+
+          # all of these default to true, but feel free to set to
+          # "false" if necessary for your workflow
+          android: true
+          dotnet: true
+          haskell: true
+          large-packages: true
+          docker-images: true
+          swap-storage: true
+
       - name: Checkout project
         uses: actions/checkout@v2
         with:
@@ -25,15 +47,47 @@ jobs:
       - name: Build project
         run: ~/.elan/bin/lake -Kenv=dev build LeanAPAP
 
+      - uses: actions/cache@v3
+        name: Mathlib doc Cache
+        with:
+          path: build/doc/Mathlib
+          key: DocGen4-${{ hashFiles('lake-manifest.json') }}
+          restore-keys: |
+            DocGen4-
+
       - name: Build documentation
         run: ~/.elan/bin/lake -Kenv=dev build LeanAPAP:docs
 
-      - name: Copy documentation
-        run: cp -R build/doc docs/
+      - name: Install Python
+        uses: actions/setup-python@v4
+        with:
+          python-version: '3.9'
+          cache: 'pip' # caching pip dependencies
+
+      - name: Install blueprint apt deps
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
+
+      - name: Install blueprint deps
+        run: |
+          cd blueprint && pip install -r requirements.txt
+
+      - name: Build blueprint and copy to `docs/blueprint`
+        run: |
+          inv all
+
+      - name: Copy documentation to `docs/docs`
+        run: |
+          mv build/doc docs/docs
 
       - name: Remove .gitignore for gh-pages
         run: rm docs/.gitignore
 
+      - name: Count sorries
+        run: |
+          python scripts/count_sorry.py
+
       - name: Bundle dependencies
         uses: ruby/setup-ruby@v1
         with:
@@ -45,9 +99,11 @@ jobs:
         working-directory: docs
         run: JEKYLL_ENV=production bundle exec jekyll build
 
-      - name: Deploy
-        uses: JamesIves/github-pages-[email protected]
+      - name: Upload doc & blueprint artifact
+        uses: actions/upload-pages-artifact@v1
         with:
-          SINGLE_COMMIT: true
-          BRANCH: gh-pages # The branch the action should deploy to.
-          FOLDER: docs/_site
+          path: docs/_site
+
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v1

.gitignore

@@ -13,3 +13,4 @@ src/list_decls.lean
 src/.noisy_files
 /build
 /lake-packages/*
+docs/_includes/sorries.md

blueprint/requirements.txt

@@ -0,0 +1,4 @@
+invoke==1.7.1
+plasTeX @ git+https://github.com/plastex/plastex.git
+leanblueprint @ git+https://github.com/utensil/leanblueprint.git@lean4-only
+watchfiles==0.16.1

blueprint/src/macros_common.tex

@@ -16,4 +16,6 @@
 \newcommand{\norm}[1]{\lVert #1\rVert}
 \providecommand{\tup}[1]{{\vec{#1}}}
 \newcommand{\lo}[1]{\mathcal{L}{#1}}
-\newcommand{\inn}[1]{\left\langle #1 \right\rangle}
+\newcommand{\inn}[1]{\left\langle #1 \right\rangle}
+\newcommand{\C}{\mathbb{C}}
+\newcommand{\E}{\mathbb{E}}

blueprint/src/web.tex

@@ -15,6 +15,7 @@
 
 %\home{https://github.com/YaelDillies/LeanAPAP/}
 \github{https://github.com/YaelDillies/LeanAPAP/}
+\dochome{https://YaelDillies.github.io/LeanAPAP/docs}
 
 \title{LeanAPAP}
 \author{LeanAPAP project contributors}

blueprint/tasks.py

@@ -23,6 +23,21 @@ def bp(ctx):
     run('cd src && xelatex -output-directory=../print print.tex')
     os.chdir(cwd)
 
+@task
+def bptt(ctx):
+    """
+    Build the blueprint PDF file with tectonic and prepare src/web.bbl for task `web`
+
+    NOTE: install tectonic by running `curl --proto '=https' --tlsv1.2 -fsSL https://drop-sh.fullyjustified.net |sh` in
+    `~/.local/bin/`
+    """
+
+    cwd = os.getcwd()
+    os.chdir(BP_DIR)
+    run('mkdir -p print && cd src && tectonic -Z shell-escape-cwd=. --keep-intermediates --outdir ../print print.tex')
+    # run('cp print/print.bbl src/web.bbl')
+    os.chdir(cwd)
+
 @task
 def web(ctx):
     cwd = os.getcwd()

scripts/count_sorry.py

@@ -12,7 +12,7 @@ def pretty_file(file: str):
     url = f"https://github.com/YaelDillies/LeanAPAP/blob/master/{file}"
     return f"[{name}]({url})"
 
-files = [file for tree in os.walk("src") for file in glob(os.path.join(tree[0], '*.lean'))]
+files = [file for tree in os.walk("LeanAPAP") for file in glob(os.path.join(tree[0], '*.lean'))]
 sorries = {}
 
 for file in files:

tasks.py

@@ -4,18 +4,11 @@
 from pathlib import Path
 from invoke import run, task
 
-from mathlibtools.lib import LeanProject
-
 from blueprint.tasks import web, bp, print_bp, serve
 
 ROOT = Path(__file__).parent
 
-@task
-def decls(ctx):
-    proj = LeanProject.from_path(ROOT)
-    proj.pickle_decls(ROOT/'decls.pickle')
-
-@task(decls, bp, web)
+@task(bp, web)
 def all(ctx):
     shutil.rmtree(ROOT/'docs'/'blueprint', ignore_errors=True)
     shutil.copytree(ROOT/'blueprint'/'web', ROOT/'docs'/'blueprint')
@@ -25,68 +18,3 @@ def all(ctx):
 def html(ctx):
     shutil.rmtree(ROOT/'docs'/'blueprint', ignore_errors=True)
     shutil.copytree(ROOT/'blueprint'/'web', ROOT/'docs'/'blueprint')
-
-@task
-def doc(ctx):
-    print("Making all.lean")
-    subprocess.run(["bash", "mk_all.sh"], cwd = "scripts", check=True)
-
-    print("Downloading doc-gen")
-    if os.path.exists("doc-gen"):
-        subprocess.run(["git", "fetch"], check=True, cwd="doc-gen")
-        subprocess.run(["git", "reset", "--hard", "origin/master"], check=True, cwd="doc-gen")
-    else:
-        subprocess.run(["git", "clone", "https://github.com/leanprover-community/doc-gen.git"],
-            check=True)
-
-    files = ["src/entrypoint.lean", "src/export_json.lean", "src/lean_commit.lean",
-        "color_scheme.js", "nav.js", "pygments-dark.css", "pygments.css", "search.js",
-        "STIXlicense.txt", "STIXTwoMath.woff2", "style.css"]
-    folders = ["static", "templates", "test"]
-
-    print("Copying over doc-gen files")
-    import shutil
-    for file in files:
-        shutil.copyfile("doc-gen/" + file, file)
-    for folder in folders:
-        shutil.copytree("doc-gen/" + folder, folder, dirs_exist_ok=True)
-
-    print("Compiling documentation generator")
-    subprocess.run(["lean", "--make", "src/entrypoint.lean"], check=True)
-    with open("export.json", "w") as f:
-        print("Generating documentation")
-        subprocess.run(["lean", "--run", "src/entrypoint.lean"], stdout=f, check=True)
-
-    print("Printing documentation to HTML")
-    import sys
-    sys.argv = [sys.argv[0], "-w", "https://YaelDillies.github.io/LeanAPAP/docs/"]
-    sys.path.insert(0, "doc-gen")
-    import print_docs
-    del print_docs.extra_doc_files[:]
-    print_docs.copy_yaml_bib_files = lambda p: None
-    print_docs.library_link_roots['LeanAPAP'] = 'https://github.com/YaelDillies/LeanAPAP/blob/master/src/'
-    print_docs.main()
-
-    print("Cleaning up doc-gen files")
-    os.remove("export.json")
-    for file in files:
-        os.remove(file)
-    for folder in folders:
-        shutil.rmtree(folder)
-
-    shutil.rmtree(ROOT/'docs'/'docs', ignore_errors=True)
-    shutil.move(ROOT/'html', ROOT/'docs'/'docs')
-
-# Continuous integration task.
-@task
-def ci(ctx):
-    env = os.environ.copy()
-    env["PATH"] = env["HOME"] + "/.elan/bin:" + env["PATH"]
-    subprocess.run(["ls", "-lah"], env=env, check=True)
-    subprocess.run(["git", "config", "--global", "--add", "safe.directory", "/src"],
-        env=env, check=True)
-    subprocess.run(["leanproject", "get-mathlib-cache"], env=env, check=True)
-    subprocess.run(["leanproject", "build"], env=env, check=True)
-    # Call these tasks afterwards.
-    subprocess.run(["inv", "all", "html", "doc"], env=env, check=True)
-    subprocess.run(["python3", "scripts/count_sorry.py"], env=env, check=True)