Commit 07c3c8c2 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Move to remake.

parent 62bd2022
......@@ -5,10 +5,11 @@ config.log
config.status
configure
install-sh
Makefile.in
Makefile
missing
Remakefile
.remake
remake
remake.exe
html
src/Flocq_version.v
*.vo
*.vd
*.glob
Prerequisites
-------------
You will need the Coq proof assistant (>= 8.2) with a Reals theory
You will need the Coq proof assistant (>= 8.3) with a Reals theory
compiled in.
The .tar.gz file is distributed with a working set of configure files.
They are not in the SVN repository though. Consequently, if you are
building from SVN, you will need autoconf (>= 2.59) and automake (>= 1.8).
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).
Configuring, compiling and installing
......@@ -14,14 +14,15 @@ 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".
Similarly, COQDEP can be used to specify the location of "coqdep". The
COQBIN environment variable can be used to set both variables at once.
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/Flocq".
The files are compiled at a logical location starting with "Flocq". This
default prefix can be removed with the "--disable-prefix" option.
The files are compiled at a logical location starting with "Flocq".
SUBDIRS = src
EXTRA_DIST = autogen.sh
......@@ -28,45 +28,53 @@ FILES = \
Appli/Fappli_IEEE.v \
Appli/Fappli_IEEE_bits.v
EXTRA_DIST = $(FILES)
CLEANFILES = $(FILES:=o) $(FILES:=d) $(FILES:.v=.glob)
OBJS = $(addprefix src/,$(addsuffix o,$(FILES)))
datadir = $(libdir)
all: $(OBJS)
all: $(FILES:=o)
Remakefile: Remakefile.in config.status
./config.status Remakefile
.v.vo:
@echo COQC $<
@$(COQC) $(COQRFLAG) -dont-load-proofs $<
configure config.status: configure.in
autoconf
./config.status --recheck
.v.vd:
@echo COQDEP $<
@$(COQDEP) -I Core -I Calc -I Prop -I Appli $< > $@
%.vo: %.v
@COQDEP@ -R src Flocq $< | @REMAKE@ -r $@
@COQC@ -R src Flocq -dont-load-proofs $<
SUFFIXES = .v .vo .vd
clean:
rm -f $(OBJS) src/*.glob
install-data-local:
@$(NORMAL_INSTALL)
@test -z "$(datadir)" || \
for p in Core Calc Prop Appli; do \
$(MKDIR_P) "$(DESTDIR)$(datadir)/$$p"; \
done
@list='$(FILES:=o)'; test -n "$(datadir)" || list=; \
for p in $$list; do \
if test -f "$$p"; then d=; else d="$(srcdir)/"; fi; \
echo "$$d$$p" "$(DESTDIR)$(datadir)/$$p"; \
done | \
while read src dst; do \
echo " $(INSTALL_DATA) $$src $$dst"; \
$(INSTALL_DATA) "$$src" "$$dst" || exit $$?; \
done
html/index.html: $(OBJS)
rm -rf html
mkdir -p html
@COQDOC@ -toc -interpolate -utf8 -html -g -R src Flocq -d html \
--coqlib http://coq.inria.fr/distrib/current/stdlib/ \
$(addprefix src/,$(FILES))
uninstall-local:
@$(NORMAL_UNINSTALL)
test -z "$(datadir)" || rm -rf "$(DESTDIR)$(datadir)/$$p"
doc: html/index.html
html: $(FILES:=o)
@mkdir -p ../html
$(COQDOC) -toc -g -R . Flocq -d ../html -t 'Flocq' --coqlib 'http://coq.inria.fr/library/' $(FILES)
install:
prefix=@prefix@
exec_prefix=@exec_prefix@
mkdir -p @libdir@
for d in Core Calc Prop Appli; do mkdir -p @libdir@/$d; done
for f in $(OBJS); do cp $f @libdir@/${f#src/}; done
-include $(FILES:=d)
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
cat /dev/null > $PACK/ChangeLog
rm `find $PACK -name .gitignore`
tar czf $PACK.tar.gz $PACK
rm -rf $PACK
AC_INIT([Flocq], [2.1.0],
[Sylvie Boldo <sylvie.boldo@inria.fr>, Guillaume Melquiond <guillaume.melquiond@inria.fr>],
[flocq])
AM_INIT_AUTOMAKE
m4_divert_push(99)
if test "$ac_init_help" = "long"; then
......@@ -14,22 +13,43 @@ Fine tuning of the installation directory:
AS_HELP_STRING([--libdir=DIR], [library @<:@DIR=`$COQC -where`/user-contrib/Flocq@:>@])
m4_divert_pop([HELP_ENABLE])
AC_PROG_CXX
AC_ARG_VAR(COQBIN, [path to Coq executables [empty]])
if test ${COQBIN##*/}; then COQBIN=$COQBIN/; fi
AC_ARG_VAR(COQC, [Coq compiler command [coqc]])
AC_CHECK_TOOL(COQC, coqc)
AC_MSG_CHECKING([for coqc])
if test ! "$COQC"; then COQC=`which ${COQBIN}coqc`; fi
AC_MSG_RESULT([$COQC])
AC_ARG_VAR(COQDEP, [Coq dependency analyzer command [coqdep]])
AC_CHECK_TOOL(COQDEP, coqdep)
AC_MSG_CHECKING([for coqdep])
if test ! "$COQDEP"; then COQDEP=`which ${COQBIN}coqdep`; fi
AC_MSG_RESULT([$COQDEP])
AC_ARG_VAR(COQDOC, [Coq documentation tool [coqdoc]])
AC_CHECK_TOOL(COQDOC, coqdoc)
AC_ARG_VAR(COQDOC, [Coq documentation generator command [coqdoc]])
AC_MSG_CHECKING([for coqdoc])
if test ! "$COQDOC"; then COQDOC=`which ${COQBIN}coqdoc`; fi
AC_MSG_RESULT([$COQDOC])
if test "$libdir" = '${exec_prefix}/lib'; then
libdir='`$(COQC) -where`/user-contrib/Flocq'
libdir="`$COQC -where`/user-contrib/Flocq"
fi
AC_SUBST(COQRFLAG, ['-R . Flocq'])
AC_ARG_ENABLE([prefix], AS_HELP_STRING([--disable-prefix], [do not compile files into a Flocq module]),
[if test "$enable_prefix" = "no"; then COQRFLAG= ; fi], [])
AC_CONFIG_FILES([Makefile src/Makefile src/Flocq_version.v])
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 src/Flocq_version.v])
AC_OUTPUT
This diff is collapsed.
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