interactive mode

Stream: lean4

[Dean Young]

Python has of course interactive mode. Would Lean ever find a use of such a mode? And what would that best entail.

[Tomas Skrivan]

What exactly do you mean by interactive mode, maybe repl or Jupiter style notebooks or something else? Lean is an interactive theorem prover, in my opinion it is interactive plenty already.

[Mario Carneiro]

there is also https://github.com/leanprover-community/repl, although admittedly it's not really designed for humans

[Adam Topaz]

Wasn’t there some talk about a lean4 Jupiter kernel?

[Mario Carneiro]

I recall @Bryan Gin-ge Chen had an Observable notebook mode hooked up to lean (3?)

[Tomas Skrivan]

@Arthur Paulino has more human usable repl, but it has been untouched for a long time.

[Wojciech Nawrocki]

The thing is, in Lean the editor is the REPL, so there isn't much need for a standalone program IMO.

[Dean Young]

Python's interactive mode comes in the box with Idle. I'm referring to the mode where you press return after each command.

[Dean Young]

Tomas makes a good point in that Lean is already interactive.

[Tomas Skrivan]

Yes, what you are describing is often called repl(read-eval-print-loop)

Lean is plenty interactive on the proof level but not too much interactive on the evaluation level, you can write bunch of #eval commands but it feels clunky compared to proper repl.

If lean takes off as programming language then there might be desire for a traditional repl as many people seem to enjoy using it.

I personally don't find it useful, I use it in Python only because I found it to be the only way how to get familiar with new APIs. This is not the case for Lean as it is statically typed language. You don't have to actually run the code to make sense of it.

[Mario Carneiro]

I for one hate REPLs. It's okay for one line commands but for anything more complicated you have to deal with the atrocious text editing capabilities of your chosen terminal

[Mario Carneiro]

and TBF it's not nearly as "interactive" as a good IDE

[Mario Carneiro]

having dealt with copying and pasting stuff to the REPL in HOL light and HOL4 I can tell you that even with the best editing key commands it's still horrible to use for large developments. It's like the Coq "waterfall" model, only worse because your state can get mixed up when you re-evaluate old lines

[Tomas Skrivan]

Coq's "waterfall" is the only thing I'm missing in Lean. The eager re-evaluation is a bit annoying when doing heavy computations.

[Dean Young]

I thought the interactive mode could be to do with Lean's tactic mode somehow. Each command would update the tactic state. Is that how it works with the HOLs?

[Reid Barton]

But why would you want to type tactics into a REPL rather than into a .lean file?

[Ruben Van de Velde]

vscode is basically a REPL

[Kyle Miller]

Reid Barton said:

But why would you want to type tactics into a REPL rather than into a .lean file?

Maybe we need a TacticTacticM monad for hypertactics you can use to interactively write tactic scripts (which themselves are for interactively writing proof terms). :upside_down:

[Max Nowak 🐉]

Are we talking about a REPL (in terminal) or about Notebooks (Like Jupyter does it, though VSCode has its own Notebook renderer)? A notebook mode for Lean would be awesome. Maybe it can some day replace python jupyter notebooks for machine learning courses.

[Johan Commelin]

all the core functionality is already there

[Leni Aniva]

Kind Bubble said:

I thought the interactive mode could be to do with Lean's tactic mode somehow. Each command would update the tactic state. Is that how it works with the HOLs?

Isn't that the case for now for emacs and vscode lean mode? Why do you need an extra interactive mode?

[Mac Malone]

Mario Carneiro said:

I for one hate REPLs. It's okay for one line commands but for anything more complicated you have to deal with the atrocious text editing capabilities of your chosen terminal

What would be nice is if there was a single command REPL for a Lean file (perhaps in the infoview) that would allow you to run commands at a given point without editing the file. This would prevent re-elaboration of the file, Git popups, and the risk of forgetting to remove debug code before committing (which has certainly happened to me).

[Mario Carneiro]

seems like it would not be long before such a view starts getting half-baked versions of the features of the main view: syntax highlighting, hovers, abbreviation input...

[Mac Malone]

@Mario Carneiro Sounds great! Maybe call it a scatchpad widget or something.

[Mario Carneiro]

sounds like reinventing vscode

[Mac Malone]

@Mario Carneiro My thought process was that the view code be part of the VS Code extension and thus reuse VS Code components.

[Mario Carneiro]

I don't think it is that easy to embed the literal vscode editor view in a webview

[Mac Malone]

@Mario Carneiro Ah, I guess my wording was wrong when I said "perhaps in the infoview" -- I meant as part of the infoview UI pane, not necessarily as part of the infoview webview.

[Mario Carneiro]

