Commit Graph

25 Commits

Author SHA1 Message Date
Adam C. Foltzer
3f401b4321 bump version constraint for ipython-kernel 2015-02-12 08:57:18 -08:00
Adam C. Foltzer
adcd96fa47 make notebook distributable
This commit brings the notebook into the rest of the distribution
infrastructure set up for cryptol. The main points are:

- new icryptol-kernel executable
- new icryptol shell script that wraps ipython and makes sure the
  cryptol profile is set up
- Makefile target for friendly local testing (`make notebook`)
- moved example notebooks to examples subdirectory
2015-02-11 16:21:43 -08:00
Adam C. Foltzer
62d8277574 add just enough strictness to evalCmd 2015-02-05 17:05:11 -08:00
Adam C. Foltzer
3180d12740 Merge branch 'master' into feature/issue75 2015-02-05 16:28:56 -08:00
Adam C. Foltzer
9f61032289 update notebook build mechanisms 2015-02-05 16:12:36 -08:00
Adam C. Foltzer
705230f24b another sdist fix 2015-01-28 11:28:52 -08:00
Adam C. Foltzer
92edf47dbd fix cabal sdist by including configure 2015-01-28 11:01:53 -08:00
David Raymond Christiansen
7cd2739831 Make notebook use iPython Haskell library
Now, the notebook interface runs its own ZeroMQ interface using the
EasyKernel module that is now exported from IHaskell's underlying
ipython-kernel library. This eliminates the line protocol with the
Python wrapper, and it should work on Windows (though it is not tested
there).

Part of this involved making the REPL monad able to change the IO action
used to print strings.

Continuing issues and improvment possibilities are in the issue tracker
- see issue #75 for a starting point.
2015-01-27 17:38:24 -08:00
Trevor Elliott
ca06580fc6 Remove the dependency on mtl 2015-01-27 15:12:35 -08:00
Brian Huffman
64d53546fe Remove custom fork of SBV library in favor of the official SBV-4.0.
Fixes #35.
2015-01-23 14:22:18 -08:00
Adam C. Foltzer
13a385d8c5 Fixes #172
There's now a more sensible hierarchy of locations that Cryptol uses to
look for modules. By default, in order it looks for libraries in:

1. The directories specified in the CRYPTOLPATH environment variable
2. The current directory
3. The user data directory (something like `$HOME/.cryptol`)
4. Relative to the executable's install directory
5. The static path used when building the executable (cabal's data-dir)

There is also a new command-line flag for the interpreter:
`--cryptolpath-only` which makes the interpreter ignore locations 2-5.

This commit also reworks the Makefile and build/release process. These
are bunched together because they play off each other quite a bit; the
build/release process determines the location of the `Cryptol.cry`,
which must be found when looking for modules.

Rather than leaning on `cabal install`, we now use a combination of
`cabal configure`, `cabal build`, and `cabal copy`. A couple of upshots
to this:

- More of the release staging is handled by cabal -- we don't have to go
  in and manually copy things out of the sandbox. In fact, the `cryptol`
  executable never goes into the sandbox.

- The testing infrastructure runs on executables that are in place in
  the staging directory, rather than in the sandbox. This should be more
  hygienic and realistic.

- The `Cryptol.cry` prelude file is now in `/share/cryptol` in order to
  better reflect the common POSIX structure. This means Cryptol will
  play nicer in global installs, and mirrors what other interpreted
  languages do.

- The default build settings use a prefix of `/usr/local` rather than
  using the sandbox directory. This makes them more relocatable for
  binary distributions. Set PREFIX= before making to change this.
2015-01-21 15:03:16 -08:00
Iavor S. Diatchki
e217600b61 Changes to make things work with GHC 7.10 2015-01-06 09:21:47 -08:00
Adam C. Foltzer
794017ecf5 add guards for bit vector widths during concrete evaluation
Tested on my 64-bit machine; will run tests on Jenkins slaves
2014-11-04 12:11:24 -08:00
Adam C. Foltzer
b7c33c1e86 add reasonable profiling defaults for library and executable 2014-09-25 16:45:28 -07:00
Adam C. Foltzer
6b12984912 bump version for 2.1.0 alpha 2014-09-14 19:35:24 -07:00
Adam C. Foltzer
68d1e3d6c6 Add default-language to cabal file. Closes #71 2014-09-14 14:37:43 -07:00
Thomas M. DuBuisson
a2fbf632f5 Use tf-random for higher-quality randoms.
Notice the randoms from StdGen are well-known to be quite bad.  For
example, see comments in issue #86.
2014-09-08 21:47:05 -07:00
Adam C. Foltzer
d409116160 Merge branch 'devel'
This was the branch I originally set up for git flow, but we're moving
to production=release and develop=master, so this branch is obsolete.
2014-08-19 10:31:31 -07:00
Aaron Tomb
abe336d907 Added SignCast instance and exported sbv
Changes necessary for SAWCore's use of SBV. Ultimately, these should be
merged into the upstream SBV package.
2014-08-06 09:49:19 -07:00
Adam C. Foltzer
ab39a74c98 fix #67
The python side of the notebook needed to be updated to expect a
.cabal-sandbox rather than cabal-dev sandbox. Also added a -fnotebook
flag to the cabal file to build the Haskell side of it.
2014-07-29 08:53:44 -07:00
Brian Huffman
db08bfafa9 Merge changes from SBV release version 3.1 2014-07-21 15:23:34 -07:00
Brian Huffman
b304eb2ef0 New module Cryptol.TypeCheck.TypeOf has functions to compute Type of an Expr 2014-05-09 16:27:07 -07:00
Adam C. Foltzer
7f44d616dd fixup: Paths_cryptol_parser 2014-04-18 10:28:46 -07:00
Adam C. Foltzer
5b25f8c21a it's not just a parser anymore 2014-04-18 10:18:26 -07:00
Adam C. Foltzer
ba0a0e8576 Initial import from internal repo 2014-04-17 15:34:25 -07:00