Merge pull request #1754 from GaloisInc/add-book-ci

ci: add a check for the cryptol book pdf

.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

.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

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:
     - <[email protected]>
     - <[email protected]>
     - @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).

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