Sebastian's WITS 23 talk

Stream: general

[Mario Carneiro]

Scott Morrison said:

Slides from Sebastian's keynote at WITS 23.

He talks about public signatures for Lean modules, private import and import ... for meta. I'm not sure if there will be a video.

@Sebastian Ullrich This reminds me of a feature I have been considering while watching mathport compile 2/3 of mathlib: We could have a noncomputable import Foo.Bar, which means "don't load any compiler IR from this file". The effect is that from the perspective of the importing file only all declarations in the module are noncomputable, but this is has no effect on transitive dependencies, unless one of the declarations in the current file becomes noncomputable as a result. You can still import other modules computably, and an imported module is considered noncomputable only if there are no regular (transitive) imports of the file. The idea is that if lake sees a noncomputable import it knows that while the lean files are in a dependency relationship, the c files are not, which hopefully significantly decreases the number of c files that have to be compiled when you have a project like mathport that has some very "advanced" imports but there is almost no actual compilable code involved so all the Compiling is pointless.

[Mario Carneiro]

(Note that mathport currently depends on about 2700 files in mathlib right now, and while lake exe cache get can download the oleans, you still have to compile the .c -> .o files locally. I think this takes about 5 minutes. The reason it has to import so much is because it needs the syntax declaration for every tactic in mathlib, via the Mathlib.Mathport.Syntax file, and these syntax declarations are littered throughout the code, including things like the witt vector tactics that sit on top of a sizable fraction of mathlib.)

[Sebastian Ullrich]

@Mario Carneiro You still want to import some IR in order to actually run those notations, no? But if that only needs to happen at build time and no mathlib parts should be part of the final binary, then that sounds exactly like a job for a phase separation system.

[Mario Carneiro]

Well, the constraint is that you can't produce any declarations that depend on the upstream compiled code

[Mario Carneiro]

you could still make use of the IR at build time

[Sebastian Ullrich]

We seem to be saying the same thing

[Sebastian Ullrich]

A recording should be available eventually

[Mario Carneiro]

@Sebastian Ullrich Same thing meaning that noncomputable import maps exactly to one of your proposed import variants? Is this what import Foo for meta is supposed to do?

[Mario Carneiro]

That syntax implies that you are considering other kinds of imports. Could you list all the variants you have considered?