Revision f0195e96
Added by Pierre-Loïc Garoche over 3 years ago
| configure.ac | ||
|---|---|---|
| 78 | 78 |
|
| 79 | 79 |
# Seal |
| 80 | 80 |
AC_MSG_CHECKING(seal library (optional)) |
| 81 |
AS_IF([ocamlfind query seal >/dev/null 2>&1; echo 1],
|
|
| 81 |
AS_IF([ocamlfind query seal >/dev/null 2>&1], |
|
| 82 | 82 |
[seal=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)], |
| 83 | 83 |
) |
| 84 | 84 |
AS_IF([test "x$seal" = "xyes"], [ |
| 85 | 85 |
AC_SUBST(LUSTREV_SEAL, "(module Seal_verifier.Verifier : VerifierType.S);") |
| 86 |
AC_SUBST(LUSTREV_SEAL_TAG, "") # <**/*>: package(seal)") |
|
| 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)") |
|
| 87 | 96 |
]) |
| 88 | 97 |
|
| 89 | 98 |
# z3 (optional) |
| ... | ... | |
| 125 | 134 |
]) |
| 126 | 135 |
|
| 127 | 136 |
|
| 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 |
) |
|
| 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 )
|
|
| 133 | 142 |
AS_IF([test "x$tiny" = "xyes"], [ |
| 134 | 143 |
AC_SUBST(LUSTREV_TINY, "(module Tiny_verifier.Verifier : VerifierType.S);") |
| 135 |
AC_SUBST(LUSTREV_TINY_TAG, "<**/*>: package(tiny)")
|
|
| 144 |
AC_SUBST(LUSTREV_TINY_TAG, ["<**/*>: package(apron.boxMPQ), package(apron.octMPQ), package(apron.polkaMPQ), package(tiny)"])
|
|
| 136 | 145 |
]) |
| 137 | 146 |
|
| 138 | 147 |
# Salsa |
Also available in: Unified diff
- Primitive Tiny backend
- Renamed Mpfr to lustrec_mpfr
- Introduced dependency in Zarith. Trying to move away from Num