search

GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.14k stars 123 forks source link

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

Closed marsella closed 1 week ago

marsella commented 1 week ago

Follow up to #1748.

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

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

sauclovian-g commented 1 week ago

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)

marsella commented 1 week ago

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 commented 1 week ago

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.