Coq Call 2024 10 01 - coq/coq GitHub Wiki

Topics

Roles

  • Chairman: Matthieu Sozeau
  • Secretary: Gabriel Scherer

Synthetic notes

  • Move the roadmap source file to the CEP repo for further refinements (Matthieu)

Less synthetic notes

Renaming and release management

Théo: there's a public project for tracking the renaming tasks to release Rocq 9.0: https://github.com/orgs/coq/projects/28

Two weeks ago we designated Pierre-Marie and Matthieu as release managers. We mentioned a potential release calendar, and a branching date. But we didn't write it down, and it's not on the wiki.

In the minutes of the meeting there is a date: branching mid-November ( https://github.com/coq/coq/wiki/Coq-Call-2024-09-17 )

Theo: let's assume we can branch mid-November (this is optimistic). A certain number of tasks should have been done before, and in particular everything regarding the new CLI we discussed the last time. I think we assigned Gaëtan to the new CLI. Gaëtan, do you think when you are planning to work on this?

Gaëtan: I haven't decided when I will work on it yet, probably soon. It should be good for a November release.

Théo: currently it's not scheduled, so we should not forget about it.

Théo: since last time I did three things.

  • I wrote to Gabriel Scherer about Discourse.

    I thought this may be the occasion to consider switching to a Discourse instance with our own domain name, so that we own the URL, which opens the possibility to self-host at some point if we want. I don't propose to self-host, but to do the same as OCaml: paying Discourse for hosting, and because we pay we have control over the domain/URL.

    Gabriel: we pay $45/month, we use the $300/month with a 85% discount for educational institutions. If Coq has less volume, maybe you can use the $100/month, which is $15/month with the discount.

    Théo: then we need to discuss what to do for the mailing-list. I propose to ditch the mailing-lists completely. Maybe we could consider setting up an alias that redirects coq-club to Discourse. (Then Discuss users have the possibility to subscribe in mailing-list mode.)

    We don't have to decide on this now.

  • I wrote to Zulip about our plan to rename the organization from Coq to Rocq-prover. I got an answer saying that they don't have a mechanism to hold names for us, but they told me to register rocq-prover now, and when we are ready to switch we ask them and they will do it. I did that, so we are safe. (We also have it for Github.)

  • (task three was "register a Zulip name")

Hugo: I think a channel like coq-club remains important to target people. I think it might be worth preparing a good marketing about the changes in the system, it's not just renaming but also an occasion to advertise recent changes.

Théo: there is the work on the website that will help with that. We are in contact with designers, but the work has not started yet.

Théo: there is the roadmap on the rocq-prover website https://rocq-prover.org/ Théo: this has not been widely publicized yet, so we can still easily change it.

Hugo: "agile development philosophy", "accelerating innovation" looks a bit auto-generated and not necessarily credible.

Andres: it reads like advertizement, I agree.

Andres: also, it reads a bit like a bunch of different research projects thrown together, it's a bit forced.

People: should we choose a smaller number of axes to highlights, and not list everything? But how do we choose?

Théo: if we aggregate the projects that are supported by the team (for example the "Platform docs" project, which is going to be supported by Thomas Lamiaux on the side; the "vscoq effort" which is obviously supported), these are things that can be listed as projects. And then we can list more research-oriented projects like MetaCoq, Liber Abaci, LLM4Coq...

Matthieu: in each case it's always a subset of the team, not everyone is working on it.

Théo: but is it part of our shared vision?

Enrico: to me the first part of the document is a panorama, a list of everything that is going on. This is not a roadmap or a vision. A vision is like a dream, "all software is bug-free". A roadmap is a long-term goal like self-certification. I wouldn't call this a roadmap.

Gabriel: if I wanted to suggest some small changes to the marketing part at the beginning, where should I do it?

Matthieu: on the wiki, on the repo?

... : on the CEP repo.

Hugo: just removing the word "more" would be nice.

Good first issues

Gabriel: I'd like to contribute something, like a small PR/bugfix. What should I look at?

I looked at "good first issues", but Gaëtan is not convinced, do you have other recommendations?

Pierre-Marie: easy issues we solve quickly, in most cases.

Gabriel: I am actually happy with the list, it's not perfect but it's fine. If you don't have a better process, I would recommend tagging more of those from time to time.

Emilio: an idea we discussed before, we could actually have all new issues go through a classification process. There is a "needs-triage" label. It's a human process.

Théo: about needs-triage, we switched a few months ago to using issue forms for new issues, and we are adding labels automatically for new issues. There are two issue forms you can use, one for a bug and another is for an enhancement proposal. So "kind:bug" and "kind:enhancement", but also the needs-triage label is added automatically to new issues. If someone removes the label, they triaged it.

Emilio: maybe the best way to introduce new people to Coq is not through Github but having more events. We got over 100 people in the hackaton, we got Print Notation for example. Lean has the "office hours" call. I don't think we have the resources to do that, but maybe a couple office hours per month.

Gabriel: if someone has a question on a PR, they need feedback, they can participate to the next Coq Call.

Emilio: but the name is less clear.

Gaëtan: coq calls are for making decisions.

Théo: office hours, you come without an agenda.

https://github.com/coq/coq/pull/19610

Gabriel: I disagree with Pierre-Marie on this PR! I wonder if I should just close and move on, or whether people have different opinions.

Gaëtan, Hugo: we more or less agree with Pierre-Marie.

Pierre-Marie: generic arguments have different shapes and needs, it might make sense that some printers are not declared. We had a sum of built-in arguments, and it was kind of a mess. We don't want plugins to be second-class.

Emilio: I find that these generic arguments, it's more like bad extensibility. Our system has good properties, but genargs are painful.

Pierre-Marie: you are thinking of serialization.

Emilio: if I want to pattern-match a tactic... Why is ltac a plugin in Coq, who is using Coq without Ltac? I have this suite of compilers, write an OCaml plugin that counts the number of "nsatz" tactics in a proof file. This is hell to do. Counting the number of "intros", this is hell to do.

PMP: in any case the tacexpr AST is bad. You can do that by pattern-matching, but you need to load the Ltac plugin.

Guillaume: the patch of Gabriel does not solve this issue.

Gabriel: okay, I'll close my PR. You are all wrong! But it's fine.

Théo: we have a bot written in OCaml that would appreciate more people looking at its code.

Théo: for example it needs switching to Ocaml 5. We can talk about it more offline.

CEP 42

Hugo: We only have "Definition", and all the code goes through this. Possibly we can add attributes to make things explicit in the implementation. It is a model of how to present things.

sealed and defined.

Enrico: is this like Opaque or Qed? Are you changing also About?

Théo: Opaque was abused because it was used both to designate opaque in the sense of Qed, but also in the sense of the Opaque command which does not mean the same thing.

Andres: the Qed one is the one that makes sense, and the other is the weird one.

Enrico: when I do "About", it prints "This is opaque", do you want to change to Sealed?

PMP: "sealed" matches the usual module speak in PL communities.

Gabriel: you propose to ignore the Qed/Defined at the end. I wonder if you should have a warning instead, to let users know that their potential intention is not respected.

Théo: we suggested a sort of deprecation warning of the sort you proposed, but then a few years alter Piere-Marie and Gaëtan proposed to not do this.

Hugo: there would be a warning if you put Defined on a ... But it's not an error to put Qed on a theorem, anymore.

Gabriel: I thought people had a specific idea in mind when they use Qed or Defined, and maybe we should warn them if their intention is ignored. But I hear from the discussion

Hugo: what about "productive"?

Matthieu, PMP: we could use "cofixpoint", which already exists.

Hugo: a theorem has an inductive argument and a coinductive domain. We don't have a way to say whether we want it to be guarded inductively or coinductively.

Pierre-Marie, Théo: we are trying to remove discrepancies.

Théo: it was supposed to be an attribute, and then struct would only apply when it is inductive.

Hugo: so an attribute that is on each component, and gives for each component the index of the argument (or result) on which it is guarded.

Théo: yes, we need attributes on each components for opacity anyway.

Hugo: okay, we can do that.

Emilio: the AST of Coq, that thing is hard to design. Many things in the system are invariant today, AST choices. It's hard to make design choices if we don't have a clear contract on which information is known statically. Back in the days, we required commands, they could not open proofs dynamically, and it changed. Here indeed, you could require well-bracketed expressions. I'm not sure you can come up with a satisfactory solution if you don't put more invariants on what other layers expect from the syntax. I think a discussion of runtime properties is also needed in this case.

Matthieu: so this CEP proposal, it factors more things, but it has less invariants than the previous one.

Emilio: for example you can now put Transparent at the beginning, and Qed at the end. Then what will the tools do? Currently they only have code to look at the end of proofs.

Hugo: if there is an attribute, it takes precedence.

Pierre-Marie: if you ask something qed in the attribute, and then you ask it to be transparent.

Matthieu: all the protocols have to look at the attributes now.

Emilio: are they already merged on master?

Hugo: no, it's a PR.

Emilio: ok. Once it gets in, we need a clear model.