Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Initial SAW Manual Reorganization #2224

Merged
merged 21 commits into from
Feb 19, 2025
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
bb7842c
Manual: Reorder top-level sections.
ChrisEPhifer Feb 12, 2025
cdffd66
Manual: Demote 'direct-extraction' to subsection of 'loading-code'.
ChrisEPhifer Feb 12, 2025
edf4740
Rename introduction.md -> overview.md.
ChrisEPhifer Feb 12, 2025
af3e999
saw-user-manual/overview: Add recommended new sections to outline.
ChrisEPhifer Feb 12, 2025
4396e95
saw-user-manual/structure-of-sawscript: Add new section to outline.
ChrisEPhifer Feb 12, 2025
998cbc9
saw-user-manual/structure-of-sawscript: Move first simple example.
ChrisEPhifer Feb 12, 2025
6fa6b68
saw-user-manual/invoking-saw: Move content to appendix.
ChrisEPhifer Feb 12, 2025
e94f556
saw-user-manual/specification-based-verification: Revisit example.
ChrisEPhifer Feb 12, 2025
5d8c532
saw-user-manual/appendices: Make separate directory for appendices.
ChrisEPhifer Feb 12, 2025
8350a3a
appendices/glossary: Add an (empty) glossary to the appendices.
ChrisEPhifer Feb 12, 2025
d3e8558
saw-user-manual/appendices: Properly format REPL reference.
ChrisEPhifer Feb 12, 2025
251e486
saw-user-manual/cryptol-and-its-role-in-saw: Fix broken link.
ChrisEPhifer Feb 12, 2025
8e0c99b
saw-user-manual/appendices: Add stubs for additional appendices.
ChrisEPhifer Feb 12, 2025
c40828e
saw-user-manual: Place proofs about terms after term transformation.
ChrisEPhifer Feb 12, 2025
b539c46
saw-user-manual: Clean up some 'glue' text.
ChrisEPhifer Feb 12, 2025
6e37a47
doc: Update PDFs.
ChrisEPhifer Feb 12, 2025
d460fce
Merge branch 'master' into 2156-saw-user-manual-reorg
ChrisEPhifer Feb 18, 2025
b4feed5
saw-user-manual/specification-based-verification: Missing reference.
ChrisEPhifer Feb 18, 2025
2611825
manual/cryptol-and-its-role-in-saw: Note about Cryptol manual link.
ChrisEPhifer Feb 19, 2025
e83e61e
appendices: Replace REPL glossary entries with explicit references.
ChrisEPhifer Feb 19, 2025
3b0b6e2
manual/transforming-term-values: Update section transition language.
ChrisEPhifer Feb 19, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions doc/saw-user-manual/appendices/index.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
# Appendices

:::{toctree}
:maxdepth: 1

repl-reference
:::
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
(appendix-repl-reference)=
# Appendix: REPL Reference
(repl-reference)=
# REPL Reference

The primary mechanism for interacting with SAW is through the `saw`
executable included as part of the standard binary distribution. With no
Expand Down
2 changes: 1 addition & 1 deletion doc/saw-user-manual/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -32,5 +32,5 @@ proofs-about-terms
transforming-term-values
extraction-to-the-coq-theorem-prover
formal-deprecation-process
appendix-repl-reference
appendices/index
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Annoying. Oh well.

```
2 changes: 1 addition & 1 deletion doc/saw-user-manual/invoking-saw.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,5 +4,5 @@
This section is under construction!
:::

See [the REPL reference](./appendix-repl-reference) for additional details about
See [the REPL reference](./appendices/repl-reference) for additional details about
the `saw` executable and its options.