Deploying SAW's Written Materials

[ChrisEPhifer]

Deploying the SAW Manual and Tutorials

This issue summarizes my investigation into deploying the critical written
SAW materials (the manual, the LLVM/Java tutorial, and the Rust tutorial).
A sensible deployment scheme is necessary to (1) make long-needed structural
and content changes to these resources for accuracy and cohesion now and in the
future, (2) deploy new releases of SAW, and (3) keep the online versions of
these resources, now available at https://tools.galois.com/saw, up-to-date.

First, I outline the current state of how these materials are handled.
I then propose an approach to deployment for the team's consideration that makes
use of pre-existing mechanisms for synchronizing content on GitHub with content
on GitBook.

The Current State of Things

We currently store the SAW manual and tutorials (as Markdown / TeX sources and
rendered PDFs) in the saw-script repository.

Updating these materials (properly) currently entails:

1. Editing the Markdown source(s)
2. Re-generating the PDF(s)
3. Committing/pushing the updated source(s) and the PDF(s)
4. Publishing the updated content to the Web¹

Steps 2 (with the second clause of 3) and 4 are notably unideal: The former
because we are already version-controlling the sources from which the PDFs are
built, and the sources ought to be the source of truth; the latter because human
memory is fallible, and it is extremely easy for the in-repository and
published-online versions to fall out of sync (indeed, as of this writing, that
is the case).
Furthermore, because I am currently the only developer with access to both
saw-script and the GitBook instance powering the online versions of these
materials, the final step relies on me tracking PRs here for manual/tutorial
changes that need to be published, performing those updates manually on GitBook..

Ideally, we would have a scheme that entailed only:

1. Editing the Markdown source(s)
2. Committing/pushing the updated source(s)

Where the PDFs are generated as part of CI (or, we abandon that particular
rendering entirely²) and the final step is handled by the solution
suggested below.
This would lower the burden on all SAW contributors, who before may have
been incentivized to avoid updating the manual or tutorials alongside their
other work, due to the extra efforts necessary.

The (Potential) Future State of Things

Disclaimer: I don't have a good testing strategy in mind for this, seeing as
most of what we would want to test is the deployment to GitBook itself.
Much like CI, we may just need to make attempts until we get it working.
If it is possible to create unpublished spaces in GitBook, that would be about
as well as we could do in terms of testing deployment isolated from the existing
SAW space with which we'd like to be synchronized.
If/when I am granted elevated GitBook permissions, I will explore this
possibility.

Before outlining the solution I have come up with, there is a seemingly even
easier option worth stating explicitly:

Remove the documentation from this repository entirely, allowing it to be
version-controlled exclusively via GitBook.

This solution has a glaring disadvantage that invalidates it immediately: There
is extremely limited access to the GitBook instance due to its pricing model,
leaving no way for an arbitrary SAW contributor to update documentation
(e.g. when adding/updating features or deprecating commands) without being
artificially bottlenecked by said limited access.

The solution I propose addresses this concern by, instead of removing one of the
version-controlled instances, synchronizing the two going forward, using the
"GitHub Sync" feature of GitBook.
This approach allows for bi-directional content updates subject to a review
process (PRs on GitHub, "change requests" on GitBook).

