Closed jjhugues closed 2 years ago
For the moment, alectryon only supports a per sentence way to hide Coq statements.
Not quite! If you go through reST, you can certainly hide full blocks; for example:
(*| .. coq:: none |*)
Plenty
of Coq
code
that gets
executed but not shown
(*| .. coq:: |*)
More code that gets executed and shown.
The nice part about this is that you get all the reStructuredText authoring support for free within (*| … |*)
comments, too. Check out the example in recipes/literate_coq.v
; I just updated it to cover .. coq:: none
.
But! See below for more details.
Is this something that can be supported or is there a particular reason to not support this?
What I wrote above works if you use the --frontend coq+rst
flag (that's the default for .v
files. If you use the plain coq
frontend these special reST comments are not processed, and indeed there's nothing to hide full blocks in that case. We could consider adding that feature if it helps (it's a pretty simple additional transform, really, in fact there's even a version of it mostly implemented in the custom driver that hydra-battles
currently uses), but in my experience once you start doing this sort of things you're only one step from a full literate document, so it makes things to jump to reST.
Let me know your thoughts!
Thanks for documenting this. I am no expert in reST so I did not think of this trick.
My current project has coqdoc with LaTeX, but I miss a few features since I now need to generate either HTML or a PDF. Having coq+rst to generate rest and then use pandoc is a viable alternative for me.
I guess this issue could be closed, thanks.
I'm not sure pandoc will work for this: it won't know about the .. coq::
directive.
Anything wrong with using alectryon to generate HTML and LaTeX directly? Just alectryon xyz.v -o xyz.tex
should work.
I need to test further. I need to produce a large LaTeX document, so I need something similar to coqdoc: a mode without boilerplate at the beginning. On second thought, it might be easier to implement in alectryon I presume
Which boilerplate are you referring to?
alectryon --frontend coq+rst --backend latex d.v
generates a full LaTeX document, with a preamble with all usepackages, and a begin{document}. I need to generate a LaTeX file without this part so that I can include it in a larger document, the equivalent of body-only
from coqdoc.
alectryon --frontend coq+rst --backend snippets-latex d.v
could be the way to go, but it is rejected by the latest release. Do you have any recommendation?
Oh, I see what you mean, thanks!
There's a few ways to go from here, but I'll fee much more confident in my recommendations if you can give me a bit more info on the specs of what you'd like to do. Do you have an existing document that you're translating, for example?
(Sorry for asking for so much details: it's just that this way I'll be sure that we're not going in the wrong direction based on a misunderstanding ^^)
My requirement is captured in this project: https://github.com/jjhugues/coq-alectryon-template It is similar to the sphinx recipe you have. Both have the same issue actually, see below
I am heavily documenting a Coq development, and would prefer to have the documentation directly in the Coq development. Coqdoc is a great tool but I miss a portable way to include graphics and generate index. reST supports this just fine.
So, this project aims to build a minimal working example, hopefully it can serve others in the community.
theories
to generate files in docs
for inclusion by the reST codeI am investigating the latter. I could have missed something obvious. Comments welcome!
Thanks, it makes sense! When I ran make from the Sphinx folder I got this message:
/tmp/coq-alectryon-template/docs/index.rst:9: WARNING: toctree contains reference to nonexisting document 'hello'
This makes sense because Sphinx only looks in the docs/
folder, not in the theories/
folder. As far as I can tell there's no way to make it look outside of the current Sphinx project folder, either. (Some relevant discussion is in https://github.com/sphinx-doc/sphinx/issues/7000)
I solved this one recently, I no longer have this warning, see https://github.com/jjhugues/coq-alectryon-template/commit/f8e6772d6b1467faf414c9de5ce4e0b840095b59
make generate_doc
now copies files from theories
to docs
(stupid name and approach, but this is a work-in-progress)
The remaining issue is now to generate a full PDF. As I mentioned, neither this project nor your sphinx recipe generates content for the Coq part.
Got it; I will look into the issue.
I opened an issue on the Sphinx side: https://github.com/sphinx-doc/sphinx/issues/9632 The problem is that Sphinx calls Alectryon with a list of supported formats that say only "html" even when it generates LaTeX, so Alectryon produces HTML in all cases, which the LaTeX writer ignores
Should be fixed on the latest master. Please try and let me know. Thanks for the report!
It works, but there are some glitches easy to address. See my next bug reports
For the moment, alectryon only supports a per sentence way to hide Coq statements. I miss something equivalent to
(*begin/end hide *)
to remove large chunks of Coq statements like imports, sections, etc.Is this something that can be supported or is there a particular reason to not support this? Thanks,