Makefile.build

# -*-makefile-gmake-*- (emacs mode)
#########################################################################
#
#  This file is part of the Yices SMT Solver.
#  Copyright (C) 2017 SRI International.
#
#  Yices is free software: you can redistribute it and/or modify
#  it under the terms of the GNU General Public License as published by
#  the Free Software Foundation, either version 3 of the License, or
#  (at your option) any later version.
#
#  Yices is distributed in the hope that it will be useful,
#  but WITHOUT ANY WARRANTY; without even the implied warranty of
#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
#  GNU General Public License for more details.
#
#  You should have received a copy of the GNU General Public License
#  along with Yices.  If not, see <http://www.gnu.org/licenses/>.
#
#########################################################################


#
# Build Makefile
#
# Must be invoked with the following variables set
#
#   YICES_TOP_DIR = top-level directory of Yices
#   YICES_MODE = build mode
#   YICES_MAKE_INCLUDE = configuration file to include
#   YICES_VERSION = full version
#   MAJOR = major version number
#   MINOR = minor version number
#   PATCH_LEVEL = patch level
#   ARCH = architecture (e.g, i686-pc-linux-gnu)
#   POSIXOS = OS (e.g., linux)
#
# Config variables are imported by including the file
#   $(YICES_TOP_DIR)/$(YICES_MAKE_INCLUDE)
#
# This file is constructed by running configure on the
# host and it defines the compilation tools and flags
# and the GMP libraries to use.
#

SHELL=/bin/sh

ifeq (,$(YICES_TOP_DIR))
 $(error "YICES_TOP_DIR is undefined")
endif

ifeq (,$(YICES_MAKE_INCLUDE))
 $(error "YICES_MAKE_INCLUDE is undefined")
endif

include $(YICES_TOP_DIR)/$(YICES_MAKE_INCLUDE)

#
# ldconfig is used by the install rules.
# We don't check for ldconfig in configure.ac (since that doesn't
# make much sense). We use /sbin/ldconfig as default here. If that's
# wrong, change it on the command line:
#
#   make install LDCONFIG=...
#
LDCONFIG=/sbin/ldconfig

#
# Script/command to build a README file from a template
#
arm_android=$(findstring arm-linux-android,$(ARCH))
ifeq ($(arm_android),arm-linux-android)
MKREADME=./utils/mkreadme-android
else
MKREADME=./utils/mkreadme
endif

#
# Template + script to construct yices_version.c
#
template=./src/api/yices_version_template.txt
MKVERSION=./utils/make_source_version

#
# Source directories
#
srcdir = src
srcsubdirs = mt io terms utils solvers solvers/floyd_warshall \
    solvers/funs solvers/bv solvers/egraph solvers/cdcl solvers/simplex solvers/quant \
    parser_utils model api frontend frontend/common \
    frontend/smt1 frontend/yices frontend/smt2 context exists_forall \
    mcsat mcsat/eq mcsat/weq mcsat/uf mcsat/bool mcsat/ite mcsat/nra mcsat/ff mcsat/bv \
    mcsat/bv/explain mcsat/utils

testdir = tests/unit
regressdir = tests/regress
regressdir_mcsat = tests/regress/mcsat
apitestdir = tests/api

#
# Build directory: for this architecture and mode
#
build_dir = build/$(ARCH)-$(YICES_MODE)

#
# Build subdirectories: we build two versions of Yices.  One is
# compiled and statically linked with GMP. The other one does not
# include GMP so it requires GMP as a dynamic library at runtime.
#
# build/obj: object files (for version without GMP included)
# build/lib: libraries (GMP not included)
# build/bin: binaries (GMP not included)
#
# build/static_obj: object files (for version statically linked with GMP)
# build/static_lib: libraries (GMP included)
# build/static_bin: binaries linked statically with GMP (and other libraries if possible)
#
# build/static_dll_obj: for mingw and cygwin objectfiles to construct the static
# variant of cygyices.dll or libyices.dll
#
dyn_objdir := $(build_dir)/obj
dyn_libdir := $(build_dir)/lib
dyn_bindir := $(build_dir)/bin

