Callan McGill (Feb 03 2022 at 18:41): Callan McGill (Feb 03 2022 at 18:41):Is there a nice way to do literate programming in coq or turn code into html/latex?
Emilio Jesús Gallego Arias (Feb 03 2022 at 18:42):@Callan McGill as of today Alectryon is your best bet I think
Emilio Jesús Gallego Arias (Feb 03 2022 at 18:42):But if you are willing to put up with a less polished publishing chain jsCoq also allows some of it
Karl Palmskog (Feb 03 2022 at 18:42):The closest we have is indeed Alectryon: https://github.com/cpitclaudel/alectryon
If you want to intermix Coq code and LaTeX, you could use coqdoc like what is done here: https://github.com/ilyasergey/pnp
Karl Palmskog (Feb 03 2022 at 18:45):see here for overview of an experimental toolchain that combines LaTeX and Alectryon and Coq, this is where that code lives: https://github.com/coq-community/hydra-battles/tree/master/doc/movies
Callan McGill (Feb 04 2022 at 01:56):This tool looks excellent! Do you happen to know how if I can make it aware of _CoqProject or directly pass coq options to it as without -noinit I get lots of warnings and errors
Callan McGill (Feb 04 2022 at 02:12):Alternatively, can one directly add arg -noinit to a source file somehow
Callan McGill (Feb 04 2022 at 02:31):I figured out one can pass --coqc-arg=noinit to alectryon but I think I am doing something incorrectly as it doesn't pass that arg to coqc
Li-yao (Feb 04 2022 at 03:12):Try --sertop-arg=--no_prelude. alectryon doesn't call coqc by default, that's why --coqc-arg does nothing.
Callan McGill (Feb 04 2022 at 03:16):That is perfect, thank you very much :big_smile:
Last updated: Sep 25 2023 at 14:01 UTC