There is still an issue with the encoding of finitness.
For example, if we know:
a = 1 + min b a
And we know that `b`z is finite, we SHOULD know that `a` is finite too,
but apparently we don't.
1. Preserve order of TODO list, os that we prefer unification variables
2. Stop early when looking for `x = y`.
So if we have 'a = b = c` now we'll get:
a = b
b = c
Before we would get:
a = b
a = c
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.
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.
