search

GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.14k stars 123 forks source link

Add tests to ensure code examples in Programming Cryptol book don't break #613

Open brianhuffman opened 5 years ago

brianhuffman commented 5 years ago

The Programming Cryptol book contains lots of code snippets and example REPL output. We'd like for this material to stay up-to-date with newer revisions of Cryptol. But it would also be nice not to have to check all of it manually.

We should implement a test script that compiles and runs all of the example Cryptol code and REPL commands in the LaTeX documentation to make sure they continues to parse, type-check, and produce the expected output.

robdockins commented 4 years ago

@brianhuffman, do you have in mind a good way to achieve this? Is this something you've done before?

brianhuffman commented 4 years ago

No, I've never implemented anything like this before.

For parsing and type checking, I suppose we could just have the test suite load some of the .tex files as literate cryptol.

To keep example REPL output up to date, we might need to make a custom script or tool to help do that. One approach might be to use a special latex command for REPL commands, and another special latex command for REPL output. A tool could then collect the contents of all of these latex commands in the book, and generate an .icry file and an .icry.stdout file that could be run just like any other regression test. (I'm no TeX expert, but perhaps there's even a way to make TeX produce such files automatically as a side-effect of typesetting the book?)

robdockins commented 4 years ago

After chatting with various folks about ways to achieve this, I'm not sure this is reasonable to fit into the 2.9 timeframe. It's going to involve some tedious TeX and/or Makefile kinds of hacking. What do you think @atomb?

atomb commented 4 years ago

Yeah, you're probably right. I know that when I've tried to do similar things in the past it's been somewhat complex. Let's bump it.

weaversa commented 4 years ago

@WeeknightMVP has been exploring this same issue for our Cryptol course and has a nice set of scripts for pulling Cryptol and shell sessions from markdown.

robdockins commented 3 years ago

This is pretty much done now, and has been for some time. Only the "Crash Course" chapter has really been hooked up, though.