Robert Dockins
b564b21b31
Typo in error message
2017-07-31 10:04:52 -07:00
Robert Dockins
0b9c186132
Make 'random' compute on concrete inputs in the symbolic evaluator.
...
This patch does not add a warning when using 'random' in symbolic expressions.
We currently don't have any organized mechanism for generating warnings during
evaluation, and the value of emitting such a warning is debatable.
Fixes #364
2017-07-27 15:45:37 -07:00
Aaron Tomb
520ff9183a
Build on Travis with GHC 8.2.1
...
Builds with 8.0.2 were timing out, and maybe this will help.
2017-07-27 12:08:05 -07:00
Robert Dockins
2fb706a44c
Make sure EvalErrors are propigated to the REPL error handler.
...
This keeps runtime evaluation errors from killing the Cryptol process.
2017-07-26 18:05:30 -07:00
Robert Dockins
dba3d2f7d8
Avoid using partial indexing operations.
...
Instead raise evaluation errors when indexing into finite sequences
with invalid indices.
2017-07-26 18:04:38 -07:00
Robert Dockins
36dcd49803
Update the test suite now that issue #116 is fixed.
2017-07-26 15:31:36 -07:00
Robert Dockins
399a2e47d5
Add additional thunking in logical and arithemetic primitive operations.
...
This prevents a loss of desirable sharing in the interpreter, and turns
recursive algorithms with potential sharing from exponential-time to linear
time. It appears to have little impact on other algorithms.
Fixes #432
2017-07-26 15:30:36 -07:00
Aaron Tomb
901a1d16ad
Remove references to cryptol-server from README
2017-07-24 16:22:00 -07:00
Aaron Tomb
010540c4b4
Comment out cryptol-server from Cabal file
2017-07-24 15:26:49 -07:00
Aaron Tomb
69e49d4245
Bump version to 2.5.0
2017-07-24 09:16:40 -07:00
Aaron Tomb
de80a9c2f5
Update copyright dates in Cabal file
2017-07-24 09:01:34 -07:00
Aaron Tomb
2fd6599e0b
Adopt LeventErkok's suggestion from #435
...
Closes #435 .
2017-07-21 12:58:05 -07:00
Aaron Tomb
2885d469da
Disabe the utf-8-ident test in a different way
...
If you use a `.fails` file, then the test suite fails if that test
succeeds, which it does on most platforms.
2017-07-21 12:25:44 -07:00
Aaron Tomb
bfe457f9ab
Note that the test parser.utf-8-ident fails
...
This fails on Windows and we don't really know how to fix it. The fact
that it always fails masks more interesting failures, so I think it's
better to just skip it for now.
2017-07-21 11:04:06 -07:00
Aaron Tomb
33b064b88c
Fix benchmarks for SBV 7.0
2017-07-21 08:42:49 -07:00
Aaron Tomb
10240a62d6
Add note about Z3 version to README
2017-07-21 08:42:38 -07:00
Aaron Tomb
da04f374f4
Add Travis badge to README
2017-07-21 08:34:30 -07:00
Aaron Tomb
8aa497206c
Re-enable prover identification in stats
2017-07-20 10:38:38 -07:00
Aaron Tomb
a04f236169
Update test output for SBV 7.0
...
With SBV 7.0, we get back satisfying assignments in a different order.
We should probably adjust this test to be less fragile eventually.
2017-07-20 09:33:56 -07:00
Aaron Tomb
d873664df4
Merge pull request #434 from LeventErkok/master
...
Modifications to make cryptol compile with SBV 7.0
2017-07-20 09:04:24 -07:00
Levent Erkok
5857477ab2
Modifications to make cryptol compile with SBV 7.0
...
Also, bumped up the version to 2.4.1
2017-07-18 10:25:00 -07:00
Aaron Tomb
25e2ba01c6
Disable tests on AppVeyor for now
...
More of the Makefile needs to be updated before tests will run
correctly.
2017-07-12 10:49:59 -07:00
Aaron Tomb
ec0b506230
Follow redirects when fetching Z3
2017-07-12 10:14:12 -07:00
Aaron Tomb
14ac49279a
Run tests under AppVeyor
2017-07-12 09:54:20 -07:00
Iavor Diatchki
4a43c675d9
When checking a binding, treat schema validation constraints
...
just like any other constraint from the definition.
In particular, if the schema validity depends on an outer context,
the constraints should be solve in that outer context, not here.
Fixes #314
2017-07-10 17:35:49 -07:00
Iavor Diatchki
c836d8e356
Improve error message.
...
Fixes #383
2017-07-10 17:11:55 -07:00
Iavor Diatchki
e5fa174cbb
Add some axioms about width.
...
Fixes #387
2017-07-10 16:59:03 -07:00
Iavor Diatchki
b5d6715b21
Add support for comments; panic on completely bogus inputs.
...
Note that we still do not check for errors in commands, perhaps we should?
2017-07-10 16:58:33 -07:00
Iavor Diatchki
affcc25156
Don't crash when we detect and error, tell the user instead!
...
Also, improve the printing of the errors a bit.
2017-07-10 11:59:39 -07:00
Iavor Diatchki
771c2deaa1
Slightly different error messages, should be OK.
2017-07-10 11:06:14 -07:00
Iavor Diatchki
1e4fb89f4c
Fix test, due to changes in the Prelude.
2017-07-10 11:05:59 -07:00
Iavor Diatchki
0f825daf2f
Bug fix: remember to pop-off the solver's context.
2017-07-10 11:05:47 -07:00
Iavor Diatchki
5a885e9f5a
Check for consistency before improving.
...
We may want to do this more often, but it may have a performance penalty.
Anyway, we need this check here, because previously the code was assuming
that the goals are known to be consistent, and we are just wanting to
default them, which should never make them inconsistent, just more instantiated.
The current solution is a bit of a stop-gap, until we redo the defaulting
story, and separate it form improvement.
2017-07-10 10:59:40 -07:00
Iavor Diatchki
89f0af891a
Report inconsistent constraints together.
2017-07-10 10:56:56 -07:00
Iavor Diatchki
ae3e0ea106
Add some functionality for simple checking of the consistency of goals.
2017-07-10 10:55:49 -07:00
Iavor Diatchki
04fbc4c1c2
Notice the fin inf is impossible.
2017-07-10 09:41:15 -07:00
Aaron Tomb
2d6dac4a23
Another Travis typo...
2017-07-07 15:28:52 -07:00
Aaron Tomb
ac214563f2
Put Z3 in $HOME/bin on Travis/Linux
2017-07-07 15:25:20 -07:00
Aaron Tomb
80faaa4819
Fix typo in Travis config
2017-07-07 15:11:25 -07:00
Aaron Tomb
aeeb938e18
Update Travis config to install Z3
2017-07-07 15:09:40 -07:00
Andrey Chudnov
6bdce04727
Extend built-in library caching to Cryptol::Extras
2017-07-07 14:25:22 -07:00
Aaron Tomb
48c4d764e1
Use built-in diff on Travis
2017-07-05 16:25:58 -07:00
Aaron Tomb
aa0d5179b8
Specify the diff program to use on Travis
2017-07-05 11:51:41 -07:00
Aaron Tomb
b6a0e7e3f6
Fix typo in Travis OS X script
2017-07-05 11:51:07 -07:00
Aaron Tomb
72592041f0
Back to make for AppVeyor
2017-07-05 11:26:30 -07:00
Aaron Tomb
28f037b17b
Use install instead of build for AppVeyor
2017-07-05 11:16:52 -07:00
Aaron Tomb
84e0687df6
Fix typo in Travis config
2017-07-05 11:14:38 -07:00
Aaron Tomb
16e3ed809c
Use cabal build instead of make for AppVeyor
2017-07-05 11:01:52 -07:00
Aaron Tomb
4a2f2f50e9
Add AppVeyor configuration
2017-07-05 10:57:46 -07:00
Aaron Tomb
e8a8b5292b
Add OS X configuration for Travis
2017-07-05 10:27:08 -07:00
