Fix publish path

YaelDillies · Oct 23, 2023 · 3e396ae · 3e396ae
1 parent 4d23048
commit 3e396ae
Show file tree

Hide file tree

Showing 3 changed files with 87 additions and 74 deletions.
diff --git 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
@@ -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
@@ -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)