INSTALL

Prerequisites
=============

Maude requires following the tools:

GNU g++		https://gcc.gnu.org/
  or
Clang		https://clang.llvm.org/
  C++ compiler
  
GNU bison	https://www.gnu.org/software/bison/
  Parser generator
  
flex		https://github.com/westes/flex
  Lexical analyzer generator

GNU automake https://www.gnu.org/software/automake/
  Needed for aclocal

GNU autoconf	https://www.gnu.org/software/autoconf/
  Package configuration macros - needed for Yices2 builds

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 a C++ compiler that at least supports C++11.


Maude requires the following packages:

GNU libsigsegv	  https://www.gnu.org/software/libsigsegv/
  Page fault handling library

GMP    	     	  https://gmplib.org/
  GNU Multiple Precision Arithmetic library; C++ bindings needed

Tecla		  http://www.astro.caltech.edu/~mcs/tecla/
  Command line editing library

BuDDy		  https://github.com/utwente-fmt/buddy
  Binary Decision Diagram library


Optionally, one of the following packages is needed to enable
Maude's experimental SMT features:

Yices2		  https://github.com/SRI-CSL/yices2
  or
CVC4		  https://cvc4.github.io/
  SMT Solver library


=================
Building on Linux
=================

You will need GNU g++, GNU bison, flex and GNU autoconf installed
via your distro's package manager.

Rather than build the dependencies from scratch, you might find some
or all of them available via your distro's package manager but you
will need to install the "developer" packages to get the header files.


Configuring the 3rd party packages
==================================

Decide where you are going to install them.

OPTLIB=...


libsigsegv
----------
curl -LJO https://ftp.gnu.org/gnu/libsigsegv/libsigsegv-2.13.tar.gz
tar xvf libsigsegv-2.13.tar.gz
cd libsigsegv-2.13
mkdir Opt
cd Opt

../configure \
CFLAGS="-g -fno-stack-protector -O3" \
--prefix=$OPTLIB \
--enable-shared=no

make
make check
make install


GMP
---
curl -LJO https://gmplib.org/download/gmp/gmp-6.3.0.tar.xz
tar xvf gmp-6.3.0.tar.xz
cd gmp-6.3.0
mkdir Opt
cd Opt

../configure \
--prefix=$OPTLIB \
--enable-cxx \
--enable-fat \
--enable-shared=yes \
--build=x86_64-pc-linux-gnu

make
make check
make install


BuDDy
-----
curl -LJO https://github.com/utwente-fmt/buddy/releases/download/v2.4/buddy-2.4.tar.gz
tar xvf buddy-2.4.tar.gz
cd buddy-2.4
mkdir Opt
cd Opt

../configure LDFLAGS=-lm \
CFLAGS="-g -fno-stack-protector -O3" \
CXXFLAGS="-g -fno-stack-protector -O3" \
--prefix=$OPTLIB \
--disable-shared

make
make check
make install


Telca
------
Tecla does not support building in a subdirectory.

curl -LJO https://sites.astro.caltech.edu/~mcs/tecla/libtecla-1.6.3.tar.gz
tar xvf libtecla-1.6.3.tar.gz
cd libtecla

./configure \
CFLAGS="-g -fno-stack-protector -O3" \
--prefix=$OPTLIB

make
make install


Yices2
------
Yices2 does not support building in a subdirectory and ships without
a configure file. Yices requires a dynamic GMP library to build, even
though we don't want dynamic libraries.

curl -LJO https://github.com/SRI-CSL/yices2/archive/refs/tags/Yices-2.6.4.tar.gz
tar xvf yices2-Yices-2.6.4.tar.gz
cd yices2-Yices-2.6.4

autoconf

./configure \
--prefix=$OPTLIB \
--with-static-gmp=$OPTLIB/lib/libgmp.a \
--with-static-gmp-include-dir=$OPTLIB/include \
CFLAGS="-g -fno-stack-protector -O3" \
LDFLAGS="-L$OPTLIB/lib" \
CPPFLAGS="-I$OPTLIB/include"

make
make check
make install


Building Maude
==============

First, hide or delete dynamic libraries that were made for 3rd party packages
to ensure only static libraries are linked against.

cd $OPTLIB/lib
mkdir Hidden
mv *.so* Hidden

Then in the root Maude directory:

mkdir Opt
cd Opt

../configure \
--with-yices2=yes \
--with-cvc4=no \
--enable-compiler \
CXXFLAGS="-g -Wall -O3 -fno-stack-protector" \
CPPFLAGS="-I$OPTLIB/include" \
LDFLAGS="-L$OPTLIB/lib" \
GMP_LIBS="$OPTLIB/lib/libgmpxx.a $OPTLIB/lib/libgmp.a"

make
make check
cd src/Main
cp maude maude.linux64
strip maude.linux64

Check dependencies:

ldd maude.linux64


===============
Building on Mac
===============

These are the build steps I use for making a MacOS 10.13 (High Sierra)
and later, x86-64 binary using Xcode 14.2. You will also need a recent
version of bison because the bison that ships with Xcode is ancient, and
autoconf because Yices2 ships with a configure.ac but no configure.

Rather than building the dependencies from scratch, you might find some
or all of them available under a MacOS package manager such as Homebrew
(https://brew.sh/) or MacPorts (https://www.macports.org/).

Configuring the 3rd party packages
==================================

Decide where you are going to install them.

HSLIB=...


libsigsegv
----------
curl -LJO https://ftp.gnu.org/gnu/libsigsegv/libsigsegv-2.13.tar.gz
tar xvf libsigsegv-2.13.tar.gz
cd libsigsegv-2.13
mkdir HighSierra
cd HighSierra

../configure \
CFLAGS="-g -fno-stack-protector -O3 -mmacosx-version-min=10.13" \
--prefix=$HSLIB \
--enable-shared=no

make
make check
make install


GMP
---
Note that 6.3.0 or later is needed for Apple silicon because of the
register x18 issue.

curl -LJO https://gmplib.org/download/gmp/gmp-6.3.0.tar.xz
tar xvf gmp-6.3.0.tar.xz
cd gmp-6.3.0
mkdir HighSierra
cd HighSierra

../configure \
CFLAGS="-g -fno-stack-protector -O3 -mmacosx-version-min=10.13" \
CXXFLAGS="-g -fno-stack-protector -O3 -mmacosx-version-min=10.13 -std=c++11" \
--prefix=$HSLIB \
--enable-cxx \
--enable-fat \
--enable-shared=yes

make
make check
make install


BuDDy
-----
BuDDy has a missing execute permission on its install script.

curl -LJO https://github.com/utwente-fmt/buddy/releases/download/v2.4/buddy-2.4.tar.gz
tar xvf buddy-2.4.tar.gz
cd buddy-2.4
mkdir HighSierra
cd HighSierra

../configure LDFLAGS=-lm \
CFLAGS="-g -fno-stack-protector -O3 -mmacosx-version-min=10.13" \
CXXFLAGS="-g -fno-stack-protector -O3 -mmacosx-version-min=10.13 -std=c++11" \
--prefix=$HSLIB \
--disable-shared

make
make check
chmod a+x ../tools/install-sh
make install


Telca
------
Tecla does not support building in a subdirectory and requires one of the
source files to be hacked in order to compile under clang.

curl -LJO https://sites.astro.caltech.edu/~mcs/tecla/libtecla-1.6.3.tar.gz
tar xvf libtecla-1.6.3.tar.gz
cd libtecla

Add #include <sys/ioctl.h> as the first line of enhance.c

./configure \
CFLAGS="-fno-stack-protector -O3 -mmacosx-version-min=10.13" \
--prefix=$HSLIB

make
make install


Yices2
------
Yices2 does not support building in a subdirectory and ships without
a configure file. Yices requires a dynamic GMP library to build, even
though we don't want dynamic libraries.

curl -LJO https://github.com/SRI-CSL/yices2/archive/refs/tags/Yices-2.6.4.tar.gz
tar xvf yices2-Yices-2.6.4.tar.gz
cd yices2-Yices-2.6.4

autoconf

./configure \
--prefix=$HSLIB \
--with-static-gmp=$HSLIB/lib/libgmp.a \
--with-static-gmp-include-dir=$HSLIB/include \
CFLAGS="-fno-stack-protector -O3 -mmacosx-version-min=10.13" \
LDFLAGS="-L$HSLIB/lib" \
CPPFLAGS="-I$HSLIB/include"

make
make check
make install


Building Maude
==============

First, hide or delete dynamic libraries that were made for 3rd party packages
to ensure only static libraries are linked against.

cd $HSLIB/lib
mkdir Hidden
mv *.dylib Hidden

Then in the root Maude directory:

mkdir HighSierra
cd HighSierra

../configure \
--with-yices2=yes \
--with-cvc4=no \
--enable-compiler \
BISON="path to recent bison" \
CXXFLAGS="-Wall -O3 -fno-stack-protector -fstrict-aliasing -mmacosx-version-min=10.13 -std=c++11" \
CPPFLAGS="-I$HSLIB/include" \
LDFLAGS="-L$HSLIB/lib -Wl,-no_pie" \
GMP_LIBS="$HSLIB/lib/libgmpxx.a $HSLIB/lib/libgmp.a"

make
make check
cd src/Main
cp maude maude.darwin64

Note that stripping the binary on Macs seems to break libsigsegv for some reason.

Check dependencies:

otool -L maude.darwin64