Project

General

Profile

« Previous | Next » 

Revision 9c4cc944

Added by Corentin Lauverjat over 1 year ago

Transition to dune build system
Improvement of opam integration
Dockerfile based on Alpine
Dockerfile based on Ubuntu
Update the README.md

View differences:

configure.ac
2 2

  
3 3
AC_INIT([lustrec], 1.7-gitversion, [ploc@garoche.net])
4 4
AC_SUBST(VERSION_NUMBER, 1.7)
5
AC_SUBST(VERSION_CODENAME, "Xia/Huai-dev")
6 5

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

  
13
if test -z "$share"; then
14
  share="$ac_pwd/_build/default/include"
15
fi
16

  
17
AC_SUBST(SHARE_PATH, $share)
18

  
15 19
# Next release will be
16 20
#AC_INIT([lustrec], [1.8], [ploc@garoche.net])
17
#AC_SUBST(VERSION_CODENAME, "Xia/Mang")
18
AC_MSG_NOTICE(Git branch: ${GITBRANCH})
21
AC_MSG_NOTICE(Git branch: [$gitbranch])
19 22
AC_CONFIG_SRCDIR([src/main_lustre_compiler.ml])
20 23
AC_CONFIG_SRCDIR([src/main_lustre_testgen.ml])
21 24

  
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 25
# 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)
26
AC_PREFIX_DEFAULT(./_build/install/default)
72 27

  
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, "<**/*>: 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.])])
28
# Configuration
29
AC_MSG_NOTICE(******** Configuration ********)
30
AC_MSG_NOTICE(bin path:     $prefix/bin)
31
AC_MSG_NOTICE(share path: $prefix/share)
102 32

  
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 33

  
108
AS_IF([test "x$with_z3_github" != "xyes"],
109
      [z3name=z3],
110
      [z3name=Z3]
111
      )
112
	
113
AC_MSG_CHECKING(z3 library)
34
# Seal plugin feature
114 35

  
36
AC_ARG_ENABLE(seal, 
37
  [AS_HELP_STRING([--disable-seal],[disable the seal plugin. Enabled by default if available.])
38
   AS_HELP_STRING([--enable-seal],[enable the seal plugin. Enabled if available by default.])])
115 39

  
116
#define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n']))
117
#define([z3path], esyscmd([opam config var Z3:lib | tr -d '\n']))
118 40

  
119
AS_IF([ocamlfind query $z3name >/dev/null 2>&1],
120
    [z3=yes; AC_MSG_RESULT([yes])],[zustre=no; AC_MSG_RESULT(no)],
41
AS_IF([test "x$enable_seal" != "xno"],
42
  [
43
    if (test -z "$(dune external-lib-deps --missing plugins/seal 2>&1 | cat)" ); then
44
      AC_MSG_RESULT([seal plugin : enabled])
45
      AC_SUBST(LUSTREV_SEAL, ["(module Seal_plugin.Seal_verifier.Verifier : Lustrec.VerifierType.S);"])
46
      AC_SUBST(SEAL_PLUGIN_NAME, ["seal_plugin"])
47
    else
48
      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/, $//')].])
49
      if (test "x$enable_seal" == "xyes" ); then
50
        AC_MSG_ERROR([Cannot enable the seal plugin!])
51
      fi
52
    fi
53
  ], 
54
  [AC_MSG_RESULT([seal plugin : disabled (you explicitely disabled it)])]
121 55
)
122 56

  
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
])
57
# Zustre plugin feature
58
AC_ARG_ENABLE(zustre, 
59
  [AS_HELP_STRING([--disable-zustre],[disable the Zustre plugin. Enabled by default if available.])
60
   AS_HELP_STRING([--enable-zustre],[enable the Zustre plugin. Enabled if available by default.])])
61

  
62
AS_IF([test "x$enable_zustre" != "xno"],
63
  [
64
    if (test -z "$(dune external-lib-deps --missing plugins/zustre 2>&1 | cat)" ); then
65
      AC_MSG_RESULT([zustre plugin : enabled])
66
      AC_SUBST(LUSTREV_ZUSTRE, ["(module Zustre_plugin.Zustre_verifier.Verifier : Lustrec.VerifierType.S);"])
67
      AC_SUBST(ZUSTRE_PLUGIN_NAME, ["zustre_plugin"])
68
      AC_SUBST(Z3LIBPATH, [`ocamlfind query z3 | tr -d '\n'`])
69
    else
70
      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/, $//')].])
71
      if (test "x$enable_zustre" == "xyes" ); then
72
        AC_MSG_ERROR([Cannot enable the zustre plugin!])
73
      fi
74
    fi
75
  ], 
76
  [AC_MSG_RESULT([zustre plugin disabled (you explicitely disabled it)])]
77
)
146 78

  
147
# Salsa
148
AC_ARG_ENABLE(salsa, [AS_HELP_STRING([--disable-salsa],
149
              [disable Salsa plugin. Enabled by default if available.])])