static_objdir := $(build_dir)/static_obj
static_libdir := $(build_dir)/static_lib
static_bindir := $(build_dir)/static_bin

static_dll_objdir := $(build_dir)/static_dll_obj

dyn_objsubdirs := $(srcsubdirs:%=$(dyn_objdir)/%)
static_objsubdirs := $(srcsubdirs:%=$(static_objdir)/%)
static_dll_objsubdirs := $(srcsubdirs:%=$(static_dll_objdir)/%)

#
# Binary distributions:
#
# build_dir/dist: binaries + libraries with distribution not linked with GMP
# build_dir/static_dist: includes GMP (statically linked)
#
dist_dir = $(build_dir)/dist
static_dist_dir = $(build_dir)/static_dist


#
# Directories and temporary file to build tarfiles
# - we do this in two steps: the includes, binaries, and library files
#   to be distributed are constructed by invoking make -C src
#   and copied into $(dist_dir)
#   (what's required is defined in src/Makefile and may depend
#    on the OS + compilation mode).
# - the full tar file is built from $(dist_dir) + the generic files
#   that are independent of OS and compilation modes
# - the name of the tar file depends on ARCH + MODE
#
# All tarfiles are stored in ./distributions
#
distributions = ./distributions
bindist_dir = yices-$(YICES_VERSION)

ifeq ($(YICES_MODE),debug)
  bindist_tarfile = $(bindist_dir)-$(ARCH)-dbg.tar.gz
  static_bindist_tarfile = $(bindist_dir)-$(ARCH)-static-gmp-dbg.tar.gz
else
  bindist_tarfile = $(bindist_dir)-$(ARCH).tar.gz
  static_bindist_tarfile = $(bindist_dir)-$(ARCH)-static-gmp.tar.gz
endif



#
# Build subdirectories if they are missing
#
$(build_dir):
	$(MKDIR_P) $(build_dir)

$(dyn_objdir):
	$(MKDIR_P) $(dyn_objdir)

$(dyn_objsubdirs):
	$(MKDIR_P) $@

$(dyn_libdir):
	$(MKDIR_P) $(dyn_libdir)

$(dyn_bindir):
	$(MKDIR_P) $(dyn_bindir)

$(static_objdir):
	$(MKDIR_P) $(static_objdir)

$(static_objsubdirs):
	$(MKDIR_P) $@

$(static_dll_objdir):
	$(MKDIR_P) $(static_dll_objdir)

$(static_dll_objsubdirs):
	$(MKDIR_P) $@

$(static_libdir):
	$(MKDIR_P) $(static_libdir)

$(static_bindir):
	$(MKDIR_P) $(static_bindir)

$(distdir):
	$(MKDIR_P) $(distdir)

$(static_distdir):
	$(MKDIR_P) $(static_distdir)


build_subdirs: $(build_dir) $(dyn_objsubdirs) $(dyn_libdir) $(dyn_bindir)

static_build_subdirs-mingw static_build_subdirs-cygwin: $(static_dll_objsubdirs)

static_build_subdirs-darwin static_build_subdirs-linux static_build_subdirs-unix static_build_subdirs-freebsd static_build_subdirs-netbsd:

static_build_subdirs: $(build_dir) $(static_objsubdirs) $(static_libdir) $(static_bindir) \
	static_build_subdirs-$(POSIXOS)

.PHONY: build_subdirs static_build_subdirs static_build_subdirs-darwin static-build_subdirs-cygwin \
	static_build_subdirs-mingw static_build_subdirs-linux static_build_subdirs-unix \
	static_build_subdirs-freebsd static_build_subdirs-netbsd

#
# Compilation
#
all: obj static-obj lib static-lib bin static-bin

obj: build_subdirs version
	@ echo "=== Building objects ==="
	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) obj

