Coq Call 2020 07 22

• July 22th 2020, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

Topics

• poll reminder

• 8.12 issues:

  • https://github.com/coq/coq/issues/12564 native flag doc
  • https://github.com/coq/coq/issues/11178 native-compiler slow on OSX
  • https://github.com/coq/coq/issues/11107#issuecomment-567040281 same but with flambda and both on OSX and linux

• A few questions on problems with the current Hint implementation [Emilio]

• Dependency of extraction of modules on their signature and sealed status (PR #12429) (Jason, requesting Hugo and Maxime for discussion)

Notes

• poll reminder

  We'll resume on September the 2nd.

• 8.12 issues:

  • https://github.com/coq/coq/issues/12564 native flag doc
  • https://github.com/coq/coq/issues/11178 native-compiler slow on OSX
  • https://github.com/coq/coq/issues/11107#issuecomment-567040281 same but with flambda and both on OSX and linux

  Workaround for OS X dynlinking native files being really slow by 8.12.1

  Need clearer numbers on Linux.

  Emilio will try to clarify the situation.

• A few questions on problems with the current Hint implementation [Emilio]

  Currently terms-as-hints considered fragile. CoLoR is still problematic due to its use of them in functors (Pierre-Marie is on it).

• Dependency of extraction of modules on their signature and sealed status (PR #12429) (Jason, requesting Hugo and Maxime for discussion)

  The current bugfix is introducing more complexity and changes the behavior in some cases, which might result in breaking extraction elsewhere. E.g. adding a sealing really changes the meaning of extraction...

  Separate commands for dropping definitions and inlining of definitions in extraction would give a clearer separation of concerns. Jason, Maxime and Kazuiko favor that solution over the current PR. Summary at the end of PR#12429.