Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 30f07218 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'next' into new_ide

parents 6617fc24 f0929e1c
......@@ -59,14 +59,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
}
......
......@@ -33,5 +33,5 @@ else
echo "Coq realizations OK"
fi
rm -r $TMPREAL
rm -rf $TMPREAL
exit $res
......@@ -528,8 +528,7 @@ compile_time_support = true
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
version_ok = "8.7.1"
version_ok = "8.7.0"
version_ok = "^8\.7\.[0-2]$"
version_ok = "8.6.1"
version_ok = "8.6"
command = "%e -I %l/coq-tactic -R %l/coq-tactic Why3 -R %l/coq Why3 -l %f"
......
......@@ -31,7 +31,7 @@ void parse_options(int argc, char **argv) {
};
while (1) {
int option_index = 0;
char c = 0;
int c = 0;
c = getopt_long (argc, argv, "j:s:",
long_options, &option_index);
/* Detect the end of the options. */
......
......@@ -240,6 +240,8 @@ let output_task drv fname _tname th task dir =
Driver.print_task drv (formatter_of_out_channel cout) task;
close_out cout
let unproved = ref false
let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
let limit =
{ Call_provers.empty_limit with
......@@ -252,7 +254,8 @@ let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
let res = Call_provers.wait_on_call call in
printf "%s %s %s : %a@." fname tname
(task_goal task).Decl.pr_name.Ident.id_string
Call_provers.print_prover_result res
Call_provers.print_prover_result res;
if res.Call_provers.pr_answer <> Call_provers.Valid then unproved := true
| None, None ->
Driver.print_task ~cntexample:!opt_cntexmp drv std_formatter task
| Some dir, _ -> output_task drv fname tname th task dir
......@@ -351,7 +354,8 @@ let () =
try
let load (f,ef) = load_driver (Whyconf.get_main config) env f ef in
let drv = Opt.map load !opt_driver in
Queue.iter (do_input env drv) opt_queue
Queue.iter (do_input env drv) opt_queue;
if !unproved then exit 1
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment