Coq Call 2024 05 28
- May 28th, 4pm UTC+2 (Paris time zone offset)
- https://rdv2.rendez-vous.renater.fr/coq-call
Participants:
- Looking for feedback on CEP #89 about merging the universe execution paths in
declare.ml(itself on top of #18795) and more generally on various questions arounddeclare.ml[Hugo, 20 mins] - Need help to fix Coq on MacOS [Michael S, 10 min]
- issues with XCode on MacOS Sonoma (Coq crashes in rare but 100% reproducible cases, not a stack overflow)
- older (working) versions of XCode are very hard to use (cannot compile UI software (Coqide), so XCode needs to be switched around)
- failed to patch the OCaml opam packages to use GCC as compiler (XCode is hard coded for OCaml in opam on MacOS and for whatever reason opam ignores my patches)
- reporting the XCode issue is difficult without some analysis of what is going on
- there won't be any Coq Platform releases unless I have at least a work around for this
- 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.