* Updates all the examples in CrashCourse.tex up to the functions section
This adds more REPL annotations for the exercise checker in the Programming
Cryptol book. There is still more work needed to support many of the examples in
the functions section (and presumably the rest of the book as well), so I think
this is a logical stopping point for now until we add a feature that lets you
write out a file and load it into the repl.
* Updates ProgrammingCryptol.pdf wrt recent changes
* Adds a stub executable to cabal file for checking docs
* [WIP] Adds check-exercises executable
A program that checks that the exercises in Programming Cryptol actual work when
executed against an Cryptol REPL. Instead of using \begin{Verbatim}, we use
\begin{REPL} in both the exercise and the answer, which is rendered the same but
gets checked by this program.
This is a WIP -- we still need to do a number of things, including (but not
limited to):
* Move the "REPL" macro out of CrashCourse.tex and into some including latex
file
* Change many of the "Verbatim"s into "REPL"s to test if this approach works in
general
* Several updates
* Moves REPL command definitions into main latex file
* Generalizes repl commands
* Several improvements:
* documentation of CheckExercises.hs
* factoring out addReplData, addReplin, addReplout, nextLine functions
* took the IO out of P monad (shouldn't have been there)
* worked on annotating repls for many exercises/examples in crash course
* Adds a README for check-exercises
* Uses cryptol's -e option to detect errors
* updates ProgrammingCryptol.pdf
* Fixes main function
After changing to use the -e option to detect errors, I used cabal v2-exec which
apparently does not rebuild anything, but I thought it did. This just fixes the
code so it builds again.
* Fix Dockerfile
* Include version number in CHANGES.md
* Update copyright dates
* Don't include cryptol-specs in release archives
* Remove duplicate copy of Programming Cryptol
* Add docstrings for all prelude functions and fix minor style issues.
Fixes#771
* Update `CryptolPrims` documentation
* Minor updates to the prelude
* Update CHANGES
* Updates to the cryptol book and CryptolPrims
* Fix several additional docstrings
* Specify and document properties of signed bitvector division.
Fixes#677
* Fixup test
* typos and style
* Regenerate PDFs
The `random` primitive previously took a `[32]` seed, but this causes
inconsistency between 32-bit and 64-bit platforms when the seed is large
enough to wrap around in GHC's representation of an `Int`. This patch
switches to an API that seeds directly with four 64-bit words, and so
should behave the same way on our supported platforms.
