Merge branch 'new_ide'

# Conflicts:
#	configure.in
#	src/jessie/ACSLtoWhy3.ml
#	src/jessie/register.ml

.gitignore

@@ -39,6 +39,7 @@ why3.conf
 /why3regtests.err
 /why3regtests.out
 /.merlin
+/src/jessie/.merlin
 
 # /bench/
 /bench/programs/good/booleans/

Makefile.in

@@ -2345,16 +2345,16 @@ headers:
 # myself
 #########
 
-Makefile: Makefile.in config.status
-	./config.status chmod --file $@
-
-src/jessie/Makefile: src/jessie/Makefile.in config.status
-	./config.status chmod --file $@
-
-src/config.sh: src/config.sh.in config.status
-	./config.status chmod --file $@
-
-.merlin: .merlin.in config.status
+AUTOCONF_FILES = \
+	Makefile \
+	src/jessie/Makefile \
+	src/config.sh \
+	.merlin \
+	src/jessie/.merlin \
+	lib/why3/META \
+	doc/version.tex
+
+$(AUTOCONF_FILES): %: %.in config.status
 	./config.status chmod --file $@
 
 src/util/config.ml share/Makefile.config: src/config.sh
@@ -2364,17 +2364,9 @@ src/util/config.ml share/Makefile.config: src/config.sh
 clean::
 	rm -f share/Makefile.config
 
-doc/version.tex: doc/version.tex.in config.status
-	./config.status chmod --file $@
-
 config.status: configure
 	./config.status --recheck
 
-all: lib/why3/META .merlin
-
-lib/why3/META: lib/why3/META.in config.status
-	./config.status chmod --file $@
-
 configure: configure.in Version
 	autoconf -f
 
@@ -2385,9 +2377,8 @@ configure: configure.in Version
 .PHONY: distclean
 
 distclean: clean
-	rm -f config.status config.cache config.log .merlin \
-	    Makefile src/util/config.ml doc/version.tex \
-	    src/jessie/Makefile src/config.sh lib/why3/META
+	rm -f config.status config.cache config.log \
+	    src/util/config.ml $(AUTOCONF_FILES)
 
 depend:
 	rm -f $^

configure.in

@@ -846,7 +846,7 @@ if test "$enable_pvs_libs" = yes; then
 fi
 
 #check frama-c
-FRAMAC_SUPPORTED=Aluminium
+FRAMAC_SUPPORTED=Sulfur
 if test "$enable_frama_c" = yes ; then
    AC_CHECK_PROG(FRAMAC,frama-c,frama-c,no)
    if test "$FRAMAC" = no ; then
@@ -855,20 +855,24 @@ if test "$enable_frama_c" = yes ; then
         reason_frama_c=" (frama-c not found)"
    else
       AC_MSG_CHECKING(Frama-C version)
-      FRAMAC_VERSION=`$FRAMAC -version | sed -n -e 's|\(Version: \)\?\(.*\)$|\2|p' `
+      FRAMAC_VERSION=`$FRAMAC -version | sed -n -e 's|\(Version: \)\?\(.*\)$|\2|p'`
       AC_MSG_RESULT($FRAMAC_VERSION)
       case $FRAMAC_VERSION in
          $FRAMAC_SUPPORTED-*) ;;
-         *) AC_MSG_WARN(Version $FRAMAC_VERSION not supported, version $FRAMAC_SUPPORTED required.)
+         *) AC_MSG_WARN(Version $FRAMAC_SUPPORTED required.)
             enable_frama_c=no
-            reason_frama_c=" (version Sodium required)"
+            reason_frama_c=" (version $FRAMAC_SUPPORTED required)"
             ;;
       esac
-      FRAMAC_SHARE=`$FRAMAC -print-path`
-      FRAMAC_LIBDIR=`$FRAMAC -print-libpath`
    fi
 fi
 
+if test "$enable_frama_c" = yes; then
+   FRAMAC_SHARE=`$FRAMAC -print-path`
+   FRAMAC_LIBDIR=`$FRAMAC -print-libpath`
+   FRAMAC_INCLUDE="-I $FRAMAC_LIBDIR"
+fi
+
 #Viewer for ps and pdf
 dnl AC_CHECK_PROGS(PSVIEWER,gv evince)
 dnl AC_CHECK_PROGS(PDFVIEWER,xpdf acroread evince)
