-
Notifications
You must be signed in to change notification settings - Fork 1
/
configure.ac
157 lines (138 loc) · 5.73 KB
/
configure.ac
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
# -*- Autoconf -*-
# Process this file with autoconf to produce a configure script.
AC_PREREQ(2.59)
AC_INIT([ValidSDP], [1.0.2-git])
AC_CONFIG_SRCDIR([theories/validsdp.v])
AC_DEFUN([AX_VERSION_GE], [AS_VERSION_COMPARE([$1],[$2],[$4],[$3],[$3])])
# Check for programs
AC_CHECK_TOOL([OCAMLC], [ocamlc], [no])
AS_IF([test "x$OCAMLC" = xno], [AC_MSG_ERROR([Cannot find ocamlc.])])
AC_CHECK_TOOL([COQC], [coqc], [no])
AS_IF([test "x$COQC" = xno], [AC_MSG_ERROR([Cannot find coqc.])])
AC_MSG_CHECKING(Coq version)
coq_version=`$COQC -v | grep version | sed -e 's/^.*version \([[0-9.+a-z]]*\).*$/\1/'`
AC_MSG_RESULT($coq_version)
AX_VERSION_GE([$coq_version], 8.16, [],
[ AC_MSG_ERROR([must be at least 8.16.]) ])
AC_CHECK_TOOL([OCAMLFIND], [ocamlfind], [no])
AS_IF([test "x$OCAMLFIND" = xno], [AC_MSG_ERROR([Cannot find ocamlfind.])])
# Check for libraries
AC_MSG_CHECKING([for Ltac2])
COQTOP_WHERE=`coqtop -where`
LTAC2_DIR="${COQTOP_WHERE}-core/plugins/ltac2"
AS_IF([test -d ${LTAC2_DIR}],
[ AC_MSG_RESULT([yes]) ],
[ AC_MSG_RESULT([no])
AC_MSG_ERROR([ *** Unable to find Ltac2 which should be installed with Coq])])
COQ_VERSION="v816"
SOSWIT_PLUGIN_EXT="soswitness"
SOSWIT_PLUGIN="soswitness:coq-validsdp.plugin"
META_FILE="plugins/soswitness/src/META.coq-validsdp"
CAMLPKGS="-package coq-core.plugins.ltac2 \
-package zarith \
-package logs \
-package ocplib-simplex \
-package osdp"
AX_VERSION_GE([$coq_version], 8.18,
[COQ_VERSION="v818"; SOSWIT_PLUGIN_EXT="coq-validsdp.plugin"], [])
AC_SUBST(COQ_VERSION)
AC_SUBST(SOSWIT_PLUGIN)
AC_SUBST(SOSWIT_PLUGIN_EXT)
AC_SUBST(META_FILE)
AC_SUBST(CAMLPKGS)
AC_MSG_CHECKING([for Mathcomp])
AS_IF(
[ echo "From mathcomp Require Import rat matrix countalg." > conftest.v
$COQC conftest.v > conftest.err ],
[ AC_MSG_RESULT([yes]) ],
[ AC_MSG_RESULT([no])
AC_MSG_ERROR([ *** Unable to find theories rat, matrix, countalg from coq-mathcomp-field])])
rm -f conftest.v conftest.vo conftest.err
AC_MSG_CHECKING([for Mathcomp Analysis])
AS_IF(
[ echo "Require Import mathcomp.analysis.Rstruct." > conftest.v
$COQC conftest.v > conftest.err ],
[ AC_MSG_RESULT([yes]) ],
[ AC_MSG_RESULT([no])
AC_MSG_ERROR([ *** Unable to find theory Rstruct from coq-mathcomp-analysis])])
rm -f conftest.v conftest.vo conftest.err
AC_MSG_CHECKING([for Flocq])
AS_IF(
[ echo "Require Import Flocq.Version BinNat." \
"Goal (30100 <= Flocq_version)%N. easy. Qed." > conftest.v
$COQC conftest.v > conftest.err ],
[ AC_MSG_RESULT([yes]) ],
[ AC_MSG_RESULT([no])
AC_MSG_ERROR([ *** Unable to find library Flocq >= 3.3 (http://flocq.gforge.inria.fr/)])])
rm -f conftest.v conftest.vo conftest.err
AC_MSG_CHECKING([for Coq-interval])
AS_IF(
[ echo "From Interval Require Import Real.Xreal. " \
"From Interval Require Import Float.Basic. " \
"From Interval Require Import Float.Sig. " \
"Declare Module F : FloatOps. " \
"Check F.add_UP_correct." > conftest.v
$COQC conftest.v > conftest.err ],
[ AC_MSG_RESULT([yes]) ],
[ AC_MSG_RESULT([no])
AC_MSG_ERROR([ *** Unable to find library Coq-interval master (http://coq-interval.gforge.inria.fr/)])])
rm -f conftest.v conftest.vo conftest.err
if test "$libdir" = '${exec_prefix}/lib'; then
libdir="`$COQC -where`/user-contrib/Interval"
fi
AC_MSG_CHECKING([for Multinomials])
AS_IF(
[ echo "From mathcomp Require Import ssreflect ssrfun." \
"From mathcomp.multinomials Require Import mpoly freeg." > conftest.v
$COQC conftest.v > conftest.err ],
[ AC_MSG_RESULT([yes]) ],
[ AC_MSG_RESULT([no])
AC_MSG_ERROR([ *** Unable to find library Multinomials >= 1.0 (https://github.com/math-comp/multinomials/)])])
rm -f conftest.v conftest.vo conftest.err
AC_MSG_CHECKING([for CoqEAL])
AS_IF(
[ echo "From CoqEAL.refinements Require Import hrel refinements param binord binnat binint rational binrat multipoly." > conftest.v
$COQC conftest.v > conftest.err ],
[ AC_MSG_RESULT([yes]) ],
[ AC_MSG_RESULT([no])
AC_MSG_ERROR([ *** Unable to find library CoqEAL (https://github.com/CoqEAL/CoqEAL/tree/paramcoq-dev)])])
rm -f conftest.v conftest.vo conftest.err
AC_MSG_CHECKING([for OSDP])
osdp_version=`ocamlfind query -format %v osdp 2>/dev/null`
AX_VERSION_GE([$osdp_version], 1.0,
[ AC_MSG_RESULT([yes]) ],
[ AC_MSG_RESULT([no])
AC_MSG_ERROR([ *** Unable to find library OSDP >= 1.1.1 (https://github.com/Embedded-SW-VnV/osdp).])])
AC_MSG_CHECKING([for coq-bignums])
AS_IF(
[ echo "Require Import Bignums.BigQ.BigQ." > conftest.v
$COQC conftest.v > conftest.err ],
[ AC_MSG_RESULT([yes]) ],
[ AC_MSG_RESULT([no])
AC_MSG_ERROR([ *** Unable to find library Bignums.BigQ.BigQ (opam package coq-bignums)])])
rm -f conftest.v conftest.vo conftest.err
AC_MSG_CHECKING([for libValidSDP])
AS_IF(
[ echo "From libValidSDP Require Import misc." > conftest.v
$COQC conftest.v > conftest.err ],
[ AC_MSG_RESULT([yes]) ],
[ AC_MSG_RESULT([no])
AC_MSG_ERROR([ *** Unable to find library libValidSDP (cf. directory libvalidsdp)])])
rm -f conftest.v conftest.vo conftest.err
AC_CHECK_TOOL([SDPA], [sdpa], [no])
if test "x$SDPA" != xno; then
SDPA_AVAILABLE="true"
AC_MSG_NOTICE([Optional dependency sdpa was found. Assuming osdp was built accordingly.])
else
SDPA_AVAILABLE=""
AC_MSG_NOTICE([Optional dependency sdpa was not found.])
fi
AC_SUBST(SDPA_AVAILABLE)
# Create files
AC_CONFIG_FILES([Makefile Makefile.coq.local _CoqProject plugins/soswitness/theories/soswitness_plugin.v])
AC_OUTPUT
chmod a-w Makefile Makefile.coq.local _CoqProject plugins/soswitness/theories/soswitness_plugin.v
echo ""
echo " Now run 'make && make install' to build and install $PACKAGE_NAME $PACKAGE_VERSION"
echo " (or run 'make help' to get for more info on the available rules)"
echo ""