about compilation

Stream: general

[Kenny Lau]

why do we need to re-compile the file as well as all the files that depend on the file even if all we did is adding a space?

[Kenny Lau]

or if we just change proofs?

[Sebastian Ullrich]

Because the alternative is so complex that not a single ITP I know does otherwise

[Kenny Lau]

could you elaborate?

[Sebastian Ullrich]

For adding a space, the short story is that we should compare the old and new AST's contents to decide if there was a semantic change. But Lean 3 does not even have ASTs for full definitions.

[Sebastian Ullrich]

If you change a proof, that is an actual change that results in a different .olean file. So now you need some extra logic to tell dependent files that while the .olean file has changed, they shouldn't care about that.

[Sebastian Ullrich]

etc. pp.. It's not impossible, and we have at least discussed whether we could do something in that direction in Lean 4, but it's not at all trivial

[Kenny Lau]

what is AST?

[Sebastian Ullrich]

abstract syntax tree

[Kenny Lau]

what makes ITP different from ordinary programming languages that can do that?

[Kenny Lau]

(that's probably a stupid question)

[Johan Commelin]

Ordinary programming languages would recompile everything if you changed a "proof", because the don't have "proof"-irrelevance. All their function definitions are data.

[Sebastian Ullrich]

Incremental compilation is even harder in "ordinary languages" where all definitions live in the same mutually recursive context. The Rust people have been working on it for multiple years and are still not done.

[Bryan Gin-ge Chen]

Very naïve question, but why are the proofs stored in the .olean files? Since there is proof irrelevance, isn't it true that they won't be read again?

[Bryan Gin-ge Chen]

I guess you didn't say that the proofs are stored in the .olean files and perhaps it's not true. But then my question is why should changing proofs change the .olean files?

[Keeley Hoek]

The proofs are not needed, but they witness the fact that a proof exists. I think the idea with the olean files was something that could both have its program-parts executed, and be run through a Lean checker in order to check correctness.

[Sebastian Ullrich]

Yes, the proofs are consumed by external checkers. They could be move to a separate file, but it doesn't help much: Even just inserting a newline somewhere changes position information in the .olean file. So you really need a more sophisticated dependency system than on the file level.

[Simon Hudon]

I think the easiest thing to do would be to get a build system to hash the olean files and consider a change only when the olean's hash changes

[Simon Hudon]

Changing a proof would still trigger a rebuild but adding a space wouldn't