* Update all commands to track their results
* Implement REPL :check-docstrings command
This command checks that all of the unlabeled and "repl" labeled
codeblocks in docstrings can successfully evaluate as REPL commands.
Cryptol will now indicate exit failure if any of REPL commands fail,
making it possible to use in automated testing.
:check-docstrings internal implementation is set up to track results
of subcommands in support for integration into a remote server API
endpoint.
* Implement :focus
* Add some :check-docstring test cases
* Update changelog
* Update CrashCourse.tex now that more commands are checked
* Require repl and convert \r\n to \n in lexer
- p-1 bits in an IEEE float refers to the significand, not the
mantissa, at least according to the latest preferred terminology,
which aims to keep the word "mantissa" for the full mantissa
including the units bit;
- reciprocal rather than reciprocol;
- the example in 1.23 had the wrong module declarations; also insert a
separator word between the verbatim blocks so they can be told
apart.
* 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
