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
Last updated: Jun 10 2023 at 06:31 UTC