diff --git a/.github/check_book_update.sh b/.github/check_book_update.sh new file mode 100644 index 000000000..dea6ed5ac --- /dev/null +++ b/.github/check_book_update.sh @@ -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 diff --git a/.github/workflows/book.yml b/.github/workflows/book.yml new file mode 100644 index 000000000..b9bb7f037 --- /dev/null +++ b/.github/workflows/book.yml @@ -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 diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 379744549..862fac6b9 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -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) @@ -252,3 +252,47 @@ The release process is: - - - @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). diff --git a/docs/README.md b/docs/README.md index 743d7df8e..3c0b581f8 100644 --- a/docs/README.md +++ b/docs/README.md @@ -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 @@ -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 @@ -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 @@ -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