Add Python 3.14 support

.github/workflows/ci.yml

@@ -13,13 +13,13 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        python-version: ["3.10", "3.11", "3.12", "3.13"]
+        python-version: ["3.10", "3.11", "3.12", "3.13", "3.14"]
 
     steps:
     - uses: actions/checkout@v4
 
     - name: Set up Python ${{ matrix.python-version }}
-      uses: actions/setup-python@v4
+      uses: actions/setup-python@v5
       with:
         python-version: ${{ matrix.python-version }}
 
@@ -68,7 +68,7 @@ jobs:
     - uses: actions/checkout@v4
 
     - name: Set up Python
-      uses: actions/setup-python@v4
+      uses: actions/setup-python@v5
       with:
         python-version: "3.11"
 
@@ -94,7 +94,7 @@ jobs:
     - uses: actions/checkout@v4
 
     - name: Set up Python
-      uses: actions/setup-python@v4
+      uses: actions/setup-python@v5
       with:
         python-version: "3.11"
 

.github/workflows/metrics.yml

@@ -0,0 +1,83 @@
+name: metrics
+
+on:
+  workflow_dispatch:
+    inputs:
+      sample:
+        description: "Number of AFP files to sample"
+        default: "500"
+  schedule:
+    - cron: '0 4 * * 1'   # 04:00 UTC every Monday
+
+# Allow the job to commit the refreshed README back to the repo.
+permissions:
+  contents: write
+
+concurrency:
+  group: metrics
+  cancel-in-progress: false
+
+jobs:
+  metrics:
+    runs-on: ubuntu-latest
+    timeout-minutes: 60
+
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Set up Python
+        uses: actions/setup-python@v4
+        with:
+          python-version: "3.12"
+
+      - name: Install Poetry
+        uses: snok/install-poetry@v1
+        with:
+          version: latest
+          virtualenvs-create: true
+          virtualenvs-in-project: true
+
+      - name: Install dependencies
+        run: poetry install --all-extras --no-interaction
+
+      - name: Compute cache week
+        id: week
+        run: echo "week=$(date -u +%G-%V)" >> "$GITHUB_OUTPUT"
+
+      - name: Cache AFP corpus
+        uses: actions/cache@v4
+        with:
+          path: corpus
+          # Weekly key: refreshes the corpus each ISO week, reused within the
+          # week (e.g. for manual re-runs). No restore-keys, so a new week is a
+          # genuine miss and the fetch script downloads the latest release.
+          key: afp-corpus-${{ steps.week.outputs.week }}
+
+      - name: Fetch AFP corpus
+        run: bash metrics/fetch_corpus.sh corpus
+
+      - name: Measure coverage and performance
+        env:
+          METRICS_SAMPLE: ${{ github.event.inputs.sample || '500' }}
+        run: poetry run python metrics/measure.py
+
+      - name: Update README
+        run: poetry run python metrics/update_readme.py
+
+      - name: Commit refreshed metrics
+        run: |
+          git config user.name  "metrics-bot"
+          git config user.email "metrics-bot@users.noreply.github.com"
+          git add README.rst metrics/metrics.json
+          # Pushing with the default GITHUB_TOKEN does not retrigger workflows;
+          # [skip ci] is belt-and-suspenders. No-op stays green.
+          git commit -m "chore: update AFP metrics [skip ci]" || { echo "no changes"; exit 0; }
+          # master may have advanced during the (multi-minute) run, which would
+          # reject the push; rebase onto the latest and retry a few times.
+          for attempt in 1 2 3 4 5; do
+            if git push; then exit 0; fi
+            echo "push rejected (attempt $attempt) - rebasing on origin/master ..."
+            git pull --rebase --autostash origin master
+          done
+          echo "failed to push metrics after retries" >&2
+          exit 1

.gitignore

@@ -46,3 +46,4 @@ pip-wheel-metadata/
 pytestdebug.log
 scripts/
 src/_pytest/_version.py
+corpus/

README.rst

