summaryrefslogtreecommitdiff
path: root/ide/coq.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coq.ml')
-rw-r--r--ide/coq.ml953
1 files changed, 271 insertions, 682 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 1a5b9def..07f0ece8 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -1,53 +1,14 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coq.ml 15025 2012-03-09 14:27:07Z glondu $ *)
-
-open Vernac
-open Vernacexpr
-open Pfedit
-open Pp
-open Util
-open Names
-open Term
-open Printer
-open Environ
-open Evarutil
-open Evd
-open Decl_mode
-open Hipattern
-open Tacmach
-open Reductionops
-open Termops
-open Namegen
open Ideutils
-let msg m =
- let b = Buffer.create 103 in
- Pp.msg_with (Format.formatter_of_buffer b) m;
- Buffer.contents b
-
-let msgnl m =
- (msg m)^"\n"
-
-let init () =
- (* To hide goal in lower window.
- Problem: should not hide "xx is assumed"
- messages *)
-(**)
- Flags.make_silent true;
- (* don't set a too large undo stack because Edit.create allocates an array *)
- Pfedit.set_undo (Some 5000);
-(**)
- Coqtop.init_ide ()
-
-
-let i = ref 0
+(** * Version and date *)
let get_version_date () =
let date =
@@ -55,7 +16,12 @@ let get_version_date () =
then Coq_config.date
else "<date not printable>" in
try
- let ch = open_in (Coq_config.coqsrc^"/revision") in
+ (* the following makes sense only when running with local layout *)
+ let coqroot = Filename.concat
+ (Filename.dirname Sys.executable_name)
+ Filename.parent_dir_name
+ in
+ let ch = open_in (Filename.concat coqroot "revision") in
let ver = input_line ch in
let rev = input_line ch in
(ver,rev)
@@ -71,656 +37,279 @@ let version () =
"The Coq Proof Assistant, version %s (%s)\
\nArchitecture %s running %s operating system\
\nGtk version is %s\
- \nThis is the %s version (%s is the best one for this architecture and OS)\
+ \nThis is %s (%s is the best one for this architecture and OS)\
\n"
ver date
Coq_config.arch Sys.os_type
(let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z)
- (if Mltop.is_native then "native" else "bytecode")
- (if Coq_config.best="opt" then "native" else "bytecode")
-
-let is_in_coq_lib dir =
- prerr_endline ("Is it a coq theory ? : "^dir);
- let is_same_file = same_file dir in
- List.exists
- (fun s ->
- let fdir =
- Filename.concat (Envars.coqlib ()) (Filename.concat "theories" s) in
- prerr_endline (" Comparing to: "^fdir);
- if is_same_file fdir then (prerr_endline " YES";true)
- else (prerr_endline"NO";false))
- Coq_config.theories_dirs
-
-let is_in_loadpath dir =
- Library.is_in_load_paths (System.physical_path_of_string dir)
-
-let is_in_coq_path f =
- try
- let base = Filename.chop_extension (Filename.basename f) in
- let _ = Library.locate_qualified_library false
- (Libnames.make_qualid Names.empty_dirpath
- (Names.id_of_string base)) in
- prerr_endline (f ^ " is in coq path");
- true
- with _ ->
- prerr_endline (f ^ " is NOT in coq path");
- false
-
-let is_in_proof_mode () =
- match Decl_mode.get_current_mode () with
- Decl_mode.Mode_none -> false
- | _ -> true
-
-let user_error_loc l s =
- raise (Compat.Exc_located (l, Util.UserError ("CoqIde", s)))
-
-type printing_state = {
- mutable printing_implicit : bool;
- mutable printing_coercions : bool;
- mutable printing_raw_matching : bool;
- mutable printing_no_notation : bool;
- mutable printing_all : bool;
- mutable printing_evar_instances : bool;
- mutable printing_universes : bool;
- mutable printing_full_all : bool
-}
+ (Filename.basename Sys.executable_name)
+ Coq_config.best
-let printing_state = {
- printing_implicit = false;
- printing_coercions = false;
- printing_raw_matching = false;
- printing_no_notation = false;
- printing_all = false;
- printing_evar_instances = false;
- printing_universes = false;
- printing_full_all = false;
-}
-let printing_implicit_data = ["Printing";"Implicit"], false
-let printing_coercions_data = ["Printing";"Coercions"], false
-let printing_raw_matching_data = ["Printing";"Matching"], true
-let printing_no_synth_data = ["Printing";"Synth"], true
-let printing_no_notation_data = ["Printing";"Notations"], true
-let printing_all_data = ["Printing";"All"], false
-let printing_evar_instances_data = ["Printing";"Existential";"Instances"],false
-let printing_universes_data = ["Printing";"Universes"], false
-
-let known_options = ref []
-
-let prepare_option (l,dft) =
- known_options := l :: !known_options;
- let set = (String.concat " " ("Set"::l)) ^ "." in
- let unset = (String.concat " " ("Unset"::l)) ^ "." in
- if dft then unset,set else set,unset
-
-let coqide_known_option table = List.mem table !known_options
-
-let with_printing_implicit = prepare_option printing_implicit_data
-let with_printing_coercions = prepare_option printing_coercions_data
-let with_printing_raw_matching = prepare_option printing_raw_matching_data
-let with_printing_no_synth = prepare_option printing_no_synth_data
-let with_printing_no_notation = prepare_option printing_no_notation_data
-let with_printing_all = prepare_option printing_all_data
-let with_printing_evar_instances = prepare_option printing_evar_instances_data
-let with_printing_universes = prepare_option printing_universes_data
-
-let make_option_commands () =
- let p = printing_state in
- (if p.printing_implicit then [with_printing_implicit] else [])@
- (if p.printing_coercions then [with_printing_coercions] else [])@
- (if p.printing_raw_matching then [with_printing_raw_matching;with_printing_no_synth] else [])@
- (if p.printing_no_notation then [with_printing_no_notation] else [])@
- (if p.printing_all then [with_printing_all] else [])@
- (if p.printing_evar_instances then [with_printing_evar_instances] else [])@
- (if p.printing_universes then [with_printing_universes] else [])@
- (if p.printing_full_all then [with_printing_all;with_printing_evar_instances;with_printing_universes] else [])
-
-let make_option_commands () =
- let l = make_option_commands () in
- List.iter (fun (a,b) -> prerr_endline a; prerr_endline b) l;
- l
-
-type command_attribute =
- NavigationCommand | QueryCommand | DebugCommand | KnownOptionCommand
- | OtherStatePreservingCommand | GoalStartingCommand | SolveCommand
- | ProofEndingCommand
-
-let rec attribute_of_vernac_command = function
- (* Control *)
- | VernacTime com -> attribute_of_vernac_command com
- | VernacTimeout(_,com) -> attribute_of_vernac_command com
- | VernacFail com -> attribute_of_vernac_command com
- | VernacList _ -> [] (* unsupported *)
- | VernacLoad _ -> []
-
- (* Syntax *)
- | VernacTacticNotation _ -> []
- | VernacSyntaxExtension _ -> []
- | VernacDelimiters _ -> []
- | VernacBindScope _ -> []
- | VernacOpenCloseScope _ -> []
- | VernacArgumentsScope _ -> []
- | VernacInfix _ -> []
- | VernacNotation _ -> []
-
- (* Gallina *)
- | VernacDefinition (_,_,DefineBody _,_) -> []
- | VernacDefinition (_,_,ProveBody _,_) -> [GoalStartingCommand]
- | VernacStartTheoremProof _ -> [GoalStartingCommand]
- | VernacEndProof _ -> [ProofEndingCommand]
- | VernacExactProof _ -> [ProofEndingCommand]
-
- | VernacAssumption _ -> []
- | VernacInductive _ -> []
- | VernacFixpoint _ -> []
- | VernacCoFixpoint _ -> []
- | VernacScheme _ -> []
- | VernacCombinedScheme _ -> []
-
- (* Modules *)
- | VernacDeclareModule _ -> []
- | VernacDefineModule _ -> []
- | VernacDeclareModuleType _ -> []
- | VernacInclude _ -> []
-
- (* Gallina extensions *)
- | VernacBeginSection _ -> []
- | VernacEndSegment _ -> []
- | VernacRequire _ -> []
- | VernacImport _ -> []
- | VernacCanonical _ -> []
- | VernacCoercion _ -> []
- | VernacIdentityCoercion _ -> []
-
- (* Type classes *)
- | VernacInstance _ -> []
- | VernacContext _ -> []
- | VernacDeclareInstance _ -> []
- | VernacDeclareClass _ -> []
-
- (* Solving *)
- | VernacSolve _ -> [SolveCommand]
- | VernacSolveExistential _ -> [SolveCommand]
-
- (* MMode *)
- | VernacDeclProof -> [SolveCommand]
- | VernacReturn -> [SolveCommand]
- | VernacProofInstr _ -> [SolveCommand]
-
- (* Auxiliary file and library management *)
- | VernacRequireFrom _ -> []
- | VernacAddLoadPath _ -> []
- | VernacRemoveLoadPath _ -> []
- | VernacAddMLPath _ -> []
- | VernacDeclareMLModule _ -> []
- | VernacChdir _ -> [OtherStatePreservingCommand]
-
- (* State management *)
- | VernacWriteState _ -> []
- | VernacRestoreState _ -> []
-
- (* Resetting *)
- | VernacRemoveName _ -> [NavigationCommand]
- | VernacResetName _ -> [NavigationCommand]
- | VernacResetInitial -> [NavigationCommand]
- | VernacBack _ -> [NavigationCommand]
- | VernacBackTo _ -> [NavigationCommand]
-
- (* Commands *)
- | VernacDeclareTacticDefinition _ -> []
- | VernacCreateHintDb _ -> []
- | VernacHints _ -> []
- | VernacSyntacticDefinition _ -> []
- | VernacDeclareImplicits _ -> []
- | VernacDeclareReduction _ -> []
- | VernacReserve _ -> []
- | VernacGeneralizable _ -> []
- | VernacSetOpacity _ -> []
- | VernacSetOption (_,["Ltac";"Debug"], _) -> [DebugCommand]
- | VernacSetOption (_,o,BoolValue true) | VernacUnsetOption (_,o) ->
- if coqide_known_option o then [KnownOptionCommand] else []
- | VernacSetOption _ -> []
- | VernacRemoveOption _ -> []
- | VernacAddOption _ -> []
- | VernacMemOption _ -> [QueryCommand]
-
- | VernacPrintOption _ -> [QueryCommand]
- | VernacCheckMayEval _ -> [QueryCommand]
- | VernacGlobalCheck _ -> [QueryCommand]
- | VernacPrint _ -> [QueryCommand]
- | VernacSearch _ -> [QueryCommand]
- | VernacLocate _ -> [QueryCommand]
-
- | VernacComments _ -> [OtherStatePreservingCommand]
- | VernacNop -> [OtherStatePreservingCommand]
-
- (* Proof management *)
- | VernacGoal _ -> [GoalStartingCommand]
-
- | VernacAbort _ -> []
- | VernacAbortAll -> [NavigationCommand]
- | VernacRestart -> [NavigationCommand]
- | VernacSuspend -> [NavigationCommand]
- | VernacResume _ -> [NavigationCommand]
- | VernacUndo _ -> [NavigationCommand]
- | VernacUndoTo _ -> [NavigationCommand]
- | VernacBacktrack _ -> [NavigationCommand]
-
- | VernacFocus _ -> [SolveCommand]
- | VernacUnfocus -> [SolveCommand]
- | VernacGo _ -> []
- | VernacShow _ -> [OtherStatePreservingCommand]
- | VernacCheckGuard -> [OtherStatePreservingCommand]
- | VernacProof (Tacexpr.TacId []) -> [OtherStatePreservingCommand]
- | VernacProof _ -> []
-
- (* Toplevel control *)
- | VernacToplevelControl _ -> []
-
- (* Extensions *)
- | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand]
- | VernacExtend _ -> []
-
-let is_vernac_goal_starting_command com =
- List.mem GoalStartingCommand (attribute_of_vernac_command com)
-
-let is_vernac_navigation_command com =
- List.mem NavigationCommand (attribute_of_vernac_command com)
-
-let is_vernac_query_command com =
- List.mem QueryCommand (attribute_of_vernac_command com)
-
-let is_vernac_known_option_command com =
- List.mem KnownOptionCommand (attribute_of_vernac_command com)
-
-let is_vernac_debug_command com =
- List.mem DebugCommand (attribute_of_vernac_command com)
-
-let is_vernac_goal_printing_command com =
- let attribute = attribute_of_vernac_command com in
- List.mem GoalStartingCommand attribute or
- List.mem SolveCommand attribute
-
-let is_vernac_state_preserving_command com =
- let attribute = attribute_of_vernac_command com in
- List.mem OtherStatePreservingCommand attribute or
- List.mem QueryCommand attribute
-
-let is_vernac_tactic_command com =
- List.mem SolveCommand (attribute_of_vernac_command com)
-
-let is_vernac_proof_ending_command com =
- List.mem ProofEndingCommand (attribute_of_vernac_command com)
-
-type undo_info = identifier list
-
-let undo_info () = Pfedit.get_all_proof_names ()
-
-type reset_mark = Libnames.object_name
-
-type reset_status =
- | NoReset
- | ResetAtSegmentStart of Names.identifier
- | ResetAtRegisteredObject of reset_mark
-
-type reset_info = {
- status : reset_status;
- proofs : identifier list;
- cur_prf : (identifier * int) option;
- loc_ast : Util.loc * Vernacexpr.vernac_expr;
+(** * Initial checks by launching test coqtop processes *)
+
+let rec read_all_lines in_chan =
+ try
+ let arg = input_line in_chan in
+ arg::(read_all_lines in_chan)
+ with End_of_file -> []
+
+let fatal_error_popup msg =
+ let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok
+ ~message_type:`ERROR ~message:msg ()
+ in ignore (popup#run ()); exit 1
+
+let final_info_popup small msg =
+ if small then
+ let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok
+ ~message_type:`INFO ~message:msg ()
+ in
+ let _ = popup#run () in
+ exit 0
+ else
+ let popup = GWindow.dialog () in
+ let button = GButton.button ~label:"ok" ~packing:popup#action_area#add ()
+ in
+ let scroll = GBin.scrolled_window ~hpolicy:`NEVER ~vpolicy:`AUTOMATIC
+ ~packing:popup#vbox#add ~height:500 ()
+ in
+ let _ = GMisc.label ~text:msg ~packing:scroll#add_with_viewport () in
+ let _ = popup#connect#destroy ~callback:(fun _ -> exit 0) in
+ let _ = button#connect#clicked ~callback:(fun _ -> exit 0) in
+ let _ = popup#run () in
+ exit 0
+
+let connection_error cmd lines exn =
+ fatal_error_popup
+ ("Connection with coqtop failed!\n"^
+ "Command was: "^cmd^"\n"^
+ "Answer was: "^(String.concat "\n " lines)^"\n"^
+ "Exception was: "^Printexc.to_string exn)
+
+let display_coqtop_answer cmd lines =
+ final_info_popup (List.length lines < 30)
+ ("Coqtop exited\n"^
+ "Command was: "^cmd^"\n"^
+ "Answer was: "^(String.concat "\n " lines))
+
+let check_remaining_opt arg =
+ if arg <> "" && arg.[0] = '-' then fatal_error_popup ("Illegal option: "^arg)
+
+let rec filter_coq_opts args =
+ let argstr = String.concat " " (List.map Filename.quote args) in
+ let cmd = Filename.quote (coqtop_path ()) ^" -nois -filteropts " ^ argstr in
+ let cmd = requote cmd in
+ let filtered_args = ref [] in
+ let errlines = ref [] in
+ try
+ let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in
+ filtered_args := read_all_lines oc;
+ errlines := read_all_lines ec;
+ match Unix.close_process_full (oc,ic,ec) with
+ | Unix.WEXITED 0 ->
+ List.iter check_remaining_opt !filtered_args; !filtered_args
+ | Unix.WEXITED 127 -> asks_for_coqtop args
+ | _ -> display_coqtop_answer cmd (!filtered_args @ !errlines)
+ with Sys_error _ -> asks_for_coqtop args
+ | e -> connection_error cmd (!filtered_args @ !errlines) e
+
+and asks_for_coqtop args =
+ let pb_mes = GWindow.message_dialog
+ ~message:"Failed to load coqtop. Reset the preference to default ?"
+ ~message_type:`QUESTION ~buttons:GWindow.Buttons.yes_no () in
+ match pb_mes#run () with
+ | `YES ->
+ let () = !Preferences.current.Preferences.cmd_coqtop <- None in
+ let () = custom_coqtop := None in
+ let () = pb_mes#destroy () in
+ filter_coq_opts args
+ | `DELETE_EVENT | `NO ->
+ let () = pb_mes#destroy () in
+ let cmd_sel = GWindow.file_selection
+ ~title:"Coqtop to execute (edit your preference then)"
+ ~filename:(coqtop_path ()) ~urgency_hint:true () in
+ match cmd_sel#run () with
+ | `OK ->
+ let () = custom_coqtop := (Some cmd_sel#filename) in
+ let () = cmd_sel#destroy () in
+ filter_coq_opts args
+ | `CANCEL | `DELETE_EVENT | `HELP -> exit 0
+
+exception WrongExitStatus of string
+
+let print_status = function
+ | Unix.WEXITED n -> "WEXITED "^string_of_int n
+ | Unix.WSIGNALED n -> "WSIGNALED "^string_of_int n
+ | Unix.WSTOPPED n -> "WSTOPPED "^string_of_int n
+
+let check_connection args =
+ let lines = ref [] in
+ let argstr = String.concat " " (List.map Filename.quote args) in
+ let cmd = Filename.quote (coqtop_path ()) ^ " -batch " ^ argstr in
+ let cmd = requote cmd in
+ try
+ let ic = Unix.open_process_in cmd in
+ lines := read_all_lines ic;
+ match Unix.close_process_in ic with
+ | Unix.WEXITED 0 -> () (* coqtop seems ok *)
+ | st -> raise (WrongExitStatus (print_status st))
+ with e -> connection_error cmd !lines e
+
+(** * The structure describing a coqtop sub-process *)
+
+type coqtop = {
+ pid : int; (* Unix process id *)
+ cout : in_channel ;
+ cin : out_channel ;
+ sup_args : string list;
}
-let compute_reset_info loc_ast =
- let status,cur_prf = match snd loc_ast with
- | com when is_vernac_proof_ending_command com -> NoReset,None
- | VernacEndSegment _ -> NoReset,None
- | com when is_vernac_tactic_command com ->
- NoReset,Some (Pfedit.get_current_proof_name (), Pfedit.current_proof_depth ())
- | _ ->
- (match Lib.has_top_frozen_state () with
- | Some sp ->
- prerr_endline ("On top of state "^Libnames.string_of_path (fst sp));
- ResetAtRegisteredObject sp,None
- | None -> NoReset,None)
- in
- { status = status;
- proofs = Pfedit.get_all_proof_names ();
- cur_prf = cur_prf;
- loc_ast = loc_ast;
- }
-
-let reset_initial () =
- prerr_endline "Reset initial called";
- Vernacentries.abort_refine Lib.reset_initial ()
-
-let reset_to sp =
- prerr_endline
- ("Reset called with state "^(Libnames.string_of_path (fst sp)));
- Lib.reset_to_state sp
-
-let raw_interp s =
- Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s))
-
-let interp_with_options verbosely options s =
- prerr_endline "Starting interp...";
- prerr_endline s;
- let pa = Pcoq.Gram.parsable (Stream.of_string s) in
- let pe = Pcoq.Gram.Entry.parse Pcoq.main_entry pa in
- (* Temporary hack to make coqide.byte work (WTF???) - now with less screen
- * pollution *)
- (try Pervasives.prerr_string " \r"; Pervasives.flush stderr with _ -> ());
- match pe with
- | None -> assert false
- | Some((loc,vernac) as last) ->
- if is_vernac_debug_command vernac then
- user_error_loc loc (str "Debug mode not available within CoqIDE");
- if is_vernac_navigation_command vernac then
- user_error_loc loc (str "Use CoqIDE navigation instead");
- if is_vernac_known_option_command vernac then
- user_error_loc loc (str "Use CoqIDE display menu instead");
- if is_vernac_query_command vernac then
- flash_info
- "Warning: query commands should not be inserted in scripts";
- if not (is_vernac_goal_printing_command vernac) then
- (* Verbose if in small step forward and not a tactic *)
- Flags.make_silent (not verbosely);
- let reset_info = compute_reset_info last in
- List.iter (fun (set_option,_) -> raw_interp set_option) options;
- raw_interp s;
- Flags.make_silent true;
- List.iter (fun (_,unset_option) -> raw_interp unset_option) options;
- prerr_endline ("...Done with interp of : "^s);
- reset_info
-
-let interp verbosely phrase =
- interp_with_options verbosely (make_option_commands ()) phrase
-
-let interp_and_replace s =
- let result = interp false s in
- let msg = read_stdout () in
- result,msg
-
-let rec is_pervasive_exn = function
- | Out_of_memory | Stack_overflow | Sys.Break -> true
- | Error_in_file (_,_,e) -> is_pervasive_exn e
- | Compat.Exc_located (_,e) -> is_pervasive_exn e
- | DuringCommandInterp (_,e) -> is_pervasive_exn e
- | _ -> false
-
-let print_toplevel_error exc =
- let (dloc,exc) =
- match exc with
- | DuringCommandInterp (loc,ie) ->
- if loc = dummy_loc then (None,ie) else (Some loc, ie)
- | _ -> (None, exc)
- in
- let (loc,exc) =
- match exc with
- | Compat.Exc_located (loc, ie) -> (Some loc),ie
- | Error_in_file (s, (_,fname, loc), ie) -> None, ie
- | _ -> dloc,exc
- in
- match exc with
- | End_of_input -> str "Please report: End of input",None
- | Vernacexpr.Drop -> str "Drop is not allowed by coqide!",None
- | Vernacexpr.Quit -> str "Quit is not allowed by coqide! Use menus.",None
- | _ ->
- (try Cerrors.explain_exn exc with e ->
- str "Failed to explain error. This is an internal Coq error. Please report.\n"
- ++ str (Printexc.to_string e)),
- (if is_pervasive_exn exc then None else loc)
-
-let process_exn e = let s,loc= print_toplevel_error e in (msgnl s,loc)
-
-let interp_last last =
- prerr_string "*";
+(** * Count of all active coqtops *)
+
+let toplvl_ctr = ref 0
+
+let toplvl_ctr_mtx = Mutex.create ()
+
+let coqtop_zombies () =
+ Mutex.lock toplvl_ctr_mtx;
+ let res = !toplvl_ctr in
+ Mutex.unlock toplvl_ctr_mtx;
+ res
+
+
+(** * Starting / signaling / ending a real coqtop sub-process *)
+
+(** We simulate a Unix.open_process that also returns the pid of
+ the created process. Note: this uses Unix.create_process, which
+ doesn't call bin/sh, so args shouldn't be quoted. The process
+ cannot be terminated by a Unix.close_process, but rather by a
+ kill of the pid.
+
+ >--ide2top_w--[pipe]--ide2top_r-->
+ coqide coqtop
+ <--top2ide_r--[pipe]--top2ide_w--<
+
+ Note: we use Unix.stderr in Unix.create_process to get debug
+ messages from the coqtop's Ide_slave loop.
+
+ NB: it's important to close coqide's descriptors (ide2top_w and top2ide_r)
+ in coqtop. We do this indirectly via [Unix.set_close_on_exec].
+ This way, coqide has the only remaining copies of these descriptors,
+ and closing them later will have visible effects in coqtop. Cf man 7 pipe :
+
+ - If all file descriptors referring to the write end of a pipe have been
+ closed, then an attempt to read(2) from the pipe will see end-of-file
+ (read(2) will return 0).
+ - If all file descriptors referring to the read end of a pipe have been
+ closed, then a write(2) will cause a SIGPIPE signal to be generated for
+ the calling process. If the calling process is ignoring this signal,
+ then write(2) fails with the error EPIPE.
+
+ Symmetrically, coqtop's descriptors (ide2top_r and top2ide_w) should be
+ closed in coqide.
+*)
+
+let open_process_pid prog args =
+ let (ide2top_r,ide2top_w) = Unix.pipe () in
+ let (top2ide_r,top2ide_w) = Unix.pipe () in
+ Unix.set_close_on_exec ide2top_w;
+ Unix.set_close_on_exec top2ide_r;
+ let pid = Unix.create_process prog args ide2top_r top2ide_w Unix.stderr in
+ assert (pid <> 0);
+ Unix.close ide2top_r;
+ Unix.close top2ide_w;
+ let oc = Unix.out_channel_of_descr ide2top_w in
+ let ic = Unix.in_channel_of_descr top2ide_r in
+ set_binary_mode_out oc true;
+ set_binary_mode_in ic true;
+ (pid,ic,oc)
+
+let spawn_coqtop sup_args =
+ Mutex.lock toplvl_ctr_mtx;
try
- vernac_com Vernacentries.interp last;
- Lib.add_frozen_state()
+ let prog = coqtop_path () in
+ let args = Array.of_list (prog :: "-ideslave" :: sup_args) in
+ let (pid,ic,oc) = open_process_pid prog args in
+ incr toplvl_ctr;
+ Mutex.unlock toplvl_ctr_mtx;
+ { pid = pid; cin = oc; cout = ic ; sup_args = sup_args }
with e ->
- let s,_ = process_exn e in prerr_endline ("Replay during undo failed because: "^s);
+ Mutex.unlock toplvl_ctr_mtx;
raise e
-let push_phrase cmd_stk reset_info ide_payload =
- Stack.push (ide_payload,reset_info) cmd_stk
-
-type backtrack =
- | BacktrackToNextActiveMark
- | BacktrackToMark of reset_mark
- | NoBacktrack
-
-let apply_reset = function
- | BacktrackToMark mark -> reset_to mark
- | NoBacktrack -> ()
- | BacktrackToNextActiveMark -> assert false
-
-let rewind sequence cmd_stk =
- let undo_ops = Hashtbl.create 31 in
- let current_proofs = undo_info () in
- let pop_state cont seq coq reset_op prev_proofs curprf =
- prerr_endline "pop";
- let curprf =
- Option.map
- (fun (curprf,depth) ->
- (if Hashtbl.mem undo_ops curprf then Hashtbl.replace else Hashtbl.add)
- undo_ops curprf depth;
- curprf)
- coq.cur_prf in
- let reset_op =
- match coq.status with
- | ResetAtRegisteredObject mark ->
- BacktrackToMark mark
- | _ when is_vernac_state_preserving_command (snd coq.loc_ast) ->
- reset_op
- | _ when is_vernac_tactic_command (snd coq.loc_ast) ->
- reset_op
- | _ ->
- BacktrackToNextActiveMark in
- cont seq reset_op coq.proofs curprf
- in
- let rec do_rewind seq reset_op prev_proofs curprf =
- match seq with
- | [] when ((reset_op <> BacktrackToNextActiveMark) &&
- (Util.list_subset prev_proofs current_proofs)) ->
- begin
- Hashtbl.iter
- (fun id depth ->
- if List.mem id prev_proofs then begin
- Pfedit.resume_proof (Util.dummy_loc,id);
- Pfedit.undo_todepth depth
- end)
- undo_ops;
- prerr_endline "OK for undos";
- Option.iter (fun id -> if List.mem id prev_proofs then
- Pfedit.resume_proof (Util.dummy_loc,id)) curprf;
- prerr_endline "OK for focusing";
- List.iter
- (fun id -> Pfedit.delete_proof (Util.dummy_loc,id))
- (Util.list_subtract current_proofs prev_proofs);
- prerr_endline "OK for aborts";
- apply_reset reset_op;
- prerr_endline "OK for reset"
- end
- | [] ->
- begin
- try
- let ide,coq = Stack.pop cmd_stk in
- pop_state do_rewind [] coq reset_op prev_proofs curprf;
- prerr_endline "push";
- let reset_info = compute_reset_info coq.loc_ast in
- interp_last coq.loc_ast;
- push_phrase cmd_stk reset_info ide
- with Stack.Empty -> reset_initial ()
- end
- | coq::rem ->
- pop_state do_rewind rem coq reset_op prev_proofs curprf
- in
- do_rewind sequence NoBacktrack current_proofs None
-
-type tried_tactic =
- | Interrupted
- | Success of int (* nb of goals after *)
- | Failed
-
-type hyp = env * evar_map *
- ((identifier * string) * constr option * constr) *
- (string * string)
-type concl = env * evar_map * constr * string
-type meta = env * evar_map * string
-type goal = hyp list * concl
-
-let prepare_hyp sigma env ((i,c,d) as a) =
- env, sigma,
- ((i,string_of_id i),c,d),
- (msg (pr_var_decl env a), msg (pr_ltype_env env d))
-
-let prepare_hyps sigma env =
- assert (rel_context env = []);
- let hyps =
- fold_named_context
- (fun env d acc -> let hyp = prepare_hyp sigma env d in hyp :: acc)
- env ~init:[]
- in
- List.rev hyps
-
-let prepare_goal_main sigma g =
- let env = evar_env g in
- (prepare_hyps sigma env,
- (env, sigma, g.evar_concl, msg (pr_ltype_env_at_top env g.evar_concl)))
-
-let prepare_goal sigma g =
- let options = make_option_commands () in
- List.iter (fun (set_option,_) -> raw_interp set_option) options;
- let x = prepare_goal_main sigma g in
- List.iter (fun (_,unset_option) -> raw_interp unset_option) options;
- x
-
-let get_current_pm_goal () =
- let pfts = get_pftreestate () in
- let gls = try nth_goal_of_pftreestate 1 pfts with _ -> raise Not_found in
- let sigma= sig_sig gls in
- let gl = sig_it gls in
- prepare_goal sigma gl
-
-let get_current_goals () =
- let pfts = get_pftreestate () in
- let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in
- let sigma = Tacmach.evc_of_pftreestate pfts in
- List.map (prepare_goal sigma) gls
-
-let print_no_goal () =
- (* Fall back on standard coq goal printer for completed goal printing *)
- msg (pr_open_subgoals ())
-
-let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
- [("clear "^ident),("clear "^ident^".");
-
- ("apply "^ident),
- ("apply "^ident^".");
-
- ("exact "^ident),
- ("exact "^ident^".");
-
- ("generalize "^ident),
- ("generalize "^ident^".");
-
- ("absurd <"^ident^">"),
- ("absurd "^
- pr_ast
- ^".") ] @
-
- (if is_equality_type ast then
- [ "discriminate "^ident, "discriminate "^ident^".";
- "injection "^ident, "injection "^ident^"." ]
- else
- []) @
-
- (let _,t = splay_prod env sigma ast in
- if is_equality_type t then
- [ "rewrite "^ident, "rewrite "^ident^".";
- "rewrite <- "^ident, "rewrite <- "^ident^"." ]
- else
- []) @
-
- [("elim "^ident),
- ("elim "^ident^".");
-
- ("inversion "^ident),
- ("inversion "^ident^".");
-
- ("inversion clear "^ident),
- ("inversion_clear "^ident^".")]
-
-let concl_menu (_,_,concl,_) =
- let is_eq = is_equality_type concl in
- ["intro", "intro.";
- "intros", "intros.";
- "intuition","intuition." ] @
-
- (if is_eq then
- ["reflexivity", "reflexivity.";
- "discriminate", "discriminate.";
- "symmetry", "symmetry." ]
- else
- []) @
-
- ["assumption" ,"assumption.";
- "omega", "omega.";
- "ring", "ring.";
- "auto with *", "auto with *.";
- "eauto with *", "eauto with *.";
- "tauto", "tauto.";
- "trivial", "trivial.";
- "decide equality", "decide equality.";
-
- "simpl", "simpl.";
- "subst", "subst.";
-
- "red", "red.";
- "split", "split.";
- "left", "left.";
- "right", "right.";
- ]
-
-
-let id_of_name = function
- | Names.Anonymous -> id_of_string "x"
- | Names.Name x -> x
-
-let make_cases s =
- let qualified_name = Libnames.qualid_of_string s in
- let glob_ref = Nametab.locate qualified_name in
- match glob_ref with
- | Libnames.IndRef i ->
- let {Declarations.mind_nparams = np},
- {Declarations.mind_consnames = carr ;
- Declarations.mind_nf_lc = tarr }
- = Global.lookup_inductive i
- in
- Util.array_fold_right2
- (fun n t l ->
- let (al,_) = Term.decompose_prod t in
- let al,_ = Util.list_chop (List.length al - np) al in
- let rec rename avoid = function
- | [] -> []
- | (n,_)::l ->
- let n' = next_ident_away_in_goal
- (id_of_name n)
- avoid
- in (string_of_id n')::(rename (n'::avoid) l)
- in
- let al' = rename [] (List.rev al) in
- (string_of_id n :: al') :: l
- )
- carr
- tarr
- []
- | _ -> raise Not_found
-
-let current_status () =
- let path = msg (Libnames.pr_dirpath (Lib.cwd ())) in
- let path = if path = "Top" then "Ready" else "Ready in " ^ String.sub path 4 (String.length path - 4) in
- try
- path ^ ", proving " ^ (Names.string_of_id (Pfedit.get_current_proof_name ()))
- with _ -> path
+let respawn_coqtop coqtop = spawn_coqtop coqtop.sup_args
+let interrupter = ref (fun pid -> Unix.kill pid Sys.sigint)
+let killer = ref (fun pid -> Unix.kill pid Sys.sigkill)
+
+let break_coqtop coqtop =
+ try !interrupter coqtop.pid
+ with _ -> prerr_endline "Error while sending Ctrl-C"
+
+let kill_coqtop coqtop =
+ let pid = coqtop.pid in
+ begin
+ try !killer pid
+ with _ -> prerr_endline "Kill -9 failed. Process already terminated ?"
+ end;
+ try
+ ignore (Unix.waitpid [] pid);
+ Mutex.lock toplvl_ctr_mtx; decr toplvl_ctr; Mutex.unlock toplvl_ctr_mtx
+ with _ -> prerr_endline "Error while waiting for child"
+
+(** * Calls to coqtop *)
+
+(** Cf [Ide_intf] for more details *)
+
+let p = Xml_parser.make ()
+let () = Xml_parser.check_eof p false
+
+let eval_call coqtop (c:'a Ide_intf.call) =
+ Xml_utils.print_xml coqtop.cin (Ide_intf.of_call c);
+ flush coqtop.cin;
+ let xml = Xml_parser.parse p (Xml_parser.SChannel coqtop.cout) in
+ (Ide_intf.to_answer xml c : 'a Interface.value)
+
+let interp coqtop ?(raw=false) ?(verbose=true) s =
+ eval_call coqtop (Ide_intf.interp (raw,verbose,s))
+let rewind coqtop i = eval_call coqtop (Ide_intf.rewind i)
+let inloadpath coqtop s = eval_call coqtop (Ide_intf.inloadpath s)
+let mkcases coqtop s = eval_call coqtop (Ide_intf.mkcases s)
+let status coqtop = eval_call coqtop Ide_intf.status
+let hints coqtop = eval_call coqtop Ide_intf.hints
+
+module PrintOpt =
+struct
+ type t = string list
+ let implicit = ["Printing"; "Implicit"]
+ let coercions = ["Printing"; "Coercions"]
+ let raw_matching = ["Printing"; "Matching"; "Synth"]
+ let notations = ["Printing"; "Notations"]
+ let all_basic = ["Printing"; "All"]
+ let existential = ["Printing"; "Existential"; "Instances"]
+ let universes = ["Printing"; "Universes"]
+
+ let state_hack = Hashtbl.create 11
+ let _ = List.iter (fun opt -> Hashtbl.add state_hack opt false)
+ [ implicit; coercions; raw_matching; notations; all_basic; existential; universes ]
+
+ let set coqtop options =
+ let () = List.iter (fun (name, v) -> Hashtbl.replace state_hack name v) options in
+ let options = List.map (fun (name, v) -> (name, Interface.BoolValue v)) options in
+ match eval_call coqtop (Ide_intf.set_options options) with
+ | Interface.Good () -> ()
+ | _ -> raise (Failure "Cannot set options.")
+
+ let enforce_hack coqtop =
+ let elements = Hashtbl.fold (fun opt v acc -> (opt, v) :: acc) state_hack [] in
+ set coqtop elements
+
+end
+
+let goals coqtop =
+ let () = PrintOpt.enforce_hack coqtop in
+ eval_call coqtop Ide_intf.goals
+
+let evars coqtop =
+ let () = PrintOpt.enforce_hack coqtop in
+ eval_call coqtop Ide_intf.evars