AlephProver prep helper scripts - #9
Open
mayorov-m-a wants to merge 5 commits into
Open
Conversation
getAllLakePaths stopped at the first directory containing .lake, so a git dependency that ships several packages side by side (e.g. packages/Hammer/HammerCore) contributed only its top-level build directory and imports from the sibling packages failed to resolve. Recurse into such sub-packages as well. Also honour LEAN_PATH when it is set: 'lake env' derives it from the manifest, which is authoritative for layouts the directory walk cannot infer. parseFile now sets the search path itself (and enables initializer execution) before elaborating, so the library entry point works without the caller having to replicate what bins/ExtractSorry does. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
… tests into Lake
Each ParsedSorry now carries start_byte/end_byte and kind ("tactic" or
"term"). Tools that rewrite the source need exactly this: a byte range is
what a splice replaces, and the kind decides whether the replacement needs a
leading 'by'. On input the three fields are optional (Option, so the derived
FromJson accepts a record that lacks them), which keeps records with only
line/column positions -- the shape the SorryDB database stores -- valid input
for KernelCheck and the goal extractor; ParsedSorry.acceptsKind is the helper
consumers use to filter by kind when one is given.
A sorry tactic also elaborates to a sorry term at the same position, and the
two records used to coincide and be deduplicated. With kind they differ, so
dedupByToken merges them explicitly and keeps the tactic record.
The golden tests were not runnable from a fresh checkout: LeanUtilsTest was
not a Lake target, so its fixture was never built and findOLean could not
resolve the fixture's module name. Declare it (and 'bins', so tests can import
the executables' root modules), make it the test driver, and regenerate the
expected output.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…KernelCheck's verdict on kernel errors Move findTargetEnv out of bins/KernelCheck.lean into LeanUtils/TargetEnv.lean so that other executables can recover the elaboration state at a sorry (the ContextInfo, the local context, the goal type, and the positions of the enclosing commands). Two behaviours change on the way: * A token that closes several goals (constructor <;> sorry, all_goals sorry) used to abort with "Found more than one goal". The recorded goal text now selects the intended goal, compared with whitespace collapsed because different tools wrap goals at different widths; only a genuinely ambiguous token is refused, with the candidates listed. * The record's kind, when given, restricts the match to term or tactic nodes (ParsedSorry.acceptsKind); without it both are accepted as before. KernelCheck looks the parent declaration's TheoremVal up in the environment (it is only needed for the level parameters) and runs elaboration in the sorry's own local context rather than an empty one. Also: when addDecl throws, kernelCheck reported success = true alongside the kernel's error message. Report success = false. A golden test covers the three outcomes (accepted, rejected by name, rejected by the kernel). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
ExtractGoal <file> <ParsedSorry json> [flags] re-elaborates the file,
recovers the goal and local context at the given sorry (via
LeanUtils.TargetEnv), reverts the context into binders and prints
* the source prefix up to the enclosing command (where the helper belongs,
followed by any '... in' wrappers around the declaration),
* 'theorem mytheorem <binders> : <goal> := sorry', and
* the application 'mytheorem <args>' that closes the original goal,
separated by marker lines. Replacing the sorry with 'exact <application>' and
inserting the helper before the enclosing command gives a file whose only
new sorry is the helper's, so the restatement is validated by compiling
that file. Universe parameters are renamed so they cannot collide with
section universes at the insertion point.
The default rendering is compact. A set of flags each changes one
pretty-printer or context-handling decision for goals whose compact
rendering does not re-elaborate: pp.analyze on the application, sanitizing
the context (let-bound proofs become hypotheses, sorry-tainted and unused
locals are cleared), rendering the signature from the type expression so
that the pp.* flags apply to it, pp.proofs on the statement, and hoisting
closed Prop-typed subterms into binders (only Props, so the statement stays
equivalent by proof irrelevance). Three situations are refused rather than
rendered wrongly: a statement still containing an omitted term, a goal
whose type depends on an earlier sorry, and a multi-goal token whose
recorded goal matches none of the candidates. All failures are reported as
{"error": ...}.
Golden tests cover a tactic sorry with a hypothesis, a term sorry, and the
multi-goal selection and refusal. The README documents the record format,
the payload, the flags and the refusals. Builds and passes the tests on Lean
4.17.0 (the pin), 4.18.0 and 4.27.0-rc1.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
See README diff for description