My GitHub and GitBook accounts are already associated with one another, meaning
(with AndrewS's permission/help) I can connect the SAW space to
all or part of a GitHub repository.

Additionally, we are already on our way towards a proper setup of the
saw-script repository to synchronize with the SAW space on https://tools.galois.com.
Below, I detail what changes we'll need to make to make sure nothing at the new
site inadvertently breaks upon implementing this new setup.

Preparing saw-script

The following will need to be updated in this repository before GitHub Sync can
be enabled and perform the synchronization that we desire:

1. The content in doc/ must be rearranged and augmented to, upon
   synchronization, maintain what is currently available at https://tools.galois.com/saw.
   This is (mostly) bookkeeping of names, and adding suitable Markdown files for
   all of the pages not currently maintained in this repository.
   The SUMMARY.md described below outlines the work necessary in this step.

2. A .gitbook.yaml will need to be added to the root of the repository.
   I believe the following will be appropriate, given corresponding changes in
   (1):

   root: ./doc/
   
   structure:
     readme: README.md # TODO!
     summary: SUMMARY.md # TODO!

3. Add doc/README.md, which will contain the contents one currently sees
   at https://tools.galois.com/saw.

4. Add doc/SUMMARY.md, which will define the navigation (i.e. table of
   contents) seen on that same page.
   The contents of the file will be something like:

   # Summary
   
   ## Documentation
   
   - [Manual](documentation/saw-manual.md) # NOTE: This is doc/manual/manual.md!
   - [Tutorials and Publications](documentation/tutorials-and-publications/README.md) # TODO!
     - [Program Verification with SAW](documentation/tutorials-and-publications/program-verification-with-saw/README.md) # TODO!
       - [Getting Started](documentation/tutorials-and-publications/program-verification-with-saw/getting-started.md) # TODO!
       - ... # NOTE: Omitting a bunch to keep this brief...
       - [Glossary](documentation/tutorials-and-publications/program-verification-with-saw/glossary.md) # TODO!
     - [Tutorial (Rust)](documentation/tutorials-and-publications/tutorial-rust.md) # NOTE: This is doc/rust-tutorial/rust-tutorial.md!
     - [Tutorial (LLVM/Java)](documentation/tutorials-and-publications/tutorial-llvm-java.md) # NOTE: doc/This is tutorial/tutorial.md!
   
   ## Open Source
   
   - [Overview](open-source/overview.md) # TODO!
   - [How to Contribute](open-source/how-to-contribute.md) # TODO!
   
   ## Download
   
   - [Get SAW](download/get-saw.md) # TODO!

   Notice that this matches the current layout of https://tools.galois.com/saw,
   down to the precise names used for pages (so we do not break any links in or
   out when synchronizing for the first time).

These preparations are the bulk of the work to set up synchronization.

Enabling/Configuring GitHub Sync

Important! For testing purposes, create a private/hidden GitBook space to
use in step (2) below before acting on the existing SAW space.
This will help with debugging any potential deployment issues.
Similarly, for step (3), consider selecting a branch other than master on
which to test, so no inadvertent accidents happen to our cutting-edge SAW work.

1. Be sure saw-script is prepared as described above.
2. Enable GitHub Sync in the SAW GitBook space, and install the GitBook app
   to the GaloisInc organization.
   (AndrewS will need to escalate my access to GitBook to complete this step.)
   IT may need to be involved too, as the GitBook GitHub app will need to be
   installed to the GaloisInc organization (ideally, with access to all
   repositories so we can use this setup for future spaces on https://tools.galois.com,
   such as that for Cryptol).
3. Select saw-script and the master branch (see important note above!)
   This will sync commits to master to the GitBook change history.
   Dually, if change requests are accepted/merged on GitBook, corresponding
   commits will automatically be added to master.
4. Perform the initial sync in the GitHub -> GitBook direction, so the
   content in the repository is used to determine the content of the SAW space
   on GitBook.

From this point forward, no additional process is required.
Changes made to the manual and tutorials (or any of the other resources added to
power the new site), upon being committed to master, will make their way into
the GitBook site, automatically keeping the online renderings up-to-date.

Starting From GitBook Instead

It is possible to perform an initial sync in the other direction, from GitBook
to GitHub.
We could, instead of what is outlined above:

1. Rename doc/ to doc_old/, creating a new/empty doc/.
2. Add a .gitbook.yaml containing only root: ./doc/.

These changes must be committed/merged to master before continuing.

Then, follow the steps in the previous section, except at step (4), perform the
initial sync in the GitBook -> GitHub direction.

While this seems like an overall simpler setup process (as it avoids creating
the additional pages we don't already have sources for), it has a number of
disadvantages:

• This approach requires some unnatural commits to master before the initial
  sync is performed.
  The preparation necessary for an initial GitHub -> GitBook sync, while clearly
  more complex, at least makes logical sense as changes to the saw-script
  repository.
• We are at the mercy of GitBook's naming / decision-making about the layout of
  the Markdown files.
  By controling the layout up front and in the repository, we are able to
  maintain that layout (and any potential changes to it) in the repository,
  rather than having to adapt to GitBook's decisions.
• The content at https://tools.galois.com/saw is outdated, and care must be
  taken to use the up-to-date versions of the manual/tutorials during the change
  from doc_old/ to the newly-fetched doc/.
  By starting from the repository's layout, we guarantee our initial sync pushes
  this most up-to-date version to GitBook straight away.

By handling repository preparation ourselves, we also give ourselves the
chance to do a full pass over all of the content, allowing for glaring issues to
be addressed as we go about this change.

Advantages/Disadvantages

This approach has significant advantages over a home-grown solution, but is also
subject to disadvantages, largely in the difficulty of testing/debugging the
solution, and the tedium of preparing the repository.

On the positive side:

• We finally achieve a single point of truth for SAW's written materials.
• Any and all updates to the written materials, from any SAW contributor, will
  be reflected online immediately upon committing to master.
  In addition, this mechanism adds a 'preview' to PRs on GitHub allowing
  contributors to see the effect of any changes to the manual/tutorials/other
  documentation before finalizing the merge, so they know any content updates
  render properly - no need to generate HTML/PDFs locally.

As for negatives:

• Besides targeting a private/hidden space (and using a branch other than
  master) before official deployment, there is no straightforward way to test
  this synchronization mechanism.
• Porting the "Intro to Verification with SAW" will be a bit of a pain, despite
  the work already done to get it on the new site (because GitBook does not
  provide a way to download the Markdown sources, except through GitHub Sync.)
  If we want to avoid that work, we would need to take the GitBook -> GitHub
  initial sync approach.
• We need to be careful not to break existing external/internal links at https://tools.galois.com/saw.

All of these negatives are a one-time cost rather than long-term maintenance,
leading me to believe this is our best bet given the positives.

Footnotes

1. Indeed, this step used to be even more involved, requiring an
   additional step to generate suitable HTML to deploy to https://saw.galois.com.
   This site was replaced with https://tools.galois.com/saw, a GitBook space
   that can (fortunately) render CommonMark Markdown by default. ↩

2. This would be a reasonable choice, as GitBook allows the entire space to
   be exported as a PDF. The "Galois
   Whitepaper" styling is no longer present, however, and can't be added to the
   GitBook system. I doubt this is much of a problem. ↩

[ChrisEPhifer]

After considerable internal discussion, we are not going to take the approach described above.

Most notably, this approach would serve exactly one version of the documentation: That corresponding to the master branch. Given the high volume of changes to SAW coming in the near future, this is not ideal unless we are planning to maintain all versions of the manual in one place (thanks to @sauclovian-g for this observation).

Additionally, the understanding I had of the spaces at https://tools.galois.com was somewhat flawed. These are not intended to be the final home for all things documentation. Rather, they are a hub providing at-a-glance summaries and links out to relevant materials.

Because of this, a more sensible approach would be to take inspiration from Cryptol, which deploys a Sphinx-powered site to GitHub pages (such that per-release-version documentation is always available).

Roughly, the tasks involved:

• Migrate all content in doc/ to a Sphinx-powered site. This can be the home of the user manual, tutorials, and future resources such as the SAWScript and SAWCore langauge references. For consistency with other Galois projects using Sphinx documentation, we ought to use the ReadTheDocs styling.
• Configure the repository's CI/GitHub Pages setup as Cryptol's is to handle the online Cryptol reference.
• Remove the stale content from https://tools.galois.com, and add links to appropriate GitHub Pages.