forked from formalize/coq-vyper
-
Notifications
You must be signed in to change notification settings - Fork 1
/
configure
executable file
·56 lines (46 loc) · 1.38 KB
/
configure
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
#! /bin/sh
COQC=$(which coqc)
if [ $"x$COQC" = x ]
then
echo "coqc not found"
exit 1
fi
COQ_VERSION=$("$COQC" -v | head -n 1 | sed 's/^[^0-9]*\([0-9\.]*\) .*$/\1/')
echo Found Coq $COQ_VERSION
COQ_MAJOR=$(echo "$COQ_VERSION" | sed 's/\..*$//')
COQ_MINOR=$(echo "$COQ_VERSION" | sed 's/[^.]*\.\([^\.]*\).*$/\1/')
if [ $COQ_MAJOR -ge 8 ]
then
if [ $COQ_MAJOR -gt 8 -o $COQ_MINOR -gt 13 ]
then
echo '!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!'
echo '!! !!'
echo '!! Coq 8.14 introduced a regression: https://github.com/coq/coq/issues/15067 !!'
echo '!! Until that is fixed, the build will fail. Using Coq 8.13.2 is recommended. !!'
echo '!! !!'
echo '!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!'
fi
fi
GHC=$(which ghc)
if [ x$(which "$GHC") = x ]
then
echo "ghc not found"
exit 1
fi
ALEX=$(which alex)
if [ x$(which "$ALEX") = x ]
then
echo "alex not found"
exit 1
fi
HAPPY=$(which happy)
if [ x$(which "$HAPPY") = x ]
then
echo "happy not found"
exit 1
fi
# echo "coqc: $COQC"
# echo "ghc: $GHC"
# echo "alex: $ALEX"
# echo "happy: $HAPPY"
coq_makefile -f _CoqProject -o Makefile