Mathlib/Data/Rat/Lemmas.lean

Stream: nightly-testing

[Kim Morrison]

Sigh... I'm having a rough time getting Mathlib on to v4.20.0-rc3 (hopefully the last rc!), and at the least minute I've run into Mathlib/Data/Rat/Lemmas.lean having a broken proof... It's not used, so on #24621 I've just commented it out with an adaptation note.

If someone could sort it out in a subsequent PR that would be great, otherwise I can look tomorrow, but right now I would like to sleep for 4 hours before getting up to get on a plane. :-)

[Eric Wieser]

Is making it an axiom better or wore than commenting it out?

[Mario Carneiro]

is this related to batteries#1225? (the timing is very close, I'm not sure whether the version of batteries you are using includes this PR or not it does include this PR, so this seems very likely)

[Mario Carneiro]

the author contributed a fix so I think it just needs to be cherry-picked to nightly-testing

[Kim Morrison]

(To master, but yes! Thanks for identifying this, I'll see if I can get it queued up this morning.)

[Kim Morrison]

#24625

[Ruben Van de Velde]

Did you mean to change the repository url but not the commit hash for batteries?

[Kim Morrison]

Oops, no.

[Kevin Buzzard]

Eric Wieser said:

Is making it an axiom better or wore than commenting it out?

Making it an axiom opens us up to a drive-by code inspector going "wooah look mathlib has axioms, I thought the whole point was that it was axiom-free"

[Andrew Yang]

I don't think mathlib should add more axioms. Perhaps proof_wanted?

[Mario Carneiro]

Note, this is a temporary issue which has been fixed already. Using an axiom here is fine, insofar as we would not let it hit master

[Mario Carneiro]

commenting it out worked in this case only because the theorem had no users. In the general case we could comment out all the dependencies, but this could be a lot of work to track down and also could end up implicating a huge swath of the library, so axiom is much easier

[Mario Carneiro]

sorry would be even better than axiom (which still has some knock-on effects when it comes to noncomputable marking), but it will cause a build failure (which is fine actually? as long as downstream files are built)

[Kim Morrison]

Just noting that this was commented out (briefly) on master. There axiom is obviously a no go. For nightly-testing, maybe.

[Mario Carneiro]

if we want it not to be a build failure we will need to add some exception for nightly-testing to allow sorry (and we'll probably need this in the end if we ramp up axiom checking on master)

[Mario Carneiro]

I think this should not have hit master, it should have delayed the bump. In this case it was a minor fallout but if it was any worse I think we should just have waited for the fix

[Mario Carneiro]

(I think part of the issue in this case was that batteries had a merged PR in the middle of your bump process; an alternative fix would have been to downgrade the batteries commit you used for the bump to avoid it shifting in the middle of the process)

[Kim Morrison]

I agree with all of the above. This release was an exceptionally difficult one, and this "comment out an unused theorem on master" hack should be avoided in future.