...
 
Commits (446)

Too many changes to show.

To preserve performance only 1000 of 1000+ files are displayed.

......@@ -53,6 +53,7 @@ why3.conf
/bench/programs/good/po/
/bench/valid/list/
/bench/ce/*.out
/bench/parsing/bad/*.out
# /bin/
/bin/why3.byte
......@@ -148,9 +149,6 @@ why3.conf
# /lib/why3/
/lib/why3/META
# /lib/ocaml/
/lib/ocaml/why3__BigInt_compat.ml
# /share/
/share/emacs/semantic.cache
/share/Makefile.config
......@@ -192,12 +190,15 @@ pvsbin/
/src/driver/parse_smtv2_model_lexer.ml
/src/driver/parse_smtv2_model_parser.ml
/src/driver/parse_smtv2_model_parser.mli
/src/driver/parse_smtv2_model_parser.conflicts
# /src/parser/
/src/parser/lexer.ml
/src/parser/parser.ml
/src/parser/parser.mli
/src/parser/parser.conflicts
/src/parser/handcrafted.messages.temp
/src/parser/parser_messages.ml
# /src/why3doc/
/src/why3doc/doc_lexer.ml
......@@ -209,6 +210,9 @@ pvsbin/
/src/util/json_lexer.ml
/src/util/json_parser.mli
/src/util/json_parser.ml
/src/util/json_parser.conflicts
/src/util/mlmpfr_wrapper.ml
/src/util/ppx_debug_optim
# /src/session
/src/session/xml.ml
......@@ -237,6 +241,13 @@ pvsbin/
/plugins/python/test/
/plugins/python/py_parser.conflicts
# /plugins/microc/
/plugins/microc/mc_lexer.ml
/plugins/microc/mc_parser.ml
/plugins/microc/mc_parser.mli
/plugins/microc/test/
/plugins/microc/mc_parser.conflicts
# /drivers
/drivers/coq-realizations.aux
/drivers/pvs-realizations.aux
......@@ -251,6 +262,8 @@ pvsbin/
!/tests/test-extraction/main.ml
/tests/python/*/why3session.xml
/tests/python/*/why3shapes.gz
/tests/microc/*/why3session.xml
/tests/microc/*/why3shapes.gz
# /examples/
/examples/in_progress/course/
......@@ -305,7 +318,6 @@ pvsbin/
/examples/prover/bench2
/examples/prover/macro_generator/depend
/examples/prover/macro_generator/build
/examples/in_progress/multiprecision/build/
# Try Why3
/src/trywhy3/trywhy3.byte
......
stages:
- docker
- build
- test
- nightly
- deploy
variables:
BUILD_IMAGE: "$CI_REGISTRY_IMAGE:ci-master-2019-10-04"
GIT_CLEAN_FLAGS: "-ffdxq"
build-image:
stage: docker
script:
- docker login -u "$CI_REGISTRY_USER" -p "$CI_JOB_TOKEN" "$CI_REGISTRY"
- if docker pull "$BUILD_IMAGE"; then echo "Image already exists!"; exit 1; fi
- docker build --force-rm -t "$BUILD_IMAGE" - < misc/Dockerfile.build
- docker push "$BUILD_IMAGE"
- docker rmi "$BUILD_IMAGE"
only:
variables:
- $NEW_BUILD_IMAGE
tags:
- shell
.docker_template: &docker_definition
image: "$BUILD_IMAGE"
tags:
- docker
.build_template: &build_definition
stage: build
script:
- misc/ci-docker.sh misc/ci-local.sh
- misc/ci-local.sh
<<: *docker_definition
build-system:
variables:
COMPILER: system
<<: *build_definition
build-4.02.3:
variables:
COMPILER: 4.02.3
<<: *build_definition
build-4.03.0:
variables:
COMPILER: 4.03.0
<<: *build_definition
build-4.04.2:
variables:
COMPILER: 4.04.2
COMPILER: ocaml-system
<<: *build_definition
build-4.05.0:
......@@ -44,10 +54,21 @@ build-4.07.1:
COMPILER: 4.07.1
<<: *build_definition
build-4.08.1:
variables:
COMPILER: 4.08.1
<<: *build_definition
build-4.09.0:
variables:
COMPILER: 4.09.0
<<: *build_definition
.bench_template1: &bench_definition_always
stage: test
script:
- misc/ci-docker.sh misc/ci-local.sh bench ide
- misc/ci-local.sh bench ide
<<: *docker_definition
.bench_template2: &bench_definition
<<: *bench_definition_always
......@@ -58,21 +79,6 @@ build-4.07.1:
bench-system:
<<: *bench_definition_always
bench-4.02.3:
variables:
COMPILER: 4.02.3
<<: *bench_definition
bench-4.03.0:
variables:
COMPILER: 4.03.0
<<: *bench_definition
bench-4.04.2:
variables:
COMPILER: 4.04.2
<<: *bench_definition
bench-4.05.0:
variables:
COMPILER: 4.05.0
......@@ -88,45 +94,59 @@ bench-4.07.1:
COMPILER: 4.07.1
<<: *bench_definition_always
full-4.07.1:
bench-4.08.1:
variables:
COMPILER: 4.08.1
<<: *bench_definition
bench-4.09.0:
variables:
COMPILER: 4.09.1
<<: *bench_definition
full:
stage: test
variables:
COMPILER: 4.07.1
DEBIAN_PACKAGES: hevea rubber texlive-latex-extra lmodern texlive-fonts-recommended
OPAM_PACKAGES: coq-flocq.3.1.0 js_of_ocaml-ppx alt-ergo.2.0.0
COMPILER: full
script:
- misc/ci-docker.sh misc/ci-local.sh bench ide doc
- misc/ci-local.sh bench ide doc web_ide
<<: *docker_definition
nightly-bench:
stage: nightly
variables:
COMPILER: 4.05.0
DEBIAN_PACKAGES: cvc3 spass
OPAM_PACKAGES: alt-ergo.2.0.0 zenon.0.8.0 coq.8.7.2 coq-flocq.3.1.0
COMPILER: bench
script:
- misc/ci-docker.sh misc/ci-local.sh nightly-bench-reduced
- misc/ci-local.sh nightly-bench-reduced
<<: *docker_definition
ce-bench:
stage: nightly
variables:
COMPILER: 4.05.0
DEBIAN_PACKAGES: cvc3 spass
OPAM_PACKAGES: alt-ergo.2.0.0 zenon.0.8.0 coq.8.7.2 coq-flocq.3.1.0
COMPILER: bench
script:
- misc/ci-docker.sh misc/ci-local.sh ce-bench
- misc/ci-local.sh ce-bench
<<: *docker_definition
opam:
stage: build
variables:
COMPILER: system
script:
- misc/ci-docker.sh misc/ci-opam.sh
- opam pin -v -y add why3 .
- opam pin -v -y add why3-ide .
<<: *docker_definition
deploy:
stage: deploy
script:
- misc/ci-deploy.sh
- IMAGE=$CI_REGISTRY_IMAGE:$(echo $CI_COMMIT_REF_NAME | tr -cs "[:alnum:].\n" "-")
- docker login -u "$CI_REGISTRY_USER" -p "$CI_JOB_TOKEN" "$CI_REGISTRY"
- docker pull "$IMAGE" || true
- docker build --force-rm --cache-from "$IMAGE" -t "$IMAGE" -f misc/Dockerfile.deploy .
- docker push "$IMAGE"
- docker rmi "$IMAGE"
only:
- master
- /^bugfix[/]v[0-9.]*$/
- tags
tags:
- shell
......@@ -11,6 +11,7 @@ Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <filliatr@lri.fr>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <jc@evariste.(none)>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <jc@gemini.(none)>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <filliatr@balrog.(none)>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <jean-christophe.filliatre@inria.fr>
Clément Fumex <clement.fumex@inria.fr> <fumex@moloch.lri.fr>
Quentin Garchery <garchery.quentin@gmail.com> <quentin.garchery@inria.fr>
Léon Gondelman <gondelmans@lri.fr>
......@@ -31,10 +32,11 @@ Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyen@acces.lri.fr>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyenthiminhtuyen@minhtuyen.local>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <thi-minh-tuyen.nguyen@inria.fr>
Andrei Paskevich <andrei@lri.fr> <andrei@tertium.org>
Mário Pereira <mpereira@lri.fr>
Mário Pereira <mpereira@lri.fr> <mario.j.p.pereira@gmail.com>
Mário Pereira <mpereira@lri.fr> <parreira@lri.fr>
Mário Pereira <mpereira@lri.fr> <mario-jose.parreira-pereira@inria.fr>
Andrei Paskevich <andrei@lri.fr> <andriy.paskevych@inria.fr>
Mário Pereira <mariojppereira@gmail.com> <mpereira@lri.fr>
Mário Pereira <mariojppereira@gmail.com> <mario.j.p.pereira@gmail.com>
Mário Pereira <mariojppereira@gmail.com> <parreira@lri.fr>
Mário Pereira <mariojppereira@gmail.com> <mario-jose.parreira-pereira@inria.fr>
Raphaël Rieu-Helft <raphael.rieu-helft@lri.fr>
Raphaël Rieu-Helft <raphael.rieu-helft@lri.fr> <raphael.rieu-helft@inria.fr>
Raphaël Rieu-Helft <raphael.rieu-helft@lri.fr> <raphael.rieu-helft@trust-in-soft.com>
......
S src/util
S src/core
S src/driver
S src/extract
S src/mlw
S src/parser
S src/transform
......@@ -22,6 +23,7 @@ S plugins/python
B src/util
B src/core
B src/driver
B src/extract
B src/mlw
B src/parser
B src/transform
......@@ -41,4 +43,4 @@ B plugins/tptp
B plugins/python
B lib/why3
PKG str unix num dynlink @ZIPLIB@ @LABLGTKPKG@ @META_OCAMLGRAPH@ @JSOFOCAMLPKG@
PKG str unix num dynlink @ZIPLIB@ @LABLGTKPKG@ @META_OCAMLGRAPH@ @JSOFOCAMLPKG@ @MLMPFR@
:x: marks a potential source of incompatibility
Standard library
* `pqueue.Pqueue` is now modeled using sequences instead of lists :x:
* `queue.Queue` is now modeled using sequences instead of lists :x:
* the `set` library has been revamped :x:
- in `set.Fset`, type `set` becomes `fset`; `choose` becomes `pick`
- module `appset.Appset` becomes `set.SetApp`;
......@@ -9,20 +11,33 @@ Standard library
field `contents` becomes `to_fset`; call to `empty` becomes `empty ()`
Language
* It is now possible to give a name to requires and assertions.
`requires Hyp { a = 3 }` tries to give the name `Hyp` to the corresponding
hypothesis after introduction. This uses the attribute [@hyp_name:] which is
now reserved.
* it is now possible to give a name to preconditions and assertions;
`requires Foo { a = 3 }` sets the attribute `[@hyp_name:Foo]`, which tries
to give the name `Foo` to the corresponding hypothesis after introduction
* identifiers used for specification (resp. definition) of a function `foo`
have been renamed from `foo_spec` (resp. `foo_def`) to `foo'spec` (resp. `foo'def`) :x:
* identifiers used for goals `VC foo` have been renamed to `foo'vc`
* identifiers used for record constructor `mk foo` have been renamed to `foo'mk` :x:
* the `alias` clause can now be used in program functions to force the aliasing
of function parameters and/or named returns
Tools
* counterexamples given by `why3prove` are no longer printed using JSON
by default; pass option `--json` to restore the previous behavior
* new tool `why3pp` to pretty print Why3 source code (inductive definitions to LaTeX,
formatting of mlw files)
API
* `Call_provers.print_prover_result` now takes an additional argument
`~json_model` to indicate whether counterexamples are printed using JSON :x:
* Counterexamples: indices of array are now model_value. :x:
* ITP constructor Task now contain the location of the goal :x:
* indices of array are now `model_value` for counterexamples :x:
* ITP constructor `Task` now contains the location of the goal :x:
* ITP constructor `Source_and_ce` now has 3 arguments instead of 2 :x:
* ITP constructors `File_contents` and `Source_and_ce` has a new argument for
the file format :x:
* ITP constructor `File_contents` has a new boolean argument for
interpretation of the file in the IDE as `read_only` :x:
* New ITP constructor `Ident_notif_loc`
Transformations
* `apply`/`rewrite` behaves better in presence of `let`;
......@@ -33,29 +48,38 @@ Transformations
* `induction_arg_ty_lex` is now equivalent to `induction_ty_lex`
* `induction_arg_pr` now takes an optional argument that indicates what to
generalize in the induction
* `destruct` now destruct `not p` into `p -> false`. `destruct_rec` is
allowed to further destruct afterwards.
`destruct` can also destruct `true` and `false`.
* decision procedures used for reflection now must be declared explicitly using
`meta reflection val <function_name>` :x:
* `remove` should not raise unnecessary popups anymore. Added `remove_rec`.
`bisect` should not raise unnecessary popups too.
* `destruct` now destructs `not p` into `p -> false`;
`destruct_rec` can further destruct afterwards;
`destruct` can also destruct `true` and `false` :x:
* decision procedures used for reflection must now be declared explicitly using
`meta reflection val foo` :x:
* `remove` and `bisect` should not raise unnecessary popups anymore
* added `remove_rec`
IDE
* display of counterexamples in the Task view has been improved
* auto jumping to next unproved goal can now be disabled in the preferences
* add a "reset proofs" command in the Tools menu. It removes all proofs in
the session
* strategies can now be defined using %t (resp. %m) for using a prover with
* added a "reset proofs" command in the Tools menu to remove all the proofs
from the session
* default proof strategies "Auto level 1" and "Auto level 2"
have been respectively renamed "Auto level 2" and "Auto level 3";
"Auto level 1" now behaves similarly to "Auto level 0" but with a longer
time limit; more details in the manual, section 9.6 "Proof Strategies" :x:
* strategies can now be defined using `%t` (resp. `%m`) to call a prover with
the default timelimit (resp. memlimit)
* added minimal search menu
* A merlin-like feature to find the ident located under the cursor has been
added in the Edit menu.
* Read only file can now be displayed and removed by right clicking on their
tab titles
Realizations
* Added experimental realizations for new Set theories in both Isabelle and
Coq
* added experimental realizations for new Set theories in both Isabelle and Coq
Provers
* support for CVC4 1.7 (released April 9, 2019)
* support for Alt-Ergo 2.3.0 (released February 11, 2019)
* support for Coq 8.9.1 (released May 20, 2019)
Version 1.2.0, February 11, 2019
--------------------------------
......
......@@ -9,12 +9,12 @@ After unpacking, installation is done by
./configure
make
make install (as root)
make install (as super-user if needed)
To install also the Ocaml library, do
make byte
make install-lib (as root)
make install-lib (as super-user if needed)
Installation from the git repository
......
This diff is collapsed.
......@@ -7,6 +7,8 @@
# export WHY3DATA=.
# export WHY3LOADPATH=theories
has_mpfr=`sed -n -e 's/MPFRLIB *= *\([^ ]\+\)/\1/p' share/Makefile.config`
shopt -s nullglob
suffix=$1
......@@ -44,6 +46,20 @@ goods () {
fi
}
plugins () {
pgm="bin/why3prove$suffix"
test -d $1 || exit 1
for f in $1/*.$3 ; do
printf " $f... "
if ! $pgm $2 $f > /dev/null 2>&1; then
echo "FAILED!"
echo "invocation: $pgm $2 $f"
exit 1
fi
echo "ok"
done
}
bads () {
pgm="bin/why3prove$suffix"
test -d $1 || exit 1
......@@ -323,6 +339,8 @@ goods examples/in_progress/ring_decision "-L examples/in_progress/ring_decision"
goods examples/multiprecision "-L examples/multiprecision"
goods examples/prover "-L examples/prover --debug ignore_unused_vars"
goods examples/in_progress
plugins tests/python --type-only py
plugins tests/microc --type-only c
echo ""
echo "=== Checking valid goals ==="
......@@ -366,6 +384,21 @@ execute examples/vstte10_queens.mlw NQueens.test8
# examples/queens.mlw NQueensBits.test8
# fails: cannot find definition of routine eq
# examples/residual.mlw Test.test_astar
# test of execution on real numbers; only if mpfr installed
if test -n "$has_mpfr"; then
execute bench/interp/real.mlw R.test0
execute bench/interp/real.mlw R.test1
execute bench/interp/real.mlw R.test2
execute bench/interp/real.mlw R.test3
execute bench/interp/real.mlw R.test_exp
execute bench/interp/real.mlw R.test_log
execute bench/interp/real.mlw R.test_exp_log
execute bench/interp/real.mlw R.bench1
execute bench/interp/real.mlw R.bench2
execute bench/interp/real.mlw R.bench3
else
echo "MPFR not installed, skipping tests"
fi
echo ""
echo "=== Checking extraction to OCaml ==="
......@@ -373,14 +406,12 @@ extract bench/extraction -D ocaml64
extract_and_run examples/euler001 euler001.ml 1000000
extract_and_run examples/gcd gcd.ml 6 15
extract_and_run examples/vstte10_max_sum vstte10_max_sum.ml
# needs to port
# extract_and_run examples/vstte12_combinators vstte12_combinators.ml "((((K K) K) K) K)"
extract_and_run examples/vstte12_combinators vstte12_combinators.ml "((((K K) K) K) K)"
extract_and_run examples/defunctionalization defunctionalization.ml
extract_and_run examples/sudoku sudoku.ml 2,0,9,0,0,0,0,1,0,0,0,0,0,6,0,0,0,0,0,5,3,8,0,2,7,0,0,3,0,0,0,0,0,0,0,0,0,0,0,0,7,5,0,0,3,0,4,1,2,0,8,9,0,0,0,0,4,0,9,0,0,2,0,8,0,0,0,0,1,0,0,5,0,0,0,0,0,0,0,7,6
echo ""
echo "=== Checking extraction to C ==="
extract_and_test_wmp examples/in_progress/multiprecision
extract_and_test_wmp examples/multiprecision
echo ""
......@@ -404,7 +435,6 @@ replay examples/in_progress/ring_decision "-L examples/in_progress/ring_decision
replay examples/multiprecision "-L examples/multiprecision --merging-only"
replay examples/prover "-L examples/prover --merging-only --debug ignore_unused_vars"
#replay examples/in_progress --merging-only
#replay examples/in_progress/multiprecision "-L examples/in_progress/multiprecision --merging-only"
echo ""
echo "=== Checking --list-* ==="
......
......@@ -33,22 +33,28 @@ is_xfail=none
decide_fail () {
case "$1" in
# Inconsistent integer values between two runs
"bench/ce/algebraic_types_mono_Z3,4.6.0_SP")
"bench/ce/algebraic_types_mono_Z3,4.8.4_SP")
is_xfail=integer_values;;
# Inconsistent results between two runs
"bench/ce/algebraic_types_mono_Z3,4.6.0_WP")
"bench/ce/algebraic_types_mono_Z3,4.8.4_WP")