diff options
| -rw-r--r-- | CHANGES | 9 | ||||
| -rw-r--r-- | INSTALL | 36 | ||||
| -rw-r--r-- | Makefile | 9 | ||||
| -rw-r--r-- | Makefile.build | 57 | ||||
| -rw-r--r-- | Makefile.checker | 2 | ||||
| -rw-r--r-- | Makefile.common | 22 | ||||
| -rw-r--r-- | Makefile.ide | 45 | ||||
| -rw-r--r-- | Makefile.install | 19 | ||||
| -rw-r--r-- | plugins/micromega/sos_types.mli | 40 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/coqdoc1/run.sh | 2 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/coqdoc2/run.sh | 2 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/mlpack1/run.sh | 2 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/mlpack2/run.sh | 2 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/multiroot/run.sh | 3 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/native1/run.sh | 2 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/plugin1/run.sh | 3 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/plugin2/run.sh | 3 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/plugin3/run.sh | 3 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 37 | ||||
| -rw-r--r-- | tools/coqdep.ml | 24 | ||||
| -rw-r--r-- | tools/coqdep_boot.ml | 6 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 20 | ||||
| -rw-r--r-- | tools/coqdep_common.mli | 5 | ||||
| -rw-r--r-- | tools/coqdoc/cdglobals.mli | 49 |
24 files changed, 287 insertions, 115 deletions
@@ -81,6 +81,15 @@ Tools warnings when a deprecated feature is used. Please upgrade your _CoqProject accordingly. +Build Infrastructure + +- Note that 'make world' does not build the bytecode binaries anymore. + For that, you can use 'make byte' (and 'make install-byte' afterwards). + Warning: native and byte compilations should *not* be mixed in the same + instance of 'make -j', otherwise both ocamlc and ocamlopt might race for + access to the same .cmi files. In short, use "make -j && make -j byte" + instead of "make -j world byte". + Changes from V8.6beta1 to V8.6 ============================== @@ -55,8 +55,6 @@ QUICK INSTALLATION PROCEDURE. 1. ./configure 2. make 3. make install (you may need superuser rights) -4. make clean - INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). ================================================= @@ -131,10 +129,13 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). make - to compile Coq in Objective Caml bytecode (and native-code if supported). + to compile Coq in the best OCaml mode available (native-code if supported, + bytecode otherwise). This will compile the entire system. This phase can take more or less time, - depending on your architecture and is fairly verbose. + depending on your architecture and is fairly verbose. On a multi-core machine, + it is recommended to compile in parallel, via make -jN where N is your number + of cores. 6- You can now install the Coq system. Executables, libraries, manual pages and emacs mode are copied in some standard places of your system, defined at @@ -150,7 +151,19 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) -7- You can now clean all the sources. (You can even erase them.) +7- Optionally, you could build the bytecode version of Coq via: + + make byte + + and install it via + + make install-byte + + This version is quite slower than the native code version of Coq, but could + be helpful for debugging purposes. In particular, coqtop.byte embeds an OCaml + toplevel accessible via the Drop command. + +8- You can now clean all the sources. (You can even erase them.) make clean @@ -182,11 +195,14 @@ THE AVAILABLE COMMANDS. coqtop The Coq toplevel coqc The Coq compiler - Under architecture where ocamlopt is available, there are actually two - binaries for the interactive system, coqtop.byte and coqtop (respectively - bytecode and native code versions of Coq). coqtop is a link to coqtop.byte - otherwise. coqc also invokes the fastest version of Coq. Options -opt and - -byte to coqtop and coqc selects a particular binary. + Under architecture where ocamlopt is available, coqtop is the native code + version of Coq. On such architecture, you could additionally request + the build of the bytecode version of Coq via 'make byte' and install it via + 'make install-byte'. This will create an extra binary named coqtop.byte, + that could be used for debugging purpose. If native code isn't available, + coqtop.byte is directly built by 'make', and coqtop is a link to coqtop.byte. + coqc also invokes the fastest version of Coq. Options -opt and -byte to coqtop + and coqc selects a particular binary. * `coqtop' launches Coq in the interactive mode. By default it loads basic logical definitions and tactics from the Init directory. @@ -116,16 +116,19 @@ NOARG: world .PHONY: NOARG help noconfig submake help: - @echo "Please use either" + @echo "Please use either:" @echo " ./configure" @echo " make world" @echo " make install" @echo " make clean" @echo "or make archclean" - @echo @echo "For make to be verbose, add VERBOSE=1" + @echo "If you want camlp5 to generate human-readable files, add READABLE_ML4=1" @echo - @echo "If you want camlp{4,5} to generate human-readable files, add READABLE_ML4=1" + @echo "Bytecode compilation is now a separate target:" + @echo " make byte" + @echo " make install-byte" + @echo "Please do not mix bytecode and native targets in the same make -j" UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.ml?') ifdef UNSAVED_FILES diff --git a/Makefile.build b/Makefile.build index 05bc7afdd..2b0ef7aac 100644 --- a/Makefile.build +++ b/Makefile.build @@ -51,9 +51,16 @@ COQ_XML ?= world: coq coqide documentation revision -coq: coqlib coqbinaries tools printers +coq: coqlib coqbinaries tools -.PHONY: world coq +# Note: 'world' does not build the bytecode binaries anymore. +# For that, you can use the 'byte' rule. Native and byte compilations +# shouldn't be done in a same make -j... run, otherwise both ocamlc and +# ocamlopt might race for access to the same .cmi files. + +byte: coqbyte coqide-byte pluginsbyte printers + +.PHONY: world coq byte ########################################################################### # Includes @@ -126,7 +133,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) # TIME="%C (%U user, %S sys, %e total, %M maxres)" COQOPTS=$(COQ_XML) $(NATIVECOMPUTE) -BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile +BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile LOCALINCLUDES=$(if $(filter plugins/%,$<),-I lib -I API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS))) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) @@ -208,7 +215,7 @@ ifndef ORDER_ONLY_SEP $(error This Makefile needs GNU Make 3.81 or later (that is a version that supports the order-only dependency feature without major bugs.)) endif -VO_TOOLS_DEP := $(COQTOPEXE) +VO_TOOLS_DEP := $(COQTOPBEST) ifdef COQ_XML VO_TOOLS_DEP += $(COQDOC) endif @@ -315,11 +322,11 @@ grammar/%.cmi: grammar/%.mli # Main targets (coqmktop, coqtop.opt, coqtop.byte) ########################################################################### -.PHONY: coqbinaries +.PHONY: coqbinaries coqbyte -coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(COQTOPBYTE) \ - $(CHICKEN) $(CHICKENBYTE) $(CSDPCERT) $(FAKEIDE) +coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) +coqbyte: $(COQTOPBYTE) $(CHICKENBYTE) ifeq ($(BEST),opt) $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) @@ -510,18 +517,13 @@ kernel/kernel.cma: kernel/kernel.mllib # For plugin packs -# Note: both ocamlc -pack and ocamlopt -pack will create the same .cmi, and there's -# apparently no way to avoid that (no -intf-suffix hack as below). -# We at least ensure that these two commands won't run at the same time, by a fake -# dependency from the packed .cmx to the packed .cmo. - %.cmo: %.mlpack $(SHOW)'OCAMLC -pack -o $@' $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -pack -o $@ $(filter-out %.mlpack, $^) -%.cmx: %.mlpack %.cmo +%.cmx: %.mlpack $(SHOW)'OCAMLOPT -pack -o $@' - $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack %.cmo, $^) + $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^) COND_BYTEFLAGS= \ $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(BYTEFLAGS) @@ -537,27 +539,6 @@ COND_OPTFLAGS= \ $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $< -## NB: for the moment ocamlopt erases and recreates .cmi if there's no .mli around. -## This can lead to nasty things with make -j. To avoid that: -## 1) We make .cmx always depend on .cmi -## 2) This .cmi will be created from the .mli, or trigger the compilation of the -## .cmo if there's no .mli (see rule below about MLWITHOUTMLI) -## 3) We tell ocamlopt to use the .cmi as the interface source file. With this -## hack, everything goes as if there is a .mli, and the .cmi is preserved -## and the .cmx is checked with respect to this .cmi - -HACKMLI = $(if $(wildcard $<i),,-intf-suffix .cmi) - -define diff - $(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f))) -endef - -MLWITHOUTMLI := $(call diff, $(MLFILES), $(MLIFILES:.mli=.ml)) - -$(MLWITHOUTMLI:.ml=.cmx): %.cmx: %.cmi # for .ml with .mli this is already the case - -$(MLWITHOUTMLI:.ml=.cmi): %.cmi: %.cmo - # NB: the *_FORPACK variables are generated in *.mlpack.d by ocamllibdep # The only exceptions are the sources of the csdpcert binary. # To avoid warnings, we set them manually here: @@ -568,11 +549,11 @@ plugins/micromega/csdpcert_FORPACK:= plugins/%.cmx: plugins/%.ml $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $< + $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $($(@:.cmx=_FORPACK)) -c $< %.cmx: %.ml $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) -c $< + $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) -c $< %.cmxs: %.cmx $(SHOW)'OCAMLOPT -shared -o $@' @@ -657,7 +638,7 @@ endif %.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES) $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET) + $(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) "$<" $(TOTARGET) ########################################################################### diff --git a/Makefile.checker b/Makefile.checker index 3ea0baced..435d8e8f6 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -71,7 +71,7 @@ checker/%.cmo: checker/%.ml checker/%.cmx: checker/%.ml $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) $(HACKMLI) -c $< + $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -c $< md5chk: $(SHOW)'MD5SUM cic.mli' diff --git a/Makefile.common b/Makefile.common index 62bbbc4fd..b2e1d47df 100644 --- a/Makefile.common +++ b/Makefile.common @@ -41,10 +41,26 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE) # Object and Source files ########################################################################### -ifeq ($(HASNATDYNLINK)-$(BEST),true-opt) - DEPNATDYN:= +ifeq ($(HASNATDYNLINK)-$(BEST),false-opt) + # static link of plugins, do not mention them in .v.d + DYNDEP:=-dyndep no +else + DYNDEP:=-dyndep var +endif + +# Which coqtop do we use to build .vo file ? The best ;-) +# Note: $(BEST) could be overridden by the user if a byte build is desired +# Note: coqdep -dyndep var will use $(DYNOBJ) and $(DYNLIB) extensions +# for Declare ML Module files. + +ifeq ($(BEST),opt) +COQTOPBEST:=$(COQTOPEXE) +DYNOBJ:=.cmxs +DYNLIB:=.cmxs else - DEPNATDYN:=-natdynlink no +COQTOPBEST:=$(COQTOPBYTE) +DYNOBJ:=.cmo +DYNLIB:=.cma endif INSTALLBIN:=install diff --git a/Makefile.ide b/Makefile.ide index 48a269ab7..0cfbdeb4e 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -61,23 +61,30 @@ GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0) # CoqIde special targets ########################################################################### -.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files -.PHONY: ide-toploop +.PHONY: coqide coqide-opt coqide-byte coqide-files +.PHONY: ide-toploop ide-byteloop ide-optloop # target to build CoqIde -coqide: coqide-files coqide-binaries theories/Init/Prelude.vo +coqide: coqide-files coqide-opt theories/Init/Prelude.vo -coqide-binaries: coqide-$(HASCOQIDE) ide-toploop -coqide-no: -coqide-byte: $(COQIDEBYTE) $(COQIDE) -coqide-opt: $(COQIDEBYTE) $(COQIDE) -coqide-files: $(IDEFILES) -ifeq ($(BEST),opt) -ide-toploop: $(IDETOPLOOPCMA) $(IDETOPLOOPCMA:.cma=.cmxs) +ifeq ($(HASCOQIDE),opt) +coqide-opt: $(COQIDE) ide-toploop else -ide-toploop: $(IDETOPLOOPCMA) +coqide-opt: ide-toploop endif +ifeq ($(HASCOQIDE),no) +coqide-byte: ide-byteloop +else +coqide-byte: $(COQIDEBYTE) ide-byteloop +endif + +coqide-files: $(IDEFILES) + +ide-byteloop: $(IDETOPLOOPCMA) +ide-optloop: $(IDETOPLOOPCMA:.cma=.cmxs) +ide-toploop: ide-$(BEST)loop + ifeq ($(HASCOQIDE),opt) $(COQIDE): $(LINKIDEOPT) $(SHOW)'OCAMLOPT -o $@' @@ -109,14 +116,14 @@ ide/%.cmo: ide/%.ml ide/%.cmx: ide/%.ml $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(HACKMLI) -c $< + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $< #################### ## Install targets #################### -.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles +.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles install-ide-byte ifeq ($(HASCOQIDE),no) install-coqide: install-ide-toploop @@ -124,20 +131,26 @@ else install-coqide: install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles endif +# Apparently, coqide.byte is not meant to be installed + +install-ide-byte: + $(MKDIR) $(FULLCOQLIB) + $(INSTALLSH) $(FULLCOQLIB) $(IDECMA) + $(MKDIR) $(FULLCOQLIB)/toploop + $(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/ + install-ide-bin: $(MKDIR) $(FULLBINDIR) $(INSTALLBIN) $(COQIDE) $(FULLBINDIR) install-ide-toploop: - $(MKDIR) $(FULLCOQLIB)/toploop - $(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/ ifeq ($(BEST),opt) $(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ endif install-ide-devfiles: $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \ + $(INSTALLSH) $(FULLCOQLIB) \ $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib)))) ifeq ($(BEST),opt) $(INSTALLSH) $(FULLCOQLIB) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a) diff --git a/Makefile.install b/Makefile.install index 33f881c11..4a3227620 100644 --- a/Makefile.install +++ b/Makefile.install @@ -62,15 +62,26 @@ endif install-coq: install-binaries install-library install-coq-info install-devfiles +ifeq ($(BEST),byte) +install-coq: install-byte +endif + install-binaries: install-tools $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR) + $(INSTALLBIN) $(COQC) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR) $(MKDIR) $(FULLCOQLIB)/toploop - $(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/ ifeq ($(BEST),opt) $(INSTALLBIN) $(TOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ endif +install-byte: install-ide-byte + $(MKDIR) $(FULLBINDIR) + $(INSTALLBIN) $(COQTOPBYTE) $(FULLBINDIR) + $(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/ + $(INSTALLSH) $(FULLCOQLIB) $(LINKCMO) $(PLUGINS) +ifndef CUSTOM + $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) +endif install-tools: $(MKDIR) $(FULLBINDIR) @@ -94,7 +105,7 @@ install-devfiles: $(MKDIR) $(FULLBINDIR) $(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR) $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(LINKCMO) $(GRAMMARCMA) + $(INSTALLSH) $(FULLCOQLIB) $(GRAMMARCMA) $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI) $(INSTALLSH) $(FULLCOQLIB) tools/CoqMakefile.in ifeq ($(BEST),opt) @@ -103,7 +114,7 @@ endif install-library: $(MKDIR) $(FULLCOQLIB) - $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) + $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(MKDIR) $(FULLCOQLIB)/user-contrib $(MKDIR) $(FULLCOQLIB)/kernel/byterun ifndef CUSTOM diff --git a/plugins/micromega/sos_types.mli b/plugins/micromega/sos_types.mli new file mode 100644 index 000000000..57c4e50ca --- /dev/null +++ b/plugins/micromega/sos_types.mli @@ -0,0 +1,40 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* The type of positivstellensatz -- used to communicate with sos *) + +type vname = string;; + +type term = +| Zero +| Const of Num.num +| Var of vname +| Inv of term +| Opp of term +| Add of (term * term) +| Sub of (term * term) +| Mul of (term * term) +| Div of (term * term) +| Pow of (term * int);; + +val output_term : out_channel -> term -> unit + +type positivstellensatz = + Axiom_eq of int + | Axiom_le of int + | Axiom_lt of int + | Rational_eq of Num.num + | Rational_le of Num.num + | Rational_lt of Num.num + | Square of term + | Monoid of int list + | Eqmul of term * positivstellensatz + | Sum of positivstellensatz * positivstellensatz + | Product of positivstellensatz * positivstellensatz;; + +val output_psatz : out_channel -> positivstellensatz -> unit diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index d6bb52bb4..e8291c89d 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -15,9 +15,7 @@ make install-doc DSTROOT="$PWD/tmp" sort -u > desired <<EOT . ./test -./test/test_plugin.cma ./test/test_plugin.cmi -./test/test_plugin.cmo ./test/test_plugin.cmx ./test/test_plugin.cmxs ./test/test.glob diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh index d6bb52bb4..e8291c89d 100755 --- a/test-suite/coq-makefile/coqdoc2/run.sh +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -15,9 +15,7 @@ make install-doc DSTROOT="$PWD/tmp" sort -u > desired <<EOT . ./test -./test/test_plugin.cma ./test/test_plugin.cmi -./test/test_plugin.cmo ./test/test_plugin.cmx ./test/test_plugin.cmxs ./test/test.glob diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index f6fb3bcb4..10a200dde 100755 --- a/test-suite/coq-makefile/mlpack1/run.sh +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -15,9 +15,7 @@ sort > desired <<EOT . ./test ./test/test.glob -./test/test_plugin.cma ./test/test_plugin.cmi -./test/test_plugin.cmo ./test/test_plugin.cmx ./test/test_plugin.cmxs ./test/test.v diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh index f6fb3bcb4..10a200dde 100755 --- a/test-suite/coq-makefile/mlpack2/run.sh +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -15,9 +15,7 @@ sort > desired <<EOT . ./test ./test/test.glob -./test/test_plugin.cma ./test/test_plugin.cmi -./test/test_plugin.cmo ./test/test_plugin.cmx ./test/test_plugin.cmxs ./test/test.v diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh index 863c39f50..3cd1ac305 100755 --- a/test-suite/coq-makefile/multiroot/run.sh +++ b/test-suite/coq-makefile/multiroot/run.sh @@ -19,12 +19,9 @@ sort > desired <<EOT ./test ./test/test.glob ./test/test.cmi -./test/test.cmo ./test/test.cmx ./test/test_aux.cmi -./test/test_aux.cmo ./test/test_aux.cmx -./test/test_plugin.cma ./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index f07966263..9f6295d64 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -18,9 +18,7 @@ sort > desired <<EOT . ./test ./test/test.glob -./test/test_plugin.cma ./test/test_plugin.cmi -./test/test_plugin.cmo ./test/test_plugin.cmx ./test/test_plugin.cmxs ./test/test.v diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh index 24ef8c891..c2d47166f 100755 --- a/test-suite/coq-makefile/plugin1/run.sh +++ b/test-suite/coq-makefile/plugin1/run.sh @@ -17,12 +17,9 @@ sort > desired <<EOT ./test ./test/test.glob ./test/test.cmi -./test/test.cmo ./test/test.cmx ./test/test_aux.cmi -./test/test_aux.cmo ./test/test_aux.cmx -./test/test_plugin.cma ./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh index 24ef8c891..c2d47166f 100755 --- a/test-suite/coq-makefile/plugin2/run.sh +++ b/test-suite/coq-makefile/plugin2/run.sh @@ -17,12 +17,9 @@ sort > desired <<EOT ./test ./test/test.glob ./test/test.cmi -./test/test.cmo ./test/test.cmx ./test/test_aux.cmi -./test/test_aux.cmo ./test/test_aux.cmx -./test/test_plugin.cma ./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh index 24ef8c891..c2d47166f 100755 --- a/test-suite/coq-makefile/plugin3/run.sh +++ b/test-suite/coq-makefile/plugin3/run.sh @@ -17,12 +17,9 @@ sort > desired <<EOT ./test ./test/test.glob ./test/test.cmi -./test/test.cmo ./test/test.cmx ./test/test_aux.cmi -./test/test_aux.cmo ./test/test_aux.cmx -./test/test_plugin.cma ./test/test_plugin.cmxa ./test/test_plugin.cmxs ./test/test.v diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index c25ad1f37..5e223a0b4 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -115,6 +115,17 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) OPT?= +# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d +ifeq '$(OPT)' '-byte' +USEBYTE:=true +DYNOBJ:=.cmo +DYNLIB:=.cma +else +USEBYTE:= +DYNOBJ:=.cmxs +DYNLIB:=.cmxs +endif + COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) COQCHKFLAGS?=-silent -o $(COQLIBS) COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML) @@ -213,7 +224,6 @@ CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES)) OBJFILES = $(call vo_to_obj,$(VOFILES)) ALLNATIVEFILES = \ $(OBJFILES:.o=.cmi) \ - $(OBJFILES:.o=.cmo) \ $(OBJFILES:.o=.cmx) \ $(OBJFILES:.o=.cmxs) # trick: wildcard filters out non-existing files @@ -223,8 +233,9 @@ FILESTOINSTALL = \ $(VFILES) \ $(GLOBFILES) \ $(NATIVEFILESTOINSTALL) \ + $(CMIFILESTOINSTALL) +BYTEFILESTOINSTALL = \ $(CMOFILESTOINSTALL) \ - $(CMIFILESTOINSTALL) \ $(CMAFILES) ifeq '$(HASNATDYNLINK)' 'true' DO_NATDYNLINK = yes @@ -256,9 +267,15 @@ post-all:: @# Extension point .PHONY: post-all -real-all: $(VOFILES) $(CMOFILES) $(CMAFILES) $(if $(DO_NATDYNLINK),$(CMXSFILES)) +real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) .PHONY: real-all +bytefiles: $(CMOFILES) $(CMAFILES) +.PHONY: bytefiles + +optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) +.PHONY: optfiles + # FIXME, see Ralph's bugreport quick: $(VOFILES:.vo=.vio) .PHONY: quick @@ -350,6 +367,18 @@ install-extra:: @# Extension point .PHONY: install install-extra +install-byte: + $(HIDE)for f in $(BYTEFILESTOINSTALL); do\ + df="`$(COQMF_MAKEFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ -z "$$df" ]; then\ + echo SKIP "$$f" since it has no logical path;\ + else\ + install -d "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \ + install -m 0644 "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df"; \ + echo INSTALL "$$f" "$(DESTDIR)$(COQLIBINSTALL)/$$df";\ + fi;\ + done + install-doc:: html mlihtml @# Extension point $(HIDE)install -d "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" @@ -561,7 +590,7 @@ $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack $(addsuffix .d,$(VFILES)): %.v.d: %.v $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(COQLIBS) -c "$<" $(redir_if_ok) + $(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c "$<" $(redir_if_ok) # Misc ######################################################################## diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 044399544..cba9c3eb0 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -320,19 +320,25 @@ let treat_coq_file chan = List.fold_left (fun accu v -> mark_v_done from accu v) acc strl | Declare sl -> let declare suff dir s = - let base = file_name s dir in - let opt = if !option_natdynlk then " " ^ base ^ ".cmxs" else "" in - (escape base, suff ^ opt) + let base = escape (file_name s dir) in + match !option_dynlink with + | No -> [] + | Byte -> [base,suff] + | Opt -> [base,".cmxs"] + | Both -> [base,suff; base,".cmxs"] + | Variable -> + if suff=".cmo" then [base,"$(DYNOBJ)"] + else [base,"$(DYNLIB)"] in let decl acc str = let s = basename_noext str in if not (StrSet.mem s !deja_vu_ml) then let () = deja_vu_ml := StrSet.add s !deja_vu_ml in match search_mllib_known s with - | Some mldir -> (declare ".cma" mldir s) :: acc + | Some mldir -> (declare ".cma" mldir s) @ acc | None -> match search_ml_known s with - | Some mldir -> (declare ".cmo" mldir s) :: acc + | Some mldir -> (declare ".cmo" mldir s) @ acc | None -> acc else acc in @@ -449,6 +455,7 @@ let usage () = eprintf " -coqlib dir : set the coq standard library directory\n"; eprintf " -suffix s : \n"; eprintf " -slash : deprecated, no effect\n"; + eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed"; exit 1 let split_period = Str.split (Str.regexp (Str.quote ".")) @@ -476,17 +483,22 @@ let rec parse = function | "-slash" :: ll -> Printf.eprintf "warning: option -slash has no effect and is deprecated.\n"; parse ll + | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll + | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll + | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll + | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll + | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll | ("-h"|"--help"|"-help") :: _ -> usage () | f :: ll -> treat_file None f; parse ll | [] -> () let coqdep () = if Array.length Sys.argv < 2 then usage (); + if not Coq_config.has_natdynlink then option_dynlink := No; parse (List.tl (Array.to_list Sys.argv)); (* Add current dir with empty logical path if not set by options above. *) (try ignore (Coqdep_common.find_dir_logpath (Sys.getcwd())) with Not_found -> add_norec_dir_import add_known "." []); - if not Coq_config.has_natdynlink then option_natdynlk := false; (* NOTE: These directories are searched from last to first *) if !option_boot then begin add_rec_dir_import add_known "theories" ["Coq"]; diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index 6fc826833..25f62d2be 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -16,7 +16,11 @@ open Coqdep_common *) let rec parse = function - | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll + | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll + | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll + | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll + | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll + | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll | "-c" :: ll -> option_c := true; parse ll | "-boot" :: ll -> parse ll (* We're already in boot mode by default *) | "-mldep" :: ocamldep :: ll -> diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index f5e93527c..bf8bcd0c4 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -15,7 +15,7 @@ open Minisys behavior is the one of [coqdep -boot]. Its only dependencies are [Coqdep_lexer], [Unix] and [Minisys], and it should stay so. If it need someday some additional information, pass it via - options (see for instance [option_natdynlk] below). + options (see for instance [option_dynlink] below). *) module StrSet = Set.Make(String) @@ -26,9 +26,11 @@ module StrListMap = Map.Make(StrList) let stderr = Pervasives.stderr let stdout = Pervasives.stdout +type dynlink = Opt | Byte | Both | No | Variable + let option_c = ref false let option_noglob = ref false -let option_natdynlk = ref true +let option_dynlink = ref Both let option_boot = ref false let option_mldep = ref None @@ -383,10 +385,16 @@ let rec traite_fichier_Coq suffixe verbose f = end) strl | Declare sl -> let declare suff dir s = - let base = file_name s dir in - let opt = if !option_natdynlk then " "^base^".cmxs" else "" in - printf " %s%s%s" (escape base) suff opt - in + let base = escape (file_name s dir) in + match !option_dynlink with + | No -> () + | Byte -> printf " %s%s" base suff + | Opt -> printf " %s.cmxs" base + | Both -> printf " %s%s %s.cmxs" base suff base + | Variable -> + printf " %s%s" base + (if suff=".cmo" then "$(DYNOBJ)" else "$(DYNLIB)") + in let decl str = let s = basename_noext str in if not (StrSet.mem s !deja_vu_ml) then begin diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 10da0240d..8c1787d31 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -19,7 +19,10 @@ val find_dir_logpath: string -> string list val option_c : bool ref val option_noglob : bool ref val option_boot : bool ref -val option_natdynlk : bool ref + +type dynlink = Opt | Byte | Both | No | Variable + +val option_dynlink : dynlink ref val option_mldep : string option ref val norec_dirs : StrSet.t ref val suffixe : string ref diff --git a/tools/coqdoc/cdglobals.mli b/tools/coqdoc/cdglobals.mli new file mode 100644 index 000000000..2c9b3fb8e --- /dev/null +++ b/tools/coqdoc/cdglobals.mli @@ -0,0 +1,49 @@ +type target_language = LaTeX | HTML | TeXmacs | Raw +val target_language : target_language ref +type output_t = StdOut | MultFiles | File of string +val output_dir : string ref +val out_to : output_t ref +val out_channel : out_channel ref +val ( / ) : string -> string -> string +val coqdoc_out : string -> string +val open_out_file : string -> unit +val close_out_file : unit -> unit +type glob_source_t = NoGlob | DotGlob | GlobFile of string +val glob_source : glob_source_t ref +val normalize_path : string -> string +val normalize_filename : string -> string * string +val guess_coqlib : unit -> string +val header_trailer : bool ref +val header_file : string ref +val header_file_spec : bool ref +val footer_file : string ref +val footer_file_spec : bool ref +val quiet : bool ref +val light : bool ref +val gallina : bool ref +val short : bool ref +val index : bool ref +val multi_index : bool ref +val index_name : string ref +val toc : bool ref +val page_title : string ref +val title : string ref +val externals : bool ref +val coqlib : string ref +val coqlib_path : string ref +val raw_comments : bool ref +val parse_comments : bool ref +val plain_comments : bool ref +val toc_depth : int option ref +val lib_name : string ref +val lib_subtitles : bool ref +val interpolate : bool ref +val inline_notmono : bool ref +val charset : string ref +val inputenc : string ref +val latin1 : bool ref +val utf8 : bool ref +val set_latin1 : unit -> unit +val set_utf8 : unit -> unit +type coq_module = string +type file = Vernac_file of string * coq_module | Latex_file of string |