Commit 60c113db authored by Raphael Cauderlier's avatar Raphael Cauderlier

Deactivate confluence checking by default

The configure script can be called with --with-confluence-checking for
forcing confluence checking.
parent e7c5df52
......@@ -5,6 +5,9 @@ INSTALL_LIB_DIR=/usr/local/lib/dedukti/dktactics
SUBDIRS= fol meta # example
# To activate confluence checking, set this to "--with-confluence-checking"
CONFIGURE_FLAGS=
all:
for d in $(SUBDIRS); do \
$(MAKE) all -C $$d; \
......@@ -36,6 +39,6 @@ uninstall:
rmdir $(INSTALL_LIB_DIR)
.config_vars: configure
./configure
./configure $(CONFIGURE_FLAGS)
.PHONY: clean install uninstall all
......@@ -59,14 +59,71 @@ find_and_check_binary () {
fi
}
usage () {
echo "usage: ./configure [options] [<directory>]"
echo
echo "Options are:"
echo " [-]-install_prefix <directory>"
echo " set <directory> as the directory prefix for installation of"
echo " the FoCaLize commands."
echo " (Default value for <directory> is $BOLDTAG$INSTALL_PREFIX$NORMALTAG.)"
echo " [-]-interactive"
echo " run interactively, asking questions."
echo " [-]-no-doc"
echo " do not generate the PDF documentation files."
echo " [-]-tools_prefix <directory>"
echo " set <directory> as the directory prefix where tools required to"
echo " build FoCaLiZe are installed. The currently required non-common"
echo " tools are OCaml and Coq."
}
CONFLUENCE_CHECKING=false
usage () {
echo "usage: ./configure [options]"
echo
echo "Options are:"
echo " --with-confluence-checking"
echo " activate confluence checking of the fol directory."
echo " This is slower and requires CSI^HO."
echo " -h | -help | --help"
echo " Display this message"
}
# Parsing arguments.
while : ; do
# If nothing else to parse then end the loop.
case $# in 0) break;; *);; esac
case "$1" in
--with-confluence-checking)
CONFLUENCE_CHECKING=true
shift;;
-h | -help | --help)
usage;
shift;
exit 0;;
-*)
option="$1";
echo "./configure: bad option '${option}'" >&2 && \
echo "For help, use ./configure -help" >&2 && \
shift;
exit 2;;
esac;
done
# Ensures that the file ".config_vars" exists and is empty
echo > .config_vars &&
# Mandatory
find_and_check_binary "dkdep" ".native" "DKDEP" "-version" "" &&
find_and_check_binary "dkcheck" ".native" "DKCHECK" "-version" "Dedukti v2.6" &&
find_and_check_binary "dkdep" ".native" "DKDEP" "" "" &&
#find_and_check_binary "dkmeta" ".native" "DKMETA" "-version" "Meta Dedukti v2.6" &&
#find_and_check_binary "skcheck" ".native" "SKCHECK" "-version" "Sukerujo v2.6" &&
#find_and_check_binary "skmeta" ".native" "SKMETA" "-version" "Sukerujo v2.6" &&
# Optional
find_and_check_binary "csiho" ".sh" "CSIHO" "--version" "csiho 0.3"
if $CONFLUENCE_CHECKING
then
find_and_check_binary "csiho" ".sh" "CSIHO" "--version" "csiho 0.3"
fi
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment