quick and dirty mode

Stream: lean4

[Floris van Doorn]

One thing that @Mario Carneiro and I discussed last week is a "quick-and-dirty" mode to compile a Lean file (as an option, maybe disabled by default). Our thought was:

• If you open a new file in VSCode, Lean will compile this file using quick-and-dirty mode. This means that it will try to make sense of the file as quick as possible, without rechecking all details. In particular it will not look at the value of any theorem and just presume that they are all correct. It will check all theorem statements and definition values though.
• After you edit the file, the normal Lean mode will kick in, starting at the place that you edited.

I think this would be very helpful if you want to make a small edit in a huge mathlib file. You cannot cause any errors in lines above your edit, so they need not be checked.

[Leonardo de Moura]

@Floris van Doorn Could you please create a RFC in the Lean 4 repo?

[Floris van Doorn]

Ok! lean4#2326

[Shreyas Srinivas]

Is it related to this issue? https://github.com/leanprover/vscode-lean4/issues/305

[Shreyas Srinivas]

In the sense that they save expensive elaborations until necessary

[Floris van Doorn]

Maybe a little, but I think they're quite different.

[Shreyas Srinivas]

I am guessing this can be implemented in the extension, rather than inside lean 4, with calls to the lsp

[Mario Carneiro]

no, this mode would need to be part of the elaborator state because commands/elabs/tactics in general can do arbitrarily crazy things and so you need some way for the tactics to cooperate

[Mario Carneiro]

another application of the quick-and-dirty mode is for gathering information which does not need the full elaboration result, like getting the AST of a file, for which running all the proofs is a huge waste of time

[Sebastian Ullrich]

Which is also roughly what one would need for large-scale (more than Lean 3) parallelism. In fact, it could be thought of as delaying/not executing parallel parts that are not needed for computing the state at the current position.

[Reid Barton]

It occurred to me recently that the main advantage of Lean 3's "check proofs in parallel" is that, in interactive use, slow proofs higher in the file don't make Lean take longer to check the thing you're working on (unless there are a lot of them).

[Shreyas Srinivas]

Sounds exciting. Something like an asynchronous JIT (in the sense of elaborate/compile when needed)?

[Gabriel Ebner]

• If you open a new file in VSCode, Lean will compile this file using quick-and-dirty mode. This means that it will try to make sense of the file as quick as possible, without rechecking all details. In particular it will not look at the value of any theorem and just presume that they are all correct. It will check all theorem statements and definition values though.

What would it do with this?

variable (a : False) (b : Empty) in
theorem main : 0 = 1 := by contradiction

[Mario Carneiro]

yeah, variables also came up in discussion with @Cyril Cohen about this. Apparently coq uses Proof using a b c. as a variant on include which makes it possible to compile proof bodies separately

[Mario Carneiro]

but lean 4's current strategy for calculating variables based on usage is a big problem for parallelization

[Patrick Massot]

Couldn't we simply get back Lean 3 variables?

[Mario Carneiro]

I agree, except that instead of lean 3 variables we do "variables are based only on the signature, not the body" which is 50% more sane than what lean 3 actually does

[Patrick Massot]

You mean even when the body uses pure term mode?

[Mario Carneiro]

yes, term mode vs tactic mode was never a particularly sensible dividing line and it is even less sensible in lean 4 where these are commingled

[Patrick Massot]

I agree.

[Mario Carneiro]

hm, now I wish variable! was available as a combination of variable and include, because it's silly for variable (x : A) in ... to not include x in the statement

[Gabriel Ebner]

There's quite a few macros that rely on that behavior.

[Mario Carneiro]

My contention is that if the user writes variable (x : Nat) in def foo (y : Nat) : Nat := ... then x should probably be included in foo

[Mario Carneiro]

if macros use variable ... in without knowing whether the variable will be used and hoping for it to be removed if not used, then that can be migrated to a different command. Alternatively, we just tell users to always use variable! in this position and have a linter warning for unused variable ... in declarations

[Floris van Doorn]

Gabriel, you're right that this proposal doesn't work with the current variable command...
Let's continue that discussion to a different topic.

[Gabriel Ebner]

Another relevant complication: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Change.20of.20the.20proof.20of.20.60WellFounded.60.20causes.20timeouts/near/376670923