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

The SAW Documentation Revolution (Part 1) #2202

Open
wants to merge 71 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
71 commits
Select commit Hold shift + click to select a range
51c669e
doc/internal: Move internal docs to an appropriate directory.
ChrisEPhifer Jan 25, 2025
dc42594
manual/code: Remove unused files.
ChrisEPhifer Jan 25, 2025
6b94ef9
manual: Correct erroneous internal links.
ChrisEPhifer Jan 25, 2025
a2af838
manual: Use a level-1 heading (slightly) more appropriately.
ChrisEPhifer Jan 25, 2025
85e4f55
Update fenced code block language specifiers.
ChrisEPhifer Jan 25, 2025
ea27d89
rust-tutorial: Subtract 1 from all headings after the first.
ChrisEPhifer Jan 25, 2025
e050f28
Normalize the title of the first chapter of each part.
ChrisEPhifer Jan 25, 2025
0df6156
tutorial: Remove PDF (+ generation) and split up tutorial.md.
ChrisEPhifer Jan 25, 2025
f5e4945
tutorial: Consistently use standard Markdown headings.
ChrisEPhifer Jan 25, 2025
748ed1d
tutorial: Use consistent code block style.
ChrisEPhifer Jan 25, 2025
49a85d9
tutorial: Repair broken code references.
ChrisEPhifer Jan 25, 2025
a362222
Move figures directory from tutorial to doc root.
ChrisEPhifer Jan 25, 2025
f9396ec
Rename tutorial -> llvm-java-tutorial.
ChrisEPhifer Jan 25, 2025
e98eea5
llvm-java-tutorial: Update code block style to use colon fences.
ChrisEPhifer Jan 25, 2025
9a72549
rust-tutorial: Remove PDF generation and split up rust-tutorial.md.
ChrisEPhifer Jan 25, 2025
6fd1d87
rust-tutorial: Correct minor errors in Markdown.
ChrisEPhifer Jan 25, 2025
ba8c180
rust-tutorial: Normalize code blocks.
ChrisEPhifer Jan 26, 2025
81a6250
manual: Remove PDF (+ generation) and split up manual.md.
ChrisEPhifer Jan 26, 2025
d4d6411
manual: Correct minor errors in Markdown.
ChrisEPhifer Jan 26, 2025
a416bc9
manual: Further normalize Markdown.
ChrisEPhifer Jan 26, 2025
dba1454
Rename manual -> saw-user-manual.
ChrisEPhifer Jan 26, 2025
92e1d9b
Rename llvm-java-tutorial -> llvm-java-verification-with-saw.
ChrisEPhifer Jan 26, 2025
c4444d1
Rename rust-tutorial -> rust-verification-with-saw.
ChrisEPhifer Jan 26, 2025
c3eed8f
Rename internal -> development.
ChrisEPhifer Jan 26, 2025
e815bc9
Use explicit targets and internal references.
ChrisEPhifer Jan 26, 2025
66aaa4b
development: Split up extcore.md.
ChrisEPhifer Jan 27, 2025
cf1560f
limitations: Remove redundant table of contents.
ChrisEPhifer Jan 27, 2025
226b5ca
releasing: Fix link to `CHANGES.md`.
ChrisEPhifer Jan 27, 2025
8739b29
Preemptively add a useful reference label to the SAW user manual.
ChrisEPhifer Jan 27, 2025
c318c83
releasing: Clean whitespace, remove outdated saw.galois.com link.
ChrisEPhifer Jan 27, 2025
a235e05
Add indices for all SAW documentation.
ChrisEPhifer Jan 28, 2025
f808628
saw-lexer: Add a simple pygments lexer for SAWScript.
ChrisEPhifer Jan 28, 2025
71a2d4a
Prepare doc/ for Sphinx.
ChrisEPhifer Jan 28, 2025
b7e0232
Add a Script that creates a Python virtual environment for SAW docs.
ChrisEPhifer Jan 28, 2025
954ab67
Add helper script to build HTML/PDF documents with Sphinx.
ChrisEPhifer Jan 28, 2025
a15e5b7
Commit PDF renderings of the tutorials and manual.
ChrisEPhifer Jan 28, 2025
4266590
Add a doc/ README.
ChrisEPhifer Jan 28, 2025
76be262
Attempt to fix file-bundling in CI.
ChrisEPhifer Jan 28, 2025
e22e84b
Merge branch 'master' into 2197-deploying-saws-written-materials
ChrisEPhifer Jan 28, 2025
c484801
Fix integration tests that reference documentation code.
ChrisEPhifer Jan 29, 2025
43770b7
doc/bibliography: Restore the bib file from the LLVM/Java tutorial.
ChrisEPhifer Feb 1, 2025
4b34431
rust-verification-with-saw: Replace missing '`' in Cryptol type var.
ChrisEPhifer Feb 1, 2025
b1aa596
Corrections to spelling errors.
ChrisEPhifer Feb 1, 2025
8e0179e
doc/README: Add clarifying reference to description of `make_docs`.
ChrisEPhifer Feb 1, 2025
4971718
doc/README: Remove note about removing `saw-lexer`.
ChrisEPhifer Feb 1, 2025
0eb36f3
doc/README: Add clarifying reference about PDF titles.
ChrisEPhifer Feb 2, 2025
392ae5e
saw-lexer: Cleanup imports.
ChrisEPhifer Feb 1, 2025
98386e9
saw-lexer: Remove special 'Name.Builtin' handling.
ChrisEPhifer Feb 1, 2025
094cdc3
Remove CHANGES mirror from developer docs and restore link text.
ChrisEPhifer Feb 2, 2025
b455635
doc/development: Consolidate extcore documentation into extcore.md.
ChrisEPhifer Feb 2, 2025
53a5dda
Hide SAW developer documentation.
ChrisEPhifer Feb 2, 2025
af6132d
Rename doc/development -> doc/developer.
ChrisEPhifer Feb 2, 2025
d3a27d1
doc/setup_env: Use requirements.txt in the script's directory.
ChrisEPhifer Feb 2, 2025
d0ac195
Create a scripts directory.
ChrisEPhifer Feb 2, 2025
ba3f555
Remove make_docs.sh.
ChrisEPhifer Feb 2, 2025
cf63994
doc/Makefile: Remove / replace Sphinx's default comments.
ChrisEPhifer Feb 2, 2025
e4d1853
Add scripts/package_code.sh.
ChrisEPhifer Feb 2, 2025
b5f8ef1
Makefile: Re-implement the behaviors of the old make_docs.sh.
ChrisEPhifer Feb 2, 2025
54c9c53
Generate PDFs in a (hopefully-reproducible) way.
ChrisEPhifer Feb 2, 2025
ff63fbe
doc/README: Update to reflect recent changes.
ChrisEPhifer Feb 2, 2025
d902766
Merge branch 'master' into 2197-deploying-saws-written-materials
ChrisEPhifer Feb 2, 2025
0ea2d4e
Makefile: Use make's $(shell) function.
ChrisEPhifer Feb 2, 2025
fcb3ce5
sphinx-download-dir: Sphinx role to download directories.
ChrisEPhifer Feb 3, 2025
7c614fa
scripts/requirements: Add sphinx-download-dir.
ChrisEPhifer Feb 3, 2025
bb99e83
.gitignore: Going forward, ignore all tar.gz archives in doc/.
ChrisEPhifer Feb 3, 2025
0b9f94f
Use sphinx-download-dir in the documentation.
ChrisEPhifer Feb 3, 2025
61af74a
Remove scripts/package_code.sh (and Makefile uses of the same).
ChrisEPhifer Feb 3, 2025
34b9624
Update README to reflect sphinx-download-dir changes.
ChrisEPhifer Feb 3, 2025
f8c17f9
Add CHANGES.
ChrisEPhifer Feb 3, 2025
2739adf
Merge branch 'master' into 2197-deploying-saws-written-materials
ChrisEPhifer Feb 3, 2025
2f3970b
Merge branch 'master' into 2197-deploying-saws-written-materials
ChrisEPhifer Feb 3, 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
10 changes: 0 additions & 10 deletions doc/saw-lexer/src/saw_lexer.py
Original file line number Diff line number Diff line change
Expand Up @@ -49,16 +49,6 @@ class SAWScriptLexer(RegexLexer):
bygroups(Keyword.Type, Whitespace),
),
(r"(true|false|abc|z3)(\s+)", bygroups(Keyword.Constant, Whitespace)),
Copy link
Contributor

Choose a reason for hiding this comment

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

not to kibitz further or anything 😸 but abc and z3 should probably get dropped too.

(or add the other solvers, but the full list is pretty large... there's eight each with four variant calls, plus or minus, plus a few addenda)

I think what we should do in the long run is either have saw dump out info from the primitives table, or generate both this and the primitives table from an external definition file. But right now the primitives table doesn't have enough info to make this worthwhile.

(Also what I should probably do at some point is run pygments manually on a bunch of existing proof code and fiddle with the coloring until it looks nice. FUTURE...)

# N.b. The following is very liberal, but also missing many things.
# There is no centralized list of all builtins/primitives/initial
# basis elements...
(
(
r"((?:assume|external|goal|offline|load|print|prove|read|sat|save|write|llvm|jvm|mir|crucible|w4|sbv|unint)_?\w*|"
r"admit|beta_reduce_goal|enable_experimental|java_load_class|quickcheck|return|simplify|split_goal|trivial|unfolding)(\s+)"
),
bygroups(Name.Builtin, Whitespace),
),
# All other identifiers
(r"[a-zA-Z_][\w']*", Name),
# Number literals
Expand Down