Aaron Tomb
58a57d2927
Working Debian-based Docker build script
2019-04-17 12:27:50 -07:00
Aaron Tomb
f1f7ca311c
Update Docker build to use Debian as a base
...
This makes it easier to do Haskell builds and incorporate external
tools, even though it results in a slightly bigger image.
2019-04-16 15:16:24 -07:00
Aaron Tomb
6a268930c8
Parameterize time command for make test
2019-04-16 15:16:13 -07:00
Iavor Diatchki
706e8e2b7f
Arguments after are for cryptol.
2019-03-29 10:26:34 -07:00
Iavor Diatchki
08c537122a
Update nQueens example to not print the found solution.
2019-03-25 16:20:17 -07:00
Iavor Diatchki
f8187eda30
Add an options to disable printing of examples.
...
See #584
2019-03-25 16:14:36 -07:00
Iavor Diatchki
782ab875dc
Order parameters and print type in front of the type ones.
...
We also filter them, although I don't think that's neccessary,
as I am not sure that we have a way to have two parameterized modules
in scope at the same time...
Fixes #586
2019-03-25 15:59:25 -07:00
Iavor Diatchki
83fb997326
Show module parameters when browsing. See #586
2019-03-25 15:34:38 -07:00
Iavor S. Diatchki
d5be2eab0e
Merge pull request #583 from david-christiansen/feature/vectorscmd
...
Command to dump generated tests
2019-03-19 14:37:37 -07:00
David Thrane Christiansen
209686bb60
More friendly handling of errors writing files from :dumptests
2019-03-19 13:36:43 -07:00
David Thrane Christiansen
508327058b
Improve line wrapping of help text for :dumptests
2019-03-19 13:35:38 -07:00
David Thrane Christiansen
39ef53653d
Show summaries of command arguments in :help text
2019-03-19 13:26:38 -07:00
David Thrane Christiansen
98b743c920
Compute size parameter in accord with other test code
...
This fixes a discrepancy between dumped test output and the test runner.
2019-03-19 13:26:01 -07:00
David Thrane Christiansen
8a9565595b
Render each test on a single line
2019-03-19 13:26:01 -07:00
David Thrane Christiansen
e064233acd
Preliminary support for dumping tests
...
Fix misspelling in help text
2019-03-19 13:25:55 -07:00
Brian Huffman
fc6e6be518
Tighten lower interval bounds for /^ operator.
...
The result of `x /^ y` can never be 0 unless `x` is 0.
2019-03-18 18:05:41 -07:00
Brian Huffman
7cb16586d4
Add regression test for #581 .
2019-03-18 15:29:36 -07:00
Brian Huffman
5e8d8d6f80
Implement /^ and %^ for intervals. Fixes #581 .
2019-03-18 15:29:04 -07:00
Brian Huffman
5076273c10
Add regression test for issue #582 .
2019-03-18 14:53:09 -07:00
Brian Huffman
6265cb3b0e
Add well-formedness constraints for uses of /^ and %^. Fixes #582 .
2019-03-18 14:06:04 -07:00
Aaron Tomb
3af02e9599
Make GHC 8.6 Cabal freeze file less strict
...
Now it'll work with 8.6.x
2019-03-11 15:16:12 -07:00
Aaron Tomb
361e052a78
Bump SBV version in Cabal freeze files
2019-03-11 12:21:23 -07:00
Aaron Tomb
be13fedb65
Merge pull request #580 from LeventErkok/master
...
Changes required to compile Cryptol with SBV 8.1; and model-validation support
2019-03-11 12:20:41 -07:00
Aaron Tomb
600b5ec049
Update path for cryptol-specs in .gitmodules
2019-03-11 12:13:08 -07:00
Levent Erkok
375166d06f
Add a prover-validate flag and pass it to SBV (default: off)
...
This should address the issue reported in https://github.com/GaloisInc/cryptol/issues/558
2019-03-09 13:44:20 -08:00
Levent Erkok
f3a26e24b7
Undo changes for elapsed time bug workaround
...
SBV 8.1 prints the time correctly, so this workaround isn't needed
Fixes https://github.com/GaloisInc/cryptol/issues/572
2019-03-09 13:27:35 -08:00
Levent Erkok
cbdf7c696a
Make cryptol compile with SBV 8.1
2019-03-09 13:26:41 -08:00
Brian Huffman
dc48fedcbc
Reimplement symbolic updates more efficiently. Fixes #579 .
2019-03-04 18:07:33 -08:00
Brian Huffman
0db6a86f73
Fix typos in comments.
2019-03-04 18:05:23 -08:00
Aaron Tomb
1548d2ecf4
Remove deleted examples from Makefile
2019-03-04 11:16:50 -08:00
Brian Huffman
9584fdb54d
Remove some duplicate files from /examples that were also in cryptol-specs.
...
See #571 .
2019-03-01 18:34:23 -08:00
Brian Huffman
acafb2952d
Add cryptol-specs as git submodule under /examples.
2019-03-01 18:05:28 -08:00
Iavor Diatchki
a33ddf1ae3
Improvements to edit/reload logic.
...
See #578 for details.
2019-03-01 17:25:43 -08:00
Iavor Diatchki
afe89d2ad4
Add examples of doing record updates
2019-03-01 11:10:28 -08:00
Iavor S. Diatchki
139c7d50ac
Merge pull request #576 from GaloisInc/fingerprints
...
Track file content fingerprints alongside loaded modules
2019-02-28 11:02:27 -08:00
Brian Huffman
6b53cd0c2f
Fix typo in documentation.
2019-02-28 10:46:41 -08:00
brianhuffman
f8aca88d9d
Merge pull request #575 from GaloisInc/wip/no-from-then
...
Remove [x..] syntax.
2019-02-28 10:42:38 -08:00
Brian Huffman
e59c9abfbb
Remove [x..] and [x,y..] syntax from documentation.
2019-02-28 10:38:38 -08:00
Eric Mertens
5e75f834e7
Update test for new utf-8 error message
2019-02-28 10:04:17 -08:00
Eric Mertens
5786fcf190
Track file content fingerprints alongside loaded modules
2019-02-28 09:40:21 -08:00
Brian Huffman
7ea4884fdd
Remove unused primitive type operator lengthFromThen.
2019-02-27 17:11:18 -08:00
Brian Huffman
24fb6c9511
Remove unused primitive fromThen.
2019-02-27 16:57:00 -08:00
Brian Huffman
61a17adb02
Remove [x..] and [x,y..] syntax from Cryptol.
2019-02-27 16:36:53 -08:00
Brian Huffman
c387dbe5fd
Remove all uses of [x..] syntax from examples and tests.
2019-02-27 16:25:53 -08:00
Aaron Tomb
00b58277bb
Update AppVeyor configuration
2019-02-25 16:06:01 -08:00
Aaron Tomb
8ed4dad321
Update Travis for GHC 8.6
2019-02-22 17:06:36 -08:00
Iavor Diatchki
6a8c6c3134
Update Syntax.md and re-sync it with Syntax.tex
...
Note that Syntax.tex should be generated automatically
2019-02-18 17:20:01 -08:00
Iavor Diatchki
1b780c21e1
Merge branch 'master' into rec-upd
2019-02-17 18:51:20 -08:00
Iavor Diatchki
9ad5568332
Fixup function notation in records
2019-02-17 18:45:50 -08:00
Iavor Diatchki
cf7d97fcaf
Reference implementation of updates.
2019-02-17 18:01:27 -08:00
