Commit 53109ace authored by François Bobot's avatar François Bobot

Merge remote-tracking branch 'origin/master' into computer_division_for_master

parents 1925dcc8 0dc247c1

Too many changes to show.

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

......@@ -39,6 +39,7 @@ why3.conf
/why3regtests.err
/why3regtests.out
/.merlin
/src/jessie/.merlin
# /bench/
/bench/programs/good/booleans/
......@@ -119,16 +120,19 @@ why3.conf
/doc/manual.synctex.gz
/doc/*.haux
/doc/*.pdf
/doc/generated/
/doc/html/
/doc/*.hind
/doc/*.htoc
/doc/bnf
/doc/bnf.ml
/doc/*_bnf.tex
/doc/apidoc.tex
/doc/apidoc/
/doc/stdlibdoc/
/doc/texput.log
/doc/extract_ocaml_code
/doc/*__*.ml
/doc/*_bnf.tex
# /lib
/lib/why3-cpulimit
......@@ -153,9 +157,6 @@ why3.conf
# /src/
/src/config.sh
# Coq tactic
/src/coq-tactic/why3tac.ml
# Coq
/lib/coq/version
......@@ -197,6 +198,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
......@@ -294,13 +297,16 @@ pvsbin/
/examples/in_progress/bigInt/*__*.ml
/examples/in_progress/mp/jsmain.js
/examples/in_progress/mp/*__*.ml
/examples/prover/build/*__*.ml
/examples/prover/.depend
/examples/prover/build/prover
/examples/prover/prover
/examples/prover/prover.ml
/examples/prover/bench/*/*.out
/examples/prover/bench/*/*.txt
/examples/prover/bench1
/examples/prover/bench2
/examples/prover/macro_generator/depend
/examples/prover/macro_generator/build
/examples/in_progress/multiprecision/build/
# Try Why3
/src/trywhy3/trywhy3.byte
......
......@@ -38,12 +38,12 @@ bench:
variables:
COMPILER: system
script:
- misc/ci-docker.sh misc/ci-local.sh bench
- misc/ci-docker.sh misc/ci-local.sh bench ide
.bench_template: &bench_definition
stage: test
script:
- misc/ci-docker.sh misc/ci-local.sh bench
- misc/ci-docker.sh misc/ci-local.sh bench ide
only:
- tags
- schedules
......@@ -68,6 +68,15 @@ bench-4.06.0:
COMPILER: 4.06.0
<<: *bench_definition
full:
stage: test
variables:
COMPILER: system
DEBIAN_PACKAGES: hevea rubber texlive-latex-extra
OPAM_PACKAGES: coq-flocq.2.6.1 js_of_ocaml-ppx
script:
- misc/ci-docker.sh misc/ci-local.sh bench ide doc
opam:
stage: build
variables:
......
......@@ -9,7 +9,6 @@ S src/whyml
S src/session
S src/tools
S src/ide
S src/coq-tactic
S src/why3session
S src/why3doc
S src/jessie
......@@ -31,7 +30,6 @@ B src/whyml
B src/session
B src/tools
B src/ide
B src/coq-tactic
B src/why3session
B src/why3doc
B src/jessie
......
......@@ -25,6 +25,7 @@ Language
Flanagan-Saxe-like VC generation
* support for type coercions in logic using `meta coercion`
* deprecated `theory`; use `module` instead
* term on the left of sequence `;` must be of type `unit` :x:
Standard library
* machine integers in `mach.int.*` are now range types :x:
......@@ -33,6 +34,7 @@ Standard library
Extraction
* improved extraction to OCaml
* added partial extraction to C using the memory model of `mach.c`
* added extraction to CakeML (using 'why3 extract -D cakeml ...')
Transformations
* transformations can now have arguments
......@@ -51,7 +53,8 @@ Tools
* deprecated `.why` file extension; use `.mlw` instead
Provers
* deprecated the `why3` Coq tactic
* removed the `why3` Coq tactic :x:
* dropped support for Coq 8.4 :x:
Version 0.88.3, January 11, 2018
--------------------------------
......@@ -124,10 +127,10 @@ Plugins
Provers
* support for Isabelle 2017 (released Oct 2017)
* discarded support for Isabelle 2016 (2016-1 still supported) :x:
* dropped support for Isabelle 2016 (2016-1 still supported) :x:
* support for Coq 8.6.1 (released Jul 25, 2017)
* tentative support for Coq 8.7
* discarded tactic support for Coq 8.4 (proofs still supported) :x:
* dropped tactic support for Coq 8.4 (proofs still supported) :x:
* support for CVC4 1.5 (released Jul 10, 2017)
* support for E 2.0 (released Jul 4, 2017)
* support for E 1.9.1 (release Aug 31, 2016)
......@@ -143,7 +146,7 @@ Provers
* support for Alt-Ergo 1.30 (released Nov 21, 2016)
* support for Coq 8.6 (released Dec 8, 2016)
* support for Gappa 1.3 (released Jul 20, 2016)
* discarded support for Isabelle 2015 :x:
* dropped support for Isabelle 2015 :x:
* support for Isabelle 2016-1 (released Dec 2016)
* support for Z3 4.5.0 (released Nov 8, 2016)
......@@ -193,13 +196,13 @@ Encoding
format is direct :x:
Provers
* discarded support for Alt-Ergo versions older than 0.95.2 :x:
* dropped support for Alt-Ergo versions older than 0.95.2 :x:
* support for Alt-Ergo 1.01 (released Feb 16, 2016) and
non-free versions 1.10 and 1.20
* support for Coq 8.4pl6 (released Apr 9, 2015)
* support for Coq 8.5 (released Jan 21, 2016)
* support for Gappa 1.2.0 (released May 19, 2015)
* discarded support for Isabelle 2014 :x:
* dropped support for Isabelle 2014 :x:
* support for Isabelle 2015 (released May 25, 2015) and
Isabelle 2016 (released Feb 17, 2016)
* support for Z3 4.4.0 (released Apr 29, 2015) and
......@@ -377,7 +380,7 @@ Provers
* new version of prover: Coq 8.4pl3
* new version of prover: Gappa 1.1.0
* new version of prover: E prover 1.8
* Coq 8.3 is no longer supported :x:
* dropped support for Coq 8.3 :x:
* improved support for Isabelle2013-2
* fixed Coq printer (former Coq proofs may have to be updated, with
extra qualification of imported symbols) :x:
......
This diff is collapsed.
......@@ -161,25 +161,31 @@
* The next commit : add +git to the version in file Version
* prepare the OPAM package
- update opam/why3-base/url: url and checksum of why-0.86.tar.gz
(use "md5sum distrib/why3-0.86.tar.gz")
- update opam/why3-base/descr and opam/why3/descr if necessary
- update opam/why3-base/opam with correct dependencies
- update opam/why3/opam with the dependency on why3-base
- test with "opam pin add why3 --kind=git .../why3/.git"
(it runs "opam install why3")
- update why3{,-ide,-coq}.opam/descr if necessary
- update why3{,-ide,-coq}.opam/opam with correct dependencies on external packages
* upload the OPAM package
- clone https://github.com/ocaml/opam-repository
- clone https://github.com/ocaml/opam-repository if not already done:
git clone git@github.com:.../opam-repository.git
cd opam-repository/
git remote add opam https://github.com/ocaml/opam-repository.git
opam repository add --kind=git local .
- reinitialize the repository if not fresh:
git fetch opam
git reset --hard opam/master
git push
- cd packages/why3-base; cp -r .../opam/why3-base why3-base.0.86
- cd packages/why3; cp -r .../opam/why3 why3.0.86
- create version directories:
cp -r .../why3.opam packages/why3/why3.1.0.0
cp -r .../why3-ide.opam packages/why3-ide/why3-ide.1.0.0
cp -r .../why3-coq.opam why3-coq/why3-coq.1.0.0
- update why3{-ide,-coq}.1.0.0/opam with the dependency on why3
- create why3/why3.1.0.0/url: url and checksum of why-1.0.0.tar.gz
md5sum .../distrib/why3-1.0.0.tar.gz
cp why3/why3.1.0.0/url why3-ide/why3-ide.1.0.0/url
cp why3/why3.1.0.0/url why3-coq/why3-coq.1.0.0/url
- test opam files:
opam update local
opam install why3 why3-ide why3-coq
- commit and push
- make a pull request on github
......@@ -216,9 +222,6 @@ and no epsilon
bien-fondee statiquement, generer une obligation de preuve
(feature wish de F Besson)
* Coq tactic
** ajout de bases de hint
* replayer
** deplacer option -bench dans une commande de why3session
......
......@@ -62,6 +62,7 @@ drivers () {
for f in $1/*.drv; do
if [[ $f == drivers/ocaml*.drv ]]; then continue; fi
if [[ $f == drivers/c.drv ]]; then continue; fi
if [[ $f == drivers/cakeml.drv ]]; then continue; fi
printf " $f... "
# running Why
if ! echo "theory Test goal G : 1=2 end" | $pgm -F whyml --driver $f - > /dev/null; then
......@@ -77,14 +78,13 @@ valid_goals () {
pgm="bin/why3prove$suffix"
for f in $1/*.mlw; do
printf " $f... "
if $pgm -t 10 -P alt-ergo $f | grep -q -v Valid; then
echo "valid test $f failed!"
echo "$pgm -P alt-ergo $f"
$pgm -t 10 -P alt-ergo $f
if ! $pgm -t 15 -P alt-ergo $f > /dev/null 2>&1; then
echo "FAILED!"
echo "$pgm -t 15 -P alt-ergo $f"
$pgm -t 15 -P alt-ergo $f
exit 1
else
echo "ok"
fi
echo "ok"
done
}
......@@ -269,8 +269,8 @@ goods examples/avl "-L examples/avl"
goods examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication"
goods examples/double_wp "-L examples/double_wp"
goods examples/ring_decision "-L examples/ring_decision"
goods examples/multiprecision "-L examples/multiprecision"
goods examples/in_progress
goods examples/in_progress/multiprecision "-L examples/in_progress/multiprecision"
echo ""
echo "=== Checking replay (no prover) ==="
......@@ -287,9 +287,10 @@ replay examples/WP_revisited --merging-only
replay examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps --merging-only"
replay examples/bitvectors "-L examples/bitvectors --merging-only"
replay examples/avl "-L examples/avl --merging-only"
#replay examples/to_port/verifythis_2016_matrix_multiplication "-L examples/to_port/verifythis_2016_matrix_multiplication --merging-only"
replay examples/verifythis_2016_matrix_multiplication "-L examples/verifythis_2016_matrix_multiplication --merging-only"
replay examples/double_wp "-L examples/double_wp --merging-only"
replay examples/ring_decision "-L examples/ring_decision --merging-only"
replay examples/multiprecision "-L examples/multiprecision --merging-only"
#replay examples/in_progress --merging-only
#replay examples/in_progress/multiprecision "-L examples/in_progress/multiprecision --merging-only"
echo ""
......