From b0214df70b9c9400465958486820acc9f6f8f132 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Tue, 12 Dec 2023 21:22:08 +0100
Subject: [PATCH] Proper `tasks.py`

---
 blueprint/tasks.py | 27 ++++++++++++--
 tasks.py           | 91 ++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 115 insertions(+), 3 deletions(-)
 create mode 100644 tasks.py

diff --git a/blueprint/tasks.py b/blueprint/tasks.py
index 1be20012cca..e42fa942698 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()
@@ -37,9 +52,15 @@ def serve(ctx, random_port=False):
     Handler = http.server.SimpleHTTPRequestHandler
     if random_port:
         port = random.randint(8000, 8100)
-        print("Serving on port " + str(port))
     else:
         port = 8000
+
     httpd = socketserver.TCPServer(("", port), Handler)
-    httpd.serve_forever()
-    os.chdir(cwd)
+    try:
+        (ip, port) = httpd.server_address
+        ip = ip or 'localhost'
+        print(f'Serving http://{ip}:{port}/ ...')
+        httpd.serve_forever()
+    except KeyboardInterrupt:
+        pass
+    httpd.server_close()
diff --git a/tasks.py b/tasks.py
new file mode 100644
index 00000000000..cbf6c19051b
--- /dev/null
+++ b/tasks.py
@@ -0,0 +1,91 @@
+import os
+import shutil
+import subprocess
+from pathlib import Path
+from invoke import run, task
+import json
+import re
+
+from blueprint.tasks import web, bp, print_bp, serve
+
+ROOT = Path(__file__).parent
+BP_DIR = ROOT/'blueprint'
+PROJ = 'LeanAPAP'
+
+@task(bp, web)
+def all(ctx):
+    shutil.rmtree(ROOT/'docs'/'blueprint', ignore_errors=True)
+    shutil.copytree(ROOT/'blueprint'/'web', ROOT/'docs'/'blueprint')
+    shutil.copy2(ROOT/'blueprint'/'print'/'print.pdf', ROOT/'docs'/'blueprint.pdf')
+
+@task(web)
+def html(ctx):
+    shutil.rmtree(ROOT/'docs'/'blueprint', ignore_errors=True)
+    shutil.copytree(ROOT/'blueprint'/'web', ROOT/'docs'/'blueprint')
+
+@task(all)
+def dev(ctx):
+    """
+    Serve the blueprint website, rebuild PDF and the website on file changes
+    """
+
+    from watchfiles import run_process, DefaultFilter
+
+    def callback(changes):
+        print('Changes detected:', changes)
+        bp(ctx)
+        web(ctx)
+
+    run_process(BP_DIR/'src', target='inv serve', callback=callback,
+        watch_filter=DefaultFilter(
+            ignore_entity_patterns=(
+                '.*\.aux$',
+                '.*\.log$',
+                '.*\.fls$',
+                '.*\.fdb_latexmk$',
+                '.*\.bbl$',
+                '.*\.paux$',
+                '.*\.pdf$',
+                '.*\.out$',
+                '.*\.blg$',
+                '.*\.synctex.*$',
+            )
+        ))
+
+@task
+def check(ctx):
+    """
+    Check for broken references in blueprint to Lean declarations
+    """
+
+    broken_decls = []
+
+    DECLS_FILE = ROOT/'.lake/build/doc/declarations/declaration-data.bmp'
+    if not DECLS_FILE.exists():
+        print('[ERROR] Declarations file not found. Please run `lake -Kenv=dev build %s:docs` first.' % PROJ)
+        exit(1)
+
+    DEP_GRAPH_FILE = BP_DIR/'web/dep_graph_document.html'
+    if not DEP_GRAPH_FILE.exists():
+        print('[ERROR] Dependency graph file not found. Please run `inv all` (or only `inv web`) first.')
+        exit(1)
+
+    with open(DECLS_FILE) as f:
+        lean_decls = json.load(f)['declarations']
+
+    with open(DEP_GRAPH_FILE) as f:
+        lean_decl_regex = re.compile(r'lean_decl.*href=".*/find/#doc/([^"]+)"')
+        for line in f:
+            match = lean_decl_regex.search(line)
+            if match and match.lastindex == 1:
+                blueprint_decl = match[1]
+                if blueprint_decl not in lean_decls:
+                    broken_decls.append(blueprint_decl)
+
+    if broken_decls:
+        print('[WARN] The following Lean declarations are referenced in the blueprint but not in Lean:\n')
+        for decl in broken_decls:
+            print(decl)
+        exit(1)
+    else:
+        print('[OK] All Lean declarations referenced in the blueprint exist.')