Add COQBIN to configure.ac

- A COQBIN variable, if set and non-null is prepended to the PATH in
  configure.ac. The variables COQC, COQDOC and COQTOP now contain an
  absolute path.
- In this case, if the OCAMLPATH variable is not set, a warning is
  emitted during ./configure (because the user probably wants the coq ml
  libs to be those corresponding to its current coq build)
- Other cleaning made in Makefile.in, using variables COQC
  COQTOP and COQDOC rather than fixed commands.
- `make archi_clean` now cleans more
- small addition in .gitignore (swap files for vim)

Author: Villetaneuse

.gitignore

@@ -28,6 +28,7 @@ config.status
 *.vo
 *.vok
 *.vos
+.*.swp
 
 coqthmdep
 dpd2dot

Makefile.in

@@ -62,6 +62,9 @@ OCAMLFLAGS += $(OCAML_EXTRA_OPTS)
 OCAMLOPTFLAGS = -c
 
 COQ_MAKEFILE=@COQ_MAKEFILE@
+COQTOP=@COQTOP@
+COQC=@COQC@
+COQDOC=@COQDOC@
 # COQDEP=$(OCAMLDEP)
 
 COQEXTFILES=searchdepend.mlg graphdepend.mlg
@@ -190,38 +193,38 @@ $(TESTDIR)/%.err.log: $(TESTDIR)/%.err.dpd $(DPD2DOT)
 	cp $< $@
 
 %.vo : %.v
-	coqc -q -R . dpdgraph $<
+	$(COQC) -q -R . dpdgraph $<
 
 %.html : %.v
-	coqdoc $<
+	$(COQDOC) $<
 
 %.svg : %.dot
 	dot -Tsvg -o$@ $<
 
 $(TESTDIR)/Morph%.dpd : $(TESTDIR)/Morph.vo $(TESTDIR)/Morph.cmd $(DPDPLUGIN)
 	# cd to tests to generate .dpd file there.
-	cd $(TESTDIR); coqtop -R .. dpdgraph -I .. < Morph.cmd > /dev/null 2>&1
+	cd $(TESTDIR); $(COQTOP) -R .. dpdgraph -I .. < Morph.cmd > /dev/null 2>&1
 
 $(TESTDIR)/Polymorph%.dpd : $(TESTDIR)/Polymorph.vo $(TESTDIR)/Polymorph.cmd \
                             $(DPDPLUGIN)
-	cd $(TESTDIR); coqtop -R .. dpdgraph -I .. < Polymorph.cmd
+	cd $(TESTDIR); $(COQTOP) -R .. dpdgraph -I .. < Polymorph.cmd
 
 $(TESTDIR)/graph.dpd $(TESTDIR)/graph2.dpd: \
 	             $(TESTDIR)/Test.vo $(TESTDIR)/Test.cmd $(DPDPLUGIN)
 	# cd to tests to generate .dpd file there.
-	cd $(TESTDIR); coqtop -R .. dpdgraph -I .. < Test.cmd > /dev/null 2>&1
+	cd $(TESTDIR); $(COQTOP) -R .. dpdgraph -I .. < Test.cmd > /dev/null 2>&1
 
 $(TESTDIR)/PrimitiveProjections.dpd $(TESTDIR)/PrimitiveProjections2.dpd: \
 	             $(TESTDIR)/PrimitiveProjections.vo $(TESTDIR)/PrimitiveProjections.cmd $(DPDPLUGIN)
 	# cd to tests to generate .dpd file there.
-	cd $(TESTDIR); coqtop -R .. dpdgraph -I .. < PrimitiveProjections.cmd > /dev/null 2>&1
+	cd $(TESTDIR); $(COQTOP) -R .. dpdgraph -I .. < PrimitiveProjections.cmd > /dev/null 2>&1
 
 %.dpd : %.vo %.cmd
 	# cd to tests to generate .dpd file there.
-	cd $(TESTDIR); coqtop -R .. dpdgraph -I .. < $(*F).cmd > /dev/null 2>&1
+	cd $(TESTDIR); $(COQTOP) -R .. dpdgraph -I .. < $(*F).cmd > /dev/null 2>&1
 
 $(TESTDIR)/search.log : $(TESTDIR)/Test.vo $(TESTDIR)/search.cmd $(DPDPLUGIN)