@@ -0,0 +1,162 @@
+================
+isabelle_parser
+================
+
+.. image:: https://github.com/christiankissig/python-isabelle-parser/actions/workflows/ci.yml/badge.svg?branch=master
+   :target: https://github.com/christiankissig/python-isabelle-parser/actions/workflows/ci.yml
+   :alt: CI/CD status
+
+.. image:: https://img.shields.io/badge/python-3.10%2B-blue.svg
+   :target: https://www.python.org/downloads/
+   :alt: Python 3.10+
+
+.. image:: https://img.shields.io/badge/license-MIT-green.svg
+   :target: https://github.com/christiankissig/python-isabelle-parser/blob/master/LICENSE
+   :alt: License: MIT
+
+A parser for `Isabelle/Isar <https://isabelle.in.tum.de/>`_ theory (``.thy``)
+artifacts, implemented in pure Python on top of `Lark <https://lark-parser.org/>`_
+using an Earley grammar.
+
+It turns the outer syntax of a theory file — the theory header, document
+markup, specifications (``definition``, ``datatype``, ``fun``, ``locale``,
+``class``, …), Isar proofs and FFI/ML commands — into a Lark parse tree that you
+can walk programmatically.
+
+Status
+======
+
+Work in progress. The grammar covers a large and growing share of the outer
+syntax found in the `Archive of Formal Proofs <https://www.isa-afp.org/>`_, but
+it is not yet complete: inner-syntax terms with exotic notation, some proof
+methods, and a few rarely-used commands are still rejected. Treat a successful
+parse as authoritative and a failure as "not yet supported" rather than "invalid
+Isabelle".
+
+Metrics
+=======
+
+Parser coverage and performance against the latest `Archive of Formal Proofs
+<https://www.isa-afp.org/>`_ release, refreshed weekly by the ``metrics``
+workflow (and on demand via *Run workflow*):
+
+.. METRICS:START
+
+.. list-table::
+   :header-rows: 1
+   :widths: 45 55
+
+   * - Metric
+     - Value
+   * - AFP snapshot
+     - afp-2026-06-01
+   * - Files sampled
+     - 500
+   * - Parse coverage
+     - 33.6% (168 parsed)
+   * - Timeouts (> 15s)
+     - 21.2% (106)
+   * - Throughput
+     - 0.81 files/s · 0.024 MB/s (×4 workers)
+   * - Median parse time (parsed files)
+     - 2.785 s
+   * - Measured
+     - 2026-06-03 09:58 UTC
+
+*Coverage is the share of a seeded random sample of AFP theory files that parse within the timeout; a whole file counts as failed if any statement fails. Updated weekly by the metrics workflow.*
+
+.. METRICS:END
+
+Requirements
+============
+
+* Python >= 3.10
+* `lark <https://pypi.org/project/lark/>`_
+
+Installation
+============
+
+From a clone of the repository:
+
+.. code-block:: bash
+
+   pip install .
+
+For a development checkout (tests, linters):
+
+.. code-block:: bash
+
+   pip install -e ".[dev]"
+
+Command-line usage
+==================
+
+The CLI parses a file or a literal string and prints the resulting tree:
+
+.. code-block:: bash
+
+   # parse a theory file
+   python -m isabelle_parser.cli -f path/to/Theory.thy
+
+   # parse a literal string
+   python -m isabelle_parser.cli "theory T imports Main begin end"
+
+Options:
+
+``-f``, ``--file``
+   Interpret the input argument as a filename rather than a literal string.
+
+``-t``, ``--timeout SECONDS``
+   Abort the parse after ``SECONDS`` and report a failure instead of hanging.
+   The Earley chart can grow super-linearly on large or highly ambiguous files,
+   so this is a useful guard when parsing a whole corpus.
+
+The command exits non-zero if parsing fails.
+
+Library usage
+=============
+
+.. code-block:: python
+
+   from isabelle_parser import parse, load_parser, ParsingError
+
+   source = "theory T imports Main begin\nlemma \"x = x\" by simp\nend"
+
+   try:
+       tree = parse(source)
+       print(tree.pretty())
+   except ParsingError as error:
+       print(f"parsing failed: {error}")
+
+``parse(input_text, parser=None, timeout=None)``
+   Parse ``input_text`` and return a Lark ``Tree``. If ``parser`` is omitted a
+   default parser is built for the ``start`` rule. ``timeout`` (seconds) bounds
+   the parse and raises ``ParsingError`` if exceeded; it relies on ``SIGALRM``
+   and therefore applies only on the main thread of a Unix process (it is
+   silently skipped elsewhere).
+
+``load_parser(start="start")``
+   Build and return the underlying Lark parser, optionally starting from a
+   specific grammar rule. Reuse a single instance when parsing many files —
+   building the parser is the expensive part.
+
+``ParsingError``
+   Raised for invalid input and on timeout. Lark may also raise its own
+   ``lark.exceptions.UnexpectedInput`` subclasses for structurally invalid input.
+
+Development
+===========
+
+.. code-block:: bash
+
+   pytest            # run the test suite
+   ruff check .      # lint
+   ruff format .     # format
+   isort .           # import ordering
+
+The grammar lives in ``isabelle_parser/thy_grammar.lark``.
+
+License
+=======
+
+MIT. See the ``LICENSE`` file.

isabelle_parser/cli.py

@@ -14,6 +14,14 @@ def main() -> None:
     arg_parser.add_argument(
         "-f", "--file", action="store_true", help="Interpret input as a filename"
     )
+    arg_parser.add_argument(
+        "-t",
+        "--timeout",
+        type=float,
+        default=None,
+        help="Abort the parse after this many seconds (guards against "
+        "pathological inputs that grow the Earley chart super-linearly)",
+    )
 
     # Parse arguments
     args = arg_parser.parse_args()
@@ -31,7 +39,7 @@ def main() -> None:
 
     # Lex and parse
     try:
-        result = parse(data)
+        result = parse(data, timeout=args.timeout)
     except ParsingError as e:
         print("Parsing failed due to errors.")
         print(f"Error: {e.with_source_code(data)}")

isabelle_parser/error.py

@@ -26,7 +26,7 @@ def _source_hint(self) -> str:
                 print(line)
                 underline = " " * (self.column - 1) + "^" * len(self.token)
                 return f"\n\n{line}\n{underline}\n"
-        return "source_hint"
+        return ""
 
     def __str__(self) -> str:
         location_info = ""