aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coq.ml9
-rw-r--r--ide/coqOps.ml20
-rw-r--r--ide/coqide.ml4
-rw-r--r--ide/wg_Command.ml2
-rw-r--r--lib/interface.mli4
-rw-r--r--lib/serialize.ml5
-rw-r--r--tactics/tactics.ml9
-rw-r--r--toplevel/ide_slave.ml6
-rw-r--r--toplevel/vernac.ml38
-rw-r--r--toplevel/vernac.mli4
-rw-r--r--toplevel/vernacentries.ml16
-rw-r--r--toplevel/vernacentries.mli4
12 files changed, 43 insertions, 78 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index baff54d62..9b08b4f10 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -559,13 +559,8 @@ let eval_call ?(logger=default_logger) call handle k =
Minilib.log "End eval_call";
Void
-let interp ?(logger=default_logger) ?(raw=false) ?(verbose=true) i s h k =
- eval_call ~logger (Serialize.interp (i,raw,verbose,s)) h
- (function
- | Interface.Good (Util.Inl v) -> k (Interface.Good v)
- | Interface.Good (Util.Inr v) -> k (Interface.Unsafe v)
- | Interface.Fail v -> k (Interface.Fail v)
- | Interface.Unsafe _ -> assert false)
+let interp ?(logger=default_logger) ?(raw=false) ?(verbose=true) i s =
+ eval_call ~logger (Serialize.interp (i,raw,verbose,s))
let rewind i = eval_call (Serialize.rewind i)
let inloadpath s = eval_call (Serialize.inloadpath s)
let mkcases s = eval_call (Serialize.mkcases s)
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 2647f923c..d136833d0 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -93,12 +93,12 @@ object(self)
| Interface.Fail (l, str) ->
messages#set ("Error in coqtop:\n"^str);
Coq.return ()
- | Interface.Good goals | Interface.Unsafe goals ->
+ | Interface.Good goals ->
Coq.bind Coq.evars (function
| Interface.Fail (l, str)->
messages#set ("Error in coqtop:\n"^str);
Coq.return ()
- | Interface.Good evs | Interface.Unsafe evs ->
+ | Interface.Good evs ->
proof#set_goals goals;
proof#set_evars evs;
proof#refresh ();
@@ -118,7 +118,7 @@ object(self)
Coq.interp ~logger:messages#push ~raw:true ~verbose:false 0 phrase in
let next = function
| Interface.Fail (_, err) -> display_error err; Coq.return ()
- | Interface.Good msg | Interface.Unsafe msg ->
+ | Interface.Good msg ->
messages#add msg; Coq.return ()
in
Coq.bind (Coq.seq action query) next
@@ -255,9 +255,6 @@ object(self)
let query = Coq.interp ~logger:push_msg ~verbose sentence.id phrase in
let next = function
| Interface.Good msg -> commit_and_continue msg
- | Interface.Unsafe msg ->
- set_flags sentence (CList.add_set `UNSAFE sentence.flags);
- commit_and_continue msg
| Interface.Fail (loc, msg) -> self#process_error queue phrase loc msg
in
Coq.bind query next
@@ -322,7 +319,7 @@ object(self)
(** Actually performs the undoing *)
method private undo_command_stack n clear_zone =
let next = function
- | Interface.Good n | Interface.Unsafe n ->
+ | Interface.Good n ->
let until _ len _ _ = n <= len in
(* Coqtop requested [n] more ACTUAL backtrack *)
let _, zone = self#prepare_clear_zone until clear_zone in
@@ -409,9 +406,6 @@ object(self)
| Interface.Good msg ->
messages#add msg;
stop Tags.Script.processed
- | Interface.Unsafe msg ->
- messages#add msg;
- stop Tags.Script.unjustified
in
Coq.bind (Coq.seq action query) next
in
@@ -452,15 +446,15 @@ object(self)
messages#set
("Could not determine lodpath, this might lead to problems:\n"^s);
Coq.return ()
- | Interface.Good true | Interface.Unsafe true -> Coq.return ()
- | Interface.Good false | Interface.Unsafe false ->
+ | Interface.Good true -> Coq.return ()
+ | Interface.Good false ->
let cmd = Printf.sprintf "Add LoadPath \"%s\". " dir in
let cmd = Coq.interp 0 cmd in
let next = function
| Interface.Fail (l, str) ->
messages#set ("Couln't add loadpath:\n"^str);
Coq.return ()
- | Interface.Good _ | Interface.Unsafe _ ->
+ | Interface.Good _ ->
Coq.return ()
in
Coq.bind cmd next
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 616358789..2f52e5a48 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -480,7 +480,7 @@ let update_status =
| Interface.Fail (l, str) ->
display "Oops, problem while fetching coq status.";
Coq.return ()
- | Interface.Good status | Interface.Unsafe status ->
+ | Interface.Good status ->
let path = match status.Interface.status_path with
| [] | _ :: [] -> "" (* Drop the topmost level, usually "Top" *)
| _ :: l -> " in " ^ String.concat "." l
@@ -564,7 +564,7 @@ let print_branches c cases =
let display_match = function
|Interface.Fail _ ->
flash_info "Not an inductive type"; Coq.return ()
- |Interface.Good cases | Interface.Unsafe cases ->
+ |Interface.Good cases ->
let text =
let buf = Buffer.create 1024 in
let () = print_branches (Format.formatter_of_buffer buf) cases in
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index dd8896cba..ec759b67f 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -117,7 +117,7 @@ object(self)
| Interface.Fail (l,str) ->
result#buffer#insert ("Error while interpreting "^phrase^":\n"^str);
Coq.return ()
- | Interface.Good res | Interface.Unsafe res ->
+ | Interface.Good res ->
result#buffer#insert ("Result for command " ^ phrase ^ ":\n" ^ res);
Coq.return ())
in
diff --git a/lib/interface.mli b/lib/interface.mli
index d54fb8476..3ff05f6f2 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -135,7 +135,6 @@ type location = (int * int) option (* start and end of the error *)
type 'a value =
| Good of 'a
- | Unsafe of 'a
| Fail of (location * string)
(* Request/Reply message protocol between Coq and CoqIde *)
@@ -147,9 +146,8 @@ type 'a value =
The returned string contains the messages produced
but not the updated goals (they are
to be fetch by a separated [current_goals]). *)
-(* spiwack: [Inl] for safe and [Inr] for unsafe. *)
-type interp_rty = (string,string) Util.union
type interp_sty = edit_id * raw * verbose * string
+type interp_rty = string
(** Backtracking by at least a certain number of phrases.
No finished proofs will be re-opened. Instead,
diff --git a/lib/serialize.ml b/lib/serialize.ml
index fd8c7e7e4..823f4245d 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -147,7 +147,7 @@ let expected_answer_type call : value_type =
let options = pair_t (list_t string_t) option_state_t in
let objs = coq_object_t string_t in
match call with
- | Interp _ -> check (union_t string_t string_t : interp_rty val_t)
+ | Interp _ -> check (string_t : interp_rty val_t)
| Rewind _ -> check (int_t : rewind_rty val_t)
| Goal _ -> check (option_t goals_t : goals_rty val_t)
| Evars _ -> check (option_t (list_t evar_t) : evars_rty val_t)
@@ -332,7 +332,6 @@ let to_coq_object f = function
let of_value f = function
| Good x -> Element ("value", ["val", "good"], [f x])
-| Unsafe x -> Element ("value", ["val", "unsafe"], [f x])
| Fail (loc, msg) ->
let loc = match loc with
| None -> []
@@ -344,7 +343,6 @@ let to_value f = function
| Element ("value", attrs, l) ->
let ans = massoc "val" attrs in
if ans = "good" then Good (f (singleton l))
- else if ans = "unsafe" then Unsafe (f (singleton l))
else if ans = "fail" then
let loc =
try
@@ -663,7 +661,6 @@ let pr_call = function
| About _ -> "ABOUT"
let pr_value_gen pr = function
| Good v -> "GOOD " ^ pr v
- | Unsafe v -> "UNSAFE" ^ pr v
| Fail (_,str) -> "FAIL ["^str^"]"
let pr_value v = pr_value_gen (fun _ -> "FIXME") v
let pr_full_value call value =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 210800955..c531a34fa 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3574,10 +3574,13 @@ let admit_as_an_axiom gl =
(** ppedrot: seems legit to have admitted subproofs as local*)
let con = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true na decl in
let axiom = constr_of_global (ConstRef con) in
- exact_no_check
- (applist (axiom,
+ let gl =
+ exact_no_check
+ (applist (axiom,
List.rev (Array.to_list (instance_from_named_context sign))))
- gl
+ gl in
+ Pp.feedback Interface.AddedAxiom;
+ gl
let unify ?(state=full_transparent_state) x y gl =
try
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index fd5fa85cb..2aa2cc36f 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -120,10 +120,10 @@ let interp (id,raw,verbosely,s) =
let loc_ast = Vernac.parse_sentence (pa,None) in
if not raw then coqide_cmd_checks loc_ast;
Flags.make_silent (not verbosely);
- let status = Vernac.eval_expr ~preserving:raw loc_ast in
+ Vernac.eval_expr ~preserving:raw loc_ast;
Flags.make_silent true;
- let ret = read_stdout () in
- if status then Util.Inl ret else Util.Inr ret
+ Pp.feedback Interface.Processed;
+ read_stdout ()
(** Goal display *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 67befcb17..b1c3d2b9a 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -278,9 +278,8 @@ let rec vernac_com interpfun checknav (loc,com) =
end;
begin
try
- let status = read_vernac_file verbosely (CUnix.make_suffix fname ".v") in
+ read_vernac_file verbosely (CUnix.make_suffix fname ".v");
restore_translator_coqdoc st;
- status
with reraise ->
let reraise = Errors.push reraise in
restore_translator_coqdoc st;
@@ -288,9 +287,9 @@ let rec vernac_com interpfun checknav (loc,com) =
end
| VernacList l ->
- List.fold_left (fun status (_,v) -> interp v && true) true l
+ List.iter (fun (_,v) -> interp v) l
- | v when !just_parsing -> true
+ | v when !just_parsing -> ()
| VernacFail v ->
begin
@@ -304,17 +303,15 @@ let rec vernac_com interpfun checknav (loc,com) =
| e when Errors.noncritical e -> (* In particular e is no anomaly *)
if_verbose msg_info
(str "The command has indeed failed with message:" ++
- fnl () ++ str "=> " ++ hov 0 (Errors.print e));
- true
+ fnl () ++ str "=> " ++ hov 0 (Errors.print e))
end
| VernacTime v ->
let tstart = System.get_time() in
- let status = interp v in
+ interp v;
let tend = System.get_time() in
let msg = if !time then "" else "Finished transaction in " in
- msg_info (str msg ++ System.fmt_time_difference tstart tend);
- status
+ msg_info (str msg ++ System.fmt_time_difference tstart tend)
| VernacTimeout(n,v) ->
current_timeout := Some n;
@@ -327,11 +324,8 @@ let rec vernac_com interpfun checknav (loc,com) =
in
let psh = default_set_timeout () in
try
- let status =
- rollback interpfun Cerrors.process_vernac_interp_error v
- in
+ rollback interpfun Cerrors.process_vernac_interp_error v
restore_timeout psh;
- status
with reraise ->
let reraise = Errors.push reraise in
restore_timeout psh;
@@ -369,26 +363,23 @@ and read_vernac_file verbosely s =
in
let (in_chan, fname, input) =
open_file_twice_if verbosely s in
- let status = ref true in
try
(* we go out of the following infinite loop when a End_of_input is
* raised, which means that we raised the end of the file being loaded *)
while true do
let loc_ast = parse_sentence input in
- let command_status = vernac_com interpfun checknav loc_ast in
- status := !status && command_status;
+ vernac_com interpfun checknav loc_ast;
end_inner_command (snd loc_ast);
pp_flush ()
- done;
- assert false
+ done
with any -> (* whatever the exception *)
let e = Errors.push any in
Format.set_formatter_out_channel stdout;
close_input in_chan input; (* we must close the file first *)
match e with
| End_of_input ->
- if do_beautify () then pr_new_syntax (Loc.make_loc (max_int,max_int)) None;
- !status
+ if do_beautify () then
+ pr_new_syntax (Loc.make_loc (max_int,max_int)) None
| _ -> raise_with_file fname (disable_drop e)
(** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit]
@@ -403,10 +394,9 @@ let checknav loc ast =
user_error loc "Navigation commands forbidden in nested commands"
let eval_expr ?(preserving=false) loc_ast =
- let status = vernac_com Vernacentries.interp checknav loc_ast in
+ vernac_com Vernacentries.interp checknav loc_ast;
if not preserving && not (is_navigation_vernac (snd loc_ast)) then
- Backtrack.mark_command (snd loc_ast);
- status
+ Backtrack.mark_command (snd loc_ast)
(* XML output hooks *)
let xml_start_library = ref (fun _ -> ())
@@ -421,7 +411,7 @@ let load_vernac verb file =
if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout;
try
Lib.mark_end_of_command (); (* in case we're still in coqtop init *)
- let _ = read_vernac_file verb file in
+ read_vernac_file verb file;
if !Flags.beautify_file then close_out !chan_beautify;
with any ->
let e = Errors.push any in
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 9ef3bc28a..379194945 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -26,9 +26,7 @@ val just_parsing : bool ref
Backtrack stack (triggering a save of a frozen state and the generation
of a new state label). An example of state-preserving command is one coming
from the query panel of Coqide. *)
-(* spiwack: return value: [true] if safe (general case), [false] if
- unsafe (like [Admitted]). *)
-val eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> bool
+val eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit
(** Set XML hooks *)
val set_xml_start_library : (unit -> unit) -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 18b5e8029..b1afb3b3e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -44,10 +44,6 @@ let cl_of_qualid = function
let scope_class_of_qualid qid =
Notation.scope_class_of_reference (Smartlocate.smart_global qid)
-(** Vernac commands can raise this [UnsafeSuccess] to notify they
- modified the environment in an unsafe manner, such as [Admitted]. *)
-exception UnsafeSuccess
-
(*******************)
(* "Show" commands *)
@@ -511,7 +507,7 @@ let vernac_end_proof = function
| Admitted ->
Backtrack.mark_unreachable [Pfedit.get_current_proof_name ()];
admit ();
- raise UnsafeSuccess
+ Pp.feedback Interface.AddedAxiom
| Proved (is_opaque,idopt) ->
let prf = Pfedit.get_current_proof_name () in
if is_verbose () && !qed_display_script then show_script ();
@@ -546,7 +542,7 @@ let vernac_assumption locality (local, kind) l nl=
let t,imps = interp_assumption [] c in
declare_assumptions idl is_coe kind t imps false nl && status) true l
in
- if not status then raise UnsafeSuccess
+ if not status then Pp.feedback Interface.AddedAxiom
let vernac_record k finite infer struc binders sort nameopt cfs =
let const = match nameopt with
@@ -810,7 +806,7 @@ let vernac_instance abst locality sup inst props pri =
ignore(Classes.new_instance ~abstract:abst ~global:glob sup inst props pri)
let vernac_context l =
- if not (Classes.context l) then raise UnsafeSuccess
+ if not (Classes.context l) then Pp.feedback Interface.AddedAxiom
let vernac_declare_instances locality ids =
let glob = not (make_section_locality locality) in
@@ -1902,12 +1898,8 @@ let interp c =
try
interp locality c;
if orig_program_mode || not !Flags.program_mode || isprogcmd then
- Flags.program_mode := orig_program_mode;
- true
+ Flags.program_mode := orig_program_mode
with
- | UnsafeSuccess ->
- Flags.program_mode := orig_program_mode;
- false
| reraise ->
let e = Errors.push reraise in
Flags.program_mode := orig_program_mode;
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 027d0bbd0..5a6550d56 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -27,9 +27,7 @@ val show_node : unit -> unit
val get_current_context_of_args : int option -> Evd.evar_map * Environ.env
(** The main interpretation function of vernacular expressions *)
-(* spiwack: return value: [true] if safe (general case), [false] if
- unsafe (like [Admitted]). *)
-val interp : Vernacexpr.vernac_expr -> bool
+val interp : Vernacexpr.vernac_expr -> unit
(** Print subgoals when the verbose flag is on.
Meant to be used inside vernac commands from plugins. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-08 17:05:39 +0000