even then it sounds hard. Probably it would be best to just use an actual editor view, similar to the *scratch* buffer used in emacs

[Mac Malone]

@Mario Carneiro Make sense. I confess I still have not internalized a proper model of VS Code Len extension (or VS Code overall), so what you are saying is probably a better way to actually implement what I was suggesting. However, I do still think the idea, regardless of how it is implemented, would be quite useful (and remove some significant pain points).

[Kyle Miller]

A funny simple implementation for a "scratchpad with the context at the current cursor position" would be to have a command to immediately open up a scratch file with the contents of the current file up to that cursor position.

[Damiano Testa]

You already can pass a line and column number to VSCode to open a file at a specified location. At least, you can on Linux.

[Damiano Testa]

$ code --help
[...]
  -g --goto <file:line[:character]>          Open a file at the path on the specified line and character position.
[...]

[Damiano Testa]

In fact, combining this with the output of grep -n is something that I isolated in a function.

[Kyle Miller]

@Damiano Testa The idea is to open up a new file so that you can do the things that Mac mentioned -- sometimes you'd rather explore doing things at a particular point in a file without editing the file itself.

[Kyle Miller]

Or maybe I'm not understanding what you're suggesting. I guess you're saying you can use the command line to implement "open a new file with the first N lines of such-and-such file"?

[Damiano Testa]

No, I think that I am not understanding what is being suggested.

Kyle Miller said:

Or maybe I'm not understanding what you're suggesting. I guess you're saying you can use the command line to implement "open a new file with the first N lines of such-and-such file"?

This is certainly very easy to do with a shell function: grep, sed, awk allow you to select ranges/modify a file, then you can save them to a temp file and open it with code at whatever location you want. This is really very easy to achieve. Is this what is wanted?

[Kyle Miller]

No, it's not :smile: I was thinking more of a VS Code command that would do that from within the editor. It should be easy to do without shell commands.

[Damiano Testa]

I see. I usually implement these things with the shell, since I already know the commands and I find them very simple to use. Also, they do not tie me to VSCode.

[Kyle Miller]

I'm not sure if anyone wants this feature at the moment, but it's interesting to consider as a very simple alternative to a more high-brow design. Plus it's not Lean-specific.

[Kyle Miller]

(This would also be very easy to implement in emacs lisp.)

[Damiano Testa]

Indeed. Also, due to the clumsiness with opening folder vs files in code, I have a shell script that opens the file in the git-root folder of the actual file...

[Damiano Testa]

Basically, in VSCode, the infoview is great, I like the file editor as well. But for everything else, I find that there is no comparison to the shell.

[Kyle Miller]

If there were a way to tell the Lean server that this new file is a prefix of the original file so that it can reuse the cached state, that would be a valuable feature that would greatly improve this simple command.

[Damiano Testa]

Something like saving the oleans for the current file and reuse them for the temp file?

[Kyle Miller]

You know how you can edit a file and it only checks from that point forward rather than re-elaborating the entire file from scratch? There's a cache of command state for every command underlying this. It's not in the oleans.

[Damiano Testa]

ah, something like... stop or save?

[Damiano Testa]

I remember a discussion about this and some implementation of it a while back.

[Damiano Testa]

I cannot find the thread, but save seem to exist:

example : True := by
  save
  trivial

if you hover over save it says

save is defined to be the same as skip, but the elaborator has special
handling for occurrences of save in tactic scripts and will transform by tac1;
save; tac2 to by (checkpoint tac1); tac2, meaning that the effect of
tac1 will be cached and replayed. This is useful for improving responsiveness
when working on a long tactic proof, by using save after expensive tactics.

(TODO: do this automatically and transparently so that users don't have to use
this combinator explicitly.)
``

[Damiano Testa]

I am not finding where save is defined, though.

[Trebor Huang]

To be fair isn't the Python repl less interactive than the Lean VSCode extension? If someone wants to instantly evaluate something, it isn't too hard to add a little button at the end of a lean file, which materializes the #eval for you. It can even be arranged (without any code) that everytime you hit enter a new #eval appears at the beginning of the line.

[David Thrane Christiansen]

For Lean 3, I made a little feature in the Emacs mode that would show command responses inline in the buffer. That made me not miss a REPL. Perhaps something like that would satisfy the concerns here? REPLs have lots of strange semantics, especially in languages with extensible syntax and hygienic macros, as their scoping is a bit... complicated. But hovering to see the result of an evaluation can make it hard to have a mental overview over a session, or to compare different results.

[Alex J. Best]

For reference, this sounds like https://marketplace.visualstudio.com/items?itemName=usernamehw.errorlens (I think lean.nvim does this, maybe with some plugins, too)