GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2025-01-08 17:01:19 +03:00
Code Issues Projects Releases Wiki Activity
3,078 Commits 66 Branches 28 Tags 96 MiB
3debc2bb47
Commit Graph

3078 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
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
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
Brian Huffman
52c91817d9 Update test output due to changed cryptol prelude. 2021-05-06 14:01:27 -07:00
Brian Huffman
9b7e60b9f4 Add some regression tests for sortBy to test stability of the sort. 2021-05-06 12:03:47 -07:00
Brian Huffman
3b62788841 Add sort and sortBy functions to the Cryptol prelude. 2021-05-06 12:01:33 -07:00
robdockins
ac4500a06c
Merge pull request #1192 from GaloisInc/issue1191 
Fix for issue 1191
 2021-05-06 09:34:43 -07:00
Rob Dockins
69e7689527 Fix slightly incorrect documentation 2021-05-05 17:46:17 -07:00
Rob Dockins
a05b4eda7f Add test case for issue 1191 2021-05-05 17:43:32 -07:00
Rob Dockins
a0816576cf A bit more documentation 2021-05-05 17:38:59 -07:00
Rob Dockins
6497daede6 Dispatch to shiftSeqByInteger and shiftSeqByWord 
in the `BitmapVal` cases of `shiftWordByInteger` and
`shiftWordByWord`.
 2021-05-05 17:07:22 -07:00
Rob Dockins
0707bdcd33 Fix #1191 
The barrel shifter was being called with the wrong width; the
length of the sequence to be shifted was passed instead of the number
of bits in the index word.
 2021-05-05 15:52:48 -07:00
Iavor Diatchki
c62d921fb3 More docs 2021-04-30 15:43:14 -07:00
Iavor Diatchki
402c0cc256 Mess around with html teams 2021-04-30 15:42:49 -07:00
Iavor Diatchki
7a98ab5b9b Make a table for operator precedences 2021-04-30 12:00:46 -07:00
Iavor Diatchki
29eefbc09d A shpynx temaplte for a reference manual 2021-04-29 16:47:54 -07:00
Iavor Diatchki
f43d652337 Improve error message and some tests 2021-04-29 14:42:43 -07:00
Iavor Diatchki
3cb97094b9 Unused extension 2021-04-29 14:42:16 -07:00
Iavor Diatchki
206123aa6c Fixes to the algorithm, and remove old code 2021-04-29 12:15:50 -07:00
Iavor Diatchki
7727197800 Split off tokens and new layout in a separate modules 2021-04-29 11:17:34 -07:00