This appears to increase performance of the test and benchmark suites
substantially, but there may be more opportunities to cut down on the
number of solver instances.
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
Also:
- Improves the `lexical error` message, changing it to `unrecognized
character`, and only displaying the one character that caused the
problem.
- Adds more relevant text when showing a lexical error, which should
address #219
- Switches parser to operate over lazy `Data.Text` rather than `String`
This helps with #18 and should also reduce the number of unnecessary
recompiles that were triggered by the Makefile and/or cabal. The cabal
build type is now Simple.
Most of the complication in the TH.hs module is due to the various
places the current git hash might be stored:
1. Detached HEAD: the hash is in `.git/HEAD`
2. On a branch or tag: the hash is in a file pointed to by `.git/HEAD`
in a location like `.git/refs/heads`
3. On a branch or tag but in a repository with packed refs: the hash is
in `.git/packed-refs`
These situations all arise under normal development workflows and on the
Jenkins build machines, but there might be further scenarios that cause
problems. The tradeoff seems worthwhile though as now projects that
build Cryptol as a dependency wind up having to rebuild Cryptol far less
frequently.
Many of our projects that depend on Cryptol break because we forgot to
drag along `Cryptol.cry` or it just can't work out where it is from the
perspective of the other executable.
There's now a new flag `self-contained` in `cryptol.cabal` that is on by
default that bakes the contents of the Prelude into the library, so that
it can be reproduced on demand.
This is really a hack at this point because the module system bakes in
the assumption that a module has an associated file path, so we actually
have to write the contents to a tmp file before reading them back
in. Let's do better than this in the future.
This option is disabled for targets in the Makefile because we want the
standalone interpreter to be using the distribution's `Cryptol.cry`.
Makefile now has two modes depending on whether PREFIX is set. If it's
not, we try to make the distribution as relocatable as possible, meaning
we don't rely on the baked-in-by-cabal data directory. If it is set, we
do use that path.
This involved:
- Moving a couple REPL modules into the Cryptol library hierarchy (those
that don't depend on console libraries)
- Splitting up the Makefile, which unfortunately resulted in a lot of
not-quite-duplication between the two Makefiles. Let's look into
better abstraction...
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
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.
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.