@@ -968,6 +972,7 @@ AC_SUBST(FRAMAC)
 AC_SUBST(FRAMAC_VERSION)
 AC_SUBST(FRAMAC_SHARE)
 AC_SUBST(FRAMAC_LIBDIR)
+AC_SUBST(FRAMAC_INCLUDE)
 
 AC_SUBST(enable_local)
 AC_SUBST(LOCALDIR)
@@ -982,16 +987,20 @@ dnl AC_SUBST(PSVIEWER)
 dnl AC_SUBST(PDFVIEWER)
 
 # Finally create the Makefile from Makefile.in
-AC_CONFIG_FILES(Makefile src/config.sh doc/version.tex)
+AC_CONFIG_FILES(Makefile)
+AC_CONFIG_FILES(src/config.sh doc/version.tex)
 AC_CONFIG_FILES(lib/why3/META)
 AC_CONFIG_FILES(.merlin)
 AC_CONFIG_FILES(src/jessie/Makefile)
+AC_CONFIG_FILES(src/jessie/.merlin)
 AC_CONFIG_FILES(lib/coq/version lib/pvs/version)
 AC_CONFIG_COMMANDS([chmod],
-chmod a-w Makefile src/config.sh doc/version.tex;
+chmod a-w Makefile src/jessie/Makefile;
+chmod a-w src/config.sh doc/version.tex;
 chmod a-w lib/why3/META;
 chmod a-w .merlin;
 chmod a-w src/jessie/Makefile;
+chmod a-w src/jessie/.merlin;
 chmod a-w lib/coq/version lib/pvs/version;
 chmod u+x src/config.sh)
 

src/driver/whyconf.ml

@@ -118,6 +118,14 @@ type prover_upgrade_policy =
   | CPU_upgrade of prover
   | CPU_duplicate of prover
 
