diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index ebcd6353f5..e3c249bc70 100644 --- a/.github/workflows/push.yml +++ b/.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-deploy-action@3.7.1 + - 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 diff --git a/.gitignore b/.gitignore index 37d7aa5bb9..8ea77f27af 100644 --- a/.gitignore +++ b/.gitignore @@ -13,3 +13,4 @@ src/list_decls.lean src/.noisy_files /build /lake-packages/* +docs/_includes/sorries.md diff --git a/blueprint/requirements.txt b/blueprint/requirements.txt new file mode 100644 index 0000000000..3bdadebfc4 --- /dev/null +++ b/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 diff --git a/blueprint/src/macros_common.tex b/blueprint/src/macros_common.tex index 27861d532f..4de2270627 100644 --- a/blueprint/src/macros_common.tex +++ b/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} \ No newline at end of file +\newcommand{\inn}[1]{\left\langle #1 \right\rangle} +\newcommand{\C}{\mathbb{C}} +\newcommand{\E}{\mathbb{E}} diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex index 4b9c0b9000..96c223ed35 100644 --- a/blueprint/src/web.tex +++ b/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} diff --git a/blueprint/tasks.py b/blueprint/tasks.py index 1be20012cc..23807328a4 100644 --- a/blueprint/tasks.py +++ b/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() diff --git a/scripts/count_sorry.py b/scripts/count_sorry.py index 466f444017..cd7735ec7c 100644 --- a/scripts/count_sorry.py +++ b/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: diff --git a/tasks.py b/tasks.py index bae65ce836..a33272950b 100644 --- a/tasks.py +++ b/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)