Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / configure.ac @ ec8fc65e

History | View | Annotate | Download (9.15 KB)

1
define([gitversion], esyscmd([sh -c "git log --oneline | wc -l | tr -d '\n'"]))
2
define([gitbranch], esyscmd([sh -c "git branch | grep \* | cut -d ' ' -f2"]))
3
AC_INIT([lustrec], 1.6-gitversion, [ploc@garoche.net])
4
AC_SUBST(VERSION_CODENAME, "Xia/Zhu-dev")
5
AC_SUBST(GITBRANCH, gitbranch)
6
# Next release will be
7
#AC_INIT([lustrec], [1.7], [ploc@garoche.net])
8
#AC_SUBST(VERSION_CODENAME, "Xia/Huai")
9
AC_MSG_NOTICE(Git branch: ${GITBRANCH})
10
AC_CONFIG_SRCDIR([src/main_lustre_compiler.ml])
11
AC_CONFIG_SRCDIR([src/main_lustre_testgen.ml])
12

    
13
AC_PATH_PROG([OCAMLC],[ocamlc],[:])
14
AC_MSG_CHECKING(OCaml version)
15
ocamlc_version=`$OCAMLC -v | grep version | rev| cut -d \  -f 1 | rev`
16
major=`echo $ocamlc_version | cut -d . -f 1`
17
minor=`echo $ocamlc_version | cut -d . -f 2`
18
if (test "$major" -lt 3 -a "$minor" -lt 11 ); then
19
  AC_MSG_ERROR([Ocaml version must be at least 3.11. You have version $ocamlc_version])
20
fi
21
AC_MSG_RESULT(valid ocaml version detected: $ocamlc_version)
22

    
23
AC_PATH_PROG([OCAMLBUILD],[ocamlbuild],[:])
24

    
25
# Handle a mismatch in available function btw 4.02 and 4.04
26
if (test $"$major" -eq 4 -a "$minor" -gt 2); then
27
   AC_SUBST(UPPERCASEFUN, "String.uppercase_ascii")
28
else
29
   AC_SUBST(UPPERCASEFUN, "String.uppercase")
30
fi
31

    
32
# default prefix is /usr/local
33
AC_PREFIX_DEFAULT(/usr/local)
34

    
35
dnl AC_ARG_WITH([ocamlgraph-path],
36
dnl         [AS_HELP_STRING([--ocamlgraph-path],
37
dnl               [specify the path of ocamlgraph library. graph.cmxa should be in ocamlgraph-path @<:@default=$(ocamlfind query ocamlgraph)@:>@])],
38
dnl         [AS_IF([test "x$ocamlgraph_path" = xno],
39
dnl                 [AC_MSG_ERROR([ocamlgraph library is needed])],
40
dnl                 [test "x$ocamlgraph_path" = xyes],
41
dnl                 [OCAMLGRAPH_PATH=$(ocamlfind query ocamlgraph)],
42
dnl                 [OCAMLGRAPH_PATH=$ocamlgraph_path]
43
dnl         )],
44
dnl         [OCAMLGRAPH_PATH=$(ocamlfind query ocamlgraph)]
45
dnl )
46
dnl AC_SUBST(OCAMLGRAPH_PATH)
47

    
48

    
49
# Checking libs
50
AC_CHECK_PROG(FINDLIB_CHECK,ocamlfind,yes)
51
if test x"$FINDLIB_CHECK" != x"yes" ; then
52
   AC_MSG_ERROR(ocamlfind required!)
53
fi
54
dnl AC_MSG_RESULT(Hourrah: ocamlfind found!)
55

    
56
# Checks for libraries.
57
# OCamlgraph
58
AC_MSG_CHECKING(ocaml libraries required (ocamlgraph cmdliner fmt logs num)) 
59
AS_IF([ocamlfind query ocamlgraph cmdliner fmt logs num >/dev/null 2>&1],
60
    [],[AC_MSG_ERROR(A few ocaml library required. opam install ocamlgraph cmdliner fmt logs num should solve the issue)],
61
)
62
AC_MSG_RESULT(yes)
63

    
64
#Yojson
65
AC_MSG_CHECKING(yojson library (optional))
66
AS_IF([ocamlfind query yojson >/dev/null 2>&1],
67
    [yojson=yes; AC_MSG_RESULT(yes)],[yojson=no; AC_MSG_WARN(Yojson required for lustresf. opam install yojson should solve the issue)],
68
)
69

    
70
# Seal
71
AC_MSG_CHECKING(seal library (optional))
72
AS_IF([ocamlfind query seal >/dev/null 2>&1],
73
    [seal=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)],
74
)
75
AS_IF([test "x$seal" = "xyes"], [
76
   AC_SUBST(LUSTREV_SEAL, "(module Seal_verifier.Verifier : VerifierType.S);")
77
   AC_SUBST(LUSTREV_SEAL_TAG, "<**/*>: package(seal)")
78
])
79

    
80
# z3 (optional)
81

    
82
# option to rely on github version if installed
83
AC_ARG_WITH(z3_github, [AS_HELP_STRING([--with-z3-github],
84
              [Rely on Z3 as distributed by the official github
85
	       repo rather then the opam distribution. Disabled by default.])])
86

    
87
AS_IF([test "x$with_z3_github" != "xyes"],
88
      [z3name=z3],
89
      [z3name=Z3]
90
      )
91
	
92
AC_MSG_CHECKING(z3 library)
93

    
94

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

    
98
AS_IF([ocamlfind query $z3name >/dev/null 2>&1],
99
    [z3=yes; AC_MSG_RESULT([yes])],[zustre=no; AC_MSG_RESULT(no)],
100
)
101
AS_IF([test "x$z3" = "xyes"], [
102
   AC_SUBST(LUSTREV_ZUSTRE, "(module Zustre_verifier.Verifier : VerifierType.S);")
103
   AC_SUBST(LUSTREV_Z3_TAG, "<**/*>: package($z3name)")
104
   AS_IF([test "x$z3name" = "xZ3"],
105
   	       [define([Z3path], esyscmd([ocamlfind query Z3 | tr -d '\n']))
106
	        AC_SUBST(Z3LIBPATH, "Z3path")],
107
 	       [define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n']))
108
	        AC_SUBST(Z3LIBPATH, "z3path")]
109
		)
110
])
111

    
112

    
113

    
114

    
115
# Tiny
116
AC_MSG_CHECKING(tiny library (optional))
117
AS_IF([ocamlfind query tiny >/dev/null 2>&1],
118
    [tiny=yes; AC_MSG_RESULT(yes)],[tiny=no; AC_MSG_RESULT(no)],
119
)
120
AS_IF([test "x$tiny" = "xyes"], [
121
   AC_SUBST(LUSTREV_TINY, "(module Tiny_verifier.Verifier : VerifierType.S);")
122
   AC_SUBST(LUSTREV_TINY_TAG, "<**/*>: package(tiny)")
123
])
124

    
125
# Salsa
126
AC_ARG_ENABLE(salsa, [AS_HELP_STRING([--disable-salsa],
127
              [disable Salsa plugin. Enabled by default if available.])])
128

    
129
AC_MSG_CHECKING(salsa library)
130
AS_IF([ocamlfind query salsa >/dev/null 2>&1],
131
    [salsa=yes; AC_MSG_RESULT(yes)],[salsa=no; AC_MSG_WARN(no)]
132
)
133

    
134

    
135
AS_IF([test "x$enable_salsa" != "xno"], [
136
  if (test "x$salsa" = xyes ); then
137
   AC_SUBST(SALSA, "(module Salsa_plugin.Plugin : PluginType.S);")
138
   AC_SUBST(SALSA_TAG, "<**/*.native> or <plugins/salsa/*.cm?> : package(salsa)")
139
  fi
140
])
141

    
142
# GMP
143
AC_CHECK_LIB(gmp, __gmpz_init,
144
      [gmp=yes],
145
      [AC_MSG_RESULT([GNU MP not found])
146
      gmp=no])
147

    
148
AC_CHECK_LIB(mpfr, mpfr_add, [mpfr=yes],
149
		   [AC_MSG_RESULT(
150
[MPFR not found])
151
mpfr=no])
152

    
153
# lustresf
154
AC_ARG_ENABLE(lustresf, [AS_HELP_STRING([--disable-lustresf],
155
              [disable lustresf compilation. Enabled by default.])])
156

    
157
AC_SUBST_FILE(lustresf)
158
AC_SUBST_FILE(lustresf_src)
159
lustresf=/dev/null
160
lustresf_src=/dev/null
161

    
162
AS_IF([test "x$enable_lustresf" != "xno"], [
163
  AC_MSG_CHECKING(yojson library for lustresf)
164
  AS_IF([ocamlfind query yojson >/dev/null 2>&1],
165
      [yojson=yes; AC_MSG_RESULT(yes)],[yojson=no; AC_MSG_ERROR(Yojson required for lustresf. opam install yojson should solve the issue)],
166
  )
167
  lustresf=Makefile-lustresf.in
168
  lustresf_src=src/Makefile-lustresf.in
169
  AC_SUBST(lustresf_target, "lustresf")
170
])
171

    
172
# Checking availability of path to regression tests
173
tests_path="../lustrec-tests/regression_tests"
174

    
175
AC_ARG_WITH([tests-path],
176
            [AS_HELP_STRING([--with-tests-path],
177
               [provides path to test suite (default is ../lustrec-test if available)])],
178
            [tests_path="$withval";
179
	     if (test "x$tests_path" = xyes); then
180
	       AC_MSG_ERROR(Option --with-tests-path requires a parameter: eg. --with-tests-path=value);
181
	     fi],
182
            )
