Aaron Tomb
5f769af694
Install unzip in cryptol-remote-api/Dockerfile
2021-09-29 08:13:42 -07:00
Aaron Tomb
c8c122fac6
Migrate Docker images to use what4-solvers builds
2021-09-28 16:23:16 -07:00
Iavor S. Diatchki
66e054fed3
Merge pull request #1293 from GaloisInc/T1291
...
Add rewrite rules to simplify constraints due to `generate`.
2021-09-27 14:35:28 -07:00
Iavor Diatchki
e86a94763d
Add rewrite rules to simplify constraints due to generate.
...
max 1 (a ^ n) ~> a ^ n (for a >= 1)
width (2 ^ n - 1) ~> n
Fixes #1291
2021-09-27 11:15:43 -07:00
Aaron Tomb
15b3b98482
Merge pull request #1286 from GaloisInc/at-windows-tests
...
Re-enable tests on Windows
2021-09-27 08:47:36 -07:00
Aaron Tomb
d6f3497392
Allow \ line continuation at REPL on Windows
2021-09-22 15:17:25 -07:00
Aaron Tomb
6d2709748e
Revert "Remove use of \ line continuations in tests"
...
This reverts commit 2dc5e03567
2021-09-22 15:17:13 -07:00
Matthew Yacavone
553a78e43f
Merge pull request #1285 from GaloisInc/rpc/single-conn-interface
...
[RPC] Single-connection interface
2021-09-22 16:47:12 -04:00
Matthew Yacavone
74a4c046a8
fix typo in changelog
2021-09-22 15:49:38 -04:00
Matthew Yacavone
f57435e04f
update changelog, bump version number
2021-09-22 14:41:12 -04:00
Matthew Yacavone
8351903206
add get_default_timeout/set_default_timeout, update docstrings
2021-09-22 14:30:00 -04:00
Matthew Yacavone
f5419700b4
update synchronous and single-connection interfaces
2021-09-22 13:57:19 -04:00
Aaron Tomb
2dc5e03567
Remove use of \ line continuations in tests
...
These trigger the problem described in issue #1290 . We should fix it,
but, in the meantime, it's nice to be able to use the portions of this
test that work. Testing the use of `\` continuations isn't the main
purpose of this test.
2021-09-22 10:40:10 -07:00
Matthew Yacavone
228e45f6a0
Merge branch 'master' into rpc/single-conn-interface
2021-09-22 13:32:44 -04:00
Andrew Kent
e256346f83
feat: timeout for cryptol python client methods ( #1282 )
...
interrupt and timeout methods for cryptol python client
2021-09-21 20:23:28 -07:00
Andrew Kent
fe5aa6642a
Update test_error_recovery.py ( #1288 )
...
disable certificate verification since test suite uses
self signed certs
2021-09-21 12:47:37 -07:00
Kevin Quick
8bd61befaa
Merge pull request #1287 from GaloisInc/doc_ci
...
Add some functionality comments to ci.sh
2021-09-20 09:41:38 -07:00
Kevin Quick
1e71818767
Add some functionality comments to ci.sh
2021-09-20 08:56:11 -07:00
Aaron Tomb
0216c7e6ec
Revert changes to solvers used in regression tests
2021-09-17 16:23:46 -07:00
Aaron Tomb
39b562d1af
Use cvc4 instead of w4-cvc4 in some tests
...
This is an experiment to see whether it works better on Windows.
2021-09-17 16:23:46 -07:00
Aaron Tomb
67bdb1c538
Improve speed of negshift test
...
Uses Yices instead of Z3
2021-09-17 16:23:46 -07:00
Aaron Tomb
e19f5083e0
Fix expected output for modsys/T16 on Windows
2021-09-17 16:23:46 -07:00
Aaron Tomb
4bd711bca1
Re-enable tests on Windows
...
Still leaves out RPC tests. We don't expect them to work on Windows
anytime soon.
2021-09-17 16:23:46 -07:00
Aaron Tomb
30af0baf55
Merge pull request #1284 from GaloisInc/at-prebuilt-solvers
...
Use prebuilt solver binaries from what4-solvers
2021-09-17 15:47:35 -07:00
Aaron Tomb
1bb2b540e9
Bump solver package snapshot version
2021-09-17 14:53:05 -07:00
Matthew Yacavone
196bda327c
Merge branch 'master' into rpc/single-conn-interface
2021-09-17 15:25:00 -04:00
Matthew Yacavone
ee8cbace8f
Merge pull request #1272 from GaloisInc/rpc/synchronous-interface
...
[RPC] Synchronous, typed interface for Python client
2021-09-17 15:22:23 -04:00
Aaron Tomb
6cd4383086
Fix solver dependency analysis
2021-09-17 12:05:29 -07:00
Aaron Tomb
b88544152c
Check dynamic library dependencies of solvers
2021-09-17 11:21:33 -07:00
Aaron Tomb
94a32f9a04
Disable RPC tests on macOS
...
They’re stalling for unknown reasons, and aren’t as critical as the
others. Running the Linux tests is the most critical.
2021-09-17 11:20:34 -07:00
Aaron Tomb
45c28c397d
Switch back to GHC 8.10.2 for now
...
We're using GHC 8.6.5 for tests
2021-09-15 16:14:24 -07:00
Aaron Tomb
5e31bd0575
Attempt to fix build stall on Windows
2021-09-15 16:07:37 -07:00
Matthew Yacavone
8031ffb7dd
improve docstrings around truthiness
2021-09-15 16:52:23 -04:00
Aaron Tomb
c537017abe
Include abc in with-solvers tarballs
2021-09-15 13:11:30 -07:00
Aaron Tomb
bdb2c96817
Make solver package version configurable
2021-09-15 13:11:30 -07:00
Aaron Tomb
88d24a17a2
Always overwrite solvers when unzipping
2021-09-15 13:11:30 -07:00
Aaron Tomb
aa3426e316
Fix Yices executable name
2021-09-15 13:11:30 -07:00
Aaron Tomb
5fbb1752e6
Fix typo in solver binary archive names
2021-09-15 13:11:30 -07:00
Aaron Tomb
c8bfa205e8
Use prebuilt solver binaries from what4-solvers
2021-09-15 13:11:30 -07:00
brianhuffman
cb240cdd31
Merge pull request #1281 from GaloisInc/toSignedInteger
...
Add `toSignedInteger` primitive.
2021-09-14 16:41:49 -07:00
Matthew Yacavone
80e7b1fc94
fix whitespace
2021-09-14 16:08:41 -04:00
Matthew Yacavone
a9e1119eef
add single-connection interface, update tests to use this interface
2021-09-14 16:03:09 -04:00
Matthew Yacavone
1187040463
Merge branch 'master' into rpc/synchronous-interface
2021-09-14 15:09:40 -04:00
Matthew Yacavone
ac6b2d177a
tweak typing
2021-09-14 14:43:07 -04:00
Matthew Yacavone
0cafab8c6d
get test_cryptol_api.py working again
2021-09-13 19:28:15 -04:00
Matthew Yacavone
fcccea6b49
change connect_sync to sync.connect
2021-09-13 18:56:46 -04:00
Matthew Yacavone
9ebb6d4db4
remove Solver offline method, fix mypy for test_smt.py
2021-09-13 18:33:59 -04:00
Matthew Yacavone
2ef2a35118
ensure __bool__ method of OfflineSmtQuery raises an exception
2021-09-13 18:11:50 -04:00
Matthew Yacavone
64bbbd7886
make sync SMT interface mirror cryptol REPL, revert async SMT interface
2021-09-13 17:51:07 -04:00
Brian Huffman
869deb1354
Update expected test output.
...
Some error messages changed due to the new definition in Cryptol.cry.
2021-09-10 20:08:43 -07:00
