Coq Call 2024 04 09

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

Topics

• Discussion on declare.ml and its use in abstract, obligations, etc. #18811, CEP #42), Zulip
• Library accessors #17393
• Deprecate Let/Variable/Hypothesis outside section #18880

Attendance

Chairman: Matthieu Sozeau Secretary: Yves Bertot

attending: Emilio J Gallego Arias, Yves Bertot, Guillaume Melquiond, Pierre-Marie Pédrot, Matthieu Sozeau, Enrico Tassi, Hugo Herbelin, Andres Erbsen, Pierre Roux

Notes

• merge of different execution paths for Co / Fixpoint #18811 Question were:

  • Towards merging comFixpoint, comProgramFixpoint.ml and comDefinition.ml
  • Could we also reduce the "technical debt" by merging the different paths in declare.ml for obligations-based or proof-engine-based or term-based mutual and non-mutual definitions (see also what UIs need)?
  • In particular, what typical plans for "proof obligations" (see Zulip)
  • Miscellaneous questions: what is the role of Evd.fix_undefined_variables? Do we pass a sigma to the Declare hook?

  Discussion revolved around the history of declare.ml and what remains to do. Essentially the part that takes care of universes and definition seems to lack a specification. Things seem to work a bit by chance. Equationsand Program could be better integrated. Today they contain workarounds against limitations of the API. But there are bugs in these workarounds, see this bug report Hugo is blocked on Théo's CEP 42. The problems come from the way obligations update or do not update the sigma. Descriptions of the problem are on zulip.

  Agreement converges on the fact that commands like abstract and next obligation should postpone the declaration of constants and use local variables and let-bindings instead. Then there should be an effort to assign this task to some developers. Pierre-Marie Pédrot, Andres Erbsen, Matthieu Sozeau, and Hugo will wrap this up on Zulip.

• Library accessors #17393

  The PR has been waiting for approval, which was not given on the grounds that passing a parameter to a function that is always the same could be avoided. There is a feeling that the change will make future reviews easier. It is collectively agreed that the PR should be accepted.

• Deprecate use of Let/Variable/Hypothesis outside sections #18880

  It is proposed to make the use of Let Variable or Hypothesis outside sections become an error (it is currently a warning). While it is agreed that this should be discouraged for beginning users, there are use cases where leaving this possibility can gain work (in bug minimizing and as a transient state in refactoring of proofs).

  It is agreed that the warning message should be improved but it should also be turned into an error by default, knowing that it is easy for people engaged in bug minimization or refactoring activities to transform the error into a warning. Some work should also be done on the documentation.

Leftovers

Several topics from the agenda were not treated:

• More cleanups (CoqIDE, async, side effects)
• Dangers of making env mutable see comment in #17674
• About reduction strategies (part of CEP #85) [Hugo, 10 minutes + discussion time]
  • we may allow constructors in the transparency state to control iota-reduction, the same way as we can already control primitive projections reduction by name of projection?
  • better document the role of flags (e.g. is iota needed to trigger a Proj and is delta needed to trigger a Const unfolding, or only the transparency state matters?)
  • what exact semantics for simpl never? How to document it (see #18602)? How should it impact recursive reduction of itself and injection (see #18591)?
  • did we conclude something about hnf and Tacref.hnf_constr?
  • is there some hope to improve the efficiency of cbn?
  • once fixpoint refolding is always done, would it make sense to eventually combine cbn, cbv and lazy into one machine using Call-by-Push-Value