Commit 7311bbdc authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'computer_division_for_master' into 'master'

Add part of nightly-bench in CI

See merge request !14
parents 5d7c83c6 662d5c1c
stages:
- build
- test
- nightly
- deploy
.build_template: &build_definition
......@@ -41,7 +42,8 @@ build-4.07.0:
bench:
stage: test
variables:
COMPILER: system
COMPILER: 4.04.0
OPAM_PACKAGES: alt-ergo.2.0.0
script:
- misc/ci-docker.sh misc/ci-local.sh bench ide
......@@ -81,12 +83,21 @@ bench-4.07.0:
full:
stage: test
variables:
COMPILER: system
DEBIAN_PACKAGES: hevea rubber texlive-latex-extra
OPAM_PACKAGES: coq-flocq.2.6.1 js_of_ocaml-ppx
COMPILER: 4.04.0
DEBIAN_PACKAGES: hevea rubber texlive-latex-extra lmodern texlive-fonts-recommended
OPAM_PACKAGES: coq-flocq.2.6.1 js_of_ocaml-ppx alt-ergo.2.0.0
script:
- misc/ci-docker.sh misc/ci-local.sh bench ide doc
nightly-bench:
stage: nightly
variables:
COMPILER: 4.04.0
DEBIAN_PACKAGES: cvc3 spass
OPAM_PACKAGES: alt-ergo.2.0.0 zenon.0.8.0 coq.8.7.1 coq-flocq.2.6.1
script:
- misc/ci-docker.sh misc/ci-local.sh nightly-bench-reduced
opam:
stage: build
variables:
......
counting_sort
leftist_heap
binary_sort
mergesort_array
#!/bin/sh
#!/bin/sh -eu
# regression tests for why3
REPLAYOPT=""
REGTESTS_MODE=""
while test $# != 0; do
case "$1" in
......@@ -15,6 +16,9 @@ case "$1" in
REPLAYOPT="$REPLAYOPT --prover $2"
shift
;;
"--reduced-mode")
REGTESTS_MODE="REDUCED"
;;
*)
echo "$0: Unknown option '$1'"
exit 2
......@@ -39,12 +43,24 @@ export shapes=""
run_dir () {
for f in `ls $1/*/why3session.xml`; do
if [ "$REGTESTS_MODE" = "REDUCED" ]; then
if [ -f $1/reduced_regtests.list ]; then
LIST=`sed $1/reduced_regtests.list -e "s&.*&$1/\0/why3session.xml&"`
else
LIST=
fi
else
LIST=`ls $1/*/why3session.xml`
fi
for f in $LIST; do
d=`dirname $f`
printf "Replaying $d ... "
../bin/why3replay.opt -q $REPLAYOPT $2 $d 2> $TMPERR > $TMP
ret=$?
if test "$ret" != "0" ; then
if ../bin/why3replay.opt -q $REPLAYOPT $2 $d 2> $TMPERR > $TMP ; then
printf "OK"
cat $TMP $TMPERR
success=`expr $success + 1`
else
ret=$?
printf "FAILED (ret code=$ret):"
out=`head -1 $TMP`
if test -z "$out" ; then
......@@ -54,10 +70,6 @@ run_dir () {
cat $TMP
fi
res=1
else
printf "OK"
cat $TMP $TMPERR
success=`expr $success + 1`
fi
total=`expr $total + 1`
done
......@@ -67,13 +79,13 @@ run_dir () {
echo "=== Programs already ported === MUST REPLAY AND ALL GOALS PROVED ==="
echo ""
run_dir .
run_dir . ""
run_dir double_wp "-L double_wp"
run_dir avl "-L avl"
run_dir foveoos11-cm
run_dir foveoos11-cm ""
run_dir vacid_0_binary_heaps "-L vacid_0_binary_heaps"
run_dir verifythis_2016_matrix_multiplication "-L verifythis_2016_matrix_multiplication"
run_dir WP_revisited
run_dir WP_revisited ""
run_dir prover "-L prover --debug ignore_unused_vars"
run_dir multiprecision "-L multiprecision"
echo ""
......
FROM ocaml/ocaml:debian-stable
ARG debian_version=stable
FROM ocaml/ocaml:debian-$debian_version
# install dependencies
RUN apt-get update -yq && apt-get upgrade -yq --with-new-pkgs --auto-remove
RUN apt-get update -yq && apt-get upgrade -yq --with-new-pkgs --auto-remove && apt-get install -yq --no-install-recommends wget libgmp-dev gtk+-2.0 libgtksourceview2.0-dev gnome-themes-standard libcanberra-gtk-module opam xvfb unzip build-essential autoconf automake
ARG debian_packages
RUN apt-get update
RUN apt-get install -y wget libgmp-dev gtk+-2.0 libgtksourceview2.0-dev gnome-themes-standard libcanberra-gtk-module opam xvfb
RUN apt-get install -y $debian_packages
RUN apt-get update -yq && apt-get upgrade -yq --with-new-pkgs --auto-remove && apt-get install -yq --no-install-recommends $debian_packages
RUN apt-get clean
# install provers
## CVC4 1.5
RUN wget --quiet http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.5-x86_64-linux-opt
RUN chmod a+x cvc4-1.5-x86_64-linux-opt
RUN cp cvc4-1.5-x86_64-linux-opt /usr/local/bin/cvc4-1.5
## CVC4 1.4
RUN wget --quiet http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.4-x86_64-linux-opt
RUN chmod a+x cvc4-1.4-x86_64-linux-opt
RUN cp cvc4-1.4-x86_64-linux-opt /usr/local/bin/cvc4-1.4
## Z3
RUN wget --quiet https://github.com/Z3Prover/z3/releases/download/z3-4.6.0/z3-4.6.0-x64-debian-8.10.zip
RUN unzip z3-4.6.0-x64-debian-8.10.zip
RUN cp z3-4.6.0-x64-debian-8.10/bin/z3 /usr/local/bin/z3-4.6.0
# create user
RUN sudo adduser --disabled-password --gecos '' why3
USER why3
......@@ -16,7 +31,11 @@ WORKDIR /home/why3
ARG compiler=system
RUN opam init -a -y -j1 --compiler=$compiler
RUN opam repository add coq-released https://coq.inria.fr/opam/released
RUN opam install -y depext
ARG opam_packages
RUN opam depext --dry-run menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo
RUN opam install -y menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo
RUN test -z "$opam_packages" || opam depext --dry-run $opam_packages
RUN test -z "$opam_packages" || opam install -y $opam_packages
[uninstalled_prover coq85]
name = "Coq"
version = "8.5"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "@COQVER@"
[uninstalled_prover coq86]
name = "Coq"
version = "8.6"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "@COQVER@"
[uninstalled_prover coq861]
name = "Coq"
version = "8.6.1"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "@COQVER@"
[uninstalled_prover coq872]
name = "Coq"
version = "8.7.2"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "@COQVER@"
[uninstalled_prover Alt-Ergo1.01]
name = "Alt-Ergo"
version = "1.01"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Alt-Ergo"
target_version = "2.2.0"
[uninstalled_prover Alt-Ergo1.30]
name = "Alt-Ergo"
version = "1.30"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Alt-Ergo"
target_version = "2.2.0"
[uninstalled_prover altergo_95_2]
name = "Alt-Ergo"
version = "0.95.2"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Alt-Ergo"
target_version = "2.2.0"
[uninstalled_prover altergo_99_1]
name = "Alt-Ergo"
version = "0.99.1"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Alt-Ergo"
target_version = "2.2.0"
[uninstalled_prover altergo_1_01]
name = "Alt-Ergo"
version = "0.1.01"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Alt-Ergo"
target_version = "2.2.0"
[uninstalled_prover altergo_2_0_0]
name = "Alt-Ergo"
version = "2.0.0"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "Alt-Ergo"
target_version = "2.2.0"
[uninstalled_prover cvc3_2_2]
name = "CVC3"
version = "2.2"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "CVC3"
target_version = "2.4.1"
[uninstalled_prover cvc4_1_2]
name = "CVC4"
version = "1.2"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "CVC4"
target_version = "1.4"
[uninstalled_prover cvc4_1_3]
name = "CVC4"
version = "1.3"
alternative = ""
policy = "upgrade"
target_alternative = ""
target_name = "CVC4"
target_version = "1.4"
[uninstalled_prover Z33.2]
name = "Z3"
version = "3.2"
alternative = ""
policy = "upgrade"
target_name = "Z3"
target_version = "4.6.0"
target_alternative = ""
[uninstalled_prover Z34.3.2]
name = "Z3"
version = "4.3.2"
alternative = ""
policy = "upgrade"
target_name = "Z3"
target_version = "4.6.0"
target_alternative = ""
[uninstalled_prover Z34.4.0]
name = "Z3"
version = "4.4.0"
alternative = ""
policy = "upgrade"
target_name = "Z3"
target_version = "4.6.0"
target_alternative = ""
[uninstalled_prover Z34.4.1_noBV]
name = "Z3"
version = "4.4.1"
alternative = "noBV"
policy = "upgrade"
target_name = "Z3"
target_version = "4.6.0"
target_alternative = "noBV"
[uninstalled_prover Z34.4.1]
name = "Z3"
version = "4.4.1"
alternative = ""
policy = "upgrade"
target_name = "Z3"
target_version = "4.6.0"
target_alternative = ""
[uninstalled_prover Z34.5.0]
name = "Z3"
version = "4.5.0"
alternative = ""
policy = "upgrade"
target_name = "Z3"
target_version = "4.6.0"
target_alternative = ""
[uninstalled_prover Eprover1.8-001]
name = "Eprover"
version = "1.8-001"
alternative = ""
policy = "remove"
[uninstalled_prover Eprover1.9.1-001]
name = "Eprover"
version = "1.9.1-001"
alternative = ""
policy = "remove"
[uninstalled_prover Eprover2.0]
name = "Eprover"
version = "2.0"
alternative = ""
policy = "remove"
[uninstalled_prover Gappa1.3.0]
name = "Gappa"
version = "1.3.0"
alternative = ""
policy = "remove"
[uninstalled_prover MetiTarski2.4]
name = "MetiTarski"
version = "2.4"
alternative = ""
policy = "remove"
[uninstalled_prover PolyPaver0.3]
name = "PolyPaver"
version = "0.3"
alternative = ""
policy = "remove"
[uninstalled_prover Vampire0.6]
name = "Vampire"
version = "0.6"
alternative = ""
policy = "remove"
[uninstalled_prover veriT201410]
name = "veriT"
version = "201410"
alternative = ""
policy = "remove"
......@@ -2,13 +2,22 @@
set -e
if test -z "$DEBIAN_VERSION"; then
DEBIAN_VERSION="stable"
fi
autoconf && (automake --add-missing 2> /dev/null || true)
if test -n "$DEBIAN_PACKAGES" -o -n "$OPAM_PACKAGES"; then
IMAGE=bench-image-$COMPILER--$(echo $DEBIAN_PACKAGES | sed -e 's/ /--/g')--$(echo $OPAM_PACKAGES | sed -e 's/ /--/g')
else
IMAGE=bench-image-$COMPILER
IMAGE=bench-image-$COMPILER-$DEBIAN_VERSION
if test -n "$DEBIAN_PACKAGES"; then
IMAGE=$IMAGE--$(echo $DEBIAN_PACKAGES | sed -e 's/ /--/g')
fi
docker build -t $IMAGE --force-rm -f misc/Dockerfile.init --build-arg compiler=$COMPILER --build-arg debian_packages="$DEBIAN_PACKAGES" --build-arg opam_packages="$OPAM_PACKAGES" .
if test -n "$OPAM_PACKAGES"; then
IMAGE=$IMAGE--$(echo $OPAM_PACKAGES | sed -e 's/ /--/g')
fi
docker build -t $IMAGE --force-rm -f misc/Dockerfile.init --build-arg debian_version="$DEBIAN_VERSION" --build-arg compiler=$COMPILER --build-arg debian_packages="$DEBIAN_PACKAGES" --build-arg opam_packages="$OPAM_PACKAGES" .
CID=$(docker create --rm -i -w /home/why3/why3 $IMAGE /bin/sh)
docker start $CID
docker cp . $CID:/home/why3/why3
......
......@@ -34,6 +34,13 @@ do
doc)
make doc
;;
nightly-bench-reduced)
bin/why3config --detect-provers
bench/ce-bench
sed -i why3.conf -e "s/running_provers_max = [0-9]*/running_provers_max = 1/"
cat misc/bench-few-provers-why3-conf >> why3.conf
examples/regtests.sh --reduced-mode
;;
esac
shift
done
......@@ -14,15 +14,17 @@ esac
GITBRANCH=`git rev-parse --abbrev-ref HEAD`
REPORTDIR=$PWD/../why3-reports-$GITBRANCH
if ! test -e "$REPORTDIR"; then
echo "directory '$REPORTDIR' for reports does not exist, aborting."
exit 2
fi
OUT=$REPORTDIR/nightly-bench.out
PREVIOUS=$REPORTDIR/nightly-bench.previous
DIFF=$REPORTDIR/nightly-bench.diff
REPORT=$REPORTDIR/nightly-bench.report
if ! test -e "$REPORTDIR"; then
echo "directory '$REPORTDIR' for reports does not exist, creating."
mkdir "$REPORTDIR"
touch "$PREVIOUS"
fi
DATE=`date --utc +%Y-%m-%d`
SUBJECT="Why3 [$GITBRANCH] bench : "
......@@ -84,45 +86,7 @@ perl -pi -e 's/running_provers_max = 2/running_provers_max = 4/' why3.conf
COQVER=$(bin/why3 --list-provers | sed -n -e 's/ Coq (\?\([0-9.]\+\).*/\1/p')
echo "Coq version detected: $COQVER" >> $REPORT
if test "$COQVER" != "" ; then
cat >> why3.conf <<EOF
[uninstalled_prover coq85]
alternative = ""
name = "Coq"
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "$COQVER"
version = "8.5"
[uninstalled_prover coq86]
alternative = ""
name = "Coq"
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "$COQVER"
version = "8.6"
[uninstalled_prover coq861]
alternative = ""
name = "Coq"
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "$COQVER"
version = "8.6.1"
[uninstalled_prover coq872]
alternative = ""
name = "Coq"
policy = "upgrade"
target_alternative = ""
target_name = "Coq"
target_version = "$COQVER"
version = "8.7.2"
EOF
sed bench-coq-why3-conf -e "s/@COQVER@/$COQVER/g" >> why3.conf
fi
# run the bench
......
......@@ -117,12 +117,14 @@ type prover_upgrade_policy =
| CPU_keep
| CPU_upgrade of prover
| CPU_duplicate of prover
| CPU_remove
let print_prover_upgrade_policy fmt p =
match p with
| CPU_keep -> Format.fprintf fmt "keep"
| CPU_upgrade p -> Format.fprintf fmt "upgrade to %a" print_prover p
| CPU_duplicate p -> Format.fprintf fmt "copy to %a" print_prover p
| CPU_remove -> Format.fprintf fmt "remove"
......@@ -376,6 +378,8 @@ let set_prover_upgrade_policy prover policy (i, family) =
match policy with
| CPU_keep ->
set_string section "policy" "keep"
| CPU_remove ->
set_string section "policy" "remove"
| CPU_upgrade p ->
let section = set_string section "target_name" p.prover_name in
let section = set_string section "target_version" p.prover_version in
......@@ -470,6 +474,7 @@ let load_policy provers acc (_,section) =
try
match get_string section "policy" with
| "keep" -> Mprover.add source CPU_keep acc
| "remove" -> Mprover.add source CPU_remove acc
| "upgrade" ->
let target =
{ prover_name = get_string section "target_name";
......
......@@ -173,6 +173,7 @@ type prover_upgrade_policy =
| CPU_keep
| CPU_upgrade of prover
| CPU_duplicate of prover
| CPU_remove
val print_prover_upgrade_policy : Format.formatter -> prover_upgrade_policy -> unit
......
......@@ -1026,6 +1026,7 @@ let alternatives_frame c (notebook:GPack.notebook) =
let iter p policy =
let label =
match policy with
| CPU_remove -> Pp.sprintf_wnl "proofs with %a removed" print_prover p
| CPU_keep -> Pp.sprintf_wnl "proofs with %a kept as they are" print_prover p
| CPU_upgrade t ->
Pp.sprintf_wnl "proofs with %a moved to %a" print_prover p print_prover t
......
......@@ -1383,6 +1383,7 @@ let on_selected_row r =
| Controller_itp.InternalFailure e ->
(Pp.sprintf "internal failure: %a" Exn_printer.exn_printer e)
| Controller_itp.Uninstalled _p -> "uninstalled prover"
| Controller_itp.Removed _p -> "removed proof attempt"
| Controller_itp.UpgradeProver _p -> "upgraded prover"
in
let output_text =
......@@ -1603,6 +1604,7 @@ let image_of_pa_status ~obsolete pa =
| Controller_itp.InternalFailure _e -> !image_failure
| Controller_itp.Detached -> !image_undone (* TODO !image_detached *)
| Controller_itp.Uninstalled _p -> !image_undone (* TODO !image_uninstalled *)
| Controller_itp.Removed _p -> !image_undone (* TODO !image_removed *)
| Controller_itp.UpgradeProver _p -> !image_undone
| Controller_itp.Done r ->
let pr_answer = r.Call_provers.pr_answer in
......@@ -1695,6 +1697,7 @@ let set_status_and_time_column ?limit row =
| C.Undone -> "(undone)"
| C.Uninstalled _ -> "(uninstalled prover)"
| C.UpgradeProver _ -> "(upgraded prover)"
| C.Removed _ -> "(removed prover)"
| C.Scheduled -> "(scheduled)"
| C.Running -> "(running)"
| C.Detached -> "(detached)"
......
......@@ -31,6 +31,7 @@ type proof_attempt_status =
| InternalFailure of exn (** external proof aborted by internal error *)
| Uninstalled of Whyconf.prover (** prover is uninstalled *)
| UpgradeProver of Whyconf.prover (** prover is upgraded *)
| Removed of Whyconf.prover (** prover has been removed or upgraded *)
let print_status fmt st =
match st with
......@@ -47,6 +48,8 @@ let print_status fmt st =
fprintf fmt "Prover %a is uninstalled" Whyconf.print_prover pr
| UpgradeProver pr ->
fprintf fmt "Prover upgrade to %a" Whyconf.print_prover pr
| Removed pr ->
fprintf fmt "Prover %a removed" Whyconf.print_prover pr
type transformation_status =
| TSscheduled | TSdone of transID | TSfailed of (proofNodeID * exn)
......@@ -496,7 +499,7 @@ let schedule_proof_attempt c id pr ?save_to ~limit ~callback ~notification =
let callback panid s =
begin
match s with
| UpgradeProver _ -> ()
| UpgradeProver _ | Removed _ -> ()
| Scheduled ->
Hpan.add c.controller_running_proof_attempts panid ();
update_goal_node notification ses id
......@@ -656,7 +659,7 @@ let schedule_edition c id pr ~callback ~notification =
| Interrupted
| InternalFailure _ ->
update_goal_node notification session id
| Undone | Detached | Uninstalled _ | Scheduled -> assert false
| Undone | Detached | Uninstalled _ | Scheduled | Removed _ -> assert false
end;
callback panid s
in
......@@ -731,7 +734,7 @@ let run_strategy_on_goal
callback (STSgoto (g,pc+1));
let run_next () = exec_strategy (pc+1) strat g; false in
S.idle ~prio:0 run_next
| Undone | Detached | Uninstalled _ ->
| Undone | Detached | Uninstalled _ | Removed _ ->
(* should not happen *)
assert false
in
......@@ -910,22 +913,23 @@ let copy_paste ~notification ~callback_pa ~callback_tr c from_any to_any =
let debug_replay = Debug.register_flag "replay" ~desc:"Debug@ info@ for@ replay"
let find_prover notification c goal_id pr =
if Hprover.mem c.controller_provers pr then Some pr else
if Hprover.mem c.controller_provers pr then `Found pr else
match Whyconf.get_prover_upgrade_policy c.controller_config pr with
| exception Not_found -> None
| Whyconf.CPU_keep -> None
| exception Not_found -> `Keep
| Whyconf.CPU_keep -> `Keep
| Whyconf.CPU_upgrade new_pr ->
(* does a proof using new_pr already exists ? *)
if Hprover.mem (get_proof_attempt_ids c.controller_session goal_id) new_pr
then (* yes, then we do nothing *)
None
then (* yes, then we remove the attempt *)
`Remove
else
begin
(* we modify the prover in-place *)
Session_itp.change_prover notification c.controller_session goal_id pr new_pr;
Some new_pr
`Found new_pr
end
| Whyconf.CPU_duplicate _new_pr ->
| Whyconf.CPU_remove -> `Remove
| Whyconf.CPU_duplicate _ (* _new_pr *) ->
assert false (* TODO *)
(*
(* does a proof using new_p already exists ? *)
......@@ -946,8 +950,11 @@ let replay_proof_attempt c pr limit (parid: proofNodeID) id ~callback ~notificat
(* The replay can be done on a different machine so we need
to check more things before giving the attempt to the scheduler *)
match find_prover notification c parid pr with
| None -> callback id (Uninstalled pr)
| Some pr' ->
| `Keep -> callback id (Uninstalled pr)
| `Remove ->
remove_proof_attempt c.controller_session parid pr;
callback id (Removed pr)
| `Found pr' ->
try
if pr' <> pr then callback id (UpgradeProver pr');
let _ = get_task c.controller_session parid in
......@@ -1004,7 +1011,7 @@ let replay ~valid_only ~obsolete_only ?(use_steps=false) ?(filter=fun _ -> true)
let craft_report s id pr limits pa =
match s with
| UpgradeProver _ -> found_upgraded_prover := true
| UpgradeProver _ | Removed _ -> found_upgraded_prover := true
| Scheduled | Running -> ()
| Undone | Interrupted ->
decr count;
......@@ -1144,7 +1151,7 @@ let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_i
callback_pa paid st;
begin match st with
| UpgradeProver _ | Scheduled | Running -> ()
| Detached | Uninstalled _ -> assert false
| Detached | Uninstalled _ | Removed _ -> assert false
| Undone | Interrupted -> Debug.dprintf debug "Bisecting interrupted.@."
| InternalFailure exn ->
(* Perhaps the test can be considered false in this case? *)
......@@ -1206,7 +1213,7 @@ later on. We do has if proof fails. *)
callback_pa paid st;
begin
match st with
| UpgradeProver _ -> ()
| UpgradeProver _ | Removed _ -> ()
| Scheduled ->
Debug.dprintf
debug "[Bisect] prover on subtask is scheduled@."
......
......@@ -26,6 +26,7 @@ type proof_attempt_status =
| InternalFailure of exn (** external proof aborted by internal error *)
| Uninstalled of Whyconf.prover (** prover is uninstalled *)
| UpgradeProver of Whyconf.prover (** prover is upgraded *)
| Removed of Whyconf.prover (** prover has been removed or upgraded *)
val print_status : Format.formatter -> proof_attempt_status -> unit
......
......@@ -106,6 +106,9 @@ let convert_proof_attempt (pas: proof_attempt_status) =
| Uninstalled p ->
convert_record ["proof_attempt", String "Uninstalled";
"prover", convert_prover_to_json "prover_" p]
| Removed p ->
convert_record ["proof_attempt", String "Removed";
"prover", convert_prover_to_json "prover_" p]
| UpgradeProver p ->
convert_record ["proof_attempt", String "UpgradeProver";
"prover", convert_prover_to_json "prover_" p])
......@@ -175,6 +178,7 @@ open Whyconf
let convert_policy u =
match u with
| CPU_remove -> ["policy", String "remove"]
| CPU_keep -> ["policy", String "keep"]
| CPU_upgrade p ->
["policy", String "upgrade"] @ convert_prover "target_" p
......
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