Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / configure.ac @ 3769b712

History | View | Annotate | Download (6.94 KB)

1
define([gitversion], esyscmd([sh -c "git log --oneline | wc -l | tr -d ' \n'"]))
2

    
3
AC_INIT([lustrec], 1.7-gitversion, [ploc@garoche.net])
4
AC_SUBST(VERSION_NUMBER, 1.7)
5

    
6
gitbranch=`git branch | grep \* | sed "s/\*[ ]*//"`
7
AC_SUBST(GITBRANCH, "$gitbranch")
8
if test x"$GITBRANCH" != "xmaster"; then
9
  AC_SUBST(CDASHSUBPROJ, "unstable")
10
else
11
  AC_SUBST(CDASHSUBPROJ, "master")
12
fi
13

    
14
# Next release will be
15
#AC_INIT([lustrec], [1.8], [ploc@garoche.net])
16
AC_MSG_NOTICE(Git branch: ${GITBRANCH})
17
AC_CONFIG_SRCDIR([src/main_lustre_compiler.ml])
18
AC_CONFIG_SRCDIR([src/main_lustre_testgen.ml])
19

    
20
# default prefix is /usr/local
21
AC_PREFIX_DEFAULT(/usr/local)
22

    
23
# Configuration
24
AC_MSG_NOTICE(******** Configuration ********)
25
AC_MSG_NOTICE(bin path:     $prefix/bin)
26
AC_MSG_NOTICE(include path: $prefix/include)
27

    
28

    
29
# Check seal library availability  
30
AC_MSG_CHECKING(if seal library is available)
31
AS_IF([ocamlfind query seal >/dev/null 2>&1],
32
    [seal=yes; AC_MSG_RESULT([yes])],
33
    [seal=no; AC_MSG_RESULT([no])]
34
)
35

    
36
# Check tiny library availability  
37
AC_MSG_CHECKING([if tiny library is available]) 
38
AS_IF([ocamlfind query tiny >/dev/null 2>&1],
39
    [tiny=yes; AC_MSG_RESULT([yes])],
40
    [tiny=no; AC_MSG_RESULT([no])],
41
)
42

    
43
# Check z3 library availability
44
AC_MSG_CHECKING(if z3 library is available)
45
AS_IF([ocamlfind query z3 >/dev/null 2>&1],
46
    [z3=yes; AC_MSG_RESULT([yes])],
47
    [z3=no; AC_MSG_RESULT([no])]
48
)
49

    
50
# Seal plugin feature
51

    
52
AC_ARG_ENABLE(seal, 
53
  [AS_HELP_STRING([--disable-seal],[disable the seal plugin. Enabled by default if available.])
54
   AS_HELP_STRING([--enable-seal],[enable the seal plugin. Enabled if available by default.])])
55

    
56

    
57
AS_IF([test "x$enable_seal" != "xno"],
58
  [
59
    if (test "x$seal" == "xyes" -a "x$z3" == "xyes"); then
60
      AC_MSG_RESULT([seal plugin : enabled])
61
      AC_SUBST(LUSTREV_SEAL, ["(module Seal_verifier.Verifier : Lustrec.VerifierType.S);"])
62
    else
63
      AC_MSG_RESULT([seal plugin : disabled (seal library or z3 package is not available)])
64
      if (test "x$enable_seal" == "xyes" ); then
65
        AC_MSG_ERROR([Cannot enable the seal plugin!])
66
      fi
67
    fi
68
  ], 
69
  [AC_MSG_RESULT([seal plugin disabled (you explicitely disabled it)])]
70
)
71

    
72
# Zustre plugin feature
73
AC_ARG_ENABLE(zustre, 
74
  [AS_HELP_STRING([--disable-zustre],[disable the Zustre plugin. Enabled by default if available.])
75
   AS_HELP_STRING([--enable-zustre],[enable the Zustre plugin. Enabled if available by default.])])
76

    
77
AS_IF([test "x$enable_zustre" != "xno"],
78
  [
79
    if (test "x$z3" == "xyes" ); then
80
      AC_MSG_RESULT([zustre plugin : enabled])
81
      AC_SUBST(LUSTREV_ZUSTRE, ["(module Zustre_for_lustrev.Zustre_verifier.Verifier : Lustrec.VerifierType.S);"])
82
      AC_SUBST(LUSTREV_Z3_TAG, ["<**/*verifier.native> or <tools/zustre/*.ml> or <tools/zustre/*.mli> or <tools/seal/seal_extract.ml> or <tools/seal/seal_extract.mli>: package($z3name)"])
83
      define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n']))
84
      AC_SUBST(Z3LIBPATH, "z3path")
85
    else
86
      AC_MSG_RESULT([zustre plugin : disabled (z3 is not available)])
87
      if (test "x$enable_zustre" == "xyes" ); then
88
        AC_MSG_ERROR([Cannot enable the zustre plugin!])
89
      fi
90
    fi
91
  ], 
92
  [AC_MSG_RESULT([zustre plugin disabled (you explicitely disabled it)])]
93
)
94

    
95
# Tiny plugin feature
96
AC_ARG_ENABLE(tiny, 
97
  [AS_HELP_STRING([--disable-tiny],[disable the Tiny plugin. Enabled by default if available.])
98
   AS_HELP_STRING([--enable-tiny],[enable the Tiny plugin. Enabled if available by default.])])
