Revert "Merge remote-tracking branch 'github/pr/229' into trunk"

This reverts commit b2f8f9e, reversing
changes made to da99355.

Hugo asked for more discussion on this topic, and it was not in the roadmap. I
merged it prematurely because I thought there was a consensus. Also, I missed
that it was changing coq_makefile. Sorry about that.

INSTALL

@@ -55,6 +55,8 @@ QUICK INSTALLATION PROCEDURE.
 1. ./configure
 2. make
 3. make install (you may need superuser rights)
+4. make clean
+
 
 INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
 =================================================
@@ -130,13 +132,10 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
 
 	make
 
-   to compile Coq in the best OCaml mode available (native-code if supported,
-   bytecode otherwise).
+   to compile Coq in Objective Caml bytecode (and native-code if supported).
 
    This will compile the entire system. This phase can take more or less time,
-   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.
+   depending on your architecture and is fairly verbose.
 
 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
@@ -152,19 +151,7 @@ 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- 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.)
+7- You can now clean all the sources. (You can even erase them.)
 
 	make clean
 
@@ -202,14 +189,11 @@ THE AVAILABLE COMMANDS.
 	coqtop		The Coq toplevel
 	coqc		The Coq compiler
 
-   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.
+   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.
 
     * `coqtop' launches Coq in the interactive mode. By default it loads
       basic logical definitions and tactics from the Init directory.

Makefile

@@ -109,17 +109,14 @@ 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

Makefile.build

@@ -17,16 +17,9 @@
 
 world: coq coqide documentation revision
 
-coq: coqlib coqbinaries tools
+coq: coqlib coqbinaries tools printers
 
-# 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
+.PHONY: world coq
 
 ###########################################################################
 # Includes
@@ -91,7 +84,7 @@ STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)"
 TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 
 COQOPTS=$(COQ_XML) $(NATIVECOMPUTE)
-BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile
+BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile
 
 # The SHOW and HIDE variables control whether make will echo complete commands 
 # or only abbreviated versions. 
@@ -181,7 +174,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 := $(COQTOPBEST)
+VO_TOOLS_DEP := $(COQTOPEXE)
 ifdef COQ_XML
  VO_TOOLS_DEP += $(COQDOC)
 endif
@@ -320,11 +313,11 @@ grammar/%.cmi: grammar/%.mli
 # Main targets (coqmktop, coqtop.opt, coqtop.byte)
 ###########################################################################
 
-.PHONY: coqbinaries coqbyte
+.PHONY: coqbinaries
 
-coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE)
+coqbinaries: $(COQMKTOP) $(COQTOPEXE) $(COQTOPBYTE) \
+ $(CHICKEN) $(CHICKENBYTE) $(CSDPCERT) $(FAKEIDE)
 
-coqbyte: $(COQTOPBYTE) $(CHICKENBYTE)
 
 ifeq ($(BEST),opt)
 $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs)
@@ -510,13 +503,18 @@ 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
+%.cmx: %.mlpack %.cmo
 	$(SHOW)'OCAMLOPT -pack -o $@'
-	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^)
+	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack %.cmo, $^)
 
 COND_BYTEFLAGS= \
  $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(BYTEFLAGS)
@@ -532,6 +530,27 @@ 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:
@@ -542,11 +561,11 @@ plugins/micromega/csdpcert_FORPACK:=
 
 plugins/%.cmx: plugins/%.ml
 	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $($(@:.cmx=_FORPACK)) -c $<
+	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $<
 
 %.cmx: %.ml
 	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) -c $<
+	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) -c $<
 
 %.cmxs: %.cmx
 	$(SHOW)'OCAMLOPT -shared -o $@'
@@ -631,7 +650,7 @@ endif
 
 %.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES)
 	$(SHOW)'COQDEP    $<'
-	$(HIDE)$(COQDEPBOOT) -boot $(DYNDEP) "$<" $(TOTARGET)
+	$(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET)
 
 ###########################################################################
 

Makefile.checker

@@ -71,7 +71,7 @@ checker/%.cmo: checker/%.ml
 
 checker/%.cmx: checker/%.ml
 	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -c $<
+	$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) $(HACKMLI) -c $<
 
 md5chk:
 	$(SHOW)'MD5SUM cic.mli'

Makefile.common

@@ -41,26 +41,10 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE)
 # Object and Source files
 ###########################################################################
 
-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
+ifeq ($(HASNATDYNLINK)-$(BEST),true-opt)
+  DEPNATDYN:=
 else
-COQTOPBEST:=$(COQTOPBYTE)
-DYNOBJ:=.cmo
-DYNLIB:=.cma
+  DEPNATDYN:=-natdynlink no
 endif
 
 INSTALLBIN:=install

Makefile.ide

@@ -61,30 +61,23 @@ GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0)
 # CoqIde special targets
 ###########################################################################
 
-.PHONY: coqide coqide-opt coqide-byte coqide-files
-.PHONY: ide-toploop ide-byteloop ide-optloop
+.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files
+.PHONY: ide-toploop
 
 # target to build CoqIde
-coqide: coqide-files coqide-opt theories/Init/Prelude.vo
+coqide: coqide-files coqide-binaries theories/Init/Prelude.vo
 
-ifeq ($(HASCOQIDE),opt)
-coqide-opt: $(COQIDE) ide-toploop
-else
-coqide-opt: ide-toploop
-endif
-
-ifeq ($(HASCOQIDE),no)
-coqide-byte: ide-byteloop
+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)
 else
-coqide-byte: $(COQIDEBYTE) ide-byteloop
+ide-toploop: $(IDETOPLOOPCMA)
 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 $@'
@@ -116,41 +109,35 @@ ide/%.cmo: ide/%.ml
 
 ide/%.cmx: ide/%.ml
 	$(SHOW)'OCAMLOPT  $<'
-	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $<
+	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) $(HACKMLI) -c $<
 
 
 ####################
 ## Install targets
 ####################
 
-.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles install-ide-byte
+.PHONY: install-coqide install-ide-bin install-ide-toploop install-ide-files install-ide-info install-ide-devfiles
 
 ifeq ($(HASCOQIDE),no)
 install-coqide: install-ide-toploop
 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) \
+	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA) \
 	  $(foreach lib,$(IDECMA:.cma=_MLLIB_DEPENDENCIES),$(addsuffix .cmi,$($(lib))))
 ifeq ($(BEST),opt)
 	$(INSTALLSH) $(FULLCOQLIB) $(IDECMA:.cma=.cmxa) $(IDECMA:.cma=.a)

Makefile.install

@@ -61,26 +61,15 @@ 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) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR)
+	$(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(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)
@@ -104,16 +93,19 @@ install-devfiles:
 	$(MKDIR) $(FULLBINDIR)
 	$(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR)
 	$(MKDIR) $(FULLCOQLIB)
-	$(INSTALLSH)  $(FULLCOQLIB) $(GRAMMARCMA)
+	$(INSTALLSH)  $(FULLCOQLIB) $(LINKCMO) $(GRAMMARCMA)
 	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMI)
 ifeq ($(BEST),opt)
 	$(INSTALLSH)  $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a)
 endif
 
 install-library:
 	$(MKDIR) $(FULLCOQLIB)
-	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES)
+	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS)
 	$(MKDIR) $(FULLCOQLIB)/user-contrib
+ifndef CUSTOM
+	$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
+endif
 ifeq ($(BEST),opt)
 	$(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)
 	$(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT)