Emilio Jesús Gallego Arias (Oct 20 2021 at 08:53): Emilio Jesús Gallego Arias (Oct 20 2021 at 08:53):Hi folks, I know there's been quite a bit of work on the Coq website, but IMHO it is still is non-optimal shape, a couple of points:
Karl Palmskog (Oct 20 2021 at 08:55):I thought only Platform releases would be announced: https://github.com/coq/ceps/blob/master/text/052-platform-release-cycle.md#announces
Emilio Jesús Gallego Arias (Oct 20 2021 at 08:59):Ah OK, I guess people developing Coq packages is confused tho [myself included] if we don't see a release
Emilio Jesús Gallego Arias (Oct 20 2021 at 08:59):Frankly I don't get the rationale as not to announce releases
Théo Zimmermann (Oct 20 2021 at 09:57):Yes, this was what was decided but maybe we can discuss reverting this decision during today's Call?
Enrico Tassi (Oct 20 2021 at 10:03):Why would one perform polling on the Coq website to know if the tag is put? (that is what a packager wants to know)
Enrico Tassi (Oct 20 2021 at 10:04):We have github notifications and coq-dev for it.
Pierre-Marie Pédrot (Oct 20 2021 at 10:04):Incidentally @Yannick Forster was confused yesterday about the release status of Coq 8.14 when reading the website
Enrico Tassi (Oct 20 2021 at 10:05):Hum, what did he wanted to know?
Pierre-Marie Pédrot (Oct 20 2021 at 10:05):How to install Coq and IIRC the website claims that 8.14 is the current version
Théo Zimmermann (Oct 20 2021 at 10:14):Well, yes, it does.
Théo Zimmermann (Oct 20 2021 at 10:14):Why wouldn't it?
Pierre-Marie Pédrot (Oct 20 2021 at 10:15):Because there is no official release message ?
Théo Zimmermann (Oct 20 2021 at 10:15):[And indeed, we do have release notifications on GitHub. One could think that they are sufficient for package developers to a certain extent.]
Théo Zimmermann (Oct 20 2021 at 10:16):But yes, we can discuss announcing releases to Discourse / Coq-Club / Twitter again.
Théo Zimmermann (Oct 20 2021 at 10:17):Though with the upcoming 2021.09 platform release which will include a beta for 8.14, IMHO it makes sense to delay this announcement a bit (to make it a joint announcement).
Yannick Forster (Oct 20 2021 at 10:35):I think one aspect of confusion is that the refman talks about a version which is not obtainable by the recommended way of installing Coq. This can (/will) confuse novice users (and it was my initial source of confusion)
Théo Zimmermann (Oct 20 2021 at 10:38):Do you think that novice users do actually look into which version of the software they are using?
Yannick Forster (Oct 20 2021 at 10:39):Maybe not, no. But doesn't the refman of 8.14 differ in relevant points? I would expect that if I always use the latest version of a software the reference manual actually applies to this version
Yannick Forster (Oct 20 2021 at 10:42):On the other hand, most of our novice users will be computer scientists, and it is not absurd that they check the version they have installed. After all, that's a very frequent question you get asked back when asking a question on Zulip or the like
Karl Palmskog (Oct 20 2021 at 10:42):where does "the website" claim that 8.14 is the latest version? Are we talking about the refman?
Yannick Forster (Oct 20 2021 at 10:43)::) I got confused by the refman and this page, which seem to be the only pages mentioning a version number
Karl Palmskog (Oct 20 2021 at 10:45):given that so many parts of the regular website are updated irregularly, I think we shouldn't use any version number anywhere there, even the opam-using page. Why not just opam install coq, and then some command to pin the version that was actually installed?
Yannick Forster (Oct 20 2021 at 10:49):My feeling would be that somewhere on the installation page there should be a sentence saying "The current version of Coq is 8.xx, and it can be installed in the following ways: ..." For instance a lecturer who wants to put information on a course website would need this information, no?
Yannick Forster (Oct 20 2021 at 10:52):Related: I now signed up to the coqdev mailing list to receive notifications early. If that is expected from package / library developers, maybe it makes sense to say that somewhere central (on the community page?). Right now I was unable to find any information regarding the coqdev mailing list. Alternatively, one could instruct people that they need to "watch" the repo with "All notifications" or "Custom with Releases enabled"
Karl Palmskog (Oct 20 2021 at 10:53):super weird to me at least to do both of the following on the website:
I vote for not having the (latest) version number on any static page.
Guillaume Melquiond (Oct 20 2021 at 10:58):To be clear (and to reiterate what Theo already said), releases of Coq are meant to be announced at the same time as the Platform. For previous releases of Coq, we were delaying the release so that the Platform would be ready. This time, we have decided to release early, before the Platform is actually ready. But as before, we wait for the Platform to be ready before we officially announce the release.
Théo Zimmermann (Oct 20 2021 at 11:10):Yannick Forster said:
My feeling would be that somewhere on the installation page there should be a sentence saying "The current version of Coq is 8.xx, and it can be installed in the following ways: ..." For instance a lecturer who wants to put information on a course website would need this information, no?
That used to be the case but we have decided to remove this information from the website. The reason why it still shows up on the opam using page is because this page instructs to pin Coq, but @Karl Palmskog if you know how to reformulate this without the need for showing the version number of the page, that would be very welcome.
Théo Zimmermann (Oct 20 2021 at 11:11):Yannick Forster said:
Related: I now signed up to the coqdev mailing list to receive notifications early. If that is expected from package / library developers, maybe it makes sense to say that somewhere central (on the community page?). Right now I was unable to find any information regarding the coqdev mailing list. Alternatively, one could instruct people that they need to "watch" the repo with "All notifications" or "Custom with Releases enabled"
I think this list isn't used much anymore and I personally try to encourage developers to use Discourse (dev category) instead.
Théo Zimmermann (Oct 20 2021 at 11:11):The release process checklists says: Send an announcement of the upcoming branching date on Coqdev + the Coq development category on Discourse (coqdev@inria.fr + coq+coq-development@discoursemail.com)
Théo Zimmermann (Oct 20 2021 at 11:12):Custom with Releases enabled
We should definitely encourage package maintainers to do so.
Michael Soegtrop (Oct 20 2021 at 12:02):Since this might be relevant to the discussion: I am about to release Coq Platform 2021.09 which includes Coq 8.14.0 with a beta pick (called 8.14+beta2). It also includes two picks for 8.13.2 and one for 8.12.2. There was also a beta1 based on 8.14+rc1, but this was only announced to Coq Platform package maintainers and was not a tag but a branch with improving package list.
The beta2 has about half of the Coq Platform packages in its final state - half are missing, patched or not confirmed.
Yannick Forster (Oct 20 2021 at 12:09):Just to make sure i understand correctly: A release of coq.8.14.0 exists on GitHub, but for now the platform will ship with coq.8.14+beta2?
Michael Soegtrop (Oct 20 2021 at 12:16):@Yannick Forster : no, the Coq Platform shipped Coq Platform beta1 with Coq 8.14+rc1 and soon will ship Coq Platform beta2 wit Coq 8.14.0.
The beta/rc/release numbering of Coq Platform is obviously a bit behind Coq. It takes a bit more experience to find out what makes sense, but I think it might be common that Coq Platform beta1 matches Coq rc1 and Coq Platform beta2 matches Coq .0.
The final 8.14 release of Coq Platform is planned some time in November. There are some important packages missing (stdpp and iris e.g.) in beta2.
Théo Zimmermann (Oct 20 2021 at 12:18):[What is new with the 8.14 release cycle is that the beta testing phase is deferred to the platform. That's why we've switched to doing a "rc" instead of a "beta" for Coq.]
Enrico Tassi (Oct 20 2021 at 12:28):To sum up, here the issue seems that some announcement leaked, in some way (opam instructions and refman), before the official release messages was sent to final users. For devs, I think tags were announced on coq-dev (and GH notifications + messages to platform package authors to tag), so that went well IMO.
Théo Zimmermann (Oct 20 2021 at 12:38):Leaked? OK, if you think that the default version of the refman shouldn't be updated until the corresponding platform release is ready to announce (beta pick or stable pick?). We should settle that part of the process and update the documentation. Let's talk about it in the Coq Call.
Enrico Tassi (Oct 20 2021 at 12:39):No strong opinion on my side, I was just trying to understand what went wrong and caused confusion.
Yannick Forster (Oct 20 2021 at 12:49):From my perspective, having
(1) the refman aligned with the default installation method rather than the latest GitHub release and having,
(2) a clear statement how package developers can stay tuned without getting all the noise of GitHub issues and PRs, and
(3) either no or a central mention of the latest Coq version number on the installation pages
would be a welcome improvement
Emilio Jesús Gallego Arias (Oct 20 2021 at 13:31):Coq and the Coq platform are not the same project, I still don't understand why we want to couple them. Coq is still relevant to a lot of people.
Going back to my original point, unfortunately the website is quite confusing at various levels, may seem silly, but a lot of people is struggling with getting basic information about Coq. I'm not sure if we should just remove the website and redirect it to other page, but I dunno.
Théo Zimmermann (Oct 20 2021 at 13:43):We should definitely completely redo the website (from scratch and thinking carefully about what info we want to put forward), but I think this work is a bit delayed because we should also decide if we change the name (and for what) and design a new logo at the same time.
Théo Zimmermann (Oct 20 2021 at 13:44):That's why for the last few months / years, I've focused on improving the information available on the website incrementally instead.
Théo Zimmermann (Oct 20 2021 at 13:44):And I do believe that things have improved but I may very well be wrong, and you should feel free to open issues to point to specific things that can be improved incrementally.
Théo Zimmermann (Oct 20 2021 at 13:45):And when the time comes to redo the website from scratch, then we should discuss as a group what we need to put forward / focus on.
Emilio Jesús Gallego Arias (Oct 20 2021 at 13:46):I'm afraid, based on the feedback I've gotten from people being confused at the website, that I don't see a clear path of improvement :( :(
Yannick Forster (Oct 20 2021 at 13:47):Although things might still be suboptimal (I agree that we need a new website), I think overall the state of the website and the accessibility of the Coq project have improved greatly in the last years. Probably that has various reasons, but from my perspective your work and endurance @Théo Zimmermann were central there
Yannick Forster (Oct 20 2021 at 13:48):Why are redesigning the website and choosing / changing a name entangled? Most likely, designing a new website will take (lots of) time, so I would have naively guessed that starting before possible name changes will speed up things overall
Théo Zimmermann (Oct 20 2021 at 13:50):Website design is related to logo design and logo design is related to name change. Of course, we could start work on accessibility of the website before that, but lack of time is probably the answer there.
Théo Zimmermann (Oct 20 2021 at 13:51):For instance, right now, I'm involved in preparing the upcoming Coq community survey and this is something that I do because I think it is important but also something that takes the little remaining time that I have on my hands this semester.
Théo Zimmermann (Oct 20 2021 at 13:52):So I definitely don't have time to be involved in website redesign.
Théo Zimmermann (Oct 20 2021 at 13:52):And even if we plan to hire people to help with the website redesign, having Coq developers engaged in the process is clearly very important.
Yannick Forster (Oct 20 2021 at 13:52):Sure, but will we really end up with a website design which is directly related to the logo? I.e., can't we just redesign the website and then replace logo_coq.png with logo_newnameofcoq.png?
Théo Zimmermann (Oct 20 2021 at 13:53):In terms of colors, this is likely. Probably this will stop there.
Yannick Forster (Oct 20 2021 at 13:53):I agree that business is a problem, now and in the future :)
Last updated: Sep 15 2024 at 13:02 UTC