...
 
Commits (445)

Too many changes to show.

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

......@@ -21,6 +21,7 @@ why3.conf
.*.aux
*.elc
*.summary
.merlin
\#*\#
# /
......@@ -29,7 +30,6 @@ why3.conf
/autom4te.cache
/Makefile
/configure
/install-sh
/semantic.cache
/TAGS
/output_why3
......@@ -38,8 +38,8 @@ why3.conf
/distrib
/why3regtests.err
/why3regtests.out
/.merlin
/src/jessie/.merlin
/_build
# /bench/
/bench/programs/good/booleans/
......@@ -53,6 +53,7 @@ why3.conf
/bench/programs/good/po/
/bench/valid/list/
/bench/ce/*.out
/bench/parsing/bad/*.out
# /bin/
/bin/why3.byte
......@@ -82,6 +83,9 @@ why3.conf
/bin/why3replay.byte
/bin/why3replay.opt
/bin/why3replay
/bin/why3pp.opt
/bin/why3pp.byte
/bin/why3pp
/bin/why3session.opt
/bin/why3session.byte
/bin/why3session
......@@ -94,6 +98,9 @@ why3.conf
/bin/why3webserver.opt
/bin/why3webserver.byte
/bin/why3webserver
/bin/why3pp.opt
/bin/why3pp.byte
/bin/why3pp
/bin/isabelle_client.opt
/bin/isabelle_client.byte
/bin/isabelle_client
......@@ -196,6 +203,8 @@ pvsbin/
/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
......@@ -208,6 +217,8 @@ pvsbin/
/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
......@@ -236,6 +247,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
......@@ -250,6 +268,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/
......
stages:
- docker
- build
- test
- nightly
- deploy
variables:
BUILD_IMAGE: "$CI_REGISTRY_IMAGE:ci-master-2019-11-14"
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.0
<<: *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 ide doc web_ide bench
<<: *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
Léo Andrès <leo@ndrs.fr>
Benedikt Becker <benedikt.becker@inria.fr>
Cláudio Belo Lourenço <belolourenco@gmail.com> <claudio-filipe.belo-da-silva-lourenco@inria.fr>
François Bobot <francois@bobot.eu> <bobot@lri.fr>
François Bobot <francois@bobot.eu> <francois.bobot@cea.fr>
Martin Clochard <martin.clochard@lri.fr> <martin@pc-stagiaire.(none)>
Martin Clochard <martin.clochard@lri.fr> <clochard@MC-MacBook.(none)>
Sylvain Dailler <dailler@adacore.com>
Sylvain Dailler <dailler@adacore.com> <sdailler@hauzar@adacore.com>
Sylvain Dailler <dailler@adacore.com> <sylvain.dailler@inria.fr>
Sylvain Dailler <dailler@adacore.com> <dailler@moloch.lri.fr>
Diego Diverio <diego.diverio@inria.fr>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <Jean-Christophe.Filliatre@lri.fr>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <filliatr@lri.fr>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <jc@evariste.(none)>
......@@ -20,12 +24,14 @@ Léon Gondelman <gondelmans@lri.fr> <lgondelman@lg-PC.(none)>
Léon Gondelman <gondelmans@lri.fr> <leon@ubuntu.(none)>
David Hauzar <david.hauzar@inria.fr> <hauzar@moloch.lri.fr>
Johannes Kanig <kanig@adacore.com> <johannes.kanig@lri.fr>
Rehan Malak <rehan.malak@inria.fr>
Claude Marché <claude.marche@inria.fr> <Claude.Marche@inria.fr>
Claude Marché <claude.marche@inria.fr> <cmarche@dispater.(none)>
Claude Marché <claude.marche@inria.fr> <cmarche@orcus.(none)>
Claude Marché <claude.marche@inria.fr> <cmarche@belzebuth.(none)>
Guillaume Melquiond <guillaume.melquiond@inria.fr>
Guillaume Melquiond <guillaume.melquiond@inria.fr> <melquion@moloch.saclay.inria.fr>
David Mentré <dmentre@linux-france.org>
Kim Nguyễn <kim.nguyen@lri.fr> <kn@lri.fr>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyen@lri.fr>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyen@acces.lri.fr>
......
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 @SEQLIB@ re unix num dynlink @ZIPLIB@ @LABLGTKPKG@ @META_OCAMLGRAPH@ @JSOFOCAMLPKG@ @MLMPFR@
:x: marks a potential source of incompatibility
Standard library
* `pqueue.Pqueue` now modeled using sequences instead of lists :x:
* `queue.Queue` now modeled using sequences instead of lists :x:
* `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`;
`impset.Impset` becomes `set.SetImp`
- in `set.SetApp` and `set.SetImp`, type `t` becomes `set`;
field `contents` becomes `to_fset`; call to `empty` becomes `empty ()`
* new library `fmap` for finite maps
- Fmap: polymorphic, logic finite maps to be used in logic
- MapApp, MapAppInt, MapImp, MapImpInt: monomorphic finite maps to
be used in programs
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:
* ITP constructor Source_and_ce now has 3 arguments instead of 2 :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`;
......@@ -36,34 +52,47 @@ 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
* 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"
and there is a new "Auto level 1" similar 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) for using a prover with
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
* Colors for error can now be edited in the why3.conf more precisely
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
Version 1.2.1, October 28, 2019
-------------------------------
Bug fixes
* fixed compilation with OCaml 4.09
* fixed compilation with Lablgtk3
Provers
* support for CVC4 1.7 (released April 9, 2019)
* support for Alt-Ergo 2.3.0 (released February 11, 2019)
* support for Z3 4.8.6 (released Sep 20, 2019)
* support for Z3 4.8.5 (released Jun 3, 2019)
* support for CVC4 1.7 (released Apr 9, 2019)
* support for Alt-Ergo 2.3.0 (released Feb 11, 2019)
* support for Coq 8.9.1 (released May 20, 2019)
Version 1.2.0, February 11, 2019
......@@ -266,8 +295,8 @@ Standard library
commutative :x:
Miscellaneous
* fixed support for `--enable_relocation=yes` (issue #50)
* fixed support for Windows (issue #70)
* fixed support for `--enable_relocation=yes`
* fixed support for Windows
Version 0.88.2, December 7, 2017
--------------------------------
......
This diff is collapsed.
VERSION=1.2.0+git
VERSION=1.2.1+git
......@@ -2,5 +2,4 @@
if [ ! -f "configure" ]; then
autoconf
automake --add-missing || true
fi
......@@ -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