Coq Call 2024 10 22 - coq/coq GitHub Wiki

Topics

Roles

  • Chairman: Enrico
  • Secretary: Théo

Notes

  • GitHub warned that the macOS image used in CI will stop being available soon. A tentative update by Gaëtan to the most recent macOS image leads to a failure in a rewrite rule test and we need macOS users to help debug (check the raw log of the PR CI for full details on the error). Unfortunately, none of them were present in the call. We could try to use an intermediate image version until we debug this issue (primary option chosen by Gaëtan). We could also remove the problematic test (which expects a stack overflow to happen) as an alternative.
  • Hugo has a master student (from the LP curriculum at Diderot) who has extended the behavior of the Scheme command (which can be further extended by plugins) during his internship (now over). He will probably start by submitting a PR soon on a limitation of the effect system of Coq (a two-line fix). Please be kind to him when he submits his PRs, but he can also learn thanks to the feedback on his code.
  • Hugo likes Théo's proposal in the PR to have a single ternary attribute instead of two binary ones: transparent, opaque, sealed. Hugo would have liked in the future to have the capacity to move from sealed to transparent but Pierre-Marie is strongly opposed to this because this breaks some important properties of the module system. Pierre-Marie also argues that this is an XY problem and that what users need is to be able to evaluate directly in Coq the result of a computation that includes opaque objects. The solution to this is to provide a special evaluation in Coq that allows to erase objects in Prop. Related discussion on UIP, OTT, terms reducing to eq_refl. Hugo suggests documenting why the design prevents moving a sealed definition to transparent, and Pierre-Marie completes that it could be interesting to provide guidelines on when to set something as transparent or opaque (could be worth a how-to in Platform Docs). Related: there is no clear doc on singleton elimination.
  • Gaëtan closed #19502 because interest seemed limited. Pierre-Marie defends the need. For the context, template polymorphism was reimplemented in Rocq 9.0 with rules that we understand (inspired by the meta-theory from sort polymorphism, but the implementation is independent). There is no paper, but there is a related CEP. The PR tries to be smarter when inferring arities of template polymorph inductive types. It mostly works, but the bench does not shows perf improvements and a few bugs are revealed. Enrico asks if perf is really the only justification. Pierre-Marie confirms that it's better to generate fewer universes (like in this PR). Related discussion on the performance cost of universes in general. Pierre-Marie describes that the performance cost of universes is seen in particular in typeclasses eauto (generating fresh universes before applying a hint). Enrico feels like this could help for algebraic universes.
  • Théo summarizes actions on renaming in the last two weeks, including the discussion with Erik on the Docker images. Pierre-Marie asks what do with Coq in some internal places. In the XML protocol or the CoqIDE configuration files, it seems fine to keep coq to avoid breaking things that will eventually be removed anyway. Internal file renaming is not critical but easy. Gaëtan plans to have a prototype PR of the new CLI this week.
  • Long discussion after the Coq Call is officially finished on the last topic on the agenda. After discussing the various options (e.g., making the refman independent of the stdlib and moving the examples that depend on it to the stdlib refman), the one that emerged as the most consensual is to keep the refman depending on the stdlib and even extend it to be able to depend on other CI projects (such as Equations or MathComp). A new make ci-refman target will be added for that purpose to Makefile.ci. For convenience in local development, an alternative target will be provided to build the refman without running the coqtop examples and thus without needing any dependency. During this discussion, other things related to the stdlib split were discussed: improving tooling (in particular, having a target to update already cloned CI projects in Makefile.ci), working on communication (to make sure that the split stdlib is a success and that we can attract more maintainers, work on a shared roadmap, ensure that the stdlib covers everything that it should, etc.), and how to evaluate if the split was a success (check with the stdlib maintainers what their opinion is after a few months or a year; if there are no maintainers to answer it obviously means that the split has failed and the experiment should be aborted).