GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-22 11:27:44 +03:00
Code Issues Projects Releases Wiki Activity
1,968 Commits 65 Branches 28 Tags 83 MiB
4db158eafb
Commit Graph

183 Commits

Author SHA1 Message Date
Aaron Tomb
4db158eafb Bump Cryptol version to 2.7.1 (next release) 2019-04-26 09:14:54 -07:00
Levent Erkok
cbdf7c696a Make cryptol compile with SBV 8.1 2019-03-09 13:26:41 -08:00
Eric Mertens
5786fcf190 Track file content fingerprints alongside loaded modules 2019-02-28 09:40:21 -08:00
Levent Erkok
8d09c79198 Make Cryptol compile with SBV 8.0 
SBV 8.0 is now on hackage, with several backwards compatibility breaking changes. You'll need this patch to compile cryptol against it.
 2019-01-14 16:49:19 -08:00
Kevin Quick
0616c72017
Raise base-compat upper constraint to < 0.11. 2018-08-24 16:45:28 -07:00
Aaron Tomb
45ee929b2d Bump Cabal version to 2.6.1 now that 2.6.0 is out 2018-08-01 14:39:56 -07:00
Aaron Tomb
6b926b1b3c Update Cabal file copyright 2018-08-01 09:05:39 -07:00
Aaron Tomb
70fa2033d5 Update Cabal file for Hackage acceptance 2018-08-01 09:01:30 -07:00
Brian Huffman
2e1dbad005 Improve tab completion for :set command. Fixes #154. 
Tab now completes option names after `:help :set`.

