Stream: Coq users

Topic: Literate programming / html or latex documentation


view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 03 2022 at 18:42):

@Callan McGill as of today Alectryon is your best bet I think

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Callan McGill (Feb 04 2022 at 02:12):

Alternatively, can one directly add arg -noinit to a source file somehow

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Callan McGill (Feb 04 2022 at 03:16):

That is perfect, thank you very much :big_smile:


Last updated: Jan 29 2023 at 06:02 UTC