search

coq-community / hydra-battles

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
https://coq-community.org/hydra-battles/doc/hydras.pdf
MIT License
68 stars 12 forks source link

Shorten duration of documentation CI job. #59

Open Zimmi48 opened 3 years ago

Zimmi48 commented 3 years ago

@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 https://github.com/coq-community/hydra-battles/issues/55#issuecomment-901254993

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

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 commented 3 years ago

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 commented 3 years ago

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 commented 3 years ago

Indeed, I think I will spend at least a few weeks (months ?) to

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 https://github.com/coq-community/hydra-battles/issues/59#issuecomment-901273991, 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 commented 3 years ago

FTR, the total doc build duration may currently be negatively impacted by what I noticed in https://github.com/coq-community/hydra-battles/pull/71#issuecomment-915407650, 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).