https://github.com/EasyCrypt/easycrypt
Revision 36f7f5a29ef730b23ec3b2a96e76e387e90ea0e5 authored by Alley Stoughton on 21 February 2018, 22:32:02 UTC, committed by Pierre-Yves Strub on 26 February 2018, 15:04:53 UTC
The elements of prover [...] have one of the following forms, where s is a string: s (add s to the use-only list) +s (add include s to the include/exclude list) -s (add exclude s to the include/exclude list) The include/exclude list is ordered, so that later instructions can supersede earlier ones. The use-only list was not ordered, but now is. The relative order of the use-only and include/exclude lists is irrelevant, so that, e.g., prover ["Z3" +"Alt-Ergo"] and prover [+"Alt-Ergo" "Z3"] are equivalent. The semantics is that the use-only list is first interpreted (if it's empty, one starts with the current provers as the base), and only then are the instructions of the include/exclude list applied to it, in order. There was already the special use-only instruction "ALL". Now, there is also the use-only instruction "CLEAR", which clears the use-only list, but may be superseded by the use-only instructions that follow. Examples (assuming "Z3" and "Alt-Ergo" are only known provers): prover []. (* a no-op *) prover [+"Z3"] (* adds just "Z3" to whatever current provers are *) prover [-"Z3"] (* removes just "Z3" from whatever current provers are *) prover ["ALL"] (* results in "Z3", "Alt-Ergo" *) prover ["CLEAR"] (* results in nothing *) prover ["CLEAR" +"Z3"] (* results in just "Z3" *) prover [+"Z3" "CLEAR"] (* results in just "Z3" *) prover ["CLEAR" "Z3"] (* result in just "Z3" *) prover ["Z3" "CLEAR"] (* results in nothing *) prover [-"Z3" "ALL"] (* results in "Alt-Ergo" *) prover [+"Z3" "ALL" -"Z3"] (* results in "Alt-Ergo" *) prover [-"Z3" "ALL" +"Z3"] (* results in "Z3", "Alt-Ergo" *)
1 parent 5115c89
Tip revision: 36f7f5a29ef730b23ec3b2a96e76e387e90ea0e5 authored by Alley Stoughton on 21 February 2018, 22:32:02 UTC
Added clean way to clear the list of current provers.
Added clean way to clear the list of current provers.
Tip revision: 36f7f5a
MANIFEST
Makefile
Makefile.system
MANIFEST
README.md
COPYRIGHT
# ocamlbuild configuration
_tags
myocamlbuild.ml
config/tests.config
# EasyCrypt sources
find:src:*.ml
find:src:*.mli
find:src:*.mly
find:src:*.mll
src/ecVersion.ml.in
exclude:src/ecVersion.ml
# EasyCrypt theories
find:theories:*.ec
find:theories:*.eca
# EasyCrypt extraction support library
find:extraction:*.ml
find:extraction:*.mli
find:extraction:*.ec
# system
system/Makefile
system/*.c
system/win32/*.c
system/unix/*.c
# EasyCrypt examples
find:examples:*.ec
find:examples:*.eca
# Build scripts
scripts/install/install-sh
scripts/install/distribution
scripts/testing/runtest
scripts/srctx/keywords
find:scripts/patches/:*
Computing file changes ...