Lean Blueprint Proof Extraction

Stream: general

[Frederick Pu]

Does anyone know how lean blueprint actually extracts proof information? I looked in the source code and I can only seem to style tags

[Patrick Massot]

I'm afraid there is nothing I can do with such a vague question.

[Frederick Pu]

Patrick Massot said:

I'm afraid there is nothing I can do with such a vague question.

How do I get the list of tactic states used in a particular proof? Also how do I get a list of all proofs in a particular file? Is this using the RequestM monad?

[Patrick Massot]

Lean blueprint does not extract tactic states. Are you mixing up names and thinking about informal Lean?

[Frederick Pu]

Patrick Massot said:

Lean blueprint does not extract tactic states. Are you mixing up names and thinking about informal Lean?

Yeah. Do you happen to know how informal lean does it?

[Frederick Pu]

Frederick Pu said:

Patrick Massot said:

Lean blueprint does not extract tactic states. Are you mixing up names and thinking about informal Lean?

Is it this repo? https://github.com/leanprover-community/format_lean

Yeah. Do you happen to know how informal lean does it?

[Patrick Massot]

No, format_lean is yet another project and it is completely dead since it is a Lean 3 tool. The repo of informal Lean is not yet public. But you can take inspiration from how Lean Ink does it.