Lazy snippet generation

[Casteran]

@Zimmi48 On this branch I put systematically .. coq:: none blocks around snippet-free regions of Epsilon0/T1.v and Epsilon0/Paths.v The size of T1.tex was reduced by a factor of 70, and Paths.tex by a factor of 336 !
Do you think this can help to reduce documentation generation time too?

[Zimmi48]

Sure, it should help at least a little by avoiding from requesting intermediate goals that are not printed, writing to and reading from disk, and speed up the snippet extraction script. That being said, it's not an important enough speed up to show in the CI numbers. I think that most of the time spent by Alectryon is the time that Coq takes to check proof scripts themselves (whether they are printed or not doesn't change this).

[cpitclaudel]

This looks good. I this we could also achieve this without annotations, by adding a transform that removes all irrelevant code before it gets fed to LaTeX (this is similar to what's being done here, but without annotations.)

[Zimmi48]

I think this has been superseded by #71 and could be closed, right?

[cpitclaudel]

Yep (at least on the movies/ side)

[Casteran]

Ok, So I close the issue …

…

Le 31 août 2021 à 19:35, Clément Pit-Claudel ***@***.***> a écrit : Yep — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#65 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AJW6FCSTHQULODT3F6CEA43T7UHF5ANCNFSM5CUNLPFA>. 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&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.