-	cat $(TESTDIR)/search.cmd | coqtop -R . dpdgraph -I . 2> /dev/null \
+	cat $(TESTDIR)/search.cmd | $(COQTOP) -R . dpdgraph -I . 2> /dev/null \
 	  | sed -e 's/Welcome to Coq.*/Welcome to Coq/' > $@
 
 %.dot : %.dpd  $(DPD2DOT)
@@ -292,7 +295,7 @@ clean_test :
 clean_config:
 	rm -rf autom4te.cache
 	rm -f configure config.log config.status
-	rm -r Makefile
+	rm -rf Makefile Make_coq.conf .Make_coq.d Make_coq
 
 clean : clean_coq clean_test
 	rm -f $(GENERATED)

configure.ac

@@ -10,7 +10,7 @@
 # will set several variables: (see AC_SUBST at the end of this file)
 #~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-AC_INIT(coq-dpdgraph,1.0)
+AC_INIT([coq-dpdgraph],[1.0])
 AC_MSG_NOTICE(AC_PACKAGE_NAME version AC_PACKAGE_VERSION)
 
 #~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -174,7 +174,20 @@ fi
 #~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 new_section "Coq"
 
-AC_CHECK_PROG(COQC,coqc,coqc,no)
+#AC_ARG_VAR(COQBIN, [path to Coq executables [empty]])
+#if test ${COQBIN##*/}; then COQBIN=$COQBIN/; fi
+#AC_MSG_RESULT($COQBIN)
+
+if test "a$COQBIN" != "a"; then
+    PATH="$COQBIN:$PATH";
+    if test "a$OCAMLPATH" = "a"; then
+        AC_MSG_WARN(You set COQBIN but not OCAMLPATH.)
+        AC_MSG_WARN(You may want to consider adding:)
+        AC_MSG_WARN(export OCAMLPATH='${COQBIN%/*/}/lib')
+    fi
+fi
+
+AC_PATH_PROG(COQC,coqc,[no], [$PATH])
 if test "$COQC" = no ; then
   AC_MSG_ERROR(Cannot find coqc.)
 fi
@@ -183,19 +196,28 @@ AC_MSG_CHECKING(coq version)
 COQVERSION=$($COQC -v | sed -n -e 's|.*version *\(.*\)$|\1|p' )
 AC_MSG_RESULT($COQVERSION)
 
+AC_PATH_PROG(COQTOP,coqtop,[no], [$PATH])
+if test "$COQTOP" = no ; then
+  AC_MSG_ERROR(Cannot find coqtop.)
+fi
+
+AC_PATH_PROG(COQDOC,coqdoc,[no], [$PATH])
+if test "$COQDOC" = no ; then
+  AC_MSG_ERROR(Cannot find coqdoc.)
+fi
+
 case $COQVERSION in
   8.[[0-9]][[^0-9]]*|8.10*)
     AC_MSG_ERROR(AC_PACKAGE_NAME needs Coq version 8.11 or higher)
     ;;
 esac
 
-AC_CHECK_PROG(COQ_MAKEFILE,coq_makefile,coq_makefile,no)
+AC_PATH_PROG(COQ_MAKEFILE,coq_makefile,no, [$PATH])
 if test "$COQ_MAKEFILE" = no ; then
   AC_MSG_ERROR(cannot find coq_makefile.)
 fi
 
-BINDIR_PRE=$(which coqc)
-BINDIR=$(dirname $BINDIR_PRE)
+BINDIR=$(dirname $COQC)
 
 #~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 new_section "creating Makefile"
@@ -216,13 +238,16 @@ AC_SUBST(OCAMLYACC)
 AC_SUBST(OCAML_EXTRA_OPTS)
 
 AC_SUBST(COQC)
+AC_SUBST(COQTOP)
+AC_SUBST(COQDOC)
 AC_SUBST(COQ_MAKEFILE)
 
 AC_SUBST(BINDIR)
 AC_SUBST(OCAMLGRAPH_PATH)
 
 # Finally create the Makefile from Makefile.in
-AC_OUTPUT(Makefile)
+AC_CONFIG_FILES([Makefile])
+AC_OUTPUT
 chmod a-w Makefile
 
 #~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~