|
1
|
define([gitversion], esyscmd([sh -c "git log --oneline | wc -l | tr -d ' \n'"]))
|
|
2
|
|
|
3
|
AC_INIT([lustrec], 1.7, [ploc@garoche.net])
|
|
4
|
AC_SUBST(VERSION_NUMBER, 1.7)
|
|
5
|
AC_SUBST(VERSION_CODENAME, "Xia/Huai")
|
|
6
|
|
|
7
|
gitbranch=`git branch | grep \* | sed "s/\*[ ]*//"`
|
|
8
|
AC_SUBST(GITBRANCH, "$gitbranch")
|
|
9
|
if test x"$GITBRANCH" != "xmaster"; then
|
|
10
|
AC_SUBST(CDASHSUBPROJ, "unstable")
|
|
11
|
else
|
|
12
|
AC_SUBST(CDASHSUBPROJ, "master")
|
|
13
|
fi
|
|
14
|
|
|
15
|
# Next release will be
|
|
16
|
#AC_INIT([lustrec], [1.8], [ploc@garoche.net])
|
|
17
|
#AC_SUBST(VERSION_CODENAME, "Xia/Mang")
|
|
18
|
AC_MSG_NOTICE(Git branch: ${GITBRANCH})
|
|
19
|
AC_CONFIG_SRCDIR([src/main_lustre_compiler.ml])
|
|
20
|
AC_CONFIG_SRCDIR([src/main_lustre_testgen.ml])
|
|
21
|
|
|
22
|
AC_PATH_PROG([OCAMLC],[ocamlc],[:])
|
|
23
|
AC_MSG_CHECKING(OCaml version)
|
|
24
|
ocamlc_version=`$OCAMLC -v | grep version | rev| cut -d \ -f 1 | rev`
|
|
25
|
major=`echo $ocamlc_version | cut -d . -f 1`
|
|
26
|
minor=`echo $ocamlc_version | cut -d . -f 2`
|
|
27
|
if (test "$major" -lt 3 -a "$minor" -lt 11 ); then
|
|
28
|
AC_MSG_ERROR([Ocaml version must be at least 3.11. You have version $ocamlc_version])
|
|
29
|
fi
|
|
30
|
AC_MSG_RESULT(valid ocaml version detected: $ocamlc_version)
|
|
31
|
|
|
32
|
AC_PATH_PROG([OCAMLBUILD],[ocamlbuild],[:])
|
|
33
|
|
|
34
|
# Handle a mismatch in available function btw 4.02 and 4.04
|
|
35
|
if (test $"$major" -eq 4 -a "$minor" -gt 2); then
|
|
36
|
AC_SUBST(UPPERCASEFUN, "String.uppercase_ascii")
|
|
37
|
else
|
|
38
|
AC_SUBST(UPPERCASEFUN, "String.uppercase")
|
|
39
|
fi
|
|
40
|
|
|
41
|
# default prefix is /usr/local
|
|
42
|
AC_PREFIX_DEFAULT(/usr/local)
|
|
43
|
|
|
44
|
dnl AC_ARG_WITH([ocamlgraph-path],
|
|
45
|
dnl [AS_HELP_STRING([--ocamlgraph-path],
|
|
46
|
dnl [specify the path of ocamlgraph library. graph.cmxa should be in ocamlgraph-path @<:@default=$(ocamlfind query ocamlgraph)@:>@])],
|
|
47
|
dnl [AS_IF([test "x$ocamlgraph_path" = xno],
|
|
48
|
dnl [AC_MSG_ERROR([ocamlgraph library is needed])],
|
|
49
|
dnl [test "x$ocamlgraph_path" = xyes],
|
|
50
|
dnl [OCAMLGRAPH_PATH=$(ocamlfind query ocamlgraph)],
|
|
51
|
dnl [OCAMLGRAPH_PATH=$ocamlgraph_path]
|
|
52
|
dnl )],
|
|
53
|
dnl [OCAMLGRAPH_PATH=$(ocamlfind query ocamlgraph)]
|
|
54
|
dnl )
|
|
55
|
dnl AC_SUBST(OCAMLGRAPH_PATH)
|
|
56
|
|
|
57
|
|
|
58
|
# Checking libs
|
|
59
|
AC_CHECK_PROG(FINDLIB_CHECK,ocamlfind,yes)
|
|
60
|
if test x"$FINDLIB_CHECK" != x"yes" ; then
|
|
61
|
AC_MSG_ERROR(ocamlfind required!)
|
|
62
|
fi
|
|
63
|
dnl AC_MSG_RESULT(Hourrah: ocamlfind found!)
|
|
64
|
|
|
65
|
# Checks for libraries.
|
|
66
|
# OCamlgraph
|
|
67
|
AC_MSG_CHECKING(ocaml libraries required (ocamlgraph cmdliner fmt logs num))
|
|
68
|
AS_IF([ocamlfind query ocamlgraph cmdliner fmt logs num >/dev/null 2>&1],
|
|
69
|
[],[AC_MSG_ERROR(A few ocaml library required. opam install ocamlgraph cmdliner fmt logs num should solve the issue)],
|
|
70
|
)
|
|
71
|
AC_MSG_RESULT(yes)
|
|
72
|
|
|
73
|
#Yojson
|
|
74
|
AC_MSG_CHECKING(yojson library (optional))
|
|
75
|
AS_IF([ocamlfind query yojson >/dev/null 2>&1],
|
|
76
|
[yojson=yes; AC_MSG_RESULT(yes)],[yojson=no; AC_MSG_WARN(Yojson required for lustresf. opam install yojson should solve the issue)],
|
|
77
|
)
|
|
78
|
|
|
79
|
# Seal
|
|
80
|
AC_MSG_CHECKING(seal library (optional))
|
|
81
|
AS_IF([ocamlfind query seal >/dev/null 2>&1],
|
|
82
|
[seal=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)],
|
|
83
|
)
|
|
84
|
AS_IF([test "x$seal" = "xyes"], [
|
|
85
|
AC_SUBST(LUSTREV_SEAL, "(module Seal_verifier.Verifier : VerifierType.S);")
|
|
86
|
AC_SUBST(LUSTREV_SEAL_TAG, "<**/*verifier.native>: package(seal)")
|
|
87
|
])
|
|
88
|
|
|
89
|
# Tiny
|
|
90
|
AC_MSG_CHECKING(tiny library (optional))
|
|
91
|
AS_IF([ocamlfind query tiny >/dev/null 2>&1],
|
|
92
|
[tiny=yes; AC_MSG_RESULT(yes)],[tiny=no; AC_MSG_RESULT(no)],
|
|
93
|
)
|
|
94
|
AS_IF([test "x$tiny" = "xyes"], [
|
|
95
|
dnl AC_SUBST(LUSTREV_TINY_TAG, "<**/*>: package(apron.boxMPQ), package(apron.octMPQ), package(apron.polkaMPQ), package(tiny)")
|
|
96
|
])
|
|
97
|
|
|
98
|
# z3 (optional)
|
|
99
|
|
|
100
|
AC_ARG_ENABLE(z3, [AS_HELP_STRING([--disable-z3],
|
|
101
|
[disable Z3 dependencies. Enabled by default if available.])])
|
|
102
|
|
|
103
|
# option to rely on github version if installed
|
|
104
|
AC_ARG_WITH(z3_github, [AS_HELP_STRING([--with-z3-github],
|
|
105
|
[Rely on Z3 as distributed by the official github
|
|
106
|
repo rather then the opam distribution. Disabled by default.])])
|
|
107
|
|
|
108
|
AS_IF([test "x$with_z3_github" != "xyes"],
|
|
109
|
[z3name=z3],
|
|
110
|
[z3name=Z3]
|
|
111
|
)
|
|
112
|
|
|
113
|
AC_MSG_CHECKING(z3 library)
|
|
114
|
|
|
115
|
|
|
116
|
#define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n']))
|
|
117
|
#define([z3path], esyscmd([opam config var Z3:lib | tr -d '\n']))
|
|
118
|
|
|
119
|
AS_IF([ocamlfind query $z3name >/dev/null 2>&1],
|
|
120
|
[z3=yes; AC_MSG_RESULT([yes])],[zustre=no; AC_MSG_RESULT(no)],
|
|
121
|
)
|
|
122
|
|
|
123
|
AS_IF([test "x$enable_z3" != "xno"], [
|
|
124
|
if (test "x$z3" = xyes ); then
|
|
125
|
AC_SUBST(LUSTREV_ZUSTRE, "(module Zustre_verifier.Verifier : VerifierType.S);")
|
|
126
|
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)")
|
|
127
|
AS_IF([test "x$z3name" = "xZ3"],
|
|
128
|
[define([Z3path], esyscmd([ocamlfind query Z3 | tr -d '\n']))
|
|
129
|
AC_SUBST(Z3LIBPATH, "Z3path")],
|
|
130
|
[define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n']))
|
|
131
|
AC_SUBST(Z3LIBPATH, "z3path")]
|
|
132
|
)
|
|
133
|
fi
|
|
134
|
])
|
|
135
|
|
|
136
|
|
|
137
|
dnl # Tiny
|
|
138
|
dnl AC_MSG_CHECKING(tiny library (optional))
|
|
139
|
dnl AS_IF([ocamlfind query tiny >/dev/null 2>&1],
|
|
140
|
dnl [tiny=yes; AC_MSG_RESULT(yes)],[tiny=no; AC_MSG_RESULT(no)],
|
|
141
|
dnl )
|
|
142
|
AS_IF([test "x$tiny" = "xyes"], [
|
|
143
|
AC_SUBST(LUSTREV_TINY, "(module Tiny_verifier.Verifier : VerifierType.S);")
|
|
144
|
AC_SUBST(LUSTREV_TINY_TAG, ["<**/*>: package(apron.boxMPQ), package(apron.octMPQ), package(apron.polkaMPQ), package(tiny)"])
|
|
145
|
])
|
|
146
|
|
|
147
|
# Salsa
|
|
148
|
AC_ARG_ENABLE(salsa, [AS_HELP_STRING([--disable-salsa],
|
|
149
|
[disable Salsa plugin. Enabled by default if available.])])
|
|
150
|
|
|
151
|
AC_MSG_CHECKING(salsa library)
|
|
152
|
AS_IF([ocamlfind query salsa >/dev/null 2>&1],
|
|
153
|
[salsa=yes; AC_MSG_RESULT(yes)],[salsa=no; AC_MSG_WARN(no)]
|
|
154
|
)
|
|
155
|
|
|
156
|
|
|
157
|
AS_IF([test "x$enable_salsa" != "xno"], [
|
|
158
|
if (test "x$salsa" = xyes ); then
|
|
159
|
AC_SUBST(SALSA, "(module Salsa_plugin.Plugin : PluginType.S);")
|
|
160
|
AC_SUBST(SALSA_TAG, "<**/*.native> or <plugins/salsa/*.cm?> : package(salsa)")
|
|
161
|
fi
|
|
162
|
])
|
|
163
|
|
|
164
|
# GMP
|
|
165
|
AC_CHECK_LIB(gmp, __gmpz_init,
|
|
166
|
[gmp=yes],
|
|
167
|
[AC_MSG_RESULT([GNU MP not found])
|
|
168
|
gmp=no])
|
|
169
|
|
|
170
|
AC_CHECK_LIB(mpfr, mpfr_add, [mpfr=yes],
|
|
171
|
[AC_MSG_RESULT(
|
|
172
|
[MPFR not found])
|
|
173
|
mpfr=no])
|
|
174
|
|
|
175
|
# lustresf
|
|
176
|
AC_ARG_ENABLE(lustresf, [AS_HELP_STRING([--disable-lustresf],
|
|
177
|
[disable lustresf compilation. Enabled by default.])])
|
|
178
|
|
|
179
|
AC_SUBST_FILE(lustresf)
|
|
180
|
AC_SUBST_FILE(lustresf_src)
|
|
181
|
lustresf=/dev/null
|
|
182
|
lustresf_src=/dev/null
|
|
183
|
|
|
184
|
AS_IF([test "x$enable_lustresf" != "xno"], [
|
|
185
|
AC_MSG_CHECKING(yojson library for lustresf)
|
|
186
|
AS_IF([ocamlfind query yojson >/dev/null 2>&1],
|
|
187
|
[yojson=yes; AC_MSG_RESULT(yes)],[yojson=no; AC_MSG_ERROR(Yojson required for lustresf. opam install yojson should solve the issue)],
|
|
188
|
)
|
|
189
|
lustresf=Makefile-lustresf.in
|
|
190
|
lustresf_src=src/Makefile-lustresf.in
|
|
191
|
AC_SUBST(lustresf_target, "lustresf")
|
|
192
|
])
|
|
193
|
|
|
194
|
# Checking availability of path to regression tests
|
|
195
|
tests_path="../lustrec-tests/regression_tests"
|
|
196
|
|
|
197
|
AC_ARG_WITH([tests-path],
|
|
198
|
[AS_HELP_STRING([--with-tests-path],
|
|
199
|
[provides path to test suite (default is ../lustrec-test if available)])],
|
|
200
|
[tests_path="$withval";
|
|
201
|
if (test "x$tests_path" = xyes); then
|
|
202
|
AC_MSG_ERROR(Option --with-tests-path requires a parameter: eg. --with-tests-path=value);
|
|
203
|
fi],
|
|
204
|
)
|
|
205
|
AC_MSG_NOTICE($tests_path)
|
|
206
|
AC_CHECK_FILE(${tests_path}/CMakeLists.txt,
|
|
207
|
[
|
|
208
|
valid_test_path=true
|
|
209
|
],
|
|
210
|
[
|
|
211
|
valid_test_path=false
|
|
212
|
AC_SUBST(PATH_TO_TESTS, $tests_path) ])
|
|
213
|
AC_SUBST(PATH_TO_TESTS_DEFINED, $valid_test_path)
|
|
214
|
AC_SUBST(PATH_TO_TESTS, $tests_path)
|
|
215
|
|
|
216
|
# End of config
|
|
217
|
|
|
218
|
AC_DEFUN([AC_DEFINE_DIR], [
|
|
219
|
prefix_NONE=
|
|
220
|
exec_prefix_NONE=
|
|
221
|
test "x$prefix" = xNONE && prefix_NONE=yes && prefix=$ac_default_prefix
|
|
222
|
test "x$exec_prefix" = xNONE && exec_prefix_NONE=yes && exec_prefix=$prefix
|
|
223
|
dnl In Autoconf 2.60, ${datadir} refers to ${datarootdir}, which in turn
|
|
224
|
dnl refers to ${prefix}. Thus we have to use `eval' twice.
|
|
225
|
eval ac_define_dir="\"[$]$2\""
|
|
226
|
eval ac_define_dir="\"$ac_define_dir\""
|
|
227
|
AC_SUBST($1, "$ac_define_dir")
|
|
228
|
AC_DEFINE_UNQUOTED($1, "$ac_define_dir", [$3])
|
|
229
|
test "$prefix_NONE" && prefix=NONE
|
|
230
|
test "$exec_prefix_NONE" && exec_prefix=NONE
|
|
231
|
])
|
|
232
|
|
|
233
|
AC_DEFINE_DIR([abs_datadir], [datadir])
|
|
234
|
|
|
235
|
# Instanciation
|
|
236
|
AC_CONFIG_FILES([opam
|
|
237
|
Makefile
|
|
238
|
src/Makefile
|
|
239
|
src/version.ml
|
|
240
|
src/pluginList.ml
|
|
241
|
src/verifierList.ml
|
|
242
|
src/_tags
|
|
243
|
src/ocaml_utils.ml
|
|
244
|
include/z3librc
|
|
245
|
share/FindLustre.cmake
|
|
246
|
])
|
|
247
|
|
|
248
|
AC_OUTPUT
|
|
249
|
|
|
250
|
|
|
251
|
# summary
|
|
252
|
AC_MSG_NOTICE(******** Configuration ********)
|
|
253
|
AC_MSG_NOTICE(bin path: $prefix/bin)
|
|
254
|
AC_MSG_NOTICE(include path: $prefix/include)
|
|
255
|
AC_MSG_NOTICE(******** Plugins ********)
|
|
256
|
|
|
257
|
if (test "x$gmp" = xyes -a "x$mpfr" = xyes ); then
|
|
258
|
AC_MSG_NOTICE([MPFR option enabled])
|
|
259
|
else
|
|
260
|
AC_MSG_WARN([MPFR option cannot be activated. Requires GMP and MPFR libs])
|
|
261
|
fi
|
|
262
|
|
|
263
|
if (test "x$salsa" = xyes -a "x$enable_salsa" != xno); then
|
|
264
|
AC_MSG_NOTICE([Salsa plugin enabled])
|
|
265
|
else
|
|
266
|
AC_MSG_NOTICE([Salsa plugin disabled])
|
|
267
|
fi
|
|
268
|
|
|
269
|
if (test "x$z3" = xyes -a "x$enable_z3" != xno); then
|
|
270
|
AC_MSG_NOTICE([Z3 dependencies enabled])
|
|
271
|
else
|
|
272
|
AC_MSG_NOTICE([Z3 dependencies disabled])
|
|
273
|
fi
|
|
274
|
|
|
275
|
if (test "x$yojson" = xyes -a "x$enable_lustresf" != "xno"); then
|
|
276
|
AC_MSG_NOTICE([lustresf available])
|
|
277
|
else
|
|
278
|
if (test "x$enable_lustresf" = "xno"); then
|
|
279
|
AC_MSG_NOTICE([lustresf not available (you explicitely disabled it)])
|
|
280
|
else
|
|
281
|
AC_MSG_NOTICE([lustresf not available])
|
|
282
|
fi
|
|
283
|
fi
|
|
284
|
AC_MSG_NOTICE(******** Verifiers ********)
|
|
285
|
|
|
286
|
if (test "x$z3" = xyes -a "x$enable_z3" != xno); then
|
|
287
|
AC_MSG_NOTICE([Zustre enabled])
|
|
288
|
AC_MSG_WARN(Z3 shared lib (libz3.so) has to be available in the LD_LIBRARY_PATH (DYLD_LIBRARY_PATH in OSX).)
|
|
289
|
dnl AC_MSG_WARN(It is currently located in "z3path")
|
|
290
|
AC_MSG_WARN(If not already available run "source ${prefix}/include/lustrec/z3librc")
|
|
291
|
AC_MSG_WARN(or add that line to your ~/.profile or ~/.bashrc)
|
|
292
|
else
|
|
293
|
AC_MSG_NOTICE([Zustre disabled. Require Z3 ocaml library])
|
|
294
|
fi
|
|
295
|
|
|
296
|
if (test "x$seal" = "xyes" -a "x$z3" = xyes -a "x$enable_z3" != xno); then
|
|
297
|
AC_MSG_NOTICE([Seal enabled])
|
|
298
|
else
|
|
299
|
AC_MSG_NOTICE([Seal disabled. Require Z3 library])
|
|
300
|
fi
|
|
301
|
|
|
302
|
|
|
303
|
if (test "x$tiny" = xyes); then
|
|
304
|
AC_MSG_NOTICE([Tiny enabled])
|
|
305
|
else
|
|
306
|
AC_MSG_NOTICE([Tiny disabled. Require Tiny library])
|
|
307
|
fi
|
|
308
|
|
|
309
|
AC_MSG_NOTICE(****** Regression Tests ******)
|
|
310
|
if (test "x$valid_test_path" = xfalse); then
|
|
311
|
AC_MSG_NOTICE(no valid tests path provided ($tests_path))
|
|
312
|
else
|
|
313
|
AC_MSG_NOTICE(tests path: $tests_path)
|
|
314
|
fi
|
|
315
|
AC_MSG_NOTICE(******** Configuration ********)
|
|
316
|
AC_MSG_NOTICE(Execute "make; make install" now)
|