Project

General

Profile

Download (9.87 KB) Statistics
| Branch: | Tag: | Revision:
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
AC_SUBST(VERSION_CODENAME, "Xia/Huai-dev")
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; echo 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, "") # <**/*>: package(seal)")
87
])
88

    
89
# z3 (optional)
90

    
91
AC_ARG_ENABLE(z3, [AS_HELP_STRING([--disable-z3],
92
              [disable Z3 dependencies. Enabled by default if available.])])
93

    
94
# option to rely on github version if installed
95
AC_ARG_WITH(z3_github, [AS_HELP_STRING([--with-z3-github],
96
              [Rely on Z3 as distributed by the official github
97
	       repo rather then the opam distribution. Disabled by default.])])
98

    
99
AS_IF([test "x$with_z3_github" != "xyes"],
100
      [z3name=z3],
101
      [z3name=Z3]
102
      )
103
	
104
AC_MSG_CHECKING(z3 library)
105

    
106

    
107
#define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n']))
108
#define([z3path], esyscmd([opam config var Z3:lib | tr -d '\n']))
109

    
110
AS_IF([ocamlfind query $z3name >/dev/null 2>&1],
111
    [z3=yes; AC_MSG_RESULT([yes])],[zustre=no; AC_MSG_RESULT(no)],
112
)
113

    
114
AS_IF([test "x$enable_z3" != "xno"], [
115
  if (test "x$z3" = xyes ); then
116
   AC_SUBST(LUSTREV_ZUSTRE, "(module Zustre_verifier.Verifier : VerifierType.S);")
117
   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)")
118
   AS_IF([test "x$z3name" = "xZ3"],
119
   	       [define([Z3path], esyscmd([ocamlfind query Z3 | tr -d '\n']))
120
	        AC_SUBST(Z3LIBPATH, "Z3path")],
121
 	       [define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n']))
122
	        AC_SUBST(Z3LIBPATH, "z3path")]
123
		)
124
  fi	
125
])
126

    
127

    
128
# Tiny
129
AC_MSG_CHECKING(tiny library (optional))
130
AS_IF([ocamlfind query tiny >/dev/null 2>&1],
131
    [tiny=yes; AC_MSG_RESULT(yes)],[tiny=no; AC_MSG_RESULT(no)],
132
)
133
AS_IF([test "x$tiny" = "xyes"], [
134
   AC_SUBST(LUSTREV_TINY, "(module Tiny_verifier.Verifier : VerifierType.S);")
135
   AC_SUBST(LUSTREV_TINY_TAG, "<**/*>: package(tiny)")
136
])
137

    
138
# Salsa
139
AC_ARG_ENABLE(salsa, [AS_HELP_STRING([--disable-salsa],
140
              [disable Salsa plugin. Enabled by default if available.])])
141

    
142
AC_MSG_CHECKING(salsa library)
143
AS_IF([ocamlfind query salsa >/dev/null 2>&1],
144
    [salsa=yes; AC_MSG_RESULT(yes)],[salsa=no; AC_MSG_WARN(no)]
145
)
146

    
147

    
148
AS_IF([test "x$enable_salsa" != "xno"], [
149
  if (test "x$salsa" = xyes ); then
150
   AC_SUBST(SALSA, "(module Salsa_plugin.Plugin : PluginType.S);")
151
   AC_SUBST(SALSA_TAG, "<**/*.native> or <plugins/salsa/*.cm?> : package(salsa)")
152
  fi
153
])
154

    
155
# GMP
156
AC_CHECK_LIB(gmp, __gmpz_init,
157
      [gmp=yes],
158
      [AC_MSG_RESULT([GNU MP not found])
159
      gmp=no])
160

    
161
AC_CHECK_LIB(mpfr, mpfr_add, [mpfr=yes],
162
		   [AC_MSG_RESULT(
163
[MPFR not found])
164
mpfr=no])
165

    
166
# lustresf
167
AC_ARG_ENABLE(lustresf, [AS_HELP_STRING([--disable-lustresf],
168
              [disable lustresf compilation. Enabled by default.])])
169

    
170
AC_SUBST_FILE(lustresf)
171
AC_SUBST_FILE(lustresf_src)
172
lustresf=/dev/null
173
lustresf_src=/dev/null
174

    
175
AS_IF([test "x$enable_lustresf" != "xno"], [
176
  AC_MSG_CHECKING(yojson library for lustresf)
177
  AS_IF([ocamlfind query yojson >/dev/null 2>&1],
178
      [yojson=yes; AC_MSG_RESULT(yes)],[yojson=no; AC_MSG_ERROR(Yojson required for lustresf. opam install yojson should solve the issue)],
179
  )
180
  lustresf=Makefile-lustresf.in
181
  lustresf_src=src/Makefile-lustresf.in
182
  AC_SUBST(lustresf_target, "lustresf")
183
])
184

    
185
# Checking availability of path to regression tests
186
tests_path="../lustrec-tests/regression_tests"
187

    
188
AC_ARG_WITH([tests-path],
189
            [AS_HELP_STRING([--with-tests-path],
190
               [provides path to test suite (default is ../lustrec-test if available)])],
191
            [tests_path="$withval";
192
	     if (test "x$tests_path" = xyes); then
193
	       AC_MSG_ERROR(Option --with-tests-path requires a parameter: eg. --with-tests-path=value);
194
	     fi],
195
            )
