Commit Graph

979 Commits

Author SHA1 Message Date
Thomas M. DuBuisson
1c36537d78 Update for SBV 5.7
Conflicts:
	cryptol.cabal
	src/Cryptol/Symbolic.hs
	src/Cryptol/Symbolic/Prims.hs
2015-12-23 14:13:59 -08:00
Adam C. Foltzer
579ccc96a0 backport prover command interface
Conflicts:
	src/Cryptol/REPL/Command.hs
	src/Cryptol/Symbolic.hs
2015-12-23 14:03:59 -08:00
Adam C. Foltzer
917cc27145 version bump to 2.2.6 2015-12-23 11:33:36 -08:00
Adam C. Foltzer
aeefab69a1 refactor :check and :exhaust
This is to set up improvements to the cryptol-server, and therefore
pycryptol interface.

This patch also fixes a regression in pretty-printing output caused by a
previous error in fixity of the `<>` operator
2015-12-22 18:17:20 -08:00
Adam C. Foltzer
f87ea62646 Merge branch 'server-interrupts' into HEAD 2015-12-14 13:56:52 -08:00
Thomas M. DuBuisson
1ffc086ed4 Update for SBV 5.6 2015-12-10 12:38:26 -08:00
Thomas M. DuBuisson
3afdae127a Add known failure notice for issue 212 2015-12-10 12:36:06 -08:00
Thomas M. DuBuisson
04ba8f8871 Remove 'Wrote Prelude' debug leftovers (?) 2015-12-10 12:30:26 -08:00
Thomas M. DuBuisson
6848a834fd Handle quoting, tilde, in :writeByteArray 2015-12-10 00:38:21 -08:00
Adam C. Foltzer
ba318b7a9c use compat prelude in Haskeline module 2015-12-08 15:28:09 -08:00
Adam C. Foltzer
04d62ae221 refine interrupt behavior
In order to prevent Ctrl-Cs in, e.g. Python from bringing down the
server, there's now an option to swallow SIGINT when launching the server.
2015-12-04 15:53:51 -08:00
Adam C. Foltzer
563efcc25b start improving handling of interrupts in server
This notably adds a `MonadBaseControl` instance for the `REPL` monad so
that we can catch asynchronous exceptions in the middle of `REPL`
computations. Since this is a generalization of Haskeline's exception
support, that orphan instance for the console executable is now in terms
of this new instance.
2015-12-03 15:36:43 -08:00
Daniel Wagner
fa780dbd1a skip the quotation marks when reporting temp file location 2015-11-30 16:35:40 -08:00
Thomas M. DuBuisson
fd2421dfad Rename write -> writeByteArray
huh? I thought these were already committed.  Weird.
2015-11-20 09:39:49 -08:00
Adam C. Foltzer
4796b0a75a tweak how the prelude is loaded
This removes the `self-contained` flag, since it is fine for all builds
to have the baked-in prelude as a last resort. Tinkerers can still
change the prelude as long as it's in the search path.

Also removes some unnecessary extra prelude loading by the Cryptol
server by means of a new command
2015-11-16 12:56:36 -08:00
Thomas M. DuBuisson
b355dedcf8 Test files for read/write bytearray command. 2015-11-15 10:42:04 -08:00
Thomas M. DuBuisson
a7f9b0c40d Fix merge issue with :read command. 2015-11-15 10:24:01 -08:00
Thomas M. DuBuisson
0d18bc821c Merge branch 'writeFile' of github.com:TomMD/cryptol into tommd/writeFile 2015-11-15 10:16:16 -08:00
Adam C. Foltzer
6203eedf3a bump SBV lower bound 2015-11-11 15:11:19 -08:00
Adam C. Foltzer
9f3d42344d require new aeson 2015-10-27 16:10:50 -07:00
Adam C. Foltzer
f34145282d relax aeson dependency for stackage 2015-10-27 15:00:23 -07:00
Adam C. Foltzer
18d0588d81 adapt server to new name API 2015-10-27 14:21:05 -07:00
Adam C. Foltzer
92c328f108 fix benchmarks for name API changes 2015-10-22 13:32:37 -07:00
Adam C. Foltzer
3f4e884a79 add missing Prelude.Compat 2015-10-21 13:45:54 -07:00
Adam C. Foltzer
afa90656e9 update stackage files for multiple GHCs 2015-10-21 13:32:31 -07:00
Adam C. Foltzer
b8ba4ebd69 fix benchmarks and NFData instances
The benchmark suite no longer uses the `iteSolver` option.

