Coq Call 2022 10 05
- October 5th 2022, 4pm Paris Time
- https://rdv2.rendez-vous.renater.fr/coq-call
- CI setup
- Interim Coordination (Matthieu)
- Non rectypes Nativevalues.t using GADT #16574 (PMP)
-
CI situation. 8 runners brought by Maxime (temporary solution), trying to reduce the CI consumption.
Reduction ideas:
-
only ask for full CI before merge, modifying coqbot to check that (unknown difficulty)
-
disable native compilation by default, only using it before merge / after approval
-
caching can also help (see fast-ci-mode by Emilio, https://github.com/coq/coq/issues/16201)
-
Start CI for a single compiler by default as well.
We should start the CI with one configuration only.
-
Storage: suppress artifacts and logs > 2 or 1 year. Maxime will look into it.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq 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.