cryptol/docs
2022-02-23 14:39:20 -08:00
..
ParameterizedModules Add name etc. 2021-01-25 08:33:11 -08:00
ProgrammingCryptol Fix documentation 2022-02-23 14:39:20 -08:00
RefMan Fix typo 2021-10-18 11:47:16 -07:00
.gitignore Initial import from internal repo 2014-04-17 15:34:25 -07:00
.nojekyll Disable jekyll, as it ignores files starting with _ 2021-10-18 09:47:08 -07:00
AbstractValuesAndModuleParameters.md Rename primitive demote to the more self-explanatory name number. 2018-07-27 13:52:57 -07:00
chop.hs Remove obsolete cvs-era $Header$ keywords. 2018-03-22 13:33:12 -07:00
CryptolPrims.md Update documenetation with new enumeration forms, 2021-07-20 17:01:50 -07:00
CryptolPrims.pdf Update documenetation with new enumeration forms, 2021-07-20 17:01:50 -07:00
FindExercises.hs Feature/docs checking (#976) 2020-11-20 16:53:36 -08:00
index.html Fix the URL 2021-10-18 09:49:38 -07:00
Makefile Document polynomial syntax + escape pipes in Version2Table 2020-06-26 15:32:47 -07:00
ProgrammingCryptol.pdf Update documentation 2021-08-06 15:04:38 -07:00
README.md Doc fixes (#1016) 2021-01-11 14:52:21 -08:00
Semantics.pdf Update documentation 2021-08-06 15:04:38 -07:00
Syntax.md Update documenetation with new enumeration forms, 2021-07-20 17:01:50 -07:00
Syntax.pdf Update documenetation with new enumeration forms, 2021-07-20 17:01:50 -07:00
Version2Changes.md Merge branch 'master' of github.com:GaloisInc/cryptol 2016-01-03 23:46:52 -08:00
Version2Changes.pdf Doc fixes (#1016) 2021-01-11 14:52:21 -08:00
Version2Table.md Document polynomial syntax + escape pipes in Version2Table 2020-06-26 15:32:47 -07:00
Version2Table.pdf documentation fixes (tuples, spelling, other wibble) 2015-05-05 08:38:43 -07:00

Programming Cryptol README

To use the check-exercises tool, invoke via cabal v2-exec check-exercises --. This requires the path to the LaTeX file to be checked, and has options to specify paths to the cryptol executable and log directories.

To annotate LaTeX files for the check-exercises program, we use the following commands:

  • \begin{replinVerb} and \end{replinVerb}

    This is the markup equivalent of the Verbatim environment. However, it has the added effect of adding every line of the block to a list of commands to be issued to the cryptol REPL.

  • \replin|...|

    Inline equivalent of replinVerb environment. Markup equivalent of \Verb|...|.

  • \hidereplin|..|

    Like \replin|...|, but is not rendered at all by LaTeX. This is for issuing "hidden" input to the REPL that will affect the output (like :set base=10, for example), but which we don't want to include in the PDF.

  • begin{reploutVerb} and \end{reploutVerb}

    This is the markup equivalent of the Verbatim environment. However, it has the added effect of adding every line of the block to the expected output of the preceding \replin commands.

  • \replout|...|`

    Inline equivalent of reploutVerb environment. Markup equivalent of \Verb|...|.

  • \begin{replPrompt} and \end{replPrompt}

    This is the markup equivalent of the Verbatim environment. However, it has the added effect of adding every line of the block either to input or expected output. If the line starts with the Cryptol prompt, it is added to input; otherwise, it is added to output.

  • \hidereplout|..|

    Like \replout|...|, but is not rendered at all by LaTeX. This is for recording "hidden" output from the REPL that we don't want to include in the PDF.

  • \restartrepl

    This has the effect of terminating the current input/output REPL pair. If there is input but no output, then instead of checking the output, the tool checks that the input does not raise an error.

    This command is used to divide the REPL input/output pairs into distinct "blocks" that get submitted to the REPL independently. Therefore, this command should be called every time we are defining a new REPL pair; in particular, it should come before every exercise that uses REPL commands.

Other notes:

  • I tried to do reasonable things with % comments, but I can't guarantee it will work as expected in all cases (particularly with the inline commands). It's probably best to avoid using LaTeX comments that are on the same line as any of the above commands.

  • Lines starting with "Loading module" are silently ignored from the output.

  • It would be nice to support writing code to a file, then loading that file into the REPL. We don't support this, but it will probably be necessary for handling some of the more involved examples (for instance, those that define functions).