Added a dependency on `deepseq-generics` so that the `NFData` instances
work correctly in Stackage LTS 2. Versions of `deepseq` before 1.4 have
a default instance that amounts to WHNF rather than NF, so benchmarks
were being measured incorrectly.
2015-10-21 13:19:15 -07:00
Adam C. Foltzer
dfea6365f9 support older directory without CPP 2015-10-21 13:19:15 -07:00
Adam C. Foltzer
3168bef3fa fix some 7.8 build failures 2015-10-21 13:19:15 -07:00
Adam C. Foltzer
d31fc9d24a Adapt to SBV 5.3 interface
We special-case `allSat` because we don't support running parallel
solvers for multiple answers
2015-10-21 13:18:37 -07:00
Brian Huffman
0cde0f3aab Add function unpackIdent :: Ident -> String 2015-10-16 17:08:12 -07:00
Trevor Elliott
993d19011c Remove debug info, and redundant imports 2015-10-16 13:38:06 -07:00
Trevor Elliott
39bac2034a Merge remote-tracking branch 'origin/master' into wip/name-change 2015-10-16 13:23:29 -07:00
Adam C. Foltzer
ad3fdb4e14 use base-compat to remove much CPP 2015-10-08 16:54:08 -07:00
Trevor Elliott
8100d90324 Merge remote-tracking branch 'origin/master' into wip/name-change 2015-10-07 09:18:31 -07:00
Adam C. Foltzer
4c441898d9 remove a merge error from docs Makefile 2015-10-05 15:33:04 -07:00
Trevor Elliott
5436acdbb8 Merge remote-tracking branch 'origin/master' into wip/name-change 2015-10-04 11:49:57 -07:00
Adam C. Foltzer
80daf82b8c add threading by default for executables 2015-10-01 13:50:32 -07:00
Adam C. Foltzer
baddfcaab8 Merge branch 'heads/hotfixes/v2.2.5' 2015-10-01 10:56:30 -07:00
Adam C. Foltzer
02a7afb552 Merge branch 'hotfixes/v2.2.5' into releases 2015-10-01 10:22:34 -07:00
Trevor Elliott
8942289b7f Remove problematic comment 2015-09-30 15:45:49 -07:00
Adam C. Foltzer
7d81568555 remove iteSolver option for compat with sbv 5+ 2015-09-30 14:24:21 -07:00
Trevor Elliott
cacc59529e Update test output 2015-09-29 17:35:18 -07:00
Trevor Elliott
c61467e612 Fix a shift/reduce conflict 2015-09-29 17:35:08 -07:00
Trevor Elliott
f8685e4f7c Prevent warnings or errors from shadowNames, conditionally
In some cases, it's nice to prevent errors/warnings from coming out of
shadowNames.
2015-09-29 14:53:43 -07:00
Trevor Elliott
2cec1e3782 Revert to the original makefile 2015-09-29 14:04:57 -07:00
Trevor Elliott
7f9e4f6aa1 let shouldn't interact with mono-binds 2015-09-29 11:46:21 -07:00
Adam C. Foltzer
243e051df3 bump version number, add SBV upper bound
Conflicts:
	stackage.config
2015-09-29 11:28:30 -07:00
Trevor Elliott
f8e6582230 Update tests and output 2015-09-28 21:26:26 -07:00
Trevor Elliott
0b19e4ab4d Add a NameDisp to renamer errors 2015-09-28 18:05:09 -07:00
Trevor Elliott
1a6825a5c0 Comput the output of :browse based on what's in scope 2015-09-28 17:32:15 -07:00