static-obj: static_build_subdirs version
	@ echo "=== Building static objects ==="
	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) static-obj

lib: build_subdirs version
	@ echo "=== Building libraries ==="
	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) lib

static-lib: static_build_subdirs build_subdirs version
	@ echo "=== Building libraries with GMP ==="
	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) static-lib

bin: build_subdirs version
	@ echo "=== Building binaries ==="
	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) bin

static-bin: static_build_subdirs version
	@ echo "=== Building static binaries ==="
	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) static-bin


#
# Force a new 'yices_version.c' to be generated.
# Compilation date and mode, git revision, and version numbers
# are copied into yices_version.c.
#
version:
	$(MKVERSION) $(template) src/api/yices_$(YICES_MODE)_version.c $(YICES_VERSION) $(YICES_MODE) $(ARCH)

.PHONY: version



#
# Tests: all use libyices.a in lib
# Static tests: use libyices.a in static-lib
# Don't regenerate the version file
#
test: build_subdirs version
	@ echo "=== Building libraries ==="
	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) lib
	@ echo "=== Building tests ==="
	@ $(MAKE) -C $(testdir) BUILD=../../$(build_dir) all

static-test: static_build_subdirs version
	@ echo "=== Building libraries with GMP ==="
	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) static-lib
	@ echo "=== Building tests ==="
	@ $(MAKE) -C $(testdir) BUILD=../../$(build_dir) all-static

#
# API tests: link with libyices.a like tests
#
check-api: build_subdirs version
	@ echo "=== Building libraries ==="
	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) lib
	@ echo "=== Building tests ==="
	@ $(MAKE) -C $(apitestdir) BUILD=../../$(build_dir) all

static-check-api: static_build_subdirs version
	@ echo "=== Building libraries with GMP ==="
	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) static-lib
	@ echo "=== Building tests ==="
	@ $(MAKE) -C $(apitestdir) BUILD=../../$(build_dir) all-static


#
# Regressions
#
check: regress
mcsat-check: mcsat-regress
static-check: static-regress

regress: build_subdirs version
	@ echo "=== Building binaries ==="
	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) bin
	@ echo "=== Running regressions ==="
	+@ $(regressdir)/check.sh $(regressdir) $(build_dir)/bin


mcsat-regress: build_subdirs version
	@ echo "=== Building binaries ==="
	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) bin
	@ echo "=== Running regressions ==="
	+@ $(regressdir)/check.sh $(regressdir_mcsat) $(build_dir)/bin


static-regress: static_build_subdirs version
	@ echo "=== Building binaries ==="
	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) static-bin
	@ echo "=== Running regressions ==="
	+@ $(regressdir)/check.sh $(regressdir) $(build_dir)/static_bin


static-mcsat-regress: static_build_subdirs version
	@ echo "=== Building binaries ==="
	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) static-bin
	@ echo "=== Running regressions ==="
	+@ $(regressdir)/check.sh $(regressdir_mcsat) $(build_dir)/static_bin


.PHONY: all obj static-obj lib static-lib bin static-bin test static-test \
    regress static-regress check static-check check-api static-check-api


#
# Documentation: for now we just build manual.pdf
# this assumes latexmk is available
#
doc:
	@ echo "=== Building the documentation ==="
	@ (cd doc/manual ; \
          (latexmk -pdf manual || \
            (echo "===================================="; \
             echo "  WARNING: can't run latexmk"; \
             echo "   manual.pdf may be out-of-date"; \
             echo "===================================="; )))


documentation manual: doc

.PHONY: doc documentation manual


