diff --git a/.github/workflows/documentation.yml b/.github/workflows/documentation.yml index 55d36da..66e36ff 100644 --- a/.github/workflows/documentation.yml +++ b/.github/workflows/documentation.yml @@ -4,9 +4,9 @@ on: workflow_dispatch: inputs: release_ref: - description: Exact 1.9.4 tag to publish + description: Source ref for a 1.9.4 documentation rebuild required: true - default: v1.9.4 + default: main release: types: [published] @@ -113,7 +113,8 @@ jobs: run: | gh release upload "${{ github.event.release.tag_name }}" \ artifacts/mathlib-fp-docs-1.9.4.zip \ - artifacts/mathlib-fp-docs-1.9.4.zip.sha256 --clobber + artifacts/mathlib-fp-docs-1.9.4.zip.sha256 --clobber \ + --repo "$GITHUB_REPOSITORY" deploy: if: github.event_name != 'release' || github.event.release.tag_name == 'v1.9.4' diff --git a/docs/RELEASE_NOTES_1.9.4.md b/docs/RELEASE_NOTES_1.9.4.md index 125e572..be40502 100644 --- a/docs/RELEASE_NOTES_1.9.4.md +++ b/docs/RELEASE_NOTES_1.9.4.md @@ -1,4 +1,4 @@ -# Release notes: 1.9.4 +# mathlib-fp v1.9.4 ## Numerical trust closure diff --git a/tools/build_docs.py b/tools/build_docs.py index 1828551..8c70981 100644 --- a/tools/build_docs.py +++ b/tools/build_docs.py @@ -52,6 +52,7 @@ def markdown_to_html(source: str, link_resolver=None) -> tuple[str, str]: output: list[str] = [] plain: list[str] = [] paragraph: list[str] = [] + list_item: list[str] = [] in_code = False in_list = False @@ -62,13 +63,37 @@ def flush_paragraph() -> None: plain.append(text) paragraph.clear() + def flush_list_item() -> None: + if list_item: + text = " ".join(list_item) + output.append(f"
  • {inline(text, link_resolver)}
    • ") + plain.append(text) + list_item.clear() + def close_list() -> None: nonlocal in_list if in_list: + flush_list_item() output.append("") in_list = False - for line in source.splitlines(): + def table_cells(line: str) -> list[str] | None: + value = line.strip() + if not value.startswith("|"): + return None + if value.endswith("|"): + value = value[:-1] + return [cell.strip() for cell in value[1:].split("|")] + + def is_table_divider(cells: list[str] | None, width: int) -> bool: + return bool(cells) and len(cells) == width and all( + re.fullmatch(r":?-{3,}:?", cell) for cell in cells + ) + + lines = source.splitlines() + line_index = 0 + while line_index < len(lines): + line = lines[line_index] if line.startswith("```"): flush_paragraph() close_list() @@ -80,10 +105,12 @@ def close_list() -> None: f'
    '
                 )
             in_code = not in_code
+            line_index += 1
             continue
         if in_code:
             output.append(html.escape(line) + "\n")
             plain.append(line)
+            line_index += 1
             continue
         heading = re.match(r"^(#{1,6})\s+(.+)$", line)
         if heading:
@@ -101,20 +128,61 @@ def close_list() -> None:
             if not in_list:
                 output.append("