Karl Palmskog (Nov 05 2022 at 09:58): 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 [<->].*)
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.
Shachar Itzhaky (Nov 06 2022 at 11:15):(or is this already a coqdoc feature that I am not aware of )
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.
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.
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
Pierre Rousselin (Jul 27 2023 at 19:08):I'm seconding this request for multilingual support. It's easy to add some manual tags to produce different outputs with shell scripts but an extension of coqdoc (with or without jscoq) would be nice. It would also be nice to switch language directly in a web page with (js/wa)coq.
Shachar Itzhaky (Jul 28 2023 at 14:51):@Emilio Jesús Gallego Arias do you know of existing multilingual support in markdown?
Emilio Jesús Gallego Arias (Jul 28 2023 at 15:40):@Shachar Itzhaky I'm afraid not.
Last updated: Apr 20 2024 at 10:02 UTC