Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / configure.ac @ 9b0432bc

History | View | Annotate | Download (5.66 KB)

1 6de6bcf4 ploc
define([gitversion], esyscmd([sh -c "git log --oneline | wc -l | tr -d ' \n'"]))
2 3471cb4d ploc
3 a89ad528 Corentin Lauverjat
AC_INIT([lustrec])
4 3471cb4d ploc
5 a4158a4b ploc
gitbranch=`git branch | grep \* | sed "s/\*[ ]*//"`
6 9c4cc944 Corentin Lauverjat
if test x"$gitbranch" != "xmaster"; then
7 a4158a4b ploc
  AC_SUBST(CDASHSUBPROJ, "unstable")
8
else
9
  AC_SUBST(CDASHSUBPROJ, "master")
10
fi
11 3471cb4d ploc
12 9c4cc944 Corentin Lauverjat
if test -z "$share"; then
13 9b0432bc Corentin Lauverjat
  share="$ac_pwd/_build/install/default/share/lustrec"
14 9c4cc944 Corentin Lauverjat
fi
15
16
AC_SUBST(SHARE_PATH, $share)
17
18 1e48ef45 ploc
AC_CONFIG_SRCDIR([src/main_lustre_compiler.ml])
19 bde99c3f xavier.thirioux
AC_CONFIG_SRCDIR([src/main_lustre_testgen.ml])
20 1e48ef45 ploc
21
# default prefix is /usr/local
22 9c4cc944 Corentin Lauverjat
AC_PREFIX_DEFAULT(./_build/install/default)
23 1954d776 ploc
24 9c4cc944 Corentin Lauverjat
# Seal plugin feature
25 57d61d67 ploc
26 9c4cc944 Corentin Lauverjat
AC_ARG_ENABLE(seal, 
27
  [AS_HELP_STRING([--disable-seal],[disable the seal plugin. Enabled by default if available.])
28
   AS_HELP_STRING([--enable-seal],[enable the seal plugin. Enabled if available by default.])])
29 57d61d67 ploc
30 c5de2e97 ploc
31 9c4cc944 Corentin Lauverjat
AS_IF([test "x$enable_seal" != "xno"],
32
  [
33
    if (test -z "$(dune external-lib-deps --missing plugins/seal 2>&1 | cat)" ); then
34
      AC_MSG_RESULT([seal plugin : enabled])
35
      AC_SUBST(LUSTREV_SEAL, ["(module Seal_plugin.Seal_verifier.Verifier : Lustrec.VerifierType.S);"])
36
      AC_SUBST(SEAL_PLUGIN_NAME, ["seal_plugin"])
37
    else
38
      AC_MSG_RESULT([seal plugin : disabled because the following libraries are missing : [$(dune external-lib-deps --missing plugins/seal  2>&1 | awk 'NR > 1 {print  $2}' ORS=', ' | sed 's/, $//')].])
39
      if (test "x$enable_seal" == "xyes" ); then
40
        AC_MSG_ERROR([Cannot enable the seal plugin!])
41
      fi
42
    fi
43
  ], 
44
  [AC_MSG_RESULT([seal plugin : disabled (you explicitely disabled it)])]
45 ad4774b0 ploc
)
46 7b424fe6 ploc
47 9c4cc944 Corentin Lauverjat
# Zustre plugin feature
48
AC_ARG_ENABLE(zustre, 
49
  [AS_HELP_STRING([--disable-zustre],[disable the Zustre plugin. Enabled by default if available.])
50
   AS_HELP_STRING([--enable-zustre],[enable the Zustre plugin. Enabled if available by default.])])
51
52
AS_IF([test "x$enable_zustre" != "xno"],
53
  [
54
    if (test -z "$(dune external-lib-deps --missing plugins/zustre 2>&1 | cat)" ); then
55
      AC_MSG_RESULT([zustre plugin : enabled])
56
      AC_SUBST(LUSTREV_ZUSTRE, ["(module Zustre_plugin.Zustre_verifier.Verifier : Lustrec.VerifierType.S);"])
57
      AC_SUBST(ZUSTRE_PLUGIN_NAME, ["zustre_plugin"])
58
      AC_SUBST(Z3LIBPATH, [`ocamlfind query z3 | tr -d '\n'`])
59
    else
60
      AC_MSG_RESULT([zustre plugin : disabled because the following libraries are missing : [$(dune external-lib-deps --missing plugins/zustre  2>&1 | awk 'NR > 1 {print  $2}' ORS=', ' | sed 's/, $//')].])
61
      if (test "x$enable_zustre" == "xyes" ); then
62
        AC_MSG_ERROR([Cannot enable the zustre plugin!])
63
      fi
64
    fi
65
  ], 
66
  [AC_MSG_RESULT([zustre plugin disabled (you explicitely disabled it)])]
67
)
68 ad4774b0 ploc
69 9c4cc944 Corentin Lauverjat
# Tiny plugin feature
70
AC_ARG_ENABLE(tiny, 
71
  [AS_HELP_STRING([--disable-tiny],[disable the Tiny plugin. Enabled by default if available.])
72
   AS_HELP_STRING([--enable-tiny],[enable the Tiny plugin. Enabled if available by default.])])
