Interesting that Lean (3) has seemingly moved to a weekly or even more-than-once-daily release schedule: https://github.com/leanprover-community/lean/releases -- also looks like they are using some automation for releases
Note that this is a "user" release, as Lean(3) is not more maintained by Lean's official devs: https://github.com/leanprover/lean.
I think those "unofficial" releases of Lean will effectively be the Lean everyone uses for the next year (since Lean 4 according to the Lean Zulip is still quite far off)
Does anyone have any information on the compatibility between Lean 3 and the upcoming Lean 4? Is the Lean community going to face a massive porting effort?
AFAIK the compatibility is very poor, but I know users motivated to port code.
I asked the very same question, they answered "even the syntax for very frequent thing is different". I can't say more, but I could detect the absence of a "migration strategy". Maybe they have it now, but not back in February
Also the Lean3 / 4 story seemed like problematic. In the sense that the community took over version 3 (forked) and uses/maintain it, but the main author is really on version 4. I write this just to add context to this thread: IMO lean 3 is releasing fixes, which is good, but way less challenging than releasing incompatible changes, and can surely be done more frequently.
As it comes to porting, I'd be more worried about changes in behavior than changes in syntax. Adapting syntax may cause large diffs, but may be done semi-automatically. When tactics change their behavior and break proofs, this is a whole different can of worms. I guess that also depends on how robust the proofs in the current Lean 3 corpus are. We shall see ...
their FAQ explicitly rejects upfront any promise of compatibility, so I'm not sure what you are wondering about
IIUC, each time they broke compatibility, it was for fundamental problems that required significant redesigns (and AFAIK lots of code was often _not_ ported)
Yes, I guess this finally settles that we are comparing apples and oranges in this thread.
they hopefully want to promise compatibility eventually, but not yet: https://github.com/leanprover/lean/blob/master/doc/faq.md
and the “go away” sentiment hasn’t changed: https://github.com/leanprover/lean4
I think their choice is very fair, and I applaud them for being explicit, and plan to look into using it if they ever promise compatibility :-)
Paolo G. Giarrusso said:
I think their choice is very fair, and I applaud them for being explicit, and plan to look into using it if they ever promise compatibility :-)
I agree, but I'm asking myself whether the people involved in https://github.com/leanprover-community/mathlib and https://leanprover-community.github.io/lean-perfectoid-spaces/ truly realized what they were getting themselves into. :thinking:
I hope they did. Meanwhile, Coq marketing (if it’s something relevant) could/should probably use this when promoting Coq over Lean; I expect for most users this could be a more convincing argument. You don’t even need any spin.
Back to the original topic, cheaper and more frequent bugfix releases would probably be possible and useful for Coq.
Of course there’s a question of resources, but more automated releases could save time for the release managers, and the actual implementation could be done by somebody having just good DevOps skills — and such people are likely more widely available (at least in general).
FWIW a lot has been done already (and a lot remains to do of course) to automate and streamline the release process. This is what Chapter 5 of my PhD thesis is about.
Paolo G. Giarrusso said:
Back to the original topic, cheaper and more frequent bugfix releases would probably be possible and useful for Coq.
I'm not sure I agree with that. Currently, even "point releases" such as 8.11.1 introduce minor incompatibilities that can cause packages to break. This can be quite a nuisance if ones developments rely on multiple dependencies maintained by different people. On the other hand, I don't ever recall being happy about no longer having to suffer a particular bug after a point release. :thinking:
@Christian Doczkal
Currently, even "point releases" such as 8.11.1 introduce minor incompatibilities that can cause packages to break.
That's not supposed to be true and this would usually deserve a bug report. Can you point to an example?
I don't ever recall being happy about no longer having to suffer a particular bug after a point release.
I'm pretty positive that this was the case for some users, but usually this is users who tracked a particular bug report.
@Théo Zimmermann , this is the example I had in mind: https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/imported.20from.20gitter.20room.20math-comp.2FLobby/near/196586719
@Christian Doczkal meet such a user 8.11.1 came so late for me that I used (and backported) patches myself: 8.11.0 broke cbn, hence autosubst, hence my development, and in 8.11.1 the new make vos
becomes usable with sections. For months I used a forked Coq on my machine, and kept supporting 8.10.2 on CI.
IMHO we need to distinguish a bit more clearly features such as .vos
that indeed in the first version they appear are not expected to be 100% stable, mainly due to lack of testing in the wild.
The manual clearly marked vos as experimental, so that wasn't the problem. in fact, I have probably already complained too much on this point, and I apologize; what I should say is that (with the patches in 8.11.1) make vos became (for me) one of the coolest Coq changes I've lived through (so, since 8.8), competing with dune's caching.
FWIW maybe make quick was also cool, but I never got any speedup from it (with sections) probably in part because I didn't have enough clue when I tried...
make quick
does indeed give similar speedups to properly annotated projects, but the argument posed against it was that generated .vio
files are large (which was never an issue for us on medium-largish sized projects)
I really hope the main "killer" feature that vio
offers, proving individual proofs in isolation in batch in parallel, will not be killed off... our work suggests this can, with the right tooling in CI, give huge speedups
Re properly annotated, does make quick now benefit from "set default proof using"?
I have no idea about Set Default Proof Using
, we rolled our own automatic insertion of annotations
Last updated: May 31 2023 at 02:31 UTC