As far as I know, the default configuration for the Lean VSCode plugin checks the code continuously, and so even when the user is in the middle of typing an expression, Lean will immediately report a syntax error. In contrast, proof assistants like Agda defaults to checking the code only when the user presses a key combination.

I understand that this can be changed through configuration, and you can temporarily "freeze" the proof state. But what is the design consideration behind this choice? In what ways do users have better / worse experience using continuous checking?

  • $\begingroup$ I think this is a good question, but I think it could potentially be better if framed more broadly about the pros/cons of continuous vs on-demand checking, unless there's anything specific about Leans' implementation that you're interested in? $\endgroup$
    – Josh
    Commented Feb 19, 2022 at 15:09
  • $\begingroup$ @JoshChen I was subconsciously thinking that only Lean has this as a default feature. AFAIK Isabelle also has this? $\endgroup$
    – Trebor
    Commented Feb 19, 2022 at 15:18
  • $\begingroup$ I don't really understand this question, as I mention in my answer. Doesn't continuous checking beat "check when I say so" hands down? $\endgroup$ Commented Feb 19, 2022 at 16:57
  • 1
    $\begingroup$ I feel like the question we are trying to get at is “why isn’t this feature in Agda (or Coq)”? Is it that it is hard to implement? Not important enough to implement? Or undesirable to users? $\endgroup$
    – Jason Rute
    Commented Feb 19, 2022 at 19:52
  • $\begingroup$ It is a bit inaccurate to describe what Lean is doing as just "checking". Technically, it is re-elaborating the file, a process which includes a bundle of other actions beyond syntax and type checking. For example, an #eval launchNukes statement will be re-evaluated each time the file is "checked" (launching nukes every time xD). I don't have much experience with other provers, so I am not sure if the checking in other prover is similarly more involved or if, on the other hand, they just do syntax/type checking. $\endgroup$
    – tydeu
    Commented Feb 27, 2022 at 2:02

4 Answers 4


In 2017 and 2018 I learned three languages, Rust, Scala, and Lean. All three are similar in that they enforce strong typing constraints in order to guarantee the correctness of code which can be checked at compile time instead of run time. They also use advanced features such as type classes and macros to make the language more flexible, but at the same time “safe”. All this makes compiling take longer, but if it does compile (or type check) then you know it has a better chance of working as desired.

When I first tried Rust, I just used a basic editor with syntax highlighting, and the command line to compile and run my code. It was incredibly frustrating. The compiler complained about one thing and I had to go back and fix it. I often had to resorting to tricks to learn what the type of a variable was.

When I learned Scala for work, it was strongly recommended I use the IntelliJ IDE which has an amazing Scala interface. Unlike my Rust experience, the IDE made it so much easier to learn Scala and progress. Most importantly the turn around time was much faster. Instead of waiting for a whole file to compile, I could just see instantly when I had a compile error. It is basically the same as modern continuous spell checkers. The error is unobtrusive—to me at least—and I can address it then if I know the problem (for example I made a typo) or later if I don’t.

It feels collaborative. At every point the IDE is helping me with all the little things. What is the type of this variable? Click and see? What is the order I need to put in arguments to this function? Click and see? Did I misspell something or use the wrong function? It will let me know. Is my code going to compile? I already know. If it has no red squiggles then yes.

A coworker of mine once confessed that she used to think “IDEs are for chumps”, but after her experience with Scala and IntelliJ she feels very different now.

After that Scala experience I can’t imagine not using these features when programming. I now use IDEs with language server features even for Python programming. It makes me much faster. The editors catch common typos of mine like swapping == and =. It also makes it easy to change a variable name, or refactor a piece of code without fear that I’m going to make a ton of painful little errors. It gives me a lot more power. When I returned to Rust, I looked into the Rust language server (which plugs into IDEs like VS Code). This made a night and day difference. I now am able to see not only my errors, but also get a better feel for how Rust works and what things are ok and not okay to do. There is almost zero delay between typing and feedback.

