Coq Call 2024 11 12
- November 12th 2024, 4pm UTC+2 (Paris time zone offset)
- https://rdv2.rendez-vous.renater.fr/coq-call
- Renaming the coq-contribs organization and redefinding / expanding its purpose as an archive for Coq/Rocq and Coq-/Rocq-community projects (Théo, 5-10 minutes)
- Rocq Visual identity proposals (Matthieu, 10minutes).
- remove legacy loadng (https://github.com/coq/coq/pull/18385) (Gaëtan, 10min)
- Chairman: Nicolas Tabareau
- Secretary: Pierre Roux
- attending: Emilio Gallego Arias, Yves Bertot, Gaëtan Gilbert, Pierre-marie Pédrot, Pierre Roux, Gabriel Scherer, Matthieu Sozeau, Nicolas Tabareau, Enrico Tassi, Romain Tetley, Théo Zimmermann
- information point: Renaming the coq-contribs organization and redefinding / expanding its purpose as an archive for Coq/Rocq and Coq-/Rocq-community projects (Théo, 5-10 minutes)
- rename coq-contrib to rocq-archive so that it can be used as an archiving place for projects that are no longer actively maintained but could be moved to rocq-community or rocq if they found maintainers
- coq-contrib is no longer maintained but a bot pings us in zulip stream coq-community in case of PR opening (sometimes happen, sometime maintainer found)
- in case a project is submitted to rocq-community but no maintainer is found, can be immediatly transfered to rocq-archive
- renaming to happen immediatly (without priori reservation of name which is a bit painful)
- Rocq Visual identity proposals (Matthieu, 10minutes)
- two offers from an initial dozen from a professional typographer and graphic designer
- traces of Coq remaining (including the three letters C, O and Q), traces of mythology
- two ideas: logo separated from name (elephant ?) or integrated in the R letter (one can see a mountain with a moon, the "hole" of the R reminds a hen/rooster)
- two color themes : blue, gray, red or gray replaced by orange (orange reminds a bit OCaml)
- we need to take a decision on logo and color theme so that work can be continued on website
- link to mathematical prover not obvious (is that the logo of an airline company ?)
- in any case, way better than we we currently have
- advantage of first one: we are not strongly linked with the typography, the R is not hardcoded
- we could add a lambda / a turnstyle, but may make the logo too heavy
- wide majority for the first version (where nobody sees an elephant)
- except in Paris where people find the second one smoother / warmer (the first one is maybe a bit aggressive with the idea of a fast eagle, the acute beak)
- blue / white / red probably not a good idea with current French politics / nationalism
- maybe try something completely unrelated : purple and dark grey for instance (but purple already used by roc lang)
- orange may be too light but darker may be too close from OCaml
- colors from coq-community are nice
- inscribing triangles in the "three O"
- enough feedback for the designer, hope to come back with a new iteration in about two weeks
- technical infrastructure for the website is ready (although currently rocq-prover.org contains only the long-term roadmap)
- remove legacy loading (https://github.com/coq/coq/pull/18385) (Gaëtan, 10min)
- just merged
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.