Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ci: add a check for the cryptol book pdf #1754

Merged
merged 2 commits into from
Sep 20, 2024
Merged

ci: add a check for the cryptol book pdf #1754

merged 2 commits into from
Sep 20, 2024

Conversation

marsella
Copy link
Contributor

Follow up to #1748.

This adds a small CI job that will shout if you either

  • update the ProgrammingCryptol PDF without changing the source code
  • update the book source code without changing the PDF

@sauclovian-g Do you want this requirement to be documented in a README somewhere? Or maybe CONTRIBUTING.md?

@sauclovian-g
Copy link
Contributor

Yeah, it would be good to document that. contributing.md is probably the right place (make a section about updating the documentation, basically should say something like any required documentation updates should be included with pull requests, these are the different pieces of documentation, this is how you build each one -- I'm happy to write all that if you don't want to but I don't have all the details at my fingertips)

Copy link
Contributor

@sauclovian-g sauclovian-g left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Apart from the usage point Ryan made, LGTM.

This could be written to not depend on bash but there's probably no point.

- updates contributing file with a brief overview of kinds of
  user-facing documentation
- minor updates to book-building CI documentation
@marsella
Copy link
Contributor Author

contributing.md is probably the right place

I added an overview of the docs I could find. I didn't go super deep but I tried to cover everything I could see in the docs/ directory.

This could be written to not depend on bash

I thought you might say that 😁 I figured I had a decent argument in that it's primarily being run in CI and the ubuntu base image comes with bash by default so we're not going to have to negotiate with all our supported platforms.

@sauclovian-g
Copy link
Contributor

contributing.md is probably the right place

I added an overview of the docs I could find. I didn't go super deep but I tried to cover everything I could see in the docs/ directory.

Thanks!

This could be written to not depend on bash

I thought you might say that 😁 I figured I had a decent argument in that it's primarily being run in CI and the ubuntu base image comes with bash by default so we're not going to have to negotiate with all our supported platforms.

I always do :-) shell scripting is an ancient art and bash feature bloat is not part of it. But in practice it doesn't really matter -- the important part is to avoid bashisms if you have #!/bin/sh, because that really will fail and not just on BSD. Requiring that bash is installed is vaguely annoying... but de facto it's very difficult to avoid so in our context it isn't worth spending measurable amounts of time on.

There are two reasons to avoid using bash at all; one is that it's extremely bloaty (load image is about 1.3M on netbsd vs. around 200K for /bin/sh) and the other is that it's phenomenally slow compared to other sh implementations. But neither of these things actually matters in practice most of the time.

@marsella marsella merged commit 5089ad3 into master Sep 20, 2024
49 checks passed
@marsella marsella deleted the add-book-ci branch September 20, 2024 19:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants