configure.in 4.7 KB
Newer Older
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1
AC_INIT([Coq support library for Gappa], [1.4.2],
Guillaume Melquiond's avatar
Guillaume Melquiond committed
2
        [Guillaume Melquiond <guillaume.melquiond@inria.fr>],
Guillaume Melquiond's avatar
Guillaume Melquiond committed
3
        [gappalib-coq])
4

5 6 7 8 9 10 11 12 13 14 15
m4_divert_push(99)
if test "$ac_init_help" = "long"; then
  ac_init_help=short
fi
m4_divert_pop(99)

m4_divert_push([HELP_ENABLE])
Fine tuning of the installation directory:
AS_HELP_STRING([--libdir=DIR], [library @<:@DIR=`$COQC -where`/user-contrib/Gappa@:>@])
m4_divert_pop([HELP_ENABLE])

16
AC_DEFUN([AX_VERSION_GE], [AS_VERSION_COMPARE([$1],[$2],[$4],[$3],[$3])])
17

18 19
AC_PROG_CXX

20 21 22
native_tactic=yes
byte_tactic=yes

23 24 25
AC_ARG_VAR(COQBIN, [path to Coq executables [empty]])
if test ${COQBIN##*/}; then COQBIN=$COQBIN/; fi

26
AC_ARG_VAR(COQC, [Coq compiler command [coqc]])
27
AC_MSG_CHECKING([for coqc >= 8.8])
28
if test ! "$COQC"; then COQC=`which ${COQBIN}coqc`; fi
29
coqc_version=[`$COQC -v | sed -n -e 's/^.*version \([0-9][0-9.]*\).*$/\1/p'`]
30
AX_VERSION_GE([$coqc_version], [8.8],
Guillaume Melquiond's avatar
Guillaume Melquiond committed
31 32 33
  [ AC_MSG_RESULT([$COQC]) ],
  [ AC_MSG_RESULT([no])
    AC_MSG_ERROR([ *** Unable to find Coq (http://coq.inria.fr/)]) ])
34

35
AC_ARG_VAR(COQDEP, [Coq dependency analyzer command [coqdep]])
36 37 38 39
AC_MSG_CHECKING([for coqdep])
if test ! "$COQDEP"; then COQDEP=`which ${COQBIN}coqdep`; fi
AC_MSG_RESULT([$COQDEP])

40
AC_ARG_VAR(OCAMLC, [OCaml compiler command [ocamlc]])
41 42 43
AC_MSG_CHECKING([for ocamlc])
if test ! "$OCAMLC"; then
  OCAMLC=`$COQC -config | sed -n -e 's/^OCAMLC=\(.*\)/\1/p'`
44
  if test ! "$OCAMLC"; then OCAMLC=ocamlc; fi
45
  OCAMLC=`which $OCAMLC`
46 47
fi
AC_MSG_RESULT([$OCAMLC])
48

Guillaume Melquiond's avatar
Guillaume Melquiond committed
49 50 51 52
AC_ARG_VAR(CAMLP4O, [OCaml preprocessor [camlpXo]])
AC_MSG_CHECKING([for camlpXo])
if test ! "$CAMLP4O"; then
  CAMLP4O=`$COQC -config | sed -n -e 's/^CAMLP.O=\(.*\)/\1/p'`
53 54 55
  if test ! "$CAMLP4O"; then
    CAMLP4O=camlp5o
  fi
56 57 58 59 60 61 62 63 64 65 66
  case `uname -s` in
    CYGWIN*)
      case "$CAMLP4O" in
        *:*) CAMLP4O=`cygpath -m "$CAMLP4O"` ;;
        *)   CAMLP4O=`cygpath -u "$CAMLP4O"` ;;
      esac
      ;;
    *)
      CAMLP4O=`which $CAMLP4O`
      ;;
  esac
67
fi
Guillaume Melquiond's avatar
Guillaume Melquiond committed
68
AC_MSG_RESULT([$CAMLP4O])
69

70
AC_ARG_VAR(OCAMLOPT, [OCaml compiler command [ocamlopt]])
Guillaume Melquiond's avatar
Guillaume Melquiond committed
71
AC_MSG_CHECKING([for ocamlopt >= 4.02])
72 73
if test ! "$OCAMLOPT"; then
  OCAMLOPT=`$COQC -config | sed -n -e 's/^OCAMLOPT=\(.*\)/\1/p'`
74
  if test ! "$OCAMLOPT"; then OCAMLOPT=ocamlopt; fi
75
  OCAMLOPT=`which $OCAMLOPT`
76 77
fi
ocamlopt_version=`$OCAMLOPT -version`
Guillaume Melquiond's avatar
Guillaume Melquiond committed
78
AX_VERSION_GE([$ocamlopt_version], [4.02],
79 80 81
  [ AC_MSG_RESULT([$OCAMLOPT]) ],
  [ AC_MSG_RESULT([no])
    native_tactic=no ])
82

Guillaume Melquiond's avatar
Guillaume Melquiond committed
83
AC_MSG_CHECKING([for Flocq >= 3.0])
84
AS_IF(
85
  [ echo "Require Import Flocq.Version BinNat." \
Guillaume Melquiond's avatar
Guillaume Melquiond committed
86
         "Goal (30000 <= Flocq_version)%N. easy. Qed." > conftest.v
87
    $COQC conftest.v > conftest.err ],
88 89
  [ AC_MSG_RESULT([yes]) ],
  [ AC_MSG_RESULT([no])
Guillaume Melquiond's avatar
Guillaume Melquiond committed
90
    AC_MSG_ERROR([ *** Unable to find library Flocq >= 3.0 (http://flocq.gforge.inria.fr/)])])
91 92
rm -f conftest.v conftest.vo conftest.err

93
AC_SUBST(OCAMLLIB)
94
OCAMLLIB=`$OCAMLC -where | tr -d '\r' | tr '\\\\' '/'`
95 96

AC_SUBST(COQLIB)
97
COQLIB=`$COQC -where | tr -d '\r' | tr '\\\\' '/'`
98

99
if test "$libdir" = '${exec_prefix}/lib'; then
100
  libdir="$COQLIB/user-contrib/Gappa"
101 102
fi

103
AC_SUBST(COQDEFINE)
104 105
AX_VERSION_GE([$coqc_version], [8.10],
  [ COQDEFINE=COQ810 ], [
106
AX_VERSION_GE([$coqc_version], [8.9],
107
  [ COQDEFINE=COQ89 ], [
Guillaume Melquiond's avatar
Guillaume Melquiond committed
108
AX_VERSION_GE([$coqc_version], [8.8],
109
  [ COQDEFINE=COQ88 ])
110
])])
111

112 113 114 115 116 117 118 119 120 121 122 123
AC_ARG_ENABLE([tactic],
  AS_HELP_STRING([--disable-tactic], [do not compile a "gappa" tactic]),
  [if test "$enable_tactic" = "no"; then native_tactic=no ; byte_tactic=no ; fi], [])

AC_ARG_ENABLE([native-tactic],
  AS_HELP_STRING([--disable-native-tactic], [do not compile a native "gappa" tactic]),
  [if test "$enable_native_tactic" = "no"; then native_tactic=no ; fi], [])

AC_ARG_ENABLE([byte-tactic],
  AS_HELP_STRING([--disable-byte-tactic], [do not compile a bytecode "gappa" tactic]),
  [if test "$enable_byte_tactic" = "no"; then byte_tactic=no ; fi], [])

124 125 126 127 128 129 130 131 132 133 134 135 136
AC_MSG_NOTICE([building remake...])
case `uname -s` in
MINGW*)
	$CXX -Wall -O2 -o remake.exe remake.cpp -lws2_32
	if test $? != 0; then AC_MSG_FAILURE([failed]); fi
	AC_SUBST([REMAKE], [./remake.exe])
	;;
*)
	$CXX -Wall -O2 -o remake remake.cpp
	if test $? != 0; then AC_MSG_FAILURE([failed]); fi
	AC_SUBST([REMAKE], [./remake])
	;;
esac
137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161

AC_SUBST(TACTIC_TARGETS)
AC_SUBST(TACTIC_PARAM)

tactic_mode=""
if test "$native_tactic" = yes; then
  tactic_mode="$tactic_mode native"
  TACTIC_TARGETS="$TACTIC_TARGETS gappatac.cmxs"
  if test "$byte_tactic" = no; then
    TACTIC_PARAM="-opt"
  fi
fi
if test "$byte_tactic" = yes; then
  tactic_mode="$tactic_mode bytecode"
  TACTIC_TARGETS="$TACTIC_TARGETS gappatac.cmo"
  if test "$native_tactic" = no; then
    TACTIC_PARAM="-byte"
  fi
fi

if test -z "$tactic_mode"; then tactic_mode=" none"; fi

echo
echo "=== Summary ==="
echo "Installation directory   $libdir"
162
echo "Gappa tactic            $tactic_mode"
163 164
echo

165
AC_CONFIG_FILES(Remakefile)
166
AC_OUTPUT