Karl Palmskog (May 31 2020 at 18:56): Karl Palmskog (May 31 2020 at 18:56):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
Assia Mahboubi (Jun 01 2020 at 13:11):Note that this is a "user" release, as Lean(3) is not more maintained by Lean's official devs: https://github.com/leanprover/lean.
Karl Palmskog (Jun 02 2020 at 10:01):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)
Christian Doczkal (Jun 02 2020 at 11:23):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?
Enrico Tassi (Jun 02 2020 at 12:14):AFAIK the compatibility is very poor, but I know users motivated to port code.
Enrico Tassi (Jun 02 2020 at 12:15):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
Enrico Tassi (Jun 02 2020 at 12:18):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.
Christian Doczkal (Jun 02 2020 at 12:44):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 ...
Paolo Giarrusso (Jun 02 2020 at 19:49):their FAQ explicitly rejects upfront any promise of compatibility, so I'm not sure what you are wondering about
Paolo Giarrusso (Jun 02 2020 at 19:51):IIUC, each time they broke compatibility, it was for fundamental problems that required significant redesigns (and AFAIK lots of code was often _not_ ported)
Enrico Tassi (Jun 02 2020 at 19:53):Yes, I guess this finally settles that we are comparing apples and oranges in this thread.
Paolo Giarrusso (Jun 02 2020 at 19:54):they hopefully want to promise compatibility eventually, but not yet: https://github.com/leanprover/lean/blob/master/doc/faq.md
Paolo Giarrusso (Jun 02 2020 at 19:55):and the “go away” sentiment hasn’t changed: https://github.com/leanprover/lean4
Paolo Giarrusso (Jun 02 2020 at 19:56):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 :-)
Christian Doczkal (Jun 02 2020 at 20:27):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:
Paolo Giarrusso (Jun 02 2020 at 20:36):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.
Paolo Giarrusso (Jun 02 2020 at 20:37):Back to the original topic, cheaper and more frequent bugfix releases would probably be possible and useful for Coq.
Paolo Giarrusso (Jun 02 2020 at 20:43):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).
Théo Zimmermann (Jun 02 2020 at 21:45):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.
Christian Doczkal (Jun 03 2020 at 10:58):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:
Théo Zimmermann (Jun 03 2020 at 12:35):@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?
Théo Zimmermann (Jun 03 2020 at 12:36):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.
Christian Doczkal (Jun 03 2020 at 12:40):@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
Paolo Giarrusso (Jun 05 2020 at 08:59):@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.
Emilio Jesús Gallego Arias (Jun 05 2020 at 10:19):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.
Paolo Giarrusso (Jun 06 2020 at 17:58):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.
Paolo Giarrusso (Jun 06 2020 at 17:59):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...
Karl Palmskog (Jun 06 2020 at 18:01):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)
Karl Palmskog (Jun 06 2020 at 18:03):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
Paolo Giarrusso (Jun 06 2020 at 18:31):Re properly annotated, does make quick now benefit from "set default proof using"?
Karl Palmskog (Jun 07 2020 at 22:47):I have no idea about Set Default Proof Using, we rolled our own automatic insertion of annotations
Last updated: Dec 07 2023 at 14:02 UTC