From 5cc4a320d14aa36557e85c4e7dd3cc803f94601a Mon Sep 17 00:00:00 2001
From: Niklas Halonen <niklas.halonen@protonmail.com>
Date: Thu, 18 Jul 2024 23:45:29 +0300
Subject: [PATCH] add tasks.py from
 https://github.com/YaelDillies/LeanAPAP/blob/master/tasks.py

---
 tasks.py | 91 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 91 insertions(+)
 create mode 100644 tasks.py

diff --git a/tasks.py b/tasks.py
new file mode 100644
index 0000000..cbf6c19
--- /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.')