From 382ee49700c4b4ee78ba95b2e86866ebd3b35d74 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 7 Mar 2018 01:33:17 +0100 Subject: [stm] Make toplevels standalone executables. We turn coqtop "plugins" into standalone executables, which will be installed in `COQBIN` and located using the standard `PATH` mechanism. Using dynamic linking for `coqtop` customization didn't make a lot of sense, given that only one of such "plugins" could be loaded at a time. This cleans up some code and solves two problems: - `coqtop` needing to locate plugins, - dependency issues as plugins in `stm` depended on files in `toplevel`. In order to implement this, we do some minor cleanup of the toplevel API, making it functional, and implement uniform build rules. In particular: - `stm` and `toplevel` have become library-only directories, - a new directory, `topbin`, contains the new executables, - 4 new binaries have been introduced, for coqide and the stm. - we provide a common and cleaned up way to locate toplevels. --- ide/coqidetop.mllib | 8 - ide/ide_common.mllib | 7 + ide/ide_slave.ml | 518 -------------------------------------------------- ide/ide_slave.mli | 12 -- ide/idetop.ml | 521 +++++++++++++++++++++++++++++++++++++++++++++++++++ ide/ideutils.ml | 18 +- 6 files changed, 534 insertions(+), 550 deletions(-) delete mode 100644 ide/coqidetop.mllib create mode 100644 ide/ide_common.mllib delete mode 100644 ide/ide_slave.ml delete mode 100644 ide/ide_slave.mli create mode 100644 ide/idetop.ml (limited to 'ide') diff --git a/ide/coqidetop.mllib b/ide/coqidetop.mllib deleted file mode 100644 index df988d8f1..000000000 --- a/ide/coqidetop.mllib +++ /dev/null @@ -1,8 +0,0 @@ -Xml_lexer -Xml_parser -Xml_printer -Serialize -Richpp -Xmlprotocol -Document -Ide_slave diff --git a/ide/ide_common.mllib b/ide/ide_common.mllib new file mode 100644 index 000000000..050c282ef --- /dev/null +++ b/ide/ide_common.mllib @@ -0,0 +1,7 @@ +Xml_lexer +Xml_parser +Xml_printer +Serialize +Richpp +Xmlprotocol +Document diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml deleted file mode 100644 index 6c7ca4f8e..000000000 --- a/ide/ide_slave.ml +++ /dev/null @@ -1,518 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* " ^ Xmlprotocol.pr_full_value q r) - -(** Categories of commands *) - -let coqide_known_option table = List.mem table [ - ["Printing";"Implicit"]; - ["Printing";"Coercions"]; - ["Printing";"Matching"]; - ["Printing";"Synth"]; - ["Printing";"Notations"]; - ["Printing";"All"]; - ["Printing";"Records"]; - ["Printing";"Existential";"Instances"]; - ["Printing";"Universes"]; - ["Printing";"Unfocused"]] - -let is_known_option cmd = match Vernacprop.under_control cmd with - | VernacSetOption (_, o, BoolValue true) - | VernacUnsetOption (_, o) -> coqide_known_option o - | _ -> false - -(** Check whether a command is forbidden in the IDE *) - -let ide_cmd_checks ~id {CAst.loc;v=ast} = - let user_error s = CErrors.user_err ?loc ~hdr:"IDE" (str s) in - let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in - if is_debug ast then - user_error "Debug mode not available in the IDE"; - if is_known_option ast then - warn "Set this option from the IDE menu instead"; - if is_navigation_vernac ast || is_undo ast then - warn "Use IDE navigation instead" - -(** Interpretation (cf. [Ide_intf.interp]) *) - -let ide_doc = ref None -let get_doc () = Option.get !ide_doc -let set_doc doc = ide_doc := Some doc - -let add ((s,eid),(sid,verbose)) = - let doc = get_doc () in - let pa = Pcoq.Gram.parsable (Stream.of_string s) in - let loc_ast = Stm.parse_sentence ~doc sid pa in - let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in - set_doc doc; - let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in - ide_cmd_checks ~id:newid loc_ast; - (* TODO: the "" parameter is a leftover of the times the protocol - * used to include stderr/stdout output. - * - * Currently, we force all the output meant for the to go via the - * feedback mechanism, and we don't manipulate stderr/stdout, which - * are left to the client's discrection. The parameter is still there - * as not to break the core protocol for this minor change, but it should - * be removed in the next version of the protocol. - *) - newid, (rc, "") - -let edit_at id = - let doc = get_doc () in - match Stm.edit_at ~doc id with - | doc, `NewTip -> set_doc doc; CSig.Inl () - | doc, `Focus { Stm.start; stop; tip} -> set_doc doc; CSig.Inr (start, (stop, tip)) - -(* TODO: the "" parameter is a leftover of the times the protocol - * used to include stderr/stdout output. - * - * Currently, we force all the output meant for the to go via the - * feedback mechanism, and we don't manipulate stderr/stdout, which - * are left to the client's discrection. The parameter is still there - * as not to break the core protocol for this minor change, but it should - * be removed in the next version of the protocol. - *) -let query (route, (s,id)) = - let pa = Pcoq.Gram.parsable (Stream.of_string s) in - let doc = get_doc () in - Stm.query ~at:id ~doc ~route pa - -let annotate phrase = - let doc = get_doc () in - let {CAst.loc;v=ast} = - let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in - Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa - in - (* XXX: Width should be a parameter of annotate... *) - Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast) - -(** Goal display *) - -let hyp_next_tac sigma env decl = - let id = NamedDecl.get_id decl in - let ast = NamedDecl.get_type decl in - let id_s = Names.Id.to_string id in - let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in - [ - ("clear "^id_s),("clear "^id_s^"."); - ("apply "^id_s),("apply "^id_s^"."); - ("exact "^id_s),("exact "^id_s^"."); - ("generalize "^id_s),("generalize "^id_s^"."); - ("absurd <"^id_s^">"),("absurd "^type_s^".") - ] @ [ - ("discriminate "^id_s),("discriminate "^id_s^"."); - ("injection "^id_s),("injection "^id_s^".") - ] @ [ - ("rewrite "^id_s),("rewrite "^id_s^"."); - ("rewrite <- "^id_s),("rewrite <- "^id_s^".") - ] @ [ - ("elim "^id_s), ("elim "^id_s^"."); - ("inversion "^id_s), ("inversion "^id_s^"."); - ("inversion clear "^id_s), ("inversion_clear "^id_s^".") - ] - -let concl_next_tac sigma concl = - let expand s = (s,s^".") in - List.map expand ([ - "intro"; - "intros"; - "intuition" - ] @ [ - "reflexivity"; - "discriminate"; - "symmetry" - ] @ [ - "assumption"; - "omega"; - "ring"; - "auto"; - "eauto"; - "tauto"; - "trivial"; - "decide equality"; - "simpl"; - "subst"; - "red"; - "split"; - "left"; - "right" - ]) - -let process_goal sigma g = - let env = Goal.V82.env sigma g in - let min_env = Environ.reset_context env in - let id = Goal.uid g in - let ccl = - pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) - in - let process_hyp d (env,l) = - let d' = CompactedDecl.to_named_context d in - (List.fold_right Environ.push_named d' env, - (pr_compacted_decl env sigma d) :: l) in - let (_env, hyps) = - Context.Compacted.fold process_hyp - (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in - { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } - -let export_pre_goals pgs = - { - Interface.fg_goals = pgs.Proof.fg_goals; - Interface.bg_goals = pgs.Proof.bg_goals; - Interface.shelved_goals = pgs.Proof.shelved_goals; - Interface.given_up_goals = pgs.Proof.given_up_goals - } - -let goals () = - let doc = get_doc () in - set_doc @@ Stm.finish ~doc; - try - let pfts = Proof_global.give_me_the_proof () in - Some (export_pre_goals (Proof.map_structured_proof pfts process_goal)) - with Proof_global.NoCurrentProof -> None - -let evars () = - try - let doc = get_doc () in - set_doc @@ Stm.finish ~doc; - let pfts = Proof_global.give_me_the_proof () in - let all_goals, _, _, _, sigma = Proof.proof pfts in - let exl = Evar.Map.bindings (Evd.undefined_map sigma) in - let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in - let el = List.map map_evar exl in - Some el - with Proof_global.NoCurrentProof -> None - -let hints () = - try - let pfts = Proof_global.give_me_the_proof () in - let all_goals, _, _, _, sigma = Proof.proof pfts in - match all_goals with - | [] -> None - | g :: _ -> - let env = Goal.V82.env sigma g in - let hint_goal = concl_next_tac sigma g in - let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in - let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in - Some (hint_hyps, hint_goal) - with Proof_global.NoCurrentProof -> None - - -(** Other API calls *) - -let wait () = - let doc = get_doc () in - set_doc (Stm.wait ~doc) - -let status force = - (** We remove the initial part of the current [DirPath.t] - (usually Top in an interactive session, cf "coqtop -top"), - and display the other parts (opened sections and modules) *) - set_doc (Stm.finish ~doc:(get_doc ())); - if force then - set_doc (Stm.join ~doc:(get_doc ())); - let path = - let l = Names.DirPath.repr (Lib.cwd ()) in - List.rev_map Names.Id.to_string l - in - let proof = - try Some (Names.Id.to_string (Proof_global.get_current_proof_name ())) - with Proof_global.NoCurrentProof -> None - in - let allproofs = - let l = Proof_global.get_all_proof_names () in - List.map Names.Id.to_string l - in - { - Interface.status_path = path; - Interface.status_proofname = proof; - Interface.status_allproofs = allproofs; - Interface.status_proofnum = Stm.current_proof_depth ~doc:(get_doc ()); - } - -let export_coq_object t = { - Interface.coq_object_prefix = t.Search.coq_object_prefix; - Interface.coq_object_qualid = t.Search.coq_object_qualid; - Interface.coq_object_object = Pp.string_of_ppcmds (pr_lconstr_env (Global.env ()) Evd.empty t.Search.coq_object_object) -} - -let pattern_of_string ?env s = - let env = - match env with - | None -> Global.env () - | Some e -> e - in - let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in - let (_, pat) = Constrintern.intern_constr_pattern env Evd.empty constr in - pat - -let dirpath_of_string_list s = - let path = String.concat "." s in - let m = Pcoq.parse_string Pcoq.Constr.global path in - let {CAst.v=qid} = Libnames.qualid_of_reference m in - let id = - try Nametab.full_name_module qid - with Not_found -> - CErrors.user_err ~hdr:"Search.interface_search" - (str "Module " ++ str path ++ str " not found.") - in - id - -let import_search_constraint = function - | Interface.Name_Pattern s -> Search.Name_Pattern (Str.regexp s) - | Interface.Type_Pattern s -> Search.Type_Pattern (pattern_of_string s) - | Interface.SubType_Pattern s -> Search.SubType_Pattern (pattern_of_string s) - | Interface.In_Module ms -> Search.In_Module (dirpath_of_string_list ms) - | Interface.Include_Blacklist -> Search.Include_Blacklist - -let search flags = - List.map export_coq_object (Search.interface_search ( - List.map (fun (c, b) -> (import_search_constraint c, b)) flags) - ) - -let export_option_value = function - | Goptions.BoolValue b -> Interface.BoolValue b - | Goptions.IntValue x -> Interface.IntValue x - | Goptions.StringValue s -> Interface.StringValue s - | Goptions.StringOptValue s -> Interface.StringOptValue s - -let import_option_value = function - | Interface.BoolValue b -> Goptions.BoolValue b - | Interface.IntValue x -> Goptions.IntValue x - | Interface.StringValue s -> Goptions.StringValue s - | Interface.StringOptValue s -> Goptions.StringOptValue s - -let export_option_state s = { - Interface.opt_sync = true; - Interface.opt_depr = s.Goptions.opt_depr; - Interface.opt_name = s.Goptions.opt_name; - Interface.opt_value = export_option_value s.Goptions.opt_value; -} - -let get_options () = - let table = Goptions.get_tables () in - let fold key state accu = (key, export_option_state state) :: accu in - Goptions.OptionMap.fold fold table [] - -let set_options options = - let iter (name, value) = match import_option_value value with - | BoolValue b -> Goptions.set_bool_option_value name b - | IntValue i -> Goptions.set_int_option_value name i - | StringValue s -> Goptions.set_string_option_value name s - | StringOptValue (Some s) -> Goptions.set_string_option_value name s - | StringOptValue None -> Goptions.unset_option_value_gen name - in - List.iter iter options - -let about () = { - Interface.coqtop_version = Coq_config.version; - Interface.protocol_version = Xmlprotocol.protocol_version; - Interface.release_date = Coq_config.date; - Interface.compile_date = Coq_config.compile_date; -} - -let handle_exn (e, info) = - let dummy = Stateid.dummy in - let loc_of e = match Loc.get_loc e with - | Some loc -> Some (Loc.unloc loc) - | _ -> None in - let mk_msg () = CErrors.print ~info e in - match e with - | e -> - match Stateid.get info with - | Some (valid, _) -> valid, loc_of info, mk_msg () - | None -> dummy, loc_of info, mk_msg () - -let init = - let initialized = ref false in - fun file -> - if !initialized then anomaly (str "Already initialized.") - else begin - let init_sid = Stm.get_current_state ~doc:(get_doc ()) in - initialized := true; - match file with - | None -> init_sid - | Some file -> - let doc, initial_id, _ = - get_doc (), init_sid, `NewTip in - if Filename.check_suffix file ".v" then - Stm.set_compilation_hints file; - set_doc (Stm.finish ~doc); - initial_id - end - -(* Retrocompatibility stuff, disabled since 8.7 *) -let interp ((_raw, verbose), s) = - Stateid.dummy, CSig.Inr "The interp call has been disabled, please use Add." - -(** When receiving the Quit call, we don't directly do an [exit 0], - but rather set this reference, in order to send a final answer - before exiting. *) - -let quit = ref false - -(** Disabled *) -let print_ast id = Xml_datatype.PCData "ERROR" - -(** Grouping all call handlers together + error handling *) - -let eval_call c = - let interruptible f x = - catch_break := true; - Control.check_for_interrupt (); - let r = f x in - catch_break := false; - r - in - let handler = { - Interface.add = interruptible add; - Interface.edit_at = interruptible edit_at; - Interface.query = interruptible query; - Interface.goals = interruptible goals; - Interface.evars = interruptible evars; - Interface.hints = interruptible hints; - Interface.status = interruptible status; - Interface.search = interruptible search; - Interface.get_options = interruptible get_options; - Interface.set_options = interruptible set_options; - Interface.mkcases = interruptible Vernacentries.make_cases; - Interface.quit = (fun () -> quit := true); - Interface.init = interruptible init; - Interface.about = interruptible about; - Interface.wait = interruptible wait; - Interface.interp = interruptible interp; - Interface.handle_exn = handle_exn; - Interface.stop_worker = Stm.stop_worker; - Interface.print_ast = print_ast; - Interface.annotate = interruptible annotate; - } in - Xmlprotocol.abstract_eval_call handler c - -(** Message dispatching. - Since coqtop -ideslave starts 1 thread per slave, and each - thread forwards feedback messages from the slave to the GUI on the same - xml channel, we need mutual exclusion. The mutex should be per-channel, but - here we only use 1 channel. *) -let print_xml = - let m = Mutex.create () in - fun oc xml -> - Mutex.lock m; - try Xml_printer.print oc xml; Mutex.unlock m - with e -> let e = CErrors.push e in Mutex.unlock m; iraise e - -let slave_feeder fmt xml_oc msg = - let xml = Xmlprotocol.(of_feedback fmt msg) in - print_xml xml_oc xml - -(** The main loop *) - -(** Exceptions during eval_call should be converted into [Interface.Fail] - messages by [handle_exn] above. Otherwise, we die badly, without - trying to answer malformed requests. *) - -let msg_format = ref (fun () -> - let margin = Option.default 72 (Topfmt.get_margin ()) in - Xmlprotocol.Richpp margin - ) - -(* The loop ignores the command line arguments as the current model delegates - its handing to the toplevel container. *) -let loop _args ~state = - let open Vernac.State in - set_doc state.doc; - init_signal_handler (); - catch_break := false; - let in_ch, out_ch = Spawned.get_channels () in - let xml_oc = Xml_printer.make (Xml_printer.TChannel out_ch) in - let in_lb = Lexing.from_function (fun s len -> - CThread.thread_friendly_read in_ch s ~off:0 ~len) in - (* SEXP parser make *) - let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in - let () = Xml_parser.check_eof xml_ic false in - ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc)); - while not !quit do - try - let xml_query = Xml_parser.parse xml_ic in -(* pr_with_pid (Xml_printer.to_string_fmt xml_query); *) - let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in - let () = pr_debug_call q in - let r = eval_call q in - let () = pr_debug_answer q r in -(* pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *) - print_xml xml_oc Xmlprotocol.(of_answer (!msg_format ()) q r); - flush out_ch - with - | Xml_parser.Error (Xml_parser.Empty, _) -> - pr_debug "End of input, exiting gracefully."; - exit 0 - | Xml_parser.Error (err, loc) -> - pr_error ("XML syntax error: " ^ Xml_parser.error_msg err) - | Serialize.Marshal_error (msg,node) -> - pr_error "Unexpected XML message"; - pr_error ("Expected XML node: " ^ msg); - pr_error ("XML tree received: " ^ Xml_printer.to_string_fmt node) - | any -> - pr_debug ("Fatal exception in coqtop:\n" ^ Printexc.to_string any); - exit 1 - done; - pr_debug "Exiting gracefully."; - exit 0 - -let rec parse = function - | "--help-XML-protocol" :: rest -> - Xmlprotocol.document Xml_printer.to_string_fmt; exit 0 - | "--xml_format=Ppcmds" :: rest -> - msg_format := (fun () -> Xmlprotocol.Ppcmds); parse rest - | x :: rest -> x :: parse rest - | [] -> [] - -let () = Coqtop.toploop_init := (fun coq_args extra_args -> - let args = parse extra_args in - CoqworkmgrApi.(init High); - coq_args, args) - -let () = Coqtop.toploop_run := loop - -let () = Usage.add_to_usage "coqidetop" -" --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\ -\n --help-XML-protocol print documentation of the Coq XML protocol\n" diff --git a/ide/ide_slave.mli b/ide/ide_slave.mli deleted file mode 100644 index 9db9ecd12..000000000 --- a/ide/ide_slave.mli +++ /dev/null @@ -1,12 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* " ^ Xmlprotocol.pr_full_value q r) + +(** Categories of commands *) + +let coqide_known_option table = List.mem table [ + ["Printing";"Implicit"]; + ["Printing";"Coercions"]; + ["Printing";"Matching"]; + ["Printing";"Synth"]; + ["Printing";"Notations"]; + ["Printing";"All"]; + ["Printing";"Records"]; + ["Printing";"Existential";"Instances"]; + ["Printing";"Universes"]; + ["Printing";"Unfocused"]] + +let is_known_option cmd = match Vernacprop.under_control cmd with + | VernacSetOption (_, o, BoolValue true) + | VernacUnsetOption (_, o) -> coqide_known_option o + | _ -> false + +(** Check whether a command is forbidden in the IDE *) + +let ide_cmd_checks ~id {CAst.loc;v=ast} = + let user_error s = CErrors.user_err ?loc ~hdr:"IDE" (str s) in + let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in + if is_debug ast then + user_error "Debug mode not available in the IDE"; + if is_known_option ast then + warn "Set this option from the IDE menu instead"; + if is_navigation_vernac ast || is_undo ast then + warn "Use IDE navigation instead" + +(** Interpretation (cf. [Ide_intf.interp]) *) + +let ide_doc = ref None +let get_doc () = Option.get !ide_doc +let set_doc doc = ide_doc := Some doc + +let add ((s,eid),(sid,verbose)) = + let doc = get_doc () in + let pa = Pcoq.Gram.parsable (Stream.of_string s) in + let loc_ast = Stm.parse_sentence ~doc sid pa in + let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in + set_doc doc; + let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in + ide_cmd_checks ~id:newid loc_ast; + (* TODO: the "" parameter is a leftover of the times the protocol + * used to include stderr/stdout output. + * + * Currently, we force all the output meant for the to go via the + * feedback mechanism, and we don't manipulate stderr/stdout, which + * are left to the client's discrection. The parameter is still there + * as not to break the core protocol for this minor change, but it should + * be removed in the next version of the protocol. + *) + newid, (rc, "") + +let edit_at id = + let doc = get_doc () in + match Stm.edit_at ~doc id with + | doc, `NewTip -> set_doc doc; CSig.Inl () + | doc, `Focus { Stm.start; stop; tip} -> set_doc doc; CSig.Inr (start, (stop, tip)) + +(* TODO: the "" parameter is a leftover of the times the protocol + * used to include stderr/stdout output. + * + * Currently, we force all the output meant for the to go via the + * feedback mechanism, and we don't manipulate stderr/stdout, which + * are left to the client's discrection. The parameter is still there + * as not to break the core protocol for this minor change, but it should + * be removed in the next version of the protocol. + *) +let query (route, (s,id)) = + let pa = Pcoq.Gram.parsable (Stream.of_string s) in + let doc = get_doc () in + Stm.query ~at:id ~doc ~route pa + +let annotate phrase = + let doc = get_doc () in + let {CAst.loc;v=ast} = + let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in + Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa + in + (* XXX: Width should be a parameter of annotate... *) + Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast) + +(** Goal display *) + +let hyp_next_tac sigma env decl = + let id = NamedDecl.get_id decl in + let ast = NamedDecl.get_type decl in + let id_s = Names.Id.to_string id in + let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in + [ + ("clear "^id_s),("clear "^id_s^"."); + ("apply "^id_s),("apply "^id_s^"."); + ("exact "^id_s),("exact "^id_s^"."); + ("generalize "^id_s),("generalize "^id_s^"."); + ("absurd <"^id_s^">"),("absurd "^type_s^".") + ] @ [ + ("discriminate "^id_s),("discriminate "^id_s^"."); + ("injection "^id_s),("injection "^id_s^".") + ] @ [ + ("rewrite "^id_s),("rewrite "^id_s^"."); + ("rewrite <- "^id_s),("rewrite <- "^id_s^".") + ] @ [ + ("elim "^id_s), ("elim "^id_s^"."); + ("inversion "^id_s), ("inversion "^id_s^"."); + ("inversion clear "^id_s), ("inversion_clear "^id_s^".") + ] + +let concl_next_tac sigma concl = + let expand s = (s,s^".") in + List.map expand ([ + "intro"; + "intros"; + "intuition" + ] @ [ + "reflexivity"; + "discriminate"; + "symmetry" + ] @ [ + "assumption"; + "omega"; + "ring"; + "auto"; + "eauto"; + "tauto"; + "trivial"; + "decide equality"; + "simpl"; + "subst"; + "red"; + "split"; + "left"; + "right" + ]) + +let process_goal sigma g = + let env = Goal.V82.env sigma g in + let min_env = Environ.reset_context env in + let id = Goal.uid g in + let ccl = + pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) + in + let process_hyp d (env,l) = + let d' = CompactedDecl.to_named_context d in + (List.fold_right Environ.push_named d' env, + (pr_compacted_decl env sigma d) :: l) in + let (_env, hyps) = + Context.Compacted.fold process_hyp + (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in + { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } + +let export_pre_goals pgs = + { + Interface.fg_goals = pgs.Proof.fg_goals; + Interface.bg_goals = pgs.Proof.bg_goals; + Interface.shelved_goals = pgs.Proof.shelved_goals; + Interface.given_up_goals = pgs.Proof.given_up_goals + } + +let goals () = + let doc = get_doc () in + set_doc @@ Stm.finish ~doc; + try + let pfts = Proof_global.give_me_the_proof () in + Some (export_pre_goals (Proof.map_structured_proof pfts process_goal)) + with Proof_global.NoCurrentProof -> None + +let evars () = + try + let doc = get_doc () in + set_doc @@ Stm.finish ~doc; + let pfts = Proof_global.give_me_the_proof () in + let all_goals, _, _, _, sigma = Proof.proof pfts in + let exl = Evar.Map.bindings (Evd.undefined_map sigma) in + let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in + let el = List.map map_evar exl in + Some el + with Proof_global.NoCurrentProof -> None + +let hints () = + try + let pfts = Proof_global.give_me_the_proof () in + let all_goals, _, _, _, sigma = Proof.proof pfts in + match all_goals with + | [] -> None + | g :: _ -> + let env = Goal.V82.env sigma g in + let hint_goal = concl_next_tac sigma g in + let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in + let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in + Some (hint_hyps, hint_goal) + with Proof_global.NoCurrentProof -> None + + +(** Other API calls *) + +let wait () = + let doc = get_doc () in + set_doc (Stm.wait ~doc) + +let status force = + (** We remove the initial part of the current [DirPath.t] + (usually Top in an interactive session, cf "coqtop -top"), + and display the other parts (opened sections and modules) *) + set_doc (Stm.finish ~doc:(get_doc ())); + if force then + set_doc (Stm.join ~doc:(get_doc ())); + let path = + let l = Names.DirPath.repr (Lib.cwd ()) in + List.rev_map Names.Id.to_string l + in + let proof = + try Some (Names.Id.to_string (Proof_global.get_current_proof_name ())) + with Proof_global.NoCurrentProof -> None + in + let allproofs = + let l = Proof_global.get_all_proof_names () in + List.map Names.Id.to_string l + in + { + Interface.status_path = path; + Interface.status_proofname = proof; + Interface.status_allproofs = allproofs; + Interface.status_proofnum = Stm.current_proof_depth ~doc:(get_doc ()); + } + +let export_coq_object t = { + Interface.coq_object_prefix = t.Search.coq_object_prefix; + Interface.coq_object_qualid = t.Search.coq_object_qualid; + Interface.coq_object_object = Pp.string_of_ppcmds (pr_lconstr_env (Global.env ()) Evd.empty t.Search.coq_object_object) +} + +let pattern_of_string ?env s = + let env = + match env with + | None -> Global.env () + | Some e -> e + in + let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in + let (_, pat) = Constrintern.intern_constr_pattern env Evd.empty constr in + pat + +let dirpath_of_string_list s = + let path = String.concat "." s in + let m = Pcoq.parse_string Pcoq.Constr.global path in + let {CAst.v=qid} = Libnames.qualid_of_reference m in + let id = + try Nametab.full_name_module qid + with Not_found -> + CErrors.user_err ~hdr:"Search.interface_search" + (str "Module " ++ str path ++ str " not found.") + in + id + +let import_search_constraint = function + | Interface.Name_Pattern s -> Search.Name_Pattern (Str.regexp s) + | Interface.Type_Pattern s -> Search.Type_Pattern (pattern_of_string s) + | Interface.SubType_Pattern s -> Search.SubType_Pattern (pattern_of_string s) + | Interface.In_Module ms -> Search.In_Module (dirpath_of_string_list ms) + | Interface.Include_Blacklist -> Search.Include_Blacklist + +let search flags = + List.map export_coq_object (Search.interface_search ( + List.map (fun (c, b) -> (import_search_constraint c, b)) flags) + ) + +let export_option_value = function + | Goptions.BoolValue b -> Interface.BoolValue b + | Goptions.IntValue x -> Interface.IntValue x + | Goptions.StringValue s -> Interface.StringValue s + | Goptions.StringOptValue s -> Interface.StringOptValue s + +let import_option_value = function + | Interface.BoolValue b -> Goptions.BoolValue b + | Interface.IntValue x -> Goptions.IntValue x + | Interface.StringValue s -> Goptions.StringValue s + | Interface.StringOptValue s -> Goptions.StringOptValue s + +let export_option_state s = { + Interface.opt_sync = true; + Interface.opt_depr = s.Goptions.opt_depr; + Interface.opt_name = s.Goptions.opt_name; + Interface.opt_value = export_option_value s.Goptions.opt_value; +} + +let get_options () = + let table = Goptions.get_tables () in + let fold key state accu = (key, export_option_state state) :: accu in + Goptions.OptionMap.fold fold table [] + +let set_options options = + let iter (name, value) = match import_option_value value with + | BoolValue b -> Goptions.set_bool_option_value name b + | IntValue i -> Goptions.set_int_option_value name i + | StringValue s -> Goptions.set_string_option_value name s + | StringOptValue (Some s) -> Goptions.set_string_option_value name s + | StringOptValue None -> Goptions.unset_option_value_gen name + in + List.iter iter options + +let about () = { + Interface.coqtop_version = Coq_config.version; + Interface.protocol_version = Xmlprotocol.protocol_version; + Interface.release_date = Coq_config.date; + Interface.compile_date = Coq_config.compile_date; +} + +let handle_exn (e, info) = + let dummy = Stateid.dummy in + let loc_of e = match Loc.get_loc e with + | Some loc -> Some (Loc.unloc loc) + | _ -> None in + let mk_msg () = CErrors.print ~info e in + match e with + | e -> + match Stateid.get info with + | Some (valid, _) -> valid, loc_of info, mk_msg () + | None -> dummy, loc_of info, mk_msg () + +let init = + let initialized = ref false in + fun file -> + if !initialized then anomaly (str "Already initialized.") + else begin + let init_sid = Stm.get_current_state ~doc:(get_doc ()) in + initialized := true; + match file with + | None -> init_sid + | Some file -> + let doc, initial_id, _ = + get_doc (), init_sid, `NewTip in + if Filename.check_suffix file ".v" then + Stm.set_compilation_hints file; + set_doc (Stm.finish ~doc); + initial_id + end + +(* Retrocompatibility stuff, disabled since 8.7 *) +let interp ((_raw, verbose), s) = + Stateid.dummy, CSig.Inr "The interp call has been disabled, please use Add." + +(** When receiving the Quit call, we don't directly do an [exit 0], + but rather set this reference, in order to send a final answer + before exiting. *) + +let quit = ref false + +(** Disabled *) +let print_ast id = Xml_datatype.PCData "ERROR" + +(** Grouping all call handlers together + error handling *) + +let eval_call c = + let interruptible f x = + catch_break := true; + Control.check_for_interrupt (); + let r = f x in + catch_break := false; + r + in + let handler = { + Interface.add = interruptible add; + Interface.edit_at = interruptible edit_at; + Interface.query = interruptible query; + Interface.goals = interruptible goals; + Interface.evars = interruptible evars; + Interface.hints = interruptible hints; + Interface.status = interruptible status; + Interface.search = interruptible search; + Interface.get_options = interruptible get_options; + Interface.set_options = interruptible set_options; + Interface.mkcases = interruptible Vernacentries.make_cases; + Interface.quit = (fun () -> quit := true); + Interface.init = interruptible init; + Interface.about = interruptible about; + Interface.wait = interruptible wait; + Interface.interp = interruptible interp; + Interface.handle_exn = handle_exn; + Interface.stop_worker = Stm.stop_worker; + Interface.print_ast = print_ast; + Interface.annotate = interruptible annotate; + } in + Xmlprotocol.abstract_eval_call handler c + +(** Message dispatching. + Since coqtop -ideslave starts 1 thread per slave, and each + thread forwards feedback messages from the slave to the GUI on the same + xml channel, we need mutual exclusion. The mutex should be per-channel, but + here we only use 1 channel. *) +let print_xml = + let m = Mutex.create () in + fun oc xml -> + Mutex.lock m; + try Xml_printer.print oc xml; Mutex.unlock m + with e -> let e = CErrors.push e in Mutex.unlock m; iraise e + +let slave_feeder fmt xml_oc msg = + let xml = Xmlprotocol.(of_feedback fmt msg) in + print_xml xml_oc xml + +(** The main loop *) + +(** Exceptions during eval_call should be converted into [Interface.Fail] + messages by [handle_exn] above. Otherwise, we die badly, without + trying to answer malformed requests. *) + +let msg_format = ref (fun () -> + let margin = Option.default 72 (Topfmt.get_margin ()) in + Xmlprotocol.Richpp margin + ) + +(* The loop ignores the command line arguments as the current model delegates + its handing to the toplevel container. *) +let loop ~opts:_ ~state = + let open Vernac.State in + set_doc state.doc; + init_signal_handler (); + catch_break := false; + let in_ch, out_ch = Spawned.get_channels () in + let xml_oc = Xml_printer.make (Xml_printer.TChannel out_ch) in + let in_lb = Lexing.from_function (fun s len -> + CThread.thread_friendly_read in_ch s ~off:0 ~len) in + (* SEXP parser make *) + let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in + let () = Xml_parser.check_eof xml_ic false in + ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc)); + while not !quit do + try + let xml_query = Xml_parser.parse xml_ic in +(* pr_with_pid (Xml_printer.to_string_fmt xml_query); *) + let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in + let () = pr_debug_call q in + let r = eval_call q in + let () = pr_debug_answer q r in +(* pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *) + print_xml xml_oc Xmlprotocol.(of_answer (!msg_format ()) q r); + flush out_ch + with + | Xml_parser.Error (Xml_parser.Empty, _) -> + pr_debug "End of input, exiting gracefully."; + exit 0 + | Xml_parser.Error (err, loc) -> + pr_error ("XML syntax error: " ^ Xml_parser.error_msg err) + | Serialize.Marshal_error (msg,node) -> + pr_error "Unexpected XML message"; + pr_error ("Expected XML node: " ^ msg); + pr_error ("XML tree received: " ^ Xml_printer.to_string_fmt node) + | any -> + pr_debug ("Fatal exception in coqtop:\n" ^ Printexc.to_string any); + exit 1 + done; + pr_debug "Exiting gracefully."; + exit 0 + +let rec parse = function + | "--help-XML-protocol" :: rest -> + Xmlprotocol.document Xml_printer.to_string_fmt; exit 0 + | "--xml_format=Ppcmds" :: rest -> + msg_format := (fun () -> Xmlprotocol.Ppcmds); parse rest + | x :: rest -> x :: parse rest + | [] -> [] + +let () = Usage.add_to_usage "coqidetop" +" --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\ +\n --help-XML-protocol print documentation of the Coq XML protocol\n" + +let islave_init ~opts extra_args = + let args = parse extra_args in + CoqworkmgrApi.(init High); + opts, args + +let () = + let open Coqtop in + let custom = { init = islave_init; run = loop; } in + start_coq custom diff --git a/ide/ideutils.ml b/ide/ideutils.ml index bdb39e94a..e96b99299 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -289,16 +289,10 @@ let coqtop_path () = | Some s -> s | None -> match cmd_coqtop#get with - | Some s -> s - | None -> - try - let old_prog = Sys.executable_name in - let pos = String.length old_prog - 6 in - let i = Str.search_backward (Str.regexp_string "coqide") old_prog pos - in - let new_prog = Bytes.of_string old_prog in - Bytes.blit_string "coqtop" 0 new_prog i 6; - let new_prog = Bytes.to_string new_prog in + | Some s -> s + | None -> + try + let new_prog = System.get_toplevel_path "coqidetop" in if Sys.file_exists new_prog then new_prog else let in_macos_bundle = @@ -306,8 +300,8 @@ let coqtop_path () = (Filename.dirname new_prog) (Filename.concat "../Resources/bin" (Filename.basename new_prog)) in if Sys.file_exists in_macos_bundle then in_macos_bundle - else "coqtop" - with Not_found -> "coqtop" + else "coqidetop" + with Not_found -> "coqidetop" in file (* In win32, when a command-line is to be executed via cmd.exe -- cgit v1.2.3