diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index be54e37a3dc0c73d4d706c57e79d045741616754..f488982453657e5eaa4999f023d968dc7f52fa4f 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1121,10 +1121,6 @@ src/plugins/qed/collection.mli: CEA_WP
src/plugins/qed/engine.mli: CEA_WP
src/plugins/qed/export.ml: CEA_WP
src/plugins/qed/export.mli: CEA_WP
-src/plugins/qed/export_altergo.ml: CEA_WP
-src/plugins/qed/export_altergo.mli: CEA_WP
-src/plugins/qed/export_coq.ml: CEA_WP
-src/plugins/qed/export_coq.mli: CEA_WP
src/plugins/qed/export_why3.ml: CEA_WP
src/plugins/qed/export_why3.mli: CEA_WP
src/plugins/qed/export_whycore.ml: CEA_WP
@@ -1696,10 +1692,6 @@ src/plugins/wp/ProofSession.ml: CEA_WP
src/plugins/wp/ProofSession.mli: CEA_WP
src/plugins/wp/ProofScript.ml: CEA_WP
src/plugins/wp/ProofScript.mli: CEA_WP
-src/plugins/wp/ProverCoq.ml: CEA_WP
-src/plugins/wp/ProverCoq.mli: CEA_WP
-src/plugins/wp/ProverErgo.ml: CEA_WP
-src/plugins/wp/ProverErgo.mli: CEA_WP
src/plugins/wp/ProverScript.ml: CEA_WP
src/plugins/wp/ProverScript.mli: CEA_WP
src/plugins/wp/ProverSearch.ml: CEA_WP
diff --git a/opam/opam b/opam/opam
index da3874d70e0f39db1f87982bee7664efe60adad0..b7c3f147d041645e31f22f9a08626b5a440b6ff6 100644
--- a/opam/opam
+++ b/opam/opam
@@ -137,11 +137,6 @@ depopts: [
"zmq"
]
-messages: [
- "The Frama-C/Wp native support for Coq is deprecated and only activated with Coq.8.13.x (use TIP or Why-3 instead)."
- {coq:installed}
-]
-
post-messages: [
"Why3 provers setup: rm -f ~/.why3.conf ; why3 config detect"
]
diff --git a/share/autocomplete_frama-c b/share/autocomplete_frama-c
index 9c996616dc130fe18d77ed34128ef64b1c33565d..5b1d86283067ec54e0d2aa043579fa320c96999a 100644
--- a/share/autocomplete_frama-c
+++ b/share/autocomplete_frama-c
@@ -94,7 +94,7 @@ _frama-c ()
then
local prefix=; [[ $cur == *,* ]] && prefix="${cur%,*},"
advance_options="$(frama-c -wp-detect | grep -E -o " \[.*" | grep -E -o "[^][|]*")"
- advance_options+=" none script tip native:coq native:coqide"
+ advance_options+=" none script tip"
local ambigous="$(bind -v | grep show-all-if-ambiguous)"
ambigous="${ambigous##* }"
if [[ "$ambigous" == "on" ]]
diff --git a/src/plugins/qed/Makefile b/src/plugins/qed/Makefile
index 9562883200252930fcf30501f88e412ffd0db844..fd4255b62dc97a0a5e7f454b222fe3feb96377f6 100644
--- a/src/plugins/qed/Makefile
+++ b/src/plugins/qed/Makefile
@@ -55,7 +55,7 @@ PLUGIN_CMO:= \
plib pretty export \
export_whycore \
export_why3 \
- export_coq \
+
PLUGIN_CMI:= logic engine
@@ -87,7 +87,6 @@ QED_API= \
plib.mli pretty.mli engine.mli export.mli \
export_whycore.mli \
export_why3.mli \
- export_coq.mli \
QED_MLI=$(addprefix $(Qed_DIR)/, $(QED_API))
diff --git a/src/plugins/qed/export_coq.ml b/src/plugins/qed/export_coq.ml
deleted file mode 100644
index aa39074635d604c21455ec6561e9b7675bf43797..0000000000000000000000000000000000000000
--- a/src/plugins/qed/export_coq.ml
+++ /dev/null
@@ -1,378 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Exportation Engine for Coq --- *)
-(* -------------------------------------------------------------------------- *)
-
-open Logic
-open Format
-open Plib
-open Engine
-open Export
-
-module Make(T : Term) =
-struct
-
- module T = T
- module E = Export.Make(T)
- module Env = E.Env
-
- open T
-
- type tau = (Field.t,ADT.t) datatype
- type trigger = (var,Fun.t) ftrigger
- type typedef = (tau,Field.t,Fun.t) ftypedef
-
- class virtual engine =
- object(self)
-
- inherit E.engine
-
- (* -------------------------------------------------------------------------- *)
- (* --- Types --- *)
- (* -------------------------------------------------------------------------- *)
-
- method t_int = "Z"
- method t_real = "R"
- method t_bool = "bool"
- method t_prop = "Prop"
- method t_atomic = function
- | Int | Real | Bool | Prop | Tvar _ -> true
- | Array _ -> false
- | Data(_,[]) -> true
- | Data _ -> false
- | Record _ -> true
-
- method pp_array fmt t =
- fprintf fmt "array %a" self#pp_subtau t
-
- method pp_farray fmt a b =
- fprintf fmt "farray %a %a" self#pp_subtau a self#pp_subtau b
-
- method pp_tvar fmt k =
- if 1 <= k && k <= 26 then
- let c = int_of_char 'A' + (k-1) in
- pp_print_char fmt (char_of_int c)
- else
- fprintf fmt "A%d" k
-
- method virtual datatype : T.ADT.t -> string
-
- method pp_datatype adt fmt = function
- | [] -> pp_print_string fmt (self#datatype adt)
- | ts -> Plib.pp_call_apply ~f:(self#datatype adt) self#pp_subtau fmt ts
-
- (* -------------------------------------------------------------------------- *)
- (* --- Primitives --- *)
- (* -------------------------------------------------------------------------- *)
-
- method callstyle = CallApply
- method op_scope = function Aint -> Some "%Z" | Areal -> Some "%R"
-
- method pp_int _amode fmt z = pp_print_string fmt (Z.to_string z)
- method pp_real fmt q =
- fprintf fmt "( %s / %s )%%R"
- (Z.to_string q.Q.num)
- (Z.to_string q.Q.den)
-
- method e_true = function Cterm -> "true" | Cprop -> "True"
- method e_false = function Cterm -> "false" | Cprop -> "False"
-
- (* -------------------------------------------------------------------------- *)
- (* --- Arithmetics --- *)
- (* -------------------------------------------------------------------------- *)
-
- method op_add (_:amode) = Assoc "+"
- method op_sub (_:amode) = Assoc "-"
- method op_mul (_:amode) = Assoc "*"
- method op_div = function Aint -> Call "Cdiv" | Areal -> Call "Rdiv"
- method op_mod = function Aint -> Call "Cmod" | Areal -> Call "Rmod"
- method op_minus (_:amode) = Op "-"
- method op_real_of_int = Call "IZR"
-
- method op_eq (c:cmode) (a:amode) =
- match c , a with
- | Cprop , _ -> Op "="
- | Cterm , Aint -> Call "Zeq_bool"
- | Cterm , Areal -> Call "Req_bool"
-
- method op_neq (c:cmode) (a:amode) =
- match c , a with
- | Cprop , _ -> Op "<>"
- | Cterm , Aint -> Call "Zneq_bool"
- | Cterm , Areal -> Call "Rneq_bool"
-
- method op_lt (c:cmode) (a:amode) =
- match c , a with
- | Cprop , _ -> Op "<"
- | Cterm , Aint -> Call "Zlt_bool"
- | Cterm , Areal -> Call "Rlt_bool"
-
- method op_leq (c:cmode) (a:amode) =
- match c , a with
- | Cprop , _ -> Op "<="
- | Cterm , Aint -> Call "Zle_bool"
- | Cterm , Areal -> Call "Rle_bool"
-
- (* -------------------------------------------------------------------------- *)
- (* --- Connectives --- *)
- (* -------------------------------------------------------------------------- *)
-
- method op_not = function Cterm -> Call "negb" | Cprop -> Op "~"
- method op_or = function Cterm -> Call "orb" | Cprop -> Assoc "\\/"
- method op_and = function Cterm -> Call "andb" | Cprop -> Assoc "/\\"
- method op_imply = function Cterm -> Call "implb" | Cprop -> Assoc "->"
- method op_equiv = function Cterm -> Call "eqb" | Cprop -> Op "<->"
- method op_equal = function Cterm -> Call "Aeq_bool" | Cprop -> Op "="
- method op_noteq = function Cterm -> Call "Aneq_bool" | Cprop -> Op "<>"
-
- (* -------------------------------------------------------------------------- *)
- (* --- Conditional --- *)
- (* -------------------------------------------------------------------------- *)
-
- method pp_conditional fmt a b c =
- match Export.pmode self#mode with
- | Negative ->
- begin
- fprintf fmt "branch@ %a@ %a@ %a"
- self#pp_atom a self#pp_atom b self#pp_atom c ;
- end
- | Positive ->
- begin
- fprintf fmt "itep@ %a@ %a@ %a"
- self#pp_atom a self#pp_atom b self#pp_atom c ;
- end
- | Boolean ->
- begin
- fprintf fmt "@[<hov 0>if " ;
- self#with_mode Mterm (fun _ -> self#pp_atom fmt a) ;
- fprintf fmt "@ then %a" self#pp_atom b ;
- fprintf fmt "@ else %a" self#pp_atom c ;
- fprintf fmt "@]" ;
- end
-
- (* -------------------------------------------------------------------------- *)
- (* --- Arrays --- *)
- (* -------------------------------------------------------------------------- *)
-
- method pp_array_cst fmt k v =
- let pp_domain fmt v =
- try self#pp_tau fmt (T.typeof v)
- with Not_found -> pp_print_string fmt "_"
- in
- fprintf fmt "@[<hov 2>(const@ %a :@ farray@ %a@ %a)@]"
- self#pp_atom v self#pp_tau k pp_domain v
-
- method pp_array_get fmt m k =
- fprintf fmt "%a.[ %a ]" self#pp_atom m self#pp_flow k
-
- method pp_array_set fmt m k v =
- fprintf fmt "%a.[ %a <- %a ]" self#pp_atom m self#pp_flow k self#pp_flow v
-
- (* -------------------------------------------------------------------------- *)
- (* --- Records --- *)
- (* -------------------------------------------------------------------------- *)
-
- method virtual field : T.Field.t -> string
-
- method pp_get_field fmt r f =
- fprintf fmt "%s@ %a" (self#field f) self#pp_atom r
-
- method pp_def_fields fmt fvs =
- begin
- fprintf fmt "@[<hov 2>{|" ;
- Plib.iteri
- (fun i (f,v) -> match i with
- | Ifirst | Imiddle ->
- fprintf fmt "@ @[<hov 2>%s := %a ;@]" (self#field f) self#pp_flow v
- | Isingle | Ilast ->
- fprintf fmt "@[<hov 2>%s := %a@]" (self#field f) self#pp_flow v
- ) fvs ;
- fprintf fmt "@ |}@]" ;
- end
-
- (* -------------------------------------------------------------------------- *)
- (* --- Atomicity --- *)
- (* -------------------------------------------------------------------------- *)
-
- method op_spaced = is_identifier
-
- method is_atomic e =
- match T.repr e with
- | Kint z -> Z.leq Z.zero z
- | Kreal _ -> true
- | Apply(_,[]) | Rdef _ -> true
- | Apply _ | Acst _ | Aset _ | Aget _ | Rget _ -> false
- | Eq _ | Neq _ | Lt _ | Leq _
- | And _ | Or _ | Imply _ | Bind _ | Fun _ | If _ -> false
- | _ -> T.is_simple e
-
- method pp_let fmt (_:pmode) x e =
- fprintf fmt "@[<hov 4>let %s := %a in@]@ " x self#pp_flow e
-
- (* -------------------------------------------------------------------------- *)
- (* --- Higher Order --- *)
- (* -------------------------------------------------------------------------- *)
-
- method pp_apply _cmode e fmt es =
- begin
- fprintf fmt "@[<hov 3>(%a" self#pp_atom e ;
- List.iter (fun a -> fprintf fmt "@ %a" self#pp_atom a) es ;
- fprintf fmt ")@]"
- end
-
- method private pp_param fmt (x,t) =
- fprintf fmt "(%a : %a)" self#pp_var x self#pp_tau t
-
- method pp_forall tau fmt = function
- | [] -> ()
- | x::xs ->
- fprintf fmt "@[<hov 2>forall (%a" self#pp_var x ;
- List.iter (fun y -> fprintf fmt "@ %a" self#pp_var y) xs ;
- fprintf fmt "@ : %a),@]" self#pp_tau tau
-
- method pp_exists tau fmt = function
- | [] -> ()
- | x::xs ->
- fprintf fmt "@[<hov 2>exists %a : %a@],"
- self#pp_var x self#pp_tau tau ;
- List.iter
- (fun x ->
- fprintf fmt "@ @[<hov 2>exists %a : %a@],"
- self#pp_var x self#pp_tau tau) xs
-
- method pp_lambda fmt xs =
- Plib.iteri
- (fun i x -> match i with
- | Isingle -> fprintf fmt "@[<hov 2>fun %a =>@]@ " self#pp_param x
- | Ifirst -> fprintf fmt "@[<hov 2>fun %a" self#pp_param x
- | Imiddle -> fprintf fmt "@ %a" self#pp_param x
- | Ilast -> fprintf fmt "@ %a =>@]@ " self#pp_param x
- ) xs
-
- (* -------------------------------------------------------------------------- *)
- (* --- Declarations --- *)
- (* -------------------------------------------------------------------------- *)
-
- method private pp_declare_poly fmt n =
- if n > 0 then
- begin
- fprintf fmt " (" ;
- for i=1 to n do fprintf fmt "%a " self#pp_tvar i done ;
- fprintf fmt " : Type)" ;
- end ;
-
- method declare_type fmt adt n = function
- | Tabs ->
- begin
- fprintf fmt "Parameter %s" (self#datatype adt) ;
- self#pp_declare_poly fmt n ;
- fprintf fmt " : Type.@\n"
- end
- | Tdef def ->
- begin
- fprintf fmt "@[<hov 2>Definition %s" (self#datatype adt) ;
- self#pp_declare_poly fmt n ;
- fprintf fmt " : Type :=@ %a@].@\n" self#pp_tau def ;
- end
- | Trec fts ->
- begin
- fprintf fmt "@[<hv 0>Record %s" (self#datatype adt) ;
- self#pp_declare_poly fmt n ;
- fprintf fmt " : Type := {@[<hv 2>" ;
- Plib.iteri
- (fun idx (f,t) ->
- match idx with
- | Ifirst | Imiddle ->
- fprintf fmt "@ %s : %a ;" (self#field f) self#pp_tau t
- | Isingle | Ilast ->
- fprintf fmt "@ %s : %a" (self#field f) self#pp_tau t
- ) fts ;
- fprintf fmt "@]@ }@].@\n" ;
- end
- | Tsum cases ->
- begin
- fprintf fmt "@[<hv 0>Inductive %s" (self#datatype adt) ;
- self#pp_declare_poly fmt n ;
- fprintf fmt " : Type :=" ;
- let result = Data(adt,Kind.type_params n) in
- List.iter
- (fun (c,ts) ->
- fprintf fmt "@ | @[<hov 2>%s : " (link_name (self#link c)) ;
- List.iter (fun t -> fprintf fmt "@ %a ->" self#pp_tau t) ts ;
- fprintf fmt "@ %a@]" self#pp_tau result ;
- ) cases ;
- fprintf fmt ".@]@\n" ;
- end
-
- method declare_signature fmt f ts t =
- begin
- fprintf fmt "@[<hov 4>Parameter %s :" (link_name (self#link f)) ;
- List.iter (fun t -> fprintf fmt "@ %a ->" self#pp_tau t) ts ;
- fprintf fmt "@ %a.@]@\n" self#pp_tau t ;
- end
-
- method declare_inductive fmt f ts t l =
- begin
- fprintf fmt "@[<hov 4>Inductive %s :" (link_name (self#link f)) ;
- List.iter (fun t -> fprintf fmt "@ %a ->" self#pp_tau t) ts ;
- fprintf fmt "@ %a :=" self#pp_tau t ;
- List.iter
- (fun (lemma,xs,(_:trigger list list),p) ->
- fprintf fmt "@ | @[<hov 2>%s: %a@]" lemma self#pp_prop (T.e_forall xs p)
- ) l ;
- fprintf fmt ".@]@\n"
- end
-
- method declare_definition fmt f xs t e =
- self#global
- begin fun () ->
- fprintf fmt "@[<hov 4>Definition %s" (link_name (self#link f)) ;
- List.iter
- (fun x ->
- let a = self#bind x in
- let t = T.tau_of_var x in
- fprintf fmt "@ (%a : %a)" self#pp_var a self#pp_tau t
- ) xs ;
- fprintf fmt "@ : %a :=@ " self#pp_tau t ;
- fprintf fmt "@[<hov 2>%a@]@].@\n" (self#pp_expr t) e ;
- end
-
- method declare_fixpoint ~prefix fmt f xs t e =
- begin
- self#declare_signature fmt f (List.map tau_of_var xs) t ;
- let fix = prefix ^ (link_name (self#link f)) in
- self#declare_axiom fmt fix xs []
- (e_eq (e_fun ~result:t f (List.map e_var xs)) e) ;
- end
-
- method declare_axiom fmt lemma xs (_:trigger list list) p =
- self#global
- begin fun () ->
- fprintf fmt "@[<hov 2>Hypothesis %s: %a@].@\n"
- lemma self#pp_prop (T.e_forall xs p)
- end
-
- end
-
-end
diff --git a/src/plugins/qed/export_coq.mli b/src/plugins/qed/export_coq.mli
deleted file mode 100644
index 1ae4f8c41367b7497c744aadf9e0c22c99c804f4..0000000000000000000000000000000000000000
--- a/src/plugins/qed/export_coq.mli
+++ /dev/null
@@ -1,52 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Logic
-open Format
-
-(** Exportation Engine for Coq.
-
- Provides a full {{:Export.S.engine-c.html}engine}
- from a {{:Export.S.linker-c.html}linker}. *)
-
-module Make(T : Term) :
-sig
-
- open T
- module Env : Engine.Env with type term := term
- type trigger = (var,Fun.t) Engine.ftrigger
- type typedef = (tau,Field.t,Fun.t) Engine.ftypedef
-
- class virtual engine :
- object
- inherit [Z.t,ADT.t,Field.t,Fun.t,tau,var,term,Env.t] Engine.engine
- method marks : Env.t * T.marks
- method op_spaced : string -> bool
- method declare_type : formatter -> ADT.t -> int -> typedef -> unit
- method declare_axiom : formatter -> string -> var list -> trigger list list -> term -> unit
- method declare_fixpoint : prefix:string -> formatter -> Fun.t -> var list -> tau -> term -> unit
- method declare_signature : formatter -> Fun.t -> tau list -> tau -> unit
- method declare_inductive : formatter -> Fun.t -> tau list -> tau -> (string * var list * trigger list list * term) list -> unit
- method declare_definition : formatter -> Fun.t -> var list -> tau -> term -> unit
- end
-
-end
diff --git a/src/plugins/wp/Cmath.ml b/src/plugins/wp/Cmath.ml
index d0cb850341f5042f1903ec314dbce891052717a9..44bef2bd6b3758c3a0a7d6b07850804280812116 100644
--- a/src/plugins/wp/Cmath.ml
+++ b/src/plugins/wp/Cmath.ml
@@ -180,19 +180,12 @@ let builtin_strict_leq lfun ~domain ~zero ~monotonic a b =
(* -------------------------------------------------------------------------- *)
let f_iabs =
- extern_f ~library:"cmath"
- ~link:{
- why3 = Qed.Engine.F_call "IAbs.abs";
- coq = Qed.Engine.F_call "Z.abs";
- } "\\iabs"
+ extern_f ~library:"cmath" ~link:(Qed.Engine.F_call "IAbs.abs") "\\iabs"
let f_rabs =
extern_f ~library:"cmath"
~result:Real ~params:[Sreal]
- ~link:{
- why3 = Qed.Engine.F_call "RAbs.abs";
- coq = Qed.Engine.F_call "R.abs";
- } "\\rabs"
+ ~link:(Qed.Engine.F_call "RAbs.abs") "\\rabs"
let () =
begin
diff --git a/src/plugins/wp/GuiList.ml b/src/plugins/wp/GuiList.ml
index 8363dfff62d8716da907ec99747353c581f0cccd..5db3d2b3246d8776a21304559f7179cd4032057b 100644
--- a/src/plugins/wp/GuiList.ml
+++ b/src/plugins/wp/GuiList.ml
@@ -151,9 +151,6 @@ class pane (gprovers:GuiConfig.provers) =
List.iter
self#create_prover
[ VCS.Qed ; VCS.Tactical ] ;
- let prv = Wp_parameters.Provers.get () in
- if List.mem "native:coq" prv then
- self#create_prover VCS.NativeCoq ;
ignore (list#add_column_empty) ;
list#set_selection_mode `MULTIPLE ;
gprovers#connect self#configure ;
diff --git a/src/plugins/wp/GuiNavigator.ml b/src/plugins/wp/GuiNavigator.ml
index 62afceed657f1dab08ae6c86a185833febe6bb88..d92911dc44128a9145abc4e61097cc1aa67aeb5e 100644
--- a/src/plugins/wp/GuiNavigator.ml
+++ b/src/plugins/wp/GuiNavigator.ml
@@ -261,7 +261,6 @@ class behavior
| _ ->
let mode = match mode , prover with
| Some m , _ -> m
- | None , VCS.NativeCoq -> VCS.Edit
| _ -> if VCS.is_auto prover then VCS.Batch else VCS.Fix in
schedule (Prover.prove w ~mode ~result prover) ;
refresh w
@@ -288,8 +287,6 @@ class behavior
val popup_qed = new Widget.popup ()
val popup_tip = new Widget.popup ()
- val popup_ergo = new Widget.popup ()
- val popup_coq = new Widget.popup ()
val popup_why3_auto = new Widget.popup ()
val popup_why3_inter = new Widget.popup ()
val mutable popup_target = None
@@ -331,10 +328,6 @@ class behavior
popup_why3_inter#add_item ~label:"Check Script" ~callback:(self#popup_run VCS.Batch) ;
popup_why3_inter#add_item ~label:"Edit Script" ~callback:(self#popup_run VCS.Edit) ;
popup_why3_inter#add_item ~label:"Fixup Script" ~callback:(self#popup_run VCS.FixUpdate) ;
- self#add_popup_proofmodes popup_ergo
- [ "Run",Batch ; "Open Altgr-Ergo on Fail",Edit ; "Open Altgr-Ergo",Edit ] ;
- self#add_popup_proofmodes popup_coq
- [ "Check Proof",Batch ; "Edit on Fail",Edit ; "Edit Proof",Edit ] ;
end
method private popup w p =
@@ -344,7 +337,6 @@ class behavior
match p with
| None | Some Tactical -> popup_tip#run ()
| Some Qed -> popup_qed#run ()
- | Some NativeCoq -> popup_coq#run ()
| Some (Why3 _ as p) ->
if VCS.is_auto p
then popup_why3_auto#run ()
diff --git a/src/plugins/wp/GuiProver.ml b/src/plugins/wp/GuiProver.ml
index 7de00bf46aee7be0c66323f3b969a41ac5e24549..2ff42a0eb2c54072ddc1ad675415a0d51e147003 100644
--- a/src/plugins/wp/GuiProver.ml
+++ b/src/plugins/wp/GuiProver.ml
@@ -27,7 +27,7 @@ let wg_status = `Share "theme/default/surely_invalid.png"
let smoke_status = `Share "theme/default/valid_under_hyp.png"
let filter = function
- | VCS.Qed | VCS.Tactical | VCS.NativeCoq -> false
+ | VCS.Qed | VCS.Tactical -> false
| VCS.Why3 _ -> true
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index e62d3942fbc02ab763d2820d054dcb116af1939c..7b8ec88560b335b8eea63e14982d58d7614c04fb 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -104,23 +104,13 @@ let lemma_id l = Printf.sprintf "Q_%s" (avoid_leading_backlash l)
(* -------------------------------------------------------------------------- *)
-type 'a infoprover =
- {
- why3 : 'a;
- coq : 'a;
- }
+type 'a infoprover = 'a
(* generic way to have different informations for the provers *)
-let infoprover x = {
- why3 = x;
- coq = x;
-}
+let infoprover x = x
-let map_infoprover f i = {
- why3 = f i.why3;
- coq = f i.coq;
-}
+let map_infoprover f i = f i
type library = string
@@ -256,8 +246,8 @@ struct
type t = adt
let basename = function
- | Mtype a -> basename "M" a.ext_link.why3
- | Mrecord(r,_) -> basename "R" r.ext_link.why3
+ | Mtype a -> basename "M" a.ext_link
+ | Mrecord(r,_) -> basename "R" r.ext_link
| Comp (c,KValue) -> basename (if c.cstruct then "S" else "U") c.corig_name
| Comp (c,KInit) -> basename (if c.cstruct then "IS" else "IU") c.corig_name
| Atype lt -> basename "A" lt.lt_name
@@ -328,7 +318,7 @@ let datatype ~library name =
Mtype m
let record ~link ~library fts =
- let m = new_extern ~link ~library ~debug:link.why3 in
+ let m = new_extern ~link ~library ~debug:link in
let r = { fields = [] } in
let fs = List.map (fun (f,t) -> Mfield(m,r,f,t)) fts in
r.fields <- fs ; Mrecord(m,r)
@@ -524,7 +514,7 @@ let extern_p ~library ?bool ?prop ?link ?(params=[]) ?(coloring=false) () =
| _ , _ , Some info -> info
| _ , _ , _ -> assert false
in
- let debug = Export.debug link.why3 in
+ let debug = Export.debug link in
Model {
m_category = Logic.Function;
m_params = params ;
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index a508d69de73eef2e5d291ddd00897ddd85e0b8dc..43d479e650309b770ab49f4060d56790f6ddc349 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -33,12 +33,9 @@ type library = string
(** Name for external prover.
- In case a Qed.Engine.link is used, [F_subst] patterns
- are not supported for Why-3. *)
-type 'a infoprover = {
- why3 : 'a;
- coq : 'a;
-}
+ In case a Qed.Engine.link is used, [F_subst] patterns are not supported. *)
+type 'a infoprover = 'a
+
(** generic way to have different informations for the provers *)
val infoprover: 'a -> 'a infoprover
diff --git a/src/plugins/wp/LogicBuiltins.ml b/src/plugins/wp/LogicBuiltins.ml
index 4d012aefea216dbc20cf4f76598c39462da2d9e4..9790a06df5a90580d34fbb83e393808d7b61c6c4 100644
--- a/src/plugins/wp/LogicBuiltins.ml
+++ b/src/plugins/wp/LogicBuiltins.ml
@@ -239,7 +239,7 @@ let add_logic ~source result name kinds ~library ?category ~link () =
let add_predicate ~source name kinds ~library ~link () =
let params = List.map skind kinds in
- let lfun = Lang.extern_fp ~library ~params ~link link.why3 in
+ let lfun = Lang.extern_fp ~library ~params ~link link in
register ~source name kinds (LFUN lfun)
let add_ctor ~source name kinds ~library ~link () =
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index ed8e8a09187910fc4b88a8c415dbbd9e477f78cb..e0d4f620803ca394f56cbd1ba015bd08e7418946 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -34,7 +34,7 @@ ifneq ("$(FRAMAC_INTERNAL)","yes")
include $(FRAMAC_SHARE)/Makefile.config
endif
-# Coq Resources Installation
+# Resources Installation
include $(PLUGIN_DIR)/share/Makefile.resources
# Extension of the GUI for wp is compilable
@@ -84,7 +84,7 @@ PLUGIN_CMO:= \
MemMemory MemTyped MemRegion MemVal \
wpReached wpRTE wpTarget \
CfgCompiler StmtSemantics \
- VCS script proof wpo wpReport \
+ VCS script wpo wpReport \
Footprint Tactical Strategy \
TacClear TacSplit TacChoice TacRange TacInduction \
TacArray TacCompound TacUnfold \
@@ -94,7 +94,7 @@ PLUGIN_CMO:= \
TacSequence \
TacCongruence TacOverflow Auto \
ProofSession ProofScript ProofEngine \
- ProverTask ProverCoq \
+ ProverTask \
filter_axioms Cache ProverWhy3 \
driver prover ProverSearch ProverScript \
Factory \
@@ -158,7 +158,6 @@ endif
WP_CONFIGURE_MAKEFILE= \
$(Wp_DIR)/Makefile.in \
- $(Wp_DIR)/share/Makefile.coqwp \
$(Wp_DIR)/share/Makefile.resources \
$(CONFIG_STATUS_DIR)/config.status
@@ -303,13 +302,10 @@ clean::
## All relative to share/
-ALL_COQ_SOURCES= $(addprefix coqwp/, $(COQ_LIBS_CEA) $(COQ_LIBS_INRIA))
-ALL_COQ_BINARIES= $(addsuffix o, $(ALL_COQ_SOURCES))
ALL_WHY3_SOURCES= $(addprefix why3/frama_c_wp/, $(WHY3_LIBS_CEA))
ALL_RESOURCES= \
wp.driver \
- $(ALL_COQ_SOURCES) \
$(ALL_WHY3_SOURCES)
INSTALL_OPT?=
@@ -324,22 +320,6 @@ clean::
$(Wp_DIR)/share/instwp: $(Wp_DIR)/share/install.ml
$(OCAMLC) $(WARNINGS) -w -70 -o $@ unix.cma $^
-# --------------------------------------------------------------------------
-# --- Pre-Compiled Coq Libraries ---
-# --------------------------------------------------------------------------
-
-WP_COQC_ENABLED=@COQC@
-
-ifeq ($(WP_COQC_ENABLED),yes)
-
-include $(Wp_DIR)/share/Makefile.coqwp
-
-byte:: coqwpcompile
-opt:: coqwpcompile
-clean:: wp-coq-clean
-
-endif #($(WP_COQC_ENABLED),yes)
-
# --------------------------------------------------------------------------
# --- Installation ---
# --------------------------------------------------------------------------
@@ -350,7 +330,7 @@ install:: clean-install
$(INSTALL_SHARE) -p \
-i $(Wp_DIR)/share \
-d $(FRAMAC_DATADIR)/wp \
- $(ALL_RESOURCES) -f -b $(ALL_COQ_BINARIES)
+ $(ALL_RESOURCES) -f -b
uninstall::
$(PRINT_RM) WP shared files
diff --git a/src/plugins/wp/Plang.ml b/src/plugins/wp/Plang.ml
index f67bbaa35648f67879d15b843d33f180ff8e71cf..e6aa02a41fa981c382c95f23bb4405cc550bbf58 100644
--- a/src/plugins/wp/Plang.ml
+++ b/src/plugins/wp/Plang.ml
@@ -75,7 +75,7 @@ class engine =
object(self)
inherit E.engine as super
inherit Lang.idprinting
- method infoprover w = w.why3
+ method infoprover w = w
(* --- Types --- *)
diff --git a/src/plugins/wp/ProverCoq.ml b/src/plugins/wp/ProverCoq.ml
deleted file mode 100644
index 75a1361e434a0a813ada48324e9da4cbd8584f8f..0000000000000000000000000000000000000000
--- a/src/plugins/wp/ProverCoq.ml
+++ /dev/null
@@ -1,671 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Prover Coq Interface --- *)
-(* -------------------------------------------------------------------------- *)
-
-open Cil_types
-open Qed
-open Lang
-open Definitions
-
-let dkey = Wp_parameters.register_category "prover"
-
-let cluster_file c =
- let dir = WpContext.directory () in
- let base = cluster_id c in
- Printf.sprintf "%s/%s.v" (dir :> string) base
-
-(* -------------------------------------------------------------------------- *)
-(* --- External Coq Libraries --- *)
-(* -------------------------------------------------------------------------- *)
-
-(* Applies to both WP resources from the Share, and User-defined libraries *)
-let option_file = LogicBuiltins.create_option
- (fun ~driver_dir x -> driver_dir ^ "/" ^ x)
- "coq" "file"
-
-type coqlib = {
- c_id : string ; (* Identifies the very original file. *)
- c_source : string ; (* Original file directory. *)
- c_file : string ; (* Relative Coq source file. *)
- c_path : string ; (* Relative Coq source directory. *)
- c_name : string ; (* Module package. *)
- c_module : string ; (* Full module name. *)
-}
-
-(* example:
-
- {
- c_id="/mydir/foobar:a/b/User.v" ;
- c_source="/mydir/foobar" ;
- c_file= "a/b/User.v" ;
- c_path = "a/b" ;
- c_name = "a.b" ;
- c_module = "a.b.User" ;
- }
-
-*)
-
-(* Take the directory name and changes all '/' into '.' *)
-let name_of_path path =
- if path = "." then ""
- else
- String.map (fun c -> if c = '/' || c = '\\' then '.' else c) path
-
-let find_nonwin_column opt =
- let p = String.rindex opt ':' in
- if String.length opt >= 3 &&
- opt.[1] = ':' && (opt.[2] = '/' || opt.[2] = '\\') && p = 1 then
- (* windows absolute path, not <source>:<dir>/<file.v> format. *)
- raise Not_found
- else p
-
-(* Parses the coq.file option from the driver. *)
-let parse_c_option opt =
- try
- (* Format "<source>:<dir>/<file.v>" *)
- let p = find_nonwin_column opt in
- let c_source = String.sub opt 0 p in
- let c_file = String.sub opt (p+1) (String.length opt - p - 1) in
- let c_path = Filename.dirname c_file in
- let c_name = name_of_path c_path in
- let coqid = Filename.chop_extension (Filename.basename c_file) in
- let c_module =
- Printf.sprintf "%s.%s" c_name
- (String.capitalize_ascii coqid)
- in
- { c_id = opt ; c_source ; c_file ; c_path ; c_name ; c_module }
- with Not_found ->
- (* Format "<source>/<file.v>" *)
- let c_source = Filename.dirname opt in
- let c_file = Filename.basename opt in
- let c_module =
- String.capitalize_ascii (Filename.chop_extension c_file)
- in
- { c_id = opt ; c_source ; c_file ; c_path = "." ; c_name = "" ; c_module }
-
-let coqlibs = Hashtbl.create 128 (*[LC] Not Projectified. *)
-let c_option opt =
- try Hashtbl.find coqlibs opt
- with Not_found ->
- let clib = parse_c_option opt in
- Hashtbl.add coqlibs opt clib ; clib
-(* -------------------------------------------------------------------------- *)
-(* --- Dependencies --- *)
-(* -------------------------------------------------------------------------- *)
-
-type depend =
- | D_cluster of cluster (* Generated in <out>/<model>/A.v *)
- | D_coqlib of coqlib (* From <source>/ or <out>/coqwp/ *)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Exporting Formulae to Coq --- *)
-(* -------------------------------------------------------------------------- *)
-
-let engine =
- let module E = Qed.Export_coq.Make(Lang.F.QED) in
- object(self)
- inherit E.engine as super
- inherit Lang.idprinting
- method infoprover p = p.coq
-
- method! pp_fun cmode fct ts =
- if fct == Vlist.f_concat
- then Vlist.export self ts
- else super#pp_fun cmode fct ts
-
- end
-
-
-class visitor fmt c =
- object(self)
-
- inherit Definitions.visitor c
- inherit ProverTask.printer fmt (cluster_title c)
-
- val mutable deps : depend list = []
-
- (* --- Managing Formatter --- *)
-
- method flush =
- begin
- Format.pp_print_newline fmt () ;
- List.rev deps
- end
-
- (* --- Files, Theories and Clusters --- *)
-
- method add_coqfile opt =
- let clib = c_option opt in
- Format.fprintf fmt "Require Import %s.@\n" clib.c_module ;
- deps <- (D_coqlib clib) :: deps
-
- method on_library thy =
- let files = LogicBuiltins.get_option option_file ~library:thy in
- List.iter self#add_coqfile files
-
- method on_cluster c =
- self#lines ;
- Format.fprintf fmt "Require Import %s.@\n" (cluster_id c) ;
- deps <- (D_cluster c) :: deps
-
- method on_type lt def =
- begin
- self#lines ;
- engine#declare_type fmt (Lang.adt lt) (List.length lt.lt_params) def ;
- end
-
- method private gen_on_comp kind c fts =
- begin
- self#paragraph ;
- let adt = match kind with
- | KValue -> Lang.comp c
- | KInit -> Lang.comp_init c
- in
- let t = match fts with
- | None -> Qed.Engine.Tabs
- | Some fts -> Qed.Engine.Trec fts
- in
- engine#declare_type fmt adt 0 t ;
- end
-
- method on_comp = self#gen_on_comp KValue
- method on_icomp = self#gen_on_comp KInit
-
- method on_dlemma l =
- begin
- self#paragraph ;
- engine#declare_axiom fmt
- (Lang.lemma_id l.l_name)
- l.l_forall l.l_triggers
- (F.e_prop l.l_lemma)
- end
-
- method on_dfun d =
- begin
- self#paragraph ;
- match d.d_definition with
- | Logic t ->
- engine#declare_signature fmt
- d.d_lfun (List.map F.tau_of_var d.d_params) t ;
- | Function(t,mu,v) ->
- let pp = match mu with
- | Rec -> engine#declare_fixpoint ~prefix:"Fix"
- | Def -> engine#declare_definition
- in pp fmt d.d_lfun d.d_params t v
- | Predicate(mu,p) ->
- let pp = match mu with
- | Rec -> engine#declare_fixpoint ~prefix:"Fix"
- | Def -> engine#declare_definition
- in pp fmt d.d_lfun d.d_params Logic.Prop (F.e_prop p)
- | Inductive dl ->
- engine#declare_inductive fmt
- d.d_lfun (List.map F.tau_of_var d.d_params) Logic.Prop
- (List.map (fun l -> (Lang.lemma_id l.l_name,
- l.l_forall,
- l.l_triggers,
- (F.e_prop l.l_lemma))
- ) dl)
- end
-
- end
-
-let write_cluster c =
- let f = cluster_file c in
- Wp_parameters.debug ~dkey "Generate '%s'" f ;
- let deps = Command.print_file f
- begin fun fmt ->
- let v = new visitor fmt c in
- v#lines ;
- v#printf "Require Import ZArith.@\n" ;
- v#printf "Require Import Reals.@\n" ;
- v#on_library "qed" ;
- v#vself ;
- v#flush ;
- end
- in Wp_parameters.print_generated f ; deps
-
-(* -------------------------------------------------------------------------- *)
-(* --- Assembling Goal --- *)
-(* -------------------------------------------------------------------------- *)
-
-(* Returns whether source was modified after target *)
-let need_recompile ~source ~target =
- try
- let t_src = (Unix.stat source).Unix.st_mtime in
- let t_tgt = (Unix.stat target).Unix.st_mtime in
- t_src >= t_tgt
- with Unix.Unix_error _ -> true
-
-(* Used to mark version of clusters already available *)
-
-module CLUSTERS = WpContext.Index
- (struct
- type key = cluster
- type data = int * depend list
- let name = "ProverCoq.FILES"
- let compare = cluster_compare
- let pretty = pp_cluster
- end)
-
-(* Used to mark coqlib versions to use *)
-module Marked = Set.Make
- (struct
- type t = depend
- let compare d1 d2 =
- match d1 , d2 with
- | D_coqlib _ , D_cluster _ -> (-1)
- | D_cluster _ , D_coqlib _ -> 1
- | D_cluster c1 , D_cluster c2 -> Definitions.cluster_compare c1 c2
- | D_coqlib c1 , D_coqlib c2 -> String.compare c1.c_id c2.c_id
- end)
-
-type included = string * string
-(* -R <path> <name>, name possibly empty, use -I instead *)
-type coqcc = {
- mutable marked : Marked.t ;
- mutable includes : included list ; (* (reversed) includes with as *)
- mutable sources : string list ; (* (reversed) file .v to recompile *)
-}
-
-let add_include coqcc dir =
- if not (List.mem dir coqcc.includes) then coqcc.includes <- dir :: coqcc.includes
-
-let add_source coqcc file =
- if not (List.mem file coqcc.sources) then coqcc.sources <- file :: coqcc.sources
-
-(* Recursive assembly: some file need further dependencies *)
-
-let rec assemble coqcc d =
- if not (Marked.mem d coqcc.marked) then
- begin
- coqcc.marked <- Marked.add d coqcc.marked ;
- match d with
- | D_cluster cluster -> assemble_cluster coqcc cluster
- | D_coqlib clib -> assemble_coqlib coqcc clib
- end
-
-and assemble_cluster coqcc c =
- let (age,deps) = try CLUSTERS.find c with Not_found -> (-1,[]) in
- let deps =
- if age < cluster_age c then
- let deps = write_cluster c in
- CLUSTERS.update c (cluster_age c , deps) ; deps
- else deps in
- List.iter (assemble coqcc) deps ;
- add_source coqcc (cluster_file c)
-
-and assemble_coqlib coqcc c =
- let compiled = Printf.sprintf "%s/%so" c.c_source c.c_file in
- if Sys.file_exists compiled then
- let dir = Printf.sprintf "%s/%s" c.c_source c.c_path in
- add_include coqcc (dir,c.c_name)
- else
- begin
- let tgtdir = Wp_parameters.get_output_dir "coqwp" in
- let source = Printf.sprintf "%s/%s" c.c_source c.c_file in
- let target = Printf.sprintf "%s/%s" (tgtdir :> string) c.c_file in
- let dir = Printf.sprintf "%s/%s" (tgtdir :> string) c.c_path in
- if need_recompile ~source ~target then
- begin
- Wp_parameters.make_output_dir dir ;
- Command.copy source target ;
- end ;
- add_include coqcc (dir,c.c_name) ;
- add_source coqcc target;
- end
-
-(* -------------------------------------------------------------------------- *)
-(* --- Assembling Goal --- *)
-(* -------------------------------------------------------------------------- *)
-
-let assemble_goal ~pid axioms prop =
- let title = Pretty_utils.to_string WpPropId.pretty pid in
- let model = WpContext.directory () in
- let id = WpPropId.get_propid pid in
- let file = Printf.sprintf "%s/%s.coq" (model :> string) id in
- let goal = cluster ~id ~title () in
- let deps = Command.print_file file
- begin fun fmt ->
- let v = new visitor fmt goal in
- v#printf "Require Import ZArith.@\n" ;
- v#printf "Require Import Reals.@\n" ;
- v#on_library "qed" ;
- v#vgoal axioms prop ;
- let libs = Wp_parameters.CoqLibs.get () in
- if libs <> [] then
- begin
- v#section "Additional Libraries" ;
- List.iter v#add_coqfile libs ;
- v#hline ;
- end ;
- v#paragraph ;
- engine#global
- begin fun () ->
- v#printf "@[<hv 2>Goal@ %a.@]@."
- engine#pp_prop (F.e_prop prop) ;
- end ;
- v#flush
- end in
- let coqcc = { marked = Marked.empty ; includes = [] ; sources = [] } in
- List.iter (assemble coqcc) deps ;
- let includes = ((model :> string) , "") :: List.rev coqcc.includes in
- let sources = List.rev coqcc.sources in
- includes , sources , file
-
-(* -------------------------------------------------------------------------- *)
-(* --- Running Coq --- *)
-(* -------------------------------------------------------------------------- *)
-
-open Task
-open VCS
-
-let coq_timeout () =
- let coqtimeout = Wp_parameters.CoqTimeout.get () in
- let gentimeout = Wp_parameters.Timeout.get () in
- max coqtimeout gentimeout
-
-let coqide_lock = Task.mutex ()
-let emacs_regexp = Str.regexp_string_case_fold "emacs"
-let is_emacs cmd =
- try ignore (Str.search_forward emacs_regexp cmd 0) ; true
- with Not_found -> false
-
-class runcoq includes source =
- let base = Filename.chop_extension source in
- let logout = base ^ "_Coq.out" in
- let logerr = base ^ "_Coq.err" in
- object(self)
-
- inherit ProverTask.command "coq"
-
- method private project =
- let dir = Filename.dirname source in
- let p = Wp_parameters.CoqProject.get () in
- Command.pp_to_file (Printf.sprintf "%s/%s" dir p)
- begin fun fmt ->
- List.iter
- (fun (dir,name) ->
- if name = "" then
- Format.fprintf fmt "-R %s ''@\n" dir
- else
- Format.fprintf fmt "-R %s %s@\n" dir name
- ) includes ;
- Format.fprintf fmt "-arg@\n" ;
- end
-
- method private options =
- begin
- List.iter
- (fun (dir,name) ->
- if name = "" then
- self#add ["-R";dir;""]
- else
- self#add ["-R";dir;name]
- ) includes ;
- end
-
- method failed : 'a. 'a task =
- begin
- let name = Filename.basename source in
- Wp_parameters.feedback ~ontty:`Message "[Coq] '%s' compilation failed." name ;
- if Wp_parameters.verbose_atleast 1 then
- begin
- ProverTask.pp_file ~message:"Coqc (stdout)" ~file:logout ;
- ProverTask.pp_file ~message:"Coqc (stderr)" ~file:logerr ;
- end ;
- Task.failed "Compilation of '%s' failed." name ;
- end
-
- method compile =
- let cmd = Wp_parameters.CoqCompiler.get () in
- self#set_command cmd ;
- self#options ;
- self#add [ source ] ;
- self#timeout (coq_timeout ()) ;
- Task.call
- (fun () ->
- let name = Filename.basename source in
- Wp_parameters.feedback ~ontty:`Transient
- "[Coq] Compiling '%s'." name) ()
- >>= self#run ~logout ~logerr
- >>= fun r ->
- if r = 127 then Task.failed "Command '%s' not found" cmd
- else if r <> 0 then self#failed
- else Task.return ()
-
- method check =
- let cmd = Wp_parameters.CoqCompiler.get () in
- self#set_command cmd ;
- self#options ;
- self#add [ source ] ;
- self#timeout (coq_timeout ()) ;
- self#run ~logout ~logerr () >>= function
- | 127 -> Task.failed "Command '%s' not found" cmd
- | 0 -> Task.return true
- | 1 -> Task.return false
- | _ -> self#failed
-
- method coqide =
- let coqide = Wp_parameters.CoqIde.get () in
- self#set_command coqide ;
- if is_emacs coqide then
- begin
- self#project ;
- self#add [ source ] ;
- end
- else
- begin
- self#options ;
- self#add [ source ] ;
- end ;
- Task.sync coqide_lock (self#run ~logout ~logerr)
- end
-
-(* -------------------------------------------------------------------------- *)
-(* --- Compilation Helpers --- *)
-(* -------------------------------------------------------------------------- *)
-
-let shared_demon = ref true
-let shared_headers : (string,unit Task.shared) Hashtbl.t = Hashtbl.create 120
-
-let shared includes source =
- try Hashtbl.find shared_headers source
- with Not_found ->
- if !shared_demon then
- begin
- shared_demon := false ;
- let server = ProverTask.server () in
- Task.on_server_stop server (fun () -> Hashtbl.clear shared_headers) ;
- end ;
- let shared = Task.shared ~retry:true
- (fun () -> (new runcoq includes source)#compile)
- in Hashtbl.add shared_headers source shared ; shared
-
-let rec compile_headers includes forced = function
- | [] -> Task.nop
- | source::headers ->
- let target = source ^ "o" in
- if forced || need_recompile ~source ~target then
- begin
- let cc = shared includes source in
- Task.share cc >>= fun () -> compile_headers includes true headers
- end
- else compile_headers includes forced headers
-
-(* -------------------------------------------------------------------------- *)
-(* --- Coq Prover --- *)
-(* -------------------------------------------------------------------------- *)
-
-let ontty = `Feedback
-
-open Wpo
-
-type coq_wpo = {
- cw_pid : WpPropId.prop_id ;
- cw_gid : string ;
- cw_goal : string ; (* filename for goal without proof *)
- cw_script : string ; (* filename for goal with proof script *)
- cw_headers : string list ; (* filename for libraries *)
- cw_includes : included list ; (* -R ... ... *)
-}
-
-let make_script w script closing =
- Command.print_file w.cw_script
- begin fun fmt ->
- Command.pp_from_file fmt w.cw_goal ;
- Format.fprintf fmt "Proof.@\n%s%s@\n@." script closing ;
- end
-
-let try_script w script closing =
- make_script w script closing ;
- (new runcoq w.cw_includes w.cw_script)#check
-
-let rec try_hints w = function
- | [] -> Task.return false
- | (kind,script,closing) :: hints ->
- Wp_parameters.feedback ~ontty "[Coq] Goal %s : %s" w.cw_gid kind ;
- try_script w script closing >>= fun succeed ->
- if succeed then
- let required,hints = WpPropId.prop_id_keys w.cw_pid in
- let keys = List.merge String.compare required hints in
- Proof.add_script_for ~gid:w.cw_gid keys script closing ;
- Task.return true
- else
- try_hints w hints
-
-let try_prove w =
- begin
- match Proof.script_for ~pid:w.cw_pid ~gid:w.cw_gid with
- | Some (script,closing) ->
- Wp_parameters.feedback ~ontty "[Coq] Goal %s : Saved script" w.cw_gid ;
- try_script w script closing
- | None -> Task.return false
- end
- >>= fun succeed ->
- if succeed then
- Task.return true
- else
- try_hints w (Proof.hints_for ~pid:w.cw_pid)
-
-let try_coqide w =
- let script,closing =
- Proof.script_for_ide ~pid:w.cw_pid ~gid:w.cw_gid in
- make_script w script closing ;
- (new runcoq w.cw_includes w.cw_script)#coqide >>= fun st ->
- if st = 0 then
- match Proof.parse_coqproof w.cw_script with
- | None ->
- Wp_parameters.feedback "[Coq] No proof found" ;
- Task.return false
- | Some(script,closing) ->
- if Proof.is_empty_script script then
- begin
- Proof.delete_script_for ~gid:w.cw_gid ;
- Task.canceled () ;
- end
- else
- begin
- let req,hs = WpPropId.prop_id_keys w.cw_pid in
- let hints = List.merge String.compare req hs in
- Proof.add_script_for ~gid:w.cw_gid hints script closing ;
- Wp_parameters.feedback ~ontty "[Coq] Goal %s : Script" w.cw_gid ;
- try_script w script closing
- end
- else if st = 127
- then Task.failed "CoqIde command '%s' not found" (Wp_parameters.CoqIde.get ())
- else Task.failed "CoqIde exits with status %d." st
-
-let prove_session ~mode w =
- begin
- compile_headers w.cw_includes false w.cw_headers >>=
- begin fun () ->
- match mode with
- | Batch | Update -> try_prove w
- | Edit -> try_coqide w
- | Fix | FixUpdate ->
- begin
- try_prove w >>> function
- | Task.Result true -> Task.return true
- | Task.Failed e -> Task.raised e
- | Task.Canceled | Task.Timeout _ | Task.Result false -> try_coqide w
- end
- end
- end
- >>= Task.call (fun r -> if r then VCS.valid else VCS.unknown)
-
-let gen_session w =
- begin
- make_script w " ...\n" "Qed." ;
- Wp_parameters.print_generated w.cw_script ;
- Task.return VCS.no_result
- end
-
-let prove_session ~mode w =
- if Wp_parameters.Generate.get () then
- gen_session w
- else
- prove_session ~mode w
-
-let prove_prop wpo ~mode ~axioms ~prop =
- let pid = wpo.po_pid in
- let gid = wpo.po_gid in
- let model = wpo.po_model in
- let context = Wpo.get_context wpo in
- let script = DISK.file_goal ~pid ~model ~prover:NativeCoq in
- let includes , headers , goal =
- WpContext.on_context context (assemble_goal ~pid axioms) prop
- in
- prove_session ~mode {
- cw_pid = pid ;
- cw_gid = gid ;
- cw_goal = goal ;
- cw_script = script ;
- cw_headers = headers ;
- cw_includes = includes ;
- }
-
-let prove_annot wpo vcq ~mode =
- Task.todo
- begin fun () ->
- let prop =
- WpContext.on_context (Wpo.get_context wpo)
- (GOAL.compute_proof ~pid:wpo.po_pid) vcq.VC_Annot.goal in
- prove_prop wpo ~mode ~axioms:None ~prop
- end
-
-let prove_lemma wpo vca ~mode =
- Task.todo
- begin fun () ->
- let lemma = vca.VC_Lemma.lemma in
- let depends = vca.VC_Lemma.depends in
- let prop = F.p_forall lemma.l_forall lemma.l_lemma in
- let axioms = Some(lemma.l_cluster,depends) in
- prove_prop wpo ~mode ~axioms ~prop
- end
-
-let prove mode wpo =
- match wpo.Wpo.po_formula with
- | GoalAnnot vcq -> prove_annot wpo vcq ~mode
- | GoalLemma vca -> prove_lemma wpo vca ~mode
diff --git a/src/plugins/wp/ProverCoq.mli b/src/plugins/wp/ProverCoq.mli
deleted file mode 100644
index 35287cc626049deb497a95353d6737e3e44b587a..0000000000000000000000000000000000000000
--- a/src/plugins/wp/ProverCoq.mli
+++ /dev/null
@@ -1,30 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Task
-open VCS
-
-(* -------------------------------------------------------------------------- *)
-(* --- Alt-Ergo Theorem Prover --- *)
-(* -------------------------------------------------------------------------- *)
-
-val prove : mode -> Wpo.t -> result task
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index ffdbeed2d2d9c31f449b8e316b9237bcde3162a5..9b4df821321a90605ab696180861dc73c5037a7d 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -37,10 +37,9 @@ struct
let stage = function
| Prover( Qed , { verdict = Valid } ) -> 0
| Prover( Why3 _ , { verdict = Valid } ) -> 1
- | Prover( NativeCoq , { verdict = Valid } ) -> 2
- | Tactic _ -> 3
- | Prover _ -> 4
- | Error _ -> 5
+ | Tactic _ -> 2
+ | Prover _ -> 3
+ | Error _ -> 4
let time = function
| Tactic _ | Error _ -> 0.0
diff --git a/src/plugins/wp/ProverTask.ml b/src/plugins/wp/ProverTask.ml
index 1811bf0a2bb5d253b8cd144f23ca4b5a5cf0a5cf..cb0989a0c924cd1133d9837c78ebbb812dd920e7 100644
--- a/src/plugins/wp/ProverTask.ml
+++ b/src/plugins/wp/ProverTask.ml
@@ -302,7 +302,6 @@ let server ?procs () =
let np = getprocs procs in
let s = Task.server ~procs:np () in
Why3Provers.set_procs np ;
- Task.on_server_stop s Proof.savescripts ;
server := Some s ; s
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index a21e48d0d86a6ae13935ac743ae2ca4de7b55051..e89b87890f82921162f173f4fec10d8bfd3b42c8 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -140,7 +140,7 @@ let lfun_name (lfun:Lang.lfun) =
| ACSL f -> Qed.Engine.F_call (Lang.logic_id f)
| CTOR c -> Qed.Engine.F_call (Lang.ctor_id c)
| Model({m_source=Generated(_,n)}) -> Qed.Engine.F_call n
- | Model({m_source=Extern e}) -> e.Lang.ext_link.Lang.why3
+ | Model({m_source=Extern e}) -> e.Lang.ext_link
let coerce ~cnv sort expected r =
@@ -151,8 +151,8 @@ let coerce ~cnv sort expected r =
| _ -> r
let name_of_adt = function
- | Lang.Mtype a -> a.Lang.ext_link.Lang.why3
- | Mrecord(a,_) -> a.Lang.ext_link.Lang.why3
+ | Lang.Mtype a -> a.Lang.ext_link
+ | Mrecord(a,_) -> a.Lang.ext_link
| Comp (c, KValue) -> Lang.comp_id c
| Comp (c, KInit) -> Lang.comp_init_id c
| Atype lt -> Lang.type_id lt
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 9adac2908d3a76ddd90e4364f97ecb507c446dbc..2faa6011629180a42c57748deef6e8074fd42600 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -28,7 +28,6 @@ let dkey_shell = Wp_parameters.register_category "shell"
type prover =
| Why3 of Why3Provers.t (* Prover via WHY *)
- | NativeCoq (* Direct Coq and Coqide *)
| Qed (* Qed Solver *)
| Tactical (* Interactive Prover *)
@@ -42,12 +41,6 @@ type mode =
let parse_prover = function
| "" | "none" -> None
| "qed" | "Qed" -> Some Qed
- | "native-coq" (* for wp-reports *)
- | "native:coq" | "native:coqide" | "native:coqedit"
- ->
- Wp_parameters.warning ~once:true ~current:false
- "native support for coq is deprecated, use tip instead" ;
- Some NativeCoq
| "script" -> Some Tactical
| "tip" -> Some Tactical
| "why3" -> Some (Why3 { Why3.Whyconf.prover_name = "why3";
@@ -83,7 +76,6 @@ let parse_mode m =
let name_of_prover = function
| Why3 s -> Why3Provers.print_wp s
- | NativeCoq -> "native:coq"
| Qed -> "qed"
| Tactical -> "script"
@@ -92,7 +84,6 @@ let title_of_prover = function
if Wp_parameters.has_dkey dkey_shell
then Why3Provers.name s
else Why3Provers.title s
- | NativeCoq -> "Coq (native)"
| Qed -> "Qed"
| Tactical -> "Script"
@@ -119,13 +110,12 @@ let sanitize_why3 s =
let filename_for_prover = function
| Why3 s -> sanitize_why3 (Why3Provers.print_wp s)
- | NativeCoq -> "Coq"
| Qed -> "Qed"
| Tactical -> "Tactical"
let is_auto = function
| Qed -> true
- | Tactical | NativeCoq -> false
+ | Tactical -> false
| Why3 p ->
match p.prover_name with
| "Alt-Ergo" | "CVC4" | "Z3" -> true
@@ -145,9 +135,6 @@ let cmp_prover p q =
| Tactical , Tactical -> 0
| Tactical , _ -> (-1)
| _ , Tactical -> 1
- | NativeCoq , NativeCoq -> 0
- | NativeCoq , _ -> (-1)
- | _ , NativeCoq -> 1
| Why3 p , Why3 q -> Why3Provers.compare p q
let pp_prover fmt p = Format.pp_print_string fmt (title_of_prover p)
@@ -331,7 +318,6 @@ let pp_result fmt r =
let is_qualified prover result =
match prover with
| Qed | Tactical -> true
- | NativeCoq -> result.verdict <> Timeout
| Why3 _ -> result.cached || result.prover_time < Rformat.epsilon
let pp_cache_miss fmt st updating prover result =
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 544d259d47e23e193e085865b6e3ceb1ed9e13e2..7d81ce1743c382abc88859f5c3fc9b9f6e5363f9 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -28,7 +28,6 @@
type prover =
| Why3 of Why3Provers.t (** Prover via WHY *)
- | NativeCoq (** Direct Coq and Coqide *)
| Qed (** Qed Solver *)
| Tactical (** Interactive Prover *)
diff --git a/src/plugins/wp/Vlist.ml b/src/plugins/wp/Vlist.ml
index 204b5adac9cc3198cf8ed535afe360e8cc849dbe..87dc9ab818146f8fd3a6a76e9d1138f8ca9196b6 100644
--- a/src/plugins/wp/Vlist.ml
+++ b/src/plugins/wp/Vlist.ml
@@ -40,14 +40,8 @@ let library = "vlist"
let t_list = "\\list"
let l_list = Lang.infoprover "list"
let l_concat = Lang.infoprover (E.F_right "concat")
-let l_elt = Lang.(E.({
- why3 = F_call "elt" ;
- coq = F_subst "(cons %1 nil)" ;
- }))
-let l_repeat = Lang.(E.({
- why3 = F_call "repeat" ;
- coq = F_call "repeat" ;
- }))
+let l_elt = E.(F_call "elt")
+let l_repeat = E.(F_call "repeat")
(*--- Typechecking ---*)
diff --git a/src/plugins/wp/driver.mll b/src/plugins/wp/driver.mll
index 400780fc71d0bafcd88602899de0d5c30747847f..e2c95f53cd26e6b9e19ed7c3ddd6779839d1d939 100644
--- a/src/plugins/wp/driver.mll
+++ b/src/plugins/wp/driver.mll
@@ -285,11 +285,9 @@ and bal = parse
skip input; Lang.infoprover link
| RECLINK l ->
skip input ;
- begin try
- {Lang.why3 = conv_bal def (List.assoc "why3" l);
- coq = conv_bal def (List.assoc "coq" l) }
+ begin try conv_bal def (List.assoc "why3" l);
with Not_found ->
- failwith "a link must contain an entry for 'why3' and 'coq'"
+ failwith "a link must contain an entry for 'why3'"
end
| _ -> failwith "Missing link symbol"
@@ -299,11 +297,9 @@ and bal = parse
skip input ; Lang.infoprover f
| `RecString l ->
skip input ;
- begin try
- {Lang.why3 = List.assoc "why3" l;
- coq = List.assoc "coq" l }
+ begin try List.assoc "why3" l
with Not_found ->
- failwith "a link must contain an entry for 'why3' and 'coq'"
+ failwith "a link must contain an entry for 'why3'"
end
| _ -> failwith "Missing link symbol"
diff --git a/src/plugins/wp/proof.ml b/src/plugins/wp/proof.ml
deleted file mode 100644
index f9d54288e6a9df846fbc65c55b020a8951065f07..0000000000000000000000000000000000000000
--- a/src/plugins/wp/proof.ml
+++ /dev/null
@@ -1,321 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Proof Script Database --- *)
-(* -------------------------------------------------------------------------- *)
-
-let scriptbase : (string, string list * string * string) Hashtbl.t = Hashtbl.create 81
-(* [ goal name -> sorted hints , script , closing ] *)
-let scriptfile = ref None (* current file script name *)
-let needback = ref false (* file script need backup before modification *)
-let needsave = ref false (* file script need to be saved *)
-let needwarn = ref false (* user should be prompted for chosen scriptfile *)
-
-let sanitize hint =
- try
- let n = String.length hint in
- if n <= 0 then raise Exit ;
- for i = 0 to n - 1 do
- match hint.[i] with
- | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_' | '-' | '*' -> ()
- | _ -> raise Exit
- done ; true
- with Exit -> false
-
-let register_script goal hints proof closing =
- let hints = List.sort String.compare (List.filter sanitize hints) in
- Hashtbl.replace scriptbase goal (hints,proof,closing)
-
-let delete_script_for ~gid =
- Hashtbl.remove scriptbase gid
-
-(* -------------------------------------------------------------------------- *)
-(* --- Proof Scripts Parsers --- *)
-(* -------------------------------------------------------------------------- *)
-
-open Script
-
-let is_empty_script script =
- try
- for i=0 to String.length script - 1 do
- match script.[i] with '\n' | ' ' | '\t' -> () | _ -> raise Exit
- done ; true
- with Exit -> false
-
-let parse_coqproof file =
- let input = Script.open_file file in
- try
- let rec fetch_proof input =
- match token input with
- | Proof(p,c) -> Some(p,c)
- | Eof -> None
- | _ -> skip input ; fetch_proof input
- in
- let proof = fetch_proof input in
- Script.close input ; proof
- with e ->
- Script.close input ;
- raise e
-
-let collect_scripts input =
- while key input "Goal" do
- let g = ident input in
- eat input "." ;
- let xs =
- if key input "Hint" then
- let xs = idents input in
- eat input "." ; xs
- else []
- in
- let proof,qed =
- match token input with
- | Proof(p,c) -> skip input ; p,c
- | _ -> error input "Missing proof"
- in
- register_script g xs proof qed
- done ;
- if token input <> Eof
- then error input "Unexpected script declaration"
-
-let parse_scripts file =
- if Sys.file_exists file then
- begin
- let input = Script.open_file file in
- try
- collect_scripts input ;
- Script.close input ;
- with e ->
- Script.close input ;
- raise e
- end
-
-let dump_scripts file =
- let out = open_out file in
- let fmt = Format.formatter_of_out_channel out in
- try
- Format.fprintf fmt "(* Generated by Frama-C WP *)@\n@\n" ;
- let goals = Hashtbl.fold (fun goal _ gs -> goal::gs) scriptbase [] in
- List.iter
- (fun goal ->
- let (hints,proof,qed) = Hashtbl.find scriptbase goal in
- Format.fprintf fmt "Goal %s.@\n" goal ;
- (match hints with
- | [] -> ()
- | k::ks ->
- Format.fprintf fmt "Hint %s" k ;
- List.iter (fun k -> Format.fprintf fmt ",%s" k) ks ;
- Format.fprintf fmt ".@\n");
- Format.fprintf fmt "Proof.@\n%s%s@\n@." proof qed
- ) (List.sort String.compare goals) ;
- Format.pp_print_newline fmt () ;
- close_out out ;
- with e ->
- Format.pp_print_newline fmt () ;
- close_out out ;
- raise e
-
-(* -------------------------------------------------------------------------- *)
-(* --- Scripts Management --- *)
-(* -------------------------------------------------------------------------- *)
-
-let rec choose k =
- let file = Printf.sprintf "wp%d.script" k in
- if Sys.file_exists file then choose (succ k) else file
-
-let savescripts () =
- if !needsave then
- match !scriptfile with
- | None -> ()
- | Some file ->
- if Wp_parameters.UpdateScript.get () then
- try
- if !needback then
- ( Command.copy file (file ^ ".back") ; needback := false ) ;
- if !needwarn then
- ( needwarn := false ;
- Wp_parameters.warning ~current:false
- "No script file specified.@\n\
- Your proofs are saved in '%s'@\n\
- Use -wp-script '%s' to re-run them."
- file file ;
- ) ;
- dump_scripts file ;
- needsave := false ;
- with e ->
- Wp_parameters.abort
- "Error when dumping script file '%s':@\n%s" file
- (Printexc.to_string e)
- else
- Wp_parameters.warning ~once:true ~current:false
- "Script base modified : modification will not be saved"
-
-let loadscripts () =
- let user = Wp_parameters.Script.get () in
- if !scriptfile <> Some user then
- begin
- savescripts () ;
- begin
- try parse_scripts user ;
- with e ->
- Wp_parameters.error
- "Error in script file '%s':@\n%s" user
- (Printexc.to_string e)
- end ;
- if Wp_parameters.UpdateScript.get () then
- if user = "" then
- (* update new file *)
- begin
- let ftmp = choose 0 in
- Wp_parameters.Script.set ftmp ;
- scriptfile := Some ftmp ;
- needwarn := true ;
- needback := false ;
- end
- else
- (* update user's file *)
- begin
- scriptfile := Some user ;
- needback := Sys.file_exists user ;
- end
- else
- (* do not update *)
- begin
- scriptfile := Some user ;
- needback := false ;
- end
- end
-
-let find_script_for_goal ~gid =
- loadscripts () ;
- try
- let _,proof,qed = Hashtbl.find scriptbase gid in
- Some(proof,qed)
- with Not_found ->
- None
-
-let update_hints_for_goal goal hints =
- try
- let old_hints,script,qed = Hashtbl.find scriptbase goal in
- let new_hints = List.sort String.compare hints in
- if Stdlib.compare new_hints old_hints <> 0 then
- begin
- Hashtbl.replace scriptbase goal (new_hints,script,qed) ;
- needsave := true ;
- end
- with Not_found -> ()
-
-
-let rec matches n xs ys =
- match xs , ys with
- | x::rxs , y::rys ->
- let c = String.compare x y in
- if c < 0 then matches n rxs ys else
- if c > 0 then matches n xs rys else
- matches (succ n) rxs rys
- | _ -> n
-
-let rec filter xs ys =
- match xs , ys with
- | [] , _ -> ys
- | _::_ , [] -> raise Not_found
- | x::rxs , y::rys ->
- let c = String.compare x y in
- if c < 0 then raise Not_found else
- if c > 0 then y :: filter xs rys else
- filter rxs rys
-
-let most_suitable (n,_,_,_) (n',_,_,_) = n'-n
-
-let find_script_with_hints required hints =
- loadscripts () ;
- let required = List.sort String.compare required in
- let hints = List.sort String.compare hints in
- List.sort most_suitable
- begin
- Hashtbl.fold
- (fun g (xs,proof,qed) scripts ->
- try
- let n = matches 0 hints (filter required xs) in
- (n,g,proof,qed)::scripts
- with Not_found -> scripts)
- scriptbase []
- end
-
-let add_script_for ~gid hints proof =
- needsave := true ; register_script gid hints proof
-
-(* -------------------------------------------------------------------------- *)
-(* --- Prover API --- *)
-(* -------------------------------------------------------------------------- *)
-
-let script_for ~pid ~gid =
- let found = find_script_for_goal ~gid in
- ( if found <> None then
- let required,hints = WpPropId.prop_id_keys pid in
- let all = List.merge String.compare required hints in
- update_hints_for_goal gid all ) ;
- found
-
-let rec head n = function [] -> []
- | x::xs -> if n > 0 then x :: head (pred n) xs else []
-
-let hints_for ~pid =
- let default = match Wp_parameters.CoqTactic.get () with
- | "none" -> []
- | tactic -> ["Default tactic",Printf.sprintf " %s.\n" tactic,"Qed."]
- in
- if Wp_parameters.TryHints.get () then
- let nhints = Wp_parameters.Hints.get () in
- if nhints > 0 then
- let required,hints = WpPropId.prop_id_keys pid in
- let scripts = find_script_with_hints required hints in
- default @ List.map (fun (_,_,s,q) -> "Hint",s,q) (head nhints scripts)
- else default
- else default
-
-let script_for_ide ~pid ~gid =
- match find_script_for_goal ~gid with
- | Some script -> script
- | None ->
- let required,hints = WpPropId.prop_id_keys pid in
- let hints = find_script_with_hints required hints in
- let script =
- if hints = [] then
- begin
- match Wp_parameters.CoqTactic.get () with
- | "none" -> ""
- | tactic -> Format.asprintf "(* %s. *)\n" tactic
- end
- else
- begin
- let nhints = Wp_parameters.Hints.get () in
- Format.asprintf "%t"
- (fun fmt ->
- List.iter
- (fun (_,g,script,_) ->
- Format.fprintf fmt
- "(*@ --------------------------------------\n \
- @ From '%s': \n%s*)\n%!" g script
- ) (head nhints hints))
- end
- in script , "Qed."
diff --git a/src/plugins/wp/proof.mli b/src/plugins/wp/proof.mli
deleted file mode 100644
index 8fb4c7f14a7e12645cfb358da664d216c1bf64b6..0000000000000000000000000000000000000000
--- a/src/plugins/wp/proof.mli
+++ /dev/null
@@ -1,48 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2021 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(* -------------------------------------------------------------------------- *)
-(** Coq Proof Scripts *)
-(* -------------------------------------------------------------------------- *)
-
-open WpPropId
-
-val is_empty_script : string -> bool
-(** Check a proof script text for emptyness *)
-
-val delete_script_for : gid:string -> unit
-(** [delete_script ~gid] remove known script for goal. *)
-
-val add_script_for : gid:string -> string list -> string -> string -> unit
-(** [new_script goal keys proof qed] registers the script [proof]
- terminated by [qed] for goal [gid] and keywords [keys] *)
-
-val parse_coqproof : string -> (string * string) option
-(** [parse_coqproof f] parses a coq-file [f] and fetch the first proof. *)
-
-val savescripts : unit -> unit
-(** If necessary, dump the scripts database into the file
- specified by [-wp-script f]. *)
-
-val script_for : pid:prop_id -> gid:string -> (string * string) option
-val script_for_ide : pid:prop_id -> gid:string -> string * string
-val hints_for : pid:prop_id -> (string * string * string) list
diff --git a/src/plugins/wp/prover.ml b/src/plugins/wp/prover.ml
index 7ba0c5f0a554a5319d8711a69fcda4c4c28e7301..4483cf24c32f0571871134cd696ecbded8eb93cb 100644
--- a/src/plugins/wp/prover.ml
+++ b/src/plugins/wp/prover.ml
@@ -33,7 +33,6 @@ let dispatch ?(config=VCS.default) mode prover wpo =
begin
match prover with
| Qed | Tactical -> Task.return VCS.no_result
- | NativeCoq -> ProverCoq.prove mode wpo
| Why3 prover ->
let smoke = Wpo.is_smoke_test wpo in
ProverWhy3.prove
diff --git a/src/plugins/wp/share/Makefile.coqwp b/src/plugins/wp/share/Makefile.coqwp
deleted file mode 100644
index 9bdd3d154b0096059f1d5a09c6a4877def52982a..0000000000000000000000000000000000000000
--- a/src/plugins/wp/share/Makefile.coqwp
+++ /dev/null
@@ -1,87 +0,0 @@
-##########################################################################
-# #
-# This file is part of WP plug-in of Frama-C. #
-# #
-# Copyright (C) 2007-2021 #
-# CEA (Commissariat a l'energie atomique et aux energies #
-# alternatives) #
-# #
-# you can redistribute it and/or modify it under the terms of the GNU #
-# Lesser General Public License as published by the Free Software #
-# Foundation, version 2.1. #
-# #
-# It is distributed in the hope that it will be useful, #
-# but WITHOUT ANY WARRANTY; without even the implied warranty of #
-# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
-# GNU Lesser General Public License for more details. #
-# #
-# See the GNU Lesser General Public License version 2.1 #
-# for more details (enclosed in the file licenses/LGPLv2.1). #
-# #
-##########################################################################
-
-
-WPLSHARE=$(Wp_DIR)/share
-
-# --------------------------------------------------------------------------
-# --- Coq Compilation
-# --------------------------------------------------------------------------
-
-.PHONY: coqwpcompile
-
-COQWPINCLUDES= -R $(WPLSHARE)/coqwp ''
-COQWPBINARIES= $(addprefix $(WPLSHARE)/, $(ALL_COQ_BINARIES))
-
-coqwpcompile: $(COQWPBINARIES)
-
-$(WPLSHARE)/coqwp/%.vo: $(WPLSHARE)/coqwp/%.v
- echo "Coqc $<"
- coqc -w none $(COQWPINCLUDES) $<
-
-$(WPLSHARE)/coqwp/%.ide: $(WPLSHARE)/coqwp/%.v
- echo "Coqide $<"
- coqide $(COQWPINCLUDES) $<
-
-$(WPLSHARE)/coqwp/.depend: $(addprefix $(WPLSHARE)/, $(WP_COQ_SOURCES))
- echo "Coqdep $(WPLSHARE)/coqwp"
- @coqdep $(COQWPINCLUDES) $(WPLSHARE)/coqwp/*.v $(WPLSHARE)/coqwp/**/*.v > $@
-
-# --------------------------------------------------------------------------
-# --- Additional Targets
-# --------------------------------------------------------------------------
-
-.PHONY: wp-coq-compile wp-coq-clean wp-coq-install wp-coq-uninstall
-
-wp-coq-compile: coqwpcompile
- @echo "Run 'make wp-coq-install' to install all precompiled libraries"
-
-wp-coq-clean:
- find $(Wp_DIR) \( -name "*.vo" -or -name "*.glob" -or -name ".*.aux" \) -delete
- rm -f $(WPLSHARE)/coqwp/.depend
-
-wp-coq-install:
- $(PRINT_INSTALL) "Coq Libraries"
- $(INSTALL_SHARE) -f -p -s \
- -i $(Wp_DIR)/share \
- -d $(FRAMAC_DATADIR)/wp \
- $(ALL_COQ_BINARIES)
-
-wp-coq-uninstall:
- $(PRINT_RM) "Coq Libraries"
- @rm -f $(FRAMAC_DATADIR)/wp/why3/*.vo
- @rm -f $(FRAMAC_DATADIR)/wp/coqwp/*.vo
- @rm -f $(FRAMAC_DATADIR)/wp/coqwp/*/*.vo
-
-# --------------------------------------------------------------------------
-# --- Coq Dependencies
-# --------------------------------------------------------------------------
-
-ifneq ($(MAKECMDGOALS),clean)
-ifneq ($(MAKECMDGOALS),distclean)
-ifneq ($(MAKECMDGOALS),smartclean)
-sinclude $(WPLSHARE)/coqwp/.depend
-endif
-endif
-endif
-
-# --------------------------------------------------------------------------
diff --git a/src/plugins/wp/share/Makefile.resources b/src/plugins/wp/share/Makefile.resources
index 4fea780bb2adefba6f7d67c28ebf9904ab6f2adb..f28c1d26ae72c9c86b50ff23477f1a55a46bbc51 100644
--- a/src/plugins/wp/share/Makefile.resources
+++ b/src/plugins/wp/share/Makefile.resources
@@ -39,93 +39,6 @@ WHY3_LIBS_CEA:= \
## Used in share/why3
WHY3_API_LIBS_CEA:= WHY3_LIBS_CEA
-# --------------------------------------------------------------------------
-# --- Coq Libraries
-# --------------------------------------------------------------------------
-
-## Used in share/coqwp
-
-COQ_LIBS_CEA:= \
- ArcTrigo.v \
- Bits.v \
- Cbits.v \
- Cfloat.v \
- Cint.v \
- Cmath.v \
- Square.v \
- ExpLog.v \
- Memory.v \
- Qed.v \
- Qedlib.v \
- Vset.v \
- Vlist.v \
- Zbits.v
-
-COQ_LIBS_INRIA:=\
- BuiltIn.v \
- HighOrd.v \
- bool/Bool.v \
- int/Abs.v \
- int/ComputerDivision.v \
- int/EuclideanDivision.v \
- int/ComputerOfEuclideanDivision.v \
- int/Exponentiation.v \
- int/Int.v \
- int/MinMax.v \
- int/Power.v \
- map/Map.v \
- map/Const.v \
- real/Abs.v \
- real/FromInt.v \
- real/MinMax.v \
- real/Real.v \
- real/RealInfix.v \
- real/Square.v \
- real/ExpLog.v \
- real/PowerReal.v \
- real/Trigonometry.v
-
-# --------------------------------------------------------------------------
-# --- Alt-Ergo Libraries
-# --------------------------------------------------------------------------
-
-# Used in share/ergo
-
-ERGO_LIBS_CEA:= \
- ArcTrigo.mlw \
- Cbits.mlw \
- Cfloat.mlw \
- Cint.mlw \
- Cmath.mlw \
- Square.mlw \
- ExpLog.mlw \
- Memory.mlw \
- Qed.mlw \
- Vset.mlw \
- Vlist.mlw
-
-ERGO_LIBS_INRIA:= \
- bool.Bool.mlw \
- int.Abs.mlw \
- int.ComputerDivision.mlw \
- int.ComputerOfEuclideanDivision.mlw \
- int.Int.mlw \
- int.MinMax.mlw \
- map.Map.mlw \
- map.Const.mlw \
- real.Abs.mlw \
- real.FromInt.mlw \
- real.MinMax.mlw \
- real.Real.mlw \
- real.RealInfix.mlw \
- real.Square.mlw \
- real.Truncate.mlw \
- real.ExpLog.mlw \
- real.PowerReal.mlw \
- real.Trigonometry.mlw \
- real.Hyperbolic.mlw \
- real.Polar.mlw
-
# --------------------------------------------------------------------------
# --- LICENSES
# --------------------------------------------------------------------------
@@ -135,23 +48,13 @@ ERGO_LIBS_INRIA:= \
WP_SHARE_SRC_CEA_RESOURCES:= \
wp.driver \
why3/coq.drv \
- $(addprefix why3/frama_c_wp/, $(WHY3_LIBS_CEA)) \
- $(addprefix coqwp/, $(COQ_LIBS_CEA)) \
- $(addprefix ergo/, $(ERGO_LIBS_CEA))
+ $(addprefix why3/frama_c_wp/, $(WHY3_LIBS_CEA))
ALL_CEA_RESOURCES+= \
install.ml \
Makefile.resources \
- Makefile.coqwp \
$(WP_SHARE_SRC_CEA_RESOURCES)
-ALL_UNMODIFIED_WHY3_RESOURCES:= \
- $(addprefix coqwp/, $(COQ_LIBS_INRIA))
-
-ALL_MODIFIED_WHY3_RESOURCES:= \
- $(addprefix ergo/, $(ERGO_LIBS_INRIA))
-
-
##########################################################################
# Local Variables:
# mode: makefile
diff --git a/src/plugins/wp/share/wp.driver b/src/plugins/wp/share/wp.driver
index 48a312726cbf71bd861b9b850b99053ab64ae39c..92fcd8039c8d53ea7bff2188cad2a46b63075dc5 100644
--- a/src/plugins/wp/share/wp.driver
+++ b/src/plugins/wp/share/wp.driver
@@ -21,63 +21,39 @@
/**************************************************************************/
library qed:
-coq.file += "coqwp/BuiltIn.v";
-coq.file += "coqwp:bool/Bool.v";
-coq.file += "coqwp/HighOrd.v";
-coq.file += "coqwp:int/Int.v";
-coq.file += "coqwp:int/Abs.v";
-coq.file += "coqwp:int/ComputerDivision.v";
-coq.file += "coqwp:int/EuclideanDivision.v";
-coq.file += "coqwp:int/ComputerOfEuclideanDivision.v";
-coq.file += "coqwp:real/Real.v";
-coq.file += "coqwp:real/RealInfix.v";
-coq.file += "coqwp:real/FromInt.v";
-coq.file += "coqwp:map/Map.v";
-coq.file += "coqwp:bool/Bool.v";
-coq.file += "coqwp/Qedlib.v";
-coq.file += "coqwp/Qed.v";
why3.import += "int.Abs:IAbs";
why3.import += "frama_c_wp.qed.Qed";
why3.qualifier := "frama_c_wp.qed";
library const:
-coq.file += "coqwp:map/Const.v";
why3.import += "map.Const";
library minmax_int:
-coq.file += "coqwp:int/MinMax.v";
why3.import += "int.MinMax:Ig";
logic integer "\\max"(integer,integer) =
commutative:associative:idempotent:
- {coq="Zmax";why3="Ig.max"};
+ {why3="Ig.max"};
logic integer "\\min"(integer,integer) =
commutative:associative:idempotent:
- {coq="Zmin";why3="Ig.min"};
+ {why3="Ig.min"};
library minmax_real:
-coq.file += "coqwp:real/MinMax.v";
why3.import += "real.MinMax:Rg";
logic real "\\max"(real,real) =
commutative:associative:idempotent:
- {coq="Rmax";why3="Rg.max"};
+ {why3="Rg.max"};
logic real "\\min"(real,real) =
commutative:associative:idempotent:
- {coq="Rmin";why3="Rg.min"};
+ {why3="Rg.min"};
library cint:
-coq.file += "coqwp/Bits.v";
-coq.file += "coqwp/Zbits.v";
-coq.file += "coqwp/Cint.v";
why3.import += "frama_c_wp.cint.Cint";
library cbits: cint
logic boolean "bit_test"(integer,integer) := \bit_test_stdlib;
-coq.file += "coqwp/Cbits.v";
why3.import += "frama_c_wp.cbits.Cbits";
library cfloat: cmath sqrt
-coq.file += "coqwp:real/Abs.v";
-coq.file += "coqwp/Cfloat.v";
why3.import += "frama_c_wp.cfloat.Cfloat";
type "rounding_mode" = "Rounding.mode";
ctor "\\Up"() = "Rounding.RTP";
@@ -100,33 +76,24 @@ logic float64 "\\round_double"(rounding_mode,real) = "round_double";
library vset:
type set = "set";
-coq.file := "coqwp/Vset.v";
why3.import := "vset.Vset";
library vlist:
-coq.file := "coqwp/Vlist.v";
why3.import := "frama_c_wp.vlist.Vlist";
library memory:
-coq.file := "coqwp/Memory.v";
why3.import := "frama_c_wp.memory.Memory";
library sqrt: cmath
why3.import += "real.Square";
-coq.file += "coqwp/Square.v";
why3.import += "frama_c_wp.cmath.Square";
library exponential: qed
why3.import += "real.ExpLog" ;
why3.import += "frama_c_wp.cmath.ExpLog" ;
-coq.file += "coqwp:real/ExpLog.v" ;
-coq.file += "coqwp/Exp.v" ;
library power: exponential sqrt
why3.import += "real.PowerReal" ;
-coq.file += "coqwp:int/Exponentiation.v" ;
-coq.file += "coqwp:int/Power.v" ;
-coq.file += "coqwp:real/PowerReal.v" ;
library truncate: qed
why3.import += "real.Truncate" ;
@@ -134,17 +101,12 @@ why3.import += "real.Truncate" ;
library cmath: qed
why3.import += "real.Abs:RAbs" ;
why3.import += "frama_c_wp.cmath.Cmath";
-coq.file += "coqwp:real/Abs.v" ;
-coq.file += "coqwp:real/Square.v";
-coq.file += "coqwp/Cmath.v";
library trigonometry: sqrt cmath
why3.import += "real.Trigonometry";
-coq.file += "coqwp:real/Trigonometry.v";
library arctrigo: trigonometry
why3.import += "frama_c_wp.cmath.ArcTrigo";
-coq.file += "coqwp/ArcTrigo.v";
library hyperbolic: sqrt exponential
why3.import += "real.Hyperbolic";
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 18a0bdb55351abd6caec31e62c573887bb5830b8..56f0e0a3e6d676db2e5a28960f18fda513676512 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -885,105 +885,6 @@ module BackTrack = Int
Limits backtracking when applying strategies."
end)
-let () = Parameter_customize.set_group wp_prover_options
-module Script =
- String(struct
- let option_name = "-wp-coq-script"
- let arg_name = "f.script"
- let default = ""
- let help = "Set user's file for Coq proofs."
- end)
-
-let () = Parameter_customize.set_group wp_prover_options
-module UpdateScript =
- True(struct
- let option_name = "-wp-update-coq-script"
- let help = "If turned off, do not save or modify user's proofs."
- end)
-
-let () = Parameter_customize.set_group wp_prover_options
-module CoqTimeout =
- Int(struct
- let option_name = "-wp-coq-timeout"
- let default = 30
- let arg_name = "n"
- let help =
- Printf.sprintf
- "Set the timeout (in seconds) for Coq (default: %d)." default
- end)
-
-let () = Parameter_customize.set_group wp_prover_options
-module CoqCompiler =
- String(struct
- let option_name = "-wp-coqc"
- let default = "coqc"
- let arg_name = "cmd"
- let help =
- Printf.sprintf
- "Set the command line to run Coq Compiler (default 'coqc')."
- end)
-
-let () = Parameter_customize.set_group wp_prover_options
-module CoqIde =
- String(struct
- let option_name = "-wp-coqide"
- let default = "coqide"
- let arg_name = "cmd"
- let help =
- Printf.sprintf
- "Set the command line to run CoqIde (default 'coqide')\n\
- If the command-line contains 'emacs' (case insentive),\n\
- a coq-project file is used instead of coq options."
- end)
-
-let () = Parameter_customize.set_group wp_prover_options
-module CoqProject =
- String(struct
- let option_name = "-wp-coq-project"
- let default = "_CoqProject"
- let arg_name = "file"
- let help =
- Printf.sprintf
- "Set the Coq-Project file to used with Proof General (default '_CoqProject')"
- end)
-
-let () = Parameter_customize.set_group wp_prover_options
-module CoqTactic =
- String
- (struct
- let option_name = "-wp-coq-tactic"
- let arg_name = "proof"
- let default = "auto with zarith"
- let help = "Default tactic for Coq"
- end)
-
-let () = Parameter_customize.set_group wp_prover_options
-module TryHints =
- False
- (struct
- let option_name = "-wp-coq-tryhints"
- let help = "Try scripts from other goals (see also -wp-hints)"
- end)
-
-let () = Parameter_customize.set_group wp_prover_options
-module Hints =
- Int
- (struct
- let option_name = "-wp-coq-hints"
- let arg_name = "n"
- let default = 3
- let help = "Maximum number of proposed Coq scripts (default 3)"
- end)
-
-let () = Parameter_customize.set_group wp_prover_options
-module CoqLibs =
- String_list
- (struct
- let option_name = "-wp-coq-lib"
- let arg_name = "*.v,*.vo"
- let help = "Additional libraries for Coq"
- end)
-
let () = Parameter_customize.set_group wp_prover_options
let () = Parameter_customize.no_category ()
module Why3Flags =
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index b5c36d48cb38d5f1f99942b848452293fc2425bc..e1b72778280ab32247250c2c94c2bdc4746cb71d 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -118,24 +118,14 @@ module CacheEnv: Parameter_sig.Bool
module CacheDir: Parameter_sig.String
module CachePrint: Parameter_sig.Bool
module Drivers: Parameter_sig.String_list
-module Script: Parameter_sig.String
-module UpdateScript: Parameter_sig.Bool
module Timeout: Parameter_sig.Int
module SmokeTimeout: Parameter_sig.Int
module InteractiveTimeout: Parameter_sig.Int
module TimeExtra: Parameter_sig.Int
module TimeMargin: Parameter_sig.Int
-module CoqTimeout: Parameter_sig.Int
-module CoqCompiler : Parameter_sig.String
-module CoqIde : Parameter_sig.String
-module CoqProject : Parameter_sig.String
module Steps: Parameter_sig.Int
module Procs: Parameter_sig.Int
module ProofTrace: Parameter_sig.Bool
-module CoqLibs: Parameter_sig.String_list
-module CoqTactic: Parameter_sig.String
-module Hints: Parameter_sig.Int
-module TryHints: Parameter_sig.Bool
module Why3Flags: Parameter_sig.String_list
module Auto: Parameter_sig.String_list
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 91b006ef291d742097c1cfa6365f5d2490ac9cc8..a309ee7ed01ee5101ff5e455e720ff4298f7056f 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -107,7 +107,6 @@ struct
let ext = match prover with
| Qed -> "qed"
| Why3 _ -> "why"
- | NativeCoq -> "v"
| Tactical -> "tac"
in
let id = WpPropId.get_propid pid in
@@ -117,7 +116,6 @@ struct
let ext = match prover with
| Qed -> "qed"
| Why3 _ -> "why"
- | NativeCoq -> "v"
| Tactical -> "tac"
in
let id = (Kf.vi kf).vname in
@@ -468,7 +466,7 @@ module ProverType =
type t = prover
include Datatype.Undefined
let name = "Wpo.prover"
- let reprs = [ NativeCoq; Qed ]
+ let reprs = [ Qed ]
end)
(* to get a "reasonable" API doc: *)
let () = Type.set_ml_name ProverType.ty (Some "Wpo.prover")