I’ve been focusing on non-theorem provers in my answer since I don’t want to make this a Lean verse “the others” post. Lean happens to have continuous checking, but so do many of the new proof assistants like Arend and Metamath Zero. It, in many ways, just seems like an obvious choice, at least for proof assistant designers who can afford to put in the time to make it work, and users who generally like interactivity. (Of course, users like Dima Pasechnik who prefer the command line would understandably hate being forced to use an IDE. While users, like myself, now get annoyed when I have to push a key command to check another step of code in an older theorem prover.)

Also, Andrej Bauer makes a good point that the current systems which don’t have continuous checking are perfectly usable. This one feature is likely not a reason to switch tools. Nonetheless, I think all heavily used computer languages will have this feature in the next 10 years (including Agda and Coq). There are just a large number of users who like it, and it seems for them (at least for me for sure) to increase productivity and mastery of the language.

Now, why don't other theorem provers like Agda and Coq have this asynchronous continuous checking? I can only speculate, but as Andrej’s answer suggests, they likely were created before continuous checking was feasible and common. Also, it is likely not the easiest thing to implement and likely harder to add on after the fact. (Creating continuous checking language servers for Python for example is a big business, including PyCharm (the sister to IntelliJ) as well as VS Code’s proprietary Pylance plugin. This suggests that a lot of work must go into making these quality tools.). Nonetheless, it does look like both Agda and Coq are adding support for the language server protocol (and maybe with that continuous checking). See here for Agda. See here for Coq.

Also, it isn’t enough to have continuous checking. It has to be performant. Even Lean’s checking can sometimes stall. This is especially common if one is looking at a file deep inside mathlib. (One consideration with continuous checking is what to do if a file is being edited and not saved yet. VS code doesn’t save edits automatically but IntelliJ does. I wonder if this impacts how the continuous checking works in each IDE.) In Lean, if a file is open and being edited, then any dependencies on that file need to be rechecked if they are used in another open file. Sometimes Lean will even recheck the open file when it is not being edited which is annoying. This can cause massive performance issues in Lean that require a restart. I’m sure it can be fixed (edit: and Sebastian Ullrich informed me that it is fixed in Lean 4), but it does show the downsides of continuous checking in that it is hard to get right. In general, no continuous checking is better than bad continuous checking.

I’ll just end with another comment about IDEs. I think IDEs (especially "native" apps like VS Code and IntelliJ, but also Emacs and Vim) have come a long way in the past 5 to 10 years. For example, it used to be that the only way to do remote development (i.e. you can work with a theorem prover or programming language on another server) was to use the text-only versions of Emacs or Vim from the command line. But now seamless remote development in a GUI environment is also available in VS Code (for free) and IntelliJ (for a price). Further, VS Code, IntelliJ, Emacs (and I assume Vim) also have good git integration and a built-in terminal for whenever you need the command line.

Similarly, the language server protocol has also made it a lot easier to integrate continuous checking tools with all IDEs. For example, any editor which supports LSP can use Rust’s language server. There is no need for a separate Rust plugin or Rust editor. This can move the development of these tools back to the language designers and make them integrate tighter with the compiler. (Edit: Sebastian Ullrich pointed out that to take full advantage of the Rust analyzer, which goes beyond LSP, one still needs a separate plugin, and the same is true for Lean and other ITPs.)

  • 2
    $\begingroup$ I would consider Emacs an IDE, not a command-line tool. $\endgroup$ Commented Feb 22, 2022 at 19:27
  • $\begingroup$ @MikeShulman Emacs is definitely an IDE. However, it is also a CLT in that you can use it directly from the command line in say a text only remote ssh session. That is an old argument against using "native" IDEs like Sublime, IntelliJ, VS Code, etc. The argument goes you can't use them to directly work on another machine, so you better get used to using Emacs or Vim. However, my point is that this isn't a valid argument anymore. I can use VS Code to do seamless remote development. (I'll rephrase my answer. In particular I think Emacs and Vim have also come a long way, partly due to LSP.) $\endgroup$
    – Jason Rute
    Commented Feb 22, 2022 at 19:44
  • $\begingroup$ Note that rust-analyzer extends the LSP such that you do need an editor-specific plugin after all to make the most of it github.com/rust-analyzer/rust-analyzer/blob/master/docs/dev/…. This is of course doubly true for any ITP, which tend to require user interfaces quite different from other languages and not covered by the LSP (example: Lean 4 github.com/leanprover/lean4/blob/master/src/Lean/Data/Lsp/…). $\endgroup$ Commented Feb 23, 2022 at 11:41
  • $\begingroup$ Btw, you might be relieved to hear that in Lean 4, edits do not automatically affect other open files. That seemed like the saner default behavior to me, and no users have revolted... yet. $\endgroup$ Commented Feb 23, 2022 at 11:43
  • $\begingroup$ Edited my answer to reflect all the comments. $\endgroup$
    – Jason Rute
    Commented Feb 23, 2022 at 12:39

I can report on my personal user experiences with Coq, Agda and Lean:

  1. Coq checks an initial segment of the file (and it does not matter what garbage fills the rest of the file). The Emacs mode can be set up so that Coq automatically checks the next input as soon as the user types in the period . (which indicates the end of the command). I don't like that, it feels like the machine is rushing me. I much prefer the mode in which I tell Coq what precisely to check.

  2. Agda checks the entire file. The user may request re-checking of the file, or they may just submit the solution to one of the goals (in which case, I think, it only checks the submitted fragment, but I am not sure). In practice, checking the whole file is not a problem. If there is garbage at the bottom of the file, it has to be commented out, and Agda mode has shortcuts for doing so.

  3. Lean is designed to work more like the programming language IDEs that can check fragments of code, rather than whole files. By default it proactively checks the user input, which works well in most situations. The user may also choose a more passive strategy.

One should understand that Coq is much older than Agda, which is much older than Lean. They were designed in different times when people did not have computers with $2^n$ cores and $2^{2^m}$ kilobytes of memory. It is fair to say that Lean's interface is natural evolution of the older interfaces.

I can tell you from experience that telling the machine "please check this here" is no big deal. It feels completely natural to tell Coq up to what point it should check the file. Telling Agda when to check things gives me the feeling of being in the driver's seat. Lean's eager checking gives a different feel, it is more like having someone looking at what you are doing and giving you instant feedback. I am pretty sure beginners would in general prefer Lean's mode, as they do not have to learn when to tell the proof assistant to look at their work (but they learn quickly, at least my students do).

There have been occasions when I had to turn off Lean interactive mode because it went off and started compiling huge amounts of stuff, and eventually hogged available memory. But this was a rather specific situation when I was experimenting with processing a very large number of small files (thousands). It would be nice if there were a way of telling Lean "never ever check anything in this folder unless I tell you to" (for all I know it can do that).

In conclusion, I would say that the precise details of the interactive mode are not very important, but I cannot imagine working non-interactively.

  • 2
    $\begingroup$ Lean's parser seems to be surprisingly tolerant of errors, usually being able to resynchronize itself even within expressions. I wonder if this, beyond more powerful computers, is partly responsible for feasibility of the feature -- are Coq and Agda like this? I last used Agda years ago, and I remember it being very Haskell-like with parse errors. $\endgroup$ Commented Feb 19, 2022 at 18:45
  • $\begingroup$ Extra info: Isabelle's IDE jEdit checks up to the point, going through the last completed command (have something, apply tactic), issuing an error message if the input for the command is incomplete. $\endgroup$ Commented Feb 19, 2022 at 20:28
  • $\begingroup$ @KyleMiller: in the recent years the traditional compilers have been moving in the direction of processing fragments rather than whole files (see LSP). Agda and Coq were designed before this trend, so they don't do that, although they both have the ability to process a file incrementally. Lean is much newer and it supports the modern kind of interaction with an IDE. $\endgroup$ Commented Feb 19, 2022 at 22:09
  • 2
    $\begingroup$ I don't think it's always true that checking the whole file is not a problem in Agda. I've definitely encountered situations where re-checking the whole file will take several minutes: not something I want to do with every line of code I write! $\endgroup$ Commented Feb 20, 2022 at 4:48
  • 1
    $\begingroup$ I installed the vscode mode and after using it for 3 minutes it looks perfectly good. $\endgroup$ Commented Feb 21, 2022 at 12:57

The following is more of a response to Kevin's answer than the answer to the question.

Lean's VSCode IDE-like interface aggressively over-instruments the interaction with the user - this is and always will be a subjective view.

All these auto-completions, popups, quick changes in syntax highlighting might be extremely distractive for some users. E.g. I find I can only work with VSCode - even if I use its TeX plugin writing a paper - in "zen mode" - where most of menus and tabs are hidden, and it still is often too much interaction.

It is naive to think that as much interaction as possible is the best for everyone.

  • $\begingroup$ As I said in a comment above, is this the reason Agda (and Coq) doesn’t have a feature like this? Or is it for some other reason. $\endgroup$
    – Jason Rute
    Commented Feb 20, 2022 at 12:35
  • $\begingroup$ users who prefer CLIs to IDEs are probably a smallish minority, but it doesn't mean they have to suffer. I'm not against IDEs in general, but customisation is important. $\endgroup$ Commented Feb 20, 2022 at 15:43
  • $\begingroup$ Don’t all these tools including Lean have CLIs? $\endgroup$
    – Jason Rute
    Commented Feb 20, 2022 at 17:31
  • $\begingroup$ No, my point is that some IDEs (these with a lot of "bling") are unbearable to use for people who might be fine using (usable) CLIs. $\endgroup$ Commented Feb 20, 2022 at 19:27
  • $\begingroup$ So you are saying tools like Lean which focus on language servers have unusable CLIs which hurt users like you? $\endgroup$
    – Jason Rute
    Commented Feb 20, 2022 at 20:28

I do not really understand this question. The only advantage which "check up until this point and then stop" has over continuous checking is that you get to freeze the state and examine it whilst writing your next line of code. However if this ability is incorporated into your continuous checking system then you have a system which has all the benefits of "check up until this point and then stop" whilst retaining the many benefits of continuous checking (i.e. making it much easier to write code).

Lean with VS Code offers this functionality. You can "pin" states if you want, i.e. keep the state you want to see (e.g. because you want to refer to it whilst thinking about what you want to write next) whilst also simultaneously enjoying the benefits of continuous checking (i.e. you can see two goal states at once when a state is pinned; your current continuously-checked goal and the pinned static one). Pin a state by hitting the pin icon above it.

Lean with VS Code also offers the ability to pause the output of continuous checking and to turn it off completely, however these are options which I use far less often.

  • 5
    $\begingroup$ With respect Kevin, this answer reads more like another ad for Lean (which has its place, just not here) instead of an attempt to seriously compare and explain the design decisions made in choosing continuous over non-continuous checking. $\endgroup$
    – Josh
    Commented Feb 19, 2022 at 16:12
  • 3
    $\begingroup$ It's not a competition between Lean and all the other proof assistants. $\endgroup$ Commented Feb 19, 2022 at 16:50
  • 1
    $\begingroup$ Point taken Josh: whilst I agree with Andrej, I will edit and I'll leave a comment under the question explaining why I think it's in some sense lousy. $\endgroup$ Commented Feb 19, 2022 at 16:52
  • 1
    $\begingroup$ OK: edited. If you're still not happy then feel free to ask me to delete (perhaps explaining why) or feel free to edit yourself; I don't care about internet points, I am just trying to write a helpful answer to what I see as a rather weird question; if someone can point out some benefit to a non-continuous-checking system over what I am used to then this would change everything. $\endgroup$ Commented Feb 19, 2022 at 16:59
  • 2
    $\begingroup$ When writing e.g. the statement of a theorem I find it really helpful to be told immediately that I've made a syntax error. Now I have understood where the red lines occur and in particular if they're there because I'm in the middle of a sentence or if they're there because I goofed, I could not imagine going back to a non-continuous-checking system. As I say I still don't understand this question. It's like asking "I want to get from A to B as fast as possible. My two options are a fast car, and a slower car. What are the advantages of the slower car?" You're saying "it's only a bit slower". $\endgroup$ Commented Feb 19, 2022 at 17:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.