Unexpected compilation errors and errors in ProofNet Lean4 dataset

[brando90]

Script:

"""
Example script: pantograph_import.py

Demonstrates how to:
  - Initialize a Pantograph Server with Mathlib.
  - Prepend custom headers/imports to a theorem snippet.
  - Detect Lean "syntax/parse" errors by searching for "error:" lines
    while ignoring "unsolved goals."
  - Validate that all statements in the "proofnet-v2-lean4" dataset are
    syntax-error-free on both validation and test splits.
"""

import os
from pantograph.server import Server
from typing import List, Tuple
import re


##############################################################################
# 1) The minimal helper that identifies "error:" lines, ignoring unsolved goals
##############################################################################
def check_lean_compiles_syntax_only(server: Server, lean_snippet: str, debug: bool = False) -> Tuple[int, List]:
    r"""
    Check a Lean 4 code snippet for *parse/syntax errors* (ignore "unsolved goals").

    Implementation:
      - We call `server.load_sorry(lean_snippet)`, which compiles the snippet.
      - For each message in the returned compilation units:
        * If the line contains "error:" (case-insensitive is optional),
          we check if it also has "unsolved goals" — if so, skip it, because
          that's not a parse/lexical error.
        * Otherwise, count it as a syntax error.

    Returns the count of syntax/parse errors found.

    Example
    -------
    >>> server = Server(imports=["Mathlib"], project_path="~/mathlib4")
    >>> code = "theorem two_eq_two : 2 = 2 := by"  # incomplete
    >>> num_errs = check_lean_compiles_syntax_only(server, code)
    >>> print(num_errs)  # 1 or more
    """
    try:
        compilation_units = server.load_sorry(lean_snippet)
    except:
        print(f'\n----{lean_snippet=}----\n') if debug else None
        import traceback
        traceback.print_exc() if debug else None
        return 1, ['PyPantograph threw someexception.']

    syntax_error_count = 0
    syntax_compilation_err_units: list = []
    for comp_unit in compilation_units:
        for msg in comp_unit.messages:
            # Quick check: if 'error:' is in the message, but not "unsolved goals"
            # => it's likely a parse/lexical error.
            # (In practice, we often see strings like "<anonymous>:1:5: error: ...")
            if "error:" in msg and ("unsolved goals" not in msg.lower()):
                syntax_error_count += 1
        if syntax_error_count > 0 and debug:
            syntax_compilation_err_units.append(comp_unit)

    return syntax_error_count, syntax_compilation_err_units


##############################################################################
# 2) Minimal usage example with a single snippet
##############################################################################
def main_single_test():
    """
    Quick demonstration on a single snippet. 
    We'll only treat "error:" lines that do NOT mention 'unsolved goals' as parse errors.
    """
    print("=== Single Snippet Test ===")

    # (A) Initialize Pantograph for a Lean 4 project that includes Mathlib:
    project_path = os.path.expanduser("~/mathlib4")  # Adjust as needed
    server = Server(
        imports=["Mathlib"],
        project_path=project_path
    )

    # (B) The snippet (with a custom open + a theorem using `:= sorry`)
    lean_snippet = (
        "open Complex Filter Function Metric Finset open scoped BigOperators Topology\n\n"
        "theorem exercise_1_13b {f : ℂ → ℂ} (Ω : Set ℂ) (a b : Ω) (h : IsOpen Ω) "
        "(hf : DifferentiableOn ℂ f Ω) (hc : ∃ (c : ℝ), ∀ z ∈ Ω, (f z).im = c) "
        ": f a = f b := sorry"
    )

    syntax_errs = check_lean_compiles_syntax_only(server, lean_snippet)
    print(f"\nSnippet:\n{lean_snippet}\n")

    if syntax_errs == 0:
        print("[OK] No syntax/parse errors found (though it might have unsolved goals).")
    else:
        print(f"[ERROR] Found {syntax_errs} parse/lexical syntax errors.")


