analysis
analysis copied to clipboard
math-comp
doc generated with alectryon
~~- I have only seen part of it, it seems to take forever from topology.v~~
but I'm first-time user, I may very well have gotten it wrong @proux01 @thery
Indeed, it's terribly slow (nearly 45 minutes for topology.v), I don't know why, the file is large (4800 lines and generated HTML is 3.7 Mo) but not exceptionally huge. Maybe @cpitclaudel or @ejgallego would have an idea?
I can have a look, thanks for the ping. What commands do I need to run to compile that file?
Maybe @cpitclaudel or @ejgallego would have an idea?
No idea, other than the well-known efficiency problems as of today; we are working on some workarounds that I feel should help a lot [pyCoq and coq-layout-engine], mainly the allowing tools such as Alectryon do everything in a single pass [no roundtrip] , but still not there yet.
Did you try --html-minification #cpitclaudel/alectryon/issues/35
I just tried but it ends up with an error (^CTraceback (most recent call last): ..., referring to .py files from alectryon) this time after about 30 min.
I can have a look, thanks for the ping. What commands do I need to run to compile that file?
Thanks for your time (and for the tool, the rendering is nice).
make alectryon. This is a target in Makefile.common.
I got a bit more feedback from @ejgallego : https://github.com/ejgallego/coq-serapi/issues/260
It looks like it is going to be difficult to use alectryon for us. :-(
I tried again today with Alectryon 1.4.0, coq-serapi 8.15.0+0.15.0, coq 8.15.2 and it seems that it could generate html versions for all files, see https://math-comp.github.io/analysis/htmldoc_master_alectryon/.
However there were a number of warnings (Dynlink error... The offending chunk is deliminated by...) and
a critical error ([sertop] Critical Dynlink critical).
I guess that part of the problem is that alectryon does not find .vo files despite the -R options
that I maybe got wrong.
--html-minification does not seem to have a visible effect.
Is there a way to hide the Proof. ... Qed. blocks?
Great work!
Is there a way to hide the Proof. ... Qed. blocks?
Not built-in; it's relatively easy to add it as a custom script, but the exact process depends on what you need. Do you want them removed completely, or dynamically shown/hidden with a click?
However there were a number of warnings (Dynlink error... The offending chunk is deliminated by...) and a critical error ([sertop] Critical Dynlink critical).
How annoying. I didn't have time to work on Alectryon while I was at AWS, but I'm planning to resume now that I've moved. Is there a simple recipe I could try out?
--html-minificationdoes not seem to have a visible effect.
Maybe I can try to help with that too.
Do you want them removed completely, or dynamically shown/hidden with a click?
Dynamic would be great but we were only thinking about hiding as with coqdoc. In fact, so far, we were mostly thinking of using alectryon as a replacement for coqdoc to generate the documentation of MathComp-Analysis as in: https://math-comp.github.io/analysis/
Is there a simple recipe I could try out?
Maybe clone this branch https://github.com/math-comp/analysis/tree/alectryon
and try make alectryon. This takes some time.