#
# Binary distribution:
#
# On mingw, there's a manual step involved. So build the
# distribution as follows:
# 1) make dist (or make static-dist)
# 2) from a Visual Studio console,
#    go to ./build/i686-pc-mingw32-release/dist/lib
#    then type 'lib /machine:x86 /def:libyices.def
# 3) clean up: remove libyices.def and libyices.exp
#    from ./build/i686-pc-mingw32-release/dist/lib
# 4) make tarfile (or make static-tarfile)
#
# On other platforms: make binary-distribution or make
# static-distribution should work.
#
# On MacOS X, the tar command adds files of the form ._xxxx to store
# metadata/extended file attributes. This gets ugly if we untar on
# some other platform. To prevent generation of these ._xxxx files, it
# is enough to set the environment variable COPYFILE_DISABLE to 1. We
# do this systematically (even on other systems). Hopefully,
# COPYFILE_DISABLE should not matter on other systems than MacOS X.
#
# We use a shell script ./util/mkreadme to make sure
# the README file in the tarfile is up to date (probably
# not foolproof)
#
$(distributions):
	$(MKDIR_P) $(distributions)

$(dist_dir):
	$(MKDIR_P) $(dist_dir)

$(static_dist_dir):
	$(MKDIR_P) $(static_dist_dir)

binary-distribution: dist tarfile

static-distribution: static-dist static-tarfile

dist: build_subdirs version $(dist_dir)
	@ echo "=== Preparing binary distribution ==="
	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) dist

static-dist: static_build_subdirs build_subdirs version $(static_dist_dir)
	@ echo "=== Preparing static binary distribution ==="
	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) static-dist


