Coq Call 2024 11 12 - coq/coq GitHub Wiki

Topics

  • 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)

Roles

  • Chairman: Nicolas Tabareau
  • Secretary: Pierre Roux

Notes

  • 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