Shorten duration of documentation CI job.

[Zimmi48]

@palmskog You were worried about CI length: it turns out that the CI job that was already the lengthiest (building the documentation) is impacted by the addition of Gaia as a dependency, since it also needs to install all of hydra-battles dependencies. I'll open a separate issue about this.

Originally posted by @Zimmi48 in #55 (comment)

More generally, the duration issues of this job come from several sources:

• install dependencies: 9 minutes
  • the introduction of Gaia impacted this duration by about 6 minutes
  • before then, there was already the issue of building mathcomp, because the workflow uses the standard Coq images to be able to set the correct OCaml compiler version for SerAPI
• install Alectryon: 4 minutes (this includes in particular building SerAPI and its dependencies).

It seems to me that there are only two solutions: building a custom Docker image or updating this workflow to rely on Nix instead of Docker-Coq-Action. I will attempt the latter, but it may take a while.

[palmskog]

I also believe the best solution is to switch to Nix for documentation deployment. I think there is hope that there will eventually be Docker images that contain both SerAPI and Alectryon and recent OCaml (e.g., https://github.com/coq-community/docker-coq-action/issues/57), but that may take even longer than the Nix update.

Another thing that could help the documentation job go quicker is to make sure it uses Dune to selectively build the needed Coq parts (for example, I don't think Pierre has plans to include the Gaia bridge code in the book for a while).

[Zimmi48]

Another thing that could help the documentation job go quicker is to make sure it uses Dune to selectively build the needed Coq parts (for example, I don't think Pierre has plans to include the Gaia bridge code in the book for a while).

This, or even adapt doc/movies/Makefile so that the dependencies of the listed COQ_FILES are built with the coq_makefile setup.

[Casteran]

Indeed, I think I will spend at least a few weeks (months ?) to - adapt to Alectryon the files part-hydras.tex and chapter-primrec.tex - develop .v files in theories/gaia (and learn a little ssreflect :-) ) In a first time, I can also write a little doc on the Gaia bridge, with the old Coqsrc and Coqanswer blocks, while there remains building issues. It’s not hard to convert them to snippets. I think also that it will be also necessary to adapt doc/movies/Makefile for documenting theories/additions/ with Alectryon.

…

Le 18 août 2021 à 18:56, Théo Zimmermann ***@***.***> a écrit : Another thing that could help the documentation job go quicker is to make sure it uses Dune to selectively build the needed Coq parts (for example, I don't think Pierre has plans to include the Gaia bridge code in the book for a while). This, or even adapt doc/movies/Makefile so that the dependencies of the listed COQ_FILES are built with the coq_makefile setup. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#59 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AJW6FCVSCBPMWB2NRXFGTLDT5PQ3JANCNFSM5CMNL7IQ>. 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>.

[Zimmi48]

FTR, the total doc build duration may currently be negatively impacted by what I noticed in #71 (comment), i.e. the "Build Alectryon snippets" step in the build-doc job does not do anything anymore and the snippet building happen in the "Compile LaTeX document" step. The reason why this may negatively impact build duration is because only the former uses -j $(nproc).