Coq Call 2024 11 05 - coq/coq GitHub Wiki

Topics

  • Gitlab CI artifact size issue (Gaëtan, 15min)

    We use too much space in the disks provided by Inria (2Tbytes out of the 4 they planned). We propose to reduce the time that artifacts are are kept from one month to one week (with some exceptions for docomentation and bench results), and to see with the Inria production people if this is the solution (in the long run, we may consider reducing that time to 3 days, but again not for all artifacts).

  • Unification of the syntax of Theorem/Fixpoint/Definition etc. (#19031) (Hugo, 10 minutes)

    This point was not studied.

  • "Make the output of info_auto be the list of tactics it finds" #19654 (See here) (Jim, 10 minutes)

    There is a long discussion about the fact that using a tree structure to represent a successful proof built by auto is not accurate. We agree to ask Pierre-Marie Pédrot to produce a counter example, so that the limitations of a displaying tool can be better documented.

it is agreed that the output of Print HintDB should not rely on a presentation by tactics (as it is done now), but on a presentation by hints.

  • Issue "Use correct tactics in TC eauto output; show "Resolve thm" in Print HintDb rather than "simple apply thm", which is not always what's used" #19788 (Jim, 5 minutes)

    It is agreed that the output of Print HintDB should not rely on a presentation by tactics (as it is done now), but on a presentation by hints. External hints should have a name, but we still have to decide on a syntax.

  • Renaming updates. Discussion about renaming the CEPs and coqbot (Théo, 5-15 minutes)

    The docker organization accepted to fast-track our project. We also have sponsorship from the OSS foundation. We will have the same support for Rocq as for Coq.

    It is agreed that CEPS should be renamed into RFCs. On the other hand, a name for coqbot has not been decided in the meeting. It has been suggested to look at some French culture words associated with the tasks of butler.

  • Integration of parts of coq-lsp/fleche/petanque into Coq repo or Coq organization (Nicolas, 5min) Mention the start of a discussion summarized in a collaborative pad and schedule a dedicated meeting to continue the discussion (not necessarily next Coq call).

    This point is mostly an information point and a call for volunteers. People who wish to participate in this task should contact Nicolas.

  • Modification of the Add Field command and the ring, field, ring_simplify, and field_simplify tactics with respect to pre and post-processing #19795 (Yves, 10 minutes).

    Up to now, when Add Field is called, there is an automatic call to Add Ring with the parameters that can be deduced from that passed to Add Field, except the parameters for pre- and postprocessing. Yves proposes to change the behavior of Add Field so that pre- and processors, when they are given, are passed to Add Ring. This more uniform behavior should be easier to understand. There is approval on this point.

    When it comes to pre- and proprocessing, the ring, field, ring_simplify, and field_simplify tactics do not behave in the way that can be understood from the documentation.

    There is a PR that is already proposed for these modifications, but it only partially covers solves the mismatch with the intuitive behavior. Yves suggests that this PR should be integrated first as is, another PR coming later to correct the remaining unsatisfactory behavior.

Roles

  • Chairman: Nicolas T.
  • Secretary: Yves Bertot