Stream: Coq users

Topic: how to refer to Rocq/Coq theorem prover in a thesis writt...


view this post on Zulip Kiran Gopinathan (Mar 13 2024 at 13:42):

Hiya!! Sorry, this is a slightly non-technical question so I'm sorry if this is the wrong place to ask this. I'm currently working on writing up my thesis and much of my work builds on top of Rocq, so I am referring to it quite a lot in the thesis. My advisor mentioned that actually it hasn't been renamed yet, and actually it is still called Coq, but I figure that my thesis will be more inclusive and forward compatible if I use Rocq.

I was thinking about opening an issue on the github about this, but thought the Zulip might be a better option.

view this post on Zulip Gaëtan Gilbert (Mar 13 2024 at 13:53):

It is indeed still called Coq.

view this post on Zulip Kazuhiko Sakaguchi (Mar 13 2024 at 14:16):

Perhaps you can define a LaTeX macro \Coq, and change its definition if renaming happens before the defense.

view this post on Zulip Kiran Gopinathan (Mar 13 2024 at 14:26):

Hmm, I see, yes, @Kazuhiko Sakaguchi that seems like the best way to go then. I'll just use a macro, and change it if the renaming goes forward before the defence. Thankfully the size of Rocq and Coq are fairly close so it shouldn't affect typesetting much.

view this post on Zulip Julien Puydt (Mar 14 2024 at 12:26):

sed -i *.tex -e "s/Coq/Gallo/g"

is also a one-line solution.

view this post on Zulip Gaëtan Gilbert (Mar 14 2024 at 12:33):

what is Gallo?

view this post on Zulip Théo Winterhalter (Mar 14 2024 at 12:35):

Also wouldn't that change Thierry's surname as well?

view this post on Zulip Kazuhiko Sakaguchi (Mar 14 2024 at 12:37):

Indeed, defining a LaTeX macro would be a bit more robust.

view this post on Zulip Julien Puydt (Mar 14 2024 at 13:12):

Gallo is Coq in italian, portuguese and spanish

view this post on Zulip Théo Winterhalter (Mar 14 2024 at 13:15):

Anyway the name is likely going to become Rocq, but the current policy (at least if I remember correctly what was said at CoqPL) is to keep using Coq until the renaming is official.


Last updated: Jun 13 2024 at 21:01 UTC