Stream: jsCoq

Topic: coqdoc comments in multiple languages


view this post on Zulip Karl Palmskog (Nov 05 2022 at 09:58):

Could one have coqdoc comments in several languages and allow real-time switching between languages in a jsCoq interface? Would be interesting to have this beginner material available in this way: https://www.math.univ-paris13.fr/~rousselin/commencer_sujet.v

I'm thinking in the direction of annotating the source something like:

(**fr L'équivalence logique est notée en coq [<->].*)
(**en Logical equivalence in Coq is written [<->].*)

view this post on Zulip Shachar Itzhaky (Nov 06 2022 at 11:15):

That's a nice idea; in fact it feels like it would be a pity for this to be a jsCoq-only feature. If users invest the time and effort to write multilingual documents they would probably want coqdoc to also be able to generate outputs in multiple languages.

view this post on Zulip Shachar Itzhaky (Nov 06 2022 at 11:15):

(or is this already a coqdoc feature that I am not aware of )

view this post on Zulip Karl Palmskog (Nov 06 2022 at 12:31):

no, there is no feature like that in coqdoc to my knowledge. Maybe it could be more easily integrated into Alectryon? The reason for jsCoq is that one might use the browser language.

view this post on Zulip Shachar Itzhaky (Nov 06 2022 at 13:20):

sure that sounds plausible. I wonder if at least there is an existing convention for those language tags.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 07 2022 at 15:55):

jsCoq (and coq-lsp) support markdown natively (and LaTeX soon) so IMHO it would be sense to use existing facilities for these formats


Last updated: Jan 30 2023 at 17:03 UTC