Coq Call 2023 10 03
- October 3rd 4pm UTC+2 (Paris time zone offset)
- https://rdv2.rendez-vous.renater.fr/coq-call
-
ensuring Coq remains safe for async interruptions (Emilio, 15min)
- see also https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Situation.20of.20async.20interruptions
- https://github.com/coq/coq/pull/17638
- https://github.com/coq/coq/issues/17760
The problem is well-known, basically any code:
try foo () with | _ -> falseis wrong, as it will consider
foo ()to returnfalseeven when actually what happened is an async exception. This is a problem in practice. At some point I had a PR trying to make some progress on that issue, but likely not the right way https://github.com/coq/coq/pull/15937 -
check on progress for completeing the items in the roadmap (Théo, 5-10min)
- Chairman: ?
- Secretary: ?
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.