building a single file in mathlib

Stream: lean4

[Johan Commelin]

I was trying to do an automated git bisect on mathlib. But I realize that in Lean 4 I no longer know how to build a single Lean file. Can someone please educate me?

[Damiano Testa]

lake env lean [file]
## or
lake build [file]

one of the two takes a path, the other the same format as import -- can't remember which one. Should be done from the root dir, I think.

[Johan Commelin]

Thanks

[Damiano Testa]

I think that build will build the o/ileans, the other will not.

[Johan Commelin]

The first seems to do what I want (-;

[Sebastian Ullrich]

These are not the same! Only the latter command will rebuild dependencies and save .oleans

[Johan Commelin]

I want to count heartbeats for some decl. So I don't think rebuilding is necessary, right?

[Johan Commelin]

I'm grabbing oleans from the cache

[Sebastian Ullrich]

Then it's fine

[Julian Berman]

Maybe this is a separate question, but neither of the two work for a case where you have a directory not listed as a package in the lakefile -- is there a way to do that perchance? The use case is I have some directory inside my local mathlib repo where I have random self contained files I've played with that depend on Mathlib. It'd be convenient if there was a way to say "build Scratch/foo.lean", which doesn't work as-is because Scratch obviously isn't in Mathlib's lakefile as a package. But lake / lean must have all it needs to do that, because opening/editing files in there works fine and builds what's needed at edit-time, so I mostly haven't bothered and rely on this being built in the editor -- is there some CLI way to do it?

[Matthew Ballard]

It might also be ergonomic to use

time -v lake env lean --profile X/Y/Z.lean

if you don't want to jump into the editor ever.

[Johan Commelin]

During the bisect, I just edited the file at the start, and git was smart enough to keep the edit in place all the way till the end of the bisect. So I didn't have to edit much either. But I'll keep this in mind.

[David Loeffler]

While we're on the topic of building single files:

IMHO, the fact that lake build expects input in the same format as import, delimited with ., makes it un-ergonomic to build single files from the command line – it defeats the shell tab completion for filenames. This is a regression from lean 3, where lean --makehappily accepted a file path. Can I take the opportunity to request support for tab-completion in lake build?

[Johan Commelin]

cc @Mac Malone

[Mac Malone]

lean4#2756

[Damiano Testa]

For a temporary fix, take a look at

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/fastest.20way.20to.20copy.20module.20name.20of.20the.20current.20file.3F/near/401710404

(I'm on mobile, I hope the link works!)

[Kevin Buzzard]

Regarding @Julian Berman 's situation (also a regression from lean 3), I fixed this locally by moving my scratch directory into the Mathlib directory (which makes it slightly harder to find, but at least I can now compile on command line)

[Julian Berman]

Bleh yeah reasonable, I guess I could do that too, it's just slightly easier to commit accidentally, but I'll gitignore.

[Kevin Buzzard]

I edit my .git/info/exclude rather than goofing around with mathlib's .gitignore