Tab also completes `:help` with names of primitive types
and type classes (cf. #504).
 2018-07-30 18:11:14 -07:00
Aaron Tomb
e42500e706 Update version to 2.6.0 in preparation for release 
After the release, let's update the version to 2.6.1 immediately.
 2018-07-30 13:24:33 -07:00
Brian Huffman
d5c9a030da Split new modules Fixity and Selector from Cryptol.Parser.AST. 2018-06-11 14:28:49 -07:00
Aaron Tomb
99f3fdbf37 Merge Cryptol/Extras.cry with Cryptol.cry 
Closes #427.
 2018-05-23 15:55:05 -07:00
Iavor Diatchki
a0c15874e2 Factor out panic code into its own little package. 2018-05-22 14:27:03 -07:00
Brian Huffman
62dfa1d58f Use sbv version 7.7. Fixes #486. 
Also add regression test for #486.
 2018-04-30 09:54:26 -07:00
Aaron Tomb
126c384ff6 Avoid most recent version of base-compat 
The latest version causes build failures. Ultimately, we should be able
to fix the code to work with newer base-compat versions on various GHC
verions, but this gets builds to work for now.
 2018-04-18 10:07:08 -07:00
Brian Huffman
2e4fa35209 Remove unused package dependencies. 2018-03-21 11:15:46 -07:00
Aaron Tomb
7f27ed592d Remove unnecessary dependency on old-time 2018-03-12 12:53:27 -07:00
Max Orhai
1c2996610d Use blaze for HTML generation 2018-03-05 17:07:19 -08:00
Iavor Diatchki
989e5734ef Move defaulting code to a separate module. 2017-12-22 16:01:19 -08:00
Iavor Diatchki
9c06f07223 Move errors to their own module. 2017-12-21 13:59:53 -08:00
Iavor Diatchki
2d3e146766 Allow evaluation in parameterized module, as long as parameters are not used. 2017-10-27 14:59:32 -07:00
Iavor Diatchki
5c51d32a4e Fix up html syntax highlighting. 2017-10-25 11:12:37 -07:00
Iavor Diatchki
07c5e1fcb8 Bump language standard to 2010. We're beyond '98 anyway... 2017-10-24 11:59:34 -07:00
Iavor S. Diatchki
095a7718d9 Add a pass to rewrite a param. module, into a non-param module 
All definitions are parameterized by all parameters.
 2017-10-19 13:45:40 -07:00
Iavor S. Diatchki
7dc7be45bb Merge remote-tracking branch 'origin/master' into abstract-types 
# Conflicts:
#	src/Cryptol/REPL/Monad.hs
 2017-10-13 10:45:35 -07:00
Iavor S. Diatchki
933e2cd2ee Merge branch 'abstract-types' of github.com:GaloisInc/cryptol into abstract-types 
# Conflicts:
#	src/Cryptol/ModuleSystem/InstantiateModule.hs
 2017-10-05 12:45:11 -07:00
Brian Huffman
a9de74ed5d Implement module-name completion and validation for :browse. 
Fixes #396.
 2017-10-04 19:17:42 -07:00
Iavor Diatchki
5208739653 Don't print directly to stdout. Fixes #166 2017-10-04 15:50:31 -07:00
Iavor Diatchki
2ef0a67d9b Merge branch 'master' into abstract-types 2017-10-03 13:35:57 -07:00
Rob Dockins
f02a3c783b Bump simple-smt version bounds to pull in a bug fix. 
Fixes #457
 2017-10-03 10:20:15 -07:00
Iavor Diatchki
498b99cda3 Split out exports specs; add some parsing for functor instances. 2017-10-02 15:01:45 -07:00
Iavor Diatchki
7135284f80 Basics of sort of module instantiation 2017-09-29 16:27:13 -07:00
Iavor Diatchki
60523d5986 Delete old solver stuff. 
The main user visible effect of this might be that sometime things on
the Cryptol command line are instantiated in a slightly different way:
we get `inf` sometimes when we got a finite example before.

We could work around this if it is an issue, but I am not sure which
behavior is more reasonable.
 2017-09-26 14:02:52 -07:00
Aaron Tomb
c05281d390 Fix spurious failures due to lazy I/O 
Regression test check31 was failing somewhat unpredictably due to the
use of lazy I/O when loading the Z3 prelude for the type checker. Using
the `strict` package seems to fix it.
 2017-09-13 15:31:43 -07:00
Eric Mertens
28bc4f81de Work around happy bug by adding type signature on ipat 2017-09-11 10:36:59 -07:00
Eric Mertens
bf571569fa Add upper bound on happy 
A bug introduced in happy-1.19.6 causes incorrect type signatures
to be generated in the parser source file which lead to type
checker errors
 2017-09-11 10:20:22 -07:00
Iavor S. Diatchki
ca2136fab9 Merge pull request #440 from sliverdragon37/master 
Adds the :ast and :extract-coq commands for printing out a parseable AST
 2017-08-15 10:25:08 -07:00
Eric Mullen
05b8f0f3c1 more polished 2017-08-14 15:45:37 -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
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
d76f21f89e Update benchmarks to find Prelude and CryptolTC.z3 
Since they don’t run in the normal REPL environment, they need to know
about where to find the Prelude and CryptolTC.z3 more directly.
 2017-03-21 12:31:04 -07:00
Iavor S. Diatchki
41131fe7ed Redo the export to SMT story in a much simpler way. 2017-02-16 16:46:38 -08:00
Iavor S. Diatchki
3c15d086d1 Merge branch 'master' into wip/solver 2017-02-08 16:24:46 -08:00
Iavor S. Diatchki
710355176a More rules and things; external solver disabled; we can at least load ChaCha 2017-02-08 15:08:50 -08:00
Brian Huffman
140ab21f11 Add new unoptimized reference interpreter; use in REPL with ":eval <expr>" 2017-02-03 09:02:25 -08:00
Iavor S. Diatchki
f3db823f3e Checkpoint: (broken, but builds) 2017-02-01 11:43:01 -08:00
Iavor S. Diatchki
b788079244 More aggressive goal simplification. 2017-01-31 14:12:53 -08:00
Iavor S. Diatchki
12bb2c30c8 Merge branch 'master' into wip/solver 2017-01-31 10:15:49 -08:00