73
74
AS_IF([test "x$enable_tiny" != "xno"], [
75
  if (test -z "$(dune external-lib-deps --missing plugins/tiny 2>&1 | cat)" ); then
76
      AC_MSG_RESULT([tiny plugin : enabled])
77
      AC_SUBST(LUSTREV_TINY, ["(module Tiny_plugin.Tiny_verifier.Verifier : Lustrec.VerifierType.S);"])
78
      AC_SUBST(TINY_PLUGIN_NAME, ["tiny_plugin"])
79
    else
80
      AC_MSG_RESULT([tiny plugin : disabled because the following libraries are missing : [$(dune external-lib-deps --missing plugins/tiny  2>&1 | awk 'NR > 1 {print  $2}' ORS=', ' | sed 's/, $//')].])
81
      if (test "x$enable_tiny" == "xyes" ); then
82
        AC_MSG_ERROR([Cannot enable the tiny plugin!])
83
      fi
84
    fi
85
],
86
  [AC_MSG_RESULT([tiny plugin : disabled (you explicitely disabled it)])])
87 1954d776 ploc
88 9c4cc944 Corentin Lauverjat
# Salsa plugin feature
89
AC_ARG_ENABLE(salsa, 
90
  [AS_HELP_STRING([--disable-salsa],[disable the salsa plugin. Enabled by default if available.])
91
   AS_HELP_STRING([--enable-salsa],[enable the salsa plugin. Enabled if available by default.])])
92 1954d776 ploc
93
94
AS_IF([test "x$enable_salsa" != "xno"], [
95 9c4cc944 Corentin Lauverjat
  if (test -z "$(dune external-lib-deps --missing plugins/salsa 2>&1 | cat)" ); then
96
      AC_MSG_RESULT([salsa plugin : enabled])
97
      AC_SUBST(SALSA, ["(module Salsa_plugin.Plugin : Lustrec.PluginType.S);"])
98
      AC_SUBST(SALSA_PLUGIN_NAME, ["salsa_plugin"])
99
    else
100
      AC_MSG_RESULT([salsa plugin : disabled because the following libraries are missing : [$(dune external-lib-deps --missing plugins/salsa  2>&1 | awk 'NR > 1 {print  $2}' ORS=', ' | sed 's/, $//')].])
101
      if (test "x$enable_salsa" == "xyes" ); then
102
        AC_MSG_ERROR([Cannot enable the salsa plugin!])
103
      fi
104
    fi
105
],
106
  [AC_MSG_RESULT([salsa plugin : disabled (you explicitely disabled it)])])
107
108 1954d776 ploc
109 d21f00de Christophe Garion
# GMP
110 bad7b67a Christophe Garion
AC_CHECK_LIB(gmp, __gmpz_init,
111 04a63d25 xthirioux
      [gmp=yes],
112
      [AC_MSG_RESULT([GNU MP not found])
113
      gmp=no])
114 9c4cc944 Corentin Lauverjat
#MPFR
115 bad7b67a Christophe Garion
AC_CHECK_LIB(mpfr, mpfr_add, [mpfr=yes],
116 04a63d25 xthirioux
		   [AC_MSG_RESULT(
117
[MPFR not found])
118
mpfr=no])
119
120 3b4b7a2e Christophe Garion
121
AC_SUBST_FILE(lustresf)
122
AC_SUBST_FILE(lustresf_src)
123
lustresf=/dev/null
124
lustresf_src=/dev/null
125
126 9c4cc944 Corentin Lauverjat
127
lustresf=Makefile-lustresf.in
128
lustresf_src=src/Makefile-lustresf.in
129
AC_SUBST(lustresf_target, "lustresf")
130
131 1e48ef45 ploc
132
133
AC_DEFUN([AC_DEFINE_DIR], [
134
  prefix_NONE=
135
  exec_prefix_NONE=
136
  test "x$prefix" = xNONE && prefix_NONE=yes && prefix=$ac_default_prefix
137
  test "x$exec_prefix" = xNONE && exec_prefix_NONE=yes && exec_prefix=$prefix
138
dnl In Autoconf 2.60, ${datadir} refers to ${datarootdir}, which in turn
139
dnl refers to ${prefix}.  Thus we have to use `eval' twice.
140
  eval ac_define_dir="\"[$]$2\""
141
  eval ac_define_dir="\"$ac_define_dir\""
142
  AC_SUBST($1, "$ac_define_dir")
143
  AC_DEFINE_UNQUOTED($1, "$ac_define_dir", [$3])
144
  test "$prefix_NONE" && prefix=NONE
145
  test "$exec_prefix_NONE" && exec_prefix=NONE
146
])
147
148
AC_DEFINE_DIR([abs_datadir], [datadir])
149
150
# Instanciation
151 9c4cc944 Corentin Lauverjat
AC_CONFIG_FILES([
152 fb716d2c ploc
		 Makefile
153 9c4cc944 Corentin Lauverjat
     src/dune
154
     plugins/zustre/dune
155
     src/pluginList.ml
156 ad4774b0 ploc
		 src/verifierList.ml
157 9c4cc944 Corentin Lauverjat
     lib/version.ml
158 5c3b45a0 ploc
		 share/FindLustre.cmake
159 1954d776 ploc
		 ])
160 1e48ef45 ploc
161
AC_OUTPUT