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. --- Makefile.ide | 50 ++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 36 insertions(+), 14 deletions(-) (limited to 'Makefile.ide') diff --git a/Makefile.ide b/Makefile.ide index ac4ba75d4..eca0f20d4 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -45,7 +45,9 @@ COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES) IDEDEPS:=clib/clib.cma lib/lib.cma IDECMA:=ide/ide.cma -IDETOPLOOPCMA=ide/coqidetop.cma +IDETOPEXE=bin/coqidetop$(EXE) +IDETOP=bin/coqidetop.opt$(EXE) +IDETOPBYTE=bin/coqidetop.byte$(EXE) LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.mli ide/coqide_main.ml LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.mli ide/coqide_main.ml @@ -88,15 +90,15 @@ endif coqide-files: $(IDEFILES) -ide-byteloop: $(IDETOPLOOPCMA) -ide-optloop: $(IDETOPLOOPCMA:.cma=.cmxs) -ide-toploop: ide-$(BEST)loop +ide-byteloop: $(IDETOPBYTE) +ide-optloop: $(IDETOP) +ide-toploop: $(IDETOPEXE) ifeq ($(HASCOQIDE),opt) $(COQIDE): $(LINKIDEOPT) $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa \ - lablgtksourceview2.cmxa str.cmxa $(IDEFLAGS:.cma=.cmxa) $^ + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \ + -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS:.cma=.cmxa) $^ $(STRIP) $@ else $(COQIDE): $(COQIDEBYTE) @@ -105,8 +107,8 @@ endif $(COQIDEBYTE): $(LINKIDE) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma \ - lablgtksourceview2.cma str.cma $(IDEFLAGS) $(IDECDEPSFLAGS) $^ + $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ \ + -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS) $(IDECDEPSFLAGS) $^ ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp5deps here $(SHOW)'CAMLP5O $<' @@ -135,6 +137,29 @@ ide/ideutils.cmx: ide/ideutils.ml $(SHOW)'OCAMLOPT $<' $(HIDE)$(filter-out -safe-string,$(OCAMLOPT)) $(COQIDEFLAGS) $(filter-out -safe-string,$(OPTFLAGS)) -c $< +IDETOPCMA:=ide/ide_common.cma +IDETOPCMX:=$(IDETOPCMA:.cma=.cmxa) + +# Special rule for coqidetop +$(IDETOPEXE): $(IDETOP:.opt=.$(BEST)) + cp $< $@ + +$(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX) + $(SHOW)'COQMKTOP -o $@' + $(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide \ + -I kernel/byterun/ -cclib -lcoqrun \ + $(SYSMOD) -package camlp5.gramlib \ + $(LINKCMX) $(IDETOPCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@ + $(STRIP) $@ + $(CODESIGN) $@ + +$(IDETOPBYTE): ide/idetop.ml $(LINKCMO) $(LIBCOQRUN) $(IDETOPCMA) + $(SHOW)'COQMKTOP -o $@' + $(HIDE)$(OCAMLC) -linkall -linkpkg $(MLINCLUDES) -I ide \ + -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \ + $(SYSMOD) -package camlp5.gramlib \ + $(LINKCMO) $(IDETOPCMA) $(BYTEFLAGS) $< -o $@ + #################### ## Install targets #################### @@ -164,13 +189,11 @@ install-ide-bin: install-ide-toploop: ifeq ($(BEST),opt) - $(MKDIR) $(FULLCOQLIB)/toploop/ - $(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ + $(INSTALLBIN) $(IDETOPEXE) $(IDETOP) $(FULLBINDIR) endif install-ide-toploop-byte: ifneq ($(BEST),opt) - $(MKDIR) $(FULLCOQLIB)/toploop/ - $(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/ + $(INSTALLBIN) $(IDETOPEXE) $(IDETOPBYTE) $(FULLBINDIR) endif install-ide-devfiles: @@ -206,8 +229,7 @@ $(COQIDEAPP)/Contents: $(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \ - unix.cmxa lablgtk.cmxa lablgtksourceview2.cmxa str.cmxa \ - threads.cmxa $(IDEFLAGS:.cma=.cmxa) $^ + -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS:.cma=.cmxa) $^ $(STRIP) $@ $(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents -- cgit v1.2.3 From db1719fbac08b5582fafddd4b76ef92f69cc5bc1 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 28 Feb 2018 03:26:12 +0100 Subject: [ide] Remove special option `-ideslave` This has no effect anymore, verbose printing is controlled now by the regular, common `quiet` flag. --- Makefile.build | 2 +- Makefile.ide | 2 +- ide/coq.ml | 4 ++-- ide/idetop.ml | 7 +++---- lib/flags.ml | 2 -- lib/flags.mli | 3 --- lib/stateid.ml | 10 +++------- stm/asyncTaskQueue.ml | 2 +- tools/fake_ide.ml | 6 +++--- toplevel/coqargs.ml | 1 - vernac/vernacentries.ml | 2 +- 11 files changed, 15 insertions(+), 26 deletions(-) (limited to 'Makefile.ide') diff --git a/Makefile.build b/Makefile.build index b19841a37..5f5eaf3a4 100644 --- a/Makefile.build +++ b/Makefile.build @@ -504,7 +504,7 @@ $(COQWORKMGR): $(call bestobj, clib/clib.cma lib/lib.cma stm/spawned.cmo stm/coq $(HIDE)$(call bestocaml, $(SYSMOD)) # fake_ide : for debugging or test-suite purpose, a fake ide simulating -# a connection to coqtop -ideslave +# a connection to coqidetop FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/document.cmo \ ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo \ diff --git a/Makefile.ide b/Makefile.ide index eca0f20d4..37f698e0c 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -36,7 +36,7 @@ COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide # Note : for just building bin/coqide, we could only consider # config, lib, ide and ide/utils. But the coqidetop plugin (the -# one that will be loaded by coqtop -ideslave) refers to some +# one that will be loaded by coqidetop) refers to some # core modules of coq, for instance printing/*. IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils diff --git a/ide/coq.ml b/ide/coq.ml index 65456d685..63986935a 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -152,7 +152,7 @@ let print_status = function 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 -ideslave " ^ argstr in + let cmd = Filename.quote (coqtop_path ()) ^ " -batch " ^ argstr in let cmd = requote cmd in try let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in @@ -377,7 +377,7 @@ let spawn_handle args respawner feedback_processor = else "on" in - let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: "-ideslave" :: args) in + let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: args) in let env = match !ideslave_coqtop_flags with | None -> None diff --git a/ide/idetop.ml b/ide/idetop.ml index e40af003b..64f165cde 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -18,9 +18,8 @@ open Printer module NamedDecl = Context.Named.Declaration module CompactedDecl = Context.Compacted.Declaration -(** Ide_slave : an implementation of [Interface], i.e. mainly an interp - function and a rewind function. This specialized loop is triggered - when the -ideslave option is passed to Coqtop. *) +(** Idetop : an implementation of [Interface], i.e. mainly an interp + function and a rewind function. *) (** Signal handling: we postpone ^C during input and output phases, @@ -429,7 +428,7 @@ let eval_call c = Xmlprotocol.abstract_eval_call handler c (** Message dispatching. - Since coqtop -ideslave starts 1 thread per slave, and each + Since [coqidetop] 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. *) diff --git a/lib/flags.ml b/lib/flags.ml index 56940f1cf..7e0065beb 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -57,8 +57,6 @@ let in_toplevel = ref false let profile = false -let ide_slave = ref false - let raw_print = ref false let we_are_parsing = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 17776d68a..02d8a3adc 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -52,9 +52,6 @@ val in_toplevel : bool ref val profile : bool -(* -ide_slave: printing will be more verbose, will affect stm caching *) -val ide_slave : bool ref - (* development flag to detect race conditions, it should go away. *) val we_are_parsing : bool ref diff --git a/lib/stateid.ml b/lib/stateid.ml index a258d5052..5485c4bf1 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -11,15 +11,11 @@ type t = int let initial = 1 let dummy = 0 -let fresh, in_range = +let fresh = let cur = ref initial in - (fun () -> incr cur; !cur), (fun id -> id >= 0 && id <= !cur) + fun () -> incr cur; !cur let to_string = string_of_int -let of_int id = - (* Coqide too to parse ids too, but cannot check if they are valid. - * Hence we check for validity only if we are an ide slave. *) - if !Flags.ide_slave then assert (in_range id); - id +let of_int id = id let to_int id = id let newer_than id1 id2 = id1 > id2 diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 0105f821e..85a7f1495 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -123,7 +123,7 @@ module Make(T : Task) () = struct ["-worker-id"; name; "-async-proofs-worker-priority"; CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)] - | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl + | ("-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl | ("-async-proofs" |"-vio2vo" |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv" |"-compile" |"-compile-verbose" diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 47bd2493f..016201128 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** Fake_ide : Simulate a [coqide] talking to a [coqtop -ideslave] *) +(** Fake_ide : Simulate a [coqide] talking to a [coqidetop] *) let error s = prerr_endline ("fake_id: error: "^s); @@ -284,7 +284,7 @@ let read_command inc = Parser.parse grammar inc let usage () = error (Printf.sprintf - "A fake coqide process talking to a coqtop -ideslave.\n\ + "A fake coqide process talking to a coqtop -toploop coqidetop.\n\ Usage: %s (file|-) []\n\ Input syntax is the following:\n%s\n" (Filename.basename Sys.argv.(0)) @@ -296,7 +296,7 @@ let main = if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe (Sys.Signal_handle (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1)); - let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in + let def_args = ["--xml_format=Ppcmds"] in let idetop_name = System.get_toplevel_path "coqidetop" in let coqtop_args, input_file = match Sys.argv with | [| _; f |] -> Array.of_list def_args, f diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 5c1ffd784..89602c9b5 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -529,7 +529,6 @@ let parse_args arglist : coq_cmdopts * string list = |"-stm-debug" -> Stm.stm_debug := true; oval |"-emacs" -> set_emacs oval |"-filteropts" -> { oval with filter_opts = true } - |"-ideslave" -> Flags.ide_slave := true; oval |"-impredicative-set" -> { oval with impredicative_set = Declarations.ImpredicativeSet } |"-indices-matter" -> Indtypes.enforce_indices_matter (); oval diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f0e41d27c..938e9718a 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2243,7 +2243,7 @@ let with_fail st b f = | HasNotFailed -> user_err ~hdr:"Fail" (str "The command has not failed!") | HasFailed msg -> - if not !Flags.quiet || !Flags.test_mode || !Flags.ide_slave then Feedback.msg_info + if not !Flags.quiet || !Flags.test_mode then Feedback.msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg) | _ -> assert false end -- cgit v1.2.3