##############################################################################
# 3) Checking both validation and test splits from "proofnet-v2-lean4"
##############################################################################
def main_hf_proofnet():
    """
    Illustrates checking the proofnet-v2-lean4 dataset on both validation
    and test splits for syntax correctness. If the dataset is correct, we
    expect zero syntax errors.
    """
    print("=== Checking proofnet-v2-lean4 (val + test) ===")
    from datasets import load_dataset

    # 1) Initialize server, pointing at your local Lean + Mathlib project
    project_path = os.path.expanduser("~/mathlib4")
    server = Server(
        imports=["Mathlib"],
        project_path=project_path
    )

    # 2) Helper to run a syntax check loop
    def check_split(split_name: str):
        ds = load_dataset("UDACA/proofnet-v2-lean4", split=split_name)
        total_snippets = 0
        num_parse_ok = 0

        for row in ds:
            header = row["header"]
            # Optionally remove "import Mathlib" if it appears
            header = header.replace("import Mathlib", "")

            # Combine the snippet:
            snippet = f"{header}\n\n{row['formal_statement']}"
            syntax_err_count, syntax_compilation_err_units = check_lean_compiles_syntax_only(server, snippet, debug=True)

            total_snippets += 1
            if syntax_err_count == 0:
                num_parse_ok += 1
            else:
                print(f'Current number of syntax errors for current sinppet: {syntax_err_count=}')
                print(f'----\n{snippet}\n----')
                print(f'{syntax_compilation_err_units=}')

        print(f"Split={split_name}: {num_parse_ok}/{total_snippets} have zero syntax errors.")
        return num_parse_ok, total_snippets

    # 3) Run for validation
    val_ok, val_total = check_split("validation")

    # 4) Run for test
    test_ok, test_total = check_split("test")

    # Summarize
    print("=== Summary ===")
    print(f"Validation: {val_ok}/{val_total} OK")
    print(f"Test:       {test_ok}/{test_total} OK")


##############################################################################
# 4) Entry point
##############################################################################
if __name__ == "__main__":
    # Example single snippet test
    # main_single_test()

    # (Optional) Check the entire proofnet-v2-lean4 validation & test
    main_hf_proofnet()

Errors:

(zip_fit) brando9@skampere1~/ZIP-FIT $  cd /lfs/skampere1/0/brando9/ZIP-FIT ; /usr/bin/env /lfs/skampere1/0/brando9/miniconda/envs/zip_fit/bin/python /lfs/skampere1/0/brando9/.vscode-server-insiders/extensions/ms-python.debugpy-2024.14.0-linux-x64/bundled/libs/debugpy/adapter/../../debugpy/launcher 32783 -- /lfs/skampere1/0/brando9/ZIP-FIT/experiments/pantograph_imports.py 
=== Checking proofnet-v2-lean4 (val + test) ===
Repo card metadata block was not found. Setting CardData to empty.
Current number of syntax errors for current sinppet: syntax_err_count=1
----


open Fintype Complex Polynomial LinearMap FiniteDimensional Module Module.End
open scoped BigOperators



theorem exercise_6_2 {V : Type*} [NormedAddCommGroup V] [Module ℂ V]
[InnerProductSpace ℂ V] (u v : V) :
  ⟪u, v⟫_ℂ = 0 ↔ ∀ (a : ℂ), ‖u‖  ≤ ‖u + a • v‖:= sorry
----
syntax_compilation_err_units=[CompilationUnit(i_begin=108, i_end=226, messages=['<anonymous>:10:7: error: expected token\n'], invocations=None, goal_state=None, goal_src_boundaries=None, new_constants=None), CompilationUnit(i_begin=226, i_end=295, messages=[], invocations=None, goal_state=None, goal_src_boundaries=None, new_constants=None)]
Current number of syntax errors for current sinppet: syntax_err_count=1
----


open Fintype Complex Polynomial LinearMap FiniteDimensional Module Module.End
open scoped BigOperators



theorem exercise_6_7 {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V] (u v : V) :
  ⟪u, v⟫_ℂ = (‖u + v‖^2 - ‖u - v‖^2 + I*‖u + I•v‖^2 - I*‖u-I•v‖^2) / 4:= sorry
