Coq Call 2021 01 13

• January 13, 2021, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• #13656 Avoid using "subgoals" in the UI, it means the same as "goals" - discuss whether we should proceed with this change. It will require changes to Proof General (already done), Iris and coq-record-update, used by Bedrock2.
• CEP #53 proposes the functionality for a visual debugger for Ltac and other tactic languages and the general steps needed to implement it
• Q for vernac-maintainers: making Print Module actually print what is in a module and libobject.
• Unknown attributes should not raise an error but issue a warning! Arg!

Notes

• [#13656] go through with the change, no objection to the correction. Just be careful with syncing with ProofGeneral.

• Debugger for Ltac CEP:

  • First fixing some of the problems of the existing debugger (e.g. breakpoint setting)
  • Pierre-Marie points out the difficulty of integrating the interactive aspect of the debugger with the interactive aspect of Coq itself.
  • Enrico suggests the debug mode to act as a non-terminating command, freezing the STM basically.
  • Interleaving document execution with debugging sounds hard.
  • Debugger protocols for vscode or other IDEs should be relatively easy to share
  • Agree on CEP plan.

• Discussion about attributes, warnings and options. Maybe the warning config mechanism could be separate from options, as it is more elaborate, e.g. additive.

• Interesting discussion about printing of modules (and their extra-logical information). Not easy to reach in the current sea of libobjects. Discussion to be continued when Maxime is around.