aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/asyncTaskQueue.ml20
-rw-r--r--stm/asyncTaskQueue.mli2
-rw-r--r--stm/coqworkmgrApi.ml2
-rw-r--r--stm/coqworkmgrApi.mli2
-rw-r--r--stm/dag.ml2
-rw-r--r--stm/dag.mli2
-rw-r--r--stm/lemmas.ml29
-rw-r--r--stm/lemmas.mli3
-rw-r--r--stm/proofworkertop.ml2
-rw-r--r--stm/queryworkertop.ml2
-rw-r--r--stm/spawned.ml15
-rw-r--r--stm/spawned.mli2
-rw-r--r--stm/stm.ml290
-rw-r--r--stm/stm.mli11
-rw-r--r--stm/stm.mllib1
-rw-r--r--stm/tQueue.ml2
-rw-r--r--stm/tQueue.mli2
-rw-r--r--stm/tacworkertop.ml2
-rw-r--r--stm/texmacspp.ml766
-rw-r--r--stm/texmacspp.mli12
-rw-r--r--stm/vcs.ml2
-rw-r--r--stm/vcs.mli2
-rw-r--r--stm/vernac_classifier.ml26
-rw-r--r--stm/vernac_classifier.mli2
-rw-r--r--stm/vio_checking.ml2
-rw-r--r--stm/vio_checking.mli2
-rw-r--r--stm/workerPool.ml2
-rw-r--r--stm/workerPool.mli2
28 files changed, 233 insertions, 976 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index e0315dec52..a7b381ad62 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -104,7 +104,8 @@ module Make(T : Task) = struct
marshal_err ("unmarshal_more_data: "^s)
let report_status ?(id = !Flags.async_proofs_worker_id) s =
- Pp.feedback ~state_id:Stateid.initial (Feedback.WorkerStatus(id, s))
+ let open Feedback in
+ feedback ~id:(State Stateid.initial) (WorkerStatus(id, s))
module Worker = Spawn.Sync(struct end)
@@ -123,7 +124,7 @@ module Make(T : Task) = struct
"-async-proofs-worker-priority";
Flags.string_of_priority !Flags.async_proofs_worker_priority]
| ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
- | ("-async-proofs" |"-toploop" |"-vi2vo"
+ | ("-async-proofs" |"-toploop" |"-vio2vo"
|"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv"
|"-compile" |"-compile-verbose"
|"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl ->
@@ -182,6 +183,13 @@ module Make(T : Task) = struct
let () = Unix.sleep 1 in
kill_if ()
in
+ let kill_if () =
+ try kill_if ()
+ with Sys.Break ->
+ let () = stop_waiting := true in
+ let () = TQueue.broadcast queue in
+ Worker.kill proc
+ in
let _ = Thread.create kill_if () in
try while true do
@@ -295,8 +303,8 @@ module Make(T : Task) = struct
let main_loop () =
let slave_feeder oc fb =
Marshal.to_channel oc (RespFeedback fb) []; flush oc in
- Pp.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
- Pp.log_via_feedback (fun msg -> Richpp.repr (Richpp.richpp_of_pp msg));
+ Feedback.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
+ Feedback.set_logger Feedback.feedback_logger;
Universes.set_remote_new_univ_level (bufferize (fun () ->
marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel;
match unmarshal_more_data (Option.get !slave_ic) with
@@ -312,7 +320,7 @@ module Make(T : Task) = struct
let response = slave_respond request in
report_status "Idle";
marshal_response (Option.get !slave_oc) response;
- Ephemeron.clear ()
+ CEphemeron.clear ()
with
| MarshalError s ->
pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index a3fe4b8c0d..f140f8ed57 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml
index c34d447e60..20d5152aac 100644
--- a/stm/coqworkmgrApi.ml
+++ b/stm/coqworkmgrApi.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli
index 42dd39b927..548958140e 100644
--- a/stm/coqworkmgrApi.mli
+++ b/stm/coqworkmgrApi.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/dag.ml b/stm/dag.ml
index d0515d3ff1..0c7f9f34bd 100644
--- a/stm/dag.ml
+++ b/stm/dag.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/dag.mli b/stm/dag.mli
index 14ccdc9f1a..6b4442df00 100644
--- a/stm/dag.mli
+++ b/stm/dag.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 0a542c9c03..0a63a3a0fe 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -31,6 +31,7 @@ open Reductionops
open Constrexpr
open Constrintern
open Impargs
+open Context.Rel.Declaration
type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
let mk_hook hook = hook
@@ -44,7 +45,8 @@ let call_hook fix_exn hook l c =
let retrieve_first_recthm = function
| VarRef id ->
- (pi2 (Global.lookup_named id),variable_opacity id)
+ let open Context.Named.Declaration in
+ (get_value (Global.lookup_named id),variable_opacity id)
| ConstRef cst ->
let cb = Global.lookup_constant cst in
(Global.body_of_constant_body cb, is_opaque cb)
@@ -107,11 +109,12 @@ let find_mutually_recursive_statements thms =
(fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c))
(Global.env()) hyps in
let ind_hyps =
- List.flatten (List.map_i (fun i (_,b,t) ->
+ List.flatten (List.map_i (fun i decl ->
+ let t = get_type decl in
match kind_of_term t with
| Ind ((kn,_ as ind),u) when
let mind = Global.lookup_mind kn in
- mind.mind_finite <> Decl_kinds.CoFinite && Option.is_empty b ->
+ mind.mind_finite <> Decl_kinds.CoFinite && is_local_assum decl ->
[ind,x,i]
| _ ->
[]) 0 (List.rev whnf_hyp_hds)) in
@@ -147,7 +150,7 @@ let find_mutually_recursive_statements thms =
assert (List.is_empty rest);
(* One occ. of common coind ccls and no common inductive hyps *)
if not (List.is_empty common_same_indhyp) then
- if_verbose msg_info (str "Assuming mutual coinductive statements.");
+ if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
flush_all ();
indccl, true, []
| [], _::_ ->
@@ -155,7 +158,7 @@ let find_mutually_recursive_statements thms =
| ind :: _ ->
if List.distinct_f ind_ord (List.map pi1 ind)
then
- if_verbose msg_info
+ if_verbose Feedback.msg_info
(strbrk
("Coinductive statements do not follow the order of "^
"definition, assuming the proof to be by induction."));
@@ -303,7 +306,7 @@ let admit (id,k,e) pl hook () =
let () = match k with
| Global, _, _ -> ()
| Local, _, _ | Discharge, _, _ ->
- msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++
+ Feedback.msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++
str "declared as an axiom.")
in
let () = assumption_message id in
@@ -333,7 +336,7 @@ let universe_proof_terminator compute_guard hook =
make_terminator begin function
| Admitted (id,k,pe,(ctx,pl)) ->
admit (id,k,pe) pl (hook (Some ctx)) ();
- Pp.feedback Feedback.AddedAxiom
+ Feedback.feedback Feedback.AddedAxiom
| Proved (opaque,idopt,proof) ->
let is_opaque, export_seff, exports = match opaque with
| Vernacexpr.Transparent -> false, true, []
@@ -400,7 +403,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
| Anonymous -> Tactics.intro) (List.rev ids) in
let init_tac,guard = match recguard with
| Some (finite,guard,init_tac) ->
- let rec_tac = Proofview.V82.tactic (rec_tac_initializer finite guard thms snl) in
+ let rec_tac = rec_tac_initializer finite guard thms snl in
Some (match init_tac with
| None ->
if Flags.is_auto_intros () then
@@ -450,7 +453,7 @@ let start_proof_com kind thms hook =
let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
let t', imps' = interp_type_evars_impls ~impls env evdref t in
evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref);
- let ids = List.map pi1 ctx in
+ let ids = List.map get_name ctx in
(compute_proof_name (pi1 kind) sopt,
(nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
(ids, imps @ lift_implicits (List.length ids) imps'),
@@ -517,7 +520,5 @@ let save_proof ?proof = function
(* Miscellaneous *)
let get_current_context () =
- try Pfedit.get_current_goal_context ()
- with e when Logic.catchable_exception e ->
- let env = Global.env () in
- (Evd.from_env env, env)
+ Pfedit.get_current_context ()
+
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index 93f24b42cb..f751598f04 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -65,4 +65,3 @@ val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> uni
and the current global env *)
val get_current_context : unit -> Evd.evar_map * Environ.env
-
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml
index 0e40c345c1..23538a467e 100644
--- a/stm/proofworkertop.ml
+++ b/stm/proofworkertop.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml
index c8e6432bb7..fff6d55434 100644
--- a/stm/queryworkertop.ml
+++ b/stm/queryworkertop.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/spawned.ml b/stm/spawned.ml
index 66fe07dbc4..2eae6f5e24 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -13,19 +13,6 @@ let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
type chandescr = AnonPipe | Socket of string * int * int
-let handshake cin cout =
- try
- match input_value cin with
- | Hello(v, pid) when v = proto_version ->
- prerr_endline (Printf.sprintf "Handshake with %d OK" pid);
- output_value cout (Hello (proto_version,Unix.getpid ())); flush cout
- | _ -> raise (Failure "handshake protocol")
- with
- | Failure s | Invalid_argument s | Sys_error s ->
- pr_err ("Handshake failed: " ^ s); raise (Failure "handshake")
- | End_of_file ->
- pr_err "Handshake failed: End_of_file"; raise (Failure "handshake")
-
let open_bin_connection h pr pw =
let open Unix in
let _, cout = open_connection (ADDR_INET (inet_addr_of_string h,pr)) in
diff --git a/stm/spawned.mli b/stm/spawned.mli
index d0183e081d..acad49f379 100644
--- a/stm/spawned.mli
+++ b/stm/spawned.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/stm.ml b/stm/stm.ml
index e08f69a0e9..e2acb10293 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,8 +8,8 @@
let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
-let prerr_endline s = if false then begin pr_err s end else ()
-let prerr_debug s = if !Flags.debug then begin pr_err s end else ()
+let prerr_endline s = if false then begin pr_err (s ()) end else ()
+let prerr_debug s = if !Flags.debug then begin pr_err (s ()) end else ()
open Vernacexpr
open Errors
@@ -18,6 +18,7 @@ open Names
open Util
open Ppvernac
open Vernac_classifier
+open Feedback
module Hooks = struct
@@ -27,32 +28,30 @@ let with_fail, with_fail_hook = Hook.make ()
let state_computed, state_computed_hook = Hook.make
~default:(fun state_id ~in_cache ->
- feedback ~state_id Feedback.Processed) ()
+ feedback ~id:(State state_id) Processed) ()
let state_ready, state_ready_hook = Hook.make
~default:(fun state_id -> ()) ()
let forward_feedback, forward_feedback_hook = Hook.make
~default:(function
- | { Feedback.id = Feedback.Edit edit_id; route; contents } ->
- feedback ~edit_id ~route contents
- | { Feedback.id = Feedback.State state_id; route; contents } ->
- feedback ~state_id ~route contents) ()
+ | { id = id; route; contents } ->
+ feedback ~id:id ~route contents) ()
let parse_error, parse_error_hook = Hook.make
- ~default:(function
- | Feedback.Edit edit_id -> fun loc msg ->
- feedback ~edit_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))
- | Feedback.State state_id -> fun loc msg ->
- feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) ()
+ ~default:(fun id loc msg ->
+ feedback ~id (ErrorMsg (loc, Pp.string_of_ppcmds msg))) ()
let execution_error, execution_error_hook = Hook.make
~default:(fun state_id loc msg ->
- feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) ()
+ feedback ~id:(State state_id) (ErrorMsg (loc, Pp.string_of_ppcmds msg))) ()
let unreachable_state, unreachable_state_hook = Hook.make
~default:(fun _ _ -> ()) ()
+let tactic_being_run, tactic_being_run_hook = Hook.make
+ ~default:(fun _ -> ()) ()
+
include Hook
(* enables: Hooks.(call foo args) *)
@@ -80,6 +79,20 @@ let async_proofs_workers_extra_env = ref [||]
type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr }
let pr_ast { expr } = pr_vernac expr
+let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
+
+(* Commands piercing opaque *)
+let may_pierce_opaque = function
+ | { expr = VernacPrint (PrintName _) } -> true
+ | { expr = VernacExtend (("Extraction",_), _) } -> true
+ | { expr = VernacExtend (("SeparateExtraction",_), _) } -> true
+ | { expr = VernacExtend (("ExtractionLibrary",_), _) } -> true
+ | { expr = VernacExtend (("RecursiveExtractionLibrary",_), _) } -> true
+ | { expr = VernacExtend (("ExtractionConstant",_), _) } -> true
+ | { expr = VernacExtend (("ExtractionInlinedConstant",_), _) } -> true
+ | { expr = VernacExtend (("ExtractionInductive",_), _) } -> true
+ | _ -> false
+
(* Wrapper for Vernacentries.interp to set the feedback id *)
let vernac_interp ?proof id ?route { verbose; loc; expr } =
let rec internal_command = function
@@ -89,11 +102,11 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
| VernacTime (_,e) | VernacRedirect (_,(_,e)) -> internal_command e
| _ -> false in
if internal_command expr then begin
- prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr))
+ prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr))
end else begin
- set_id_for_feedback ?route (Feedback.State id);
+ set_id_for_feedback ?route (State id);
Aux_file.record_in_aux_set_at loc;
- prerr_endline ("interpreting " ^ string_of_ppcmds(pr_vernac expr));
+ prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr))
with e ->
let e = Errors.push e in
@@ -103,8 +116,8 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
(* Wrapper for Vernac.parse_sentence to set the feedback id *)
let vernac_parse ?newtip ?route eid s =
let feedback_id =
- if Option.is_empty newtip then Feedback.Edit eid
- else Feedback.State (Option.get newtip) in
+ if Option.is_empty newtip then Edit eid
+ else State (Option.get newtip) in
set_id_for_feedback ?route feedback_id;
let pa = Pcoq.Gram.parsable (Stream.of_string s) in
Flags.with_option Flags.we_are_parsing (fun () ->
@@ -121,7 +134,7 @@ let vernac_parse ?newtip ?route eid s =
let pr_open_cur_subgoals () =
try Printer.pr_open_subgoals ()
- with Proof_global.NoCurrentProof -> str""
+ with Proof_global.NoCurrentProof -> Pp.str ""
let update_global_env () =
if Proof_global.there_are_pending_proofs () then
@@ -139,10 +152,10 @@ type branch_type =
proof_mode * Stateid.t * Stateid.t * vernac_qed_type * Vcs_.Branch.t ]
type cmd_t = {
ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *)
- ceff : bool; (* is a side-effecting command *)
+ ceff : bool; (* is a side-effecting command in the middle of a proof *)
cast : ast;
cids : Id.t list;
- cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch ] }
+ cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch | `SkipQueue ] }
type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list
type qed_t = {
qast : ast;
@@ -213,7 +226,7 @@ end = struct (* {{{ *)
let find_proof_at_depth vcs pl =
try List.find (function
| _, { Vcs_.kind = `Proof(m, n) } -> Int.equal n pl
- | _, { Vcs_.kind = `Edit _ } -> anomaly(str"find_proof_at_depth")
+ | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth")
| _ -> false)
(List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs))
with Not_found -> failwith "find_proof_at_depth"
@@ -221,9 +234,9 @@ end = struct (* {{{ *)
exception Expired
let visit vcs id =
if Stateid.equal id Stateid.initial then
- anomaly(str"Visiting the initial state id")
+ anomaly(Pp.str "Visiting the initial state id")
else if Stateid.equal id Stateid.dummy then
- anomaly(str"Visiting the dummy state id")
+ anomaly(Pp.str "Visiting the dummy state id")
else
try
match Vcs_.Dag.from_node (Vcs_.dag vcs) id with
@@ -239,7 +252,7 @@ end = struct (* {{{ *)
| [n, Sideff (Some x); p, Noop]
| [p, Noop; n, Sideff (Some x)]-> { step = `Sideff(`Ast (x,p)); next = n }
| [n, Sideff (Some x)]-> {step = `Sideff(`Ast (x,Stateid.dummy)); next=n}
- | _ -> anomaly (str ("Malformed VCS at node "^Stateid.to_string id))
+ | _ -> anomaly (Pp.str ("Malformed VCS at node "^Stateid.to_string id))
with Not_found -> raise Expired
end (* }}} *)
@@ -298,7 +311,7 @@ module VCS : sig
val proof_nesting : unit -> int
val checkout_shallowest_proof_branch : unit -> unit
- val propagate_sideff : ast option -> unit
+ val propagate_sideff : replay:ast option -> unit
val gc : unit -> unit
@@ -322,10 +335,10 @@ end = struct (* {{{ *)
"stm_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in
let string_of_transaction = function
| Cmd { cast = t } | Fork (t, _,_,_) ->
- (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
+ (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR")
| Sideff (Some t) ->
sprintf "Sideff(%s)"
- (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
+ (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR")
| Sideff None -> "EnvChange"
| Noop -> " "
| Alias (id,_) -> sprintf "Alias(%s)" (Stateid.to_string id)
@@ -463,14 +476,14 @@ end = struct (* {{{ *)
let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with
| h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in
checkout branch;
- prerr_endline ("mode:" ^ mode);
+ prerr_endline (fun () -> "mode:" ^ mode);
Proof_global.activate_proof_mode mode
with Failure _ ->
checkout Branch.master;
- Proof_global.disactivate_proof_mode "Classic"
+ Proof_global.disactivate_current_proof_mode ()
(* copies the transaction on every open branch *)
- let propagate_sideff t =
+ let propagate_sideff ~replay:t =
List.iter (fun b ->
checkout b;
let id = new_node () in
@@ -510,7 +523,10 @@ end = struct (* {{{ *)
let rec fill id =
if (get_info id).state = None then fill (Vcs_aux.visit v id).next
else copy_info_w_state v id in
- fill stop
+ let v = fill stop in
+ (* We put in the new dag the first state (since Qed shall run on it,
+ * see check_task_aux) *)
+ copy_info_w_state v start
let nodes_in_slice ~start ~stop =
List.rev (List.map fst (nodes_in_slice ~start ~stop))
@@ -720,12 +736,12 @@ end = struct (* {{{ *)
let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
f id
=
- feedback ~state_id:id Feedback.(ProcessingIn !Flags.async_proofs_worker_id);
+ feedback ~id:(State id) (ProcessingIn !Flags.async_proofs_worker_id);
let str_id = Stateid.to_string id in
if is_cached id && not redefine then
anomaly (str"defining state "++str str_id++str" twice");
try
- prerr_endline("defining "^str_id^" (cache="^
+ prerr_endline (fun () -> "defining "^str_id^" (cache="^
if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
let good_id = match safe_id with None -> !cur_id | Some id -> id in
fix_exn_ref := exn_on id ~valid:good_id;
@@ -733,7 +749,7 @@ end = struct (* {{{ *)
fix_exn_ref := (fun x -> x);
if cache = `Yes then freeze `No id
else if cache = `Shallow then freeze `Shallow id;
- prerr_endline ("setting cur id to "^str_id);
+ prerr_endline (fun () -> "setting cur id to "^str_id);
cur_id := id;
if feedback_processed then
Hooks.(call state_computed id ~in_cache:false);
@@ -1042,7 +1058,7 @@ end = struct (* {{{ *)
List.iter (fun (id,s) -> State.assign id s) l; `End
| `Fresh, BuildProof { t_assign; t_loc; t_name; t_states; t_drop },
RespBuiltProof (pl, time) ->
- feedback (Feedback.InProgress ~-1);
+ feedback (InProgress ~-1);
t_assign (`Val pl);
record_pb_time t_name t_loc time;
if !Flags.async_proofs_full || t_drop
@@ -1050,7 +1066,7 @@ end = struct (* {{{ *)
else `End
| `Fresh, BuildProof { t_assign; t_loc; t_name; t_states },
RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } ->
- feedback (Feedback.InProgress ~-1);
+ feedback (InProgress ~-1);
let info = Stateid.add ~valid Exninfo.null e_error_at in
let e = (RemoteException e_msg, info) in
t_assign (`Exn e);
@@ -1066,7 +1082,7 @@ end = struct (* {{{ *)
let e = (RemoteException (strbrk s), info) in
t_assign (`Exn e);
Hooks.(call execution_error start Loc.ghost (strbrk s));
- feedback (Feedback.InProgress ~-1)
+ feedback (InProgress ~-1)
let build_proof_here ~drop_pt (id,valid) loc eop =
Future.create (State.exn_on id ~valid) (fun () ->
@@ -1077,7 +1093,7 @@ end = struct (* {{{ *)
Aux_file.record_in_aux_at loc "proof_build_time"
(Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
let p = Proof_global.return_proof ~allow_partial:drop_pt () in
- if drop_pt then Pp.feedback ~state_id:id Feedback.Complete;
+ if drop_pt then feedback ~id:(State id) Complete;
p)
let perform_buildp { Stateid.exn_info; stop; document; loc } drop my_states =
@@ -1115,16 +1131,17 @@ end = struct (* {{{ *)
| Some (safe, err) -> err, safe
| None -> Stateid.dummy, Stateid.dummy in
let e_msg = iprint (e, info) in
- prerr_endline "failed with the following exception:";
- prerr_endline (string_of_ppcmds e_msg);
+ prerr_endline (fun () -> "failed with the following exception:");
+ prerr_endline (fun () -> string_of_ppcmds e_msg);
let e_safe_states = List.filter State.is_cached my_states in
RespError { e_error_at; e_safe_id; e_msg; e_safe_states }
let perform_states query =
if query = [] then [] else
- let is_tac = function
- | VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _ -> true
- | _ -> false in
+ let is_tac e = match classify_vernac e with
+ | VtProofStep _, _ -> true
+ | _ -> false
+ in
let initial =
let rec aux id =
try match VCS.visit id with { next } -> aux next
@@ -1169,7 +1186,7 @@ end = struct (* {{{ *)
"The system state could not be sent to the worker process. "^
"Falling back to local, lazy, evaluation."));
t_assign(`Comp(build_proof_here ~drop_pt t_exn_info t_loc t_stop));
- feedback (Feedback.InProgress ~-1)
+ feedback (InProgress ~-1)
end (* }}} *)
@@ -1249,7 +1266,7 @@ end = struct (* {{{ *)
let (e, info) = Errors.push e in
(try match Stateid.get info with
| None ->
- pperrnl (
+ msg_error (
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
spc () ++ iprint (e, info))
| Some (_, cur) ->
@@ -1259,12 +1276,12 @@ end = struct (* {{{ *)
| { step = `Qed ( { qast = { loc } }, _) }
| { step = `Sideff (`Ast ( { loc }, _)) } ->
let start, stop = Loc.unloc loc in
- pperrnl (
+ msg_error (
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
str ": chars " ++ int start ++ str "-" ++ int stop ++
spc () ++ iprint (e, info))
| _ ->
- pperrnl (
+ msg_error (
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
spc () ++ iprint (e, info))
with e ->
@@ -1324,7 +1341,6 @@ end = struct (* {{{ *)
let set_perspective idl =
ProofTask.set_perspective idl;
TaskQueue.broadcast (Option.get !queue);
- let open Stateid in
let open ProofTask in
let overlap s1 s2 =
List.exists (fun x -> CList.mem_f Stateid.equal x s2) s1 in
@@ -1358,7 +1374,7 @@ end = struct (* {{{ *)
else
let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in
let t_uuid = Future.uuid f in
- feedback (Feedback.InProgress 1);
+ feedback (InProgress 1);
let task = ProofTask.(BuildProof {
t_exn_info; t_start = start; t_stop = stop; t_assign; t_drop = drop_pt;
t_loc = loc; t_uuid; t_name = pname;
@@ -1381,7 +1397,7 @@ end = struct (* {{{ *)
| Some (ReqBuildProof (r, b, _)) -> Some(r, b)
| _ -> None)
tasks in
- prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length reqs));
+ prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs));
reqs
let reset_task_queue () = TaskQueue.clear (Option.get !queue)
@@ -1395,7 +1411,7 @@ and TacTask : sig
t_state : Stateid.t;
t_state_fb : Stateid.t;
t_assign : output Future.assignement -> unit;
- t_ast : ast;
+ t_ast : int * ast;
t_goal : Goal.goal;
t_kill : unit -> unit;
t_name : string }
@@ -1412,7 +1428,7 @@ end = struct (* {{{ *)
t_state : Stateid.t;
t_state_fb : Stateid.t;
t_assign : output Future.assignement -> unit;
- t_ast : ast;
+ t_ast : int * ast;
t_goal : Goal.goal;
t_kill : unit -> unit;
t_name : string }
@@ -1421,7 +1437,7 @@ end = struct (* {{{ *)
r_state : Stateid.t;
r_state_fb : Stateid.t;
r_document : VCS.vcs option;
- r_ast : ast;
+ r_ast : int * ast;
r_goal : Goal.goal;
r_name : string }
@@ -1465,6 +1481,9 @@ end = struct (* {{{ *)
| Some { t_kill } -> t_kill ()
| _ -> ()
+ let command_focus = Proof.new_focus_kind ()
+ let focus_cond = Proof.no_cond command_focus
+
let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } =
Option.iter VCS.restore vcs;
try
@@ -1474,15 +1493,15 @@ end = struct (* {{{ *)
let g = Evd.find sigma0 r_goal in
if not (
Evarutil.is_ground_term sigma0 Evd.(evar_concl g) &&
- List.for_all (fun (_,bo,ty) ->
- Evarutil.is_ground_term sigma0 ty &&
- Option.cata (Evarutil.is_ground_term sigma0) true bo)
- Evd.(evar_context g))
+ List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0))
+ Evd.(evar_context g))
then
Errors.errorlabstrm "Stm" (strbrk("the par: goal selector supports ground "^
"goals only"))
else begin
- vernac_interp r_state_fb r_ast;
+ let (i, ast) = r_ast in
+ Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p);
+ vernac_interp r_state_fb ast;
let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in
match Evd.(evar_body (find sigma r_goal)) with
| Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress")
@@ -1511,12 +1530,11 @@ end = struct (* {{{ *)
module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask)
let vernac_interp cancel nworkers safe_id id { verbose; loc; expr = e } =
- let e, etac, time, fail =
+ let e, time, fail =
let rec find time fail = function
- | VernacSolve(_,_,re,b) -> re, b, time, fail
| VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e
| VernacFail e -> find time true e
- | _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in
+ | _ -> e, time, fail in find false false e in
Hooks.call Hooks.with_fail fail (fun () ->
(if time then System.with_time false else (fun x -> x)) (fun () ->
ignore(TaskQueue.with_n_workers nworkers (fun queue ->
@@ -1528,8 +1546,7 @@ end = struct (* {{{ *)
Future.create_delegate
~name:(Printf.sprintf "subgoal %d" i)
(State.exn_on id ~valid:safe_id) in
- let t_ast =
- { verbose;loc;expr = VernacSolve(SelectNth i,None,e,etac) } in
+ let t_ast = (i, { verbose; loc; expr = e }) in
let t_name = Goal.uid g in
TaskQueue.enqueue_task queue
({ t_state = safe_id; t_state_fb = id;
@@ -1548,7 +1565,7 @@ end = struct (* {{{ *)
with Not_found -> Errors.anomaly(str"Partac: wrong focus") in
if Future.is_over f then
let pt, uc = Future.join f in
- prerr_endline (string_of_ppcmds(hov 0 (
+ prerr_endline (fun () -> string_of_ppcmds(hov 0 (
str"g=" ++ str gid ++ spc () ++
str"t=" ++ (Printer.pr_constr pt) ++ spc () ++
str"uc=" ++ Evd.pr_evar_universe_context uc)));
@@ -1604,11 +1621,11 @@ end = struct (* {{{ *)
Reach.known_state ~cache:`No r_where;
try
vernac_interp r_for { r_what with verbose = true };
- feedback ~state_id:r_for Feedback.Processed
+ feedback ~id:(State r_for) Processed
with e when Errors.noncritical e ->
let e = Errors.push e in
let msg = string_of_ppcmds (iprint e) in
- feedback ~state_id:r_for (Feedback.ErrorMsg (Loc.ghost, msg))
+ feedback ~id:(State r_for) (ErrorMsg (Loc.ghost, msg))
let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
let name_of_request { r_what } = string_of_ppcmds (pr_ast r_what)
@@ -1658,9 +1675,9 @@ let delegate name =
let time = get_hint_bp_time name in
time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio
|| !Flags.async_proofs_full
-
+
let collect_proof keep cur hd brkind id =
- prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
+ prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
let no_name = "" in
let name = function
| [] -> no_name
@@ -1680,16 +1697,20 @@ let collect_proof keep cur hd brkind id =
let has_proof_no_using = function
| Some (_, { expr = VernacProof(_,None) }) -> true
| _ -> false in
- let may_pierce_opaque = function
- | { expr = VernacPrint (PrintName _) } -> true
- | _ -> false in
+ let too_complex_to_delegate = function
+ | { expr = (VernacDeclareModule _
+ | VernacDefineModule _
+ | VernacDeclareModuleType _
+ | VernacInclude _) } -> true
+ | { expr = (VernacRequire _ | VernacImport _) } -> true
+ | ast -> may_pierce_opaque ast in
let parent = function Some (p, _) -> p | None -> assert false in
let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in
let rec collect last accn id =
let view = VCS.visit id in
match view.step with
| (`Sideff (`Ast(x,_)) | `Cmd { cast = x })
- when may_pierce_opaque x -> `Sync(no_name,None,`Print)
+ when too_complex_to_delegate x -> `Sync(no_name,None,`Print)
| `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next
| `Sideff (`Ast(x,_)) -> collect (Some (id,x)) (id::accn) view.next
(* An Alias could jump everywhere... we hope we can ignore it*)
@@ -1757,7 +1778,7 @@ let string_of_reason = function
| `NoPU_NoHint_NoES -> "no 'Proof using..', no .aux file, inside a section"
| `Unknown -> "unsupported case"
-let log_string s = prerr_debug ("STM: " ^ s)
+let log_string s = prerr_debug (fun () -> "STM: " ^ s)
let log_processing_async id name = log_string Printf.(sprintf
"%s: proof %s: asynch" (Stateid.to_string id) name
)
@@ -1779,17 +1800,17 @@ let known_state ?(redefine_qed=false) ~cache id =
Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env ()
in
let rec pure_cherry_pick_non_pstate id = Future.purify (fun id ->
- prerr_endline ("cherry-pick non pstate " ^ Stateid.to_string id);
+ prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
reach id;
cherry_pick_non_pstate ()) id
(* traverses the dag backward from nodes being already calculated *)
and reach ?(redefine_qed=false) ?(cache=cache) id =
- prerr_endline ("reaching: " ^ Stateid.to_string id);
+ prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id);
if not redefine_qed && State.is_cached ~cache id then begin
State.install_cached id;
Hooks.(call state_computed id ~in_cache:true);
- prerr_endline ("reached (cache)")
+ prerr_endline (fun () -> "reached (cache)")
end else
let step, cache_step, feedback_processed =
let view = VCS.visit id in
@@ -1797,19 +1818,26 @@ let known_state ?(redefine_qed=false) ~cache id =
| `Alias (id,_) -> (fun () ->
reach view.next; reach id
), cache, true
+ | `Cmd { cast = x; cqueue = `SkipQueue } -> (fun () ->
+ reach view.next), cache, true
| `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () ->
reach ~cache:`Shallow view.next;
+ Hooks.(call tactic_being_run true);
Partac.vernac_interp
- cancel !Flags.async_proofs_n_tacworkers view.next id x
+ cancel !Flags.async_proofs_n_tacworkers view.next id x;
+ Hooks.(call tactic_being_run false)
), cache, true
| `Cmd { cast = x; cqueue = `QueryQueue cancel }
when Flags.async_proofs_is_master () -> (fun () ->
reach view.next;
Query.vernac_interp cancel view.next id x
), cache, false
- | `Cmd { cast = x; ceff = eff } -> (fun () ->
- reach view.next; vernac_interp id x;
- if eff then update_global_env ()), cache, true
+ | `Cmd { cast = x; ceff = eff; ctac } -> (fun () ->
+ reach view.next;
+ if ctac then Hooks.(call tactic_being_run true);
+ vernac_interp id x;
+ if ctac then Hooks.(call tactic_being_run false);
+ if eff then update_global_env ()), (if eff then `Yes else cache), true
| `Fork ((x,_,_,_), None) -> (fun () ->
reach view.next; vernac_interp id x;
wall_clock_last_fork := Unix.gettimeofday ()
@@ -1865,7 +1893,7 @@ let known_state ?(redefine_qed=false) ~cache id =
if not delegate then ignore(Future.compute fp);
reach view.next;
vernac_interp id ~proof x;
- feedback ~state_id:id Feedback.Incomplete
+ feedback ~id:(State id) Incomplete
| { VCS.kind = `Master }, _ -> assert false
end;
Proof_global.discard_all ()
@@ -1920,7 +1948,7 @@ let known_state ?(redefine_qed=false) ~cache id =
else cache_step in
State.define
~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id;
- prerr_endline ("reached: "^ Stateid.to_string id) in
+ prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
reach ~redefine_qed id
end (* }}} *)
@@ -1935,7 +1963,7 @@ let init () =
Backtrack.record ();
Slaves.init ();
if Flags.async_proofs_is_master () then begin
- prerr_endline "Initializing workers";
+ prerr_endline (fun () -> "Initializing workers");
Query.init ();
let opts = match !Flags.async_proofs_private_flags with
| None -> []
@@ -1987,9 +2015,9 @@ let rec join_admitted_proofs id =
let join () =
finish ();
wait ();
- prerr_endline "Joining the environment";
+ prerr_endline (fun () -> "Joining the environment");
Global.join_safe_environment ();
- prerr_endline "Joining Admitted proofs";
+ prerr_endline (fun () -> "Joining Admitted proofs");
join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ()));
VCS.print ();
VCS.print ()
@@ -2002,7 +2030,6 @@ let check_task name (tasks,rcbackup) i =
let vcs = VCS.backup () in
try
let rc = Future.purify (Slaves.check_task name tasks) i in
- pperr_flush ();
VCS.restore vcs;
rc
with e when Errors.noncritical e -> VCS.restore vcs; false
@@ -2012,7 +2039,6 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
let finish_task u (_,_,i) =
let vcs = VCS.backup () in
let u = Future.purify (Slaves.finish_task name u d p t) i in
- pperr_flush ();
VCS.restore vcs;
u in
try
@@ -2020,7 +2046,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
(u,a,true), p
with e ->
let e = Errors.push e in
- pperrnl (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
+ msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
exit 1
let merge_proof_branch ?valid ?id qast keep brname =
@@ -2065,7 +2091,7 @@ let handle_failure (e, info) vcs tty =
anomaly(str"error with no safe_id attached:" ++ spc() ++
Errors.iprint_no_report (e, info))
| Some (safe_id, id) ->
- prerr_endline ("Failed at state " ^ Stateid.to_string id);
+ prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
VCS.restore vcs;
if tty && interactive () = `Yes then begin
(* We stay on a valid state *)
@@ -2090,13 +2116,14 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
let warn_if_pos a b =
if b then msg_warning(pr_ast a ++ str" should not be part of a script") in
let v, x = expr, { verbose = verbose; loc; expr } in
- prerr_endline ("{{{ processing: "^ string_of_ppcmds (pr_ast x));
+ prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x));
let vcs = VCS.backup () in
try
let head = VCS.current_branch () in
VCS.checkout head;
let rc = begin
- prerr_endline (" classified as: " ^ string_of_vernac_classification c);
+ prerr_endline (fun () ->
+ " classified as: " ^ string_of_vernac_classification c);
match c with
(* PG stuff *)
| VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok
@@ -2132,7 +2159,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
VCS.commit id (Alias (oid,x));
Backtrack.record (); if w == VtNow then finish (); `Ok
| VtStm (VtBack id, false), VtNow ->
- prerr_endline ("undo to state " ^ Stateid.to_string id);
+ prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
Backtrack.backto id;
VCS.checkout_shallowest_proof_branch ();
Reach.known_state ~cache:(interactive ()) id; `Ok
@@ -2157,8 +2184,13 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
let id = VCS.new_node ~id:newtip () in
let queue =
if !Flags.async_proofs_full then `QueryQueue (ref false)
+ else if Flags.(!compilation_mode = BuildVio) &&
+ VCS.((get_branch head).kind = `Master) &&
+ may_pierce_opaque x
+ then `SkipQueue
else `MainQueue in
- VCS.commit id (Cmd {ctac=false;ceff=false;cast = x; cids = []; cqueue = queue });
+ VCS.commit id (Cmd {
+ ctac=false;ceff=false;cast = x; cids = []; cqueue = queue });
Backtrack.record (); if w == VtNow then finish (); `Ok
| VtQuery (false,_), VtLater ->
anomaly(str"classifier: VtQuery + VtLater must imply part_of_script")
@@ -2181,7 +2213,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
anomaly(str"VtProofMode must be executed VtNow")
| VtProofMode mode, VtNow ->
let id = VCS.new_node ~id:newtip () in
- VCS.commit id (Cmd {ctac=false;ceff=false;cast = x;cids=[];cqueue = `MainQueue});
+ VCS.commit id (Cmd {
+ ctac=false;ceff=false;cast = x;cids=[];cqueue = `MainQueue});
List.iter
(fun bn -> match VCS.get_branch bn with
| { VCS.root; kind = `Master; pos } -> ()
@@ -2199,7 +2232,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
| VtProofStep paral, w ->
let id = VCS.new_node ~id:newtip () in
let queue = if paral then `TacQueue (ref false) else `MainQueue in
- VCS.commit id (Cmd {ctac = true;ceff = false;cast = x;cids = [];cqueue = queue });
+ VCS.commit id (Cmd {
+ ctac = true;ceff = false;cast = x;cids = [];cqueue = queue });
Backtrack.record (); if w == VtNow then finish (); `Ok
| VtQed keep, w ->
let valid = if tty then Some(VCS.get_branch_pos head) else None in
@@ -2213,15 +2247,23 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
vernac_interp (VCS.get_branch_pos head) x; `Ok
| VtSideff l, w ->
+ let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
let id = VCS.new_node ~id:newtip () in
VCS.checkout VCS.Branch.master;
- VCS.commit id (Cmd {ctac=false;ceff=true;cast=x;cids=l;cqueue=`MainQueue});
- VCS.propagate_sideff (Some x);
+ VCS.commit id (Cmd {
+ ctac=false;ceff=in_proof;cast=x;cids=l;cqueue=`MainQueue });
+ (* We can't replay a Definition since universes may be differently
+ * inferred. This holds in Coq >= 8.5 *)
+ let replay = match x.expr with
+ | VernacDefinition(_, _, DefineBody _) -> None
+ | _ -> Some x in
+ VCS.propagate_sideff ~replay;
VCS.checkout_shallowest_proof_branch ();
Backtrack.record (); if w == VtNow then finish (); `Ok
(* Unknown: we execute it, check for open goals and propagate sideeff *)
| VtUnknown, VtNow ->
+ let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
let id = VCS.new_node ~id:newtip () in
let head_id = VCS.get_branch_pos head in
Reach.known_state ~cache:`Yes head_id; (* ensure it is ok *)
@@ -2231,17 +2273,23 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
Reach.known_state ~cache:(interactive ()) mid;
vernac_interp id x;
(* Vernac x may or may not start a proof *)
- if VCS.Branch.equal head VCS.Branch.master &&
- Proof_global.there_are_pending_proofs ()
- then begin
+ if not in_proof && Proof_global.there_are_pending_proofs () then
+ begin
let bname = VCS.mk_branch_name x in
- VCS.commit id (Fork (x,bname,Doesn'tGuaranteeOpacity,[]));
- VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1));
- Proof_global.activate_proof_mode "Classic";
+ let opacity_of_produced_term =
+ match x.expr with
+ (* This AST is ambiguous, hence we check it dynamically *)
+ | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity
+ | _ -> Doesn'tGuaranteeOpacity in
+ VCS.commit id (Fork (x,bname,opacity_of_produced_term,[]));
+ let proof_mode = default_proof_mode () in
+ VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1));
+ Proof_global.activate_proof_mode proof_mode;
end else begin
- VCS.commit id (Cmd {ctac = false; ceff = true;
- cast = x; cids = []; cqueue = `MainQueue});
- VCS.propagate_sideff (Some x);
+ VCS.commit id (Cmd {
+ ctac=false;ceff=in_proof;cast=x;cids=[];cqueue=`MainQueue });
+ (* We hope it can be replayed, but we can't really know *)
+ VCS.propagate_sideff ~replay:(Some x);
VCS.checkout_shallowest_proof_branch ();
end in
State.define ~safe_id:head_id ~cache:`Yes step id;
@@ -2259,25 +2307,20 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
expr = VernacShow (ShowGoal OpenSubgoals) }
| _ -> ()
end;
- prerr_endline "processed }}}";
+ prerr_endline (fun () -> "processed }}}");
VCS.print ();
rc
with e ->
let e = Errors.push e in
handle_failure e vcs tty
-let print_ast id =
- try
- match VCS.visit id with
- | { step = `Cmd { cast = { loc; expr } } }
- | { step = `Fork (({ loc; expr }, _, _, _), _) }
- | { step = `Qed ({ qast = { loc; expr } }, _) } ->
- let xml =
- try Texmacspp.tmpp expr loc
- with e -> Xml_datatype.PCData ("ERROR " ^ Printexc.to_string e) in
- xml;
- | _ -> Xml_datatype.PCData "ERROR"
- with _ -> Xml_datatype.PCData "ERROR"
+let get_ast id =
+ match VCS.visit id with
+ | { step = `Cmd { cast = { loc; expr } } }
+ | { step = `Fork (({ loc; expr }, _, _, _), _) }
+ | { step = `Qed ({ qast = { loc; expr } }, _) } ->
+ Some (expr, loc)
+ | _ -> None
let stop_worker n = Slaves.cancel_worker n
@@ -2303,7 +2346,7 @@ type focus = {
tip : Stateid.t
}
-let query ~at ?(report_with=(Stateid.dummy,Feedback.default_route)) s =
+let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
Future.purify (fun s ->
if Stateid.equal at Stateid.dummy then finish ()
else Reach.known_state ~cache:`Yes at;
@@ -2437,7 +2480,7 @@ let edit_at id =
anomaly (str ("edit_at "^Stateid.to_string id^": ") ++
Errors.print_no_report e)
| Some (_, id) ->
- prerr_endline ("Failed at state " ^ Stateid.to_string id);
+ prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
VCS.restore vcs;
VCS.print ();
iraise (e, info)
@@ -2589,4 +2632,5 @@ let interp_hook = Hooks.interp_hook
let with_fail_hook = Hooks.with_fail_hook
let unreachable_state_hook = Hooks.unreachable_state_hook
let get_fix_exn () = !State.fix_exn_ref
+let tactic_being_run_hook = Hooks.tactic_being_run_hook
(* vim:set foldmethod=marker: *)
diff --git a/stm/stm.mli b/stm/stm.mli
index 2c9b983ec1..6ffe0beb44 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -76,7 +76,9 @@ val get_current_state : unit -> Stateid.t
(* Misc *)
val init : unit -> unit
-val print_ast : Stateid.t -> Xml_datatype.xml
+
+(* This returns the node at that position *)
+val get_ast : Stateid.t -> (Vernacexpr.vernac_expr * Loc.t) option
(* Filename *)
val set_compilation_hints : string -> unit
@@ -108,6 +110,9 @@ val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t
(* ready means that master has it at hand *)
val state_ready_hook : (Stateid.t -> unit) Hook.t
+(* called with true before and with false after a tactic explicitly
+ * in the document is run *)
+val tactic_being_run_hook : (bool -> unit) Hook.t
(* Messages from the workers to the master *)
val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t
@@ -122,7 +127,7 @@ val state_of_id : Stateid.t -> [ `Valid of state option | `Expired ]
(** read-eval-print loop compatible interface ****************************** **)
(* Adds a new line to the document. It replaces the core of Vernac.interp.
- [finish] is called as the last bit of this function is the system
+ [finish] is called as the last bit of this function if the system
is running interactively (-emacs or coqtop). *)
val interp : bool -> vernac_expr located -> unit
@@ -132,7 +137,7 @@ val get_all_proof_names : unit -> Id.t list
val get_current_proof_name : unit -> Id.t option
val show_script : ?proof:Proof_global.closed_proof -> unit -> unit
-(** Reverse dependency hooks *)
+(* Hooks to be set by other Coq components in order to break file cycles *)
val process_error_hook : Future.fix_exn Hook.t
val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof ->
Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 92b3a869a9..bd792b01f6 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -7,6 +7,5 @@ Vernac_classifier
Lemmas
CoqworkmgrApi
AsyncTaskQueue
-Texmacspp
Stm
Vio_checking
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index 2dad962bec..ee121c46a2 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/tQueue.mli b/stm/tQueue.mli
index 1df52d2523..27eca12aff 100644
--- a/stm/tQueue.mli
+++ b/stm/tQueue.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml
index c1a37fed91..d5333d1077 100644
--- a/stm/tacworkertop.ml
+++ b/stm/tacworkertop.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
deleted file mode 100644
index 70eccc2403..0000000000
--- a/stm/texmacspp.ml
+++ /dev/null
@@ -1,766 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Xml_datatype
-open Vernacexpr
-open Constrexpr
-open Names
-open Misctypes
-open Bigint
-open Decl_kinds
-open Extend
-open Libnames
-
-let unlock loc =
- let start, stop = Loc.unloc loc in
- (string_of_int start, string_of_int stop)
-
-let xmlWithLoc loc ename attr xml =
- let start, stop = unlock loc in
- Element(ename, [ "begin", start; "end", stop ] @ attr, xml)
-
-let get_fst_attr_in_xml_list attr xml_list =
- let attrs_list =
- List.map (function
- | Element (_, attrs, _) -> (List.filter (fun (a,_) -> a = attr) attrs)
- | _ -> [])
- xml_list in
- match List.flatten attrs_list with
- | [] -> (attr, "")
- | l -> (List.hd l)
-
-let backstep_loc xmllist =
- let start_att = get_fst_attr_in_xml_list "begin" xmllist in
- let stop_att = get_fst_attr_in_xml_list "end" (List.rev xmllist) in
- [start_att ; stop_att]
-
-let compare_begin_att xml1 xml2 =
- let att1 = get_fst_attr_in_xml_list "begin" [xml1] in
- let att2 = get_fst_attr_in_xml_list "begin" [xml2] in
- match att1, att2 with
- | (_, s1), (_, s2) when s1 == "" || s2 == "" -> 0
- | (_, s1), (_, s2) when int_of_string s1 > int_of_string s2 -> 1
- | (_, s1), (_, s2) when int_of_string s1 < int_of_string s2 -> -1
- | _ -> 0
-
-let xmlBeginSection loc name = xmlWithLoc loc "beginsection" ["name", name] []
-
-let xmlEndSegment loc name = xmlWithLoc loc "endsegment" ["name", name] []
-
-let xmlThm typ name loc xml =
- xmlWithLoc loc "theorem" ["type", typ; "name", name] xml
-
-let xmlDef typ name loc xml =
- xmlWithLoc loc "definition" ["type", typ; "name", name] xml
-
-let xmlNotation attr name loc xml =
- xmlWithLoc loc "notation" (("name", name) :: attr) xml
-
-let xmlReservedNotation attr name loc =
- xmlWithLoc loc "reservednotation" (("name", name) :: attr) []
-
-let xmlCst name ?(attr=[]) loc =
- xmlWithLoc loc "constant" (("name", name) :: attr) []
-
-let xmlOperator name ?(attr=[]) ?(pprules=[]) loc =
- xmlWithLoc loc "operator"
- (("name", name) :: List.map (fun (a,b) -> "format"^a,b) pprules @ attr) []
-
-let xmlApply loc ?(attr=[]) xml = xmlWithLoc loc "apply" attr xml
-
-let xmlToken loc ?(attr=[]) xml = xmlWithLoc loc "token" attr xml
-
-let xmlTyped xml = Element("typed", (backstep_loc xml), xml)
-
-let xmlReturn ?(attr=[]) xml = Element("return", attr, xml)
-
-let xmlCase xml = Element("case", [], xml)
-
-let xmlScrutinee ?(attr=[]) xml = Element("scrutinee", attr, xml)
-
-let xmlWith xml = Element("with", [], xml)
-
-let xmlAssign id xml = Element("assign", ["target",string_of_id id], [xml])
-
-let xmlInductive kind loc xml = xmlWithLoc loc "inductive" ["kind",kind] xml
-
-let xmlCoFixpoint xml = Element("cofixpoint", [], xml)
-
-let xmlFixpoint xml = Element("fixpoint", [], xml)
-
-let xmlCheck loc xml = xmlWithLoc loc "check" [] xml
-
-let xmlAssumption kind loc xml = xmlWithLoc loc "assumption" ["kind",kind] xml
-
-let xmlComment loc xml = xmlWithLoc loc "comment" [] xml
-
-let xmlCanonicalStructure attr loc = xmlWithLoc loc "canonicalstructure" attr []
-
-let xmlQed ?(attr=[]) loc = xmlWithLoc loc "qed" attr []
-
-let xmlPatvar id loc = xmlWithLoc loc "patvar" ["id", id] []
-
-let xmlReference ref =
- let name = Libnames.string_of_reference ref in
- let i, j = Loc.unloc (Libnames.loc_of_reference ref) in
- let b, e = string_of_int i, string_of_int j in
- Element("reference",["name", name; "begin", b; "end", e] ,[])
-
-let xmlRequire loc ?(attr=[]) xml = xmlWithLoc loc "require" attr xml
-let xmlImport loc ?(attr=[]) xml = xmlWithLoc loc "import" attr xml
-
-let xmlAddLoadPath loc ?(attr=[]) xml = xmlWithLoc loc "addloadpath" attr xml
-let xmlRemoveLoadPath loc ?(attr=[]) = xmlWithLoc loc "removeloadpath" attr
-let xmlAddMLPath loc ?(attr=[]) = xmlWithLoc loc "addmlpath" attr
-
-let xmlExtend loc xml = xmlWithLoc loc "extend" [] xml
-
-let xmlScope loc action ?(attr=[]) name xml =
- xmlWithLoc loc "scope" (["name",name;"action",action] @ attr) xml
-
-let xmlProofMode loc name = xmlWithLoc loc "proofmode" ["name",name] []
-
-let xmlProof loc xml = xmlWithLoc loc "proof" [] xml
-
-let xmlRawTactic name rtac =
- Element("rawtactic", ["name",name],
- [PCData (Pp.string_of_ppcmds (Pptactic.pr_raw_tactic rtac))])
-
-let xmlSectionSubsetDescr name ssd =
- Element("sectionsubsetdescr",["name",name],
- [PCData (Proof_using.to_string ssd)])
-
-let xmlDeclareMLModule loc s =
- xmlWithLoc loc "declarexmlmodule" []
- (List.map (fun x -> Element("path",["value",x],[])) s)
-
-(* tactics *)
-let xmlLtac loc xml = xmlWithLoc loc "ltac" [] xml
-
-(* toplevel commands *)
-let xmlGallina loc xml = xmlWithLoc loc "gallina" [] xml
-
-let xmlTODO loc x =
- xmlWithLoc loc "todo" [] [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
-let string_of_name n =
- match n with
- | Anonymous -> "_"
- | Name id -> Id.to_string id
-
-let string_of_glob_sort s =
- match s with
- | GProp -> "Prop"
- | GSet -> "Set"
- | GType _ -> "Type"
-
-let string_of_cast_sort c =
- match c with
- | CastConv _ -> "CastConv"
- | CastVM _ -> "CastVM"
- | CastNative _ -> "CastNative"
- | CastCoerce -> "CastCoerce"
-
-let string_of_case_style s =
- match s with
- | LetStyle -> "Let"
- | IfStyle -> "If"
- | LetPatternStyle -> "LetPattern"
- | MatchStyle -> "Match"
- | RegularStyle -> "Regular"
-
-let attribute_of_syntax_modifier sm =
-match sm with
- | SetItemLevel (sl, NumLevel n) ->
- List.map (fun s -> ("itemlevel", s)) sl @ ["level", string_of_int n]
- | SetItemLevel (sl, NextLevel) ->
- List.map (fun s -> ("itemlevel", s)) sl @ ["level", "next"]
- | SetLevel i -> ["level", string_of_int i]
- | SetAssoc a ->
- begin match a with
- | NonA -> ["",""]
- | RightA -> ["associativity", "right"]
- | LeftA -> ["associativity", "left"]
- end
- | SetEntryType (s, _) -> ["entrytype", s]
- | SetOnlyParsing v -> ["compat", Flags.pr_version v]
- | SetFormat (system, (loc, s)) ->
- let start, stop = unlock loc in
- ["format-"^system, s; "begin", start; "end", stop]
-
-let string_of_assumption_kind l a many =
- match l, a, many with
- | (Discharge, Logical, true) -> "Hypotheses"
- | (Discharge, Logical, false) -> "Hypothesis"
- | (Discharge, Definitional, true) -> "Variables"
- | (Discharge, Definitional, false) -> "Variable"
- | (Global, Logical, true) -> "Axioms"
- | (Global, Logical, false) -> "Axiom"
- | (Global, Definitional, true) -> "Parameters"
- | (Global, Definitional, false) -> "Parameter"
- | (Local, Logical, true) -> "Local Axioms"
- | (Local, Logical, false) -> "Local Axiom"
- | (Local, Definitional, true) -> "Local Parameters"
- | (Local, Definitional, false) -> "Local Parameter"
- | (Global, Conjectural, _) -> "Conjecture"
- | ((Discharge | Local), Conjectural, _) -> assert false
-
-let rec pp_bindlist bl =
- let tlist =
- List.flatten
- (List.map
- (fun (loc_names, _, e) ->
- let names =
- (List.map
- (fun (loc, name) ->
- xmlCst (string_of_name name) loc) loc_names) in
- match e with
- | CHole _ -> names
- | _ -> names @ [pp_expr e])
- bl) in
- match tlist with
- | [e] -> e
- | l -> xmlTyped l
-and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *)
- Element ("decl_notation", ["name", s], [pp_expr ce])
-and pp_local_binder lb = (* don't know what it is for now *)
- match lb with
- | LocalRawDef ((_, nam), ce) ->
- let attrs = ["name", string_of_name nam] in
- pp_expr ~attr:attrs ce
- | LocalRawAssum (namll, _, ce) ->
- let ppl =
- List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in
- xmlTyped (ppl @ [pp_expr ce])
-and pp_local_decl_expr lde = (* don't know what it is for now *)
- match lde with
- | AssumExpr (_, ce) -> pp_expr ce
- | DefExpr (_, ce, _) -> pp_expr ce
-and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) =
- (* inductive_expr *)
- let b,e = Loc.unloc l in
- let location = ["begin", string_of_int b; "end", string_of_int e] in
- [Element ("lident", ["name", Id.to_string id] @ location, [])] @ (* inductive name *)
- begin match cl_or_rdexpr with
- | Constructors coel -> List.map (fun (_, (_, ce)) -> pp_expr ce) coel
- | RecordDecl (_, ldewwwl) ->
- List.map (fun (((_, x), _), _) -> pp_local_decl_expr x) ldewwwl
- end @
- begin match ceo with (* don't know what it is for now *)
- | Some ce -> [pp_expr ce]
- | None -> []
- end @
- (List.map pp_local_binder lbl)
-and pp_recursion_order_expr optid roe = (* don't know what it is for now *)
- let attrs =
- match optid with
- | None -> []
- | Some (loc, id) ->
- let start, stop = unlock loc in
- ["begin", start; "end", stop ; "name", Id.to_string id] in
- let kind, expr =
- match roe with
- | CStructRec -> "struct", []
- | CWfRec e -> "rec", [pp_expr e]
- | CMeasureRec (e, None) -> "mesrec", [pp_expr e]
- | CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in
- Element ("recursion_order", ["kind", kind] @ attrs, expr)
-and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) =
- (* fixpoint_expr *)
- let start, stop = unlock loc in
- let id = Id.to_string id in
- [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
- (* fixpoint name *)
- [pp_recursion_order_expr optid roe] @
- (List.map pp_local_binder lbl) @
- [pp_expr ce] @
- begin match ceo with (* don't know what it is for now *)
- | Some ce -> [pp_expr ce]
- | None -> []
- end
-and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
- (* Nota: it is like fixpoint_expr without (optid, roe)
- * so could be merged if there is no more differences *)
- let start, stop = unlock loc in
- let id = Id.to_string id in
- [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
- (* cofixpoint name *)
- (List.map pp_local_binder lbl) @
- [pp_expr ce] @
- begin match ceo with (* don't know what it is for now *)
- | Some ce -> [pp_expr ce]
- | None -> []
- end
-and pp_lident (loc, id) = xmlCst (Id.to_string id) loc
-and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce]
-and pp_cases_pattern_expr cpe =
- match cpe with
- | CPatAlias (loc, cpe, id) ->
- xmlApply loc
- (xmlOperator "alias" ~attr:["name", string_of_id id] loc ::
- [pp_cases_pattern_expr cpe])
- | CPatCstr (loc, ref, cpel1, cpel2) ->
- xmlApply loc
- (xmlOperator "reference"
- ~attr:["name", Libnames.string_of_reference ref] loc ::
- [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1));
- Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
- | CPatAtom (loc, optr) ->
- let attrs = match optr with
- | None -> []
- | Some r -> ["name", Libnames.string_of_reference r] in
- xmlApply loc (xmlOperator "atom" ~attr:attrs loc :: [])
- | CPatOr (loc, cpel) ->
- xmlApply loc (xmlOperator "or" loc :: List.map pp_cases_pattern_expr cpel)
- | CPatNotation (loc, n, (subst_constr, subst_rec), cpel) ->
- xmlApply loc
- (xmlOperator "notation" loc ::
- [xmlOperator n loc;
- Element ("subst", [],
- [Element ("subterms", [],
- List.map pp_cases_pattern_expr subst_constr);
- Element ("recsubterms", [],
- List.map
- (fun (cpel) ->
- Element ("recsubterm", [],
- List.map pp_cases_pattern_expr cpel))
- subst_rec)]);
- Element ("args", [], (List.map pp_cases_pattern_expr cpel))])
- | CPatPrim (loc, tok) -> pp_token loc tok
- | CPatRecord (loc, rcl) ->
- xmlApply loc
- (xmlOperator "record" loc ::
- List.map (fun (r, cpe) ->
- Element ("field",
- ["reference", Libnames.string_of_reference r],
- [pp_cases_pattern_expr cpe]))
- rcl)
- | CPatDelimiters (loc, delim, cpe) ->
- xmlApply loc
- (xmlOperator "delimiter" ~attr:["name", delim] loc ::
- [pp_cases_pattern_expr cpe])
-and pp_case_expr (e, name, pat) =
- match name, pat with
- | None, None -> xmlScrutinee [pp_expr e]
- | Some (loc, name), None ->
- let start, stop= unlock loc in
- xmlScrutinee ~attr:["name", string_of_name name;
- "begin", start; "end", stop] [pp_expr e]
- | Some (loc, name), Some p ->
- let start, stop= unlock loc in
- xmlScrutinee ~attr:["name", string_of_name name;
- "begin", start; "end", stop]
- [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
- | None, Some p ->
- xmlScrutinee [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
-and pp_branch_expr_list bel =
- xmlWith
- (List.map
- (fun (_, cpel, e) ->
- let ppcepl =
- List.map pp_cases_pattern_expr (List.flatten (List.map snd cpel)) in
- let ppe = [pp_expr e] in
- xmlCase (ppcepl @ ppe))
- bel)
-and pp_token loc tok =
- let tokstr =
- match tok with
- | String s -> PCData s
- | Numeral n -> PCData (to_string n) in
- xmlToken loc [tokstr]
-and pp_local_binder_list lbl =
- let l = (List.map pp_local_binder lbl) in
- Element ("recurse", (backstep_loc l), l)
-and pp_const_expr_list cel =
- let l = List.map pp_expr cel in
- Element ("recurse", (backstep_loc l), l)
-and pp_expr ?(attr=[]) e =
- match e with
- | CRef (r, _) ->
- xmlCst ~attr
- (Libnames.string_of_reference r) (Libnames.loc_of_reference r)
- | CProdN (loc, bl, e) ->
- xmlApply loc
- (xmlOperator "forall" loc :: [pp_bindlist bl] @ [pp_expr e])
- | CApp (loc, (_, hd), args) ->
- xmlApply ~attr loc (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args)
- | CAppExpl (loc, (_, r, _), args) ->
- xmlApply ~attr loc
- (xmlCst (Libnames.string_of_reference r)
- (Libnames.loc_of_reference r) :: List.map pp_expr args)
- | CNotation (loc, notation, ([],[],[])) ->
- xmlOperator notation loc
- | CNotation (loc, notation, (args, cell, lbll)) ->
- let fmts = Notation.find_notation_extra_printing_rules notation in
- let oper = xmlOperator notation loc ~pprules:fmts in
- let cels = List.map pp_const_expr_list cell in
- let lbls = List.map pp_local_binder_list lbll in
- let args = List.map pp_expr args in
- xmlApply loc (oper :: (List.sort compare_begin_att (args @ cels @ lbls)))
- | CSort(loc, s) ->
- xmlOperator (string_of_glob_sort s) loc
- | CDelimiters (loc, scope, ce) ->
- xmlApply loc (xmlOperator "delimiter" ~attr:["name", scope] loc ::
- [pp_expr ce])
- | CPrim (loc, tok) -> pp_token loc tok
- | CGeneralization (loc, kind, _, e) ->
- let kind= match kind with
- | Explicit -> "explicit"
- | Implicit -> "implicit" in
- xmlApply loc
- (xmlOperator "generalization" ~attr:["kind", kind] loc :: [pp_expr e])
- | CCast (loc, e, tc) ->
- begin match tc with
- | CastConv t | CastVM t |CastNative t ->
- xmlApply loc
- (xmlOperator ":" loc ~attr:["kind", (string_of_cast_sort tc)] ::
- [pp_expr e; pp_expr t])
- | CastCoerce ->
- xmlApply loc
- (xmlOperator ":" loc ~attr:["kind", "CastCoerce"] ::
- [pp_expr e])
- end
- | CEvar (loc, ek, cel) ->
- let ppcel = List.map (fun (id,e) -> xmlAssign id (pp_expr e)) cel in
- xmlApply loc
- (xmlOperator "evar" loc ~attr:["id", string_of_id ek] ::
- ppcel)
- | CPatVar (loc, id) -> xmlPatvar (string_of_id id) loc
- | CHole (loc, _, _, _) -> xmlCst ~attr "_" loc
- | CIf (loc, test, (_, ret), th, el) ->
- let return = match ret with
- | None -> []
- | Some r -> [xmlReturn [pp_expr r]] in
- xmlApply loc
- (xmlOperator "if" loc ::
- return @ [pp_expr th] @ [pp_expr el])
- | CLetTuple (loc, names, (_, ret), value, body) ->
- let return = match ret with
- | None -> []
- | Some r -> [xmlReturn [pp_expr r]] in
- xmlApply loc
- (xmlOperator "lettuple" loc ::
- return @
- (List.map (fun (loc, var) -> xmlCst (string_of_name var) loc) names) @
- [pp_expr value; pp_expr body])
- | CCases (loc, sty, ret, cel, bel) ->
- let return = match ret with
- | None -> []
- | Some r -> [xmlReturn [pp_expr r]] in
- xmlApply loc
- (xmlOperator "match" loc ~attr:["style", (string_of_case_style sty)] ::
- (return @
- [Element ("scrutinees", [], List.map pp_case_expr cel)] @
- [pp_branch_expr_list bel]))
- | CRecord (_, _) -> assert false
- | CLetIn (loc, (varloc, var), value, body) ->
- xmlApply loc
- (xmlOperator "let" loc ::
- [xmlCst (string_of_name var) varloc; pp_expr value; pp_expr body])
- | CLambdaN (loc, bl, e) ->
- xmlApply loc
- (xmlOperator "lambda" loc :: [pp_bindlist bl] @ [pp_expr e])
- | CCoFix (_, _, _) -> assert false
- | CFix (loc, lid, fel) ->
- xmlApply loc
- (xmlOperator "fix" loc ::
- List.flatten (List.map
- (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d))
- fel))
-
-let pp_comment (c) =
- match c with
- | CommentConstr e -> [pp_expr e]
- | CommentString s -> [Element ("string", [], [PCData s])]
- | CommentInt i -> [PCData (string_of_int i)]
-
-let rec tmpp v loc =
- match v with
- (* Control *)
- | VernacLoad (verbose,f) ->
- xmlWithLoc loc "load" ["verbose",string_of_bool verbose;"file",f] []
- | VernacTime (loc,e) ->
- xmlApply loc (Element("time",[],[]) ::
- [tmpp e loc])
- | VernacRedirect (s, (loc,e)) ->
- xmlApply loc (Element("redirect",["path", s],[]) ::
- [tmpp e loc])
- | VernacTimeout (s,e) ->
- xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
- [tmpp e loc])
- | VernacFail e -> xmlApply loc (Element("fail",[],[]) :: [tmpp e loc])
- | VernacError _ -> xmlWithLoc loc "error" [] []
-
- (* Syntax *)
- | VernacTacticNotation _ as x ->
- xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
- | VernacSyntaxExtension (_, ((_, name), sml)) ->
- let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
- xmlReservedNotation attrs name loc
-
- | VernacOpenCloseScope (_,(true,name)) -> xmlScope loc "open" name []
- | VernacOpenCloseScope (_,(false,name)) -> xmlScope loc "close" name []
- | VernacDelimiters (name,Some tag) ->
- xmlScope loc "delimit" name ~attr:["delimiter",tag] []
- | VernacDelimiters (name,None) ->
- xmlScope loc "undelimit" name ~attr:[] []
- | VernacBindScope (name,l) ->
- xmlScope loc "bind" name
- (List.map (function
- | ByNotation(loc,name,None) -> xmlNotation [] name loc []
- | ByNotation(loc,name,Some d) ->
- xmlNotation ["delimiter",d] name loc []
- | AN ref -> xmlReference ref) l)
- | VernacInfix (_,((_,name),sml),ce,sn) ->
- let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
- let sc_attr =
- match sn with
- | Some scope -> ["scope", scope]
- | None -> [] in
- xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
- | VernacNotation (_, ce, (lstr, sml), sn) ->
- let name = snd lstr in
- let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
- let sc_attr =
- match sn with
- | Some scope -> ["scope", scope]
- | None -> [] in
- xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
- | VernacNotationAddFormat _ as x -> xmlTODO loc x
- | VernacUniverse _
- | VernacConstraint _
- | VernacPolymorphic (_, _) as x -> xmlTODO loc x
- (* Gallina *)
- | VernacDefinition (ldk, ((_,id),_), de) ->
- let l, dk =
- match ldk with
- | Some l, dk -> (l, dk)
- | None, dk -> (Global, dk) in (* Like in ppvernac.ml, l 585 *)
- let e =
- match de with
- | ProveBody (_, ce) -> ce
- | DefineBody (_, Some _, ce, None) -> ce
- | DefineBody (_, None , ce, None) -> ce
- | DefineBody (_, Some _, ce, Some _) -> ce
- | DefineBody (_, None , ce, Some _) -> ce in
- let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
- let str_id = Id.to_string id in
- (xmlDef str_dk str_id loc [pp_expr e])
- | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) ->
- let str_tk = Kindops.string_of_theorem_kind tk in
- let str_id = Id.to_string id in
- (xmlThm str_tk str_id loc [pp_expr statement])
- | VernacStartTheoremProof _ as x -> xmlTODO loc x
- | VernacEndProof pe ->
- begin
- match pe with
- | Admitted -> xmlQed loc
- | Proved (_, Some ((_, id), Some tk)) ->
- let nam = Id.to_string id in
- let typ = Kindops.string_of_theorem_kind tk in
- xmlQed ~attr:["name", nam; "type", typ] loc
- | Proved (_, Some ((_, id), None)) ->
- let nam = Id.to_string id in
- xmlQed ~attr:["name", nam] loc
- | Proved _ -> xmlQed loc
- end
- | VernacExactProof _ as x -> xmlTODO loc x
- | VernacAssumption ((l, a), _, sbwcl) ->
- let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in
- let many =
- List.length (List.flatten (List.map fst binders)) > 1 in
- let exprs =
- List.flatten (List.map pp_simple_binder binders) in
- let l = match l with Some x -> x | None -> Decl_kinds.Global in
- let kind = string_of_assumption_kind l a many in
- xmlAssumption kind loc exprs
- | VernacInductive (_, _, iednll) ->
- let kind =
- let (_, _, _, k, _),_ = List.hd iednll in
- begin
- match k with
- | Record -> "Record"
- | Structure -> "Structure"
- | Inductive_kw -> "Inductive"
- | CoInductive -> "CoInductive"
- | Class _ -> "Class"
- | Variant -> "Variant"
- end in
- let exprs =
- List.flatten (* should probably not be flattened *)
- (List.map
- (fun (ie, dnl) -> (pp_inductive_expr ie) @
- (List.map pp_decl_notation dnl)) iednll) in
- xmlInductive kind loc exprs
- | VernacFixpoint (_, fednll) ->
- let exprs =
- List.flatten (* should probably not be flattened *)
- (List.map
- (fun (fe, dnl) -> (pp_fixpoint_expr fe) @
- (List.map pp_decl_notation dnl)) fednll) in
- xmlFixpoint exprs
- | VernacCoFixpoint (_, cfednll) ->
- (* Nota: it is like VernacFixpoint without so could be merged *)
- let exprs =
- List.flatten (* should probably not be flattened *)
- (List.map
- (fun (cfe, dnl) -> (pp_cofixpoint_expr cfe) @
- (List.map pp_decl_notation dnl)) cfednll) in
- xmlCoFixpoint exprs
- | VernacScheme _ as x -> xmlTODO loc x
- | VernacCombinedScheme _ as x -> xmlTODO loc x
-
- (* Gallina extensions *)
- | VernacBeginSection (_, id) -> xmlBeginSection loc (Id.to_string id)
- | VernacEndSegment (_, id) -> xmlEndSegment loc (Id.to_string id)
- | VernacNameSectionHypSet _ as x -> xmlTODO loc x
- | VernacRequire (from, import, l) ->
- let import = match import with
- | None -> []
- | Some true -> ["export","true"]
- | Some false -> ["import","true"]
- in
- let from = match from with
- | None -> []
- | Some r -> ["from", Libnames.string_of_reference r]
- in
- xmlRequire loc ~attr:(from @ import) (List.map (fun ref ->
- xmlReference ref) l)
- | VernacImport (true,l) ->
- xmlImport loc ~attr:["export","true"] (List.map (fun ref ->
- xmlReference ref) l)
- | VernacImport (false,l) ->
- xmlImport loc (List.map (fun ref ->
- xmlReference ref) l)
- | VernacCanonical r ->
- let attr =
- match r with
- | AN (Qualid (_, q)) -> ["qualid", string_of_qualid q]
- | AN (Ident (_, id)) -> ["id", Id.to_string id]
- | ByNotation (_, s, _) -> ["notation", s] in
- xmlCanonicalStructure attr loc
- | VernacCoercion _ as x -> xmlTODO loc x
- | VernacIdentityCoercion _ as x -> xmlTODO loc x
-
- (* Type classes *)
- | VernacInstance _ as x -> xmlTODO loc x
-
- | VernacContext _ as x -> xmlTODO loc x
-
- | VernacDeclareInstances _ as x -> xmlTODO loc x
-
- | VernacDeclareClass _ as x -> xmlTODO loc x
-
- (* Modules and Module Types *)
- | VernacDeclareModule _ as x -> xmlTODO loc x
- | VernacDefineModule _ as x -> xmlTODO loc x
- | VernacDeclareModuleType _ as x -> xmlTODO loc x
- | VernacInclude _ as x -> xmlTODO loc x
-
- (* Solving *)
-
- | (VernacSolve _ | VernacSolveExistential _) as x ->
- xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
- (* Auxiliary file and library management *)
- | VernacAddLoadPath (recf,name,None) ->
- xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name] []
- | VernacAddLoadPath (recf,name,Some dp) ->
- xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name]
- [PCData (Names.DirPath.to_string dp)]
- | VernacRemoveLoadPath name -> xmlRemoveLoadPath loc ~attr:["path",name] []
- | VernacAddMLPath (recf,name) ->
- xmlAddMLPath loc ~attr:["rec",string_of_bool recf;"path",name] []
- | VernacDeclareMLModule sl -> xmlDeclareMLModule loc sl
- | VernacChdir _ as x -> xmlTODO loc x
-
- (* State management *)
- | VernacWriteState _ as x -> xmlTODO loc x
- | VernacRestoreState _ as x -> xmlTODO loc x
-
- (* Resetting *)
- | VernacResetName _ as x -> xmlTODO loc x
- | VernacResetInitial as x -> xmlTODO loc x
- | VernacBack _ as x -> xmlTODO loc x
- | VernacBackTo _ -> PCData "VernacBackTo"
-
- (* Commands *)
- | VernacDeclareTacticDefinition _ as x -> xmlTODO loc x
- | VernacCreateHintDb _ as x -> xmlTODO loc x
- | VernacRemoveHints _ as x -> xmlTODO loc x
- | VernacHints _ as x -> xmlTODO loc x
- | VernacSyntacticDefinition ((_, name), (idl, ce), _, _) ->
- let name = Id.to_string name in
- let attrs = List.map (fun id -> ("id", Id.to_string id)) idl in
- xmlNotation attrs name loc [pp_expr ce]
- | VernacDeclareImplicits _ as x -> xmlTODO loc x
- | VernacArguments _ as x -> xmlTODO loc x
- | VernacArgumentsScope _ as x -> xmlTODO loc x
- | VernacReserve _ as x -> xmlTODO loc x
- | VernacGeneralizable _ as x -> xmlTODO loc x
- | VernacSetOpacity _ as x -> xmlTODO loc x
- | VernacSetStrategy _ as x -> xmlTODO loc x
- | VernacUnsetOption _ as x -> xmlTODO loc x
- | VernacSetOption _ as x -> xmlTODO loc x
- | VernacAddOption _ as x -> xmlTODO loc x
- | VernacRemoveOption _ as x -> xmlTODO loc x
- | VernacMemOption _ as x -> xmlTODO loc x
- | VernacPrintOption _ as x -> xmlTODO loc x
- | VernacCheckMayEval (_,_,e) -> xmlCheck loc [pp_expr e]
- | VernacGlobalCheck _ as x -> xmlTODO loc x
- | VernacDeclareReduction _ as x -> xmlTODO loc x
- | VernacPrint _ as x -> xmlTODO loc x
- | VernacSearch _ as x -> xmlTODO loc x
- | VernacLocate _ as x -> xmlTODO loc x
- | VernacRegister _ as x -> xmlTODO loc x
- | VernacComments (cl) ->
- xmlComment loc (List.flatten (List.map pp_comment cl))
-
- (* Stm backdoor *)
- | VernacStm _ as x -> xmlTODO loc x
-
- (* Proof management *)
- | VernacGoal _ as x -> xmlTODO loc x
- | VernacAbort _ as x -> xmlTODO loc x
- | VernacAbortAll -> PCData "VernacAbortAll"
- | VernacRestart as x -> xmlTODO loc x
- | VernacUndo _ as x -> xmlTODO loc x
- | VernacUndoTo _ as x -> xmlTODO loc x
- | VernacBacktrack _ as x -> xmlTODO loc x
- | VernacFocus _ as x -> xmlTODO loc x
- | VernacUnfocus as x -> xmlTODO loc x
- | VernacUnfocused as x -> xmlTODO loc x
- | VernacBullet _ as x -> xmlTODO loc x
- | VernacSubproof _ as x -> xmlTODO loc x
- | VernacEndSubproof as x -> xmlTODO loc x
- | VernacShow _ as x -> xmlTODO loc x
- | VernacCheckGuard as x -> xmlTODO loc x
- | VernacProof (tac,using) ->
- let tac = Option.map (xmlRawTactic "closingtactic") tac in
- let using = Option.map (xmlSectionSubsetDescr "using") using in
- xmlProof loc (Option.List.(cons tac (cons using [])))
- | VernacProofMode name -> xmlProofMode loc name
-
- (* Toplevel control *)
- | VernacToplevelControl _ as x -> xmlTODO loc x
-
- (* For extension *)
- | VernacExtend _ as x ->
- xmlExtend loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
- (* Flags *)
- | VernacProgram e -> xmlApply loc (Element("program",[],[]) :: [tmpp e loc])
- | VernacLocal (b,e) ->
- xmlApply loc (Element("local",["flag",string_of_bool b],[]) ::
- [tmpp e loc])
-
-let tmpp v loc =
- match tmpp v loc with
- | Element("ltac",_,_) as x -> x
- | xml -> xmlGallina loc [xml]
diff --git a/stm/texmacspp.mli b/stm/texmacspp.mli
deleted file mode 100644
index 58dec8fdc1..0000000000
--- a/stm/texmacspp.mli
+++ /dev/null
@@ -1,12 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Xml_datatype
-open Vernacexpr
-
-val tmpp : vernac_expr -> Loc.t -> xml
diff --git a/stm/vcs.ml b/stm/vcs.ml
index dfcbc19ae4..38c029901d 100644
--- a/stm/vcs.ml
+++ b/stm/vcs.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/vcs.mli b/stm/vcs.mli
index fb79d02cbf..8f22fee843 100644
--- a/stm/vcs.mli
+++ b/stm/vcs.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index dcb6700941..b1df3c9ca6 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -10,6 +10,8 @@ open Vernacexpr
open Errors
open Pp
+let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
+
let string_of_in_script b = if b then " (inside script)" else ""
let string_of_vernac_type = function
@@ -102,12 +104,10 @@ let rec classify_vernac e =
| VernacCheckMayEval _ ->
VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
(* ProofStep *)
- | VernacSolve (SelectAllParallel,_,_,_) -> VtProofStep true, VtLater
| VernacProof _
| VernacBullet _
| VernacFocus _ | VernacUnfocus
| VernacSubproof _ | VernacEndSubproof
- | VernacSolve _
| VernacCheckGuard
| VernacUnfocused
| VernacSolveExistential _ -> VtProofStep false, VtLater
@@ -117,27 +117,27 @@ let rec classify_vernac e =
(* StartProof *)
| VernacDefinition (
(Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) ->
- VtStartProof("Classic",Doesn'tGuaranteeOpacity,[i]), VtLater
+ VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater
| VernacDefinition (_,((_,i),_),ProveBody _) ->
- VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater
+ VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater
| VernacStartTheoremProof (_,l,_) ->
let ids =
CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
- VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
- | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
+ VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
+ | VernacGoal _ -> VtStartProof (default_proof_mode (),GuaranteesOpacity,[]), VtLater
| VernacFixpoint (_,l) ->
let ids, open_proof =
List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
- then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+ then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
else VtSideff ids, VtLater
| VernacCoFixpoint (_,l) ->
let ids, open_proof =
List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
- then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+ then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
else VtSideff ids, VtLater
(* Sideff: apply to all open branches. usually run on master only *)
| VernacAssumption (_,_,l) ->
@@ -175,13 +175,6 @@ let rec classify_vernac e =
| VernacRegister _
| VernacNameSectionHypSet _
| VernacComments _ -> VtSideff [], VtLater
- | VernacDeclareTacticDefinition l ->
- let open Libnames in
- let open Vernacexpr in
- VtSideff (List.map (function
- | TacticDefinition ((_,r),_) -> r
- | TacticRedefinition (Ident (_,r),_) -> r
- | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater
(* Who knows *)
| VernacLoad _ -> VtSideff [], VtNow
(* (Local) Notations have to disappear *)
@@ -197,7 +190,6 @@ let rec classify_vernac e =
| VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
| VernacSyntaxExtension _
| VernacSyntacticDefinition _
- | VernacTacticNotation _
| VernacRequire _ | VernacImport _ | VernacInclude _
| VernacDeclareMLModule _
| VernacContext _ (* TASSI: unsure *)
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
index 0680fe8420..45ca5cf6b5 100644
--- a/stm/vernac_classifier.mli
+++ b/stm/vernac_classifier.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
index ce930cacb7..d4dcf72c13 100644
--- a/stm/vio_checking.ml
+++ b/stm/vio_checking.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/vio_checking.mli b/stm/vio_checking.mli
index e2da502693..c0b6d9e6fa 100644
--- a/stm/vio_checking.mli
+++ b/stm/vio_checking.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/workerPool.ml b/stm/workerPool.ml
index db3bb5ad44..b94fae547d 100644
--- a/stm/workerPool.ml
+++ b/stm/workerPool.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/stm/workerPool.mli b/stm/workerPool.mli
index f46303b547..75c325360e 100644
--- a/stm/workerPool.mli
+++ b/stm/workerPool.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 10:31:01 +0000