Commit ce89a1a4 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Switch build system to remake.

parent 2cece95d
......@@ -4,10 +4,9 @@ ChangeLog
config.log
config.status
configure
install-sh
Makefile.in
Makefile
missing
.remake
remake
remake.exe
*.vo
*.vd
*.glob
Prerequisites
-------------
You will need the Coq proof assistant (>= 8.2) with a Reals theory compiled
You will need the Coq proof assistant (>= 8.4) with a Reals theory compiled
in. You will need the Flocq library (http://flocq.gforge.inria.fr/) to be
installed too.
The .tar.gz file is distributed with a working set of configure files. They
are not in the GIT repository though. Consequently, if you are building from
GIT, you will need autoconf (>= 2.59) and automake (>= 1.8).
are not in the git repository though. Consequently, if you are building from
git, you will need autoconf (>= 2.59).
Configuring, compiling and installing
......@@ -15,14 +15,13 @@ Configuring, compiling and installing
Ideally, you should just have to type:
$ ./configure && make && make install
$ ./configure && ./remake && ./remake install
The environment variable "COQC" can be set to the Coq compiler command. The
configure script defaults to "coqc".
The environment variable COQC can be passed to the configure script in order
to set the Coq compiler command. The configure script defaults to "coqc".
The option "--libdir=DIR" can be set to the directory where the compiled
library files should be installed by "make install". By default, the target
directory is "`$COQC -where`/user-contrib/Interval".
Option "--libdir=DIR" sets the directory where the compiled library files
should be installed by "./remake install". By default, the target directory
is "`$COQC -where`/user-contrib/Interval".
The files are compiled at a logical location starting with "Interval". This
default prefix can be removed with the "--disable-prefix" option.
The files are compiled at a logical location starting with "Interval".
SUBDIRS = src testsuite
EXTRA_DIST = autogen.sh
FILES = \
Interval_bigint_carrier.v \
Interval_bisect.v \
Interval_definitions.v \
Interval_float_sig.v \
Interval_generic_ops.v \
Interval_generic_proof.v \
Interval_generic.v \
Interval_interval.v \
Interval_interval_float.v \
Interval_interval_float_full.v \
Interval_missing.v \
Interval_specific_ops.v \
Interval_specific_sig.v \
Interval_stdz_carrier.v \
Interval_tactic.v \
Interval_transcend.v \
Interval_xreal.v \
Interval_xreal_derive.v
OBJS = $(addprefix src/,$(addsuffix o,$(FILES)))
all: $(OBJS)
clean: src/clean testsuite/clean
check: testsuite/check
Remakefile: Remakefile.in config.status
./config.status Remakefile
configure config.status: configure.in
autoconf
./config.status --recheck
%.vo: %.v
@COQDEP@ -R src Interval ${1%.vo}.v | @REMAKE@ -r $1
@COQC@ -R src Interval -dont-load-proofs ${1%.vo}.v
src/clean:
rm -f $OBJS src/*.glob
testsuite/check: src/Interval_tactic.vo
set +e
cd testsuite
logfile="failures-$(date '+%Y-%m-%d').log"
cat /dev/null > log.tmp
cat /dev/null > "$logfile"
for f in *.v; do
cp "$f" check_tmp.v
@COQC@ -R ../src Interval check_tmp.v > output.tmp 2>&1
return_code=$?
if [ ${return_code} -ne 0 ]; then
(echo "*** $f exited with error code ${return_code}"; cat output.tmp; echo) >> "$logfile"
echo "$f exited with error code ${return_code}" >> log.tmp
fi
rm -f check_tmp.v check_tmp.vo check_tmp.glob output.tmp
done
return_code=0
if [ -s log.tmp ]; then
echo "*** Failures:"
cat log.tmp
return_code=1
else
rm "$logfile"
fi
rm log.tmp
exit ${return_code}
testsuite/clean:
rm -f testsuite/failures-*.log
install:
prefix=@prefix@
exec_prefix=@exec_prefix@
mkdir -p @libdir@
cp $OBJS @libdir@
EXTRA_DIST = \
configure
dist: $(EXTRA_DIST)
PACK=@PACKAGE_TARNAME@-@PACKAGE_VERSION@
DIRS=$(git ls-tree -d -r --name-only HEAD)
FILES=$(git ls-tree -r --name-only HEAD)
rm -rf $PACK.tar.gz $PACK
mkdir $PACK
for d in $DIRS; do mkdir $PACK/$d; done
for f in $FILES ${EXTRA_DIST}; do cp $f $PACK/$f; done
git log --pretty="format:%ad %s" --date=short > $PACK/ChangeLog
rm $(find $PACK -name .gitignore)
tar czf $PACK.tar.gz $PACK
rm -rf $PACK
AC_INIT([Interval], [0.15.1],
[Guillaume Melquiond <guillaume.melquiond@inria.fr>],
[interval])
AM_INIT_AUTOMAKE
m4_divert_push(99)
if test "$ac_init_help" = "long"; then
......@@ -14,6 +13,8 @@ Fine tuning of the installation directory:
AS_HELP_STRING([--libdir=DIR], [library @<:@DIR=`$COQC -where`/user-contrib/Interval@:>@])
m4_divert_pop([HELP_ENABLE])
AC_PROG_CXX
AC_ARG_VAR(COQC, [Coq compiler command [coqc]])
AC_CHECK_TOOL(COQC, coqc)
......@@ -31,12 +32,22 @@ AS_IF(
rm -f conftest.v conftest.vo conftest.err
if test "$libdir" = '${exec_prefix}/lib'; then
libdir='`$(COQC) -where`/user-contrib/Interval'
libdir="`$COQC -where`/user-contrib/Interval"
fi
AC_SUBST(COQRFLAG, ['-R . Interval'])
AC_ARG_ENABLE([prefix], AS_HELP_STRING([--disable-prefix], [do not compile files into an Interval module]),
[if test "$enable_prefix" = "no"; then COQRFLAG= ; fi], [])
AC_CONFIG_FILES([Makefile src/Makefile testsuite/Makefile])
AC_MSG_NOTICE([building remake...])
case `uname -s` in
MINGW*)
$CXX -Wall -O2 -o remake.exe remake.cpp -lws2_32
if test $? != 0; then AC_MSG_FAILURE([failed]); fi
AC_SUBST([REMAKE], [./remake.exe])
;;
*)
$CXX -Wall -O2 -o remake remake.cpp
if test $? != 0; then AC_MSG_FAILURE([failed]); fi
AC_SUBST([REMAKE], [./remake])
;;
esac
AC_CONFIG_FILES(Remakefile)
AC_OUTPUT
This diff is collapsed.
FILES = \
Interval_bigint_carrier.v \
Interval_bisect.v \
Interval_definitions.v \
Interval_float_sig.v \
Interval_generic_ops.v \
Interval_generic_proof.v \
Interval_generic.v \
Interval_interval.v \
Interval_interval_float.v \
Interval_interval_float_full.v \
Interval_missing.v \
Interval_specific_ops.v \
Interval_specific_sig.v \
Interval_stdz_carrier.v \
Interval_tactic.v \
Interval_transcend.v \
Interval_xreal.v \
Interval_xreal_derive.v
data_DATA = $(FILES:=o)
EXTRA_DIST = $(FILES)
CLEANFILES = $(FILES:=o) $(FILES:=d) $(FILES:.v=.glob)
datadir = $(libdir)
.v.vo:
@echo COQC $<
@$(COQC) $(COQRFLAG) -dont-load-proofs $<
.v.vd:
@echo COQDEP $<
@$(COQDEP) -I . $< > $@
SUFFIXES = .v .vo .vd
-include $(FILES:=d)
EXTRA_DIST = $(wildcard *.v)
check:
@logfile="failures-$$(date '+%Y-%m-%d').log"; \
cat /dev/null > log.tmp; \
cat /dev/null > "$$logfile"; \
for f in $(EXTRA_DIST); do \
cp "$$f" check_tmp.v; \
$(COQC) -R ../src Interval check_tmp.v > output.tmp 2>&1; \
return_code=$$?; \
if [ $${return_code} -ne 0 ]; then \
(echo "*** $$f exited with error code $${return_code}"; cat output.tmp; echo) >> "$$logfile"; \
echo "$$f exited with error code $${return_code}" >> log.tmp; \
fi; \
rm -f check_tmp.v check_tmp.vo check_tmp.glob output.tmp; \
done; \
return_code=0; \
if [ -s log.tmp ]; then \
echo "*** Failures:"; \
cat log.tmp; \
return_code=1; \
else \
rm "$$logfile"; \
fi; \
rm log.tmp; \
exit $${return_code}
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment