Stop compiler at first error?

Stream: general

[David Loeffler]

Is there a way to compile a single file (like "lean --make") but stopping at the first sign of an error, rather than continuing with the compilation through to the end of the file?

[Scott Morrison]

I don't think so. Perhaps it might be possible to read stderr and abort if you can read anything from it??

[Eric Wieser]

I think we do this in CI?

[Eric Wieser]

https://github.com/leanprover-community/mathlib/blob/master/scripts/detect_errors.py#L40

[Adam Topaz]

Indeed env LEAN_ABORT_ON_PANIC=1 lake build

[Adam Topaz]

(For lean4, that is)

[David Loeffler]

Adam Topaz said:

Indeed env LEAN_ABORT_ON_PANIC=1 lake build

Good to know this exists in lean4. The context is that I'm hacking together a script to detect unnecessary import statements, because flattening the import hierarchy will make life easier during the porting process. So applying it to mathlib4 is not useful (yet).

[David Loeffler]

(We already have leanproject reduce-imports but that only detects import statements in the transitive closure of other imports. I want to detect imports that do actually have an effect, but where the stuff that's ipmorted doesn't get used.)

[Adam Topaz]

For lean3 it seems you have to do what Scott suggests using the script Eric mentioned. You can take a look at how mathlib3 CI does this.

[Eric Wieser]

David Loeffler said:

I want to detect imports that do actually have an effect, but where the stuff that's ipmorted doesn't get used.

I assume you're aware that the graphs in #mathlib4 > port progress (but not the ones on #port-dashboard) already do this?

[Eric Wieser]

because flattening the import hierarchy will make life easier during the porting process.

I'm not sure how true this is; while it might mean some files can be ported sooner, it won't have much effect on the overall speed of porting all of mathlib, as we're far beyond the bottleneck now

[Eric Wieser]

Where it might help is that fewer imports mean faster simp calls due to fewer available lemmas

[Eric Wieser]

But I think most of our timeout problems are caused by unreasonably nasty unification problems related to typeclasses, not large simp lemma sets

[Eric Wieser]

That said, the tool you're describing does still sound useful to have in the long run :)

[Mario Carneiro]

is that actually observed in lean 4? The way discrimination tree indexing works means that it is almost completely indifferent to having more lemmas in the simp set

[Mario Carneiro]

although a larger simp set does mean more initialization time at import

[David Loeffler]

Eric Wieser said:

David Loeffler said:

I want to detect imports that do actually have an effect, but where the stuff that's imported doesn't get used.

I assume you're aware that the graphs in #mathlib4 > port progress (but not the ones on #port-dashboard) already do this?

Do they really? I wasn't aware of that. How exactly is this detection done?

[Mario Carneiro]

it checks the declarations in the file to see whether they use any declarations in the target file

[David Loeffler]

Mario Carneiro said:

it checks the declarations in the file to see whether they use any declarations in the target file

I wonder if it might be useful to extract that check and run it as part of the CI test cycle (at some point in the future)

[Mario Carneiro]

It is expensive

[Mario Carneiro]

plus the results are not so easily interpretable as to be usable in a CI check

[Adam Topaz]

Mario, this isn’t really related, but how can I make lean4 emit errors in json?

[Eric Wieser]

Mario Carneiro said:

It is expensive

This is also the reason that #port-dashboard does not attempt this

[Adam Topaz]

The json flag doesn’t exist in lean4 as far as I know

[Mario Carneiro]

that's an open issue IIRC

[Mario Carneiro]

there is no such flag

[Eric Wieser]

Does the flag belong in lake or lean?

[Mario Carneiro]

both?

[Eric Wieser]

Does lake invoke lean as a subprocess, or hook into it directly somehow?

[Mario Carneiro]

lake definitely wants lean to emit json

[Mario Carneiro]

it calls it as a subprocess

[Eric Wieser]

I made a thread about the --json argument, but I don't know if I've seen an issue

[Eric Wieser]

It might be worth tagging that mathport-high-priority, since it means we can get better CI feedback on mathlib4 PRs