diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 08709d0eb0..e3c249bc70 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -73,15 +73,13 @@ jobs: run: | cd blueprint && pip install -r requirements.txt - - name: Build blueprint + - name: Build blueprint and copy to `docs/blueprint` run: | - cd blueprint && inv all + inv all - - name: Copy documentation + - name: Copy documentation to `docs/docs` run: | - cp -R build/doc docs/ - mkdir -p docs/_site - mv blueprint/web docs/_site/blueprint + mv build/doc docs/docs - name: Remove .gitignore for gh-pages run: rm docs/.gitignore diff --git a/blueprint/tasks.py b/blueprint/tasks.py index 717957d86e..0a8b433ec5 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() @@ -44,10 +59,10 @@ def serve(ctx, random_port=False): httpd.serve_forever() os.chdir(cwd) -@task(bp, web) -def all(ctx): - """ - Run all tasks: `bp`, and `web` - """ +# @task(bp, web) +# def all(ctx): +# """ +# Run all tasks: `bp`, and `web` +# """ - pass +# pass diff --git a/tasks.py b/tasks.py index bae65ce836..f272cf4ed4 100644 --- a/tasks.py +++ b/tasks.py @@ -4,18 +4,18 @@ from pathlib import Path from invoke import run, task -from mathlibtools.lib import LeanProject +# 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 +# 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') @@ -26,67 +26,67 @@ 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) +# @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) +# 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"] +# 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("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("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("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) +# 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') +# 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) +# # 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)