lean --make doesn't show sorries the second time round

Stream: general

[Bhavik Mehta]

Running lean --make on a file with sorries gives the warnings, but only the first time it's run; is there a switch I can do to make it show the warnings every time?

[Kevin Buzzard]

You can remove the olean as a workaround

[Bhavik Mehta]

I guess this works but I'd really rather not make things recompile again

[Bryan Gin-ge Chen]

You could rename the oleans and then rename them back...

[Reid Barton]

Import it from another file?

[Reid Barton]

which warnings do you want?

[Reid Barton]

If you want to know about all the warnings then of course lean needs to rebuild the file, right?

[Bhavik Mehta]

Right but if it's already built then I should be able to get the warnings? For errors, if I do lean --make twice I get all the errors both times, but not for warnings

[Reid Barton]

If there are errors then Lean doesn't write an .olean file I think, so this is a different situation

[Reid Barton]

Bhavik Mehta said:

but not for warnings

I don't understand what this means

[Reid Barton]

do you mean if there are only warnings?

[Bhavik Mehta]

Yeah if there are only warnings

[Bhavik Mehta]

Reid Barton said:

If there are errors then Lean doesn't write an .olean file I think, so this is a different situation

Ah I didn't know this, I see

[Bhavik Mehta]

image.png By the way, this is what I wanted it for - it's nice to see at a glance which files are broken by a mathlib bump in a project

[Johan Commelin]

@Bhavik Mehta Hey, that looks nice! Are you preparing a PR to leanproject?

[Bhavik Mehta]

I can, but it's pretty slow and pretty hacky

[Bhavik Mehta]

I didn't want to recompile everything each time it's run so it searches for the bytestring "orry" in the compiled oleans to check for sorries

[Johan Commelin]

lol, nice hack

[Bhavik Mehta]

luckily none of my lemmas are called worry

[Johan Commelin]

Wait till we start formalising self-driving cars. That will give you lots of lorry and worry...

[Jasmin Blanchette]

Seriously, worry might have been a better name for sorry. In Isabelle, where it's from, we also have oops, for "forget this proof attempt". A common mistake is to mix up oops and sorry, ending up with a "lemma" one knows is unprovable. The names are clever and funny, but perhaps too clever for their own good.

[Johan Commelin]

We should take more advantage of the fact that lean supports unicode: I suggest replacing sorry with :oops: :scream: :boom: :see_no_evil:

[Simon Hudon]

@Johan Commelin I think @Jasmin Blanchette was recommending less cleverness and more clarity.

[Patrick Massot]

I think Johan understood.

[Gabriel Ebner]

Historical side remark: as you all know, the synthetic sorrys that Lean inserts for syntax errors are printed as ⁇. Originally I wanted to print them as 💩, but then quickly switched to ⁇ to make it look more professional.

[Kevin Buzzard]

/me puts his glasses on

[Kevin Buzzard]

eew