Rewrite CI scripts

[favonia]

I was intrigued by #1096, #1098, and #1099 and decided to take a curious look. The current build system is a bit more complicated than I expected. Currently, I am cleaning up the scripts while learning them. This is still a WIP and, while I'm hopeful, I can't guarantee I would achieve something better in the end.

• Rewrite updater of errata.tex
• Rewrite the script for make dvi
• Skip the testing of make default in the presence of update-nightlies
• Rewrite and split update-nightlies into (1) wiki updater and (2) PDF updater
  • Rewrite the wiki updater
  • Rewrite the PDF updater; blocked by Redirects for nightly builds #1103
• Try other ways to install TexLive (optional)

[favonia]

Updates: the <meta> redirection solution suggested in #1103 has been implemented in this PR. This is a major rewrite. One can now download the PDFs by using these URLs:

• https://hott.github.io/book/hott-a4.pdf.html
• https://hott.github.io/book/hott-ebook.pdf.html
• https://hott.github.io/book/hott-letter.pdf.html
• https://hott.github.io/book/hott-online.pdf.html
• https://hott.github.io/book/errata.pdf.html

When viewed in a browser (not via command line tools), the user will be redirected to the real PDFs, such as https://hott.github.io/book/hott-online-1319-g54f404d.pdf.

I dropped the "nightly" in the URLs but it's easy to put it back.

[favonia]

Some areas for improvements that I intend NOT to address in this PR:

1. Do people still care about DVIs? Can we drop the support for DVIs altogether?
2. Building these PDFs takes lots of time. Some thoughts:
   • Can the build system be made a bit more "parallel"? I tried forcing the make to run tasks in parallel and it did not end well.
   • Can we somehow restructure the LaTeX source so that it does not have to be rerun so many times?
3. Perhaps it would be helpful to find or even build a smaller texlive Docker image to reduce the build time.

[mikeshulman]

Nice! Is this ready to merge?

I don't suppose there's any way for the redirecting URLs to end in .pdf without the extra .html.

Did we ever support DVIs? I don't remember ever offering them for download.

Does it really matter how long the build takes? It only needs to be run when new changes are merged into the repository, which is quite infrequent.

[favonia]

Nice! Is this ready to merge?

Yes. We can just merge it now!

Did we ever support DVIs? I don't remember ever offering them for download.

We check whether make dvi will run successfully every time, even if the generated DVIs are not used. I feel we could potentially remove all the code about DVIs, including the relevant code in Makefile. However, I intend not to make these changes in this PR even if we want to cut all the DVI-related code.

Does it really matter how long the build takes? It only needs to be run when new changes are merged into the repository, which is quite infrequent.

It's mostly my perfectionism kicking in. Currently, the CI will also be run for every new commit in a pull request (but then the script will not push any changes to the website or the wiki unless it's run on the master branch). It is potentially useful to know whether some changes would break something as soon as possible. I have tried to reduce the time to about 6-7mins by not building all the PDFs (that is, not running make all but only making the ones that will be offered for download). I'm more used to squeezing the CI time down to 3mins or less but 6-7mins in any case will not be the end of the world. So, in sum, it's probably okay.

[mikeshulman]

Thank you very much for doing this!!

[favonia]

I don't suppose there's any way for the redirecting URLs to end in .pdf without the extra .html.

Sorry I somehow missed this. It's actually already working. You can drop the .html. I was a bit hesitant because I am not sure whether GitHub will change this in the future and/or whether some browsers will rely on the file extension .html to correctly interpret the resource (they should not... but I don't have control over them). Shorter URLs are great to tell other people where to download the PDFs, but I would use longer versions on https://homotopytypetheory.org/book/, for example.

Currently, these two are the same:

• https://hott.github.io/book/hott-a4.pdf
• https://hott.github.io/book/hott-a4.pdf.html

[mikeshulman]

Can we do something to prevent these actions from trying to run on forks?

[Alizter]

@favonia

 if: github.repository_owner == 'HoTT'

or something should do that. You will probably have to put a step in each workflow to exit early if it is the wrong owner.

[favonia]

We can attach an if to a job instead of individual steps. Before making a PR, I'd like to learn more about the purpose of stopping these actions. The updates in a forked repository will not affect the main repository (HoTT/book), so the correctness is maintained, and I thought it's good to know whether the CI would have worked. Therefore, I wonder if the concern is about the CI doing useless work? In sum, I wish to know (1) which actions to stop (updating gh-pages, updating wiki, or both? I suppose we still want to try whether make and make dvi work) and (2) the motivation of the changes in case I could come up with some creative solution.

[mikeshulman]

I think it makes sense to compile the book on pushes to forks, but not to try to update any posted versions. I just pulled from upstream and pushed to my fork, and got a notification that pushing to the wiki failed (although not, interestingly, that pushing to gh-pages failed; maybe it actually pushed something to my personal gh-pages?). I don't want everyone with a fork to get notifications like that every time they push.

[favonia]

I don't want everyone with a fork to get notifications like that every time they push.

Got it. I took a look and figured out what was going on: the code I used assumed that wiki pages already existed, but there are no wiki pages on your personal fork. The code was written by other people, and perhaps the easiest fix is to turn it off.

For gh-pages, yes, those files are in https://github.com/mikeshulman/book/tree/gh-pages

[mikeshulman]

Thanks. I don't think everyone with a fork should get versions of the book stored on their gh-pages either.