----
syntax_compilation_err_units=[CompilationUnit(i_begin=108, i_end=211, messages=['<anonymous>:9:7: error: expected token\n'], invocations=None, goal_state=None, goal_src_boundaries=None, new_constants=None), CompilationUnit(i_begin=211, i_end=306, messages=[], invocations=None, goal_state=None, goal_src_boundaries=None, new_constants=None)]

----lean_snippet='\n\nopen Filter Set TopologicalSpace\nopen scoped Topology\n\n\n\ntheorem exercise_22_2b {X : Type*} [TopologicalSpace X]\n  {A : Set X} (r : X → A) (hr : Continuous r) (h : ∀ x : A, r x = x) :\n  QuotientMap r:= sorry'----

Traceback (most recent call last):
  File "/lfs/skampere1/0/brando9/ZIP-FIT/experiments/pantograph_imports.py", line 44, in check_lean_compiles_syntax_only
    compilation_units = server.load_sorry(lean_snippet)
                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/lfs/skampere1/0/brando9/PyPantograph/pantograph/utils.py", line 16, in wrapper
    return asyncio.run(func(*args, **kwargs))
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/lfs/skampere1/0/brando9/miniconda/envs/zip_fit/lib/python3.11/asyncio/runners.py", line 190, in run
    return runner.run(main)
           ^^^^^^^^^^^^^^^^
  File "/lfs/skampere1/0/brando9/miniconda/envs/zip_fit/lib/python3.11/asyncio/runners.py", line 118, in run
    return self._loop.run_until_complete(task)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/lfs/skampere1/0/brando9/miniconda/envs/zip_fit/lib/python3.11/asyncio/base_events.py", line 654, in run_until_complete
    return future.result()
           ^^^^^^^^^^^^^^^
  File "/lfs/skampere1/0/brando9/PyPantograph/pantograph/server.py", line 348, in load_sorry_async
    raise ServerError(result)
pantograph.server.ServerError: {'error': 'frontend', 'desc': 'Coupling is not allowed in drafting'}
Current number of syntax errors for current sinppet: syntax_err_count=1
----


open Filter Set TopologicalSpace
open scoped Topology



theorem exercise_22_2b {X : Type*} [TopologicalSpace X]
  {A : Set X} (r : X → A) (hr : Continuous r) (h : ∀ x : A, r x = x) :
  QuotientMap r:= sorry
----
syntax_compilation_err_units=['PyPantograph threw someexception.']
Split=validation: 182/185 have zero syntax errors.
Repo card metadata block was not found. Setting CardData to empty.
Current number of syntax errors for current sinppet: syntax_err_count=1
----


open Fintype Complex Polynomial LinearMap FiniteDimensional Module Module.End
open scoped BigOperators



theorem exercise_6_13 {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V] {n : ℕ}
  {e : Fin n → V} (he : Orthonormal ℂ e) (v : V) :
  ‖v‖^2 = ∑ i : Fin n, ‖⟪v, e i⟫_ℂ‖^2 ↔ v ∈ Submodule.span ℂ (e '' Set.univ):= sorry
----
syntax_compilation_err_units=[CompilationUnit(i_begin=108, i_end=297, messages=['<anonymous>:10:31: error: expected token\n'], invocations=None, goal_state=None, goal_src_boundaries=None, new_constants=None), CompilationUnit(i_begin=297, i_end=362, messages=[], invocations=None, goal_state=None, goal_src_boundaries=None, new_constants=None)]

----lean_snippet='\n\nopen Filter Set TopologicalSpace\nopen scoped Topology\n\n\n\ntheorem exercise_22_2a {X Y : Type*} [TopologicalSpace X]\n  [TopologicalSpace Y] (p : X → Y) (h : Continuous p) :\n  QuotientMap p ↔ ∃ (f : Y → X), Continuous f ∧ p ∘ f = id:= sorry'----

Traceback (most recent call last):
  File "/lfs/skampere1/0/brando9/ZIP-FIT/experiments/pantograph_imports.py", line 44, in check_lean_compiles_syntax_only
    compilation_units = server.load_sorry(lean_snippet)
                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/lfs/skampere1/0/brando9/PyPantograph/pantograph/utils.py", line 16, in wrapper
    return asyncio.run(func(*args, **kwargs))
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/lfs/skampere1/0/brando9/miniconda/envs/zip_fit/lib/python3.11/asyncio/runners.py", line 190, in run
    return runner.run(main)
           ^^^^^^^^^^^^^^^^
  File "/lfs/skampere1/0/brando9/miniconda/envs/zip_fit/lib/python3.11/asyncio/runners.py", line 118, in run
    return self._loop.run_until_complete(task)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/lfs/skampere1/0/brando9/miniconda/envs/zip_fit/lib/python3.11/asyncio/base_events.py", line 654, in run_until_complete
    return future.result()
           ^^^^^^^^^^^^^^^
  File "/lfs/skampere1/0/brando9/PyPantograph/pantograph/server.py", line 348, in load_sorry_async
    raise ServerError(result)
pantograph.server.ServerError: {'error': 'frontend', 'desc': 'Coupling is not allowed in drafting'}
Current number of syntax errors for current sinppet: syntax_err_count=1
----


open Filter Set TopologicalSpace
open scoped Topology



theorem exercise_22_2a {X Y : Type*} [TopologicalSpace X]
  [TopologicalSpace Y] (p : X → Y) (h : Continuous p) :
  QuotientMap p ↔ ∃ (f : Y → X), Continuous f ∧ p ∘ f = id:= sorry
----
syntax_compilation_err_units=['PyPantograph threw someexception.']
Current number of syntax errors for current sinppet: syntax_err_count=1
----


open Filter Set TopologicalSpace
open scoped Topology



theorem exercise_23_11 {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
  (p : X → Y) (hq : QuotientMap p)
  (hY : ConnectedSpace Y) (hX : ∀ y : Y, IsConnected (p ⁻¹' {y})) :
  ConnectedSpace X:= sorry
----
syntax_compilation_err_units=[CompilationUnit(i_begin=59, i_end=274, messages=['<anonymous>:9:20: error: function expected at\n  QuotientMap\nterm has type\n  ?m.19\n'], invocations=None, goal_state=GoalState(state_id=335, goals=[Goal(variables=[Variable(t='Sort u_3', v=None, name='x✝'), Variable(t='x✝', v=None, name='QuotientMap'), Variable(t='Type u_1', v=None, name='X'), Variable(t='Type u_2', v=None, name='Y'), Variable(t='TopologicalSpace X', v=None, name='inst✝¹'), Variable(t='TopologicalSpace Y', v=None, name='inst✝'), Variable(t='X → Y', v=None, name='p'), Variable(t='sorry', v=None, name='hq'), Variable(t='ConnectedSpace Y', v=None, name='hY'), Variable(t="∀ (y : Y), IsConnected (p ⁻¹' {y})", v=None, name='hX')], target='ConnectedSpace X', sibling_dep=[], name=None, is_conversion=False)], _sentinel=[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, 146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159, 160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173, 174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231, 232, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 255, 256, 257, 258, 259, 260, 261, 262, 263, 264, 265, 266, 267, 268, 269, 270, 271, 272, 273, 274, 275, 276, 277, 278, 279, 280, 281, 282, 283, 284, 285, 286, 287, 288, 289, 290, 291, 292, 293, 294, 295, 296, 297, 298, 299, 300, 301, 302, 303, 304, 305, 306, 307, 308, 309, 310, 311, 312, 313, 314, 315, 316, 317, 318, 319, 320, 321, 322, 323, 324, 325, 326, 327, 328, 329, 330, 331, 332, 333, 334]), goal_src_boundaries=[[269, 274]], new_constants=None)]
Split=test: 183/186 have zero syntax errors.
=== Summary ===
Validation: 182/185 OK
Test:       183/186 OK

[brando90]

partially cross posted (for the lean part of the questions): https://proofassistants.stackexchange.com/questions/4666/fixing-made-up-quotientmap-in-proofnet-what-is-the-recommended-name

[lenianiva]

Didn't we establish that QuotientMap wasn't a real type in mathlib? Do you have a MWE?