diff options
45 files changed, 161 insertions, 582 deletions
diff --git a/.gitignore b/.gitignore index 36536ec96..cec51986d 100644 --- a/.gitignore +++ b/.gitignore @@ -157,7 +157,6 @@ plugins/ssr/ssrvernac.ml kernel/byterun/coq_jumptbl.h kernel/copcodes.ml -tools/tolink.ml ide/index_urls.txt .lia.cache checker/names.ml @@ -87,7 +87,7 @@ EXISTINGMLI := $(call find, '*.mli') ## Files that will be generated GENML4FILES:= $(ML4FILES:.ml4=.ml) -export GENMLFILES:=$(LEXFILES:.mll=.ml) tools/tolink.ml kernel/copcodes.ml +export GENMLFILES:=$(LEXFILES:.mll=.ml) kernel/copcodes.ml export GENHFILES:=kernel/byterun/coq_jumptbl.h export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) @@ -246,7 +246,7 @@ archclean: clean-ide optclean voclean rm -f $(ALLSTDLIB).* optclean: - rm -f $(COQTOPEXE) $(COQMKTOP) $(CHICKEN) + rm -f $(COQTOPEXE) $(CHICKEN) 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 d548a8bd8..940943c41 100644 --- a/Makefile.build +++ b/Makefile.build @@ -228,8 +228,8 @@ endef define bestocaml $(if $(OPT),\ -$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@ && $(CODESIGN) $@,\ -$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ $(1) $(addsuffix .cma,$(2)) $^) +$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ -linkpkg $(1) $^ && $(STRIP) $@ && $(CODESIGN) $@,\ +$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ -linkpkg $(1) $^) endef # Camlp5 settings @@ -239,9 +239,8 @@ CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) -SYSMOD:=str unix dynlink threads -SYSCMA:=$(addsuffix .cma,$(SYSMOD)) -SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD)) +# Main packages linked by Coq. +SYSMOD:=-package num,str,unix,dynlink,threads # We do not repeat the dependencies already in SYSMOD here P4CMA:=gramlib.cma @@ -370,19 +369,30 @@ grammar/%.cmi: grammar/%.mli ########################################################################### -# Main targets (coqmktop, coqtop.opt, coqtop.byte) +# Main targets (coqtop.opt, coqtop.byte) ########################################################################### .PHONY: coqbinaries coqbyte -coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) +coqbinaries: $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) coqbyte: $(COQTOPBYTE) $(CHICKENBYTE) +COQTOP_OPT_MLTOP=toplevel/coqtop_opt_bin.cmx +COQTOP_BYTE_MLTOP=toplevel/coqtop_byte_bin.cmo + +$(COQTOP_BYTE_MLTOP): toplevel/coqtop_byte_bin.ml + $(SHOW)'OCAMLC $<' + $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -package compiler-libs.toplevel -c $< + ifeq ($(BEST),opt) -$(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) +$(COQTOPEXE): $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT_MLTOP) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) $(LINKMETADATA) -o $@ + $(HIDE)$(OCAMLOPT) -linkall -linkpkg -I toplevel \ + -I kernel/byterun/ -cclib -lcoqrun \ + $(SYSMOD) -package camlp5.gramlib \ + $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) \ + $(COQTOP_OPT_MLTOP) toplevel/coqtop_bin.ml -o $@ $(STRIP) $@ $(CODESIGN) $@ else @@ -390,23 +400,14 @@ $(COQTOPEXE): $(COQTOPBYTE) cp $< $@ endif -$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) +# Are "-cclib lcoqrun -dllib -lcoqrun" necessary? +$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@ - -# coqmktop - -COQMKTOPCMO:=lib/clib.cma lib/cErrors.cmo tools/tolink.cmo tools/coqmktop.cmo - -$(COQMKTOP): $(call bestobj, $(COQMKTOPCMO)) - $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) - -tools/tolink.ml: Makefile.build Makefile.common - $(SHOW)"ECHO... >" $@ - $(HIDE)echo "let copts = \"-cclib -lcoqrun\"" > $@ - $(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@ - $(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@ + $(HIDE)$(OCAMLC) -linkall -linkpkg -I toplevel \ + -I kernel/byterun -dllpath $(abspath kernel/byterun) -cclib -lcoqrun -dllib -lcoqrun \ + $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \ + $(LINKCMO) $(BYTEFLAGS) \ + $(COQTOP_BYTE_MLTOP) toplevel/coqtop_bin.ml -o $@ # coqc @@ -414,7 +415,7 @@ COQCCMO:=lib/clib.cma lib/cErrors.cmo toplevel/usage.cmo tools/coqc.cmo $(COQC): $(call bestobj, $(COQCCMO)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) + $(HIDE)$(call bestocaml, $(SYSMOD)) ########################################################################### # other tools @@ -451,11 +452,11 @@ tools/coqdep_boot.cmx : tools/coqdep_common.cmx $(COQDEPBOOT): $(call bestobj, $(COQDEPBOOTSRC)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, -I tools, unix) + $(HIDE)$(call bestocaml, -I tools -package unix) $(OCAMLLIBDEP): $(call bestobj, tools/ocamllibdep.cmo) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, -I tools, unix) + $(HIDE)$(call bestocaml, -I tools -package unix) # The full coqdep (unused by this build, but distributed by make install) @@ -466,36 +467,36 @@ COQDEPCMO:=lib/clib.cma lib/cErrors.cmo lib/cWarnings.cmo \ $(COQDEP): $(call bestobj, $(COQDEPCMO)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) + $(HIDE)$(call bestocaml, $(SYSMOD)) $(GALLINA): $(call bestobj, tools/gallina_lexer.cmo tools/gallina.cmo) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,) + $(HIDE)$(call bestocaml,) COQMAKEFILECMO:=lib/clib.cma tools/coq_makefile.cmo $(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,str unix threads) + $(HIDE)$(call bestocaml, -package str,unix,threads) $(COQTEX): $(call bestobj, tools/coq_tex.cmo) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,str) + $(HIDE)$(call bestocaml, -package str) $(COQWC): $(call bestobj, tools/coqwc.cmo) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,) + $(HIDE)$(call bestocaml, -package str) COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \ cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo ) $(COQDOC): $(call bestobj, $(COQDOCCMO)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,str unix) + $(HIDE)$(call bestocaml, -package str,unix) $(COQWORKMGR): $(call bestobj, lib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,, $(SYSMOD)) + $(HIDE)$(call bestocaml, $(SYSMOD)) # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqtop -ideslave @@ -506,13 +507,13 @@ FAKEIDECMO:= lib/clib.cma lib/cErrors.cmo lib/spawn.cmo ide/document.cmo \ $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,-I ide,str unix threads) + $(HIDE)$(call bestocaml, -I ide -package str,unix,threads) # votour: a small vo explorer (based on the checker) bin/votour: $(call bestobj, lib/cObj.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, -I checker,) + $(HIDE)$(call bestocaml, -I checker) ########################################################################### # Csdp to micromega special targets @@ -524,7 +525,7 @@ CSDPCERTCMO:=lib/clib.cma $(addprefix plugins/micromega/, \ $(CSDPCERT): $(call bestobj, $(CSDPCERTCMO)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,nums unix) + $(HIDE)$(call bestocaml, -package num,unix) ########################################################################### # tests diff --git a/Makefile.checker b/Makefile.checker index 435d8e8f6..b14f705be 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -29,7 +29,7 @@ CHKLIBS:= -I config -I lib -I checker ifeq ($(BEST),opt) $(CHICKEN): checker/check.cmxa checker/main.ml $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(SYSCMXA) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^ + $(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^ $(STRIP) $@ $(CODESIGN) $@ else @@ -39,7 +39,7 @@ endif $(CHICKENBYTE): checker/check.cma checker/main.ml $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(SYSCMA) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^ + $(HIDE)$(OCAMLC) -linkpkg $(SYSMOD) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^ checker/check.cma: checker/check.mllib | md5chk $(SHOW)'OCAMLC -a -o $@' diff --git a/Makefile.common b/Makefile.common index 4d63b08e2..f436d3e8f 100644 --- a/Makefile.common +++ b/Makefile.common @@ -12,8 +12,6 @@ # Executables ########################################################################### -COQMKTOP:=bin/coqmktop$(EXE) - COQTOPBYTE:=bin/coqtop.byte$(EXE) COQTOPEXE:=bin/coqtop$(EXE) diff --git a/Makefile.install b/Makefile.install index 27694106f..84aa11a5e 100644 --- a/Makefile.install +++ b/Makefile.install @@ -105,7 +105,6 @@ INSTALLCMX = $(sort $(filter-out checker/% ide/% tools/% dev/% configure.cmx, $( install-devfiles: $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR) $(MKDIR) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(GRAMMARCMA) $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) @@ -140,7 +139,7 @@ install-coq-info: install-coq-manpages install-emacs install-latex MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \ man/coqwc.1 man/coqdoc.1 man/coqide.1 \ - man/coq_makefile.1 man/coqmktop.1 man/coqchk.1 + man/coq_makefile.1 man/coqchk.1 install-coq-manpages: $(MKDIR) $(FULLMANDIR)/man1 diff --git a/checker/inductive.ml b/checker/inductive.ml index 1271a02b0..22353ec16 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -1070,8 +1070,8 @@ let check_fix env ((nvect,_),(names,_,bodies as _recdef) as fix) = done (* -let cfkey = Profile.declare_profile "check_fix";; -let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; +let cfkey = CProfile.declare_profile "check_fix";; +let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;; *) (************************************************************************) diff --git a/config/coq_config.mli b/config/coq_config.mli index 6a834a304..40661f428 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -41,12 +41,8 @@ val caml_flags : string (* arguments passed to ocamlc (ie. CAMLFLAGS) *) val best : string (* byte/opt *) val arch : string (* architecture *) val arch_is_win32 : bool -val osdeplibs : string (* OS dependent link options for ocamlc *) val vmbyteflags : string list (* -custom/-dllib -lcoqrun *) - -(* val defined : string list (* options for lib/ocamlpp *) *) - val version : string (* version number of Coq *) val caml_version : string (* OCaml version used to compile Coq *) val caml_version_nums : int list (* OCaml version used to compile Coq by components *) diff --git a/configure.ml b/configure.ml index 3850f119b..2292913d5 100644 --- a/configure.ml +++ b/configure.ml @@ -16,7 +16,7 @@ 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";"coqmktop";"coqworkmgr"; +let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqworkmgr"; "coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"] let verbose = ref false (* for debugging this script *) @@ -680,17 +680,15 @@ let natdynlinkflag = (** * OS dependent libraries *) -let osdeplibs = "-cclib -lunix" - -let operating_system, osdeplibs = +let operating_system = if starts_with arch "sun4" then let os, _ = run "uname" ["-r"] in if starts_with os "5" then - "Sun Solaris "^os, osdeplibs^" -cclib -lnsl -cclib -lsocket" + "Sun Solaris "^os else - "Sun OS "^os, osdeplibs + "Sun OS "^os else - (try Sys.getenv "OS" with Not_found -> ""), osdeplibs + (try Sys.getenv "OS" with Not_found -> "") (** Num library *) @@ -1016,7 +1014,6 @@ let print_summary () = pr " Operating system : %s\n" operating_system; pr " Coq VM bytecode link flags : %s\n" (String.concat " " vmbyteflags); pr " Other bytecode link flags : %s\n" custom_flag; - pr " OS dependent libraries : %s\n" osdeplibs; pr " OCaml version : %s\n" caml_version; pr " OCaml binaries in : %s\n" (esc camlbin); pr " OCaml library in : %s\n" (esc camllib); @@ -1109,7 +1106,6 @@ let write_configml f = pr_s "cflags" cflags; pr_s "caml_flags" caml_flags; pr_s "best" best_compiler; - pr_s "osdeplibs" osdeplibs; pr_s "version" coq_version; pr_s "caml_version" caml_version; pr_li "caml_version_nums" caml_version_nums; @@ -1240,7 +1236,6 @@ let write_makefile f = pr "# Supplementary libs for some systems, currently:\n"; pr "# . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket\n"; pr "# . others : -cclib -lunix\n"; - pr "OSDEPLIBS=%s\n\n" osdeplibs; pr "# executable files extension, currently:\n"; pr "# Unix systems:\n"; pr "# Win32 systems : .exe\n"; diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt index a6d8e4462..7e80e33c6 100644 --- a/dev/build/windows/ReadMe.txt +++ b/dev/build/windows/ReadMe.txt @@ -418,7 +418,6 @@ Binary file ./bin/coqchk.exe matches Binary file ./bin/coqdep.exe matches Binary file ./bin/coqdoc.exe matches Binary file ./bin/coqide.exe matches -Binary file ./bin/coqmktop.exe matches Binary file ./bin/coqtop.byte.exe matches Binary file ./bin/coqtop.exe matches Binary file ./bin/coqworkmgr.exe matches @@ -438,7 +437,6 @@ Binary file ./bin/ocamldoc.exe matches Binary file ./bin/ocamldoc.opt.exe matches Binary file ./bin/ocamlfind.exe matches Binary file ./bin/ocamlmklib.exe matches -Binary file ./bin/ocamlmktop.exe matches Binary file ./bin/ocamlobjinfo.exe matches Binary file ./bin/ocamlopt.exe matches Binary file ./bin/ocamlopt.opt.exe matches diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md index 7d3d811cc..fa145d498 100644 --- a/dev/doc/debugging.md +++ b/dev/doc/debugging.md @@ -73,8 +73,8 @@ Per function profiling To profile function foo in file bar.ml, add the following lines, just after the definition of the function: - let fookey = Profile.declare_profile "foo";; - let foo a b c = Profile.profile3 fookey foo a b c;; + let fookey = CProfile.declare_profile "foo";; + let foo a b c = CProfile.profile3 fookey foo a b c;; where foo is assumed to have three arguments (adapt using Profile.profile1, Profile. profile2, etc). diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt index 0c6d3ee80..26f3d0ddc 100644 --- a/dev/doc/setup.txt +++ b/dev/doc/setup.txt @@ -279,7 +279,7 @@ You can load them by switching to the window holding the "ocamldebug" shell and Some of the functions were you might want to set a breakpoint and see what happens next --------------------------------------------------------------------------------------- -- Coqtop.start : This function is called by the code produced by "coqmktop". +- Coqtop.start : This function is the main entry point of coqtop. - Coqtop.parse_args : This function is responsible for parsing command-line arguments. - Coqloop.loop : This function implements the read-eval-print loop. - Vernacentries.interp : This function is called to execute the Vernacular command user have typed.\ diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index c411db100..962aa98b6 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -4,53 +4,24 @@ The distribution provides utilities to simplify some tedious works beside proof development, tactics writing or documentation. -\section[Building a toplevel extended with user tactics]{Building a toplevel extended with user tactics\label{Coqmktop}\ttindex{coqmktop}} +\section[Using Coq as a library]{Using Coq as a library} -The native-code version of \Coq\ cannot dynamically load user tactics -using {\ocaml} code. It is possible to build a toplevel of \Coq, -with {\ocaml} code statically linked, with the tool {\tt - coqmktop}. - -For example, one can build a native-code \Coq\ toplevel extended with a tactic -which source is in {\tt tactic.ml} with the command -\begin{verbatim} - % coqmktop -opt -o mytop.out tactic.cmx -\end{verbatim} -where {\tt tactic.ml} has been compiled with the native-code -compiler {\tt ocamlopt}. This command generates an executable -called {\tt mytop.out}. To use this executable to compile your \Coq\ -files, use {\tt coqc -image mytop.out}. - -A basic example is the native-code version of \Coq\ ({\tt coqtop.opt}), -which can be generated by {\tt coqmktop -opt -o coqopt.opt}. - - -\paragraph[Application: how to use the {\ocaml} debugger with Coq.]{Application: how to use the {\ocaml} debugger with Coq.\index{Debugger}} - -One useful application of \texttt{coqmktop} is to build a \Coq\ toplevel in -order to debug your tactics with the {\ocaml} debugger. -You need to have configured and compiled \Coq\ for debugging -(see the file \texttt{INSTALL} included in the distribution). -Then, you must compile the Caml modules of your tactic with the -option \texttt{-g} (with the bytecode compiler) and build a stand-alone -bytecode toplevel with the following command: +In previous versions, \texttt{coqmktop} was used to build custom +toplevels --- for example for better debugging or custom static +linking. Nowadays, the preferred method is to use \texttt{ocamlfind}. +The most basic custom toplevel is built using: \begin{quotation} -\texttt{\% coqmktop -g -o coq-debug}~\emph{<your \texttt{.cmo} files>} +\texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg + -package coq.toplevel toplevel/coqtop\_bin.ml -o my\_toplevel.native} \end{quotation} - -To launch the \ocaml\ debugger with the image you need to execute it in -an environment which correctly sets the \texttt{COQLIB} variable. -Moreover, you have to indicate the directories in which -\texttt{ocamldebug} should search for Caml modules. - -A possible solution is to use a wrapper around \texttt{ocamldebug} -which detects the executables containing the word \texttt{coq}. In -this case, the debugger is called with the required additional -arguments. In other cases, the debugger is simply called without additional -arguments. Such a wrapper can be found in the \texttt{dev/} -subdirectory of the sources. +For example, to statically link LTAC, you can just do: +\begin{quotation} +\texttt{\% ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg + -package coq.toplevel -package coq.ltac toplevel/coqtop\_bin.ml -o my\_toplevel.native} +\end{quotation} +and similarly for other plugins. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/engine/uState.ml b/engine/uState.ml index 6566ad989..6131f4c03 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -240,8 +240,8 @@ let add_constraints ctx cstrs = uctx_univ_variables = vars; uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } -(* let addconstrkey = Profile.declare_profile "add_constraints_context";; *) -(* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *) +(* let addconstrkey = CProfile.declare_profile "add_constraints_context";; *) +(* let add_constraints_context = CProfile.profile2 addconstrkey add_constraints_context;; *) let add_universe_constraints ctx cstrs = let univs, local = ctx.uctx_local in diff --git a/engine/universes.ml b/engine/universes.ml index 0250295fd..30490ec56 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -946,8 +946,8 @@ let normalize_context_set ctx us algs = let us = normalize_opt_subst us in (us, algs), (ctx', Constraint.union noneqs eqs) -(* let normalize_conkey = Profile.declare_profile "normalize_context_set" *) -(* let normalize_context_set a b c = Profile.profile3 normalize_conkey normalize_context_set a b c *) +(* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *) +(* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *) let is_trivial_leq (l,d,r) = Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r)) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 2579ac045..7b921d35b 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -250,7 +250,7 @@ let cook_constant ~hcons env { from = cb; info } = cook_context = Some const_hyps; } -(* let cook_constant_key = Profile.declare_profile "cook_constant" *) -(* let cook_constant = Profile.profile2 cook_constant_key cook_constant *) +(* let cook_constant_key = CProfile.declare_profile "cook_constant" *) +(* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *) let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 62aa9a2d7..2a629f00a 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1098,8 +1098,8 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) = () (* -let cfkey = Profile.declare_profile "check_fix";; -let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; +let cfkey = CProfile.declare_profile "check_fix";; +let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;; *) (************************************************************************) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index b0f4a1e5f..c07ac973b 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -833,8 +833,8 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 = let gen_conv cv_pb ?(l2r=false) ?(reds=full_transparent_state) env ?(evars=(fun _->None), universes env) = let evars, univs = evars in if Flags.profile then - let fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in - Profile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs + let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in + CProfile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs else gen_conv cv_pb l2r reds env evars univs let conv = gen_conv CONV @@ -860,8 +860,8 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = (* Profiling *) let infer_conv_universes = if Flags.profile then - let infer_conv_universes_key = Profile.declare_profile "infer_conv_universes" in - Profile.profile8 infer_conv_universes_key infer_conv_universes + let infer_conv_universes_key = CProfile.declare_profile "infer_conv_universes" in + CProfile.profile8 infer_conv_universes_key infer_conv_universes else infer_conv_universes let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_state) @@ -895,13 +895,13 @@ let default_conv cv_pb ?(l2r=false) env t1 t2 = let default_conv_leq = default_conv CUMUL (* -let convleqkey = Profile.declare_profile "Kernel_reduction.conv_leq";; +let convleqkey = CProfile.declare_profile "Kernel_reduction.conv_leq";; let conv_leq env t1 t2 = - Profile.profile4 convleqkey conv_leq env t1 t2;; + CProfile.profile4 convleqkey conv_leq env t1 t2;; -let convkey = Profile.declare_profile "Kernel_reduction.conv";; +let convkey = CProfile.declare_profile "Kernel_reduction.conv";; let conv env t1 t2 = - Profile.profile4 convleqkey conv env t1 t2;; + CProfile.profile4 convleqkey conv env t1 t2;; *) (* Application with on-the-fly reduction *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 4ccef5c38..4a935f581 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -435,8 +435,8 @@ let infer env constr = let infer = if Flags.profile then - let infer_key = Profile.declare_profile "Fast_infer" in - Profile.profile2 infer_key (fun b c -> infer b c) + let infer_key = CProfile.declare_profile "Fast_infer" in + CProfile.profile2 infer_key (fun b c -> infer b c) else (fun b c -> infer b c) let assumption_of_judgment env {uj_val=c; uj_type=t} = diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 00c0ea70d..f1e8d1031 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -890,24 +890,24 @@ let dump_universes output g = let merge_constraints = if Flags.profile then - let key = Profile.declare_profile "merge_constraints" in - Profile.profile2 key merge_constraints + let key = CProfile.declare_profile "merge_constraints" in + CProfile.profile2 key merge_constraints else merge_constraints let check_constraints = if Flags.profile then - let key = Profile.declare_profile "check_constraints" in - Profile.profile2 key check_constraints + let key = CProfile.declare_profile "check_constraints" in + CProfile.profile2 key check_constraints else check_constraints let check_eq = if Flags.profile then - let check_eq_key = Profile.declare_profile "check_eq" in - Profile.profile3 check_eq_key check_eq + let check_eq_key = CProfile.declare_profile "check_eq" in + CProfile.profile3 check_eq_key check_eq else check_eq let check_leq = if Flags.profile then - let check_leq_key = Profile.declare_profile "check_leq" in - Profile.profile3 check_leq_key check_leq + let check_leq_key = CProfile.declare_profile "check_leq" in + CProfile.profile3 check_leq_key check_leq else check_leq diff --git a/kernel/vars.ml b/kernel/vars.ml index f52d734ef..eae917b5a 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -133,8 +133,8 @@ let substn_many lamv n c = substrec n c (* -let substkey = Profile.declare_profile "substn_many";; -let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;; +let substkey = CProfile.declare_profile "substn_many";; +let substn_many lamv n c = CProfile.profile3 substkey substn_many lamv n c;; *) let make_subst = function @@ -274,8 +274,8 @@ let subst_univs_constr subst c = let subst_univs_constr = if Flags.profile then - let subst_univs_constr_key = Profile.declare_profile "subst_univs_constr" in - Profile.profile2 subst_univs_constr_key subst_univs_constr + let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in + CProfile.profile2 subst_univs_constr_key subst_univs_constr else subst_univs_constr let subst_univs_level_constr subst c = @@ -347,8 +347,8 @@ let subst_instance_constr subst c = in aux c -(* let substkey = Profile.declare_profile "subst_instance_constr";; *) -(* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *) +(* let substkey = CProfile.declare_profile "subst_instance_constr";; *) +(* let subst_instance_constr inst c = CProfile.profile2 substkey subst_instance_constr inst c;; *) let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx diff --git a/lib/profile.ml b/lib/cProfile.ml index 0bc226a45..0bc226a45 100644 --- a/lib/profile.ml +++ b/lib/cProfile.ml diff --git a/lib/profile.mli b/lib/cProfile.mli index cae4397a1..cae4397a1 100644 --- a/lib/profile.mli +++ b/lib/cProfile.mli diff --git a/lib/envars.ml b/lib/envars.ml index 206d75033..8ebf84057 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -153,19 +153,17 @@ let coqpath = let exe s = s ^ Coq_config.exec_extension -let ocamlfind () = - if !Flags.ocamlfind_spec then !Flags.ocamlfind else Coq_config.ocamlfind +let ocamlfind () = Coq_config.ocamlfind (** {2 Camlp4 paths} *) let guess_camlp4bin () = which (user_path ()) (exe Coq_config.camlp4) let camlp4bin () = - if !Flags.camlp4bin_spec then !Flags.camlp4bin else - if !Flags.boot then Coq_config.camlp4bin else - try guess_camlp4bin () - with Not_found -> - Coq_config.camlp4bin + if !Flags.boot then Coq_config.camlp4bin else + try guess_camlp4bin () + with Not_found -> + Coq_config.camlp4bin let camlp4 () = camlp4bin () / exe Coq_config.camlp4 diff --git a/lib/flags.ml b/lib/flags.ml index b43d5f74d..9631da633 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -153,14 +153,6 @@ let is_standard_doc_url url = let coqlib_spec = ref false let coqlib = ref "(not initialized yet)" -(* Options for changing ocamlfind (used by coqmktop) *) -let ocamlfind_spec = ref false -let ocamlfind = ref Coq_config.camlbin - -(* Options for changing camlp4bin (used by coqmktop) *) -let camlp4bin_spec = ref false -let camlp4bin = ref Coq_config.camlp4bin - (* Level of inlining during a functor application *) let default_inline_level = 100 diff --git a/lib/flags.mli b/lib/flags.mli index b82fe6128..1b1e264f0 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -122,12 +122,6 @@ val is_standard_doc_url : string -> bool val coqlib_spec : bool ref val coqlib : string ref -(** Options for specifying where OCaml binaries reside *) -val ocamlfind_spec : bool ref -val ocamlfind : string ref -val camlp4bin_spec : bool ref -val camlp4bin : string ref - (** Level of inlining during a functor application *) val set_inline_level : int -> unit val get_inline_level : unit -> int diff --git a/lib/lib.mllib b/lib/lib.mllib index 8791f0741..66f939a91 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -9,7 +9,7 @@ System CThread Spawn Trie -Profile +CProfile Explore Predicate Rtree diff --git a/man/coqmktop.1 b/man/coqmktop.1 deleted file mode 100644 index 810df782c..000000000 --- a/man/coqmktop.1 +++ /dev/null @@ -1,71 +0,0 @@ -.TH COQ 1 "April 25, 2001" - -.SH NAME -coqmktop \- The Coq Proof Assistant user-tactics linker - - -.SH SYNOPSIS -.B coqmktop -[ -.I options -] -.I files - - -.SH DESCRIPTION - -.B coqmktop -builds a new Coq toplevel extended with user-tactics. -.IR files \& -are the Objective Caml object or library files -(i.e. with suffix .cmo, .cmx, .cma or .cmxa) to link with the Coq system. -The linker produces an executable Coq toplevel which can be called -directly or through coqc(1), using the \-image option. - -.SH OPTIONS - -.TP -.BI \-h -Help. List the available options. - -.TP -.BI \-srcdir \ dir -Specify where the Coq source files are - -.TP -.BI \-o \ exec\-file -Specify the name of the resulting toplevel - -.TP -.B \-opt -Compile in native code - -.TP -.B \-full -Link high level tactics - -.TP -.B \-top -Build Coq on a ocaml toplevel (incompatible with -.BR \-opt ) - -.TP -.BI \-R \ dir -Specify recursively directories for Ocaml - -.TP -.B \-v8 -Link with V8 grammar - - -.SH SEE ALSO - -.BR coqtop (1), -.BR ocamlmktop (1). -.BR ocamlc (1). -.BR ocamlopt (1). -.br -.I -The Coq Reference Manual. -.I -The Coq web site: http://coq.inria.fr diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 1f2e5f7ac..2e14243d8 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -361,8 +361,8 @@ end) = struct end (* let my_type_of env evars c = Typing.e_type_of env evars c *) -(* let mytypeofkey = Profile.declare_profile "my_type_of";; *) -(* let my_type_of = Profile.profile3 mytypeofkey my_type_of *) +(* let mytypeofkey = CProfile.declare_profile "my_type_of";; *) +(* let my_type_of = CProfile.profile3 mytypeofkey my_type_of *) let type_app_poly env env evd f args = @@ -2086,8 +2086,8 @@ let get_hyp gl (c,l) clause l2r = let general_rewrite_flags = { under_lambdas = false; on_morphisms = true } -(* let rewriteclaustac_key = Profile.declare_profile "cl_rewrite_clause_tac";; *) -(* let cl_rewrite_clause_tac = Profile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) +(* let rewriteclaustac_key = CProfile.declare_profile "cl_rewrite_clause_tac";; *) +(* let cl_rewrite_clause_tac = CProfile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) (** Setoid rewriting when called with "rewrite" *) let general_s_rewrite cl l2r occs (c,l) ~new_goals = diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e5776d2ec..cb8844623 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1063,8 +1063,8 @@ let evar_conv_x ts = evar_conv_x (ts, true) (* Profiling *) let evar_conv_x = if Flags.profile then - let evar_conv_xkey = Profile.declare_profile "evar_conv_x" in - Profile.profile6 evar_conv_xkey evar_conv_x + let evar_conv_xkey = CProfile.declare_profile "evar_conv_x" in + CProfile.profile6 evar_conv_xkey evar_conv_x else evar_conv_x let evar_conv_hook_get, evar_conv_hook_set = Hook.make ~default:evar_conv_x () diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 318176611..d9994c473 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1269,11 +1269,11 @@ let nf_all env sigma = (* Conversion *) (********************************************************************) (* -let fkey = Profile.declare_profile "fhnf";; -let fhnf info v = Profile.profile2 fkey fhnf info v;; +let fkey = CProfile.declare_profile "fhnf";; +let fhnf info v = CProfile.profile2 fkey fhnf info v;; -let fakey = Profile.declare_profile "fhnf_apply";; -let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;; +let fakey = CProfile.declare_profile "fhnf_apply";; +let fhnf_apply info k h a = CProfile.profile4 fakey fhnf_apply info k h a;; *) let is_transparent e k = diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index f8f086fad..00b175c48 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -227,8 +227,8 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = (* let f,_,_,_ = retype ~polyprop sigma in *) (* if lax then f env c else anomaly_on_error (f env) c *) -(* let get_type_of_key = Profile.declare_profile "get_type_of" *) -(* let get_type_of = Profile.profile5 get_type_of_key get_type_of *) +(* let get_type_of_key = CProfile.declare_profile "get_type_of" *) +(* let get_type_of = CProfile.profile5 get_type_of_key get_type_of *) (* let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = *) (* get_type_of polyprop lax env sigma c *) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 85383ba39..5a522e06a 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -927,8 +927,8 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c = let whd_simpl_stack = if Flags.profile then - let key = Profile.declare_profile "whd_simpl_stack" in - Profile.profile3 key whd_simpl_stack + let key = CProfile.declare_profile "whd_simpl_stack" in + CProfile.profile3 key whd_simpl_stack else whd_simpl_stack (* Same as [whd_simpl] but also reduces constants that do not hide a diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 2e213a51d..b49da57a4 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -552,8 +552,8 @@ let solve_all_instances env evd filter unique split fail = Hook.get get_solve_all_instances env evd filter unique split fail (** Profiling resolution of typeclasses *) -(* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *) -(* let solve_problem = Profile.profile5 solve_classeskey solve_problem *) +(* let solve_classeskey = CProfile.declare_profile "solve_typeclasses" *) +(* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *) let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ()) ?(split=true) ?(fail=true) env evd = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 84ffab426..08329391d 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -2015,8 +2015,8 @@ let w_unify env evd cv_pb flags ty1 ty2 = let w_unify = if Flags.profile then - let wunifkey = Profile.declare_profile "w_unify" in - Profile.profile6 wunifkey w_unify + let wunifkey = CProfile.declare_profile "w_unify" in + CProfile.profile6 wunifkey w_unify else w_unify let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 = diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 3e3313eb5..cd2b10906 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -30,8 +30,8 @@ let refiner pr goal_sigma = (* Profiling refiner *) let refiner = if Flags.profile then - let refiner_key = Profile.declare_profile "refiner" in - Profile.profile2 refiner_key refiner + let refiner_key = CProfile.declare_profile "refiner" in + CProfile.profile2 refiner_key refiner else refiner (*********************) diff --git a/tactics/auto.ml b/tactics/auto.ml index fa8435d1f..e7e21b5f4 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -514,8 +514,8 @@ let delta_auto debug mod_delta n lems dbnames = let delta_auto = if Flags.profile then - let key = Profile.declare_profile "delta_auto" in - Profile.profile5 key delta_auto + let key = CProfile.declare_profile "delta_auto" in + CProfile.profile5 key delta_auto else delta_auto let auto ?(debug=Off) n = delta_auto debug false n diff --git a/tactics/eauto.ml b/tactics/eauto.ml index d2e014e55..6ea6155e0 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -404,8 +404,8 @@ let e_search_auto debug (in_depth,p) lems db_list gl = pr_info_nop d; user_err Pp.(str "eauto: search failed") -(* let e_search_auto_key = Profile.declare_profile "e_search_auto" *) -(* let e_search_auto = Profile.profile5 e_search_auto_key e_search_auto *) +(* let e_search_auto_key = CProfile.declare_profile "e_search_auto" *) +(* let e_search_auto = CProfile.profile5 e_search_auto_key e_search_auto *) let eauto_with_bases ?(debug=Off) np lems db_list = tclTRY (e_search_auto debug np lems db_list) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6aa052d32..839090903 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1982,11 +1982,11 @@ let cut_and_apply c = (* Exact tactics *) (********************************************************************) -(* let convert_leqkey = Profile.declare_profile "convert_leq";; *) -(* let convert_leq = Profile.profile3 convert_leqkey convert_leq *) +(* let convert_leqkey = CProfile.declare_profile "convert_leq";; *) +(* let convert_leq = CProfile.profile3 convert_leqkey convert_leq *) -(* let refine_no_checkkey = Profile.declare_profile "refine_no_check";; *) -(* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *) +(* let refine_no_checkkey = CProfile.declare_profile "refine_no_check";; *) +(* let refine_no_check = CProfile.profile2 refine_no_checkkey refine_no_check *) let exact_no_check c = Refine.refine ~typecheck:false (fun h -> (h,c)) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 80b1f584b..2b56c63a0 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -87,7 +87,6 @@ COQCHK ?= "$(COQBIN)coqchk" COQDEP ?= "$(COQBIN)coqdep" GALLINA ?= "$(COQBIN)gallina" COQDOC ?= "$(COQBIN)coqdoc" -COQMKTOP ?= "$(COQBIN)coqmktop" COQMKFILE ?= "$(COQBIN)coq_makefile" # Timing scripts diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml deleted file mode 100644 index 950ed53cc..000000000 --- a/tools/coqmktop.ml +++ /dev/null @@ -1,314 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** {1 Coqmktop} *) - -(** coqmktop is a script to link Coq, analogous to ocamlmktop. - The command line contains options specific to coqmktop, options for the - Ocaml linker and files to link (in addition to the default Coq files). *) - -(** {6 Utilities} *) - -(** Split a string at each blank -*) -let split_list = - let spaces = Str.regexp "[ \t\n]+" in - fun str -> Str.split spaces str - -[@@@ocaml.warning "-3"] (* String.uncapitalize_ascii since 4.03.0 GPR#124 *) -let capitalize = String.capitalize -[@@@ocaml.warning "+3"] - -let (/) = Filename.concat - -(** Which user files do we support (and propagate to ocamlopt) ? -*) -let supported_suffix f = match CUnix.get_extension f with - | ".ml" | ".cmx" | ".cmo" | ".cmxa" | ".cma" | ".c" -> true - | _ -> false - -let supported_flambda_option f = List.mem f Coq_config.flambda_flags - -(** From bytecode extension to native -*) -let native_suffix f = match CUnix.get_extension f with - | ".cmo" -> (Filename.chop_suffix f ".cmo") ^ ".cmx" - | ".cma" -> (Filename.chop_suffix f ".cma") ^ ".cmxa" - | ".a" -> f - | _ -> failwith ("File "^f^" has not extension .cmo, .cma or .a") - -(** Transforms a file name in the corresponding Caml module name. -*) -let module_of_file name = - capitalize (try Filename.chop_extension name with Invalid_argument _ -> name) - -(** Run a command [prog] with arguments [args]. - We do not use [Sys.command] anymore, see comment in [CUnix.sys_command]. -*) -let run_command prog args = - match CUnix.sys_command prog args with - | Unix.WEXITED 127 -> failwith ("no such command "^prog) - | Unix.WEXITED n -> n - | Unix.WSIGNALED n -> failwith (prog^" killed by signal "^string_of_int n) - | Unix.WSTOPPED n -> failwith (prog^" stopped by signal "^string_of_int n) - - - -(** {6 Coqmktop options} *) - -let opt = ref false -let top = ref false -let echo = ref false -let no_start = ref false - -let is_ocaml4 = Coq_config.caml_version.[0] <> '3' - -(** {6 Includes options} *) - -(** Since the Coq core .cma are given with their relative paths - (e.g. "lib/clib.cma"), we only need to include directories mentionned in - the temp main ml file below (for accessing the corresponding .cmi). *) - -let std_includes basedir = - let rebase d = match basedir with None -> d | Some base -> base / d in - ["-I"; rebase "."; - "-I"; rebase "lib"; - "-I"; rebase "vernac"; (* For Mltop *) - "-I"; rebase "toplevel"; - "-I"; rebase "kernel/byterun"; - "-I"; Envars.camlp4lib () ] @ - (if is_ocaml4 then ["-I"; "+compiler-libs"] else []) - -(** For the -R option, visit all directories under [dir] and add - corresponding -I to the [opts] option list (in reversed order) *) -let incl_all_subdirs dir opts = - let l = ref opts in - let add f = l := f :: "-I" :: !l in - let rec traverse dir = - if Sys.file_exists dir && Sys.is_directory dir then - let () = add dir in - let subdirs = try Sys.readdir dir with any -> [||] in - Array.iter (fun f -> traverse (dir/f)) subdirs - in - traverse dir; !l - - -(** {6 Objects to link} *) - -(** NB: dynlink is now always linked, it is used for loading plugins - and compiled vm code (see native-compiler). We now reject platforms - with ocamlopt but no dynlink.cmxa during ./configure, and give - instructions there about how to build a dummy dynlink.cmxa, - cf. dev/dynlink.ml. *) - -(** OCaml + CamlpX libraries *) - -let ocaml_libs = ["str.cma";"unix.cma";"nums.cma";"dynlink.cma";"threads.cma"] -let camlp4_libs = ["gramlib.cma"] -let libobjs = ocaml_libs @ camlp4_libs - -(** Toplevel objects *) - -let ocaml_topobjs = - if is_ocaml4 then - ["ocamlcommon.cma";"ocamlbytecomp.cma";"ocamltoplevel.cma"] - else - ["toplevellib.cma"] - -let camlp4_topobjs = ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"] - -let topobjs = ocaml_topobjs @ camlp4_topobjs - -(** Coq Core objects *) - -let copts = (split_list Coq_config.osdeplibs) @ (split_list Tolink.copts) -let core_objs = split_list Tolink.core_objs -let core_libs = split_list Tolink.core_libs - -(** Build the list of files to link and the list of modules names -*) -let files_to_link userfiles = - let top = if !top then topobjs else [] in - let modules = List.map module_of_file (top @ core_objs @ userfiles) in - let objs = libobjs @ top @ core_libs in - let objs' = (if !opt then List.map native_suffix objs else objs) @ userfiles - in (modules, objs') - - -(** {6 Parsing of the command-line} *) - -let usage () = - prerr_endline "Usage: coqmktop <options> <ocaml options> files\ -\nFlags are:\ -\n -coqlib dir Specify where the Coq object files are\ -\n -ocamlfind dir Specify where the ocamlfind binary is\ -\n -camlp4bin dir Specify where the Camlp4/5 binaries are\ -\n -o exec-file Specify the name of the resulting toplevel\ -\n -boot Run in boot mode\ -\n -echo Print calls to external commands\ -\n -opt Compile in native code\ -\n -top Build Coq on a OCaml toplevel (incompatible with -opt)\ -\n -R dir Add recursively dir to OCaml search path\ -\n"; - exit 1 - -let parse_args () = - let rec parse (op,fl) = function - | [] -> List.rev op, List.rev fl - - (* Directories *) - | "-coqlib" :: d :: rem -> - Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem - | "-ocamlfind" :: d :: rem -> - Flags.ocamlfind_spec := true; Flags.ocamlfind := d ; parse (op,fl) rem - | "-camlp4bin" :: d :: rem -> - Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem - | "-R" :: d :: rem -> parse (incl_all_subdirs d op,fl) rem - | ("-coqlib"|"-camlbin"|"-camlp4bin"|"-R") :: [] -> usage () - - (* Boolean options of coqmktop *) - | "-boot" :: rem -> Flags.boot := true; parse (op,fl) rem - | "-opt" :: rem -> opt := true ; parse (op,fl) rem - | "-top" :: rem -> top := true ; parse (op,fl) rem - | "-no-start" :: rem -> no_start:=true; parse (op, fl) rem - | "-echo" :: rem -> echo := true ; parse (op,fl) rem - - (* Extra options with arity 0 or 1, directly passed to ocamlc/ocamlopt *) - | ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem -> - parse (o::op,fl) rem - | ("-cclib"|"-ccopt"|"-I"|"-o"|"-w" as o) :: rem' -> - begin - match rem' with - | a :: rem -> parse (a::o::op,fl) rem - | [] -> usage () - end - - | ("-h"|"-help"|"--help") :: _ -> usage () - | f :: rem when supported_flambda_option f -> parse (op,fl) rem - | f :: rem when supported_suffix f -> parse (op,f::fl) rem - | f :: _ -> prerr_endline ("Don't know what to do with " ^ f); exit 1 - in - parse ([],[]) (List.tl (Array.to_list Sys.argv)) - - -(** {6 Temporary main file} *) - -(** remove the temporary main file -*) -let clean file = - let rm f = if Sys.file_exists f then Sys.remove f in - let basename = Filename.chop_suffix file ".ml" in - if not !echo then begin - rm file; - rm (basename ^ ".o"); - rm (basename ^ ".cmi"); - rm (basename ^ ".cmo"); - rm (basename ^ ".cmx") - end - -(** Initializes the kind of loading in the main program -*) -let declare_loading_string () = - if not !top then - "Mltop.remove ();;" - else - "begin try\ -\n (* Enable rectypes in the toplevel if it has the directive #rectypes *)\ -\n begin match Hashtbl.find Toploop.directive_table \"rectypes\" with\ -\n | Toploop.Directive_none f -> f ()\ -\n | _ -> ()\ -\n end\ -\n with\ -\n | Not_found -> ()\ -\n end;;\ -\n\ -\n let ppf = Format.std_formatter;;\ -\n Mltop.set_top\ -\n {Mltop.load_obj=\ -\n (fun f -> if not (Topdirs.load_file ppf f)\ -\n then CErrors.user_err Pp.(str (\"Could not load plugin \"^f)));\ -\n Mltop.use_file=Topdirs.dir_use ppf;\ -\n Mltop.add_dir=Topdirs.dir_directory;\ -\n Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\ -\n" - -(** create a temporary main file to link -*) -let create_tmp_main_file modules = - let main_name,oc = Filename.open_temp_file "coqmain" ".ml" in - try - (* Add the pre-linked modules *) - output_string oc "List.iter Mltop.add_known_module [\""; - output_string oc (String.concat "\";\"" modules); - output_string oc "\"];;\n"; - (* Initializes the kind of loading *) - output_string oc (declare_loading_string()); - (* Start the toplevel loop *) - if not !no_start then output_string oc "Coqtop.start();;\n"; - close_out oc; - main_name - with reraise -> - clean main_name; raise reraise - -(* TODO: remove once OCaml 4.04 is adopted *) -let split_on_char sep s = - let r = ref [] in - let j = ref (String.length s) in - for i = String.length s - 1 downto 0 do - if s.[i] = sep then begin - r := String.sub s (i + 1) (!j - i - 1) :: !r; - j := i - end - done; - String.sub s 0 !j :: !r - -(** {6 Main } *) - -let main () = - let (options, userfiles) = parse_args () in - (* Directories: *) - let () = Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)) in - let basedir = if !Flags.boot then None else Some (Envars.coqlib ()) in - (* Which ocaml compiler to invoke *) - let prog = if !opt then "opt" else "ocamlc" in - (* Which arguments ? *) - if !opt && !top then failwith "no custom toplevel in native code!"; - let flags = if !opt then Coq_config.flambda_flags else Coq_config.vmbyteflags in - let topstart = if !top then [ "topstart.cmo" ] else [] in - let (modules, tolink) = files_to_link userfiles in - let main_file = create_tmp_main_file modules in - try - (* - We add topstart.cmo explicitly because we shunted ocamlmktop wrapper. - - With the coq .cma, we MUST use the -linkall option. *) - let coq_camlflags = - List.filter ((<>) "") (split_on_char ' ' Coq_config.caml_flags) in - let args = - coq_camlflags @ "-linkall" :: "-w" :: "-31" :: flags @ copts @ options @ - (std_includes basedir) @ tolink @ [ main_file ] @ topstart - in - if !echo then begin - let command = String.concat " " (Envars.ocamlfind ()::prog::args) in - print_endline command; - print_endline - ("(command length is " ^ - (string_of_int (String.length command)) ^ " characters)"); - flush Pervasives.stdout - end; - let exitcode = run_command (Envars.ocamlfind ()) (prog::args) in - clean main_file; - exitcode - with reraise -> clean main_file; raise reraise - -let pr_exn = function - | Failure msg -> msg - | Unix.Unix_error (err,fn,arg) -> fn^" "^arg^" : "^Unix.error_message err - | any -> Printexc.to_string any - -let _ = - try exit (main ()) - with any -> Printf.eprintf "Error: %s\n" (pr_exn any); exit 1 diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 6048dae3b..2fa9f0ab4 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -756,7 +756,7 @@ let init_toplevel arglist = (* Coq's init process, phase 1: - OCaml parameters, and basic structures and IO *) - Profile.init_profile (); + CProfile.init_profile (); init_gc (); Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) let init_feeder = Feedback.add_feeder coqtop_init_feed in @@ -846,7 +846,5 @@ let start () = let sigma, env = Pfedit.get_current_context () in Feedback.msg_notice (Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ()) end; - Profile.print_profile (); + CProfile.print_profile (); exit 0 - -(* [Coqtop.start] will be called by the code produced by coqmktop *) diff --git a/toplevel/coqtop_bin.ml b/toplevel/coqtop_bin.ml new file mode 100644 index 000000000..56aced92a --- /dev/null +++ b/toplevel/coqtop_bin.ml @@ -0,0 +1,2 @@ +(* Main coqtop initialization *) +let () = Coqtop.start() diff --git a/toplevel/coqtop_byte_bin.ml b/toplevel/coqtop_byte_bin.ml new file mode 100644 index 000000000..7d8354ec3 --- /dev/null +++ b/toplevel/coqtop_byte_bin.ml @@ -0,0 +1,21 @@ +let drop_setup () = + begin try + (* Enable rectypes in the toplevel if it has the directive #rectypes *) + begin match Hashtbl.find Toploop.directive_table "rectypes" with + | Toploop.Directive_none f -> 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); + }) + +let _ = drop_setup () diff --git a/toplevel/coqtop_opt_bin.ml b/toplevel/coqtop_opt_bin.ml new file mode 100644 index 000000000..410b4679a --- /dev/null +++ b/toplevel/coqtop_opt_bin.ml @@ -0,0 +1,3 @@ +let drop_setup () = Mltop.remove () + +let _ = drop_setup () |