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.
Cryptol's invocation of proof tools has changed quite a bit since this
PR was first opened, so this took a fair amount of work to
integrate. However we now have the :satNum option, and multiple sat
results are correctly bound to `it`.
We can take advantage of information from signatures if we check instead of
infer. I'm not sure if this is actually paying off, but it should mean that we
unify less when signatures are present, and generate goals that are a little
more specific.
When `:set mono-binds=on`, any local definitions lacking type
signatures will not be generalized (i.e., will be monomorphic). This
reduces what is in most cases unnecessary polymorphism that can give
rise to constraints that are difficult to solve. This also improves
the performance of the Cryptol interpreter by lifting many polymorphic
type applications out of the inner loops that are commonly defined as
bindings in `where` clauses.
The flag is on by default in the Cryptol REPL, and in most cases makes
it possible to leave out more type signatures in `where` clauses than
before. However, some programs really do rely on inferring polymorphic
types for local variables; in this case adding an explicit polymorphic
type signature to the local binding in question will make the program
typecheck.
