From 9fb34c89fcde828111ab2dfe649da3e28728bdaa Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Thu, 26 Oct 2023 16:08:46 +0200 Subject: [PATCH] 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) --- .gitignore | 1 + Makefile.in | 21 ++++++++++++--------- configure.ac | 37 +++++++++++++++++++++++++++++++------ 3 files changed, 44 insertions(+), 15 deletions(-) diff --git a/.gitignore b/.gitignore index 37acdcd67..69797a982 100644 --- a/.gitignore +++ b/.gitignore @@ -28,6 +28,7 @@ config.status *.vo *.vok *.vos +.*.swp coqthmdep dpd2dot diff --git a/Makefile.in b/Makefile.in index f049f7141..65039c0be 100644 --- a/Makefile.in +++ b/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) diff --git a/configure.ac b/configure.ac index 36fcf4eb2..5b96b3fd0 100644 --- a/configure.ac +++ b/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 "$COQBIN"; then + PATH="$COQBIN:$PATH"; + if ! test "$OCAMLPATH"; 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 #~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~