Commit Graph

193 Commits

Author SHA1 Message Date
Iavor Diatchki
c62d921fb3 More docs 2021-04-30 15:43:14 -07:00
Iavor Diatchki
402c0cc256 Mess around with html teams 2021-04-30 15:42:49 -07:00
Iavor Diatchki
7a98ab5b9b Make a table for operator precedences 2021-04-30 12:00:46 -07:00
Iavor Diatchki
29eefbc09d A shpynx temaplte for a reference manual 2021-04-29 16:47:54 -07:00
Rob Dockins
cc8822f736 Update reference implementation and documentation 2021-04-13 10:27:17 -07:00
Rob Dockins
23a0f0f260 Update documentation PDFs 2021-04-06 09:48:41 -07:00
Rob Dockins
eb9d3e900d Update book exercise output 2021-03-02 17:18:36 -08:00
Rob Dockins
6b784b11ec Typo
Fixes #1039
2021-02-17 16:13:04 -08:00
Rob Dockins
0abde1e55e Update option names in documentation 2021-02-11 16:27:04 -08:00
Iavor Diatchki
8796390244 Add name etc. 2021-01-25 08:33:11 -08:00
Iavor Diatchki
c9307065b9 A short talk on the new parameterized moduels design 2021-01-14 15:43:04 -08:00
Rob Dockins
301c74cb8f Docs typos 2021-01-12 17:00:24 -08:00
Rob Dockins
976468dce7 Fix typos 2021-01-12 11:20:57 -08:00
Rob Dockins
600f43b5f0 Update the Programming Cryptol book with documentation about newtypes. 2021-01-12 11:19:53 -08:00
Rob Dockins
557b928caf Update syntax and semantics documents with newtype changes 2021-01-12 11:18:58 -08:00
Ben Selfridge
7489dbd52e
Doc fixes (#1016)
* 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
2021-01-11 14:52:21 -08:00
Ben Selfridge
f45389b8cd Adds "replPrompt" command 2020-12-12 08:47:21 -08:00
Ben Selfridge
5c18b35523 Brings CrashCourse.tex up-to-date with respect to recent changes
Both in this branch and in master (which I'd previously missed).
2020-12-10 17:12:50 -08:00
Ben Selfridge
c78424334e Adds repl annotations for more of CrashCourse.tex 2020-12-09 16:15:17 -08:00
Ben Selfridge
861e9e9651
Feature/docs checking (#976)
* 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.
2020-11-20 16:53:36 -08:00
Aaron Tomb
692c814776
Don't add an extra copy of Programming Cryptol (#970)
Two different Makefiles each copied it and used different file names.

Closes #969.
2020-11-17 09:26:03 -08:00
Brian Huffman
97b967c8bd Update generated pdf. 2020-10-14 10:47:28 -07:00
Brian Huffman
36b8bd2e07 Fix miscellaneous typos in Syntax.md. 2020-10-13 11:09:51 -07:00
Brian Huffman
754c6ac59b Remove errant comma in exercise solution in the book. 2020-10-13 11:08:12 -07:00
Brian Huffman
33d6ae77b7 Fix description of lg2 in exercise answer in the book.
This is one of the errors mentioned in issue #931.
2020-10-13 11:06:52 -07:00
Brian Huffman
a23267fe3d More accurate descriptions for lg2 and width in book appendix.
Fixes #931.
2020-10-13 10:53:32 -07:00
Brian Huffman
e08cac3828 Remove redundant word "Size" in table of built-in type-level operators.
We have decided to avoid the term "size type" in favor of
"numeric type" (#597), and the word is uninformative in this
context anyway.
2020-10-13 10:39:25 -07:00
Rob Dockins
6b9a9f1294 Fix book typos 2020-09-29 21:50:30 -07:00
Rob Dockins
9822d5fd9a Update documentation and reference interpreter 2020-09-29 14:55:05 -07:00
Brian Huffman
41532cc5e0 Update generated ProgrammingCryptol.pdf. 2020-09-23 11:15:59 -07:00
Brian Huffman
c938793107 Replace usage of zipWith (^) with (^) in a book example.
Fixes #803.
2020-09-23 11:15:59 -07:00
Brian Huffman
f6d9f4b0e9 Fix mixed-up solutions to book exercises about any and all.
This fixes an issue mentioned in a comment to #887.
2020-09-23 11:15:59 -07:00
Brian Huffman
6676702f7f Fix wrong inferred type for twoPlusXY in book exercise.
Fixes #887.
2020-09-23 11:15:59 -07:00
Brian Huffman
206cb5ef44 Switch toInteger to fromZ in book example.
Fixes #873.
2020-09-23 11:15:59 -07:00
Brian Huffman
c4299a148b Add missing ']' in book example.
Fixes #880.
2020-09-23 11:15:59 -07:00
Rob Dockins
04bd63380e Edit reference semantics for style and update PDF 2020-09-02 10:26:23 -07:00
Aaron Tomb
5100132e4c
Tweak a few things for 2.9.0 (#833)
* 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
2020-07-28 08:41:27 -07:00
Iavor Diatchki
39acf61ee5 Update documentation with info about floats + fractional literals 2020-07-14 15:36:37 -07:00
Rob Dockins
0d7d98bcfb Add a trivial "parmap" implementation to the reference interpreter. 2020-07-09 10:54:03 -07:00
Brett Boston
0e35995ee4 Document element type constraints for enumerations 2020-07-08 10:13:55 -07:00
weaversa
d4b4d5fe2f
wording fix 2020-07-05 14:54:34 -04:00
Brett Boston
a87684aad4 Clarify that each file can only contain a single module 2020-06-30 19:10:33 -07:00
robdockins
87d5edab00
Documentation updates (#779)
* 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
2020-06-30 10:58:25 -07:00
Brett Boston
f742b1614a Document polynomial syntax + escape pipes in Version2Table 2020-06-26 15:32:47 -07:00
Brett Boston
b136902476 Correct definition of rotate in Section 3.3
Closes #758
2020-06-18 17:44:38 -07:00
Brett Boston
8b6581f263 Fix typo in definition of distributed property of gf28DotProduct
Closes #762
2020-06-18 17:37:17 -07:00
Rob Dockins
c09ee13f27 Update documentation PDFs 2020-06-04 13:39:00 -07:00
Rob Dockins
897f631910 Fix reference semantics of the signed bitvector primitives 2020-05-27 15:34:58 -07:00
Rob Dockins
e2f45ee5e4 Update documentation PDFs 2020-05-27 14:21:46 -07:00
Rob Dockins
542debdb67 Documentation tweaks 2020-05-27 14:21:17 -07:00