+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
+
+
+
 type config_prover = {
   prover  : prover;
   command : string;

src/driver/whyconf.mli

@@ -174,6 +174,8 @@ type prover_upgrade_policy =
   | CPU_upgrade of prover
   | CPU_duplicate of prover
 
+val print_prover_upgrade_policy : Format.formatter -> prover_upgrade_policy -> unit
+
 val set_prover_upgrade_policy :
   config -> prover -> prover_upgrade_policy -> config
 (** [set_prover_upgrade c p cpu] sets or updates the policy to follow if the

src/ide/gconfig.ml

@@ -1030,7 +1030,7 @@ let alternatives_frame c (notebook:GPack.notebook) =
   in
   let remove button p () =
     button#destroy ();
-    c.config <- set_policies c.config (Mprover.remove p (get_policies c.config))
+    c.config <- set_policies c.config (Mprover.remove p (get_policies c.config));
   in
   let iter p policy =
     let label =
@@ -1195,7 +1195,7 @@ let run_auto_detection gconfig =
 
 (*let () = Debug.dprintf debug "[config] end of configuration initialization@."*)
 
-let uninstalled_prover_dialog c unknown =
+let uninstalled_prover_dialog ~callback c unknown =
   let others,names,versions =
     Whyconf.unknown_to_known_provers
       (Whyconf.get_provers c.config) unknown
@@ -1219,13 +1219,26 @@ let uninstalled_prover_dialog c unknown =
     (* header *)
     let hb = GPack.hbox ~packing:vbox#add () in
     let _ = GMisc.image ~stock:`DIALOG_WARNING ~packing:hb#add () in
-    let _ =
+    let (_:GMisc.label) =
       let text =
         Pp.sprintf "The prover %a is not installed"
-          Whyconf.print_prover unknown
+                   Whyconf.print_prover unknown
       in
       GMisc.label ~ypad:20 ~text ~xalign:0.5 ~packing:hb#add ()
     in
+    let (_:GMisc.label) =
+      let text =
+        "WARNING: this policy will not be taken into account immediately \
+         but only if you replay again the proofs."
+      in
+      GMisc.label ~text ~line_wrap:true ~packing:vbox#add ()
+    in
+    let (_:GMisc.label) =
+      let text =
+        "WARNING: do not forget to save preferences to keep this policy in future sessions"
+      in
+      GMisc.label ~text ~line_wrap:true ~packing:vbox#add ()
+    in
     (* choices *)
     let vbox_pack =
       vbox#pack ~fill:true ~expand:true ?from:None ?padding:None
@@ -1302,6 +1315,7 @@ let uninstalled_prover_dialog c unknown =
         | _ -> assert false
     in
     c.config <- set_prover_upgrade_policy c.config unknown policy;
+    let () = callback unknown policy in
     ()
 
 

src/ide/gconfig.mli

@@ -117,6 +117,7 @@ val show_about_window : unit -> unit
 val preferences : t -> unit
 
 val uninstalled_prover_dialog :
+  callback: (Whyconf.prover -> Whyconf.prover_upgrade_policy -> unit) ->
   t -> Whyconf.prover -> unit
 
 

src/ide/why3ide.ml

@@ -2193,9 +2193,13 @@ let check_uninstalled_prover =
   let uninstalled_prover_seen = Whyconf.Hprover.create 3 in
   fun p ->
   if not (Whyconf.Hprover.mem uninstalled_prover_seen p)
-  then begin
+  then
+    begin
       Whyconf.Hprover.add uninstalled_prover_seen p ();
-      uninstalled_prover_dialog gconfig p
+      let callback p u =
+        send_request (Set_prover_policy(p,u))
+      in
+      uninstalled_prover_dialog ~callback gconfig p
     end
 
 let treat_notification n =

src/jessie/.merlin.in

+REC
+
+FLG @FRAMAC_INCLUDE@

src/jessie/ACSLtoWhy3.ml

@@ -75,7 +75,7 @@ let () =
 
 open Cil_types
 open Why3
-
+open Wstdlib
 
 
 
@@ -207,7 +207,7 @@ let bv32_module =
 let bv32_type : Why3.Ity.itysymbol =
   Pmodule.ns_find_its bv32_module.Pmodule.mod_export ["t"]
 
-let bv32_to_int : Term.lsymbol = find bv32_module "to_uint"
+let bv32_to_int : Term.lsymbol = find bv32_module "t'int"
 
 let bv32_to_int_fun : Expr.rsymbol = find_rs bv32_module "to_uint"
 
@@ -385,11 +385,13 @@ let rec logic_type ty =
 let logic_constant c =
   match c with
     | Integer(_value,Some s) ->
-      let c = Literals.integer s in Number.(ConstInt { ic_negative = false; ic_abs = c})
+      let c = Literals.integer s in
+      Term.t_const (Number.(ConstInt {ic_negative = false; ic_abs = c})) Ty.ty_int
     | Integer(_value,None) ->
       Self.not_yet_implemented "logic_constant Integer None"
     | LReal { r_literal = s } ->
-      let c = Literals.floating_point s in Number.(ConstReal {rc_negative = false; rc_abs = c})
+      let c = Literals.floating_point s in
+      Term.t_const (Number.(ConstReal {rc_negative = false; rc_abs = c})) Ty.ty_real
     | (LStr _|LWStr _|LChr _|LEnum _) ->
       Self.not_yet_implemented "logic_constant"
 
@@ -441,9 +443,7 @@ let bound_vars = Hashtbl.create 257
 let create_lvar v =
   let id = Ident.id_fresh v.lv_name in
   let vs = Term.create_vsymbol id (logic_type v.lv_type) in
-(*
   Self.result "create logic variable %d" v.lv_id;
-*)
   Hashtbl.add bound_vars v.lv_id vs;
   vs
 
@@ -456,11 +456,22 @@ let get_lvar lv =
 
 let program_vars = Hashtbl.create 257
 
+(*
 let create_var v is_mutable =
 (* *)
   Self.result "create local program variable %s (%d), mutable = %b" v.vname v.vid is_mutable;
  (* *)
   Hashtbl.add program_vars v.vid is_mutable
+ *)
+
+let create_var_full v =
+  Self.result "create program variable %s (%d)" v.vname v.vid;
+  let id = Ident.id_fresh v.vname in
+  let ty,def = ctype_and_default v.vtype in
+  let def = Mlw_expr.e_app (mk_ref ty) [def] in
+  let let_defn, vs = Mlw_expr.create_let_pv_defn id def in
+  Hashtbl.add program_vars v.vid (vs,true,ty);
+  let_defn,vs
 
 let global_vars : (int,Ity.pvsymbol) Hashtbl.t = Hashtbl.create 257
 
@@ -608,6 +619,10 @@ let rec term_node ~label t lvm old =
     | TLval lv -> tlval ~label lv lvm old
     | TBinOp (op, t1, t2) -> bin (term ~label t1 lvm old) op (term ~label t2 lvm old)
     | TUnOp (op, t) -> unary op (term ~label t lvm old)
+    | TConst cst -> logic_constant cst
+    | TLval lv -> tlval ~label lv
+    | TBinOp (op, t1, t2) -> bin (term ~label t1) op (term ~label t2)
+    | TUnOp (op, t) -> unary op (term ~label t)
     | TCastE (_, _) -> Self.not_yet_implemented "term_node TCastE"
     | Tapp (li, labels, args) ->
       begin
@@ -629,11 +644,12 @@ let rec term_node ~label t lvm old =
     | Tat (t, lab) ->
       begin
         match lab with
-          | LogicLabel(None, "Here") -> snd (term ~label:Here t lvm old)
-          | LogicLabel(None, "Old") -> snd (term ~label:Old t lvm old)
-          | LogicLabel(None, lab) -> snd (term ~label:(At lab) t lvm old)
-          | LogicLabel(Some _, _lab) ->
-            Self.not_yet_implemented "term_node Tat/LogicLabel/Some"
+          | BuiltinLabel Cil_types.Here -> snd (term ~label:Here t lvm old)
+          | BuiltinLabel Cil_types.Old -> snd (term ~label:Old t lvm old)
+          | BuiltinLabel _ ->
+            Self.not_yet_implemented "term_node Tat/BuiltinLabel/other"
+          | FormalLabel _ ->
+            Self.not_yet_implemented "term_node Tat/FormalLabel"
           | StmtLabel _ ->
             Self.not_yet_implemented "term_node Tat/StmtLabel"
       end
@@ -897,6 +913,7 @@ let rec logic_decl ~in_axiomatic a _loc (theories,decls) =
       let targs =
         List.map (fun s -> Ty.create_tvsymbol (Ident.id_fresh s)) lt.lt_params
       in
+(*
       begin
         match lt.lt_def with
         | None ->
@@ -907,6 +924,30 @@ let rec logic_decl ~in_axiomatic a _loc (theories,decls) =
            (theories,d::decls)
         | Some _ -> Self.not_yet_implemented "logic_decl Dtype non abstract"
       end
+||||||| merged common ancestors
+      let tdef = match lt.lt_def with
+          | None -> None
+          | Some _ -> Self.not_yet_implemented "logic_decl Dtype non abstract"
+      in
+      let ts =
+        Ty.create_tysymbol
+          (Ident.id_user lt.lt_name (Loc.extract loc)) targs tdef
+      in
+      Hashtbl.add logic_types lt.lt_name ts;
+      let d = Decl.create_ty_decl ts in
+      (theories,d::decls)
+ *)
+      let tdef = match lt.lt_def with
+          | None -> Ty.NoDef
+          | Some _ -> Self.not_yet_implemented "logic_decl Dtype non abstract"
+      in
+      let ts =
+        Ty.create_tysymbol
+          (Ident.id_user lt.lt_name (Loc.extract loc)) targs tdef
+      in
+      Hashtbl.add logic_types lt.lt_name ts;
+      let d = Decl.create_ty_decl ts in
+      (theories,d::decls)
     | Dfun_or_pred (li, _loc) ->
       begin
         match li.l_labels with
@@ -931,7 +972,7 @@ let rec logic_decl ~in_axiomatic a _loc (theories,decls) =
           | _ ->
             Self.not_yet_implemented "Dfun_or_pred with labels"
       end
-    | Dlemma(name,is_axiom,labels,vars,p,loc) ->
+    | Dlemma(name,is_axiom,labels,vars,p,attrs,loc) ->
       begin
         match labels,vars with
           | [],[] ->
@@ -948,7 +989,7 @@ let rec logic_decl ~in_axiomatic a _loc (theories,decls) =
           | _ ->
             Self.not_yet_implemented "Dlemma with labels or vars"
       end
-    | Daxiomatic (name, decls', loc) ->
+    | Daxiomatic (name, decls', attrs, loc) ->
       let theories =
         add_decls_as_module theories
           (Ident.id_fresh global_logic_decls_theory_name) decls
@@ -964,15 +1005,14 @@ let rec logic_decl ~in_axiomatic a _loc (theories,decls) =
         add_decls_as_module theories (Ident.id_user name (Loc.extract loc)) decls''
       in
       (theories,[])
-    | Dvolatile (_, _, _, _)
+    | Dvolatile (_, _, _, _, _)
     | Dinvariant (_, _)
     | Dtype_annot (_, _)
     | Dmodel_annot (_, _)
-    | Dcustom_annot (_, _, _)
+    | Dcustom_annot (_, _, _, _)
         -> Self.not_yet_implemented "logic_decl"
 
-let identified_proposition p =
-  { name = p.ip_name; loc = p.ip_loc; content = p.ip_content }
+let identified_proposition p = p.ip_content
 
 
 
@@ -1011,6 +1051,8 @@ let annot a e =
     Self.not_yet_implemented "annot AAllocation"
   | APragma _ ->
     Self.not_yet_implemented "annot APragma"
+  | AExtended _ ->
+    Self.not_yet_implemented "annot AExtended"
 
 let loop_annot a =
   let inv,var =
@@ -1036,8 +1078,10 @@ let loop_annot a =
       | AAllocation _ ->
         Self.not_yet_implemented "loop_annot AAllocation"
       | APragma _ ->
-        Self.not_yet_implemented "loop_annot APragma")
-    ([], []) a
+        Self.not_yet_implemented "loop_annot APragma"
+      | AExtended _ ->
+        Self.not_yet_implemented "loop_annot AExtended")
+      ([], []) a
   in
   (fun lvm old ->
    List.rev_map
@@ -1254,6 +1298,8 @@ let instr denv i =
   | Skip _loc -> e_void
   | Code_annot (_, _) ->
     Self.not_yet_implemented "instr Code_annot"
+  | Local_init _ ->
+    Self.not_yet_implemented "instr Local_init"
 
 let exc_break =
   Ity.create_xsymbol (Ident.id_fresh "Break") Ity.ity_unit

src/jessie/Makefile.in

@@ -27,7 +27,7 @@ Jessie3.cmx: $(addsuffix .cmx, $(MODULES))
 	ocamlopt.opt $(FLAGS) $(INCLUDE) -o $@ -pack $^
 
 Jessie3.cmxs: Jessie3.cmx
-	ocamlopt.opt -shared $(FLAGS) $(INCLUDE) -o $@ $(addsuffix .cmx, @MENHIRLIB@) $(addsuffix .cmxa, @ZIPLIB@) $(WHYLIB)/why3.cmxa $^
+	ocamlopt.opt -shared $(FLAGS) $(INCLUDE) -o $@ nums.cmxa $(addsuffix .cmx, @MENHIRLIB@) $(addsuffix .cmxa, @ZIPLIB@) $(WHYLIB)/why3.cmxa $^
 
 %.cmi: %.mli
 	ocamlc.opt $(FLAGS) $(INCLUDE) -c $^

src/jessie/register.ml

@@ -32,6 +32,7 @@ let limit = Call_provers.{ limit_time = 1 ;
                            limit_steps = -1;}
 
 let run_on_task fmt prover prover_driver t =
+  let limit = { Call_provers.empty_limit with Call_provers.limit_time = 3 } in
   let result =
     Call_provers.wait_on_call
       (Why3.Driver.prove_task
@@ -58,7 +59,7 @@ let get_prover config env acc (short, name) =
   (* loading the driver *)
   let driver : Why3.Driver.driver =
     try
-      Why3.Driver.load_driver env prover.Whyconf.driver []
+      Why3.Whyconf.load_driver (Why3.Whyconf.get_main config) env prover.Whyconf.driver []
     with e ->
       ACSLtoWhy3.Self.fatal "Failed to load driver for %s: %a@." name
         Exn_printer.exn_printer e
@@ -74,9 +75,9 @@ let process () =
       List.fold_left
         (get_prover ACSLtoWhy3.config ACSLtoWhy3.env)
         []
-        [ "Z441", "Z3,4.4.1,";
-          "C414", "CVC4,1.4,";
-          "A101", "Alt-Ergo,1.01,";
+        [ "C415", "CVC4,1.5,";
+          "Z460", "Z3,4.6.0,";
+          "A220", "Alt-Ergo,2.2.0,";
         ]
     with e ->
       ACSLtoWhy3.Self.fatal "Exception raised when loading prover drivers:@ %a"

src/session/controller_itp.ml

@@ -78,7 +78,7 @@ let print_strategy_status fmt st =
 
 type controller =
   { mutable controller_session: Session_itp.session;
-    controller_config : Whyconf.config;
+    mutable controller_config : Whyconf.config;
     mutable controller_env: Env.env;
     controller_provers:
       (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
@@ -92,6 +92,9 @@ let set_session_max_tasks n =
   session_max_tasks := n;
   Prove_client.set_max_running_provers n
 
+let set_session_prover_upgrade_policy c p u =
+  c.controller_config <- Whyconf.set_prover_upgrade_policy c.controller_config p u
+
 let load_drivers c =
   let env = c.controller_env in
   let config = c.controller_config in

src/session/controller_itp.mli

@@ -85,7 +85,7 @@ end
 
 type controller = private
   { mutable controller_session : Session_itp.session;
-    controller_config : Whyconf.config;
+    mutable controller_config : Whyconf.config;
     mutable controller_env : Env.env;
     controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
     controller_strategies : (string * string * string * Strategy.instruction array) Wstdlib.Hstr.t;
@@ -101,6 +101,9 @@ val set_session_max_tasks : int -> unit
 (** sets the maximum number of proof tasks that can be running at the
     same time. Initially set to 1. *)
 
+val set_session_prover_upgrade_policy :
+  controller -> Whyconf.prover -> Whyconf.prover_upgrade_policy -> unit
+
 
 val print_session : Format.formatter -> controller -> unit
 

src/session/itp_communication.ml

@@ -10,7 +10,6 @@
 (********************************************************************)
 
 (* Information that the IDE may want to have *)
-type prover = string
 type transformation = (string * string)
 type strategy = string
 
@@ -109,6 +108,7 @@ type ide_request =
   | Command_req             of node_ID * string
   | Add_file_req            of string
   | Set_config_param        of string * int
+  | Set_prover_policy       of Whyconf.prover * Whyconf.prover_upgrade_policy
   | Get_file_contents       of string
   | Get_task                of node_ID * bool * bool
   | Remove_subtree          of node_ID
@@ -127,7 +127,7 @@ let modify_session (r: ide_request) =
   | Command_req _ | Add_file_req _ | Remove_subtree _ | Copy_paste _
   | Reload_req -> true
 
-  | Set_config_param _ | Get_file_contents _
+  | Set_config_param _ | Set_prover_policy _ | Get_file_contents _
   | Get_task _ | Save_file_req _ | Get_first_unproven_node _
   | Save_req | Exit_req | Get_global_infos
   | Interrupt_req -> false
@@ -142,6 +142,9 @@ let print_request fmt r =
   | Command_req (_nid, s)           -> fprintf fmt "command \"%s\"" s
   | Add_file_req f                  -> fprintf fmt "open file %s" f
   | Set_config_param(s,i)           -> fprintf fmt "set config param %s %i" s i
+  | Set_prover_policy(p1,p2)        ->
+     fprintf fmt "set prover policy %a -> %a" Whyconf.print_prover p1
+             Whyconf.print_prover_upgrade_policy p2
   | Get_file_contents _f            -> fprintf fmt "get file contents"
   | Get_first_unproven_node _nid    -> fprintf fmt "get first unproven node"
   | Get_task(nid,b,loc)           -> fprintf fmt "get task(%d,%b,%b)" nid b loc

src/session/itp_communication.mli

@@ -9,7 +9,7 @@
 (*                                                                  *)
 (********************************************************************)
 
-type prover = string
+
 (* Name and description *)
 type transformation = (string * string)
 type strategy = string
@@ -121,6 +121,7 @@ type ide_request =
      provers, applying transformations, stategies.  *)
   | Add_file_req            of string
   | Set_config_param        of string * int
+  | Set_prover_policy       of Whyconf.prover * Whyconf.prover_upgrade_policy
   | Get_file_contents       of string
   | Get_task                of node_ID * bool * bool
   (** [Get_task(id,b,loc)] requests for the text of the task in node

src/session/itp_server.ml

@@ -1296,8 +1296,8 @@ end
    let request_is_valid r =
      match r with
      | Save_req | Reload_req | Get_file_contents _ | Save_file_req _
-     | Interrupt_req | Add_file_req _ | Set_config_param _ | Exit_req
-     | Get_global_infos -> true
+     | Interrupt_req | Add_file_req _ | Set_config_param _ | Set_prover_policy _
+     | Exit_req | Get_global_infos -> true
      | Get_first_unproven_node ni ->
          Hint.mem model_any ni
      | Remove_subtree nid ->
@@ -1417,6 +1417,9 @@ end
          | "memlimit" -> Server_utils.set_session_memlimit i
          | _ -> P.notify (Message (Error ("Unknown config parameter "^s)))
        end
+    | Set_prover_policy(p,u)   ->
+       let c = d.cont in
+       Controller_itp.set_session_prover_upgrade_policy c p u
     | Exit_req                -> exit 0
      )
     with

src/session/json_util.ml

@@ -16,11 +16,13 @@ open Json_base
 
 (* TODO match exceptions and complete some cases *)
 
-let convert_prover_to_json (p: Whyconf.prover) =
-  Record (convert_record
-    ["prover_name", String p.Whyconf.prover_name;
-     "prover_version", String p.Whyconf.prover_version;
-     "prover_altern", String p.Whyconf.prover_altern])
+let convert_prover (prefix:string) (p: Whyconf.prover) =
+  [prefix ^ "name", String p.Whyconf.prover_name;
+   prefix ^ "version", String p.Whyconf.prover_version;
+   prefix ^ "altern", String p.Whyconf.prover_altern]
+let convert_prover_to_json (prefix:string) (p: Whyconf.prover) =
+
+  Record (convert_record (convert_prover prefix p))
 
 let convert_infos (i: global_information) =
   let convert_prover (s,h,p) =
@@ -101,10 +103,10 @@ let convert_proof_attempt (pas: proof_attempt_status) =
                       "exception", String (Pp.string_of Exn_printer.exn_printer e)]
   | Uninstalled p ->
       convert_record ["proof_attempt", String "Uninstalled";
-                      "prover", convert_prover_to_json p]
+                      "prover", convert_prover_to_json "prover_" p]
   | UpgradeProver p ->
       convert_record ["proof_attempt", String "UpgradeProver";
-                      "prover", convert_prover_to_json p])
+                      "prover", convert_prover_to_json "prover_" p])
 
 let convert_update u =
   Record (match u with
@@ -154,6 +156,7 @@ let convert_request_constructor (r: ide_request) =
   | Add_file_req _            -> String "Add_file_req"
   | Save_file_req _           -> String "Save_file_req"
   | Set_config_param _        -> String "Set_config_param"
+  | Set_prover_policy _       -> String "Set_prover_policy"
   | Get_file_contents _       -> String "Get_file_contents"
   | Get_task _                -> String "Get_task"
   | Remove_subtree _          -> String "Remove_subtree"
@@ -165,6 +168,16 @@ let convert_request_constructor (r: ide_request) =
   | Interrupt_req             -> String "Interrupt_req"
   | Get_global_infos          -> String "Get_global_infos"
 
+open Whyconf
+
+let convert_policy u =
+  match u with
+  | CPU_keep -> ["policy", String "keep"]
+  | CPU_upgrade p ->
+     ["policy", String "upgrade"] @ convert_prover "target_" p