Remove interface plugin

It has moved to the contribs (Sophia-Antipolis/Interface).

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

Makefile

@@ -193,7 +193,6 @@ cruftclean: ml4clean
 indepclean:
 	rm -f $(GENFILES)
 	rm -f $(COQTOPBYTE) $(COQMKTOPBYTE) $(COQCBYTE) $(CHICKENBYTE)
-	rm -f bin/coq-interface$(EXE) bin/coq-parser$(EXE)
 	find . -name '*~' -o -name '*.cm[ioa]' | xargs rm -f
 	find . -name '*_mod.ml' | xargs rm -f
 	find plugins test-suite -name '*.vo' -o -name '*.glob' | xargs rm -f
@@ -224,7 +223,6 @@ docclean:
 archclean: clean-ide cleantheories
 	rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN) $(COQDEPBOOT)
 	rm -f $(COQTOPOPT) $(COQMKTOPOPT) $(COQCOPT) $(CHICKENOPT)
-	rm -f bin/coq-parser.opt$(EXE) bin/coq-interface.opt$(EXE)
 	find . -name '*.cmx' -o -name '*.cmxs' -o -name '*.cmxa' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f
 	rm -f $(TOOLS) $(CSDPCERT)
 	rm -rf _build myocamlbuild_config.ml

Makefile.build

@@ -33,16 +33,16 @@ endif
 
 NOARG: world
 
-# build and install the three subsystems: coq, coqide, pcoq
-world: revision coq coqide pcoq
-install: install-coq install-coqide install-pcoq
+# build and install the three subsystems: coq, coqide
+world: revision coq coqide
+install: install-coq install-coqide
 
 ifeq ($(WITHDOC),all)
 world: doc
 install: install-doc
 endif
 
-#install-manpages: install-coq-manpages install-pcoq-manpages
+#install-manpages: install-coq-manpages
 
 ###########################################################################
 # Compilation options
@@ -336,74 +336,6 @@ install-ide-info:
 	$(MKDIR) $(FULLIDELIB)
 	$(INSTALLLIB) ide/FAQ $(FULLIDELIB)
 
