Coq Call 2024 06 04

• June 04th, 4pm UTC+2 (Paris time zone offset)
• https://rdv2.rendez-vous.renater.fr/coq-call

Participants: Pierre Roux, Pierre Rousselin, Matthieu Sozeau, Gaëtan Gilbert, Guillaume Melquiond, Enrico Tassi, Yves Bertot

Topics

• Refman ltac1 vs ltac2: currently the tactic doc is essentially about the ltac1 version of tactics (especially syntax wise) and some shared tactics like progress and tactic related concepts like goal selectors are documented in the ltac1 chapter. What do we want to do about this? (Gaëtan, 15min)

Roles

• Chairman: Matthieu Sozeau
• Secretary: Yves Bertot

Notes

Remark: in these notes, Ltac is sometimes called Ltac1.

The reference manual for Coq describes tactics from the point of view of Ltac1. Some tactics have a different syntax and semantics depending on whether the proof mode is "classic" (meaning Ltac) or Ltac2 (changing the proof mode can be done using Command "Default Proof Mode " as documented here.

Some tactics are only documented in the part of the documentation for Ltac1.

To make usage transition from Ltac to Ltac2, it would be necessary for every tactic whether they have a different behavior. However, it is not desired to have a heavy documentation that combines documentations for the two variants.

One of the proposals is to be radical, and write a new documentation for Ltac2 that would be stand alone, considering that the current documentation for Ltac should not receive any changes?

In its current form, the documentation for Coq has a chapter "Tactics" that documents all the elementary tactics, and when the behavior is different between Ltac and Ltac2, it is the Ltac behavior that is described, without mention of a discrepancy.

A second proposal is to annotate in a light way the the current documentation of elementary tactics, to express when these tactics can also be used in Ltac2. When there is a difference in behavior, the Tactics chapter should contain a lightweight remark mentioning the difference and pointing to the Ltac2 documentation for an detailed description of the difference. The Ltac2 documentation could contain a stand-alone description of the tactic (from the point of view of Ltac2) and a description of the discrepancy between behaviors in Ltac and Ltac2.

The second proposal is generally approved by the people present.

There is a discussion concerning the gain achieved by moving from Ltac to Ltac2. People cite the possibility to have functions that operate on the goal and return a value in a type different from unit (which makes it possible to avoid cumbersome CPS style programming), and also the fact that it is not necessary anymore to store data in the goal's context interaction between successive tactics. It is agreed that explaining these gains requires a tutorial, rather than a modification of the reference manual.