Coq Call 2020 06 24

• June 24th 2020, 4pm-5pm Paris Time
• The link to the visio room: https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• What is the plan for Ltac2 to become a drop in replacement of Ltac1 (for new projects)? (Théo)

  See Jason's assessment at https://github.com/coq/coq/pull/12085#issuecomment-647771222 and Andrew's complaint about its documentation at https://github.com/coq/coq/issues/12549

• Adding back fiat-crypto-legacy (Emilio) https://github.com/coq/coq/pull/12554

• Upgrading Jenkins/coq-bench (the qualif server seems to be completely borked, see this issue I reported on Jenkins; if we can reset the installed version of Jenkins to the one on production, that'd be great, but the web interface doesn't seem to allow downgrading the qualif server) (Jason)

• Integrating coq-bench with coqbot (https://github.com/coq/coq-bench/pull/85) (What's the blocker?) (Jason)

Notes

• Ltac 2 improvements needed.

  By 8.13 should have solved all the relatively simple issues preventing usage, e.g. printf-like functionality, access to casts, more or less stable API for low level terms (we can't guarantee the term scruture won't ever change though).

  Jim suggests making a project page gathering the issues so we can track progress on this. Théo, Jim and Pierre-Marie agree on setting a roadmap through issues and a github project

  Issue with duplication of documentation between Ltac1 and Ltac2 which provides the same set of tactics more or less. Pierre-Marie does not think it would be easy to share syntax at the surface level. But certainly Ltac2's versions of the tactics will have similar behavior than their Ltac1's counterparts.

• Adding back fiat-crypto-legacy (Emilio) https://github.com/coq/coq/pull/12554

  Jason is willing to put in the time to maintain it, and help understanding failures in the proof automation part.

  Maxime suggests adding it to the allow_failure pipeline, but Théo mentions it does not report back this information very well. A coqbot change can allow that, pinging Jason in case of failure. Théo is on it. Emilio raises the point that we still need to investigate regressions in developments. We agree but see the cost/benefit for f-c-l to have been too high in the past (partly due to our inability to quickly debug the Ltac code there). Hence we compromise on this tradeoff of putting it in allow-failure for now.

• Integrating coq-bench with coqbot (https://github.com/coq/coq-bench/pull/85) (What's the blocker?) (Jason)

  PR seems ready and coqbot support can come later.

• Upgrading Jenkins/coq-bench (the qualif server seems to be completely borked, see this issue I reported on Jenkins; if we can reset the installed version of Jenkins to the one on production, that'd be great, but the web interface doesn't seem to allow downgrading the qualif server) (Jason)

  Maxime can investigate replacing Jenkins with gitlab workers. Otherwise we need to ask Inria's CI team.