This "fix" adds two locations to the search path for Cryptol modules so that we can find the prelude on both Windows and Unix platforms. This is not ideal and should be replaced in the next version, but should have no negative impact for now unless people have multiple Cryptol.cry files hanging out in their filesystems.
Previously, if one command was a prefix of another command, that would lead to an ambiguous lookup from the command trie. Now there are two ways to look up: one works like previously, which is good for tab-completion, and the other will only return one result if there is an exact match.
This means we can now have multiple forms of each command, so we can explicitly have short forms like :e -> :edit that won't be changed just based on what names we give to future commands.
This closes#90, and also #94 which was blocked on this due to :exhaust and :edit conflicting.
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).
This technically fixes#103, but not in a tremendously satisfying way. What we would like to do is clean up the progress bars for the :check, and report which input gave rise to the exception.
When the prover is set to "any", Cryptol now checks for all available,
supported provers, submits the problem to all of them in parallel, and
uses the result from whichever finishes first.
While this stops us from leaving the REPL due to negative indicies,
there is an underlying issue we should deal with: absurdly large
indicies. In this case, `list @ (~zero : [64]) means we'll iterate
through 2^64 elements.
Setting the prover to "offline" now triggers generation of an SMT-Lib file without invoking a prover on it. If the setting "smtfile" has its default value of "-", the script is printed to standard output. If it has any other value, the value taken as the name of the file to write to. If "smtfile" is set to anything other than "-" during a normal, online proof, the script is saved in the given file after the proof completes, rather than being saved in a temporary file that's subsequently deleted. This behavior can be useful for debugging.
Reopens#94; the book talks about using :e to edit files, and having :exhaust in the command trie breaks this. We need to figure out a better way to disambiguate (#90)
intSize was undefined, causing repl terminate. This is probably because
the incorrect type signature using the scoped type variable (`:: a`
should probably have been `:: SBV a`) either way, bitSize and
bitSizeMaybe should use the same code when the size is finite.
When :check was executed on a function accepting words as arguments
cryptol would generate mostly small words. This strategy failed to find
counter-examples in formulas such as:
(\a b -> (((a : [16]) + b) % 17) == ( (a % 17 + b %17) % 17 ) )
This failure is particularly egregious considering 50% of the inputs
result in False. We now generate a better distribution of words and are
discussing use of a smart-check like strategy or an evaluation of the
logic to tailor generation in a future release (see issue #87).
In layout mode, setting cfgModuleScope to true ensures that the lexer
will generate virtual open/close braces and virtual semicolons between
decls.
This is a follow-up to c689a15cfc.
