coq-interface and coq-parser can be calls to coqtop with adequate code dynlink

 From files in contrib/interface, we create (if natdynlink is available) two
 plugins named coqinterface_plugin.{cma,cmxs} and coqparser_plugin.{cma,cmxs}.
 These plugins are loaded respectively by CoqInterface.v and CoqParser.v.
 So coq-interface can be "coqtop -require CoqInterface", and coq-parser can be
 "coqtop -batch -l CoqParser" (this one cannot be compiled into a .vo, otherwise
 a customized toplevel is launched during the compilation). Turing coq-interface
 and coq-parser and their .opt versions into shell scripts allow to spare around
 40 Mb of disk space...

 Nota: at dynlink, parse.ml was conflicting with the module Parse of the ocaml
 runtime, so I renamed it into coqparser.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11940 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 68 insertions, 13 deletions

diff --git a/Makefile.build b/Makefile.build
index 1bdc6e6b1a..c75d260d75 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -422,12 +422,8 @@ ide/%.cmx: ide/%.ml | ide/%.ml.d
 	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -c $<
 
 ide/ide.cma: $(COQIDECMO)
-	$(SHOW)'OCAMLC -a -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $^
 
 ide/ide.cmxa: $(COQIDECMO:.cmo=.cmx)
-	$(SHOW)'OCAMLOPT -a -o $@'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $^
 
 # install targets
 
@@ -459,10 +455,11 @@ install-ide-info:
 # Pcoq: special binaries for debugging (coq-interface, coq-parser)
 ###########################################################################
 
-# target to build Pcoq
-pcoq: pcoq-binaries pcoq-files
+ifeq ($(HASNATDYNLINK),false)
+
+# old approach, via coqmktop
 
-pcoq-binaries:: $(COQINTERFACE) 
+PCOQPLUGINS:=
 
 bin/coq-interface$(EXE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(INTERFACE)
 	$(SHOW)'COQMKTOP -o $@'
@@ -482,8 +479,39 @@ bin/coq-parser.opt$(EXE): $(LIBCOQRUN) $(PARSERCMX)
 	$(HIDE)$(OCAMLOPT) -linkall $(OPTFLAGS) -o $@ \
 	  $(LIBCOQRUN) $(DYNLINKCMXA) str.cmxa nums.cmxa $(CMXA) $(PARSERCMX)
 
-pcoq-files:: $(INTERFACEVO) $(INTERFACERC)
+else 
+
+# HASNATDYNLINK is available :
+# coq-interface and coq-parser are direct calls to coqtop with some dynlink
+
+PCOQPLUGINS:=contrib/interface/coqinterface_plugin.cma \
+             contrib/interface/coqparser_plugin.cma
+
+contrib/interface/coqinterface_plugin.cma: $(INTERFACE)
+contrib/interface/coqinterface_plugin.cmxa: $(INTERFACE:.cmo=.cmx)
+contrib/interface/coqparser_plugin.cma: $(PARSERCODE)
+contrib/interface/coqparser_plugin.cmxa: $(PARSERCODE:.cmo=.cmx)
+
+bin/coq-interface$(EXE):
+	echo "#!/bin/sh" > $@
+	echo "exec coqtop -require CoqInterface" >> $@
+	chmod +x $@
+
+bin/coq-parser$(EXE):
+	echo "#!/bin/sh" > $@
+	echo "exec coqtop -batch -l CoqParser" >> $@
+	chmod +x $@
+
+endif # of HASNATDYNLINK
+
+PCOQFILES:= $(INTERFACEVO) $(INTERFACERC) $(PCOQPLUGINS) $(PCOQPLUGINS:.cma=.cmxs)
+
+# target to build Pcoq
+pcoq: pcoq-binaries pcoq-files
+
+pcoq-binaries:: $(COQINTERFACE)
 
+pcoq-files:: $(PCOQFILES)
 
 # install targets
 install-pcoq:: install-pcoq-binaries install-pcoq-files install-pcoq-manpages
@@ -494,7 +522,7 @@ install-pcoq-binaries::
 
 install-pcoq-files::
 	$(MKDIR) $(FULLCOQLIB)/contrib/interface
-	$(INSTALLLIB) $(INTERFACERC) $(FULLCOQLIB)/contrib/interface
+	$(INSTALLLIB) $(PCOQFILES) $(FULLCOQLIB)/contrib/interface
 
 install-pcoq-manpages:
 	$(MKDIR) $(FULLMANDIR)/man1
diff --git a/Makefile.common b/Makefile.common
index d5fa289932..920df2d2b5 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -418,18 +418,23 @@ INTERFACECMX:=$(INTERFACE:.cmo=.cmx)
 PARSERREQUIRES:=$(LINKCMO) $(LIBCOQRUN) # Solution de facilité...
 PARSERREQUIRESCMX:=$(LINKCMX)
 
+COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-parser$(EXE)
 ifeq ($(BEST),opt)
-  COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE) bin/coq-parser$(EXE) bin/coq-parser.opt$(EXE)
-else
-  COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-parser$(EXE)
+ifeq ($(HASNATDYNLINK),false)
+  COQINTERFACE:=$(COQINTERFACE) bin/coq-interface.opt$(EXE) bin/coq-parser.opt$(EXE)
+endif
 endif
 
 PARSERCODE:=contrib/interface/line_parser.cmo contrib/interface/vtp.cmo \
-           contrib/interface/xlate.cmo contrib/interface/parse.cmo
+           contrib/interface/xlate.cmo contrib/interface/coqparser.cmo
 PARSERCMO:=$(PARSERREQUIRES) $(PARSERCODE)
 PARSERCMX:= $(PARSERREQUIRESCMX) $(PARSERCODE:.cmo=.cmx)
 
+ifneq ($(HASNATDYNLINK),false)
 INTERFACERC:= contrib/interface/vernacrc
+else
+INTERFACERC:= contrib/interface/vernacrc contrib/interface/CoqParser.v
+endif
 
 CSDPCERTCMO:= contrib/micromega/mutils.cmo contrib/micromega/micromega.cmo \
 	      contrib/micromega/mfourier.cmo  contrib/micromega/certificate.cmo \
@@ -868,7 +873,11 @@ LIBFILESLIGHT:=$(THEORIESLIGHTVO)
 
 ## Specials
 
+ifneq ($(HASNATDYNLINK),false)
+INTERFACEVO:=contrib/interface/CoqInterface.vo
+else
 INTERFACEVO:=
+endif
 
 
 MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
diff --git a/contrib/interface/CoqInterface.v b/contrib/interface/CoqInterface.v
new file mode 100644
index 0000000000..e86fb2fce9
--- /dev/null
+++ b/contrib/interface/CoqInterface.v
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Declare ML Module "coqinterface_plugin".
diff --git a/contrib/interface/CoqParser.v b/contrib/interface/CoqParser.v
new file mode 100644
index 0000000000..db4aa06dcc
--- /dev/null
+++ b/contrib/interface/CoqParser.v
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Declare ML Module "coqparser_plugin".
diff --git a/contrib/interface/parse.ml b/contrib/interface/coqparser.ml
index 5de6060f05..5de6060f05 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/coqparser.ml