Skip to content

Commit

Permalink
Merge pull request #1754 from GaloisInc/add-book-ci
Browse files Browse the repository at this point in the history
ci: add a check for the cryptol book pdf
  • Loading branch information
marsella authored Sep 20, 2024
2 parents c2e3772 + d6c1f0f commit 5089ad3
Show file tree
Hide file tree
Showing 4 changed files with 130 additions and 7 deletions.
47 changes: 47 additions & 0 deletions .github/check_book_update.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
#!/usr/bin/env bash
#
# Indicates whether the Programming Cryptol book PDF needs to be updated.
#
# Usage
# This is primarily for use in CI. You can run it locally using the following:
# > bash check_book_update.sh $(git diff --name-only --diff-filter ACDMRT master)
#
# If you are merging to a branch other than `master`, use that branch name
# instead.
#

TEX_CHANGED=0
PDF_CHANGED=0

# Examine the set of changed files to see if either the book source code
# or the book PDF were changed.
for fname in $@ ; do
case $fname in
docs/ProgrammingCryptol/*)
TEX_CHANGED=1
TEX_FILES="$TEX_FILES$fname " ;;
docs/ProgrammingCryptol.pdf)
PDF_CHANGED=1 ;;
esac
done

if (($TEX_CHANGED)) && ((! $PDF_CHANGED)); then
echo -e "Changed files: $TEX_FILES"
echo "The Programming Cryptol source code changed, but the PDF was"
echo "not updated. Please rebuild the book to incorporate your changes"
echo "and copy the file to 'docs/ProgrammingCryptol.pdf'."
exit 1
elif (($TEX_CHANGED)) && (($PDF_CHANGED)); then
echo "Thanks for updating the PDF along with your changed source code!"
echo "This CI job doesn't check that you incorporated all the source"
echo "changes into the PDF; please confirm that it's properly updated"
echo "before merging."
exit 0
elif ((! $TEX_CHANGED)) && (($PDF_CHANGED)); then
echo "The Programming Cryptol PDF changed but there was no corresponding"
echo "change to the source code."
exit 1
else
echo "There were no changes to the book. No action needed."
exit 0
fi
21 changes: 21 additions & 0 deletions .github/workflows/book.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
#
# Checks that the PDF version of the Programming Cryptol book was updated
# if and only if the constituent source files were changed.
#

name: Programming Cryptol PDF Update
on: [pull_request]

jobs:
update_needed:
runs-on: ubuntu-latest
steps:
- id: checkout
uses: actions/checkout@v4
with:
fetch-depth: 0
- name: "Check if update to local PDF is needed"
run: |
changed_files=$(git diff --name-only --diff-filter ACDMRT ${{ github.event.pull_request.base.sha }} ${{ github.sha }})
# This will fail if any files have spaces in the names.
bash .github/check_book_update.sh $changed_files
46 changes: 45 additions & 1 deletion CONTRIBUTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ It describes our methods and practices for:
- Testing and continuous integration
- Organizing, branching, and merging this repository
- Producing and publishing release artifacts
- **TODO**: documentation
- Documentation
- **TODO**: feature/release planning, ticket assignment, etc

This is a living document that is not (and possibly cannot be)
Expand Down Expand Up @@ -252,3 +252,47 @@ The release process is:
- <cryptol-team@lists.galois.com>
- <cryptol-users@community.galois.com>
- @galois on Twitter (for major releases)

# Documentation

There are several overlapping forms of documentation for users of Cryptol:
- the Programming Cryptol book;
- the reference manual; and
- other miscellaneous design docs and changelogs.

These all live in the `docs/` directory.
Some of these forms of documentation, including the book and some of the
design docs, are housed here both in source (LaTeX source code, markdown
files) and compiled (PDF) formats.

Contributors should update the relevant documentation when they modify or
extend user-facing features. Updates should be included in with pull requests
that change the relevant feature. Contributors should re-build any PDFs or
other artifacts when changing the corresponding source code.

## Programming Cryptol
The book lives in `docs/ProgrammingCryptol/`. There's a `Makefile` to build
it. The compiled artifact lives in `docs/ProgrammingCryptol.pdf`; the
`Makefile` does not build to that location, so updated artifacts need to be
copied over. The CI aims to check whether the source and the artifact were
updated in tandem (see `.github/workflows/book.yml`).

## RefMan
The reference manual lives in `docs/RefMan/`. There's a `Makefile` to build
it locally. It's also built by the CI on pull request and deployed to the
website (see `.github/workflows/docs.yml`), which allows users to browse
manual versions corresponding to the `master` branch, any release, and any open
PR. There are no artifacts that need to be manually maintained by contributors.

## Other documentation
There is a variety of other documentation, such as
- The Cryptol preliminaries document (`docs/CryptolPrims.pdf`);
- The Cryptol syntax guide (`docs/Syntax.pdf`);
- The parameterized module guide (`docs/ParameterizedModules/`); and
- other design docs and guides in `docs/`.

Many of these are overlapping with or subsumed by the reference manual and the
book. We recommend that contributors do not build on these documents and
instead focus their efforts on the reference manual and the book. However, if
the source for these is updated, the corresponding PDFs should also be updated
using `pandoc` (see `docs/ParameterizedModules/Makefile` for an example).
23 changes: 17 additions & 6 deletions docs/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,15 @@
Programming Cryptol README
## Programming Cryptol README

The Programming Cryptol book source code is in `docs/ProgrammingCryptol/`.
It can be built using the `Makefile` in that directory.

There is a pre-built PDF version of the book in this directory. Any updates
to the source code must be accompanied by a corresponding update to the stored
PDF. Developers should build the PDF locally (the default build location
is `docs/ProgrammingCryptol/tmp/Cryptol.pdf`), copy it into this directory,
and rename it to `ProgrammingCryptol.pdf`.

### Other usage notes

To use the check-exercises tool, invoke via `cabal v2-exec
check-exercises --`. This requires the path to the LaTeX file to be
Expand All @@ -13,7 +24,7 @@ following commands:
This is the markup equivalent of the `Verbatim` environment.
However, it has the added effect of adding every line of the block
to a list of commands to be issued to the cryptol REPL.

* `\replin|...|`

Inline equivalent of `replinVerb` environment. Markup equivalent of
Expand All @@ -30,8 +41,8 @@ following commands:

This is the markup equivalent of the `Verbatim` environment.
However, it has the added effect of adding every line of the block
to the expected output of the preceding `\replin` commands.
to the expected output of the preceding `\replin` commands.

* \replout|...|`

Inline equivalent of `reploutVerb` environment. Markup equivalent of
Expand All @@ -49,13 +60,13 @@ following commands:
Like `\replout|...|`, but is not rendered at all by LaTeX. This is
for recording "hidden" output from the REPL that we don't want to
include in the PDF.

* `\restartrepl`

This has the effect of terminating the current input/output REPL pair. If
there is input but no output, then instead of checking the output, the tool
checks that the input does not raise an error.

This command is used to divide the REPL input/output pairs into distinct
"blocks" that get submitted to the REPL independently. Therefore, this command
should be called every time we are defining a new REPL pair; in particular, it
Expand Down

0 comments on commit 5089ad3

Please sign in to comment.