From 57524f299c7934010ca7d6d940ae1d8a1ae8900a Mon Sep 17 00:00:00 2001 From: Fabian Gloeckle Date: Fri, 13 Mar 2026 06:47:57 -0700 Subject: [PATCH 1/2] Add side-by-side layout: TeX content left, Lean declarations right Introduce a two-column layout for blueprint pages that displays the LaTeX theorem content on the left and the corresponding Lean doc-gen declarations (statements, equations, structure fields) in a side panel on the right. Key changes: - blueprint.py: Add functions to load and parse doc-gen4 declaration data (load_docgen_declarations, parse_docgen_statement) and extract HTML/plain-text for declaration headers, equations, and structure fields. Add rewrite_lean_links() Jinja2 filter that rewrites doc-gen links at render time: links to declarations present in the blueprint point to the blueprint URL, while others point to the project's doc-gen docs. - blueprint.jinja2s: Add a thmenv template that supports injecting extra header content (thm_header_extras_tpl, thm_header_hidden_extras_tpl) and a right-side panel (thm_side_panel_tpl) next to each theorem environment wrapper. - blueprint.css: Add ~490 lines of CSS for the two-column CSS Grid layout. Theorem wrappers span both columns with their own internal grid. Includes responsive fallback to single-column on smaller screens, wider TOC sidebar, and styling for Lean declaration headers, equations, structure fields, and link types. - _config.yml: Fix baseurl to use the project name subpath so GitHub Pages serves the site at the correct URL. --- leanblueprint/Packages/blueprint.py | 681 ++++++++++++++---- .../renderer_templates/blueprint.jinja2s | 55 ++ leanblueprint/jekyll_templates/_config.yml | 4 +- leanblueprint/static/blueprint.css | 488 +++++++++++++ 4 files changed, 1089 insertions(+), 139 deletions(-) diff --git a/leanblueprint/Packages/blueprint.py b/leanblueprint/Packages/blueprint.py index dc83348..4f99363 100644 --- a/leanblueprint/Packages/blueprint.py +++ b/leanblueprint/Packages/blueprint.py @@ -11,6 +11,9 @@ You can also add options that will be passed to the dependency graph package. """ + +import json +import re import string from pathlib import Path @@ -23,52 +26,294 @@ log = getLogger() PKG_DIR = Path(__file__).parent -STATIC_DIR = Path(__file__).parent.parent/'static' +STATIC_DIR = Path(__file__).parent.parent / "static" + + +def rewrite_lean_links(html_str: str, document) -> str: + """Jinja2 filter to rewrite doc-gen links at render time. + + - Links to declarations in the blueprint → blueprint URL (using node.url) + - Links not in blueprint → project dochome + """ + lean_to_node = document.userdata.get("lean_to_blueprint_node", {}) + project_dochome = document.userdata.get( + "project_dochome_for_links", + "https://leanprover-community.github.io/mathlib4_docs", + ) + project_dochome = project_dochome.rstrip("/") + + def replace_link(match): + href = match.group(1) + link_text = match.group(2) + + # Extract the Lean declaration name from the href + hash_match = re.search(r'#([^"]+)', href) + if hash_match: + lean_name = hash_match.group(1) + + # Check if in blueprint + if lean_name in lean_to_node: + node = lean_to_node[lean_name] + # At render time, node.url should be available + try: + node_url = node.url + if node_url: + return f'{link_text}' + except Exception: + pass + + # Not in blueprint - rewrite to dochome + if href.startswith("./"): + new_href = project_dochome + href[1:] + elif href.startswith("../"): + path = href + while path.startswith("../"): + path = path[3:] + new_href = f"{project_dochome}/{path}" + else: + new_href = href + + return f'{link_text}' + + # Match ... patterns + return re.sub( + r']*href="([^"]*)"[^>]*>(.*?)', replace_link, html_str, flags=re.DOTALL + ) + + +def load_docgen_declarations(document) -> dict: + """Load declaration data from doc-gen4 declaration-data.bmp.""" + search_paths = [ + document.userdata.get("docgen_declarations_path"), + "../docbuild/.lake/build/doc/declarations/declaration-data.bmp", + "../../docbuild/.lake/build/doc/declarations/declaration-data.bmp", + ] + working_dir = Path(document.userdata.get("working-dir", ".")) + + for rel_path in search_paths: + if rel_path is None: + continue + full_path = working_dir / rel_path + if full_path.exists(): + try: + data = json.loads(full_path.read_text()) + return data.get("declarations", {}) + except Exception as e: + log.warning(f"Failed to parse {full_path}: {e}") + return {} + + +def parse_docgen_statement(html_path: Path, decl_name: str) -> dict: + """Parse the Lean statement, equation, and structure fields from a doc-gen HTML file. + + Returns a dict with keys: + - statement_text: plain text of the declaration header + - equation_text: plain text of equations (for defs) + - statement_html: HTML of the declaration header + - equation_html: HTML of equations (for defs) + - fields_html: HTML of structure fields (for structures) + - fields_text: plain text of structure fields (for structures) + + Links are kept as-is - they will be rewritten at render time by a Jinja2 filter. + """ + result = { + "statement_text": "", + "equation_text": "", + "statement_html": "", + "equation_html": "", + "fields_html": "", + "fields_text": "", + } + + if not html_path.exists(): + return result + + try: + content = html_path.read_text() + + # Find the specific declaration block + start_pattern = rf'
' + start_match = re.search(start_pattern, content) + if not start_match: + return result + + start_pos = start_match.end() + + # Find where this declaration ends - look for next declaration or mod_doc + end_pattern = r'
' + header_start_match = re.search(header_start_pattern, decl_html) + if header_start_match: + # Find the matching closing
by counting nested divs + start_idx = header_start_match.end() + depth = 1 + pos = start_idx + while depth > 0 and pos < len(decl_html): + next_open = decl_html.find("", pos) + if next_close == -1: + break + if next_open != -1 and next_open < next_close: + depth += 1 + pos = next_open + 4 + else: + depth -= 1 + if depth == 0: + raw_header = decl_html[start_idx:next_close] + result["statement_html"] = ( + f'
{raw_header}
' + ) + # Also extract plain text version as fallback + header_text = raw_header + header_text = re.sub( + r'.*?', "", header_text + ) + header_text = re.sub( + r'.*?', "", header_text + ) + header_text = re.sub( + r']*class="break_within"[^>]*>.*?', "", header_text + ) + header_text = re.sub(r"]*>", "", header_text) + header_text = re.sub(r"", "", header_text) + header_text = re.sub(r"]*>", "", header_text) + header_text = re.sub(r"", "", header_text) + header_text = re.sub( + r'
', " : ", header_text + ) + header_text = re.sub(r"
", "", header_text) + header_text = re.sub(r"<[^>]+>", "", header_text) + header_text = re.sub(r"\s+", " ", header_text).strip() + header_text = re.sub(r"^[\s.]+", "", header_text) + header_text = re.sub(r":\s*:", ":", header_text) + result["statement_text"] = header_text + pos = next_close + 6 + + # Extract equation from Equations details block - only within THIS declaration + eq_pattern = r'
Equations
    (.*?)
