Tooling: Line-by-line checking for lean?

Stream: new members

[Markus de Medeiros]

I come from rocq and I'm used to being able to check my proof script line by line. Is there any way to do the same thing with the current lean tooling? I'm on emacs but may be willing to change for this feature if it's present in some other editor.

[Richard Copley]

The tools will check a proof and give you feedback, if the proof is part of a project. How far have you got? Do you have lean4-mode on your load-path and added to your auto-mode-alist?

[Kyle Miller]

There's no line-by-line checking in Lean (I assume you're talking about the feature where you can set the point up to which rocq checks the proof, right Markus?)

[Markus de Medeiros]

Yes to Kyle-- sounds like what I want doesn't exist then. Thanks anyways!

[Bolton Bailey]

I'm confused, are we not just talking about putting your cursor on the line you are interested in and seeing the proof state at that location? What is it that Rocq has that Lean doesn't?

[Kyle Miller]

There's an editing model other ITPs use where there's a point you set where everything before that point has been checked and everything after is not being checked. (Here's a section of the Proof General documentation about that.)

I usually fake it by inserting #exit nearby to keep things from repeatedly typechecking as I'm editing.

[Markus de Medeiros]

This is helpful, thanks. I've been commenting and uncommenting code but #exit is cleaner .