From 0a829ad04841d0973b22b4407b95f518276b66e7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 25 Jun 2014 11:09:55 +0200 Subject: cut toploop(s) out of coqtop: now they are loaded dynamically User interface writers can drop a footop.cmxs in $(COQLIB)/toploop/ and pass -toploop footop to customize the coq main loop. A toploop must set Coqtop.toploop_init and Coqtop.toploop_run to functions respectively initializing the toploop (and parsing toploop specific arguments) and running the main loop itself. For backward compatibility -ideslave and -async-proofs worker do set the toploop to coqidetop and stmworkertop respectively. --- Makefile.build | 19 +- Makefile.common | 5 +- idetop/coqidetop.mllib | 1 + idetop/ide_slave.ml | 453 ++++++++++++++++++++++++++++++++++++++++++++++++ stm/stmworkertop.ml | 15 ++ stm/stmworkertop.mllib | 1 + toplevel/coqinit.ml | 4 + toplevel/coqtop.ml | 56 +++--- toplevel/coqtop.mli | 6 + toplevel/ide_slave.ml | 446 ----------------------------------------------- toplevel/ide_slave.mli | 17 -- toplevel/mltop.ml | 5 +- toplevel/mltop.mli | 1 + toplevel/toplevel.mllib | 1 - 14 files changed, 531 insertions(+), 499 deletions(-) create mode 100644 idetop/coqidetop.mllib create mode 100644 idetop/ide_slave.ml create mode 100644 stm/stmworkertop.ml create mode 100644 stm/stmworkertop.mllib delete mode 100644 toplevel/ide_slave.ml delete mode 100644 toplevel/ide_slave.mli diff --git a/Makefile.build b/Makefile.build index 6d12063ca8..0f05dc606a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -210,7 +210,7 @@ miniopt: $(COQTOPEXE) pluginsopt minibyte: $(COQTOPBYTE) pluginsbyte ifeq ($(BEST),opt) -$(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) +$(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -thread -o $@ $(STRIP) $@ @@ -219,7 +219,7 @@ $(COQTOPEXE): $(COQTOPBYTE) cp $< $@ endif -$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) +$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -thread -o $@ @@ -301,8 +301,8 @@ IDEFILES=$(wildcard ide/coq*.lang) ide/coq_style.xml ide/coq.png ide/mac_default coqide-binaries: coqide-$(HASCOQIDE) coqide-no: -coqide-byte: $(COQIDEBYTE) $(COQIDE) -coqide-opt: $(COQIDEBYTE) $(COQIDE) +coqide-byte: $(COQIDEBYTE) $(COQIDE) $(IDETOPLOOPCMA) +coqide-opt: $(COQIDEBYTE) $(COQIDE) $(IDETOPLOOPCMA) $(IDETOPLOOPCMA:.cma=.cmxs) coqide-files: $(IDEFILES) ifeq ($(HASCOQIDE),opt) @@ -334,6 +334,11 @@ endif install-ide-bin: $(MKDIR) $(FULLBINDIR) $(INSTALLBIN) $(COQIDE) $(FULLBINDIR) + $(MKDIR) $(FULLCOQLIB)/toploop + $(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/ +ifeq ($(BEST),opt) + $(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ +endif install-ide-devfiles: $(MKDIR) $(FULLCOQLIB) @@ -618,6 +623,12 @@ install-coqlight: install-binaries install-library-light install-binaries: install-tools $(MKDIR) $(FULLBINDIR) $(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR) + $(MKDIR) $(FULLCOQLIB)/toploop + $(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/ +ifeq ($(BEST),opt) + $(INSTALLBIN) $(TOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ +endif + install-tools: $(MKDIR) $(FULLBINDIR) diff --git a/Makefile.common b/Makefile.common index d971e9b2eb..4b6cc764a9 100644 --- a/Makefile.common +++ b/Makefile.common @@ -72,7 +72,7 @@ PLUGINS:=\ SRCDIRS:=\ $(CORESRCDIRS) \ - tools tools/coqdoc \ + tools tools/coqdoc idetop\ $(addprefix plugins/, $(PLUGINS)) IDESRCDIRS:=\ @@ -159,6 +159,8 @@ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma \ stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma +TOPLOOPCMA:=stm/stmworkertop.cma + GRAMMARCMA:=tools/compat5.cmo grammar/grammar.cma OMEGACMA:=plugins/omega/omega_plugin.cma @@ -212,6 +214,7 @@ LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa) IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo lib/xml_printer.cmo lib/errors.cmo lib/spawn.cmo IDECMA:=ide/ide.cma +IDETOPLOOPCMA=idetop/coqidetop.cma LINKIDE:=$(IDEDEPS) $(IDECMA) ide/coqide_main.ml LINKIDEOPT:=$(IDEOPTDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml diff --git a/idetop/coqidetop.mllib b/idetop/coqidetop.mllib new file mode 100644 index 0000000000..7826877448 --- /dev/null +++ b/idetop/coqidetop.mllib @@ -0,0 +1 @@ +Ide_slave diff --git a/idetop/ide_slave.ml b/idetop/ide_slave.ml new file mode 100644 index 0000000000..2185084a01 --- /dev/null +++ b/idetop/ide_slave.ml @@ -0,0 +1,453 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + flush_all (); + Pp_control.std_ft := out_ft; + Pp_control.err_ft := out_ft; + Pp_control.deep_ft := deep_out_ft; + ), + (fun () -> Format.pp_print_flush out_ft (); + let r = Buffer.contents out_buff in + Buffer.clear out_buff; r) + +let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s + +let pr_debug s = + if !Flags.debug then pr_with_pid s +let pr_debug_call q = + if !Flags.debug then pr_with_pid ("<-- " ^ Serialize.pr_call q) +let pr_debug_answer q r = + if !Flags.debug then pr_with_pid ("--> " ^ Serialize.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"]] + +let is_known_option cmd = match cmd with + | VernacSetOption (o,BoolValue true) + | VernacUnsetOption o -> coqide_known_option o + | _ -> false + +let is_debug cmd = match cmd with + | VernacSetOption (["Ltac";"Debug"], _) -> true + | _ -> false + +let is_query cmd = match cmd with + | VernacChdir None + | VernacMemOption _ + | VernacPrintOption _ + | VernacCheckMayEval _ + | VernacGlobalCheck _ + | VernacPrint _ + | VernacSearch _ + | VernacLocate _ -> true + | _ -> false + +let is_undo cmd = match cmd with + | VernacUndo _ | VernacUndoTo _ -> true + | _ -> false + +(** Check whether a command is forbidden by CoqIDE *) + +let coqide_cmd_checks (loc,ast) = + let user_error s = Errors.user_err_loc (loc, "CoqIde", str s) in + if is_debug ast then + user_error "Debug mode not available within CoqIDE"; + if is_known_option ast then + msg_warning (strbrk"This will not work. Use CoqIDE display menu instead"); + if Vernac.is_navigation_vernac ast || is_undo ast then + msg_warning (strbrk "Rather use CoqIDE navigation instead"); + if is_query ast then + msg_warning (strbrk "Query commands should not be inserted in scripts") + +(** Interpretation (cf. [Ide_intf.interp]) *) + +let add ((s,eid),(sid,verbose)) = + let newid, rc = Stm.add ~ontop:sid verbose ~check:coqide_cmd_checks eid s in + let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in + newid, (rc, read_stdout ()) + +let edit_at id = + match Stm.edit_at id with + | `NewTip -> CSig.Inl () + | `Focus { Stm.start; stop; tip} -> CSig.Inr (start, (stop, tip)) + +let query (s,id) = Stm.query ~at:id s; read_stdout () + +(** Goal display *) + +let hyp_next_tac sigma env (id,_,ast) = + let id_s = Names.Id.to_string id in + let type_s = string_of_ppcmds (pr_ltype_env env 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 id = Goal.uid g in + let ccl = + let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in + string_of_ppcmds (pr_goal_concl_style_env env norm_constr) in + let process_hyp h_env d acc = + let d = Context.map_named_declaration (Reductionops.nf_evar sigma) d in + (string_of_ppcmds (pr_var_decl h_env d)) :: acc in + let hyps = + List.rev (Environ.fold_named_context process_hyp env ~init: []) in + { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } + +let goals () = + Stm.finish (); + let s = read_stdout () in + if not (String.is_empty s) then msg_info (str s); + try + let pfts = Proof_global.give_me_the_proof () in + let (goals, zipper, shelf, given_up, sigma) = Proof.proof pfts in + let fg = List.map (process_goal sigma) goals in + let map_zip (lg, rg) = + let lg = List.map (process_goal sigma) lg in + let rg = List.map (process_goal sigma) rg in + (lg, rg) + in + let bg = List.map map_zip zipper in + let shelf = List.map (process_goal sigma) shelf in + let given_up = List.map (process_goal sigma) given_up in + Some { Interface.fg_goals = fg; + Interface.bg_goals = bg; + shelved_goals = shelf; + given_up_goals = given_up; } + with Proof_global.NoCurrentProof -> None + +let evars () = + try + Stm.finish (); + let s = read_stdout () in + if not (String.is_empty s) then msg_info (str s); + let pfts = Proof_global.give_me_the_proof () in + let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in + let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in + let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar 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 { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals 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 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) *) + Stm.finish (); + if force then Stm.join (); + let s = read_stdout () in + if not (String.is_empty s) then msg_info (str s); + 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 (); + } + +let search flags = Search.interface_search flags + +let get_options () = + let table = Goptions.get_tables () in + let fold key state accu = (key, state) :: accu in + Goptions.OptionMap.fold fold table [] + +let set_options options = + let iter (name, value) = match 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 + in + List.iter iter options + +let about () = { + Interface.coqtop_version = Coq_config.version; + Interface.protocol_version = Serialize.protocol_version; + Interface.release_date = Coq_config.date; + Interface.compile_date = Coq_config.compile_date; +} + +let handle_exn e = + let dummy = Stateid.dummy in + let loc_of e = match Loc.get_loc e with + | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc) + | _ -> None in + let mk_msg e = read_stdout ()^"\n"^string_of_ppcmds (Errors.print e) in + match e with + | Errors.Drop -> dummy, None, "Drop is not allowed by coqide!" + | Errors.Quit -> dummy, None, "Quit is not allowed by coqide!" + | e -> + match Stateid.get e with + | Some (valid, _) -> valid, loc_of e, mk_msg e + | None -> dummy, loc_of e, mk_msg e + +let init = + let initialized = ref false in + fun file -> + if !initialized then anomaly (str "Already initialized") + else begin + initialized := true; + match file with + | None -> Stm.get_current_state () + | Some file -> + let dir = Filename.dirname file in + let open Loadpath in let open CUnix in + let initial_id, _ = + if not (is_in_load_paths (physical_path_of_string dir)) then + Stm.add false ~ontop:(Stm.get_current_state ()) + 0 (Printf.sprintf "Add LoadPath \"%s\". " dir) + else Stm.get_current_state (), `NewTip in + Stm.set_compilation_hints file; + initial_id + end + +(* Retrocompatibility stuff *) +let interp ((_raw, verbose), s) = + let vernac_parse s = + let pa = Pcoq.Gram.parsable (Stream.of_string s) in + Flags.with_option Flags.we_are_parsing (fun () -> + match Pcoq.Gram.entry_parse Pcoq.main_entry pa with + | None -> raise (Invalid_argument "vernac_parse") + | Some ast -> ast) + () in + Stm.interp verbose (vernac_parse s); + Stm.get_current_state (), CSig.Inl (read_stdout ()) + +(** 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 + +(** Grouping all call handlers together + error handling *) + +let eval_call xml_oc log c = + let interruptible f x = + catch_break := true; + Control.check_for_interrupt (); + let r = f x in + catch_break := false; + let out = read_stdout () in + if not (String.is_empty out) then log (str out); + 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.interp = interruptible interp; + Interface.handle_exn = handle_exn; + Interface.stop_worker = Stm.stop_worker; + } in + Serialize.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 = Errors.push e in Mutex.unlock m; raise e + + +let slave_logger xml_oc level message = + (* convert the message into XML *) + let msg = string_of_ppcmds (hov 0 message) in + let message = { + Interface.message_level = level; + Interface.message_content = msg; + } in + let () = pr_debug (Printf.sprintf "-> %S" msg) in + let xml = Serialize.of_message message in + print_xml xml_oc xml + +let slave_feeder xml_oc msg = + let xml = Serialize.of_feedback 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 loop () = + 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 + CThread.prepare_in_channel_for_thread_friendly_io in_ch; + let in_lb = Lexing.from_function (fun s len -> + CThread.thread_friendly_read in_ch s ~off:0 ~len) in + let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in + let () = Xml_parser.check_eof xml_ic false in + set_logger (slave_logger xml_oc); + set_feeder (slave_feeder xml_oc); + (* We'll handle goal fetching and display in our own way *) + Vernacentries.enable_goal_printing := false; + Vernacentries.qed_display_script := false; + Flags.make_term_color false; + 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 q = Serialize.to_call xml_query in + let () = pr_debug_call q in + let r = eval_call xml_oc (slave_logger xml_oc Interface.Notice) q in + let () = pr_debug_answer q r in +(* pr_with_pid (Xml_printer.to_string_fmt (Serialize.of_answer q r)); *) + print_xml xml_oc (Serialize.of_answer 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_debug ("Syntax error in query: " ^ Xml_parser.error_msg err); + exit 1 + | Serialize.Marshal_error -> + pr_debug "Incorrect query."; + exit 1 + | any -> + pr_debug ("Fatal exception in coqtop:\n" ^ Printexc.to_string any); + exit 1 + done; + pr_debug "Exiting gracefully."; + exit 0 + +let () = Coqtop.toploop_init := (fun args -> + Flags.make_silent true; + init_stdout (); + args) + +let () = Coqtop.toploop_run := loop diff --git a/stm/stmworkertop.ml b/stm/stmworkertop.ml new file mode 100644 index 0000000000..50afd97ab5 --- /dev/null +++ b/stm/stmworkertop.ml @@ -0,0 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + Flags.make_silent true; + Stm.slave_init_stdout (); + args) + +let () = Coqtop.toploop_run := Stm.slave_main_loop + diff --git a/stm/stmworkertop.mllib b/stm/stmworkertop.mllib new file mode 100644 index 0000000000..78b54b2ea9 --- /dev/null +++ b/stm/stmworkertop.mllib @@ -0,0 +1 @@ +Stmworkertop diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 85a59c50ee..45aa980b79 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -92,6 +92,10 @@ let init_load_path () = (* NOTE: These directories are searched from last to first *) (* first, developer specific directory to open *) if Coq_config.local then coq_add_path (coqlib/"dev") "dev"; + (* main loops *) + Mltop.add_ml_dir (coqlib/"toploop"); + if Coq_config.local then Mltop.add_ml_dir (coqlib/"stm"); + if Coq_config.local then Mltop.add_ml_dir (coqlib/"idetop"); (* then standard library *) add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false; (* then plugins *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a4770b348a..0523ffd44a 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -38,6 +38,20 @@ let print_header () = ppnl (str ("Welcome to Coq "^ver^" ("^rev^")")); pp_flush () +let warning s = msg_warning (strbrk s) + +let toploop = ref None +let toploop_init = ref (fun x -> x) +let toploop_run = ref (fun () -> + if Dumpglob.dump () then begin + if_verbose warning "Dumpglob cannot be used in interactive mode."; + Dumpglob.noglob () + end; + Coqloop.loop(); + (* Initialise and launch the Ocaml toplevel *) + Coqinit.init_ocaml_path(); + Mltop.ocaml_toploop()) + let output_context = ref false let memory_stat = ref false @@ -201,8 +215,6 @@ let error_missing_arg s = prerr_endline "See --help for the syntax of supported options"; exit 1 -let warning s = msg_warning (strbrk s) - let filter_opts = ref false let exitcode () = if !filter_opts then 2 else 0 @@ -217,6 +229,7 @@ let get_async_proofs_mode opt next = function | "on" -> Flags.APonParallel 0 | "worker" -> let n = int_of_string (next()) in assert (n > 0); + toploop := Some "stmworkertop"; Flags.APonParallel n | "lazy" -> Flags.APonLazy | _ -> prerr_endline ("Error: on/off/lazy/worker expected after "^opt); exit 1 @@ -341,7 +354,7 @@ let parse_args arglist = |"-async-proofs-j" -> Flags.async_proofs_n_workers := (get_int opt (next ())) |"-async-proofs-worker-flags" -> - Flags.async_proofs_worker_flags := Some (next ()) + Flags.async_proofs_worker_flags := Some (next ()); |"-compat" -> Flags.compat_version := get_compat_version (next ()) |"-compile" -> add_compile false (next ()) |"-compile-verbose" -> add_compile true (next ()) @@ -363,6 +376,7 @@ let parse_args arglist = |"-main-channel" -> Spawned.main_channel := get_host_port opt (next()) |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) |"-vi2vo" -> add_compile false (next ()); Flags.compilation_mode := Vi2Vo + |"-toploop" -> toploop := Some (next ()) (* Options with zero arg *) |"-batch" -> set_batch_mode () @@ -377,7 +391,7 @@ let parse_args arglist = |"-h"|"-H"|"-?"|"-help"|"--help" -> usage () |"--help-XML-protocol" -> Serialize.document Xml_printer.to_string_fmt; exit 0 - |"-ideslave" -> Flags.ide_slave := true + |"-ideslave" -> toploop := Some "coqidetop"; Flags.ide_slave := true |"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet |"-indices-matter" -> Indtypes.enforce_indices_matter () |"-just-parsing" -> Vernac.just_parsing := true @@ -436,27 +450,22 @@ let init arglist = begin try let extras = parse_args arglist in - if not (List.is_empty extras) && not !filter_opts then begin - prerr_endline ("Don't know what to do with " ^ String.concat " " extras); - prerr_endline "See --help for the list of supported options"; - exit 1 - end; (* If we have been spawned by the Spawn module, this has to be done * early since the master waits us to connect back *) Spawned.init_channels (); Envars.set_coqlib Errors.error; - if !print_where then (print_endline (Envars.coqlib ()); exit (exitcode ())); + if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ())); if !print_config then (Usage.print_config (); exit (exitcode ())); if !filter_opts then (print_string (String.concat "\n" extras); exit 0); - if !Flags.ide_slave then begin - Flags.make_silent true; - Ide_slave.init_stdout () - end else if Flags.async_proofs_is_worker () then begin - Flags.make_silent true; - Stm.slave_init_stdout () + init_load_path (); + Option.iter Mltop.load_ml_object_raw !toploop; + let extras = !toploop_init extras in + if not (List.is_empty extras) then begin + prerr_endline ("Don't know what to do with "^String.concat " " extras); + prerr_endline "See --help for the list of supported options"; + exit 1 end; if_verbose print_header (); - init_load_path (); inputstate (); Mltop.init_known_plugins (); set_vm_opt (); @@ -500,18 +509,7 @@ let start () = let () = init_toplevel (List.tl (Array.to_list Sys.argv)) in (* In batch mode, Coqtop has already exited at this point. In interactive one, dump glob is nothing but garbage ... *) - if !Flags.ide_slave then - Ide_slave.loop () - else if Flags.async_proofs_is_worker () then - Stm.slave_main_loop () - else - let () = if Dumpglob.dump () then - let () = if_verbose warning "Dumpglob cannot be used in interactive mode." in - Dumpglob.noglob () in - Coqloop.loop(); - (* Initialise and launch the Ocaml toplevel *) - Coqinit.init_ocaml_path(); - Mltop.ocaml_toploop(); + !toploop_run (); exit 1 (* [Coqtop.start] will be called by the code produced by coqmktop *) diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index ee511edbbc..875cf2ec0f 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -14,3 +14,9 @@ val init_toplevel : string list -> unit val start : unit -> unit + + +(* For other toploops *) +val toploop_init : (string list -> string list) ref +val toploop_run : (unit -> unit) ref + diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml deleted file mode 100644 index 8f2fa69a00..0000000000 --- a/toplevel/ide_slave.ml +++ /dev/null @@ -1,446 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - flush_all (); - Pp_control.std_ft := out_ft; - Pp_control.err_ft := out_ft; - Pp_control.deep_ft := deep_out_ft; - ), - (fun () -> Format.pp_print_flush out_ft (); - let r = Buffer.contents out_buff in - Buffer.clear out_buff; r) - -let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s - -let pr_debug s = - if !Flags.debug then pr_with_pid s -let pr_debug_call q = - if !Flags.debug then pr_with_pid ("<-- " ^ Serialize.pr_call q) -let pr_debug_answer q r = - if !Flags.debug then pr_with_pid ("--> " ^ Serialize.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"]] - -let is_known_option cmd = match cmd with - | VernacSetOption (o,BoolValue true) - | VernacUnsetOption o -> coqide_known_option o - | _ -> false - -let is_debug cmd = match cmd with - | VernacSetOption (["Ltac";"Debug"], _) -> true - | _ -> false - -let is_query cmd = match cmd with - | VernacChdir None - | VernacMemOption _ - | VernacPrintOption _ - | VernacCheckMayEval _ - | VernacGlobalCheck _ - | VernacPrint _ - | VernacSearch _ - | VernacLocate _ -> true - | _ -> false - -let is_undo cmd = match cmd with - | VernacUndo _ | VernacUndoTo _ -> true - | _ -> false - -(** Check whether a command is forbidden by CoqIDE *) - -let coqide_cmd_checks (loc,ast) = - let user_error s = Errors.user_err_loc (loc, "CoqIde", str s) in - if is_debug ast then - user_error "Debug mode not available within CoqIDE"; - if is_known_option ast then - msg_warning (strbrk"This will not work. Use CoqIDE display menu instead"); - if Vernac.is_navigation_vernac ast || is_undo ast then - msg_warning (strbrk "Rather use CoqIDE navigation instead"); - if is_query ast then - msg_warning (strbrk "Query commands should not be inserted in scripts") - -(** Interpretation (cf. [Ide_intf.interp]) *) - -let add ((s,eid),(sid,verbose)) = - let newid, rc = Stm.add ~ontop:sid verbose ~check:coqide_cmd_checks eid s in - let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in - newid, (rc, read_stdout ()) - -let edit_at id = - match Stm.edit_at id with - | `NewTip -> CSig.Inl () - | `Focus { Stm.start; stop; tip} -> CSig.Inr (start, (stop, tip)) - -let query (s,id) = Stm.query ~at:id s; read_stdout () - -(** Goal display *) - -let hyp_next_tac sigma env (id,_,ast) = - let id_s = Names.Id.to_string id in - let type_s = string_of_ppcmds (pr_ltype_env env 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 id = Goal.uid g in - let ccl = - let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in - string_of_ppcmds (pr_goal_concl_style_env env norm_constr) in - let process_hyp h_env d acc = - let d = Context.map_named_declaration (Reductionops.nf_evar sigma) d in - (string_of_ppcmds (pr_var_decl h_env d)) :: acc in - let hyps = - List.rev (Environ.fold_named_context process_hyp env ~init: []) in - { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } - -let goals () = - Stm.finish (); - let s = read_stdout () in - if not (String.is_empty s) then msg_info (str s); - try - let pfts = Proof_global.give_me_the_proof () in - let (goals, zipper, shelf, given_up, sigma) = Proof.proof pfts in - let fg = List.map (process_goal sigma) goals in - let map_zip (lg, rg) = - let lg = List.map (process_goal sigma) lg in - let rg = List.map (process_goal sigma) rg in - (lg, rg) - in - let bg = List.map map_zip zipper in - let shelf = List.map (process_goal sigma) shelf in - let given_up = List.map (process_goal sigma) given_up in - Some { Interface.fg_goals = fg; - Interface.bg_goals = bg; - shelved_goals = shelf; - given_up_goals = given_up; } - with Proof_global.NoCurrentProof -> None - -let evars () = - try - Stm.finish (); - let s = read_stdout () in - if not (String.is_empty s) then msg_info (str s); - let pfts = Proof_global.give_me_the_proof () in - let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in - let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in - let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar 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 { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals 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 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) *) - Stm.finish (); - if force then Stm.join (); - let s = read_stdout () in - if not (String.is_empty s) then msg_info (str s); - 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 (); - } - -let search flags = Search.interface_search flags - -let get_options () = - let table = Goptions.get_tables () in - let fold key state accu = (key, state) :: accu in - Goptions.OptionMap.fold fold table [] - -let set_options options = - let iter (name, value) = match 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 - in - List.iter iter options - -let about () = { - Interface.coqtop_version = Coq_config.version; - Interface.protocol_version = Serialize.protocol_version; - Interface.release_date = Coq_config.date; - Interface.compile_date = Coq_config.compile_date; -} - -let handle_exn e = - let dummy = Stateid.dummy in - let loc_of e = match Loc.get_loc e with - | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc) - | _ -> None in - let mk_msg e = read_stdout ()^"\n"^string_of_ppcmds (Errors.print e) in - match e with - | Errors.Drop -> dummy, None, "Drop is not allowed by coqide!" - | Errors.Quit -> dummy, None, "Quit is not allowed by coqide!" - | e -> - match Stateid.get e with - | Some (valid, _) -> valid, loc_of e, mk_msg e - | None -> dummy, loc_of e, mk_msg e - -let init = - let initialized = ref false in - fun file -> - if !initialized then anomaly (str "Already initialized") - else begin - initialized := true; - match file with - | None -> Stm.get_current_state () - | Some file -> - let dir = Filename.dirname file in - let open Loadpath in let open CUnix in - let initial_id, _ = - if not (is_in_load_paths (physical_path_of_string dir)) then - Stm.add false ~ontop:(Stm.get_current_state ()) - 0 (Printf.sprintf "Add LoadPath \"%s\". " dir) - else Stm.get_current_state (), `NewTip in - Stm.set_compilation_hints file; - initial_id - end - -(* Retrocompatibility stuff *) -let interp ((_raw, verbose), s) = - let vernac_parse s = - let pa = Pcoq.Gram.parsable (Stream.of_string s) in - Flags.with_option Flags.we_are_parsing (fun () -> - match Pcoq.Gram.entry_parse Pcoq.main_entry pa with - | None -> raise (Invalid_argument "vernac_parse") - | Some ast -> ast) - () in - Stm.interp verbose (vernac_parse s); - Stm.get_current_state (), CSig.Inl (read_stdout ()) - -(** 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 - -(** Grouping all call handlers together + error handling *) - -let eval_call xml_oc log c = - let interruptible f x = - catch_break := true; - Control.check_for_interrupt (); - let r = f x in - catch_break := false; - let out = read_stdout () in - if not (String.is_empty out) then log (str out); - 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.interp = interruptible interp; - Interface.handle_exn = handle_exn; - Interface.stop_worker = Stm.stop_worker; - } in - Serialize.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 = Errors.push e in Mutex.unlock m; raise e - - -let slave_logger xml_oc level message = - (* convert the message into XML *) - let msg = string_of_ppcmds (hov 0 message) in - let message = { - Interface.message_level = level; - Interface.message_content = msg; - } in - let () = pr_debug (Printf.sprintf "-> %S" msg) in - let xml = Serialize.of_message message in - print_xml xml_oc xml - -let slave_feeder xml_oc msg = - let xml = Serialize.of_feedback 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 loop () = - 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 - CThread.prepare_in_channel_for_thread_friendly_io in_ch; - let in_lb = Lexing.from_function (fun s len -> - CThread.thread_friendly_read in_ch s ~off:0 ~len) in - let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in - let () = Xml_parser.check_eof xml_ic false in - set_logger (slave_logger xml_oc); - set_feeder (slave_feeder xml_oc); - (* We'll handle goal fetching and display in our own way *) - Vernacentries.enable_goal_printing := false; - Vernacentries.qed_display_script := false; - Flags.make_term_color false; - 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 q = Serialize.to_call xml_query in - let () = pr_debug_call q in - let r = eval_call xml_oc (slave_logger xml_oc Interface.Notice) q in - let () = pr_debug_answer q r in -(* pr_with_pid (Xml_printer.to_string_fmt (Serialize.of_answer q r)); *) - print_xml xml_oc (Serialize.of_answer 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_debug ("Syntax error in query: " ^ Xml_parser.error_msg err); - exit 1 - | Serialize.Marshal_error -> - pr_debug "Incorrect query."; - exit 1 - | any -> - pr_debug ("Fatal exception in coqtop:\n" ^ Printexc.to_string any); - exit 1 - done; - pr_debug "Exiting gracefully."; - exit 0 diff --git a/toplevel/ide_slave.mli b/toplevel/ide_slave.mli deleted file mode 100644 index fb927cf33f..0000000000 --- a/toplevel/ide_slave.mli +++ /dev/null @@ -1,17 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit - -val loop : unit -> unit diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 11f00d6e54..695fd3b82e 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -211,7 +211,8 @@ let file_of_name name = let suffix = get_ml_object_suffix name in let fail s = errorlabstrm "Mltop.load_object" - (str"File not found on loadpath : " ++ str s) in + (str"File not found on loadpath : " ++ str s ++ str"\n" ++ + str"Loadpath: " ++ str(String.concat ":" !coq_mlpath_copy)) in if is_native then let name = match suffix with | Some ((".cmo"|".cma") as suffix) -> @@ -290,6 +291,8 @@ let load_ml_object mname fname= add_known_module mname; init_ml_object mname +let load_ml_object_raw fname = dir_ml_load (file_of_name fname) + (* Summary of declared ML Modules *) (* List and not String.Set because order is important: most recent first. *) diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index 196c0bf94b..a4ba732d26 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -54,6 +54,7 @@ val add_rec_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool val add_known_module : string -> unit val module_is_known : string -> bool val load_ml_object : string -> string -> unit +val load_ml_object_raw : string -> unit (** {5 Initialization functions} *) diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index a5519d5860..d22524e5ca 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -15,7 +15,6 @@ Mltop Vernacentries Whelp Vernac -Ide_slave Usage Coqloop Coqinit -- cgit v1.2.3