99

    
100
AS_IF([test "x$enable_tiny" != "xno"], [
101
  if (test "x$tiny" == "xyes" ); then
102
      AC_MSG_RESULT([tiny plugin : enabled])
103
      AC_SUBST(LUSTREV_TINY, ["(module Tiny_for_lustrev.Tiny_verifier.Verifier : Lustrec.VerifierType.S);"])
104
      AC_SUBST(LUSTREV_TINY_TAG, ["<**/*>: package(apron.boxMPQ), package(apron.octMPQ), package(apron.polkaMPQ), package(tiny)"])
105
    else
106
      AC_MSG_RESULT([tiny plugin : disabled (tiny library is not available)])
107
      if (test "x$enable_tiny" == "xyes" ); then
108
        AC_MSG_ERROR([Cannot enable the tiny plugin!])
109
      fi
110
    fi
111
])
112

    
113
# Salsa plugin feature
114
AC_ARG_ENABLE(salsa, 
115
  [AS_HELP_STRING([--disable-salsa],[disable the salsa plugin. Enabled by default if available.])
116
   AS_HELP_STRING([--enable-salsa],[enable the salsa plugin. Enabled if available by default.])])
117

    
118

    
119
AS_IF([test "x$enable_salsa" != "xno"], [
120
  if (test "x$salsa" == "xyes" ); then
121
      AC_MSG_RESULT([salsa plugin : enabled])
122
      AC_SUBST(SALSA, ["(module Salsa_plugin.Plugin : Lustrec.PluginType.S);"])
123
      AC_SUBST(SALSA_TAG, ["<**/*.native> or <plugins/salsa/*.cm?> : package(salsa)"])
124
    else
125
      AC_MSG_RESULT([salsa plugin : disabled (salsa library is not available)])
126
      if (test "x$enable_salsa" == "xyes" ); then
127
        AC_MSG_ERROR([Cannot enable the salsa plugin!])
128
      fi
129
    fi
130
])
131

    
132

    
133
# GMP
134
AC_CHECK_LIB(gmp, __gmpz_init,
135
      [gmp=yes],
136
      [AC_MSG_RESULT([GNU MP not found])
137
      gmp=no])
138
#MPFR
139
AC_CHECK_LIB(mpfr, mpfr_add, [mpfr=yes],
140
		   [AC_MSG_RESULT(
141
[MPFR not found])
142
mpfr=no])
143

    
144

    
145
AC_SUBST_FILE(lustresf)
146
AC_SUBST_FILE(lustresf_src)
147
lustresf=/dev/null
148
lustresf_src=/dev/null
149

    
150

    
151
lustresf=Makefile-lustresf.in
152
lustresf_src=src/Makefile-lustresf.in
153
AC_SUBST(lustresf_target, "lustresf")
154

    
155

    
156
# Checking availability of path to regression tests
157
tests_path="../lustrec-tests/regression_tests"
158

    
159
AC_ARG_WITH([tests-path],
160
            [AS_HELP_STRING([--with-tests-path],
161
               [provides path to test suite (default is ../lustrec-test if available)])],
162
            [tests_path="$withval";
163
	     if (test "x$tests_path" = xyes); then
164
	       AC_MSG_ERROR(Option --with-tests-path requires a parameter: eg. --with-tests-path=value);
165
	     fi],
166
            )
167
AC_MSG_NOTICE($tests_path)
168
AC_CHECK_FILE(${tests_path}/CMakeLists.txt,
169
              [
170
	      valid_test_path=true
171
	      ],
172
	      [
173
	      valid_test_path=false
174
	        AC_SUBST(PATH_TO_TESTS, $tests_path)	      ])
175
AC_SUBST(PATH_TO_TESTS_DEFINED, $valid_test_path)
176
AC_SUBST(PATH_TO_TESTS, $tests_path)
177

    
178
# End of config
179

    
180
AC_DEFUN([AC_DEFINE_DIR], [
181
  prefix_NONE=
182
  exec_prefix_NONE=
183
  test "x$prefix" = xNONE && prefix_NONE=yes && prefix=$ac_default_prefix
184
  test "x$exec_prefix" = xNONE && exec_prefix_NONE=yes && exec_prefix=$prefix
185
dnl In Autoconf 2.60, ${datadir} refers to ${datarootdir}, which in turn
186
dnl refers to ${prefix}.  Thus we have to use `eval' twice.
187
  eval ac_define_dir="\"[$]$2\""
188
  eval ac_define_dir="\"$ac_define_dir\""
189
  AC_SUBST($1, "$ac_define_dir")
190
  AC_DEFINE_UNQUOTED($1, "$ac_define_dir", [$3])
191
  test "$prefix_NONE" && prefix=NONE
192
  test "$exec_prefix_NONE" && exec_prefix=NONE
193
])
194

    
195
AC_DEFINE_DIR([abs_datadir], [datadir])
196

    
197
# Instanciation
198
AC_CONFIG_FILES([opam
199
		 Makefile
200
		 src/pluginList.ml
201
		 src/verifierList.ml
202
		 include/z3librc
203
		 share/FindLustre.cmake
204
		 ])
205

    
206
AC_OUTPUT
207

    
208

    
209

    
210

    
211
AC_MSG_NOTICE(****** Regression Tests  ******)
212
if (test "x$valid_test_path" = xfalse); then
213
  AC_MSG_NOTICE(no valid tests path provided ($tests_path))
214
else
215
AC_MSG_NOTICE(tests path: $tests_path)
216
fi
217
AC_MSG_NOTICE(******** Configuration ********)
218
AC_MSG_NOTICE(Execute "make; make install" now)