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.

Sign up for GitHub

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

Fix the dead links in the tutorials #2170

Merged
merged 5 commits into from
Dec 20, 2024
Merged

Fix the dead links in the tutorials #2170

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
c7536c8
tutorial: Use the preferred musl domain name.
ChrisEPhifer Dec 20, 2024
a68daa1
tutorial: Replace SAT competition format link.
ChrisEPhifer Dec 20, 2024
94ac55c
rust-tutorial: Update link to Rust static items documentation.
ChrisEPhifer Dec 20, 2024
02a3853
rust-tutorial: Fix the Cryptol Salsa20 spec link.
ChrisEPhifer Dec 20, 2024
d84d0ab
sawScriptTutorial: Add the updated tutorial PDF.
ChrisEPhifer Dec 20, 2024
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
4 changes: 2 additions & 2 deletions doc/rust-tutorial/rust-tutorial.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1685,7 +1685,7 @@ so use it with caution.
## Static items

Sometimes, Rust code makes use of [_static
items_](https://doc.rust-lang.org/std/intrinsics/fn.ctpop.html), which are
items_](https://doc.rust-lang.org/reference/items/static-items.html), which are
definitions that are defined in a precise memory location for the entire
duration of the program. As such, static items can be thought of as a form of
global variables.
Expand Down Expand Up @@ -1974,7 +1974,7 @@ transcribing an English-language specification to executable Cryptol code is
interesting in its own right, but it is not the primary focus of this tutorial.
As such, we will save you some time by providing a pre-baked Cryptol
implementation of the Salsa20 spec
[here](https://github.com/GaloisInc/saw-script/tree/master/doc/rust-tutorial/code/salsa20/src/Salsa20.cry).
[here](https://github.com/GaloisInc/saw-script/blob/master/doc/rust-tutorial/code/salsa20/Salsa20.cry).
(This implementation is
[adapted](https://github.com/GaloisInc/cryptol-specs/blob/1366ccf71db9dca58b16ff04ca7d960a4fe20e34/Primitive/Symmetric/Cipher/Stream/Salsa20.cry)
from the [`cryptol-specs`](https://github.com/GaloisInc/cryptol-specs) repo.)
Expand Down
4 changes: 2 additions & 2 deletions doc/tutorial/tutorial.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ $include 19-26 code/ffs.c

Another optimized version, in the following rather mysterious program
(also in `ffs.c`), based on the `ffs` implementation in [musl
libc](http://www.musl-libc.org/).
libc](http://musl.libc.org/).

``` {.c}
$include 69-76 code/ffs.c
Expand Down Expand Up @@ -307,7 +307,7 @@ In addition to the `abc`, `z3`, and `yices` proof tactics used
above, SAWScript can also invoke arbitrary external SAT solvers
that read CNF files and produce results according to the SAT
competition
[input and output conventions](http://www.satcompetition.org/2009/format-solvers2009.html),
[input and output conventions](https://jix.github.io/varisat/manual/0.2.0/formats/dimacs.html),
using the `external_cnf_solver` tactic. For example, you can use
[PicoSAT](http://fmv.jku.at/picosat/) to prove the theorem `thm` from
the last example, with the following commands:
Expand Down
Loading