Coq Call 2021 02 03

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

Topics

• bump OCaml lower bound to 4.07.1 for 8.14? Stdlib, Seq, less flambda problems, default of the platform, Ubuntu LTS has 4.08, Debian stable 4.05 / testing 4.11, Fedora 4.10. (Enrico)
• Future of locality attributes (general question regarding all commands declaring objects) (Théo)

Notes

• Locality attributes in general

  Example: Hint View behavior? Currently export (no locality attribute accepted yet)

  Remaining superglobal hints:

  • Export for typeclass instances remaining (currently superglobal)
  • Bind Scope / Delimit Scope
  • Reduction Strategies
  • Arguments
  • Declare Equivalent Keys
  • Schemes
  • Autorewrite databases

  It's ok if inside sections certain Hints do not support Export (e.g. Hints with terms), but we should have uniform behavior when they do.

  We realize that the release summary and warning are a little ambiguous between the recommended fix for older developments (maintaining backward compatibility) and the recommended way to introduce new hints which are currently different. See issue https://github.com/coq/coq/issues/13809 by A. Appel prompting this discussion. There is a way to make the stdlib not issue the warning on standard user code proposed by J. Gross.

• OCaml version bump

  Seems like 4.07.1 is a good target (but 4.08 would not be, due to complexity issues introduced, which are fixed by 4.11). In the future using dune we should have more flexibility switching versions but beware that dune itself requires 4.08 at least.

  We still test with 4.05 on a basic build, but recommend 4.07.1 and make it the baseline for the CI.