Coq Call 2020 07 22 - coq/coq GitHub Wiki
- 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.