diff options
| -rw-r--r-- | ide/coq.ml | 83 | ||||
| -rw-r--r-- | ide/coq.mli | 4 | ||||
| -rw-r--r-- | ide/coqide.ml | 23 | ||||
| -rw-r--r-- | ide/coqide.mli | 13 | ||||
| -rw-r--r-- | ide/coqide_main.ml4 | 7 | ||||
| -rw-r--r-- | ide/minilib.ml | 1 | ||||
| -rw-r--r-- | ide/minilib.mli | 1 |
7 files changed, 97 insertions, 35 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index b1bb1f183..cc41ee230 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -54,15 +54,9 @@ let rec read_all_lines in_chan = arg::(read_all_lines in_chan) with End_of_file -> [] -let coqtop_path () = - let prog = Sys.executable_name in - let dir = Filename.dirname prog in - if Filename.check_suffix prog ".byte" then dir^"/coqtop.byte" - else dir^"/coqtop.opt" - let filter_coq_opts args = let argstr = String.concat " " (List.map Filename.quote args) in - let cmd = coqtop_path () ^" -nois -filteropts " ^ argstr in + let cmd = !Minilib.coqtop_path ^" -nois -filteropts " ^ argstr in let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in let filtered_args = read_all_lines oc in let message = read_all_lines ec in @@ -75,28 +69,46 @@ exception Coqtop_output of string list let check_connection args = try - let args = String.concat " " ("-batch"::args) in - let ic = Unix.open_process_in (coqtop_path () ^ " " ^ args) in + let argstr = String.concat " " (List.map Filename.quote args) in + let cmd = !Minilib.coqtop_path ^ " -batch " ^ argstr in + let ic = Unix.open_process_in cmd in let lines = read_all_lines ic in - match (Unix.close_process_in ic) with + match Unix.close_process_in ic with | Unix.WEXITED 0 -> prerr_endline "coqtop seems ok" | _ -> raise (Coqtop_output lines) - with End_of_file -> - Pervasives.prerr_endline "Cannot start connection with coqtop"; + with + | End_of_file -> + Pervasives.prerr_endline "Cannot start connection with coqtop"; + exit 1 | Coqtop_output lines -> Pervasives.prerr_endline "Connection with coqtop failed:"; List.iter Pervasives.prerr_endline lines; exit 1 -(* TODO: we can probably merge check_connection () and coqlib () *) +(** It is tempting to merge the following function with the previous one, + but check_connection fails if no initial.coq is found, while + check_coqlib doesn't check that. *) -let coqlib () = +let check_coqlib args = try - let ic = Unix.open_process_in (coqtop_path () ^" -where") in - let str = input_line ic in - ignore (Unix.close_process_in ic); - str - with _ -> failwith "Error while reading coqlib from coqtop" + let argstr = String.concat " " (List.map Filename.quote args) in + let cmd = !Minilib.coqtop_path ^ " " ^ argstr ^ " -where" in + let ic = Unix.open_process_in cmd in + let lines = read_all_lines ic in + match Unix.close_process_in ic with + | Unix.WEXITED 0 -> + (match lines with + | [coqlib] -> coqlib + | _ -> raise (Coqtop_output lines)) + | _ -> raise (Coqtop_output lines) + with + | End_of_file -> + Pervasives.prerr_endline "Cannot start connection with coqtop"; + exit 1 + | Coqtop_output lines -> + Pervasives.prerr_endline "Connection with coqtop failed:"; + List.iter Pervasives.prerr_endline lines; + exit 1 let eval_call coqtop (c:'a Ide_intf.call) = Marshal.to_channel coqtop.cin c []; @@ -117,21 +129,32 @@ let toplvl_ctr = ref 0 let toplvl_ctr_mtx = Mutex.create () +(** 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. +*) + +let open_process_pid prog args = + let (in_read,in_write) = Unix.pipe () in + let (out_read,out_write) = Unix.pipe () in + let pid = Unix.create_process prog args out_read in_write Unix.stderr in + assert (pid <> 0); + Unix.close out_read; + Unix.close in_write; + let ic = Unix.in_channel_of_descr in_read in + let oc = Unix.out_channel_of_descr out_write 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 - let (in_read,in_write) = Unix.pipe () in - let (out_read,out_write) = Unix.pipe () in - let prog = coqtop_path () in + let prog = !Minilib.coqtop_path in let args = Array.of_list (prog :: "-ideslave" :: sup_args) in - let pid = Unix.create_process prog args out_read in_write Unix.stderr in - assert (pid <> 0); - Unix.close out_read; - Unix.close in_write; - let ic = Unix.in_channel_of_descr in_read in - let oc = Unix.out_channel_of_descr out_write in - set_binary_mode_out oc true; - set_binary_mode_in ic true; + 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 ; version = 0 } diff --git a/ide/coq.mli b/ide/coq.mli index 37c5bcd00..f04dfeede 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -9,8 +9,10 @@ val short_version : unit -> string val version : unit -> string val filter_coq_opts : string list -> bool * string list +(* A mock coqtop launch, checking in particular that initial.coq is found *) val check_connection : string list -> unit -val coqlib : unit -> string +(* Same, with less checks, but returning coqlib *) +val check_coqlib : string list -> string type coqtop diff --git a/ide/coqide.ml b/ide/coqide.ml index ed5f1159f..1ce2133d1 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -530,6 +530,8 @@ let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) = buffer#apply_tag ~start:decl_start ~stop:decl_end Tags.Script.folded; buffer#apply_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden) +(** The arguments that will be passed to coqtop. No quoting here, since + no /bin/sh when using create_process instead of open_process. *) let sup_args = ref [] class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs _ct = @@ -3154,6 +3156,27 @@ let rec check_for_geoproof_input () = (* cb_Dr#set_text "Ack" *) done +let default_coqtop_path () = + let prog = Sys.executable_name in + let dir = Filename.dirname prog in + if Filename.check_suffix prog ".byte" then dir^"/coqtop.byte" + else dir^"/coqtop.opt" + +let set_coqtop_path argv = + let coqtop = ref "" in + let rec filter_coqtop = function + | "-coqtop" :: prog :: args -> + if !coqtop = "" then + (coqtop:=prog; filter_coqtop args) + else + (output_string stderr "Error: multiple -coqtop options"; exit 1) + | arg::args -> arg::filter_coqtop args + | [] -> (if !coqtop = "" then coqtop := default_coqtop_path (); []) + in + let argv = filter_coqtop argv in + Minilib.coqtop_path := !coqtop; + argv + let process_argv argv = try let continue,filtered = filter_coq_opts (List.tl argv) in diff --git a/ide/coqide.mli b/ide/coqide.mli index dd3995eb9..de9eb0238 100644 --- a/ide/coqide.mli +++ b/ide/coqide.mli @@ -10,9 +10,20 @@ command line, initialize the load path, load the input state, load the files given on the command line, load the ressource file, produce the output state if any, and finally will launch the interface. *) + +(** The arguments that will be passed to coqtop. No quoting here, since + no /bin/sh when using create_process instead of open_process. *) val sup_args : string list ref -val do_load : string -> unit + +(** Filter the argv from the option -coqtop, and set + Minilib.coqtop_path accordingly *) +val set_coqtop_path : string list -> string list + +(** Ask coqtop the remaining options it doesn't recognize *) val process_argv : string list -> string list + +val do_load : string -> unit + val crash_save : int -> unit val ignore_break : unit -> unit val check_for_geoproof_input : unit -> unit diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 index 4db3ba143..9b567ce5f 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml4 @@ -12,11 +12,12 @@ let macready () = IFDEF MacInt THEN gtk_mac_ready () ELSE () END let () = let argl = Array.to_list Sys.argv in + let argl = Coqide.set_coqtop_path argl in let files = Coqide.process_argv argl in let args = List.filter (fun x -> not (List.mem x files)) (List.tl argl) in - Coqide.sup_args := List.map Filename.quote args; - Coq.check_connection !Coqide.sup_args; - Minilib.coqlib := Coq.coqlib (); + Coq.check_connection args; + Minilib.coqlib := Coq.check_coqlib args; + Coqide.sup_args := args; Coqide.ignore_break (); GtkMain.Rc.add_default_file (Ideutils.lib_ide_file ".coqide-gtk2rc"); (try diff --git a/ide/minilib.ml b/ide/minilib.ml index b791d779c..9833fbd6b 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -61,3 +61,4 @@ let subst_command_placeholder s t = let home = try Sys.getenv "HOME" with Not_found -> "." let coqlib = ref "" +let coqtop_path = ref "" diff --git a/ide/minilib.mli b/ide/minilib.mli index aac3e3d77..22338250f 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -22,3 +22,4 @@ val subst_command_placeholder : string -> string -> string val home : string val coqlib : string ref +val coqtop_path : string ref |