Remakefile.in 2.32 KB
Newer Older
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
FILES = \
	Flocq_version.v \
	Core/Fcore_Raux.v \
	Core/Fcore_Zaux.v \
	Core/Fcore_defs.v \
	Core/Fcore_digits.v \
	Core/Fcore_float_prop.v \
	Core/Fcore_FIX.v \
	Core/Fcore_FLT.v \
	Core/Fcore_FLX.v \
	Core/Fcore_FTZ.v \
	Core/Fcore_generic_fmt.v \
	Core/Fcore_rnd.v \
	Core/Fcore_rnd_ne.v \
	Core/Fcore_ulp.v \
	Core/Fcore.v \
	Calc/Fcalc_bracket.v \
	Calc/Fcalc_digits.v \
	Calc/Fcalc_div.v \
	Calc/Fcalc_ops.v \
	Calc/Fcalc_round.v \
	Calc/Fcalc_sqrt.v \
	Prop/Fprop_div_sqrt_error.v \
	Prop/Fprop_mult_error.v \
	Prop/Fprop_plus_error.v \
	Prop/Fprop_relative.v \
	Prop/Fprop_Sterbenz.v \
28
	Appli/Fappli_rnd_odd.v \
Guillaume Melquiond's avatar
Guillaume Melquiond committed
29
	Appli/Fappli_IEEE.v \
30 31
	Appli/Fappli_IEEE_bits.v \
	Appli/Fappli_double_round.v
Guillaume Melquiond's avatar
Guillaume Melquiond committed
32 33 34

OBJS = $(addprefix src/,$(addsuffix o,$(FILES)))

35 36
EXAMPLES = \
	Double_round_beta_odd.v \
37
	Sqrt_sqr.v \
38
	average.v \
39
	Triangle.v
40 41 42

EOBJS = $(addprefix examples/,$(addsuffix o,$(EXAMPLES)))

43 44
.PHONY: all clean dist doc install

Guillaume Melquiond's avatar
Guillaume Melquiond committed
45 46
all: $(OBJS)

47 48
check: $(EOBJS)

Guillaume Melquiond's avatar
Guillaume Melquiond committed
49 50 51
Remakefile: Remakefile.in config.status
	./config.status Remakefile

52 53 54
src/Flocq_version.v: src/Flocq_version.v.in config.status
	./config.status src/Flocq_version.v

Guillaume Melquiond's avatar
Guillaume Melquiond committed
55 56 57 58 59 60 61 62 63
configure config.status: configure.in
	autoconf
	./config.status --recheck

%.vo: %.v
	@COQDEP@ -R src Flocq $< | @REMAKE@ -r $@
	@COQC@ -R src Flocq -dont-load-proofs $<

clean:
64
	rm -f $(OBJS) $(EOBJS) src/*.glob examples/*.glob
Guillaume Melquiond's avatar
Guillaume Melquiond committed
65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84

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))

doc: html/index.html

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

EXTRA_DIST = \
	configure

Guillaume Melquiond's avatar
Guillaume Melquiond committed
85 86 87 88
REMOVE_FROM_DIST = \
	src/Appli/Fappli_Axpy.v \
	src/Translate/

Guillaume Melquiond's avatar
Guillaume Melquiond committed
89 90 91 92 93 94 95 96
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
Guillaume Melquiond's avatar
Guillaume Melquiond committed
97
	for f in $(REMOVE_FROM_DIST) ; do rm -rf $PACK/$f; done
Guillaume Melquiond's avatar
Guillaume Melquiond committed
98 99 100 101 102
	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