aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--INSTALL36
-rw-r--r--Makefile7
-rw-r--r--Makefile.build57
-rw-r--r--Makefile.checker2
-rw-r--r--Makefile.common22
-rw-r--r--Makefile.ide45
-rw-r--r--Makefile.install22
-rw-r--r--plugins/micromega/sos_types.mli40
-rw-r--r--tools/coq_makefile.ml50
-rw-r--r--tools/coqdep.ml24
-rw-r--r--tools/coqdep_boot.ml6
-rw-r--r--tools/coqdep_common.ml20
-rw-r--r--tools/coqdep_common.mli5
-rw-r--r--tools/coqdoc/cdglobals.mli49
14 files changed, 280 insertions, 105 deletions
diff --git a/INSTALL b/INSTALL
index 5a300010d..56ff522dc 100644
--- a/INSTALL
+++ b/INSTALL
@@ -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).
=================================================
@@ -132,10 +130,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
@@ -151,7 +152,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
@@ -189,11 +202,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.
diff --git a/Makefile b/Makefile
index 93b89a489..db23ad0a8 100644
--- a/Makefile
+++ b/Makefile
@@ -109,14 +109,17 @@ 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 "Bytecode compilation is now a separate target:"
+ @echo " make byte"
+ @echo " make install-byte"
+ @echo "Please do 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 ebf2996f1..90834ec8c 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -17,9 +17,16 @@
world: coq coqide documentation revision
-coq: coqlib coqbinaries tools printers
+coq: coqlib coqbinaries tools
-.PHONY: world coq
+# Note: 'world' do 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
@@ -84,7 +91,7 @@ STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)"
TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
COQOPTS=$(COQ_XML) $(NATIVECOMPUTE)
-BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile
+BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile
# The SHOW and HIDE variables control whether make will echo complete commands
# or only abbreviated versions.
@@ -174,7 +181,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
@@ -313,11 +320,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)
@@ -503,18 +510,13 @@ test-suite: world $(ALLSTDLIB).v
# 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)
@@ -530,27 +532,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:
@@ -561,11 +542,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 $@'
@@ -650,7 +631,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 49fe1fd93..aacd801b5 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 4dad8cf0d..b4aad7bdd 100644
--- a/Makefile.install
+++ b/Makefile.install
@@ -61,15 +61,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)
@@ -93,7 +104,7 @@ install-devfiles:
$(MKDIR) $(FULLBINDIR)
$(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR)
$(MKDIR) $(FULLCOQLIB)
- $(INSTALLSH) $(FULLCOQLIB) $(LINKCMO) $(GRAMMARCMA)
+ $(INSTALLSH) $(FULLCOQLIB) $(GRAMMARCMA)
$(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI)
ifeq ($(BEST),opt)
$(INSTALLSH) $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a)
@@ -101,11 +112,8 @@ endif
install-library:
$(MKDIR) $(FULLCOQLIB)
- $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS)
+ $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES)
$(MKDIR) $(FULLCOQLIB)/user-contrib
-ifndef CUSTOM
- $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
-endif
ifeq ($(BEST),opt)
$(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)
$(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT)
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/tools/coq_makefile.ml b/tools/coq_makefile.ml
index c86253477..f116c5580 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -293,9 +293,8 @@ let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function
let cmxss = List.rev_append cmos mllibs in
let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxss)] inc in
let where_what_oth = vars_to_put_by_root
- [("VOFILES",vfiles);("VFILES",vfiles);
- ("GLOBFILES",vfiles);("NATIVEFILES",vfiles);
- ("CMOFILES",cmos);("CMIFILES",cmis);("CMAFILES",mllibs)]
+ [("VOFILES",vfiles);("VFILES",vfiles);("GLOBFILES",vfiles);
+ ("NATIVEFILES",vfiles);("CMIFILES",cmis)]
inc in
let doc_dir = where_put_doc inc in
if is_install = Project_file.UnspecInstall then begin
@@ -307,6 +306,12 @@ let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function
print "\n";
end;
if not_empty cmxss then begin
+ print "install-byte:\n";
+ install_include_by_root "0755"
+ (vars_to_put_by_root [("CMOFILES",cmos);("CMAFILES",mllibs)] inc);
+ print "\n";
+ end;
+ if not_empty cmxss then begin
print "install-toploop: $(MLLIBFILES:.mllib=.cmxs)\n";
printf "\t install -d \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
printf "\t install -m 0755 $? \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
@@ -506,7 +511,7 @@ let variables is_install opt (args,defs) =
end;
(* Coq executables and relative variables *)
if !some_vfile || !some_mlpackfile || !some_mllibfile then
- print "COQDEP?=\"$(COQBIN)coqdep\" -c\n";
+ print "COQDEP?=\"$(COQBIN)coqdep\" -c -dyndep var\n";
if !some_vfile then begin
print "COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n";
print "COQCHKFLAGS?=-silent -o\n";
@@ -537,7 +542,16 @@ else
CAMLP4EXTEND=
endif\n";
print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\
- $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n";
+ $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n";
+ print "ifeq '$(OPT)' '-byte'\n";
+ print "USEBYTE:=true\n";
+ print "DYNOBJ:=.cmo\n";
+ print "DYNLIB:=.cma\n";
+ print "else\n";
+ print "USEBYTE:=\n";
+ print "DYNOBJ:=.cmxs\n";
+ print "DYNLIB:=.cmxs\n";
+ print "endif\n\n";
end;
match is_install with
| Project_file.NoInstall -> ()
@@ -756,13 +770,19 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
print "HASNATDYNLINK_OR_EMPTY :=\n";
print "endif\n\n";
section "Definition of the toplevel targets.";
- print "all: ";
- if !some_vfile then print "$(VOFILES) ";
- if !some_mlfile || !some_ml4file || !some_mlpackfile then print "$(CMOFILES) ";
- if !some_mllibfile then print "$(CMAFILES) ";
- if !some_mlfile || !some_ml4file || !some_mllibfile || !some_mlpackfile
- then print "$(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) ";
+ let has_cmo = !some_mlfile || !some_ml4file || !some_mlpackfile in
+ let has_ml = has_cmo || !some_mllibfile in
+ print "all:";
+ if !some_vfile then print " $(VOFILES)";
+ if has_ml then print " $(if $(USEBYTE),bytefiles,optfiles)";
print_list "\\\n " other_targets; print "\n\n";
+ print "bytefiles:";
+ if has_cmo then print " $(CMOFILES)";
+ if !some_mllibfile then print " $(CMAFILES)";
+ print "\n\n";
+ print "optfiles:";
+ if has_ml then print " $(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES))";
+ print "\n\n";
if !some_mlifile then
begin
print "mlihtml: $(MLIFILES:.mli=.cmi)\n";
@@ -808,9 +828,11 @@ let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc =
print ".PHONY: ";
print_list
" "
- ("all" :: "archclean" :: "beautify" :: "byte" :: "clean" :: "cleanall"
- :: "gallina" :: "gallinahtml" :: "html" :: "install" :: "install-doc"
- :: "install-natdynlink" :: "install-toploop" :: "opt" :: "printenv"
+ ("all" :: "archclean" :: "beautify" :: "byte" :: "bytefiles"
+ :: "clean" :: "cleanall"
+ :: "gallina" :: "gallinahtml" :: "html" :: "install" :: "install-byte"
+ :: "install-doc" :: "install-natdynlink" :: "install-toploop"
+ :: "opt" :: "optfiles" :: "printenv"
:: "quick" :: "uninstall" :: "userinstall" :: "validate" :: "vio2vo"
:: (sds@(CList.map_filter
(fun (n,_,is_phony,_) ->
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index a7c32e1d6..991a3221f 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 cc63c13d7..8bf7fee4b 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
@@ -380,10 +382,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 633c474ad..205e99176 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 03:08:21 +0000