Commit Graph

34 Commits

Author SHA1 Message Date
Adam C. Foltzer
58a605e8ff update examples and documentation 2016-01-19 18:19:35 -08:00
Adam C. Foltzer
4d3fc9a413 Update copyright dates and add missing headers 2016-01-19 18:19:35 -08:00
Adam C. Foltzer
07da2018b7 switch to more portable seeding for random
The `random` primitive previously took a `[32]` seed, but this causes
inconsistency between 32-bit and 64-bit platforms when the seed is large
enough to wrap around in GHC's representation of an `Int`. This patch
switches to an API that seeds directly with four 64-bit words, and so
should behave the same way on our supported platforms.
2016-01-19 18:17:34 -08:00
Adam C. Foltzer
9c07fe1006 merge in the 2.2.6 changes, including z3 switch 2015-12-23 16:10:56 -08:00
Adam C. Foltzer
3ae0dda7ac switch to Z3 for typechecking and proving
Note: the hardcoding in this patch is only for the 2.2 hotfix branch; in
the 2.3 branch we will only have to change the default setting for the
typechecker.
2015-12-23 14:59:10 -08:00
Adam C. Foltzer
4c441898d9 remove a merge error from docs Makefile 2015-10-05 15:33:04 -07:00
Adam C. Foltzer
baddfcaab8 Merge branch 'heads/hotfixes/v2.2.5' 2015-10-01 10:56:30 -07:00
Adam C. Foltzer
7d81568555 remove iteSolver option for compat with sbv 5+ 2015-09-30 14:24:21 -07:00
Jenkins Builder
75539f9244 add \protect to fix error on Windows docs 2015-09-16 13:12:37 -07:00
Adam C. Foltzer
2ca0e6f732 switch back to non-latexmk for book (Windows)
Windows didn't like the latexmk solution from
5eb5f00d0a.
2015-09-16 11:37:00 -07:00
Adam C. Foltzer
5eb5f00d0a change how the book is built 2015-09-15 13:38:06 -07:00
Dylan McNamee
c27c91af3a fixed negative stepped sequence example (issue #234) in ProgrammingCryptol 2015-06-05 12:02:16 -07:00
Dylan McNamee
aa1565bac4 documentation fixes (tuples, spelling, other wibble) 2015-05-05 08:38:43 -07:00
Adam C. Foltzer
0536d0f15a update copyright years 2015-03-24 11:19:52 -07:00
Adam C. Foltzer
7d650526cd Update book pdf with changes from a15fb75 2015-01-21 15:49:25 -08:00
Adam C. Foltzer
a15fb75856 update book with allSat 2015-01-18 17:03:43 -08:00
Adam C. Foltzer
284338c938 Add the mono-binds flag
When `:set mono-binds=on`, any local definitions lacking type
signatures will not be generalized (i.e., will be monomorphic). This
reduces what is in most cases unnecessary polymorphism that can give
rise to constraints that are difficult to solve. This also improves
the performance of the Cryptol interpreter by lifting many polymorphic
type applications out of the inner loops that are commonly defined as
bindings in `where` clauses.

The flag is on by default in the Cryptol REPL, and in most cases makes
it possible to leave out more type signatures in `where` clauses than
before. However, some programs really do rely on inferring polymorphic
types for local variables; in this case adding an explicit polymorphic
type signature to the local binding in question will make the program
typecheck.
2014-12-15 17:48:25 -08:00
Dylan McNamee
fb93e5f4b3 fixes for tickets 22, 20, 107, 102, in preparation for merging 26 2014-09-23 13:32:09 -07:00
Dylan McNamee
9319e0c19c tweaking notice, adding regression test for GitHub issue #110 2014-09-19 13:09:44 -07:00
Rob Dickerson
8250adfdbe Changing some split examples in crash course to use splitBy instead. 2014-09-18 02:59:11 -05:00
Dylan McNamee
0e29d1d369 issue 108 from Sean, and a minor tweak to the AES chapter's formatting. 2014-09-17 12:28:30 -07:00
Dylan McNamee
75852a2596 Merge branch 'master' of https://github.com/GaloisInc/cryptol 2014-09-10 14:27:26 -07:00
Dylan McNamee
81adb95a37 tweaks to documentation and Salsa20 fix from Sean 2014-09-10 14:27:08 -07:00
Adam C. Foltzer
86b2a80db4 Add basic support for :exhaust
Fixes #94. We should look into the :exhaust optimization later if necessary
2014-09-10 11:16:07 -04:00
Adam C. Foltzer
15e6fec34d update documentation for #82 2014-09-09 11:59:39 -04:00
Dylan McNamee
3ebc8bffcd Incorporating Sean Weaver's fixes to programming cryptol - ticket #80 2014-09-02 10:26:35 -07:00
Dylan McNamee
87042d4604 fixing lone bad reference in doc, added syntax chapter, replaced Salsa spec
PDF with pointer to it, fixed table in section 1.2.2
2014-04-30 11:37:15 -07:00
Adam C. Foltzer
8c97b35bb2 updated docs 2014-04-24 10:55:52 -07:00
Dylan McNamee
8fbb351063 final tweaks to the book 2014-04-24 10:53:00 -07:00
Adam C. Foltzer
4a2da5686a temporarily check docs into the repo
Getting the right TeX Live and pandoc environments on the build slaves
is turning out to be a Big Headache. For now, build docs locally and
keep the repo copies up to date.
2014-04-23 19:16:57 -07:00
Adam C. Foltzer
72cd17c11b change name of book pdf 2014-04-23 18:52:26 -07:00
Dylan McNamee
288178dea2 markdown -> .md, Acks section, adding spec to contrib 2014-04-23 13:15:18 -07:00
Adam C. Foltzer
e937d172d3 !=== is now !== (!!!) 2014-04-18 14:57:40 -07:00
Adam C. Foltzer
ba0a0e8576 Initial import from internal repo 2014-04-17 15:34:25 -07:00