Getting States from a Theorem without Tracing

[princesspeace]

I'm trying to extract all the intermediate states from a theorem.

Is there anyway to do this without tracing the entire repo it is in and creating an AST?

Also, is it possible to extract the intermediate states of a theorem where has_tactic_proof() is false? Many theorems are a combination of terms and tactics.

[yangky11]

Hi,

Currently, LeanDojo does not support extracting information about a single theorem without tracing the entire repo.

Also, we only extract states before/after tactics (has_tactic_proof() may or may not be true). If you'd like to extract all states, I'd suggest writing a Lean metaprogram similar to what we have done here:

LeanDojo/src/lean_dojo/data_extraction/ExtractData.lean

Line 293 in d399420

match parent with

[princesspeace]

Hi, thanks for the response.

Would this be done just as simple as removing the match i.stx.getKind with ? I'm also curious as to why you don't extract all states - shouldn't these states contain some useful information for training ?

[yangky11]

Kind of, though I'm not 100% sure since I didn't try. In LeanDojo, we focus on tactics as the interaction mode between human/LLMs and Lean. Therefore, we only extract states before/after tactics.

[realharryhero]

Any progress on this @princesspeace ? Ideally, it'd be nice to enter the dojo just given the theorem statement in LEAN.

[darabos]

Check out Lean REPL. It's much lower level than LeanDojo, and lacks most (all? 😅 ) of its conveniences. But it lets you just pass in a theorem as a string with a sorry proof and see and interact with the proof state at the sorry.

[realharryhero]

Sorry for the (very) late reply; that's exactly what I need. Thank you!