Latex snippet generation

[Casteran]

I noticed that the movies/*.tex files contain all the Coq code and answers of the corresponding .v file (even the lines which are not contained in any snippet). I don't know wether it really affects the performance of document generation on
long modules (like theories/ordinals/Epsilon0/T1.v or theories/ordinals/Epsilon0/Paths.v.
Perhaps a "lazy" snippet generation is hard to design.

[Casteran]

A possible workaround is to insert systematically comments (*| .. coq:: none |*) (*||*) around every snippet-free region.
I tried it on theories/ordinals/Epsilon0/Paths.v, and it reduced the size of doc/movies/Paths.v from more than 100k lines to just 353 !
I will proceed to a few more experiments.
Notice that this method forbids a user to use Alectryon to look into the so hidden parts of a library

[Zimmi48]

Yes, modules need to be reexecuted by Alectryon to extract snippets from them. I don't think that adding .. coq:: none can prevent that. The only solution I can see would be to cut these modules into smaller pieces.

[Casteran]

OK, I think I’ll finish first the adaptation to Alectryon of the hydras part of the document (75% done already). Then, we can think about how to improve some details. This adaptation takes some time, because I noticed several inconsistencies to fix between the .v files and the Coqsrc and Coqanswer hand-made blocks. Thanks to Alectryon, the snippets inclusions are now consistent by construction 😀

…

Le 23 août 2021 à 13:42, Théo Zimmermann ***@***.***> a écrit : Yes, modules need to be reexecuted by Alectryon to extract snippets from them. I don't think that adding .. coq:: none can prevent that. The only solution I can see would be to cut these modules into smaller pieces. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#64 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AJW6FCUTFSCS7MY2ENKN4YTT6IX25ANCNFSM5CUBBFJQ>. Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email>.

[cpitclaudel]

OK, I think I’ll finish first the adaptation to Alectryon of the hydras part of the document (75% done already). Then, we can think about how to improve some details. This adaptation takes some time, because I noticed several inconsistencies to fix between the .v files and the Coqsrc and Coqanswer hand-made blocks. Thanks to Alectryon, the snippets inclusions are now consistent by construction 😀

Ah, this makes me very happy :)

I noticed that the movies/*.tex files contain all the Coq code and answers of the corresponding .v file (even the lines which are not contained in any snippet).

The revamped driver that I made in #71 doesn't generate these latex files any more; only the snippets.

Perhaps a "lazy" snippet generation is hard to design.

That's pretty much what #71 does :)

A possible workaround is to insert systematically comments (*| .. coq:: none |*) (*||*) around every snippet-free region.

… and indeed this should not be needed any more with #71.