196
AC_MSG_NOTICE($tests_path)
197
AC_CHECK_FILE(${tests_path}/CMakeLists.txt,
198
              [
199
	      valid_test_path=true
200
	      ],
201
	      [
202
	      valid_test_path=false
203
	        AC_SUBST(PATH_TO_TESTS, $tests_path)	      ])
204
AC_SUBST(PATH_TO_TESTS_DEFINED, $valid_test_path)
205
AC_SUBST(PATH_TO_TESTS, $tests_path)
206

    
207
# End of config
208

    
209
AC_DEFUN([AC_DEFINE_DIR], [
210
  prefix_NONE=
211
  exec_prefix_NONE=
212
  test "x$prefix" = xNONE && prefix_NONE=yes && prefix=$ac_default_prefix
213
  test "x$exec_prefix" = xNONE && exec_prefix_NONE=yes && exec_prefix=$prefix
214
dnl In Autoconf 2.60, ${datadir} refers to ${datarootdir}, which in turn
215
dnl refers to ${prefix}.  Thus we have to use `eval' twice.
216
  eval ac_define_dir="\"[$]$2\""
217
  eval ac_define_dir="\"$ac_define_dir\""
218
  AC_SUBST($1, "$ac_define_dir")
219
  AC_DEFINE_UNQUOTED($1, "$ac_define_dir", [$3])
220
  test "$prefix_NONE" && prefix=NONE
221
  test "$exec_prefix_NONE" && exec_prefix=NONE
222
])
223

    
224
AC_DEFINE_DIR([abs_datadir], [datadir])
225

    
226
# Instanciation
227
AC_CONFIG_FILES([opam
228
		 Makefile
229
		 src/Makefile
230
		 src/version.ml
231
		 src/pluginList.ml
232
		 src/verifierList.ml
233
		 src/_tags
234
		 src/ocaml_utils.ml
235
		 include/z3librc
236
		 share/FindLustre.cmake
237
		 ])
238

    
239
AC_OUTPUT
240

    
241

    
242
# summary
243
AC_MSG_NOTICE(******** Configuration ********)
244
AC_MSG_NOTICE(bin path:     $prefix/bin)
245
AC_MSG_NOTICE(include path: $prefix/include)
246
AC_MSG_NOTICE(********    Plugins    ********)
247

    
248
  if (test "x$gmp" = xyes -a "x$mpfr" = xyes ); then
249
      AC_MSG_NOTICE([MPFR option enabled])
250
  else
251
      AC_MSG_WARN([MPFR option cannot be activated. Requires GMP and MPFR libs])
252
  fi
253

    
254
  if (test "x$salsa" = xyes -a "x$enable_salsa" != xno); then
255
      AC_MSG_NOTICE([Salsa plugin enabled])
256
  else
257
      AC_MSG_NOTICE([Salsa plugin disabled])
258
  fi
259

    
260
  if (test "x$z3" = xyes -a "x$enable_z3" != xno); then
261
      AC_MSG_NOTICE([Z3 dependencies enabled])
262
  else
263
      AC_MSG_NOTICE([Z3 dependencies disabled])
264
  fi
265

    
266
  if (test "x$yojson" = xyes -a "x$enable_lustresf" != "xno"); then
267
      AC_MSG_NOTICE([lustresf available])
268
  else
269
      if (test "x$enable_lustresf" = "xno"); then
270
        AC_MSG_NOTICE([lustresf not available (you explicitely disabled it)])
271
      else
272
        AC_MSG_NOTICE([lustresf not available])
273
      fi
274
  fi
275
AC_MSG_NOTICE(********   Verifiers    ********)
276

    
277
  if (test "x$z3" = xyes  -a "x$enable_z3" != xno); then
278
      AC_MSG_NOTICE([Zustre enabled])
279
      AC_MSG_WARN(Z3 shared lib (libz3.so) has to be available in the LD_LIBRARY_PATH (DYLD_LIBRARY_PATH in OSX).)
280
      dnl AC_MSG_WARN(It is currently located in "z3path")
281
      AC_MSG_WARN(If not already available run "source ${prefix}/include/lustrec/z3librc")
282
      AC_MSG_WARN(or add that line to your ~/.profile or ~/.bashrc)
283
else
284
      AC_MSG_NOTICE([Zustre disabled. Require Z3 ocaml library])
285
  fi
286

    
287
if (test "x$seal" = "xyes" -a "x$z3" = xyes  -a "x$enable_z3" != xno); then
288
      AC_MSG_NOTICE([Seal   enabled])
289
  else
290
      AC_MSG_NOTICE([Seal   disabled. Require Z3 library])
291
  fi
292

    
293

    
294
  if (test "x$tiny" = xyes); then
295
      AC_MSG_NOTICE([Tiny   enabled])
296
  else
297
      AC_MSG_NOTICE([Tiny   disabled. Require Tiny library])
298
  fi
299

    
300
AC_MSG_NOTICE(****** Regression Tests  ******)
301
if (test "x$valid_test_path" = xfalse); then
302
  AC_MSG_NOTICE(no valid tests path provided ($tests_path))
303
else
304
AC_MSG_NOTICE(tests path: $tests_path)
305
fi
306
AC_MSG_NOTICE(******** Configuration ********)
307
AC_MSG_NOTICE(Execute "make; make install" now)
(14-14/17)