Coq Call 2019 11 20 - coq/coq GitHub Wiki

November 20th, 4pm Paris Time

Topics

• Change in coqdep behavior for vos: https://github.com/coq/coq/pull/11074 (Arthur)
• Status of the fix of template poly https://github.com/coq/coq/pull/11128
• Coq demo at the Paris Open Source Summit (Matthieu) https://www.opensourcesummit.paris/
• Release managers for 8.12 ?
• Role of side effects in declare (Emilio)
• Report on WIP on implicit arguments (Hugo)

Notes

• Fix for template poly ok with Pierre-Marie

• 8.12 RMs: Emilio and Théo

• RM for 8.11: hashes for 8.11 versions of libraries in CI: the majority seems to favor that over asking for user branches (esp for .v only libraries that should work with multiple versions).

• Role of side effects in declare (Emilio)

  • Cleanups coming about side effect handling in declare_def to move to the STM / higher-levels
  • Mainly for defined proofs to clean the handling of side effect export/handling.

• Implicit Arguments (Hugo)

  • Many questions of design and a few (7) PRs of cleanup.
  • Would be good to have a summary of the changes and use-cases.
    • What are the arguments for keeping non-maximal implicits, if we keep them shall we add [] to terms?
    • Check (c : T) requiring a coercion in front of c, should it print it or not?
    • Same for implicits, what should defensive/not defensive do: is it not rather a UI issue as we can't just have a do-it all Print?
  • Maxime asks what could be a goal design/feature set for implicits in the future.