Initial SAW Manual Reorganization #2224
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
See #2156; this implements the parts of @smithdtyler's and @sauclovian-g's suggestions that involved simple reorganization of existing top-level resources. Note that there are no _content_ changes to make this reordering 'flow' properly; there may be confusing references with this ordering as-is.
This was another of @smithdtyler's suggestions (and is certainly appropriate; it's odd that the direct-extraction documentation was ever this far away from other ways of loading code / creating Terms in SAWScript).
This aligns with another recommendation from @smithdtyler.
(Thank you once again to @smithdtyler for this!) This adds new sections to the manual overview (with no content, yet - just "under construction" warnings) as recommended: - SAW Use Cases, to clarify who SAW is for - SAW Terminology, to clarify how SAW is discussed - Running Example, to clarify how SAW is (generally) used, and enhance later sections of the manual by referencing the same example
Namely, "Parts of a SAW Script". Like before, there is no content other than a warning that this part of the manual is under construction.
As @smithdtyler rightfully points out, this was way later in the manual than it ought to have been, so this commit moves it up where they suggest, and tweaks the wording slightly to better fit in. Despite that tweak, the same "under construction" message used previously is repeated here to emphasize the content is subject to change.
The existing content here is better in an appendix dedicated to the REPL and its options/use. It ought to be replaced with common usage, some examples, and a reference to the appendix for additional detail. The last of these items is completed by this commit; the others are noted in the "under construction" warning for this page, which was added in place of the original text (which moved wholesale to the appendix).
Rather, add a section to do so (for convenience, the "under construction" message provides a cross-reference to the intended "first simple example" to revisit here).
Previously, for the first appendix, we made it a top-level document of the user manual. Since there are a number of other resources we may wish to add to what we consider to be 'appendices' of the manual (e.g. a glossary, a command reference, a full SAWScript language reference), this commit preemptively adds some additional hierarchical structure to the manual to better organize these resources, even if for the time being there is only one. Note that this commit includes appropriate re-titling/re-naming of the one existing appendix, to avoid excessive or redundant use of the word 'appendix' in titles etc.
This document will be the home of definitions of terminology used throughout the
manual that users new-ish to verification, and completely new to SAW, are
unlikely to know.
I decided to leave the glossary empty for the time being, but adding new terms
is very simple:
Definition lists that have a {.glossary} attribute will be able to be
cross-referenced using the {term} role.
So, to add terms, under an appropriate {.glossary}, write:
```markdown
My term
: The definition of my term
```
Then, anywhere else in the document tree, this definition can be referenced
with:
```markdown
{term}`my term`
```
Note that capitalization in the reference is irrelevant.
Sphinx will emit warnings for anything annotated {term} that does not have an
entry in a {.glossary}.
In particular, use proper definition list formatting.
This allows the lists to be turned into glossaries, if desired; as an example,
this commit makes the definition list of environment variables a {.glossary},
and adds some references to these terms to the text where they are mentioned (at
least, the first use -- this isn't a wiki, after all).
The link to the Cryptol programming guide referred to the old cryptol.net, which also has issues redirecting to resources on tools.galois.com. Instead of fixing that redirection (which involves extra steps and effort), this commit instead updates the link to point to the new home of that same programming guide PDF.
In particular, per #2156 and its comments: - A command reference - Deprecated items - A SAWScript language reference The last of these was stubbed as a separate directory, given that the scope of such a reference is likely to warrant / necessitate splitting the contents across multiple files. The others are single-file documents at the top of appendices.
As written, this is a more logical ordering of these manual sections. Most importantly, the proof-about-terms document references ideas introduced in the transforming-term-values document; thus, the latter is prerequisite. Later updates to the manual may revisit this, but significant changes to the text will be necessary to discuss proofs before transformations.
To avoid big rewrites of whole sections of the manual at this stage, this commit updates the "bare minimum" text necessary to account for the reorganized manual sections.
I'm not entirely sure why the Rust verification tutorial ended up updated; perhaps I missed something in an earlier PR.
sauclovian-g
approved these changes
Feb 13, 2025
| @@ -32,5 +32,5 @@ proofs-about-terms | |||
| transforming-term-values | |||
| extraction-to-the-coq-theorem-prover | |||
| formal-deprecation-process | |||
| appendix-repl-reference | |||
| appendices/index | |||
There was a problem hiding this comment.
Is there a way to get appendices to come out as A. Glossary B. Command Reference C. REPL Reference, etc. instead of being sections 17.1-17.4 of a chapter 17?
(like what \appendix does in latex)
There was a problem hiding this comment.
I chewed on this one for a while, since Sphinx does have a latex_appendices setting.
Unfortunately, without some gnarly convolution, I couldn't get this to behave the way I wanted -- while it would have the desired effect of labeling the appendices as you suggest (with page breaks between), the material ends up duplicated (since, to appear in the HTML render, those documents need to be somewhere in the document tree; latex_appendices naturally only changes the LaTeX output).
At least for now, I say we leave this alone - it seems latex_appendices was designed to include external documents in LaTeX renderings, rather than documents that are already part of the system.
I got aggressive when cleaning up some commits, and removed a helpful reference in the "under construction" warning (helpful in that it highlighted that this section is intended to build on an earlier section).
In particular, a note that the link to the Cryptol programming guide PDF should be made canonical. The note suggests uploading the PDF to the Cryptol repository, as we do with the SAW manual.
This is to avoid undesirable styling of these glossary items in documents (in particular, glossary terms render italicized/emphasized, and this is not appropriate for things like `PATH` and other REPL terms). The approach sacrifices the inline convenience of glossary terms, which allows for freedoms like different capitalization, to achieve control over styling - since this explicit reference approach can be used as any other link.
This is exactly @sauclovian-g's suggestion (#2224 (comment)).
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is an attempt at making the reorganization changes suggested in #2156 without making heavyweight changes to the manual content itself.
sawREPL reference)It may make sense to include additional updates in this particular work, but I'm personally happy merging this progress so others interested in updating manual sections could get started independently.