mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-10-26 22:29:08 +03:00
861e9e9651
* 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. |
||
---|---|---|
.. | ||
aes | ||
appendices | ||
basic | ||
bib | ||
classic | ||
conclusion | ||
cover | ||
crashCourse | ||
des | ||
enigma | ||
highAssurance | ||
main | ||
misc | ||
preface | ||
prims | ||
sha | ||
technicalities | ||
title | ||
tools | ||
utils | ||
.gitignore | ||
Makefile |