The `random` primitive previously took a `[32]` seed, but this causes
inconsistency between 32-bit and 64-bit platforms when the seed is large
enough to wrap around in GHC's representation of an `Int`. This patch
switches to an API that seeds directly with four 64-bit words, and so
should behave the same way on our supported platforms.
Note: the hardcoding in this patch is only for the 2.2 hotfix branch; in
the 2.3 branch we will only have to change the default setting for the
typechecker.
This is to set up improvements to the cryptol-server, and therefore
pycryptol interface.
This patch also fixes a regression in pretty-printing output caused by a
previous error in fixity of the `<>` operator
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`
- Move the stackage file so it's not on by default (will test with it on
Jenkins instead of all the time)
- Use CPP to remove unnecessary import warnings in 7.10
- Move the stackage file so it's not on by default (will test with it on
Jenkins instead of all the time)
- Use CPP to remove unnecessary import warnings in 7.10
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.
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.
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`.
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.
The Smtlib solver was translating Fin constraints to True, as it didn't know
how to handle them. They should have been skipped, and returned back as
unsolved goals instead.
This tries to address #125 by making the errors from the renamer a little bit
more clear.
Squashed commit of the following:
commit 8afd3d7961b58df042fe801c3c5e1b9787f813bc
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 19:33:59 2014 -0800
Update tests for new renamer errors
commit 7cac01836d8943cf3b08d6715ac328e3b6658cef
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 19:33:49 2014 -0800
Add `at` on errors and warnings to be more consistent
commit 308908ba318a4cdc839710f66f1a487543f8c07e
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 19:06:57 2014 -0800
More consistent renamer warnings
commit be8100a78e9eaba6d554591121c24ed5dcd3c780
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 18:56:53 2014 -0800
More consistent error formatting from the renamer
commit 26c45c3b51e0bdbcf6a1431cab8e1eb8760ea0bb
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 18:56:36 2014 -0800
Remove an un-triggerable error
commit ccdb93e036ba1e111ccd977c8b3b35523f3c1bf0
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 16:38:44 2014 -0800
Try to give better errors for unbound identifiers
commit eb5784145985bb55c761088eaba27c67d08c1326
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 16:38:23 2014 -0800
Remove old TODOs about located errors
commit b984bb5f451f3aa7b4fc8f15167483c5142ee9a3
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 14:37:34 2014 -0800
Differentiate missing type and expression symbols
commit b9e6f13856db6765dced3cb9565cdc8387a7976d
Author: Trevor Elliott <trevor@galois.com>
Date: Wed Dec 3 14:36:52 2014 -0800
Remove a shadowing warning
Due to the limitations of the GHC runtime, we can't get around the
possibility of out-of-memory errors, but we can prevent individual
bitvectors from being too large for the libgmp-backed bignums.
There is now an architecture-dependent check whenever creating a new
`BV` value in the concrete evaluator to ensure the width does not
exceed the GMP limits. If a width is too large, the evaluation returns
to the REPL much like diving by zero.
To mark a failing test as a known failure, you should add a file with
a name like this:
TESTNAME.icry.fails
When the test runs, if it fails, then the contents of this file is displayed.
It is a probably a good idea for the contents to reference the ticket where
the failure was reported.
When the problem is fixed, the `.fails` should be removed. Failing to do
so will result in test failure (i.e., a test that passes but has a `.fails`
file is considered an error).
See #66 for more discussion. Basically we don't want the type of `it` to be different for unsat or sat results, so we put undefined values in there instead. Also, instead of using tuples and different field names to distinguish formula arguments of various arities, we use a convention of fields `arg1`, `arg2`, ...
Per @weaversa's suggestions in #66, we now bind records to `it` for sat results, leading to less ambiguity about the meaning of those results. There is still some weirdness to this; the fields present in the record change based on the result and the arity of the formula, but this seems like a reasonable approach given that it's not an expression that needs a type.
Similar to what @weaversa requested in #66, we bind `it` to `False`
when we can't find a sat assignment, and `it` to `True` when we've
proved a theorem.
Also adds some simple tests for the sat/prove result binding, and let
binding at the repl.
This test works as of revision db08bfafa9.
Versions of SBV prior to 3.1 did not distinguish the boolean type from
the size-1 bitvector type; this example uses literals like "0b0" and
"0b1", so it triggered the SBV bug, which manifested as a type error from
the external SMT solver.
