-
Notifications
You must be signed in to change notification settings - Fork 1
/
INSTALL
129 lines (99 loc) · 4.4 KB
/
INSTALL
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
Prerequisites
=============
Maude requires following the tools:
GNU gcc http://gcc.gnu.org/
GNU bison http://www.gnu.org/software/bison/
GNU flex http://www.gnu.org/software/flex/
It is recommended that you use the latest versions of bison and flex
since Maude is known to tickle bugs in certain older versions. You
should use gcc 3.1 or later as there are code generation issues with
the 3.0.* series.
Maude requires the following packages:
GNU gmp http://www.swox.com/gmp/
GNU libsigsegv http://libsigsegv.sourceforge.net/
Tecla http://www.astro.caltech.edu/~mcs/tecla/
BuDDY http://sourceforge.net/projects/buddy
CVC4 (optional) http://cvc4.cs.nyu.edu/web/
Yices2 (optional) https://github.com/SRI-CSL/yices2.git
Configuring the 3rd party packages
==================================
Because of C++ ABI incompatibilities, GNU gmp, BuDDy and CVC4 must be
compiled with the same compiler you will use for Maude.
GNU gmp must be configured with --enable-cxx to generate the C++
bindings. The option --disable-shared is recommended to avoid linking
issues on various platforms.
It is recommended that Tecla be configured with CFLAGS set to
"-O2 -D_POSIX_C_SOURCE=1". This has the effect of using the thread
unsafe library calls which avoids binary compatibility issues on
various platforms. It is recommended that Tecla is built and installed
with the command:
make TARGETS=normal TARGET_LIBS=static install
to avoid linking issues on various platforms.
As of 2.4 BuDDy has moved to autoconf. The option --disable-shared is
recommended to avoid linking issues on various platforms.
Yices2 must be built from source, and does not support building
in an architecture specific subdirectory. The lastest source tree
should be obtained from the git repository since the current
release (Yices 2.5.2) exports a function, tputs(), that conflicts
with the function of the same name in the curses/ncurses system
library that is needed by Tecla.
Building Maude
==============
Only one of CVC4 and Yices2 should be linked to provide an SMT backend.
By default, Maude is configured to use Yices2.
If everything is installed in standard places you can configure and
build Maude with the commands:
./configure
make
Passing --with-yices2=no --with-cvc4=yes to configure will use CVC4
instead of Yices2. Passing both options as no will build Maude without
SMT support.
A very basic test suite can be run using the command:
make check
If you installed any of the 3rd party packages in non-standard places
you can indicate where the header files are by setting CPPFLAGS and
where the library files by setting LDFLAGS. If you have multiple
versions of any these libraries in your environment you can select
particular versions explicitly by setting:
GMP_LIBS (defaults to -lgmpxx -lgmp)
LIBSIGSEGV_LIB (defaults to -lsigsegv)
TECLA_LIBS (defaults to -ltecla -lcurses)
BUDDY_LIB (defaults to -lbuddy)
CVC4_LIB (defaults to -lcvc4)
YICES2_LIB (defaults to -lyices)
A more realistic configure to make, check and install a static binary
using a separate build tree might look something like:
mkdir Build
cd Build
../configure \
CPPFLAGS="-I/home/me/include" \
LDFLAGS="-static -L/home/me/lib" \
GMP_LIBS="/home/me/lib/libgmpxx.a /home/me/lib/libgmp.a"
make
make check
make install
The maude binary is installed in $(bindir) and the .maude files are
installed in $(datadir). In order for the Maude binary to find the
.maude files you should set the environment variable MAUDE_LIB to
point to $(datadir). Alternatively you could move the .maude files to
$(bindir).
Note that if your CVC4 library is built using CLN then you must
also link this library (-lcln).
Note for Mac users
==================
As of Mavericks, Apple no longer supports gcc so Maude must be compiled
with clang. The easiest way is to install the Mac Ports version of each of
the needed tools and libraries (except Yices2 which must built from sources
obtained from the git repository). With Mac Ports installed in /opt/local
I use the configuration line:
../configure \
CC=cc \
CXX=c++ \
FLEX=/opt/local/bin/flex \
BISON=/opt/local/bin/bison \
CFLAGS="-Wall -O2 -I/opt/local/include -fno-stack-protector -fstrict-aliasing" \
CXXFLAGS="-Wall -O2 -I/opt/local/include -fno-stack-protector -fstrict-aliasing" \
BUDDY_LIB="/opt/local/lib/libbdd.a" \
TECLA_LIBS="/opt/local/lib/libtecla.a /usr/lib/libncurses.dylib" \
LIBSIGSEGV_LIB="/opt/local/lib/libsigsegv.a" \
GMP_LIBS="/opt/local/lib/libgmp.a /opt/local/lib/libgmpxx.a"