faster lean --make

Stream: new members

[Joachim Breitner]

When changing files down in the dependency chain, or after pulling master on a slow or expensive internet connection (so better no leanproject get-cache), I run lean --make src/file/I/plan/to/edit.lean before opening that file in vscode, and that can take a while.
Does lean --make support a “fast mode” where it skips checking proofs in dependent files? At least those irrelevant proofs of Prop things? Or is that fundamentally not possible.

[Eric Rodriguez]

maybe --old is what you're looking for? here is an overview of it

[Joachim Breitner]

Thanks!
Not exactly what I had in mind, but also a good trick. I assume that new lemmas will still be visible through transitive imports, even if the intermediate module’s old lean file was still used?

[Joachim Breitner]

lean --help calls it --old-oleans. Is that the same? Should I update the docs to use the full flag name to avoid confusion?

[Joachim Breitner]

What I had in mind could maybe be rephrased as: “Replace every proof of a lemma that produces a Prop and has it’s result type fully spelled out with by sorry”

[Eric Rodriguez]

huh, I thought it was just --old but the code disagrees image.png

[Yakov Pechersky]

Do you want to skip checking proofs, but still check definitions? Because if you skip those, your proofs that use defeq will fail.

[Joachim Breitner]

Right, that why I (very naively, I'm very new here) suggest that only for proofs that are irrelevant for downstream modules.

[Arthur Paulino]

I'm afraid namespaces and @[simp] lemmas make this task more challenging than we'd like, because building such dependency chain becomes a semantic task rather than purely syntactical

[Joachim Breitner]

Hmm, I don’t see it yet, can you elaborate?

[Arthur Paulino]

Suppose you have a file A in which bar is declared in the namespace foo. Then file B imports A and opens foo in order to use bar. Now, in the file C, bar is declared openly, even though it also imports A. B and C import A and make use of bar (without dots), but they're talking about different declarations of bar

[Arthur Paulino]

It might be possible to figure that out with some meticulous parsing, but it doesn't look like an easy task to me.

And in the case of simp lemmas, it's really impossible to know they're being used just by parsing text files

[Reid Barton]

Using a lemma does not mean you necessarily need to know the proof of the lemma though. simp [foo.bar] doesn't care about the proof of foo.bar. The question is what would break if we replaced all proofs of lemmas by sorry.

[Reid Barton]

I think this was discussed long ago but I don't remember if there was a conclusion about whether a feature like this could work.

[Joachim Breitner]

Right, I am _not_ talking about only checking the “obvious dependencies” on a symbol level of the file I care about (that is hardly possible with simp and instances etc.), but about skipping the checking of (all irrelevant) proofs.
Although that’s done in parallel anyways, isn’t it? So maybe it wouldn’t help that much.

[Alex J. Best]

Joachim Breitner said:

lean --help calls it --old-oleans. Is that the same? Should I update the docs to use the full flag name to avoid confusion?

You could update the doc if you like, it seems most people here just call it old though, as getopt_long is used, unambiguous abbreviations are allowed in command line args. Even the original PR description https://github.com/leanprover-community/lean/pull/208 calls it old :grinning: