Skip to content
Permalink
Browse files
ocamlyices2: only build the static stub using static libgmp.a.
The library libgmp.a will be searched in system dirs or you can use the flag
--with-static-gmp= when running ./configure for setting your own libgmp.a. If
no libgmp.a is found, the shared library is used. You can force the use of
shared gmp library with --with-shared-gmp.

If --with-shared-gmp is not given, the libgmp.a that has been found
will be included in the list of installed files. The reason is because
if we want to build a shared-gmp-free binary, zarith will sometimes pick the
shared library (with -lgmp) over the static lbirary libgmp.a.

Including libgmp.a in the distribution of ocamlyices2 is a convenience for
creating gmp-shared-free binaries.

Why do we prefer using a static version of libgmp.a?
===================================================

This is because we build a non-PIC static version of libyices.a. If
we wanted to build both static and shared stubs, we should either
- build a PIC libyices.a but it would conflict with the non-PIC one
- build a shared library libyices.so.

For now, I chose to just skip the shared stubs (dllyices2_stubs.so).

Also:

* turn on -fPIC (in configure.ac) only if non-static gmp
* added a way to link statically to libgmp.a (--with-static-gmp)
* use -package instead of -I/lib for compiling *.c in ocamlc

This option uses the change I made to the build system of libyices.
Why? Because I want the possibility of producing binaries that do
not need any dll alongside.

Guess the host system and pass it to libyices ./configure
=========================================================
It is now possible to use ./configure for mingw32 cross-compilation.
  • Loading branch information
maelvls committed May 5, 2017
1 parent b831a8c commit ccb5a5639de46b5335b0e4b73d0ee10d0f4b5379
Showing 10 changed files with 4,407 additions and 126 deletions.
@@ -1,4 +1,4 @@
all: ext build
all: ext/lib/libyices.a build
# Be helpful if not configured
Makefile.config: configure
@echo Please run ./configure first; exit 1
@@ -25,7 +25,7 @@ CMA_FILE = src/$(LIB_NAME).cma
CMXA_FILE = src/$(LIB_NAME).cmxa
LIB_FILE = src/lib$(LIB_NAME)_stubs.a
A_FILE = src/$(LIB_NAME).a # Generated with the .cmxa
DLL_FILE = src/dll$(LIB_NAME)_stubs.so
DLL_FILE = src/dll$(LIB_NAME)_stubs.$(SO)

ANNOT_FILES = $(ML_SOURCE:%.ml=%.annot)
ifdef BIN_ANNOT
@@ -37,13 +37,21 @@ TESTS_OPT = $(TESTS:%.ml=%.opt)


# Build and install files

BUILD_FILES = $(CMA_FILE) $(DLL_FILE) $(LIB_FILE)
# For now, DLL_FILE is not built because it needs either a PIC libyices.a
# that we could build with --with-pic, or the shared library libyices.so.
# For now, only the static stub is built and linked statically against
# non-PIC libyices.a.
# We also put libgmp.a (if a static libgmp has been found/given) to be sure
# that a static version of libgmp is picked in priority when linking against
# Zarith. To avoid this behaviour, just pass --with-shared-gmp.
BUILD_FILES = $(CMA_FILE) $(LIB_FILE)
INSTALL_FILES = META \
$(CMA_FILE) $(DLL_FILE) $(LIB_FILE)\
$(CMA_FILE) $(LIB_FILE) \
$(MLI_SOURCE) $(CMI_FILES) \
$(ANNOT_FILES) \
src/libyices.a
ext/lib/libyices.a \
$(if $(STATIC_GMP),src/libgmp.a)

ifdef HAVE_OCAMLOPT
BUILD_FILES += $(CMXA_FILE) $(CMXS_FILE) $(A_FILE)
INSTALL_FILES += $(CMXA_FILE) $(CMXS_FILE) $(A_FILE)
@@ -61,13 +69,15 @@ ifdef HAVE_OUNIT
endif

################################################################################
src/libyices.a: ext/lib/libyices.a
cp $^ $@

ext: ext/libyices.a

ext/libyices.a:
$(MAKE) -C ext
src/libyices.a: ext/libyices.a
cp ext/libyices.a src/libyices.a
MAKE_VARIABLES = \
$(if $(STATIC_GMP),STATIC_GMP=$(STATIC_GMP)) \
$(if $(FORCE_SHARED_GMP),FORCE_SHARED_GMP=$(FORCE_SHARED_GMP)) \
HOST=$(HOST)
ext/lib/libyices.a:
$(MAKE) -C ext $(MAKE_VARIABLES)

