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`.
The issue is not the set of names in scope, it is the type names
printed out by the :t command. It should use the same names that
are in scope in the module.
If the type of an expression contains a type synonym that is not
in scope at all, then I'm not sure what exactly it should do.
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.
- update copyright date
- point to new Haskell.org downloads rather than HP
- new WiX version
- smoke test subsumes `:prove True`
- repo layout simpler (no `notebook`, `sbv` subdirs)
- no notebook documentation
Closes#112.
This adds a check at REPL startup that `cvc4` is an executable on the
path. It doesn't check for versions, as we're mostly stuck with
"prerelease" versions.
I made it easy to add more smoke tests at startup; we should add these
as we think of them.
We previously read a batch script from `$HOME/.cryptol` on REPL startup,
but this turns out to conflict with the directory returned by
`System.Directory.getAppUserDataDirectory`.
This commit changes the name to `.cryptolrc` and updates the interpreter
flags and such accordingly.
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...
- Introduce monad type SpecT m a = StateT SpecCache (ModuleT m) a
(easier to call from code written in ModuleT monad)
- Fix bug where specializing expressions under ETAbs could cause
type variables to `escape` from their scopes.
- Function `withDeclGroups` lets you run arbitrary specializer monad
action within the context of a set of DeclGroups. This is used to
implement specialization of where-expressions, and also for the new
function `specializeDeclGroups`, which specializes a set of DeclGroups
using the monomorphic bindings as the 'root set' to determine what
other specialized bindings to include.
Previously we were just using Prelude's `readFile`, which uses the
system default locale. This meant that people writing Cryptol in other
locales might produce source files that work fine for them but not
others. Now the interpreter sets the default locale to utf8 at startup.
Additionally, the code to catch exceptions from loading modules was too
lazy, allowing exceptions to bring down the whole process when the
module contents were forced outside of the `try`.
We also assumed that any IO exception was from files not being found;
there's now an "Other IO exception" possiblity. Incorrect locales will
trigger this alternative because the actual IOException raised isn't
specific to locale errors.
Revised how we do output for `:sat` and `:prove` without arguments,
making it more clear what properties are being checked in each case.
Also reworded the output of `:check` slightly in the case where the
property has no inputs. It would be nice to make `:check` output more
consistent with the others.
Fixes a bug pointed out by @weaversa:
https://github.com/GaloisInc/cryptol/issues/127#issuecomment-64464455
In addition to the other search path changes in #127, we now will add
the directory containing files to be loaded to the search path. This
applies to:
- files loaded with a command line argument, like in the original
comment
- arguments to `:l`, so for example `:l examples/DES.cry` would work
- batch file arguments, so for example running `cryptol -b
/some/path/bar.cry` adds `/some/path` to the search path.
By popular demand and general consensus (#163), defaulting and shadowing
warnings are now off by default in the notebook. They can be reenabled
by using `:set` in a cell much like they can be toggled at the command
line.
The main reason for this change is that we can't help but emit all of
the warnings for the entire module context whenever any part of that
module changes. If we could focus the warnings so that they're only
relevant for this particular cell, we should probably reenable them by
default.