' + eq_match = re.search(eq_pattern, decl_html, re.DOTALL) + if eq_match: + eq_html = eq_match.group(1) + + # Keep links as-is for render-time rewriting + result["equation_html"] = ( + f'
    {eq_html}
' + ) + + # Also create plain text version + eq_html_clean = re.sub(r"]*>", "", eq_html) + eq_html_clean = re.sub(r"", "", eq_html_clean) + eq_html_clean = re.sub(r"]*>", "", eq_html_clean) + eq_html_clean = re.sub(r"", "", eq_html_clean) + eq_html_clean = re.sub(r'
  • ', "", eq_html_clean) + eq_html_clean = re.sub(r"
    • ", "\n", eq_html_clean) + eq_html_clean = re.sub(r"<[^>]+>", "", eq_html_clean) + eq_html_clean = re.sub(r"\s+", " ", eq_html_clean).strip() + result["equation_text"] = eq_html_clean + + # Extract structure fields from structure_fields ul - only within THIS declaration + fields_pattern = r'
      ]*>(.*?)
    ' + fields_match = re.search(fields_pattern, decl_html, re.DOTALL) + if fields_match: + fields_html = fields_match.group(1) + + # Keep links as-is for render-time rewriting + result["fields_html"] = ( + f'
      {fields_html}
    ' + ) + + # Also create plain text version + fields_text_parts = [] + field_pattern = r']*class="structure_field"[^>]*>.*?
    (.*?)
    ' + for field_match in re.finditer(field_pattern, fields_html, re.DOTALL): + field_info = field_match.group(1) + # Strip HTML tags for plain text + field_text = re.sub(r"<[^>]+>", "", field_info) + field_text = re.sub(r"\s+", " ", field_text).strip() + if field_text: + fields_text_parts.append(field_text) + result["fields_text"] = "\n".join(fields_text_parts) + + return result + except Exception as e: + log.warning(f"Failed to parse statement from {html_path}: {e}") + return result + + +def get_docgen_base_path(document) -> Path: + """Get the base path for doc-gen HTML files.""" + search_paths = [ + "../docbuild/.lake/build/doc", + "../../docbuild/.lake/build/doc", + ] + working_dir = Path(document.userdata.get("working-dir", ".")) + + for rel_path in search_paths: + full_path = working_dir / rel_path + if full_path.exists(): + return full_path + return None class home(Command): r"""\home{url}""" - args = 'url:url' + + args = "url:url" def invoke(self, tex): Command.invoke(self, tex) - self.ownerDocument.userdata['project_home'] = self.attributes['url'] + self.ownerDocument.userdata["project_home"] = self.attributes["url"] return [] class github(Command): r"""\github{url}""" - args = 'url:url' + + args = "url:url" def invoke(self, tex): Command.invoke(self, tex) - self.ownerDocument.userdata['project_github'] = self.attributes['url'].textContent.rstrip( - '/') + self.ownerDocument.userdata["project_github"] = self.attributes[ + "url" + ].textContent.rstrip("/") return [] class dochome(Command): r"""\dochome{url}""" - args = 'url:url' + + args = "url:url" def invoke(self, tex): Command.invoke(self, tex) - self.ownerDocument.userdata['project_dochome'] = self.attributes['url'].textContent + self.ownerDocument.userdata["project_dochome"] = self.attributes[ + "url" + ].textContent return [] class graphcolor(Command): r"""\graphcolor{node_type}{color}{color_descr}""" - args = 'node_type:str color:str color_descr:str' + + args = "node_type:str color:str color_descr:str" def digest(self, tokens): Command.digest(self, tokens) attrs = self.attributes - colors = self.ownerDocument.userdata['dep_graph']['colors'] - node_type = attrs['node_type'] + colors = self.ownerDocument.userdata["dep_graph"]["colors"] + node_type = attrs["node_type"] if node_type not in colors: - log.warning(f'Unknown node type {node_type}') - colors[node_type] = (attrs['color'].strip(), attrs['color_descr'].strip()) + log.warning(f"Unknown node type {node_type}") + colors[node_type] = (attrs["color"].strip(), attrs["color_descr"].strip()) class leanok(Command): @@ -76,7 +321,23 @@ class leanok(Command): def digest(self, tokens): Command.digest(self, tokens) - self.parentNode.userdata['leanok'] = True + self.parentNode.userdata["leanok"] = True + + +class leantarget(Command): + r"""\leantarget - marks this theorem/definition as a main target result""" + + def digest(self, tokens): + Command.digest(self, tokens) + self.parentNode.userdata["leantarget"] = True + + +class leanhelper(Command): + r"""\leanhelper - marks this theorem/lemma as a helper/auxiliary result""" + + def digest(self, tokens): + Command.digest(self, tokens) + self.parentNode.userdata["leanhelper"] = True class notready(Command): @@ -84,7 +345,7 @@ class notready(Command): def digest(self, tokens): Command.digest(self, tokens) - self.parentNode.userdata['notready'] = True + self.parentNode.userdata["notready"] = True class mathlibok(Command): @@ -92,58 +353,109 @@ class mathlibok(Command): def digest(self, tokens): Command.digest(self, tokens) - self.parentNode.userdata['leanok'] = True - self.parentNode.userdata['mathlibok'] = True + self.parentNode.userdata["leanok"] = True + self.parentNode.userdata["mathlibok"] = True class lean(Command): - r"""\lean{decl list} """ - args = 'decls:list:nox' + r"""\lean{decl list}""" + + args = "decls:list:nox" def digest(self, tokens): Command.digest(self, tokens) - decls = [dec.strip() for dec in self.attributes['decls']] - self.parentNode.setUserData('leandecls', decls) - all_decls = self.ownerDocument.userdata.setdefault('lean_decls', []) + decls = [dec.strip() for dec in self.attributes["decls"]] + self.parentNode.setUserData("leandecls", decls) + all_decls = self.ownerDocument.userdata.setdefault("lean_decls", []) all_decls.extend(decls) class discussion(Command): - r"""\discussion{issue_number} """ - args = 'issue:str' + r"""\discussion{issue_number}""" + + args = "issue:str" def digest(self, tokens): Command.digest(self, tokens) self.parentNode.setUserData( - 'issue', self.attributes['issue'].lstrip('#').strip()) + "issue", self.attributes["issue"].lstrip("#").strip() + ) -CHECKMARK_TPL = Template(""" +CHECKMARK_TPL = Template( + """ {% if obj.userdata.leanok and ('proved_by' not in obj.userdata or obj.userdata.proved_by.userdata.leanok ) %} ✓ {% endif %} -""") - -LEAN_DECLS_TPL = Template(""" - {% if obj.userdata.leandecls %} - - {% call modal('Lean declarations') %} -
      - {% for lean, url in obj.userdata.lean_urls %} -
    • {{ lean }}
      • - {% endfor %} -
    - {% endcall %} +""" +) + +LEAN_SIDE_PANEL_TPL = Template( + """ +{% if obj.userdata.lean_entries %} +{% set has_content = [] %} +{% for entry in obj.userdata.lean_entries %} +{% if entry.statement_html or entry.statement %}{% if has_content.append(1) %}{% endif %}{% endif %} +{% endfor %} +{% if has_content %} +
    + {% for entry in obj.userdata.lean_entries %} + {% if entry.statement_html or entry.statement %} +
    + {% if entry.statement_html %} +
    +
    + docs + {% if entry.github_url %}source{% endif %} +
    + {{ doc.userdata.rewrite_lean_links_fn(entry.statement_html, doc) | safe }} + {% if entry.fields_html %} + {{ doc.userdata.rewrite_lean_links_fn(entry.fields_html, doc) | safe }} + {% elif entry.fields_text %} + 
    {{ entry.fields_text }}
    + {% endif %} + {% if entry.equation_html %} + {{ doc.userdata.rewrite_lean_links_fn(entry.equation_html, doc) | safe }} + {% elif entry.equation %} + 
    {{ entry.equation }}
    + {% endif %} +
    + {% elif entry.statement %} +
    + {{ entry.short_name }} + {% if entry.github_url %}📄{% endif %} +
    + 
    {{ entry.statement }}
    + {% if entry.fields_html %} + {{ doc.userdata.rewrite_lean_links_fn(entry.fields_html, doc) | safe }} + {% elif entry.fields_text %} + 
    {{ entry.fields_text }}
    + {% endif %} + {% if entry.equation_html %} + {{ doc.userdata.rewrite_lean_links_fn(entry.equation_html, doc) | safe }} + {% elif entry.equation %} + 
    {{ entry.equation }}
    + {% endif %} {% endif %} -""") +
    + {% endif %} + {% endfor %} +
    +{% endif %} +{% endif %} +""" +) -GITHUB_ISSUE_TPL = Template(""" +GITHUB_ISSUE_TPL = Template( + """ {% if obj.userdata.issue %} Discussion {% endif %} -""") +""" +) -LEAN_LINKS_TPL = Template(""" +LEAN_LINKS_TPL = Template( + """ {% if thm.userdata['lean_urls'] -%} {%- if thm.userdata['lean_urls']|length > 1 -%}
    @@ -158,13 +470,16 @@ def digest(self, tokens): Lean {%- endif -%} {%- endif -%} -""") +""" +) -GITHUB_LINK_TPL = Template(""" +GITHUB_LINK_TPL = Template( + """ {% if thm.userdata['issue'] -%} Discussion {%- endif -%} -""") +""" +) def ProcessOptions(options, document): @@ -175,23 +490,26 @@ def ProcessOptions(options, document): # This is a bit hacky but needed for backward compatibility with # project who used the blueprint package before the depgraph one was # split. - plugins = document.config['general'].data['plugins'].value - if 'plastexdepgraph' not in plugins: - plugins.append('plastexdepgraph') + plugins = document.config["general"].data["plugins"].value + if "plastexdepgraph" not in plugins: + plugins.append("plastexdepgraph") # And now load the package. - document.context.loadPythonPackage(document, 'depgraph', options) - if 'showmore' in options: - if 'plastexshowmore' not in plugins: - plugins.append('plastexshowmore') + document.context.loadPythonPackage(document, "depgraph", options) + if "showmore" in options: + if "plastexshowmore" not in plugins: + plugins.append("plastexshowmore") # And now load the package. - document.context.loadPythonPackage(document, 'showmore', {}) + document.context.loadPythonPackage(document, "showmore", {}) - templatedir = PackageTemplateDir(path=PKG_DIR/'renderer_templates') + templatedir = PackageTemplateDir(path=PKG_DIR / "renderer_templates") document.addPackageResource(templatedir) - jobname = document.userdata['jobname'] - outdir = document.config['files']['directory'] - outdir = string.Template(outdir).substitute({'jobname': jobname}) + # Register the link rewriting function for use in templates + document.userdata["rewrite_lean_links_fn"] = rewrite_lean_links + + jobname = document.userdata["jobname"] + outdir = document.config["files"]["directory"] + outdir = string.Template(outdir).substitute({"jobname": jobname}) def make_lean_data() -> None: """ @@ -199,125 +517,214 @@ def make_lean_data() -> None: Also create the file lean_decls of all Lean names referred to in the blueprint. """ - project_dochome = document.userdata.get('project_dochome', - 'https://leanprover-community.github.io/mathlib4_docs') + project_dochome = document.userdata.get( + "project_dochome", "https://leanprover-community.github.io/mathlib4_docs" + ) + project_github = document.userdata.get("project_github", "") + + # Load doc-gen data + docgen_decls = load_docgen_declarations(document) + docgen_base = get_docgen_base_path(document) + + # Build mapping from Lean names to blueprint nodes + # URLs will be resolved at render time when node.url is available + lean_to_node = {} + for graph in document.userdata["dep_graph"]["graphs"].values(): + for node in graph.nodes: + leandecls = node.userdata.get("leandecls", []) + for leandecl in leandecls: + lean_to_node[leandecl] = node + + # Store the mapping and dochome in document for access during rendering + document.userdata["lean_to_blueprint_node"] = lean_to_node + document.userdata["project_dochome_for_links"] = project_dochome - for graph in document.userdata['dep_graph']['graphs'].values(): + for graph in document.userdata["dep_graph"]["graphs"].values(): nodes = graph.nodes for node in nodes: - leandecls = node.userdata.get('leandecls', []) + leandecls = node.userdata.get("leandecls", []) lean_urls = [] + lean_entries = [] for leandecl in leandecls: lean_urls.append( - (leandecl, - f'{project_dochome}/find/#doc/{leandecl}')) - - node.userdata['lean_urls'] = lean_urls - - used = node.userdata.get('uses', []) - node.userdata['can_state'] = all(thm.userdata.get('leanok') - for thm in used) and not node.userdata.get('notready', False) - proof = node.userdata.get('proved_by') + (leandecl, f"{project_dochome}/find/#doc/{leandecl}") + ) + + # Build lean_entries with docgen data + decl_info = docgen_decls.get(leandecl, {}) + doc_link = decl_info.get("docLink", "").lstrip("./") + + # Parse statement and equation from doc-gen HTML if available + # Links are kept as relative - will be rewritten at render time + statement = "" + equation = "" + statement_html = "" + equation_html = "" + fields_html = "" + fields_text = "" + if docgen_base and doc_link: + html_file = doc_link.split("#")[0] + html_path = docgen_base / html_file + parsed = parse_docgen_statement(html_path, leandecl) + statement = parsed["statement_text"] + equation = parsed["equation_text"] + statement_html = parsed["statement_html"] + equation_html = parsed["equation_html"] + fields_html = parsed["fields_html"] + fields_text = parsed["fields_text"] + + # Get short name (last component) + short_name = leandecl.split(".")[-1] + + entry = { + "name": leandecl, + "short_name": short_name, + "kind": decl_info.get("kind", ""), + "doc_url": f"{project_dochome}/{doc_link}", + "statement": statement, + "equation": equation, + "statement_html": statement_html, + "equation_html": equation_html, + "fields_html": fields_html, + "fields_text": fields_text, + } + # GitHub URL from docLink path + if project_github and doc_link: + module_path = doc_link.split("#")[0].replace(".html", ".lean") + entry["github_url"] = ( + f"{project_github}/blob/summary/{module_path}" + ) + lean_entries.append(entry) + + node.userdata["lean_urls"] = lean_urls + node.userdata["lean_entries"] = lean_entries + + used = node.userdata.get("uses", []) + node.userdata["can_state"] = all( + thm.userdata.get("leanok") for thm in used + ) and not node.userdata.get("notready", False) + proof = node.userdata.get("proved_by") if proof: - used.extend(proof.userdata.get('uses', [])) - node.userdata['can_prove'] = all(thm.userdata.get('leanok') - for thm in used) - node.userdata['proved'] = proof.userdata.get( - 'leanok', False) + used.extend(proof.userdata.get("uses", [])) + node.userdata["can_prove"] = all( + thm.userdata.get("leanok") for thm in used + ) + node.userdata["proved"] = proof.userdata.get("leanok", False) else: - node.userdata['can_prove'] = False - node.userdata['proved'] = False + node.userdata["can_prove"] = False + node.userdata["proved"] = False for node in nodes: - node.userdata['fully_proved'] = all(n.userdata.get('proved', False) or item_kind( - n) == 'definition' for n in graph.ancestors(node).union({node})) + node.userdata["fully_proved"] = all( + n.userdata.get("proved", False) or item_kind(n) == "definition" + for n in graph.ancestors(node).union({node}) + ) - lean_decls_path = Path(document.userdata['working-dir']).parent/"lean_decls" + lean_decls_path = Path(document.userdata["working-dir"]).parent / "lean_decls" lean_decls_path.write_text("\n".join(document.userdata.get("lean_decls", []))) document.addPostParseCallbacks(150, make_lean_data) - document.addPackageResource([PackageCss(path=STATIC_DIR/'blueprint.css')]) - - colors = document.userdata['dep_graph']['colors'] = { - 'mathlib': ('darkgreen', 'Dark green'), - 'stated': ('green', 'Green'), - 'can_state': ('blue', 'Blue'), - 'not_ready': ('#FFAA33', 'Orange'), - 'proved': ('#9CEC8B', 'Green'), - 'can_prove': ('#A3D6FF', 'Blue'), - 'defined': ('#B0ECA3', 'Light green'), - 'fully_proved': ('#1CAC78', 'Dark green') + document.addPackageResource([PackageCss(path=STATIC_DIR / "blueprint.css")]) + + colors = document.userdata["dep_graph"]["colors"] = { + "mathlib": ("darkgreen", "Dark green"), + "stated": ("green", "Green"), + "can_state": ("blue", "Blue"), + "not_ready": ("#FFAA33", "Orange"), + "proved": ("#9CEC8B", "Green"), + "can_prove": ("#A3D6FF", "Blue"), + "defined": ("#B0ECA3", "Light green"), + "fully_proved": ("#1CAC78", "Dark green"), } def colorizer(node) -> str: data = node.userdata - color = '' - if data.get('mathlibok'): - color = colors['mathlib'][0] - elif data.get('leanok'): - color = colors['stated'][0] - elif data.get('can_state'): - color = colors['can_state'][0] - elif data.get('notready'): - color = colors['not_ready'][0] + color = "" + if data.get("mathlibok"): + color = colors["mathlib"][0] + elif data.get("leanok"): + color = colors["stated"][0] + elif data.get("can_state"): + color = colors["can_state"][0] + elif data.get("notready"): + color = colors["not_ready"][0] return color def fillcolorizer(node) -> str: data = node.userdata - stated = data.get('leanok') - can_state = data.get('can_state') - can_prove = data.get('can_prove') - proved = data.get('proved') - fully_proved = data.get('fully_proved') + stated = data.get("leanok") + can_state = data.get("can_state") + can_prove = data.get("can_prove") + proved = data.get("proved") + fully_proved = data.get("fully_proved") - fillcolor = '' + fillcolor = "" if proved: - fillcolor = colors['proved'][0] + fillcolor = colors["proved"][0] elif can_prove and (can_state or stated): - fillcolor = colors['can_prove'][0] - if item_kind(node) == 'definition': + fillcolor = colors["can_prove"][0] + if item_kind(node) == "definition": if stated: - fillcolor = colors['defined'][0] + fillcolor = colors["defined"][0] elif can_state: - fillcolor = colors['can_prove'][0] + fillcolor = colors["can_prove"][0] elif fully_proved: - fillcolor = colors['fully_proved'][0] + fillcolor = colors["fully_proved"][0] return fillcolor - document.userdata['dep_graph']['colorizer'] = colorizer - document.userdata['dep_graph']['fillcolorizer'] = fillcolorizer + document.userdata["dep_graph"]["colorizer"] = colorizer + document.userdata["dep_graph"]["fillcolorizer"] = fillcolorizer def make_legend() -> None: """ Extend the dependency graph legend defined by the depgraph plugin by adding information specific to Lean blueprints. This is registered - as a post-parse callback to allow users to redefine colors and their + as a post-parse callback to allow users to redefine colors and their descriptions. """ - document.userdata['dep_graph']['legend'].extend([ - (f"{document.userdata['dep_graph']['colors']['can_state'][1]} border", - "the statement of this result is ready to be formalized; all prerequisites are done"), - (f"{document.userdata['dep_graph']['colors']['not_ready'][1]} border", - "the statement of this result is not ready to be formalized; the blueprint needs more work"), - (f"{document.userdata['dep_graph']['colors']['can_state'][1]} background", - "the proof of this result is ready to be formalized; all prerequisites are done"), - (f"{document.userdata['dep_graph']['colors']['proved'][1]} border", - "the statement of this result is formalized"), - (f"{document.userdata['dep_graph']['colors']['proved'][1]} background", - "the proof of this result is formalized"), - (f"{document.userdata['dep_graph']['colors']['fully_proved'][1]} background", - "the proof of this result and all its ancestors are formalized"), - (f"{document.userdata['dep_graph']['colors']['mathlib'][1]} border", - "this is in Mathlib"), - ]) + document.userdata["dep_graph"]["legend"].extend( + [ + ( + f"{document.userdata['dep_graph']['colors']['can_state'][1]} border", + "the statement of this result is ready to be formalized; all prerequisites are done", + ), + ( + f"{document.userdata['dep_graph']['colors']['not_ready'][1]} border", + "the statement of this result is not ready to be formalized; the blueprint needs more work", + ), + ( + f"{document.userdata['dep_graph']['colors']['can_state'][1]} background", + "the proof of this result is ready to be formalized; all prerequisites are done", + ), + ( + f"{document.userdata['dep_graph']['colors']['proved'][1]} border", + "the statement of this result is formalized", + ), + ( + f"{document.userdata['dep_graph']['colors']['proved'][1]} background", + "the proof of this result is formalized", + ), + ( + f"{document.userdata['dep_graph']['colors']['fully_proved'][1]} background", + "the proof of this result and all its ancestors are formalized", + ), + ( + f"{document.userdata['dep_graph']['colors']['mathlib'][1]} border", + "this is in Mathlib", + ), + ] + ) document.addPostParseCallbacks(150, make_legend) - document.userdata.setdefault( - 'thm_header_extras_tpl', []).extend([CHECKMARK_TPL]) - document.userdata.setdefault('thm_header_hidden_extras_tpl', []).extend([LEAN_DECLS_TPL, - GITHUB_ISSUE_TPL]) - document.userdata['dep_graph'].setdefault('extra_modal_links_tpl', []).extend([ - LEAN_LINKS_TPL, GITHUB_LINK_TPL]) + document.userdata.setdefault("thm_header_extras_tpl", []).extend([CHECKMARK_TPL]) + document.userdata.setdefault("thm_header_hidden_extras_tpl", []).extend( + [GITHUB_ISSUE_TPL] + ) + # Side panel template goes in a new hook for content that appears after the theorem + document.userdata.setdefault("thm_side_panel_tpl", []).extend([LEAN_SIDE_PANEL_TPL]) + document.userdata["dep_graph"].setdefault("extra_modal_links_tpl", []).extend( + [LEAN_LINKS_TPL, GITHUB_LINK_TPL] + ) diff --git a/leanblueprint/Packages/renderer_templates/blueprint.jinja2s b/leanblueprint/Packages/renderer_templates/blueprint.jinja2s index 782aeda..a6141a0 100644 --- a/leanblueprint/Packages/renderer_templates/blueprint.jinja2s +++ b/leanblueprint/Packages/renderer_templates/blueprint.jinja2s @@ -1,2 +1,57 @@ name: leanok lean mathlibok notready discussion + +name: thmenv +{% macro icon(icon, id='', class='') %} + +{% endmacro %} +{% macro modal(title) %} +
    +
    +
    +

    {{ title }}

    + +
    + {{ caller() }} +
    +
    +{% endmacro %} +
    +
    +
    + + {{ obj.caption }} + + {% if obj.ref %} + {{obj.ref}} + {% endif %} + {% if obj.title %} + {{ obj.title }} + {% endif %} + {% if doc.userdata['thm_header_extras_tpl'] %} +
    + {% for tpl in doc.userdata['thm_header_extras_tpl'] %} + {% include tpl %} + {% endfor %} +
    + {% endif %} + {% if doc.userdata['thm_header_hidden_extras_tpl'] %} +
    + {% for tpl in doc.userdata['thm_header_hidden_extras_tpl'] %} + {% include tpl %} + {% endfor %} +
    + {% endif %} +
    +
    + {{ obj }} +
    +
    + {% if doc.userdata['thm_side_panel_tpl'] %} +
    + {% for tpl in doc.userdata['thm_side_panel_tpl'] %} + {% include tpl %} + {% endfor %} +
    + {% endif %} +
    diff --git a/leanblueprint/jekyll_templates/_config.yml b/leanblueprint/jekyll_templates/_config.yml index ddad425..be1f3f3 100644 --- a/leanblueprint/jekyll_templates/_config.yml +++ b/leanblueprint/jekyll_templates/_config.yml @@ -21,14 +21,14 @@ title: {| web_title |} #email: your-email@example.com description: {| web_subtitle |} -baseurl: "" # the subpath of your site, e.g. /blog +baseurl: "/{| github_projectname |}" # the subpath of your site, e.g. /blog url: "{| home |}" # the base hostname & protocol for your site, e.g. http://example.com twitter_username: github_username: {| github_username |} repository: {| github_username |}/{| github_projectname |} # Build settings -remote_theme: {| jekyll_theme |} +remote_theme: {| jekyll_theme |} plugins: - jekyll-remote-theme - jekyll-github-metadata diff --git a/leanblueprint/static/blueprint.css b/leanblueprint/static/blueprint.css index c7be366..cd51ed3 100644 --- a/leanblueprint/static/blueprint.css +++ b/leanblueprint/static/blueprint.css @@ -5,3 +5,491 @@ a.github_link { color: inherit; } +/* Wider TOC sidebar */ +@media (min-width: 1024px) { + nav.toc { + max-width: 35ch !important; + min-width: 30ch !important; + } +} + +/* ============================================ + TWO-COLUMN LAYOUT: TeX Left, Lean Right + ============================================ + + Architecture: main-text is a 2-column CSS Grid. + - Column 1 (left): All regular content (paragraphs, proofs, etc.) + - Column 2 (right): Reserved for Lean panels + - Theorem wrappers: Span BOTH columns, with their own internal grid +*/ + +/* Fix scroll issue caused by theme-white.css overflow:hidden */ +body { + overflow: auto !important; + height: auto !important; +} + +div.wrapper { + overflow: visible !important; + height: auto !important; +} + +/* Override content wrapper constraints for wider layout */ +div.content-wrapper { + max-width: none !important; + width: 100% !important; +} + +div.content { + max-width: none !important; + padding: 1rem 2rem !important; + overflow: auto !important; +} + +/* Main content area: 2-column grid */ +div.main-text { + display: grid; + grid-template-columns: minmax(0, 1fr) minmax(0, 1fr); + gap: 0 2rem; /* no row gap, 2rem column gap */ + grid-auto-flow: row; /* Ensure items flow in rows, not filling gaps */ +} + +/* Default: all children go into column 1 (left) only */ +div.main-text > * { + grid-column: 1 / 2; /* Explicitly column 1 only, not spanning */ + max-width: 100%; /* Prevent overflow */ +} + +/* Headings stay in column 1 (left) only */ +div.main-text > h1, +div.main-text > h2, +div.main-text > h3 { + grid-column: 1 / 2; +} + +/* Theorem wrappers span BOTH columns, then use their own internal grid */ +div.main-text > .definition_thmwrapper, +div.main-text > .theorem_thmwrapper, +div.main-text > .lemma_thmwrapper, +div.main-text > .proposition_thmwrapper, +div.main-text > .corollary_thmwrapper, +div.main-text > .remark_thmwrapper, +div.main-text > .example_thmwrapper { + grid-column: 1 / -1; + display: grid; + grid-template-columns: 1fr 1fr; + gap: 2rem; + margin-top: 1rem; + align-items: start; +} + +/* The main theorem content takes the first (left) column */ +div.definition_thmmain, +div.theorem_thmmain, +div.lemma_thmmain, +div.proposition_thmmain, +div.corollary_thmmain, +div.remark_thmmain, +div.example_thmmain { + grid-column: 1; + grid-row: 1; /* Force to first row */ + min-width: 0; +} + +/* The side panel takes the second (right) column */ +.thm_side_panel { + grid-column: 2; + grid-row: 1; /* Force to first row, same as thmmain */ + min-width: 0; +} + +/* Hide side panel when it has no real content (only empty lean-entry divs) */ +/* Uses :has() to check for actual content */ +.thm_side_panel:not(:has(.lean-decl-box)):not(:has(.lean-statement)):not(:has(.lean-decl-link)) { + visibility: hidden; + min-height: 0; +} + +/* Lean side panel styling */ +.lean-side-panel { + padding: 0; + font-size: 0.9em; + position: sticky; + top: 1rem; + max-height: calc(100vh - 2rem); + overflow-y: auto; +} + +.lean-entry { + margin: 0.75rem 0; +} + +.lean-entry:first-child { + margin-top: 0; +} + +/* Doc-gen4 style declaration box */ +.lean-decl-box { + background: linear-gradient(135deg, #f8fafc 0%, #f1f5f9 100%); + border-left: 4px solid #22c55e; + border-radius: 0 6px 6px 0; + padding: 0.75rem; + overflow-x: auto; + font-family: 'JetBrains Mono', 'Fira Code', 'JuliaMono', monospace; + font-size: 0.85em; + line-height: 1.5; + position: relative; +} + +/* Docs/source links in top-right corner */ +.lean-decl-links { + position: absolute; + top: 0.5rem; + right: 0.5rem; + display: flex; + gap: 0.75rem; + font-size: 0.8em; +} + +.lean-doc-link, +.lean-src-link { + color: #6b7280; + text-decoration: none; +} + +.lean-doc-link:hover, +.lean-src-link:hover { + color: #3b82f6; + text-decoration: underline; +} + +/* Doc-gen4 CSS for declaration styling */ +.lean-decl-box .decl_header { + text-indent: -4ex; + padding-left: 4ex; + padding-right: 5rem; +} + +.lean-decl-box .decl_kind { + font-weight: bold; + color: #374151; +} + +.lean-decl-box .decl_name { + font-weight: bold; + color: #1e40af; + overflow-wrap: break-word; +} + +.lean-decl-box .decl_name a { + color: #1e40af; + text-decoration: none; +} + +.lean-decl-box .decl_name a:hover { + text-decoration: underline; +} + +.lean-decl-box .decl_name::after { + content: "\A"; + white-space: pre; +} + +.lean-decl-box .decl_args { + font-weight: normal; +} + +.lean-decl-box .impl_arg { + font-style: italic; + opacity: 0.5; + transition: opacity 300ms ease-in; +} + +.lean-decl-box:hover .impl_arg { + opacity: 1; +} + +.lean-decl-box .decl_type { + margin-top: 2px; + margin-left: 2ex; + color: #374151; +} + +.lean-decl-box .fn { + color: #1e40af; +} + +.lean-decl-box a { + color: #2563eb; + text-decoration: none; +} + +.lean-decl-box a:hover { + text-decoration: underline; +} + +/* Fallback header for entries without HTML */ +.lean-entry-header { + display: flex; + align-items: center; + gap: 0.5rem; + flex-wrap: wrap; + margin-bottom: 0.5rem; +} + +.lean-decl-link { + font-family: 'JetBrains Mono', 'Fira Code', 'JuliaMono', monospace; + font-size: 0.95em; + font-weight: bold; + color: #1e40af; + text-decoration: none; +} + +.lean-decl-link:hover { + text-decoration: underline; + color: #3b82f6; +} + +.lean-src { + margin-left: auto; + text-decoration: none; + font-size: 1.1em; + opacity: 0.7; +} + +.lean-src:hover { + opacity: 1; +} + +/* Fallback plain text statement */ +.lean-statement { + font-family: 'JetBrains Mono', 'Fira Code', 'JuliaMono', monospace; + font-size: 0.8em; + line-height: 1.4; + color: #334155; + background: #f8fafc; + padding: 0.5rem; + margin: 0.5rem 0 0 0; + border-radius: 3px; + border-left: 4px solid #22c55e; + overflow-x: auto; + white-space: pre-wrap; + word-break: break-word; +} + +/* Equations - inside decl box, no label */ +.lean-equation { + font-family: 'JetBrains Mono', 'Fira Code', 'JuliaMono', monospace; + font-size: 0.85em; + line-height: 1.4; + color: #065f46; + background: #ecfdf5; + padding: 0.5rem; + margin: 0.5rem 0 0 0; + border-radius: 3px; + border-left: 3px solid #10b981; + overflow-x: auto; + white-space: pre-wrap; + word-break: break-word; +} + +/* Equation HTML with links (doc-gen style) */ +.lean-equations { + font-family: 'JetBrains Mono', 'Fira Code', 'JuliaMono', monospace; + font-size: 0.85em; + line-height: 1.5; + color: #065f46; + background: #ecfdf5; + padding: 0.5rem; + margin: 0.5rem 0 0 0; + border-radius: 3px; + border-left: 3px solid #10b981; + list-style: none; +} + +.lean-equations li.equation { + margin: 0.25rem 0; + white-space: pre-wrap; + word-break: break-word; +} + +.lean-equations a { + color: #1e40af; + text-decoration: none; +} + +.lean-equations a:hover { + text-decoration: underline; +} + +.lean-equations a.blueprint-link { + color: #0d9488; + font-weight: 500; +} + +.lean-equations a.blueprint-link:hover { + color: #0f766e; +} + +/* Structure fields - styled similarly to equations */ +.lean-structure-fields { + font-family: 'JetBrains Mono', 'Fira Code', 'JuliaMono', monospace; + font-size: 0.85em; + line-height: 1.5; + color: #1e3a5f; + background: #eff6ff; + padding: 0.5rem; + margin: 0.5rem 0 0 0; + border-radius: 3px; + border-left: 3px solid #3b82f6; + list-style: none; +} + +.lean-structure-fields li.structure_field { + margin: 0.4rem 0; + padding: 0.2rem 0; + border-bottom: 1px solid #dbeafe; +} + +.lean-structure-fields li.structure_field:last-child { + border-bottom: none; +} + +.lean-structure-fields .structure_field_info { + white-space: pre-wrap; + word-break: break-word; +} + +.lean-structure-fields .structure_field_doc, +.lean-structure-fields .structure_field_doc p { + font-size: 1.05em !important; + font-family: -apple-system, BlinkMacSystemFont, 'Segoe UI', Roboto, sans-serif !important; + color: #6b7280; + margin: 0; + margin-top: 0.15rem; + font-style: italic; + line-height: 1.3; +} + +/* Code elements within structure field documentation should match surrounding text size */ +.lean-structure-fields .structure_field_doc code, +.lean-structure-fields .structure_field_doc .docstring_code { + font-size: inherit !important; + font-family: 'JetBrains Mono', 'Fira Code', 'JuliaMono', monospace !important; + font-style: normal; + background: rgba(59, 130, 246, 0.1); + padding: 0.1em 0.3em; + border-radius: 3px; + color: #1e40af; +} + +.lean-structure-fields a { + color: #1e40af; + text-decoration: none; +} + +.lean-structure-fields a:hover { + text-decoration: underline; +} + +.lean-structure-fields a.blueprint-link { + color: #0d9488; + font-weight: 500; +} + +.lean-structure-fields a.blueprint-link:hover { + color: #0f766e; +} + +/* Plain text fallback for structure fields */ +.lean-fields { + font-family: 'JetBrains Mono', 'Fira Code', 'JuliaMono', monospace; + font-size: 0.85em; + line-height: 1.4; + color: #1e3a5f; + background: #eff6ff; + padding: 0.5rem; + margin: 0.5rem 0 0 0; + border-radius: 3px; + border-left: 3px solid #3b82f6; + overflow-x: auto; + white-space: pre-wrap; + word-break: break-word; +} + +/* Blueprint links in declaration body */ +.lean-decl-box a.blueprint-link { + color: #0d9488; + font-weight: 500; +} + +.lean-decl-box a.blueprint-link:hover { + color: #0f766e; + text-decoration: underline; +} + +/* Target theorem styling - prominent, highlighted */ +.lean-side-panel.lean-target .lean-decl-box { + border-left-width: 6px; + border-left-color: #2563eb; + background: linear-gradient(135deg, #eff6ff 0%, #dbeafe 100%); + box-shadow: 0 2px 8px rgba(37, 99, 235, 0.15); +} + +.lean-side-panel.lean-target .lean-decl-box .decl_name, +.lean-side-panel.lean-target .lean-decl-box .decl_name a { + color: #1d4ed8; + font-size: 1.05em; +} + +/* Helper lemma styling - subtle, muted */ +.lean-side-panel.lean-helper .lean-decl-box { + border-left-width: 2px; + border-left-color: #9ca3af; + background: linear-gradient(135deg, #f9fafb 0%, #f3f4f6 100%); + opacity: 0.85; + font-size: 0.9em; +} + +.lean-side-panel.lean-helper .lean-decl-box .decl_name, +.lean-side-panel.lean-helper .lean-decl-box .decl_name a { + color: #4b5563; +} + +.lean-side-panel.lean-helper .lean-decl-box .decl_kind { + color: #6b7280; +} + +/* Helper can expand on hover to show full detail */ +.lean-side-panel.lean-helper .lean-decl-box:hover { + opacity: 1; +} + +/* Responsive: single column on narrow screens */ +@media (max-width: 1200px) { + div.main-text { + display: block; /* Fall back to normal flow */ + } + + div.main-text > .definition_thmwrapper, + div.main-text > .theorem_thmwrapper, + div.main-text > .lemma_thmwrapper, + div.main-text > .proposition_thmwrapper, + div.main-text > .corollary_thmwrapper, + div.main-text > .remark_thmwrapper, + div.main-text > .example_thmwrapper { + display: block; + } + + .thm_side_panel { + margin-top: 1rem; + } + + .lean-side-panel { + margin-top: 1rem; + padding-top: 1rem; + border-top: 1px solid #e5e7eb; + position: static; + max-height: none; + } +} From 35fe98bab204dd99d00484bafdf14e69085a836c Mon Sep 17 00:00:00 2001 From: Fabian Gloeckle <2.fg@hotmail.de> Date: Fri, 3 Apr 2026 02:35:10 +0200 Subject: [PATCH 2/2] Fix branch name --- leanblueprint/Packages/blueprint.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/leanblueprint/Packages/blueprint.py b/leanblueprint/Packages/blueprint.py index 4f99363..77d2f17 100644 --- a/leanblueprint/Packages/blueprint.py +++ b/leanblueprint/Packages/blueprint.py @@ -592,7 +592,7 @@ def make_lean_data() -> None: if project_github and doc_link: module_path = doc_link.split("#")[0].replace(".html", ".lean") entry["github_url"] = ( - f"{project_github}/blob/summary/{module_path}" + f"{project_github}/blob/main/{module_path}" ) lean_entries.append(entry)