Commit Graph

3245 Commits

Author SHA1 Message Date
Rob Dockins
6f9d9e72a6 Report the number of models found, if a multisat query returns more
than one model.
2021-07-19 19:39:04 -07:00
robdockins
20b8b820bb
Merge pull request #1227 from GaloisInc/explicit-stride
Explicit stride
2021-07-19 18:58:38 -07:00
Rob Dockins
af4d0d98a8 Merge remote-tracking branch 'origin/master' into explicit-stride 2021-07-14 13:34:17 -07:00
Aaron Tomb
02aa44114e
Fix allowed test failure on Windows (#1232)
This disables RPC tests on Windows. They seem to hang instead of failing at the moment, so until we get them
working it seems like it's better to just leave them out.
2021-07-09 11:04:06 -07:00
Andrew Kent
ddde44c90c
feat: portable rpc server builds use fork/threading less (#1231)
Now the `NotThreaded` cabal flag can be used to
omit the `-threaded` flag when building the rpc
servers, which reduces the number of `fork`
invocations when running the servers.
2021-07-08 14:10:07 -07:00
Aaron Tomb
c1a2bfb5c1
Attempt to fix CVC4 and Docker upload issues (#1230)
We will need a better solution to getting CVC4 eventually, but unbreaking the builds, even temporarily, is high priority. And the right solution for CVC4, with the recent transition to CVC5, is somewhat tricky.
2021-07-08 13:10:31 -07:00
Andrew Kent
571f0dd249
feat: support for all solver backends for cryptol server/client (#1224)
* feat: support for all solver backends for cryptol server/client
* chore: update server docs w.r.t. sat related functionality
* chore: reduce trailing whitespace
* chore: deduplicate usage of helper
* chore: misc build fixes
* chore: type annotation fixes
2021-07-02 07:27:40 -07:00
Rob Dockins
4d5d66ff27 update docs again 2021-06-30 16:51:54 -07:00
Rob Dockins
a3534f99b7 Update tests again 2021-06-30 16:34:17 -07:00
Rob Dockins
362649bb74 Documentation tweaks and spellcheck in the prelude 2021-06-30 16:23:15 -07:00
Rob Dockins
3ea59c7a69 Fix windows test output 2021-06-30 16:01:08 -07:00
Rob Dockins
b3c4317784 Update solver definitions related to /^ and %^. 2021-06-30 13:18:12 -07:00
Rob Dockins
acb3ca9fae Update the fin prover with changes to the division operators. 2021-06-30 10:50:40 -07:00
Rob Dockins
52587711a3 rename some identifiers in the test for issue138
We need to avoid the new `down` keyword.
2021-06-30 10:21:50 -07:00
Rob Dockins
5a8a00fc81 Minor test suite updates 2021-06-30 10:19:39 -07:00
Rob Dockins
3debc2bb47 Add a check-docs command to the cry script 2021-06-30 10:06:21 -07:00
Rob Dockins
0778fd8ff2 Update "ProgrammingCryptol"
Minor output changes in the exercises are required.
2021-06-30 10:05:39 -07:00
Rob Dockins
d1f945b20e Add regression test for enumerations with explicit strides 2021-06-30 09:25:43 -07:00
Rob Dockins
33afaccb4b Fix incorrect "unused name" warnings from primitive type declarations. 2021-06-30 09:10:26 -07:00
Rob Dockins
94a4c77fdb Relax the finiteness restriction on the first argument of /^ and %^.
We define `inf /^ n = inf` and `inf %^ n` for finite, positive `n`.
2021-06-30 08:32:39 -07:00
Rob Dockins
14a660167c Add implementations for the new enumeration primitives. 2021-06-29 16:24:40 -07:00
Rob Dockins
6fe2970b52 Add new primtives for the explicit stride enumerations.
Hook them up through the typechecker.  However, we still
need implementations.
2021-06-29 16:23:51 -07:00
Rob Dockins
70245005d8 Add new syntactic forms for enumerations with explicit stride values.
This doesn't yet pipe the new constructs through the typechecker.
2021-06-29 12:08:28 -07:00
Lisanna Dettwyler
dfae4580e3
Support TLS in cryptol-remote-api (#1203)
Add support for TLS connections in both the rpc server
and client. Allow the client to disable certificate validation
via the `verify` keyword argument, i.e.,
`cryptol.connect(verify=False)`. The docker container
for `cryptol-remote-api` also contains a self-signed
cert for testing purposes.

Co-authored-by: Andrew Kent <andrew@galois.com>
2021-06-25 14:26:09 -07:00
robdockins
03ca52ca39
Merge pull request #1221 from GaloisInc/what4-bump
What4 bump
2021-06-22 12:40:29 -07:00
Rob Dockins
4a68856a71 Add a test case for issue #1210
This bug was fixed in What4 via https://github.com/GaloisInc/what4/pull/127
which was included in What4 version 1.2.

Fixes #1210
2021-06-17 11:55:45 -07:00
Rob Dockins
3900c68619 Update build metadata to allow/require What4 1.2 2021-06-17 11:54:09 -07:00
robdockins
6669193dc0
Merge pull request #1154 from GaloisInc/set-path
Add a new 'path' option to the REPL
2021-06-15 16:09:03 -07:00
Rob Dockins
e77b8bb293 Add a new 'path' option to the REPL.
This lets the user reset the module search path. It is a bit of a
blunt instrument as it resets the entire path.  Perhaps we should also
add the ability to add new paths to the front of the search order,
e.g. with a new `:prependpath` command?

Fixes #631
2021-06-15 13:13:49 -07:00
Andrew Kent
36475d1fd9
chore: tweak rpc cryptol expr parser (#1215)
* chore: tweak rpc cryptol expr parser
* chore: update Cryptol server Expression docs
2021-06-11 08:52:34 -07:00
Lisanna Dettwyler
eb829d89b2
Release process improvements (#1176)
Closes #1175

Closes #1134
2021-06-04 11:29:28 -07:00
Andrew Kent
6a9906cd5c
Merge pull request #1200 from GaloisInc/wip/rpc/feat/newtype
initial newtype support for rpc server
2021-06-02 14:19:50 -07:00
Andrew Kent
d456663ad6 chore: address GHC warnings 2021-06-02 10:37:57 -07:00
Andrew Kent
affee13ad6 feat(rpc): newtype (and other complex value) support for RPC server/clients 2021-06-02 08:54:32 -07:00
Ryan Scott
1e07843057
Merge pull request #1207 from GaloisInc/bump-argo
Bump argo submodule to include docs for method results
2021-06-01 16:08:54 -04:00
Ryan Scott
88c369a271 Autogenerate cryptol-remote-api docs (and check them in CI)
Unfortunately, the autogenerated documentation (now located in `Cryptol.rst`)
doesn't yet have all of the information contained within the hand-written
documentation (now located in `old-Cryptol.rst`—see #1206. In pursuit of
eventually fixing that issue, the CI now makes sure that any changes to the
autogenerated documentation are checked in.
2021-06-01 11:00:26 -04:00
Ryan Scott
d7814a959b Bump argo submodule to include docs for method results
This bumps the `argo` submodule to include commit
b9b3edd992,
which adds the ability to document the results of methods (in addition to
their parameters). In addition to dealing with the breaking API changes from
that commit, this adds missing documentation for each method's results.
2021-06-01 09:05:22 -04:00
brianhuffman
33d7273346
Merge pull request #1202 from GaloisInc/lazy-callstack
Defer `CallStack` computations by representing them as data constructors.
2021-05-26 17:24:52 -07:00
Brian Huffman
cbfc6c771c Add special cases to combineCallStacks. 2021-05-26 16:03:18 -07:00
Brian Huffman
88fbbd327a Defer CallStack computations by representing them as data constructors.
This avoids expensive calls to `combineCallStacks` in the common case;
the actual call stack values are only computed in the case where they
need to be printed out.
2021-05-26 12:42:55 -07:00
Daniel Wagner
bd8588adca
Merge pull request #1199 from GaloisInc/feature/master-field-order
Add a field order option for the pretty-printer
2021-05-25 15:08:37 -04:00
Daniel Wagner
fcc6e200a9 let haddocks build 2021-05-25 00:09:14 -04:00
Daniel Wagner
c2fd939511 whitespace only 2021-05-25 00:09:14 -04:00
Daniel Wagner
f1ab9805f4 add a setting to control how records are displayed
For human consumers, it's usually nice to show record fields in the same
order they appear in the source (as sometimes programmers use the field
order as a communication channel to other programmers). However, for
machine consumers, sometimes it is nicer to adhere to a rigid,
predictable format. This commit adds a setting, `field-order`, to switch
between these two modes, with a backward-compatible default.
2021-05-25 00:09:14 -04:00
Iavor Diatchki
2611733c46 Update CHANGES to document layout rule 2021-05-11 09:35:32 -07:00
Iavor S. Diatchki
b6470cc89d
Merge pull request #1188 from GaloisInc/reference-manual
Reference manual
2021-05-10 14:12:46 -07:00
Iavor S. Diatchki
142567d04c
Merge pull request #1186 from GaloisInc/layout
Layout
2021-05-10 14:12:04 -07:00
brianhuffman
4a4673eec4
Merge pull request #1193 from GaloisInc/sort-function
Sort function
2021-05-10 11:07:01 -07:00
Matthew Yacavone
2d9250ad53
rpc: Fix bug where an empty list is sent back from the server as Unit (#1194)
* make readBack of an empty list actually return an empty list

* update test_SHA256
2021-05-07 16:27:05 -07:00
Andrew Kent
af0be41cf1
feat(rpc): make python client compat with python 3.7 (#1195) 2021-05-07 16:19:08 -07:00