debug: CFLAGS += -DDEBUG
debug: build
@@ -96,16 +106,26 @@ src/types.o: src/types.c src/config.h src/types.h src/terms.h src/misc.h
# -custom will simply integrate the ocamlrun.a in the library. With -custom,
# the resulting library will be forced to be a static library (.a).
%.o: %.c
$(OCAMLFIND) ocamlc -g -custom -c $< -ccopt '-std=c99 -fPIC $(CFLAGS) -I$(OCAML_LIBDIR) -I$(ZARITH_LIBDIR) -Iext -Isrc'
$(OCAMLFIND) ocamlc $(PACKAGES) -g -custom -c $< -ccopt '-std=c99 $(CFLAGS) -Iext/include -Isrc $(CPPFLAGS)'
mv $(notdir $@) $@

ifneq ($(STATIC_GMP),)
src/libgmp.a: $(STATIC_GMP)
cp $^ $@
$(LIB_FILE) $(DLL_FILE): | src/libgmp.a
endif

# Compile libyices2_stubs.a and dllyices2_stubs.so.
# NOTE: If I use the flag -Lext for finding the library -lyices, the resulting
# library will complain about -Lext being useless.
# To avoid that, we ocamlmklib in the same dir as libyices.a and use -L. (which
# should not output any warning when building with the yices2 package).
src/lib$(LIB_NAME)_stubs.a src/dll$(LIB_NAME)_stubs.so: $(OBJECTS) | src/libyices.a
cd $(dir $@) && $(OCAMLFIND) ocamlmklib -o $(LIB_NAME)_stubs $(notdir $^) $(LDFLAGS) $(LIBS) -L.
#
# The preprocessor variable -DNOYICES_DLL allows to disable the linking to a dll
# and thus you can link to a static libyices.a instead of libyices.dll.a/libyices.a.
# -custom = only produce static libyices_stubs.a, not the shared dllyices_stubs.so.
$(LIB_FILE) $(DLL_FILE): $(OBJECTS) | src/libyices.a
cd src && $(OCAMLFIND) ocamlmklib -o $(LIB_NAME)_stubs $(notdir $^) $(LDFLAGS) $(LIBS) -custom -lyices -L. -ccopt -DNOYICES_DLL

src/%.cmi: src/%.mli
$(OCAMLFIND) ocamlc $(PACKAGES) -I src -annot $(BIN_ANNOT) -c -o $@ $<
@@ -116,17 +136,17 @@ src/%.cmx: src/%.ml

# Library compilation ##########################################################

%$(LIB_NAME).cma: %$(LIB_NAME).cmo | %lib$(LIB_NAME)_stubs.a %dll$(LIB_NAME)_stubs.so
%$(LIB_NAME).cma: %$(LIB_NAME).cmo | %lib$(LIB_NAME)_stubs.a %dll$(LIB_NAME)_stubs.$(SO)
$(OCAMLFIND) ocamlc -a \
-cclib '-l$(LIB_NAME)_stubs -lyices -lgmp $(LDFLAGS) $(LIBS)' \
-cclib '-l$(LIB_NAME)_stubs -lyices $(LDFLAGS) $(LIBS)' \
-custom $^ -o $@

%$(LIB_NAME).cmxa %$(LIB_NAME).a: %$(LIB_NAME).cmx | %lib$(LIB_NAME)_stubs.a
$(OCAMLFIND) ocamlopt -a \
-cclib '-l$(LIB_NAME)_stubs -lyices -lgmp $(LDFLAGS) $(LIBS)' \
-cclib '-l$(LIB_NAME)_stubs -lyices $(LDFLAGS) $(LIBS)' \
$^ -o $@

%$(LIB_NAME).cmxs %$(LIB_NAME).so: %$(LIB_NAME).cmxa %$(LIB_NAME).cmx | %dll$(LIB_NAME)_stubs.so
%$(LIB_NAME).cmxs %$(LIB_NAME).$(SO): %$(LIB_NAME).cmxa %$(LIB_NAME).cmx | %dll$(LIB_NAME)_stubs.$(SO)
$(OCAMLFIND) ocamlopt -shared -I $(dir $@) $^ -o $@

# Documentation ################################################################
@@ -18,4 +18,16 @@ CC = @CC@

# Configuration
CFLAGS = @CFLAGS@
LIBS = -lyices @LIBS@
LIBS = @LIBS@

CPPFLAGS = @CPPFLAGS@
CFLAGS = @CFLAGS@
LDFLAGS = @LDFLAGS@

HOST_OS = @host_os@
HOST = @host@
HOST_CPU = @host_cpu@

SO = @SO@
STATIC_GMP = @STATIC_GMP@
FORCE_SHARED_GMP = @FORCE_SHARED_GMP@

0 comments on commit ccb5a56

Please sign in to comment.