-###########################################################################
-# Pcoq: special binaries for debugging (coq-interface, coq-parser)
-###########################################################################
-
-ifeq ($(HASNATDYNLINK),false)
-
-# old approach, via coqmktop
-
-bin/coq-interface$(EXE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(INTERFACECMA)
-	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@ $(INTERFACECMA)
-
-bin/coq-interface.opt$(EXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(INTERFACECMA:.cma=.cmxa)
-	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -o $@ $(INTERFACECMA:.cma=.cmxa)
-
-bin/coq-parser$(EXE): $(PARSERREQUIRES)
-	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(COQRUNBYTEFLAGS) -linkall $(BYTEFLAGS) -o $@ \
-	  dynlink.cma str.cma nums.cma $(CMA) $(PARSERREQUIRES)
-
-bin/coq-parser.opt$(EXE): $(LIBCOQRUN) $(PARSERREQUIRESCMX)
-	$(SHOW)'OCAMLOPT -o $@'
-	$(HIDE)$(OCAMLOPT) -linkall $(OPTFLAGS) -o $@ \
-	  $(LIBCOQRUN) $(DYNLINKCMXA) str.cmxa nums.cmxa $(CMXA) \
-          $(PARSERREQUIRESCMX)
-
-else 
-
-# HASNATDYNLINK is available :
-# coq-interface and coq-parser are direct calls to coqtop with some dynlink
-
-bin/coq-interface$(EXE):
-	echo "#!/bin/bash" > $@
-	echo 'exec '$(BINDIR)'/coqtop -require CoqInterface' >> $@
-	chmod +x $@
-
-bin/coq-parser$(EXE):
-	echo "#!/bin/bash" > $@
-	echo 'exec '$(BINDIR)'/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
-
-install-pcoq-binaries::
-	$(MKDIR) $(FULLBINDIR)
-	$(INSTALLBIN) $(COQINTERFACE) $(FULLBINDIR)
-
-install-pcoq-files::
-	$(MKDIR) $(FULLCOQLIB)/plugins/interface
-	$(INSTALLLIB) $(PCOQFILES) $(FULLCOQLIB)/plugins/interface
-
-install-pcoq-manpages:
-	$(MKDIR) $(FULLMANDIR)/man1
-	$(INSTALLLIB) $(PCOQMANPAGES) $(FULLMANDIR)/man1
-
 ###########################################################################
 # tests
 ###########################################################################
@@ -473,7 +405,7 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \
 	wellfounded setoids sorting
 
 ###########################################################################
-# 3) plugins (interface not included)
+# 3) plugins
 ###########################################################################
 
 plugins: $(PLUGINSVO)

Makefile.common

@@ -67,7 +67,7 @@ SRCDIRS:=\
   ide		\
   $(addprefix plugins/, \
     omega	romega 		micromega 	quote		ring	dp \
-    setoid_ring xml 		extraction 	interface 	fourier \
+    setoid_ring xml 		extraction 	fourier \
     cc 		funind 		firstorder 	field 		subtac \
     rtauto 	groebner        syntax)
 
@@ -231,27 +231,6 @@ COQMKTOPCMX:=$(COQMKTOPCMO:.cmo=.cmx)
 COQCCMO:=$(COQENVCMO) toplevel/usage.cmo scripts/coqc.cmo
 COQCCMX:=$(COQCCMO:.cmo=.cmx)
 
-## Pcoq tools : coq-interface, coq-parser
-
-COQINTERFACE:=bin/coq-interface$(EXE) bin/coq-parser$(EXE)
-
-INTERFACECMA:=plugins/interface/coqinterface_plugin.cma
-PARSERCMA:=plugins/interface/coqparser_plugin.cma
-
-ifeq ($(HASNATDYNLINK),false)
- ifeq ($(BEST),opt)
-  COQINTERFACE:=$(COQINTERFACE) bin/coq-interface.opt$(EXE) bin/coq-parser.opt$(EXE)
- endif
- INTERFACERC:= plugins/interface/vernacrc
- PCOQPLUGINS:=
-else
- INTERFACERC:= plugins/interface/vernacrc plugins/interface/CoqParser.v
- PCOQPLUGINS:=$(INTERFACECMA) $(PARSERCMA)
-endif
-
-PARSERREQUIRES:=$(LINKCMO) $(LIBCOQRUN) $(PARSERCMA) # Solution de facilité...
-PARSERREQUIRESCMX:=$(LINKCMX) $(PARSERCMA:.cma=.cmxa)
-
 ## Misc
 
 CSDPCERTCMO:=$(addprefix plugins/micromega/, \
@@ -597,16 +576,10 @@ DPVO:=$(addprefix plugins/dp/, \
 RTAUTOVO:=$(addprefix plugins/rtauto/, \
  Bintree.vo	Rtauto.vo )
 
-ifneq ($(HASNATDYNLINK),false)
-INTERFACEVO:=plugins/interface/CoqInterface.vo
-else
-INTERFACEVO:=
-endif
-
 PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
 	    $(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \
 	    $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO) \
-            $(INTERFACEVO) $(GBVO)
+            $(GBVO)
 
 ALLVO:= $(THEORIESVO) $(PLUGINSVO)
 VFILES:= $(ALLVO:.vo=.v)
@@ -627,8 +600,6 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
 	man/coqwc.1 man/coqdoc.1 man/coqide.1 \
 	man/coq_makefile.1 man/coqmktop.1 man/coqchk.1
 
-PCOQMANPAGES:=man/coq-interface.1 man/coq-parser.1
-
 
 ###########################################################################
 # Miscellaneous
@@ -671,10 +642,10 @@ DOC_TARGET_PATTERNS:=%.dvi %.ps %.eps %.pdf %.html %.v.tex %.hva
 STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \
   interp parsing pretyping highparsing toplevel hightactics \
   coqide-binaries coqide-byte coqide-opt $(COQIDEOPT) $(COQIDEBYTE) $(COQIDE) \
-  pcoq-binaries $(COQINTERFACE) $(CSDPCERT) coqbinaries pcoq $(TOOLS) tools \
+  $(CSDPCERT) coqbinaries $(TOOLS) tools \
   printers debug initplugins plugins \
   world install coqide coqide-files coq coqlib \
-  coqlight states pcoq-files check init theories theories-light \
+  coqlight states check init theories theories-light \
   $(DOC_TARGETS) $(VO_TARGETS) validate \
   %.vo %.glob states/% install-% %.ml4-preprocessed \
   $(DOC_TARGET_PATTERNS)

dev/ocamlweb-doc/Makefile

@@ -7,7 +7,7 @@ LOCALINCLUDES=-I ../../config -I ../../tools -I ../../tools/coqdoc \
               -I ../../plugins/omega -I ../../plugins/romega \
 	      -I ../../plugins/ring -I ../../plugins/dp -I ../../plugins/setoid_ring \
               -I ../../plugins/xml -I ../../plugins/extraction \
-              -I ../../plugins/interface -I ../../plugins/fourier \
+              -I ../../plugins/fourier \
 	      -I ../../plugins/cc \
 	      -I ../../plugins/funind -I ../../plugins/firstorder \
               -I ../../plugins/field -I ../../plugins/subtac -I ../../plugins/rtauto \