tarfile: $(distributions) doc
	@ echo "=== Building $(bindist_tarfile) ==="
	rm -f -r $(bindist_dir)
	$(MKDIR_P) $(bindist_dir)
	cp -r $(dist_dir)/* $(bindist_dir)
	cp etc/NOTICES $(bindist_dir)
	cp LICENSE.txt $(bindist_dir)/LICENSE
	$(MKREADME) $(dist_dir) etc/README.$(POSIXOS) > $(bindist_dir)/README
	if test -f etc/install-yices.$(POSIXOS) ; then \
	  cp etc/install-yices.$(POSIXOS) $(bindist_dir)/install-yices ; \
	  chmod ug+x $(bindist_dir)/install-yices ; \
	fi
	$(MKDIR_P) $(bindist_dir)/etc
	cp etc/pstdint.h $(bindist_dir)/etc
	$(MKDIR_P) $(bindist_dir)/examples
	for file in `ls examples | $(EGREP) '\.ys$$|\.smt$$|\.c$$|\.smt2$$|\.cpp$$' ` ; do \
	  cp examples/$$file $(bindist_dir)/examples ; \
	done || true
	$(MKDIR_P) $(bindist_dir)/doc
	cp doc/YICES-LANGUAGE $(bindist_dir)/doc
	cp doc/manual/manual.pdf $(bindist_dir)/doc
	chmod -R og+rX $(bindist_dir)
	COPYFILE_DISABLE=1 tar -czf $(distributions)/$(bindist_tarfile) $(bindist_dir)
	chmod -R og+rX $(distributions)
	rm -f -r $(bindist_dir)

static-tarfile: $(distributions) doc
	@ echo "=== Building $(static_bindist_tarfile) ==="
	rm -f -r $(bindist_dir)
	$(MKDIR_P) $(bindist_dir)
	cp -r $(static_dist_dir)/* $(bindist_dir)
	cp etc/NOTICES $(bindist_dir)
	cp LICENSE.txt $(bindist_dir)/LICENSE
	$(MKREADME) $(static_dist_dir) etc/README.static.$(POSIXOS) > $(bindist_dir)/README
	if test -f etc/install-yices.$(POSIXOS) ; then \
	  cp etc/install-yices.$(POSIXOS) $(bindist_dir)/install-yices ; \
	  chmod ug+x $(bindist_dir)/install-yices ; \
	fi
	$(MKDIR_P) $(bindist_dir)/etc
	cp etc/pstdint.h $(bindist_dir)/etc
	$(MKDIR_P) $(bindist_dir)/examples
	for file in `ls examples | $(EGREP) '\.ys$$|\.smt$$|\.c$$|\.smt2$$|\.cpp$$' ` ; do \
	  cp examples/$$file $(bindist_dir)/examples ; \
	done || true
	$(MKDIR_P) $(bindist_dir)/doc
	cp doc/YICES-LANGUAGE $(bindist_dir)/doc
	cp doc/manual/manual.pdf $(bindist_dir)/doc
	chmod -R og+rX $(bindist_dir)
	COPYFILE_DISABLE=1 tar -czf $(distributions)/$(static_bindist_tarfile) $(bindist_dir)
	chmod -R og+rX $(distributions)
	rm -f -r $(bindist_dir)


.PHONY: binary-distribution static-distribution dist static-dist \
	tarfile static-tarfile



#
# Install from the source.
#
# The target directories are determined by ./configure:
#   bindir = where to put binaries
#   libdir = where to put the libraries
#   includedir = where to put the include files
#
# We assume 'make binary-distribution' was done first,
# then we copy the $(dist_dir) content:
#   $(dist_dir)/bin     into $(bindir)
#   $(dist_dir)/lib     into $(libdir)
#   $(dist_dir)/include into $(includedir)
#
# Note: the default bindir, libdir, includedir are set by the
# configure script, and are imported from $(YICES_MAKE_INCLUDE).
# These defaults can be changed by using 'make install prefix=...'
#
# We also (try to) support the DESTDIR convention.
#
# The reason we don't want to force compilation in 'make install' is
# that we typically need to do 'sudo make install' but we don't want
# to compile with 'sudo make binary-distribution'.  That can easily
# fail if the source and build directory or file permissions are
# wrong, or lead to other problems.
#
install: install-$(POSIXOS)

install-default:
	$(MKDIR_P) $(DESTDIR)$(bindir)
	$(MKDIR_P) $(DESTDIR)$(libdir)
	$(MKDIR_P) $(DESTDIR)$(includedir)
	$(INSTALL) -m 664 $(dist_dir)/include/* $(DESTDIR)$(includedir)
	$(INSTALL) $(dist_dir)/bin/* $(DESTDIR)$(bindir)
	$(INSTALL) $(dist_dir)/lib/* $(DESTDIR)$(libdir)

install-darwin: install-default
	(cd $(DESTDIR)$(libdir) && $(LN_S) -f libyices.$(MAJOR).dylib libyices.dylib)

install-solaris: install-default
	$(LDCONFIG) -n $(DESTDIR)$(libdir) && (cd $(DESTDIR)$(libdir) && $(LN_S) -f libyices.so.$(YICES_VERSION) libyices.so)

# Avoid ldconfig as it's not present on musl. We create the following symlinks:
# - libyices.so.X.Y.Z -> libyices.so.X.Y
# - libyices.so.X.Y   -> libyices.so
install-linux install-unix: install-default
	(cd $(DESTDIR)$(libdir) && $(LN_S) -f libyices.so.$(YICES_VERSION) libyices.so.$(MAJOR).$(MINOR) && $(LN_S) -f libyices.so.$(MAJOR).$(MINOR) libyices.so)

# on FreeBSD: the library file is libyices.so.X.Y and ldconfig does not take -n
# TODO: fix this. We must also create a symbolic link: libyices.so.X in libdir
# the ldconfig manpage on FreeBSD says 'filenames must conform to the lib*.so.[0-9] pattern in order to
# be added to the hints file.' In other words, ldconfig on FreeBSD doesn't create the symbolic link,
# as on Linux.
install-freebsd: install-default
	(cd $(DESTDIR)$(libdir) && $(LN_S) -f libyices.so.$(MAJOR) libyices.so)

install-netbsd: install-default
	(cd $(DESTDIR)$(libdir) && $(LN_S) -f libyices.so.$(YICES_VERSION) libyices.so)

#
# cygwin and mingw install: copy the DLLs in $(bindir)
#
install-cygwin: $(build_dir) $(dist_dir)
	$(MKDIR_P) $(DESTDIR)$(bindir)
	$(MKDIR_P) $(DESTDIR)$(libdir)
	$(MKDIR_P) $(DESTDIR)$(includedir)
	$(INSTALL) -m 664 $(dist_dir)/include/* $(DESTDIR)$(includedir)
	$(INSTALL) $(dist_dir)/bin/* $(DESTDIR)$(bindir)
	$(INSTALL) $(dist_dir)/lib/*.a $(DESTDIR)$(libdir)

install-mingw: install-cygwin


.PHONY: install install-default install-darwin install-solaris \
	install-linux install-freebsd install-netbsd install-unix \
        install-cygwin install-mingw



#
# SOURCE DISTRIBUTION
#
srcdist_dir = yices-$(YICES_VERSION)
srcdist_tarfile= yices-$(YICES_VERSION)-src.tar.gz

#
# Build the source tar file
#
# NOTE: chmod -R .. may fail on some Solaris versions
# - a workaround is to use a GNU/fileutils version of chmod
#   instead of SUN's own version
# - on CSL ungoliant: make sure /csl/bin is in the path before /bin
#   and /usr/bin
#
# For tests: we copy all unit tests and the regression tests in
# arrays/bv/efsmt/mantis/wd.
#
source-distribution: $(distributions) doc
	@ echo "=== Building $(srcdist_tarfile) ==="
	rm -f -r $(srcdist_dir)
	$(MKDIR_P) $(srcdist_dir)
	cp install-sh config.guess configure configure.ac config.sub gmaketest $(srcdist_dir)
	cp Makefile Makefile.build make.include.in $(srcdist_dir)
	$(MKDIR_P) $(srcdist_dir)/autoconf
	cp autoconf/* $(srcdist_dir)/autoconf
	$(MKDIR_P) $(srcdist_dir)/configs
	$(MKDIR_P) $(srcdist_dir)/etc
	cp etc/README.source $(srcdist_dir)/README
	cp etc/NOTICES $(srcdist_dir)
	cp LICENSE.txt $(srcdist_dir)/LICENSE
	cp etc/* $(srcdist_dir)/etc
	$(MKDIR_P) $(srcdist_dir)/src
	rsync -R `find src/ -name "Makefile" -or -name "*.c" -or -name "*.h" -or -name "*.txt"` $(srcdist_dir)
	$(MKDIR_P) $(srcdist_dir)/doc
	$(MKDIR_P) $(srcdist_dir)/doc/manual
	cp doc/COMPILING doc/NOTES doc/YICES-LANGUAGE doc/GMP doc/manual/manual.pdf \
           $(srcdist_dir)/doc
	cp doc/manual/*.pdf doc/manual/*.tex doc/manual/*.bib \
           doc/manual/*.cls doc/manual/*.sty doc/manual/*.eps doc/manual/*.fig \
	   $(srcdist_dir)/doc/manual
	$(MKDIR_P) $(srcdist_dir)/utils
	cp utils/gmp-hack.h utils/mingw-build utils/setup-vs2010 utils/setup-vs2013 \
	   utils/yices_parser.txt utils/yices_input_tables.h \
	   utils/smt_parser.txt utils/smt_input_tables.h \
	   utils/smt2_parser.txt utils/smt2_input_tables.h \
	   utils/table_builder.c utils/truth_table_compiler.c \
	   utils/mkreadme utils/mkreadme-android utils/make_source_version \
	   utils/lib_name utils/gmp_version utils/yices_version \
           utils/remove_trailing_whitespaces \
           $(srcdist_dir)/utils
	$(MKDIR_P) $(srcdist_dir)/examples
	for file in `ls examples | $(EGREP) '\.ys$$|\.smt$$|\.c$$|\.smt2$$|\.cpp$$' ` ; do \
	  cp examples/$$file $(srcdist_dir)/examples ; \
	done || true
	$(MKDIR_P) $(srcdist_dir)/tests
	cp -R tests/unit $(srcdist_dir)/tests
	$(MKDIR_P) $(srcdist_dir)/tests/regress
	for t in regress/arrays regress/bv regress/efsmt regress/mantis regress/wd ; do \
	   cp -R tests/$$t $(srcdist_dir)/tests/regress ; \
	done
	cp tests/regress/check.sh $(srcdist_dir)/tests/regress
	chmod -R og+rX $(srcdist_dir)
	COPYFILE_DISABLE=1 tar -czf $(distributions)/$(srcdist_tarfile) $(srcdist_dir)
	chmod -R og+rX $(distributions)
	rm -f -r $(srcdist_dir)

.PHONY: source-distribution



#
# CLEANUP
#

#
# Basic clean: delete build sub-directories for architecture + mode
#
clean:
	rm -rf $(build_dir)/*

#
# Arch clean: delete all build subdirectories for an architecture
#
arch-clean:
	rm -rf build/$(ARCH)-*

#
# All clean delete all build directories
# - also clean the src directory
#
all-clean:
	rm -rf build/*
	$(MAKE) -C $(srcdir) clean

.PHONY: clean arch-clean all-clean



#
# Helper rule for debugging Makefiles and configure
#
show-details:
	@ echo
	@ echo "*** Recursive Makefile ***"
	@ echo
	@ echo "target is $@"
	@ echo
	@ echo "ARCH is $(ARCH)"
	@ echo "POSIXOS is $(POSIXOS)"
	@ echo "YICES_TOP_DIR is $(YICES_TOP_DIR)"
	@ echo "YICES_MAKE_INCLUDE is $(YICES_MAKE_INCLUDE)"
	@ echo "YICES_MODE is $(YICES_MODE)"
	@ echo "YICES_VERSION is $(YICES_VERSION)"
	@ echo "MAJOR is $(MAJOR)"
	@ echo "MINOR is $(MINOR)"
	@ echo "PATCH_LEVEL is $(PATCH_LEVEL)"
	@ echo
	@ echo "Configuration"
	@ echo "  EXEEXT   = $(EXEEXT)"
	@ echo "  SED      = $(SED)"
	@ echo "  LN_S     = $(LN_S)"
	@ echo "  MKDIR_P  = $(MKDIR_P)"
	@ echo "  CC       = $(CC)"
	@ echo "  CPPFLAGS = $(CPPFLAGS)"
	@ echo "  CFLAGS   = $(CFLAGS)"
	@ echo "  LIBS     = $(LIBS)"
	@ echo "  LDFLAGS  = $(LDFLAGS)"
	@ echo "  LD       = $(LD)"
	@ echo "  AR       = $(AR)"
	@ echo "  RANLIB   = $(RANLIB)"
	@ echo "  GPERF    = $(GPERF)"
	@ echo "  STRIP    = $(STRIP)"
	@ echo
	@ echo "  NO_STACK_PROTECTOR = $(NO_STACK_PROTECTOR)"
	@ echo
	@ echo "  STATIC_GMP = $(STATIC_GMP)"
	@ echo "  STATIC_GMP_INCLUDE_DIR = $(STATIC_GMP_INCLUDE_DIR)"
	@ echo
	@ echo "  PIC_GMP = $(PIC_GMP)"
	@ echo "  PIC_GMP_INCLUDE_DIR = $(PIC_GMP_INCLUDE_DIR)"
	@ echo
	@ echo "  ENABLE_MCSAT = $(ENABLE_MCSAT)"
	@ echo
	@ echo "  STATIC_LIBPOLY = $(STATIC_LIBPOLY)"
	@ echo "  STATIC_LIBPOLY_INCLUDE_DIR = $(STATIC_LIBPOLY_INCLUDE_DIR)"
	@ echo
	@ echo "  PIC_LIBPOLY = $(PIC_LIBPOLY)"
	@ echo "  PIC_LIBPOLY_INCLUDE_DIR = $(PIC_LIBPOLY_INCLUDE_DIR)"
	@ echo


.PHONY: show-details


#
# Make sure everything here is serialized
# The sub makes can be run in parallel so option -j x should be allowed
#
.NOTPARALLEL: