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. --- .merlin | 2 + CHANGES | 12 + Makefile | 4 +- Makefile.build | 39 +- Makefile.common | 7 +- Makefile.ide | 50 ++- Makefile.install | 10 +- configure.ml | 5 +- dev/base_include | 2 +- dev/ci/ci-pidetop.sh | 15 +- dev/ci/user-overlays/06859-ejgallego-stm+top.sh | 6 + ide/coqidetop.mllib | 8 - ide/ide_common.mllib | 7 + ide/ide_slave.ml | 518 ----------------------- ide/ide_slave.mli | 12 - ide/idetop.ml | 521 ++++++++++++++++++++++++ ide/ideutils.ml | 18 +- lib/system.ml | 18 +- lib/system.mli | 20 +- stm/asyncTaskQueue.ml | 10 +- stm/coqworkmgrApi.ml | 4 + stm/coqworkmgrApi.mli | 3 + stm/proofworkertop.ml | 16 - stm/proofworkertop.mllib | 1 - stm/queryworkertop.ml | 16 - stm/queryworkertop.mllib | 1 - stm/stm.ml | 2 +- stm/stm.mllib | 1 - stm/tacworkertop.ml | 16 - stm/tacworkertop.mllib | 1 - stm/workerLoop.ml | 25 -- tools/fake_ide.ml | 16 +- topbin/coqproofworker_bin.ml | 14 + topbin/coqqueryworker_bin.ml | 13 + topbin/coqtacticworker_bin.ml | 13 + topbin/coqtop_bin.ml | 16 + topbin/coqtop_byte_bin.ml | 34 ++ toplevel/coqargs.ml | 34 +- toplevel/coqargs.mli | 3 +- toplevel/coqinit.ml | 8 +- toplevel/coqloop.ml | 22 + toplevel/coqloop.mli | 10 +- toplevel/coqtop.ml | 48 +-- toplevel/coqtop.mli | 25 +- toplevel/coqtop_byte_bin.ml | 34 -- toplevel/coqtop_opt_bin.ml | 16 - toplevel/toplevel.mllib | 5 +- toplevel/workerLoop.ml | 29 ++ toplevel/workerLoop.mli | 14 + vernac/mltop.ml | 9 - vernac/mltop.mli | 3 - 51 files changed, 884 insertions(+), 852 deletions(-) create mode 100644 dev/ci/user-overlays/06859-ejgallego-stm+top.sh delete mode 100644 ide/coqidetop.mllib create mode 100644 ide/ide_common.mllib delete mode 100644 ide/ide_slave.ml delete mode 100644 ide/ide_slave.mli create mode 100644 ide/idetop.ml delete mode 100644 stm/proofworkertop.ml delete mode 100644 stm/proofworkertop.mllib delete mode 100644 stm/queryworkertop.ml delete mode 100644 stm/queryworkertop.mllib delete mode 100644 stm/tacworkertop.ml delete mode 100644 stm/tacworkertop.mllib delete mode 100644 stm/workerLoop.ml create mode 100644 topbin/coqproofworker_bin.ml create mode 100644 topbin/coqqueryworker_bin.ml create mode 100644 topbin/coqtacticworker_bin.ml create mode 100644 topbin/coqtop_bin.ml create mode 100644 topbin/coqtop_byte_bin.ml delete mode 100644 toplevel/coqtop_byte_bin.ml delete mode 100644 toplevel/coqtop_opt_bin.ml create mode 100644 toplevel/workerLoop.ml create mode 100644 toplevel/workerLoop.mli diff --git a/.merlin b/.merlin index 40db60950..404a7e793 100644 --- a/.merlin +++ b/.merlin @@ -32,6 +32,8 @@ S vernac B vernac S toplevel B toplevel +S topbin +B topbin S plugins/ltac B plugins/ltac S API diff --git a/CHANGES b/CHANGES index 3030e3311..aea7ec2f6 100644 --- a/CHANGES +++ b/CHANGES @@ -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 =========================== diff --git a/Makefile b/Makefile index f914de5a6..61b2f5cd9 100644 --- a/Makefile +++ b/Makefile @@ -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 179ca28b6..b19841a37 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 9493acd1f..372c31475 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 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 diff --git a/Makefile.install b/Makefile.install index 02695287b..0764b61fc 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 d4750700b..45c3bb67a 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 2f7183dd6..2f5d8aa84 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 d04b9637c..2ac4d2167 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 000000000..ca0076b46 --- /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/coqidetop.mllib deleted file mode 100644 index df988d8f1..000000000 --- a/ide/coqidetop.mllib +++ /dev/null @@ -1,8 +0,0 @@ -Xml_lexer -Xml_parser -Xml_printer -Serialize -Richpp -Xmlprotocol -Document -Ide_slave diff --git a/ide/ide_common.mllib b/ide/ide_common.mllib new file mode 100644 index 000000000..050c282ef --- /dev/null +++ b/ide/ide_common.mllib @@ -0,0 +1,7 @@ +Xml_lexer +Xml_parser +Xml_printer +Serialize +Richpp +Xmlprotocol +Document diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml deleted file mode 100644 index 6c7ca4f8e..000000000 --- a/ide/ide_slave.ml +++ /dev/null @@ -1,518 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* " ^ Xmlprotocol.pr_full_value q r) - -(** Categories of commands *) - -let coqide_known_option table = List.mem table [ - ["Printing";"Implicit"]; - ["Printing";"Coercions"]; - ["Printing";"Matching"]; - ["Printing";"Synth"]; - ["Printing";"Notations"]; - ["Printing";"All"]; - ["Printing";"Records"]; - ["Printing";"Existential";"Instances"]; - ["Printing";"Universes"]; - ["Printing";"Unfocused"]] - -let is_known_option cmd = match Vernacprop.under_control cmd with - | VernacSetOption (_, o, BoolValue true) - | VernacUnsetOption (_, o) -> coqide_known_option o - | _ -> false - -(** Check whether a command is forbidden in the IDE *) - -let ide_cmd_checks ~id {CAst.loc;v=ast} = - let user_error s = CErrors.user_err ?loc ~hdr:"IDE" (str s) in - let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in - if is_debug ast then - user_error "Debug mode not available in the IDE"; - if is_known_option ast then - warn "Set this option from the IDE menu instead"; - if is_navigation_vernac ast || is_undo ast then - warn "Use IDE navigation instead" - -(** Interpretation (cf. [Ide_intf.interp]) *) - -let ide_doc = ref None -let get_doc () = Option.get !ide_doc -let set_doc doc = ide_doc := Some doc - -let add ((s,eid),(sid,verbose)) = - let doc = get_doc () in - let pa = Pcoq.Gram.parsable (Stream.of_string s) in - let loc_ast = Stm.parse_sentence ~doc sid pa in - let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in - set_doc doc; - let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in - ide_cmd_checks ~id:newid loc_ast; - (* TODO: the "" parameter is a leftover of the times the protocol - * used to include stderr/stdout output. - * - * Currently, we force all the output meant for the to go via the - * feedback mechanism, and we don't manipulate stderr/stdout, which - * are left to the client's discrection. The parameter is still there - * as not to break the core protocol for this minor change, but it should - * be removed in the next version of the protocol. - *) - newid, (rc, "") - -let edit_at id = - let doc = get_doc () in - match Stm.edit_at ~doc id with - | doc, `NewTip -> set_doc doc; CSig.Inl () - | doc, `Focus { Stm.start; stop; tip} -> set_doc doc; CSig.Inr (start, (stop, tip)) - -(* TODO: the "" parameter is a leftover of the times the protocol - * used to include stderr/stdout output. - * - * Currently, we force all the output meant for the to go via the - * feedback mechanism, and we don't manipulate stderr/stdout, which - * are left to the client's discrection. The parameter is still there - * as not to break the core protocol for this minor change, but it should - * be removed in the next version of the protocol. - *) -let query (route, (s,id)) = - let pa = Pcoq.Gram.parsable (Stream.of_string s) in - let doc = get_doc () in - Stm.query ~at:id ~doc ~route pa - -let annotate phrase = - let doc = get_doc () in - let {CAst.loc;v=ast} = - let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in - Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa - in - (* XXX: Width should be a parameter of annotate... *) - Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast) - -(** Goal display *) - -let hyp_next_tac sigma env decl = - let id = NamedDecl.get_id decl in - let ast = NamedDecl.get_type decl in - let id_s = Names.Id.to_string id in - let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in - [ - ("clear "^id_s),("clear "^id_s^"."); - ("apply "^id_s),("apply "^id_s^"."); - ("exact "^id_s),("exact "^id_s^"."); - ("generalize "^id_s),("generalize "^id_s^"."); - ("absurd <"^id_s^">"),("absurd "^type_s^".") - ] @ [ - ("discriminate "^id_s),("discriminate "^id_s^"."); - ("injection "^id_s),("injection "^id_s^".") - ] @ [ - ("rewrite "^id_s),("rewrite "^id_s^"."); - ("rewrite <- "^id_s),("rewrite <- "^id_s^".") - ] @ [ - ("elim "^id_s), ("elim "^id_s^"."); - ("inversion "^id_s), ("inversion "^id_s^"."); - ("inversion clear "^id_s), ("inversion_clear "^id_s^".") - ] - -let concl_next_tac sigma concl = - let expand s = (s,s^".") in - List.map expand ([ - "intro"; - "intros"; - "intuition" - ] @ [ - "reflexivity"; - "discriminate"; - "symmetry" - ] @ [ - "assumption"; - "omega"; - "ring"; - "auto"; - "eauto"; - "tauto"; - "trivial"; - "decide equality"; - "simpl"; - "subst"; - "red"; - "split"; - "left"; - "right" - ]) - -let process_goal sigma g = - let env = Goal.V82.env sigma g in - let min_env = Environ.reset_context env in - let id = Goal.uid g in - let ccl = - pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) - in - let process_hyp d (env,l) = - let d' = CompactedDecl.to_named_context d in - (List.fold_right Environ.push_named d' env, - (pr_compacted_decl env sigma d) :: l) in - let (_env, hyps) = - Context.Compacted.fold process_hyp - (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in - { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } - -let export_pre_goals pgs = - { - Interface.fg_goals = pgs.Proof.fg_goals; - Interface.bg_goals = pgs.Proof.bg_goals; - Interface.shelved_goals = pgs.Proof.shelved_goals; - Interface.given_up_goals = pgs.Proof.given_up_goals - } - -let goals () = - let doc = get_doc () in - set_doc @@ Stm.finish ~doc; - try - let pfts = Proof_global.give_me_the_proof () in - Some (export_pre_goals (Proof.map_structured_proof pfts process_goal)) - with Proof_global.NoCurrentProof -> None - -let evars () = - try - let doc = get_doc () in - set_doc @@ Stm.finish ~doc; - let pfts = Proof_global.give_me_the_proof () in - let all_goals, _, _, _, sigma = Proof.proof pfts in - let exl = Evar.Map.bindings (Evd.undefined_map sigma) in - let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in - let el = List.map map_evar exl in - Some el - with Proof_global.NoCurrentProof -> None - -let hints () = - try - let pfts = Proof_global.give_me_the_proof () in - let all_goals, _, _, _, sigma = Proof.proof pfts in - match all_goals with - | [] -> None - | g :: _ -> - let env = Goal.V82.env sigma g in - let hint_goal = concl_next_tac sigma g in - let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in - let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in - Some (hint_hyps, hint_goal) - with Proof_global.NoCurrentProof -> None - - -(** Other API calls *) - -let wait () = - let doc = get_doc () in - set_doc (Stm.wait ~doc) - -let status force = - (** We remove the initial part of the current [DirPath.t] - (usually Top in an interactive session, cf "coqtop -top"), - and display the other parts (opened sections and modules) *) - set_doc (Stm.finish ~doc:(get_doc ())); - if force then - set_doc (Stm.join ~doc:(get_doc ())); - let path = - let l = Names.DirPath.repr (Lib.cwd ()) in - List.rev_map Names.Id.to_string l - in - let proof = - try Some (Names.Id.to_string (Proof_global.get_current_proof_name ())) - with Proof_global.NoCurrentProof -> None - in - let allproofs = - let l = Proof_global.get_all_proof_names () in - List.map Names.Id.to_string l - in - { - Interface.status_path = path; - Interface.status_proofname = proof; - Interface.status_allproofs = allproofs; - Interface.status_proofnum = Stm.current_proof_depth ~doc:(get_doc ()); - } - -let export_coq_object t = { - Interface.coq_object_prefix = t.Search.coq_object_prefix; - Interface.coq_object_qualid = t.Search.coq_object_qualid; - Interface.coq_object_object = Pp.string_of_ppcmds (pr_lconstr_env (Global.env ()) Evd.empty t.Search.coq_object_object) -} - -let pattern_of_string ?env s = - let env = - match env with - | None -> Global.env () - | Some e -> e - in - let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in - let (_, pat) = Constrintern.intern_constr_pattern env Evd.empty constr in - pat - -let dirpath_of_string_list s = - let path = String.concat "." s in - let m = Pcoq.parse_string Pcoq.Constr.global path in - let {CAst.v=qid} = Libnames.qualid_of_reference m in - let id = - try Nametab.full_name_module qid - with Not_found -> - CErrors.user_err ~hdr:"Search.interface_search" - (str "Module " ++ str path ++ str " not found.") - in - id - -let import_search_constraint = function - | Interface.Name_Pattern s -> Search.Name_Pattern (Str.regexp s) - | Interface.Type_Pattern s -> Search.Type_Pattern (pattern_of_string s) - | Interface.SubType_Pattern s -> Search.SubType_Pattern (pattern_of_string s) - | Interface.In_Module ms -> Search.In_Module (dirpath_of_string_list ms) - | Interface.Include_Blacklist -> Search.Include_Blacklist - -let search flags = - List.map export_coq_object (Search.interface_search ( - List.map (fun (c, b) -> (import_search_constraint c, b)) flags) - ) - -let export_option_value = function - | Goptions.BoolValue b -> Interface.BoolValue b - | Goptions.IntValue x -> Interface.IntValue x - | Goptions.StringValue s -> Interface.StringValue s - | Goptions.StringOptValue s -> Interface.StringOptValue s - -let import_option_value = function - | Interface.BoolValue b -> Goptions.BoolValue b - | Interface.IntValue x -> Goptions.IntValue x - | Interface.StringValue s -> Goptions.StringValue s - | Interface.StringOptValue s -> Goptions.StringOptValue s - -let export_option_state s = { - Interface.opt_sync = true; - Interface.opt_depr = s.Goptions.opt_depr; - Interface.opt_name = s.Goptions.opt_name; - Interface.opt_value = export_option_value s.Goptions.opt_value; -} - -let get_options () = - let table = Goptions.get_tables () in - let fold key state accu = (key, export_option_state state) :: accu in - Goptions.OptionMap.fold fold table [] - -let set_options options = - let iter (name, value) = match import_option_value value with - | BoolValue b -> Goptions.set_bool_option_value name b - | IntValue i -> Goptions.set_int_option_value name i - | StringValue s -> Goptions.set_string_option_value name s - | StringOptValue (Some s) -> Goptions.set_string_option_value name s - | StringOptValue None -> Goptions.unset_option_value_gen name - in - List.iter iter options - -let about () = { - Interface.coqtop_version = Coq_config.version; - Interface.protocol_version = Xmlprotocol.protocol_version; - Interface.release_date = Coq_config.date; - Interface.compile_date = Coq_config.compile_date; -} - -let handle_exn (e, info) = - let dummy = Stateid.dummy in - let loc_of e = match Loc.get_loc e with - | Some loc -> Some (Loc.unloc loc) - | _ -> None in - let mk_msg () = CErrors.print ~info e in - match e with - | e -> - match Stateid.get info with - | Some (valid, _) -> valid, loc_of info, mk_msg () - | None -> dummy, loc_of info, mk_msg () - -let init = - let initialized = ref false in - fun file -> - if !initialized then anomaly (str "Already initialized.") - else begin - let init_sid = Stm.get_current_state ~doc:(get_doc ()) in - initialized := true; - match file with - | None -> init_sid - | Some file -> - let doc, initial_id, _ = - get_doc (), init_sid, `NewTip in - if Filename.check_suffix file ".v" then - Stm.set_compilation_hints file; - set_doc (Stm.finish ~doc); - initial_id - end - -(* Retrocompatibility stuff, disabled since 8.7 *) -let interp ((_raw, verbose), s) = - Stateid.dummy, CSig.Inr "The interp call has been disabled, please use Add." - -(** When receiving the Quit call, we don't directly do an [exit 0], - but rather set this reference, in order to send a final answer - before exiting. *) - -let quit = ref false - -(** Disabled *) -let print_ast id = Xml_datatype.PCData "ERROR" - -(** Grouping all call handlers together + error handling *) - -let eval_call c = - let interruptible f x = - catch_break := true; - Control.check_for_interrupt (); - let r = f x in - catch_break := false; - r - in - let handler = { - Interface.add = interruptible add; - Interface.edit_at = interruptible edit_at; - Interface.query = interruptible query; - Interface.goals = interruptible goals; - Interface.evars = interruptible evars; - Interface.hints = interruptible hints; - Interface.status = interruptible status; - Interface.search = interruptible search; - Interface.get_options = interruptible get_options; - Interface.set_options = interruptible set_options; - Interface.mkcases = interruptible Vernacentries.make_cases; - Interface.quit = (fun () -> quit := true); - Interface.init = interruptible init; - Interface.about = interruptible about; - Interface.wait = interruptible wait; - Interface.interp = interruptible interp; - Interface.handle_exn = handle_exn; - Interface.stop_worker = Stm.stop_worker; - Interface.print_ast = print_ast; - Interface.annotate = interruptible annotate; - } in - Xmlprotocol.abstract_eval_call handler c - -(** Message dispatching. - Since coqtop -ideslave starts 1 thread per slave, and each - thread forwards feedback messages from the slave to the GUI on the same - xml channel, we need mutual exclusion. The mutex should be per-channel, but - here we only use 1 channel. *) -let print_xml = - let m = Mutex.create () in - fun oc xml -> - Mutex.lock m; - try Xml_printer.print oc xml; Mutex.unlock m - with e -> let e = CErrors.push e in Mutex.unlock m; iraise e - -let slave_feeder fmt xml_oc msg = - let xml = Xmlprotocol.(of_feedback fmt msg) in - print_xml xml_oc xml - -(** The main loop *) - -(** Exceptions during eval_call should be converted into [Interface.Fail] - messages by [handle_exn] above. Otherwise, we die badly, without - trying to answer malformed requests. *) - -let msg_format = ref (fun () -> - let margin = Option.default 72 (Topfmt.get_margin ()) in - Xmlprotocol.Richpp margin - ) - -(* The loop ignores the command line arguments as the current model delegates - its handing to the toplevel container. *) -let loop _args ~state = - let open Vernac.State in - set_doc state.doc; - init_signal_handler (); - catch_break := false; - let in_ch, out_ch = Spawned.get_channels () in - let xml_oc = Xml_printer.make (Xml_printer.TChannel out_ch) in - let in_lb = Lexing.from_function (fun s len -> - CThread.thread_friendly_read in_ch s ~off:0 ~len) in - (* SEXP parser make *) - let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in - let () = Xml_parser.check_eof xml_ic false in - ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc)); - while not !quit do - try - let xml_query = Xml_parser.parse xml_ic in -(* pr_with_pid (Xml_printer.to_string_fmt xml_query); *) - let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in - let () = pr_debug_call q in - let r = eval_call q in - let () = pr_debug_answer q r in -(* pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *) - print_xml xml_oc Xmlprotocol.(of_answer (!msg_format ()) q r); - flush out_ch - with - | Xml_parser.Error (Xml_parser.Empty, _) -> - pr_debug "End of input, exiting gracefully."; - exit 0 - | Xml_parser.Error (err, loc) -> - pr_error ("XML syntax error: " ^ Xml_parser.error_msg err) - | Serialize.Marshal_error (msg,node) -> - pr_error "Unexpected XML message"; - pr_error ("Expected XML node: " ^ msg); - pr_error ("XML tree received: " ^ Xml_printer.to_string_fmt node) - | any -> - pr_debug ("Fatal exception in coqtop:\n" ^ Printexc.to_string any); - exit 1 - done; - pr_debug "Exiting gracefully."; - exit 0 - -let rec parse = function - | "--help-XML-protocol" :: rest -> - Xmlprotocol.document Xml_printer.to_string_fmt; exit 0 - | "--xml_format=Ppcmds" :: rest -> - msg_format := (fun () -> Xmlprotocol.Ppcmds); parse rest - | x :: rest -> x :: parse rest - | [] -> [] - -let () = Coqtop.toploop_init := (fun coq_args extra_args -> - let args = parse extra_args in - CoqworkmgrApi.(init High); - coq_args, args) - -let () = Coqtop.toploop_run := loop - -let () = Usage.add_to_usage "coqidetop" -" --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\ -\n --help-XML-protocol print documentation of the Coq XML protocol\n" diff --git a/ide/ide_slave.mli b/ide/ide_slave.mli deleted file mode 100644 index 9db9ecd12..000000000 --- a/ide/ide_slave.mli +++ /dev/null @@ -1,12 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* " ^ Xmlprotocol.pr_full_value q r) + +(** Categories of commands *) + +let coqide_known_option table = List.mem table [ + ["Printing";"Implicit"]; + ["Printing";"Coercions"]; + ["Printing";"Matching"]; + ["Printing";"Synth"]; + ["Printing";"Notations"]; + ["Printing";"All"]; + ["Printing";"Records"]; + ["Printing";"Existential";"Instances"]; + ["Printing";"Universes"]; + ["Printing";"Unfocused"]] + +let is_known_option cmd = match Vernacprop.under_control cmd with + | VernacSetOption (_, o, BoolValue true) + | VernacUnsetOption (_, o) -> coqide_known_option o + | _ -> false + +(** Check whether a command is forbidden in the IDE *) + +let ide_cmd_checks ~id {CAst.loc;v=ast} = + let user_error s = CErrors.user_err ?loc ~hdr:"IDE" (str s) in + let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in + if is_debug ast then + user_error "Debug mode not available in the IDE"; + if is_known_option ast then + warn "Set this option from the IDE menu instead"; + if is_navigation_vernac ast || is_undo ast then + warn "Use IDE navigation instead" + +(** Interpretation (cf. [Ide_intf.interp]) *) + +let ide_doc = ref None +let get_doc () = Option.get !ide_doc +let set_doc doc = ide_doc := Some doc + +let add ((s,eid),(sid,verbose)) = + let doc = get_doc () in + let pa = Pcoq.Gram.parsable (Stream.of_string s) in + let loc_ast = Stm.parse_sentence ~doc sid pa in + let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in + set_doc doc; + let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in + ide_cmd_checks ~id:newid loc_ast; + (* TODO: the "" parameter is a leftover of the times the protocol + * used to include stderr/stdout output. + * + * Currently, we force all the output meant for the to go via the + * feedback mechanism, and we don't manipulate stderr/stdout, which + * are left to the client's discrection. The parameter is still there + * as not to break the core protocol for this minor change, but it should + * be removed in the next version of the protocol. + *) + newid, (rc, "") + +let edit_at id = + let doc = get_doc () in + match Stm.edit_at ~doc id with + | doc, `NewTip -> set_doc doc; CSig.Inl () + | doc, `Focus { Stm.start; stop; tip} -> set_doc doc; CSig.Inr (start, (stop, tip)) + +(* TODO: the "" parameter is a leftover of the times the protocol + * used to include stderr/stdout output. + * + * Currently, we force all the output meant for the to go via the + * feedback mechanism, and we don't manipulate stderr/stdout, which + * are left to the client's discrection. The parameter is still there + * as not to break the core protocol for this minor change, but it should + * be removed in the next version of the protocol. + *) +let query (route, (s,id)) = + let pa = Pcoq.Gram.parsable (Stream.of_string s) in + let doc = get_doc () in + Stm.query ~at:id ~doc ~route pa + +let annotate phrase = + let doc = get_doc () in + let {CAst.loc;v=ast} = + let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in + Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa + in + (* XXX: Width should be a parameter of annotate... *) + Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast) + +(** Goal display *) + +let hyp_next_tac sigma env decl = + let id = NamedDecl.get_id decl in + let ast = NamedDecl.get_type decl in + let id_s = Names.Id.to_string id in + let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in + [ + ("clear "^id_s),("clear "^id_s^"."); + ("apply "^id_s),("apply "^id_s^"."); + ("exact "^id_s),("exact "^id_s^"."); + ("generalize "^id_s),("generalize "^id_s^"."); + ("absurd <"^id_s^">"),("absurd "^type_s^".") + ] @ [ + ("discriminate "^id_s),("discriminate "^id_s^"."); + ("injection "^id_s),("injection "^id_s^".") + ] @ [ + ("rewrite "^id_s),("rewrite "^id_s^"."); + ("rewrite <- "^id_s),("rewrite <- "^id_s^".") + ] @ [ + ("elim "^id_s), ("elim "^id_s^"."); + ("inversion "^id_s), ("inversion "^id_s^"."); + ("inversion clear "^id_s), ("inversion_clear "^id_s^".") + ] + +let concl_next_tac sigma concl = + let expand s = (s,s^".") in + List.map expand ([ + "intro"; + "intros"; + "intuition" + ] @ [ + "reflexivity"; + "discriminate"; + "symmetry" + ] @ [ + "assumption"; + "omega"; + "ring"; + "auto"; + "eauto"; + "tauto"; + "trivial"; + "decide equality"; + "simpl"; + "subst"; + "red"; + "split"; + "left"; + "right" + ]) + +let process_goal sigma g = + let env = Goal.V82.env sigma g in + let min_env = Environ.reset_context env in + let id = Goal.uid g in + let ccl = + pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) + in + let process_hyp d (env,l) = + let d' = CompactedDecl.to_named_context d in + (List.fold_right Environ.push_named d' env, + (pr_compacted_decl env sigma d) :: l) in + let (_env, hyps) = + Context.Compacted.fold process_hyp + (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in + { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } + +let export_pre_goals pgs = + { + Interface.fg_goals = pgs.Proof.fg_goals; + Interface.bg_goals = pgs.Proof.bg_goals; + Interface.shelved_goals = pgs.Proof.shelved_goals; + Interface.given_up_goals = pgs.Proof.given_up_goals + } + +let goals () = + let doc = get_doc () in + set_doc @@ Stm.finish ~doc; + try + let pfts = Proof_global.give_me_the_proof () in + Some (export_pre_goals (Proof.map_structured_proof pfts process_goal)) + with Proof_global.NoCurrentProof -> None + +let evars () = + try + let doc = get_doc () in + set_doc @@ Stm.finish ~doc; + let pfts = Proof_global.give_me_the_proof () in + let all_goals, _, _, _, sigma = Proof.proof pfts in + let exl = Evar.Map.bindings (Evd.undefined_map sigma) in + let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in + let el = List.map map_evar exl in + Some el + with Proof_global.NoCurrentProof -> None + +let hints () = + try + let pfts = Proof_global.give_me_the_proof () in + let all_goals, _, _, _, sigma = Proof.proof pfts in + match all_goals with + | [] -> None + | g :: _ -> + let env = Goal.V82.env sigma g in + let hint_goal = concl_next_tac sigma g in + let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in + let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in + Some (hint_hyps, hint_goal) + with Proof_global.NoCurrentProof -> None + + +(** Other API calls *) + +let wait () = + let doc = get_doc () in + set_doc (Stm.wait ~doc) + +let status force = + (** We remove the initial part of the current [DirPath.t] + (usually Top in an interactive session, cf "coqtop -top"), + and display the other parts (opened sections and modules) *) + set_doc (Stm.finish ~doc:(get_doc ())); + if force then + set_doc (Stm.join ~doc:(get_doc ())); + let path = + let l = Names.DirPath.repr (Lib.cwd ()) in + List.rev_map Names.Id.to_string l + in + let proof = + try Some (Names.Id.to_string (Proof_global.get_current_proof_name ())) + with Proof_global.NoCurrentProof -> None + in + let allproofs = + let l = Proof_global.get_all_proof_names () in + List.map Names.Id.to_string l + in + { + Interface.status_path = path; + Interface.status_proofname = proof; + Interface.status_allproofs = allproofs; + Interface.status_proofnum = Stm.current_proof_depth ~doc:(get_doc ()); + } + +let export_coq_object t = { + Interface.coq_object_prefix = t.Search.coq_object_prefix; + Interface.coq_object_qualid = t.Search.coq_object_qualid; + Interface.coq_object_object = Pp.string_of_ppcmds (pr_lconstr_env (Global.env ()) Evd.empty t.Search.coq_object_object) +} + +let pattern_of_string ?env s = + let env = + match env with + | None -> Global.env () + | Some e -> e + in + let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in + let (_, pat) = Constrintern.intern_constr_pattern env Evd.empty constr in + pat + +let dirpath_of_string_list s = + let path = String.concat "." s in + let m = Pcoq.parse_string Pcoq.Constr.global path in + let {CAst.v=qid} = Libnames.qualid_of_reference m in + let id = + try Nametab.full_name_module qid + with Not_found -> + CErrors.user_err ~hdr:"Search.interface_search" + (str "Module " ++ str path ++ str " not found.") + in + id + +let import_search_constraint = function + | Interface.Name_Pattern s -> Search.Name_Pattern (Str.regexp s) + | Interface.Type_Pattern s -> Search.Type_Pattern (pattern_of_string s) + | Interface.SubType_Pattern s -> Search.SubType_Pattern (pattern_of_string s) + | Interface.In_Module ms -> Search.In_Module (dirpath_of_string_list ms) + | Interface.Include_Blacklist -> Search.Include_Blacklist + +let search flags = + List.map export_coq_object (Search.interface_search ( + List.map (fun (c, b) -> (import_search_constraint c, b)) flags) + ) + +let export_option_value = function + | Goptions.BoolValue b -> Interface.BoolValue b + | Goptions.IntValue x -> Interface.IntValue x + | Goptions.StringValue s -> Interface.StringValue s + | Goptions.StringOptValue s -> Interface.StringOptValue s + +let import_option_value = function + | Interface.BoolValue b -> Goptions.BoolValue b + | Interface.IntValue x -> Goptions.IntValue x + | Interface.StringValue s -> Goptions.StringValue s + | Interface.StringOptValue s -> Goptions.StringOptValue s + +let export_option_state s = { + Interface.opt_sync = true; + Interface.opt_depr = s.Goptions.opt_depr; + Interface.opt_name = s.Goptions.opt_name; + Interface.opt_value = export_option_value s.Goptions.opt_value; +} + +let get_options () = + let table = Goptions.get_tables () in + let fold key state accu = (key, export_option_state state) :: accu in + Goptions.OptionMap.fold fold table [] + +let set_options options = + let iter (name, value) = match import_option_value value with + | BoolValue b -> Goptions.set_bool_option_value name b + | IntValue i -> Goptions.set_int_option_value name i + | StringValue s -> Goptions.set_string_option_value name s + | StringOptValue (Some s) -> Goptions.set_string_option_value name s + | StringOptValue None -> Goptions.unset_option_value_gen name + in + List.iter iter options + +let about () = { + Interface.coqtop_version = Coq_config.version; + Interface.protocol_version = Xmlprotocol.protocol_version; + Interface.release_date = Coq_config.date; + Interface.compile_date = Coq_config.compile_date; +} + +let handle_exn (e, info) = + let dummy = Stateid.dummy in + let loc_of e = match Loc.get_loc e with + | Some loc -> Some (Loc.unloc loc) + | _ -> None in + let mk_msg () = CErrors.print ~info e in + match e with + | e -> + match Stateid.get info with + | Some (valid, _) -> valid, loc_of info, mk_msg () + | None -> dummy, loc_of info, mk_msg () + +let init = + let initialized = ref false in + fun file -> + if !initialized then anomaly (str "Already initialized.") + else begin + let init_sid = Stm.get_current_state ~doc:(get_doc ()) in + initialized := true; + match file with + | None -> init_sid + | Some file -> + let doc, initial_id, _ = + get_doc (), init_sid, `NewTip in + if Filename.check_suffix file ".v" then + Stm.set_compilation_hints file; + set_doc (Stm.finish ~doc); + initial_id + end + +(* Retrocompatibility stuff, disabled since 8.7 *) +let interp ((_raw, verbose), s) = + Stateid.dummy, CSig.Inr "The interp call has been disabled, please use Add." + +(** When receiving the Quit call, we don't directly do an [exit 0], + but rather set this reference, in order to send a final answer + before exiting. *) + +let quit = ref false + +(** Disabled *) +let print_ast id = Xml_datatype.PCData "ERROR" + +(** Grouping all call handlers together + error handling *) + +let eval_call c = + let interruptible f x = + catch_break := true; + Control.check_for_interrupt (); + let r = f x in + catch_break := false; + r + in + let handler = { + Interface.add = interruptible add; + Interface.edit_at = interruptible edit_at; + Interface.query = interruptible query; + Interface.goals = interruptible goals; + Interface.evars = interruptible evars; + Interface.hints = interruptible hints; + Interface.status = interruptible status; + Interface.search = interruptible search; + Interface.get_options = interruptible get_options; + Interface.set_options = interruptible set_options; + Interface.mkcases = interruptible Vernacentries.make_cases; + Interface.quit = (fun () -> quit := true); + Interface.init = interruptible init; + Interface.about = interruptible about; + Interface.wait = interruptible wait; + Interface.interp = interruptible interp; + Interface.handle_exn = handle_exn; + Interface.stop_worker = Stm.stop_worker; + Interface.print_ast = print_ast; + Interface.annotate = interruptible annotate; + } in + Xmlprotocol.abstract_eval_call handler c + +(** Message dispatching. + Since coqtop -ideslave starts 1 thread per slave, and each + thread forwards feedback messages from the slave to the GUI on the same + xml channel, we need mutual exclusion. The mutex should be per-channel, but + here we only use 1 channel. *) +let print_xml = + let m = Mutex.create () in + fun oc xml -> + Mutex.lock m; + try Xml_printer.print oc xml; Mutex.unlock m + with e -> let e = CErrors.push e in Mutex.unlock m; iraise e + +let slave_feeder fmt xml_oc msg = + let xml = Xmlprotocol.(of_feedback fmt msg) in + print_xml xml_oc xml + +(** The main loop *) + +(** Exceptions during eval_call should be converted into [Interface.Fail] + messages by [handle_exn] above. Otherwise, we die badly, without + trying to answer malformed requests. *) + +let msg_format = ref (fun () -> + let margin = Option.default 72 (Topfmt.get_margin ()) in + Xmlprotocol.Richpp margin + ) + +(* The loop ignores the command line arguments as the current model delegates + its handing to the toplevel container. *) +let loop ~opts:_ ~state = + let open Vernac.State in + set_doc state.doc; + init_signal_handler (); + catch_break := false; + let in_ch, out_ch = Spawned.get_channels () in + let xml_oc = Xml_printer.make (Xml_printer.TChannel out_ch) in + let in_lb = Lexing.from_function (fun s len -> + CThread.thread_friendly_read in_ch s ~off:0 ~len) in + (* SEXP parser make *) + let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in + let () = Xml_parser.check_eof xml_ic false in + ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc)); + while not !quit do + try + let xml_query = Xml_parser.parse xml_ic in +(* pr_with_pid (Xml_printer.to_string_fmt xml_query); *) + let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in + let () = pr_debug_call q in + let r = eval_call q in + let () = pr_debug_answer q r in +(* pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *) + print_xml xml_oc Xmlprotocol.(of_answer (!msg_format ()) q r); + flush out_ch + with + | Xml_parser.Error (Xml_parser.Empty, _) -> + pr_debug "End of input, exiting gracefully."; + exit 0 + | Xml_parser.Error (err, loc) -> + pr_error ("XML syntax error: " ^ Xml_parser.error_msg err) + | Serialize.Marshal_error (msg,node) -> + pr_error "Unexpected XML message"; + pr_error ("Expected XML node: " ^ msg); + pr_error ("XML tree received: " ^ Xml_printer.to_string_fmt node) + | any -> + pr_debug ("Fatal exception in coqtop:\n" ^ Printexc.to_string any); + exit 1 + done; + pr_debug "Exiting gracefully."; + exit 0 + +let rec parse = function + | "--help-XML-protocol" :: rest -> + Xmlprotocol.document Xml_printer.to_string_fmt; exit 0 + | "--xml_format=Ppcmds" :: rest -> + msg_format := (fun () -> Xmlprotocol.Ppcmds); parse rest + | x :: rest -> x :: parse rest + | [] -> [] + +let () = Usage.add_to_usage "coqidetop" +" --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\ +\n --help-XML-protocol print documentation of the Coq XML protocol\n" + +let islave_init ~opts extra_args = + let args = parse extra_args in + CoqworkmgrApi.(init High); + opts, args + +let () = + let open Coqtop in + let custom = { init = islave_init; run = loop; } in + start_coq custom diff --git a/ide/ideutils.ml b/ide/ideutils.ml index bdb39e94a..e96b99299 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -289,16 +289,10 @@ let coqtop_path () = | Some s -> s | None -> match cmd_coqtop#get with - | Some s -> s - | None -> - try - let old_prog = Sys.executable_name in - let pos = String.length old_prog - 6 in - let i = Str.search_backward (Str.regexp_string "coqide") old_prog pos - in - let new_prog = Bytes.of_string old_prog in - Bytes.blit_string "coqtop" 0 new_prog i 6; - let new_prog = Bytes.to_string new_prog in + | Some s -> s + | None -> + try + let new_prog = System.get_toplevel_path "coqidetop" in if Sys.file_exists new_prog then new_prog else let in_macos_bundle = @@ -306,8 +300,8 @@ let coqtop_path () = (Filename.dirname new_prog) (Filename.concat "../Resources/bin" (Filename.basename new_prog)) in if Sys.file_exists in_macos_bundle then in_macos_bundle - else "coqtop" - with Not_found -> "coqtop" + else "coqidetop" + with Not_found -> "coqidetop" in file (* In win32, when a command-line is to be executed via cmd.exe diff --git a/lib/system.ml b/lib/system.ml index dfede29e8..f109c7192 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 3349dfea3..a34280037 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 b3e1500ae..0105f821e 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 36b5d18ab..841cc08c0 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 2983b619d..be5b29177 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.ml b/stm/proofworkertop.ml deleted file mode 100644 index 4b85a05ac..000000000 --- a/stm/proofworkertop.ml +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* W.main_loop ()) - diff --git a/stm/proofworkertop.mllib b/stm/proofworkertop.mllib deleted file mode 100644 index f9f6c22d5..000000000 --- a/stm/proofworkertop.mllib +++ /dev/null @@ -1 +0,0 @@ -Proofworkertop diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml deleted file mode 100644 index aa00102aa..000000000 --- a/stm/queryworkertop.ml +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* W.main_loop ()) - diff --git a/stm/queryworkertop.mllib b/stm/queryworkertop.mllib deleted file mode 100644 index c2f73089b..000000000 --- a/stm/queryworkertop.mllib +++ /dev/null @@ -1 +0,0 @@ -Queryworkertop diff --git a/stm/stm.ml b/stm/stm.ml index 20409c25e..6b92e4737 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 72b538016..4b254e811 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.ml b/stm/tacworkertop.ml deleted file mode 100644 index 3b91df86e..000000000 --- a/stm/tacworkertop.ml +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* W.main_loop ()) - diff --git a/stm/tacworkertop.mllib b/stm/tacworkertop.mllib deleted file mode 100644 index db38fde27..000000000 --- a/stm/tacworkertop.mllib +++ /dev/null @@ -1 +0,0 @@ -Tacworkertop diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml deleted file mode 100644 index 5130b019a..000000000 --- a/stm/workerLoop.ml +++ /dev/null @@ -1,25 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* parse rest - | x :: rest -> x :: parse rest - | [] -> [] - -let loop init coq_args extra_args = - let args = parse extra_args in - Flags.quiet := true; - init (); - CoqworkmgrApi.init !async_proofs_worker_priority; - coq_args, args diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index d48c6d0af..47bd2493f 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/topbin/coqproofworker_bin.ml b/topbin/coqproofworker_bin.ml new file mode 100644 index 000000000..7ae91cfbd --- /dev/null +++ b/topbin/coqproofworker_bin.ml @@ -0,0 +1,14 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* f () + | _ -> () + end + with + | Not_found -> () + end; + let ppf = Format.std_formatter in + Mltop.(set_top + { load_obj = (fun f -> if not (Topdirs.load_file ppf f) + then CErrors.user_err Pp.(str ("Could not load plugin "^f)) + ); + use_file = Topdirs.dir_use ppf; + add_dir = Topdirs.dir_directory; + ml_loop = (fun () -> Toploop.loop ppf); + }) + +(* Main coqtop initialization *) +let _ = + drop_setup (); + Coqtop.(start_coq coqtop_toplevel) diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 17e848c5a..5c1ffd784 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 de9b6a682..9fb6219a6 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 3e7a83085..e61f830f3 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 da9169514..d7ede1c2e 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 6d9867fb9..5c07a8bf3 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 809490166..e979d0e54 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 fcc569ca0..641448f10 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/coqtop_byte_bin.ml b/toplevel/coqtop_byte_bin.ml deleted file mode 100644 index 0b65cebbb..000000000 --- a/toplevel/coqtop_byte_bin.ml +++ /dev/null @@ -1,34 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* f () - | _ -> () - end - with - | Not_found -> () - end; - let ppf = Format.std_formatter in - Mltop.(set_top - { load_obj = (fun f -> if not (Topdirs.load_file ppf f) - then CErrors.user_err Pp.(str ("Could not load plugin "^f)) - ); - use_file = Topdirs.dir_use ppf; - add_dir = Topdirs.dir_directory; - ml_loop = (fun () -> Toploop.loop ppf); - }) - -(* Main coqtop initialization *) -let _ = - drop_setup (); - Coqtop.start() diff --git a/toplevel/coqtop_opt_bin.ml b/toplevel/coqtop_opt_bin.ml deleted file mode 100644 index ea4c0ea52..000000000 --- a/toplevel/coqtop_opt_bin.ml +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* parse rest + | x :: rest -> x :: parse rest + | [] -> [] + +let arg_init init ~opts extra_args = + let extra_args = parse extra_args in + Flags.quiet := true; + init (); + 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/toplevel/workerLoop.mli b/toplevel/workerLoop.mli new file mode 100644 index 000000000..e497dee6d --- /dev/null +++ b/toplevel/workerLoop.mli @@ -0,0 +1,14 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* unit) -> + loop:(unit -> unit) -> unit diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 343b0925d..d25dea141 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 da195f4fc..ed1f9a12d 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} *) -- cgit v1.2.3