diff options
| -rw-r--r-- | .merlin | 2 | ||||
| -rw-r--r-- | CHANGES | 12 | ||||
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | Makefile.build | 39 | ||||
| -rw-r--r-- | Makefile.common | 7 | ||||
| -rw-r--r-- | Makefile.ide | 50 | ||||
| -rw-r--r-- | Makefile.install | 10 | ||||
| -rw-r--r-- | configure.ml | 5 | ||||
| -rw-r--r-- | dev/base_include | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-pidetop.sh | 15 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06859-ejgallego-stm+top.sh | 6 | ||||
| -rw-r--r-- | ide/ide_common.mllib (renamed from ide/coqidetop.mllib) | 1 | ||||
| -rw-r--r-- | ide/idetop.ml (renamed from ide/ide_slave.ml) | 19 | ||||
| -rw-r--r-- | ide/ideutils.ml | 18 | ||||
| -rw-r--r-- | lib/system.ml | 18 | ||||
| -rw-r--r-- | lib/system.mli | 20 | ||||
| -rw-r--r-- | stm/asyncTaskQueue.ml | 10 | ||||
| -rw-r--r-- | stm/coqworkmgrApi.ml | 4 | ||||
| -rw-r--r-- | stm/coqworkmgrApi.mli | 3 | ||||
| -rw-r--r-- | stm/proofworkertop.mllib | 1 | ||||
| -rw-r--r-- | stm/queryworkertop.mllib | 1 | ||||
| -rw-r--r-- | stm/stm.ml | 2 | ||||
| -rw-r--r-- | stm/stm.mllib | 1 | ||||
| -rw-r--r-- | stm/tacworkertop.mllib | 1 | ||||
| -rw-r--r-- | tools/fake_ide.ml | 16 | ||||
| -rw-r--r-- | topbin/coqproofworker_bin.ml (renamed from stm/proofworkertop.ml) | 6 | ||||
| -rw-r--r-- | topbin/coqqueryworker_bin.ml (renamed from stm/queryworkertop.ml) | 5 | ||||
| -rw-r--r-- | topbin/coqtacticworker_bin.ml (renamed from stm/tacworkertop.ml) | 5 | ||||
| -rw-r--r-- | topbin/coqtop_bin.ml (renamed from toplevel/coqtop_opt_bin.ml) | 2 | ||||
| -rw-r--r-- | topbin/coqtop_byte_bin.ml (renamed from toplevel/coqtop_byte_bin.ml) | 2 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 34 | ||||
| -rw-r--r-- | toplevel/coqargs.mli | 3 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 8 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 22 | ||||
| -rw-r--r-- | toplevel/coqloop.mli | 10 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 48 | ||||
| -rw-r--r-- | toplevel/coqtop.mli | 25 | ||||
| -rw-r--r-- | toplevel/toplevel.mllib | 5 | ||||
| -rw-r--r-- | toplevel/workerLoop.ml (renamed from stm/workerLoop.ml) | 20 | ||||
| -rw-r--r-- | toplevel/workerLoop.mli (renamed from ide/ide_slave.mli) | 6 | ||||
| -rw-r--r-- | vernac/mltop.ml | 9 | ||||
| -rw-r--r-- | vernac/mltop.mli | 3 |
42 files changed, 256 insertions, 224 deletions
@@ -32,6 +32,8 @@ S vernac B vernac S toplevel B toplevel +S topbin +B topbin S plugins/ltac B plugins/ltac S API @@ -36,6 +36,18 @@ Tactic language called by OCaml-defined tactics. - Option "Ltac Debug" now applies also to terms built using Ltac functions. +Coq binaries and process model + +- Before 8.9, Coq distributed a single `coqtop` binary and a set of + dynamically loadable plugins that used to take over the main loop + for tasks such as IDE language server or parallel proof checking. + + These plugins have been turned into full-fledged binaries so each + different process has associated a particular binary now, in + particular `coqidetop` is the CoqIDE language server, and + `coq{proof,tactic,query}worker` are in charge of task-specific and + parallel proof checking. + Changes from 8.8.0 to 8.8.1 =========================== @@ -214,7 +214,7 @@ cruftclean: ml4clean indepclean: rm -f $(GENFILES) - rm -f $(COQTOPBYTE) $(CHICKENBYTE) + rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(TOPBYTE) find . \( -name '*~' -o -name '*.cm[ioat]' -o -name '*.cmti' \) -delete rm -f */*.pp[iox] plugins/*/*.pp[iox] rm -rf $(SOURCEDOCDIR) @@ -245,7 +245,7 @@ archclean: clean-ide optclean voclean rm -f $(ALLSTDLIB).* optclean: - rm -f $(COQTOPEXE) $(CHICKEN) + rm -f $(COQTOPEXE) $(CHICKEN) $(TOPBIN) rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT) find . -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f diff --git a/Makefile.build b/Makefile.build index 179ca28b6c..b19841a378 100644 --- a/Makefile.build +++ b/Makefile.build @@ -383,29 +383,34 @@ grammar/%.cmi: grammar/%.mli .PHONY: coqbinaries coqbyte -coqbinaries: $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) +coqbinaries: $(TOPBIN) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) +coqbyte: $(TOPBYTE) $(CHICKENBYTE) -coqbyte: $(COQTOPBYTE) $(CHICKENBYTE) - -COQTOP_OPT=toplevel/coqtop_opt_bin.ml -COQTOP_BYTE=toplevel/coqtop_byte_bin.ml +# Special rule for coqtop +$(COQTOPEXE): $(TOPBIN:.opt=.$(BEST)) + cp $< $@ -ifeq ($(BEST),opt) -$(COQTOPEXE): $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT) +bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(OCAMLOPT) -linkall -linkpkg -I vernac -I toplevel \ + $(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) \ -I kernel/byterun/ -cclib -lcoqrun \ $(SYSMOD) -package camlp5.gramlib \ - $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) $(COQTOP_OPT) -o $@ + $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@ $(STRIP) $@ $(CODESIGN) $@ -else -$(COQTOPEXE): $(COQTOPBYTE) - cp $< $@ -endif +bin/%.byte$(EXE): topbin/%_bin.ml $(LINKCMO) $(LIBCOQRUN) + $(SHOW)'COQMKTOP -o $@' + $(HIDE)$(OCAMLC) -linkall -linkpkg $(MLINCLUDES) \ + -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \ + $(SYSMOD) -package camlp5.gramlib \ + $(LINKCMO) $(BYTEFLAGS) $< -o $@ + +COQTOP_BYTE=topbin/coqtop_byte_bin.ml + +# Special rule for coqtop.byte # VMBYTEFLAGS will either contain -custom of the right -dllpath for the VM -$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE) +$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(COQTOP_BYTE) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(OCAMLC) -linkall -linkpkg -I lib -I vernac -I toplevel \ -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \ @@ -477,7 +482,7 @@ COQMAKEFILECMO:=clib/clib.cma lib/lib.cma tools/coq_makefile.cmo $(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, -package str,unix,threads) + $(HIDE)$(call bestocaml, -package str) $(COQTEX): $(call bestobj, tools/coq_tex.cmo) $(SHOW)'OCAMLBEST -o $@' @@ -506,9 +511,9 @@ FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/document.cmo \ ide/xml_printer.cmo ide/richpp.cmo ide/xmlprotocol.cmo \ tools/fake_ide.cmo -$(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN)) +$(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOP) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, -I ide -package str,unix,threads) + $(HIDE)$(call bestocaml, -I ide -package str -package dynlink) # votour: a small vo explorer (based on the checker) diff --git a/Makefile.common b/Makefile.common index 9493acd1fc..372c314755 100644 --- a/Makefile.common +++ b/Makefile.common @@ -14,8 +14,11 @@ # Executables ########################################################################### -COQTOPBYTE:=bin/coqtop.byte$(EXE) +TOPBIN:=$(addsuffix .opt$(EXE), $(addprefix bin/, coqtop coqproofworker coqtacticworker coqqueryworker)) +TOPBYTE:=$(TOPBIN:.opt$(EXE)=.byte$(EXE)) + COQTOPEXE:=bin/coqtop$(EXE) +COQTOPBYTE:=bin/coqtop.byte$(EXE) COQDEP:=bin/coqdep$(EXE) COQMAKEFILE:=bin/coq_makefile$(EXE) @@ -107,8 +110,6 @@ CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \ stm/stm.cma toplevel/toplevel.cma -TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma - GRAMMARCMA:=grammar/grammar.cma ########################################################################### diff --git a/Makefile.ide b/Makefile.ide index ac4ba75d4d..eca0f20d43 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 diff --git a/Makefile.install b/Makefile.install index 02695287b9..0764b61fc7 100644 --- a/Makefile.install +++ b/Makefile.install @@ -70,17 +70,11 @@ endif install-binaries: install-tools $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQC) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR) - $(MKDIR) $(FULLCOQLIB)/toploop -ifeq ($(BEST),opt) - $(INSTALLBIN) $(TOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ -endif + $(INSTALLBIN) $(COQC) $(CHICKEN) $(COQTOPEXE) $(TOPBIN) $(FULLBINDIR) install-byte: install-coqide-byte $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQTOPBYTE) $(FULLBINDIR) - $(MKDIR) $(FULLCOQLIB)/toploop - $(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/ + $(INSTALLBIN) $(TOPBYTE) $(FULLBINDIR) $(INSTALLSH) $(FULLCOQLIB) $(LINKCMO) $(PLUGINS) ifndef CUSTOM $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) diff --git a/configure.ml b/configure.ml index d4750700b5..45c3bb67a4 100644 --- a/configure.ml +++ b/configure.ml @@ -16,8 +16,9 @@ let coq_macos_version = "8.7.90" (** "[...] should be a string comprised of three non-negative, period-separated integers [...]" *) let vo_magic = 8791 let state_magic = 58791 -let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqworkmgr"; -"coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"] +let distributed_exec = + ["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt"; + "coqc";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"] let verbose = ref false (* for debugging this script *) diff --git a/dev/base_include b/dev/base_include index 2f7183dd63..2f5d8aa843 100644 --- a/dev/base_include +++ b/dev/base_include @@ -231,7 +231,7 @@ let _ = Flags.in_toplevel := true let _ = Constrextern.set_extern_reference (fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));; -let go () = Coqloop.loop ~state:Option.(get !Coqloop.drop_last_doc) +let go () = Coqloop.(loop ~opts:Option.(get !drop_args) ~state:Option.(get !drop_last_doc)) let _ = print_string diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh index d04b9637c0..2ac4d21671 100755 --- a/dev/ci/ci-pidetop.sh +++ b/dev/ci/ci-pidetop.sh @@ -8,6 +8,17 @@ pidetop_CI_DIR="${CI_BUILD_DIR}/pidetop" git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}" -( cd "${pidetop_CI_DIR}" && coq_makefile -f Make -o Makefile.top && make -f Makefile.top "-j${NJOBS}" && make install-toploop -f Makefile.top ) +# Travis / Gitlab have different filesystem layout due to use of +# `-local`. We need to improve this divergence but if we use Dune this +# "local" oddity goes away automatically so not bothering... +if [ -d "$COQBIN/../lib/coq" ]; then + COQOCAMLLIB="$COQBIN/../lib/" + COQLIB="$COQBIN/../lib/coq/" +else + COQOCAMLLIB="$COQBIN/../" + COQLIB="$COQBIN/../" +fi -echo -en '4\nexit' | coqtop -main-channel stdfds -toploop pidetop +( cd "${pidetop_CI_DIR}" && OCAMLPATH="$COQOCAMLLIB" jbuilder build @install ) + +echo -en '4\nexit' | "$pidetop_CI_DIR/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds diff --git a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh new file mode 100644 index 0000000000..ca0076b468 --- /dev/null +++ b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh @@ -0,0 +1,6 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top" ] || [ "$CI_BRANCH" = "pr-6859" ]; then + pidetop_CI_BRANCH=stm+top + pidetop_CI_GITURL=https://bitbucket.org/ejgallego/pidetop.git +fi diff --git a/ide/coqidetop.mllib b/ide/ide_common.mllib index df988d8f11..050c282ef6 100644 --- a/ide/coqidetop.mllib +++ b/ide/ide_common.mllib @@ -5,4 +5,3 @@ Serialize Richpp Xmlprotocol Document -Ide_slave diff --git a/ide/ide_slave.ml b/ide/idetop.ml index 6c7ca4f8e5..e40af003b7 100644 --- a/ide/ide_slave.ml +++ b/ide/idetop.ml @@ -457,7 +457,7 @@ let msg_format = ref (fun () -> (* The loop ignores the command line arguments as the current model delegates its handing to the toplevel container. *) -let loop _args ~state = +let loop ~opts:_ ~state = let open Vernac.State in set_doc state.doc; init_signal_handler (); @@ -506,13 +506,16 @@ let rec parse = function | 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" + +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 bdb39e94a1..e96b992999 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 diff --git a/lib/system.ml b/lib/system.ml index dfede29e8f..f109c71925 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -116,18 +116,6 @@ let where_in_path ?(warn=true) path filename = let f = Filename.concat lpe filename in if file_exists_respecting_case lpe filename then [lpe,f] else [])) -let where_in_path_rex path rex = - search path (fun lpe -> - try - let files = Sys.readdir lpe in - CList.map_filter (fun name -> - try - ignore(Str.search_forward rex name 0); - Some (lpe,Filename.concat lpe name) - with Not_found -> None) - (Array.to_list files) - with Sys_error _ -> []) - let find_file_in_path ?(warn=true) paths filename = if not (Filename.is_implicit filename) then (* the name is considered to be a physical name and we use the file @@ -312,3 +300,9 @@ let with_time ~batch f x = let msg2 = if batch then "" else " (failure)" in Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e + +let get_toplevel_path top = + let dir = Filename.dirname Sys.argv.(0) in + let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in + let eff = if Dynlink.is_native then ".opt" else ".byte" in + dir ^ Filename.dir_sep ^ top ^ eff ^ exe diff --git a/lib/system.mli b/lib/system.mli index 3349dfea30..a34280037c 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -50,8 +50,6 @@ val is_in_path : CUnix.load_path -> string -> bool val is_in_system_path : string -> bool val where_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string -val where_in_path_rex : - CUnix.load_path -> Str.regexp -> (CUnix.physical_path * string) list val find_file_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string @@ -107,3 +105,21 @@ val time_difference : time -> time -> float (** in seconds *) val fmt_time_difference : time -> time -> Pp.t val with_time : batch:bool -> ('a -> 'b) -> 'a -> 'b + +(** [get_toplevel_path program] builds a complete path to the + executable denoted by [program]. This involves: + + - locating the directory: we don't rely on PATH as to make calls to + /foo/bin/coqtop chose the right /foo/bin/coqproofworker + + - adding the proper suffixes: .opt/.byte depending on the current + mode, + .exe if in windows. + + Note that this function doesn't check that the executable actually + exists. This is left back to caller, as well as the choice of + fallback strategy. We could add a fallback strategy here but it is + better not to as in most cases if this function fails to construct + the right name you want you execution to fail rather than fall into + choosing some random binary from the system-wide installation of + Coq. *) +val get_toplevel_path : string -> string diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index b3e1500ae4..0105f821e1 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -120,12 +120,11 @@ module Make(T : Task) () = struct let proc, ic, oc = let rec set_slave_opt = function | [] -> !async_proofs_flags_for_workers @ - ["-toploop"; !T.name^"top"; - "-worker-id"; name; + ["-worker-id"; name; "-async-proofs-worker-priority"; - CoqworkmgrApi.(string_of_priority !WorkerLoop.async_proofs_worker_priority)] + CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)] | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl - | ("-async-proofs" |"-toploop" |"-vio2vo" + | ("-async-proofs" |"-vio2vo" |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv" |"-compile" |"-compile-verbose" |"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl -> @@ -134,7 +133,8 @@ module Make(T : Task) () = struct let args = Array.of_list (set_slave_opt (List.tl (Array.to_list Sys.argv))) in let env = Array.append (T.extra_env ()) (Unix.environment ()) in - Worker.spawn ~env Sys.argv.(0) args in + let worker_name = System.get_toplevel_path ("coq" ^ !T.name) in + Worker.spawn ~env worker_name args in name, proc, CThread.prepare_in_channel_for_thread_friendly_io ic, oc let manager cpanel (id, proc, ic, oc) = diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml index 36b5d18ab6..841cc08c07 100644 --- a/stm/coqworkmgrApi.ml +++ b/stm/coqworkmgrApi.ml @@ -11,6 +11,10 @@ let debug = false type priority = Low | High + +(* Default priority *) +let async_proofs_worker_priority = ref Low + let string_of_priority = function Low -> "low" | High -> "high" let priority_of_string = function | "low" -> Low diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli index 2983b619db..be5b291776 100644 --- a/stm/coqworkmgrApi.mli +++ b/stm/coqworkmgrApi.mli @@ -14,6 +14,9 @@ type priority = Low | High val string_of_priority : priority -> string val priority_of_string : string -> priority +(* Default priority *) +val async_proofs_worker_priority : priority ref + (* Connects to a work manager if any. If no worker manager, then -async-proofs-j and -async-proofs-tac-j are used *) val init : priority -> unit diff --git a/stm/proofworkertop.mllib b/stm/proofworkertop.mllib deleted file mode 100644 index f9f6c22d51..0000000000 --- a/stm/proofworkertop.mllib +++ /dev/null @@ -1 +0,0 @@ -Proofworkertop diff --git a/stm/queryworkertop.mllib b/stm/queryworkertop.mllib deleted file mode 100644 index c2f73089b3..0000000000 --- a/stm/queryworkertop.mllib +++ /dev/null @@ -1 +0,0 @@ -Queryworkertop diff --git a/stm/stm.ml b/stm/stm.ml index 20409c25ee..6b92e47378 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1849,7 +1849,7 @@ end = struct (* {{{ *) | RespError of Pp.t | RespNoProgress - let name = ref "tacworker" + let name = ref "tacticworker" let extra_env () = [||] type competence = unit type worker_status = Fresh | Old of competence diff --git a/stm/stm.mllib b/stm/stm.mllib index 72b5380162..4b254e8113 100644 --- a/stm/stm.mllib +++ b/stm/stm.mllib @@ -5,7 +5,6 @@ TQueue WorkerPool Vernac_classifier CoqworkmgrApi -WorkerLoop AsyncTaskQueue Stm ProofBlockDelimiter diff --git a/stm/tacworkertop.mllib b/stm/tacworkertop.mllib deleted file mode 100644 index db38fde279..0000000000 --- a/stm/tacworkertop.mllib +++ /dev/null @@ -1 +0,0 @@ -Tacworkertop diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index d48c6d0af5..47bd2493f2 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -297,19 +297,7 @@ let main = (Sys.Signal_handle (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1)); let def_args = ["--xml_format=Ppcmds"; "-ideslave"] in - let coqtop_name = (* from ide/ideutils.ml *) - let prog_name = "fake_ide" in - let len_prog_name = String.length prog_name in - let fake_ide_path = Sys.executable_name in - let fake_ide_path_len = String.length fake_ide_path in - let pos = fake_ide_path_len - len_prog_name in - let rex = Str.regexp_string prog_name in - try - let i = Str.search_backward rex fake_ide_path pos in - String.sub fake_ide_path 0 i ^ "coqtop" ^ - String.sub fake_ide_path (i + len_prog_name) - (fake_ide_path_len - i - len_prog_name) - with Not_found -> assert false 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 | [| _; f; ct |] -> @@ -318,7 +306,7 @@ let main = | _ -> usage () in let inc = if input_file = "-" then stdin else open_in input_file in let coq = - let _p, cin, cout = Coqide.spawn coqtop_name coqtop_args in + let _p, cin, cout = Coqide.spawn idetop_name coqtop_args in let ip = Xml_parser.make (Xml_parser.SChannel cin) in let op = Xml_printer.make (Xml_printer.TChannel cout) in Xml_parser.check_eof ip false; diff --git a/stm/proofworkertop.ml b/topbin/coqproofworker_bin.ml index 4b85a05ac7..7ae91cfbd3 100644 --- a/stm/proofworkertop.ml +++ b/topbin/coqproofworker_bin.ml @@ -10,7 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) () -let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout - -let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ()) - +let () = + WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop diff --git a/stm/queryworkertop.ml b/topbin/coqqueryworker_bin.ml index aa00102aab..98c8581213 100644 --- a/stm/queryworkertop.ml +++ b/topbin/coqqueryworker_bin.ml @@ -10,7 +10,4 @@ module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) () -let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout - -let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ()) - +let () = WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop diff --git a/stm/tacworkertop.ml b/topbin/coqtacticworker_bin.ml index 3b91df86e0..2634baa83f 100644 --- a/stm/tacworkertop.ml +++ b/topbin/coqtacticworker_bin.ml @@ -10,7 +10,4 @@ module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) () -let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout - -let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ()) - +let () = WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop diff --git a/toplevel/coqtop_opt_bin.ml b/topbin/coqtop_bin.ml index ea4c0ea520..4490db59e7 100644 --- a/toplevel/coqtop_opt_bin.ml +++ b/topbin/coqtop_bin.ml @@ -13,4 +13,4 @@ let drop_setup () = Mltop.remove () (* Main coqtop initialization *) let _ = drop_setup (); - Coqtop.start() + Coqtop.(start_coq coqtop_toplevel) diff --git a/toplevel/coqtop_byte_bin.ml b/topbin/coqtop_byte_bin.ml index 0b65cebbbc..abe397830f 100644 --- a/toplevel/coqtop_byte_bin.ml +++ b/topbin/coqtop_byte_bin.ml @@ -31,4 +31,4 @@ let drop_setup () = (* Main coqtop initialization *) let _ = drop_setup (); - Coqtop.start() + Coqtop.(start_coq coqtop_toplevel) diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 17e848c5af..5c1ffd7841 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -52,7 +52,6 @@ type coq_cmdopts = { compilation_mode : compilation_mode; toplevel_name : Names.DirPath.t; - toploop : string option; compile_list: (string * bool) list; (* bool is verbosity *) compilation_output_name : string option; @@ -81,6 +80,8 @@ type coq_cmdopts = { print_config: bool; output_context : bool; + print_emacs : bool; + inputstate : string option; outputstate : string option; @@ -100,7 +101,6 @@ let init_args = { compilation_mode = BuildVo; toplevel_name = Names.(DirPath.make [Id.of_string "Top"]); - toploop = None; compile_list = []; compilation_output_name = None; @@ -129,6 +129,8 @@ let init_args = { print_config = false; output_context = false; + print_emacs = false; + inputstate = None; outputstate = None; } @@ -191,11 +193,8 @@ let set_vio_checking_j opts opt j = (** Options for proof general *) let set_emacs opts = - if not (Option.is_empty opts.toploop) then - CErrors.user_err Pp.(str "Flag -emacs is incompatible with a custom toplevel loop"); - Coqloop.print_emacs := true; Printer.enable_goal_tags_printing := true; - { opts with color = `OFF } + { opts with color = `OFF; print_emacs = true } let set_color opts = function | "yes" | "on" -> { opts with color = `ON } @@ -310,12 +309,9 @@ let usage batch = let lp = Coqinit.toplevel_init_load_path () in (* Necessary for finding the toplevels below *) List.iter Mltop.add_coq_path lp; - if batch then Usage.print_usage_coqc () - else begin - Mltop.load_ml_objects_raw_rex - (Str.regexp (if Mltop.is_native then "^.*top.cmxs$" else "^.*top.cma$")); - Usage.print_usage_coqtop () - end + if batch + then Usage.print_usage_coqc () + else Usage.print_usage_coqtop () (* Main parsing routine *) let parse_args arglist : coq_cmdopts * string list = @@ -401,7 +397,7 @@ let parse_args arglist : coq_cmdopts * string list = }} |"-async-proofs-worker-priority" -> - WorkerLoop.async_proofs_worker_priority := get_priority opt (next ()); + CoqworkmgrApi.async_proofs_worker_priority := get_priority opt (next ()); oval |"-async-proofs-private-flags" -> @@ -500,11 +496,6 @@ let parse_args arglist : coq_cmdopts * string list = let oval = add_compile oval false (next ()) in { oval with compilation_mode = Vio2Vo } - |"-toploop" -> - if !Coqloop.print_emacs then - CErrors.user_err Pp.(str "Flags -toploop and -emacs are incompatible"); - { oval with toploop = Some (next ()) } - |"-w" | "-W" -> let w = next () in if w = "none" then @@ -538,12 +529,7 @@ 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" -> - if !Coqloop.print_emacs then - CErrors.user_err Pp.(str "Flags -ideslave and -emacs are incompatible"); - Flags.ide_slave := true; - { oval with toploop = Some "coqidetop" } - + |"-ideslave" -> Flags.ide_slave := true; oval |"-impredicative-set" -> { oval with impredicative_set = Declarations.ImpredicativeSet } |"-indices-matter" -> Indtypes.enforce_indices_matter (); oval diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index de9b6a6823..9fb6219a61 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -27,7 +27,6 @@ type coq_cmdopts = { compilation_mode : compilation_mode; toplevel_name : Names.DirPath.t; - toploop : string option; compile_list: (string * bool) list; (* bool is verbosity *) compilation_output_name : string option; @@ -56,6 +55,8 @@ type coq_cmdopts = { print_config: bool; output_context : bool; + print_emacs : bool; + inputstate : string option; outputstate : string option; diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 3e7a830856..e61f830f39 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -75,16 +75,12 @@ let ml_path_if c p = let f x = { recursive = false; path_spec = MlPath x } in if c then List.map f p else [] -(* LoadPath for toploop toplevels *) +(* LoadPath for developers *) let toplevel_init_load_path () = let coqlib = Envars.coqlib () in (* NOTE: These directories are searched from last to first *) (* first, developer specific directory to open *) - ml_path_if Coq_config.local [coqlib/"dev"] @ - - (* main loops *) - ml_path_if (Coq_config.local || !Flags.boot) [coqlib/"stm"; coqlib/"ide"] @ - ml_path_if (System.exists_dir (coqlib/"toploop")) [coqlib/"toploop"] + ml_path_if Coq_config.local [coqlib/"dev"] (* LoadPath for Coq user libraries *) let libs_init_load_path ~load_init = diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index da91695144..d7ede1c2ee 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -410,3 +410,25 @@ let rec loop ~state = str (Printexc.to_string any)) ++ spc () ++ hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".")); loop ~state + +(* Default toplevel loop *) +let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s)) + +let drop_args = ref None +let loop ~opts ~state = + drop_args := Some opts; + let open Coqargs in + print_emacs := opts.print_emacs; + (* We initialize the console only if we run the toploop_run *) + let tl_feed = Feedback.add_feeder (coqloop_feed Topfmt.InteractiveLoop) in + if Dumpglob.dump () then begin + Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; + Dumpglob.noglob () + end; + let _ = loop ~state in + (* Initialise and launch the Ocaml toplevel *) + Coqinit.init_ocaml_path(); + Mltop.ocaml_toploop(); + (* We delete the feeder after the OCaml toploop has ended so users + of Drop can see the feedback. *) + Feedback.del_feeder tl_feed diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 6d9867fb97..5c07a8bf3b 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -10,9 +10,6 @@ (** The Coq toplevel loop. *) -(** -emacs option: printing includes emacs tags. *) -val print_emacs : bool ref - (** A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) @@ -32,8 +29,9 @@ val set_prompt : (unit -> string) -> unit (** Toplevel feedback printer. *) val coqloop_feed : Topfmt.execution_phase -> Feedback.feedback -> unit -(** Main entry point of Coq: read and execute vernac commands. *) -val loop : state:Vernac.State.t -> Vernac.State.t - (** Last document seen after `Drop` *) val drop_last_doc : Vernac.State.t option ref +val drop_args : Coqargs.coq_cmdopts option ref + +(** Main entry point of Coq: read and execute vernac commands. *) +val loop : opts:Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 809490166c..e979d0e544 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -30,8 +30,6 @@ let print_header () = Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); flush_all () -let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s)) - (* Feedback received in the init stage, this is different as the STM will not be generally be initialized, thus stateid, etc... may be bogus. For now we just print to the console too *) @@ -41,23 +39,6 @@ let coqtop_doc_feed = Coqloop.coqloop_feed Topfmt.LoadingPrelude let coqtop_rcfile_feed = Coqloop.coqloop_feed Topfmt.LoadingRcFile -(* Default toplevel loop *) -let console_toploop_run opts ~state = - (* We initialize the console only if we run the toploop_run *) - let tl_feed = Feedback.add_feeder (Coqloop.coqloop_feed Topfmt.InteractiveLoop) in - if Dumpglob.dump () then begin - Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; - Dumpglob.noglob () - end; - let _ = Coqloop.loop ~state in - (* Initialise and launch the Ocaml toplevel *) - Coqinit.init_ocaml_path(); - Mltop.ocaml_toploop(); - (* We let the feeder in place for users of Drop *) - Feedback.del_feeder tl_feed - -let toploop_run = ref console_toploop_run - let memory_stat = ref false let print_memory_stat () = begin (* -m|--memory from the command-line *) @@ -387,12 +368,6 @@ let init_color color_mode = else Topfmt.init_terminal_output ~color:false -let toploop_init = ref begin fun opts x -> - let () = init_color opts.color in - let () = CoqworkmgrApi.init !WorkerLoop.async_proofs_worker_priority in - opts, x - end - let print_style_tags opts = let () = init_color opts.color in let tags = Topfmt.dump_tags () in @@ -435,7 +410,7 @@ let init_gc () = Gc.space_overhead = 120} (** Main init routine *) -let init_toplevel arglist = +let init_toplevel custom_init arglist = (* Coq's init process, phase 1: OCaml parameters, basic structures, and IO *) @@ -475,8 +450,7 @@ let init_toplevel arglist = end; let top_lp = Coqinit.toplevel_init_load_path () in List.iter Mltop.add_coq_path top_lp; - Option.iter Mltop.load_ml_object_raw opts.toploop; - let opts, extras = !toploop_init opts extras in + let opts, extras = custom_init ~opts extras in if not (CList.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"; @@ -540,11 +514,23 @@ let init_toplevel arglist = Feedback.del_feeder !init_feeder; res -let start () = - match init_toplevel (List.tl (Array.to_list Sys.argv)) with +type custom_toplevel = { + init : opts:coq_cmdopts -> string list -> coq_cmdopts * string list; + run : opts:coq_cmdopts -> state:Vernac.State.t -> unit; +} + +let coqtop_init ~opts extra = + init_color opts.color; + CoqworkmgrApi.(init !async_proofs_worker_priority); + opts, extra + +let coqtop_toplevel = { init = coqtop_init; run = Coqloop.loop; } + +let start_coq custom = + match init_toplevel custom.init (List.tl (Array.to_list Sys.argv)) with (* Batch mode *) | Some state, opts when not opts.batch_mode -> - !toploop_run opts ~state; + custom.run ~opts ~state; exit 1 | _ , opts -> flush_all(); diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index fcc569ca07..641448f10a 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -8,16 +8,21 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** The Coq main module. The following function [start] will parse the - command line, print the banner, initialize the load path, load the input - state, load the files given on the command line, load the resource file, - produce the output state if any, and finally will launch [Coqloop.loop]. *) +(** Definition of custom toplevels. + [init] is used to do custom command line argument parsing. + [run] launches a custom toplevel. +*) +type custom_toplevel = { + init : opts:Coqargs.coq_cmdopts -> string list -> Coqargs.coq_cmdopts * string list; + run : opts:Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit; +} -val init_toplevel : string list -> Vernac.State.t option * Coqargs.coq_cmdopts +val coqtop_toplevel : custom_toplevel -val start : unit -> unit +(** The Coq main module. [start custom] will parse the command line, + print the banner, initialize the load path, load the input state, + load the files given on the command line, load the resource file, + produce the output state if any, and finally will launch + [custom.run]. *) -(* For other toploops *) -val toploop_init : - (Coqargs.coq_cmdopts -> string list -> Coqargs.coq_cmdopts * string list) ref -val toploop_run : (Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit) ref +val start_coq : custom_toplevel -> unit diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index 78b96e5e27..597173e5f5 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -1,7 +1,8 @@ Vernac Usage -G_toplevel -Coqloop Coqinit Coqargs +G_toplevel +Coqloop Coqtop +WorkerLoop diff --git a/stm/workerLoop.ml b/toplevel/workerLoop.ml index 5130b019a9..ee6d5e8843 100644 --- a/stm/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -8,18 +8,22 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(* Default priority *) -open CoqworkmgrApi -let async_proofs_worker_priority = ref Low - let rec parse = function | "--xml_format=Ppcmds" :: rest -> parse rest | x :: rest -> x :: parse rest | [] -> [] -let loop init coq_args extra_args = - let args = parse extra_args in +let arg_init init ~opts extra_args = + let extra_args = parse extra_args in Flags.quiet := true; init (); - CoqworkmgrApi.init !async_proofs_worker_priority; - coq_args, args + CoqworkmgrApi.(init !async_proofs_worker_priority); + opts, extra_args + +let start ~init ~loop = + let open Coqtop in + let custom = { + init = arg_init init; + run = (fun ~opts:_ ~state:_ -> loop ()); + } in + start_coq custom diff --git a/ide/ide_slave.mli b/toplevel/workerLoop.mli index 9db9ecd12e..e497dee6d3 100644 --- a/ide/ide_slave.mli +++ b/toplevel/workerLoop.mli @@ -8,5 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(* This empty file avoids a race condition that occurs when compiling a .ml file - that does not have a corresponding .mli file *) +(* Register a STM worker *) +val start : + init:(unit -> unit) -> + loop:(unit -> unit) -> unit diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 343b0925d9..d25dea1413 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -345,13 +345,6 @@ let load_ml_object mname ?path fname= let dir_ml_load m = ignore(dir_ml_load m) let add_known_module m = add_known_module m None -let load_ml_object_raw fname = dir_ml_load (file_of_name fname) -let load_ml_objects_raw_rex rex = - List.iter (fun (_,fp) -> - let name = file_of_name (Filename.basename fp) in - try dir_ml_load name - with e -> prerr_endline (Printexc.to_string e)) - (System.where_in_path_rex !coq_mlpath_copy rex) (* Summary of declared ML Modules *) @@ -396,8 +389,6 @@ let trigger_ml_object verb cache reinit ?path name = if cache then perform_cache_obj name end -let load_ml_object n m = ignore(load_ml_object n m) - let unfreeze_ml_modules x = reset_loaded_modules (); List.iter diff --git a/vernac/mltop.mli b/vernac/mltop.mli index da195f4fce..ed1f9a12d8 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -68,9 +68,6 @@ val add_coq_path : coq_path -> unit (** List of modules linked to the toplevel *) 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 -val load_ml_objects_raw_rex : Str.regexp -> unit (** {5 Initialization functions} *) |