183
AC_MSG_NOTICE($tests_path)
184
AC_CHECK_FILE(${tests_path}/CMakeLists.txt,
185
              [
186
	      valid_test_path=true
187
	      ],
188
	      [
189
	      valid_test_path=false
190
	        AC_SUBST(PATH_TO_TESTS, $tests_path)	      ])
191
AC_SUBST(PATH_TO_TESTS_DEFINED, $valid_test_path)
192
AC_SUBST(PATH_TO_TESTS, $tests_path)
193

    
194
# End of config
195

    
196
AC_DEFUN([AC_DEFINE_DIR], [
197
  prefix_NONE=
198
  exec_prefix_NONE=
199
  test "x$prefix" = xNONE && prefix_NONE=yes && prefix=$ac_default_prefix
200
  test "x$exec_prefix" = xNONE && exec_prefix_NONE=yes && exec_prefix=$prefix
201
dnl In Autoconf 2.60, ${datadir} refers to ${datarootdir}, which in turn
202
dnl refers to ${prefix}.  Thus we have to use `eval' twice.
203
  eval ac_define_dir="\"[$]$2\""
204
  eval ac_define_dir="\"$ac_define_dir\""
205
  AC_SUBST($1, "$ac_define_dir")
206
  AC_DEFINE_UNQUOTED($1, "$ac_define_dir", [$3])
207
  test "$prefix_NONE" && prefix=NONE
208
  test "$exec_prefix_NONE" && exec_prefix=NONE
209
])
210

    
211
AC_DEFINE_DIR([abs_datadir], [datadir])
212

    
213
# Instanciation
214
AC_CONFIG_FILES([Makefile
215
		 src/Makefile
216
		 src/version.ml
217
		 src/pluginList.ml
218
		 src/verifierList.ml
219
		 src/_tags
220
		 src/ocaml_utils.ml
221
		 include/z3librc
222
		 ])
223

    
224
AC_OUTPUT
225

    
226

    
227
# summary
228
AC_MSG_NOTICE(******** Configuration ********)
229
AC_MSG_NOTICE(bin path:     $prefix/bin)
230
AC_MSG_NOTICE(include path: $prefix/include)
231
AC_MSG_NOTICE(********    Plugins    ********)
232

    
233
  if (test "x$gmp" = xyes -a "x$mpfr" = xyes ); then
234
      AC_MSG_NOTICE([MPFR option enabled])
235
  else
236
      AC_MSG_WARN([MPFR option cannot be activated. Requires GMP and MPFR libs])
237
  fi
238

    
239
  if (test "x$salsa" = xyes -a "x$enable_salsa" != xno); then
240
      AC_MSG_NOTICE([Salsa plugin enabled])
241
  else
242
      AC_MSG_NOTICE([Salsa plugin disabled])
243
  fi
244

    
245
  if (test "x$yojson" = xyes -a "x$enable_lustresf" != "xno"); then
246
      AC_MSG_NOTICE([lustresf available])
247
  else
248
      if (test "x$enable_lustresf" = "xno"); then
249
        AC_MSG_NOTICE([lustresf not available (you explicitely disabled it)])
250
      else
251
        AC_MSG_NOTICE([lustresf not available])
252
      fi
253
  fi
254
AC_MSG_NOTICE(********   Verifiers    ********)
255

    
256
  if (test "x$seal" = "xyes"); then
257
      AC_MSG_NOTICE([Seal   enabled])
258
  else
259
      AC_MSG_NOTICE([Seal   disabled. Require Seal library])
260
  fi
261

    
262
  if (test "x$z3" = xyes); then
263
      AC_MSG_NOTICE([Zustre enabled])
264
      AC_MSG_WARN(Z3 shared lib (libz3.so) has to be available in the LD_LIBRARY_PATH.)
265
      dnl AC_MSG_WARN(It is currently located in "z3path")
266
      AC_MSG_WARN(If not already available run "source ${prefix}/include/lustrec/z3librc")
267
      AC_MSG_WARN(or add that line to your ~/.profile or ~/.bashrc)
268
else
269
      AC_MSG_NOTICE([Zustre disabled. Require Z3 ocaml library])
270
  fi
271

    
272
  if (test "x$tiny" = xyes); then
273
      AC_MSG_NOTICE([Tiny   enabled])
274
  else
275
      AC_MSG_NOTICE([Tiny   disabled. Require Tiny library])
276
  fi
277

    
278
AC_MSG_NOTICE(****** Regression Tests  ******)
279
if (test "x$valid_test_path" = xfalse); then
280
  AC_MSG_NOTICE(no valid tests path provided ($tests_path))
281
else
282
AC_MSG_NOTICE(tests path: $tests_path)
283
fi
284
AC_MSG_NOTICE(******** Configuration ********)
285
AC_MSG_NOTICE(Execute "make; make install" now)