79
# Tiny plugin feature
80
AC_ARG_ENABLE(tiny, 
81
  [AS_HELP_STRING([--disable-tiny],[disable the Tiny plugin. Enabled by default if available.])
82
   AS_HELP_STRING([--enable-tiny],[enable the Tiny plugin. Enabled if available by default.])])
83

  
84
AS_IF([test "x$enable_tiny" != "xno"], [
85
  if (test -z "$(dune external-lib-deps --missing plugins/tiny 2>&1 | cat)" ); then
86
      AC_MSG_RESULT([tiny plugin : enabled])
87
      AC_SUBST(LUSTREV_TINY, ["(module Tiny_plugin.Tiny_verifier.Verifier : Lustrec.VerifierType.S);"])
88
      AC_SUBST(TINY_PLUGIN_NAME, ["tiny_plugin"])
89
    else
90
      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/, $//')].])
91
      if (test "x$enable_tiny" == "xyes" ); then
92
        AC_MSG_ERROR([Cannot enable the tiny plugin!])
93
      fi
94
    fi
95
],
96
  [AC_MSG_RESULT([tiny plugin : disabled (you explicitely disabled it)])])
150 97

  
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
)
98
# Salsa plugin feature
99
AC_ARG_ENABLE(salsa, 
100
  [AS_HELP_STRING([--disable-salsa],[disable the salsa plugin. Enabled by default if available.])
101
   AS_HELP_STRING([--enable-salsa],[enable the salsa plugin. Enabled if available by default.])])
155 102

  
156 103

  
157 104
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
])
105
  if (test -z "$(dune external-lib-deps --missing plugins/salsa 2>&1 | cat)" ); then
106
      AC_MSG_RESULT([salsa plugin : enabled])
107
      AC_SUBST(SALSA, ["(module Salsa_plugin.Plugin : Lustrec.PluginType.S);"])
108
      AC_SUBST(SALSA_PLUGIN_NAME, ["salsa_plugin"])
109
    else
110
      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/, $//')].])
111
      if (test "x$enable_salsa" == "xyes" ); then
112
        AC_MSG_ERROR([Cannot enable the salsa plugin!])
113
      fi
114
    fi
115
],
116
  [AC_MSG_RESULT([salsa plugin : disabled (you explicitely disabled it)])])
117

  
163 118

  
164 119
# GMP
165 120
AC_CHECK_LIB(gmp, __gmpz_init,
166 121
      [gmp=yes],
167 122
      [AC_MSG_RESULT([GNU MP not found])
168 123
      gmp=no])
169

  
124
#MPFR
170 125
AC_CHECK_LIB(mpfr, mpfr_add, [mpfr=yes],
171 126
		   [AC_MSG_RESULT(
172 127
[MPFR not found])
173 128
mpfr=no])
174 129

  
175
# lustresf
176
AC_ARG_ENABLE(lustresf, [AS_HELP_STRING([--disable-lustresf],
177
              [disable lustresf compilation. Enabled by default.])])
178 130

  
179 131
AC_SUBST_FILE(lustresf)
180 132
AC_SUBST_FILE(lustresf_src)
181 133
lustresf=/dev/null
182 134
lustresf_src=/dev/null
183 135

  
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
])
136

  
137
lustresf=Makefile-lustresf.in
138
lustresf_src=src/Makefile-lustresf.in
139
AC_SUBST(lustresf_target, "lustresf")
140

  
193 141

  
194 142
# Checking availability of path to regression tests
195 143
tests_path="../lustrec-tests/regression_tests"
......
233 181
AC_DEFINE_DIR([abs_datadir], [datadir])
234 182

  
235 183
# Instanciation
236
AC_CONFIG_FILES([opam
184
AC_CONFIG_FILES([
237 185
		 Makefile
238
		 src/Makefile
239
		 src/version.ml
240
		 src/pluginList.ml
186
     src/dune
187
     plugins/zustre/dune
188
     src/pluginList.ml
241 189
		 src/verifierList.ml
242
		 src/_tags
243
		 src/ocaml_utils.ml
244
		 include/z3librc
190
     lib/version.ml
245 191
		 share/FindLustre.cmake
246 192
		 ])
247 193

  
248 194
AC_OUTPUT
249 195

  
250 196

  
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 197

  
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 198

  
309 199
AC_MSG_NOTICE(****** Regression Tests  ******)
310 200
if (test "x$valid_test_path" = xfalse); then

Also available in: Unified diff