Code compilation is setup dependent

Stream: new members

[Aatman Supkar]

I had to ask another question, and for that I tried pasting my code here to edit before asking here, to create an MWE. However, code which was compiling properly on my device (which uses version 4.15) was generating errors (mostly with the simp tactic not closing goals). Is this supposed to be happening? If yes, how am I supposed to post MWEs? I doubt the code is any help if our infoviews don't agree on what it shows...

[Eric Wieser]

I think unfortunately the answer is "update to a newer Lean version", at least in cases where you notice that the new version does something different

[Eric Wieser]

( The fact that you checked your code did the same thing on the web editor before asking is great through!)

[Aatman Supkar]

So to ask for help here, should I migrate to 4.18? Also, if simp closes a goal in an earlier version of Lean, shouldn't it continue to do so in a later version? I have simp calls at the end of a proof which aren't closing goals either, and it just feels strange.

[Aatman Supkar]

Actually, the weirdest difference of them all is perhaps the fact that import Mathlib.Order.CompleteLattice is a perfectly valid import on my device, but not on the web. (It probably doesn't matter now because I found this import redundant just right now, but it's still bizzare to me.)

[Kevin Buzzard]

That's not weird, people shuffle files around all the time (e.g. they break them into pieces).

Yes, I'm involved in a big Lean project and I bump the version of mathlib which it depends on once a week. It's the only way to survive in this ecosystem.

[Kevin Buzzard]

here is the PR which broke Mathlib.Order.CompleteLattice into Mathlib.Order.CompleteLattice.{Defs/Basic/Lemmas} last month.

[Michael Rothgang]

(In the very near future, if you're a new enough version of mathlib, you'll see a warning when importing a file that was renamed or deleted.)