Remakefile.in 2.76 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
EXAMPLES = \
36
	Average.v \
37
	Compute.v \
38 39
	Double_round_beta_odd.v \
	Homogen.v
40 41

MORE_EXAMPLES = \
42
	Cody_Waite.v \
43
	Division_u16.v \
44 45
	Sqrt_sqr.v \
	Triangle.v
46 47

EOBJS = $(addprefix examples/,$(addsuffix o,$(EXAMPLES)))
48
MOBJS = $(addprefix examples/,$(addsuffix o,$(MORE_EXAMPLES)))
49

50
.PHONY: all check check-more clean dist doc install
51

Guillaume Melquiond's avatar
Guillaume Melquiond committed
52 53
all: $(OBJS)

54 55
check: $(EOBJS)

56 57
check-more: $(MOBJS)

Guillaume Melquiond's avatar
Guillaume Melquiond committed
58 59 60
Remakefile: Remakefile.in config.status
	./config.status Remakefile

61 62 63
src/Flocq_version.v: src/Flocq_version.v.in config.status
	./config.status src/Flocq_version.v

Guillaume Melquiond's avatar
Guillaume Melquiond committed
64 65 66 67 68 69
configure config.status: configure.in
	autoconf
	./config.status --recheck

%.vo: %.v
	@COQDEP@ -R src Flocq $< | @REMAKE@ -r $@
70
	@COQC@ -R src Flocq $<
Guillaume Melquiond's avatar
Guillaume Melquiond committed
71 72

clean:
73
	rm -f $(OBJS) $(EOBJS) $(MOBJS) src/*.glob examples/*.glob
74 75 76
	for d in src src/Core src/Calc src/Prop src/Appli examples; do \
	  rm -f $d/.coq-native/*.o $d/.coq-native/*.cm*; done
	find . -type d -name ".coq-native" -empty -prune -exec rmdir "{}" \;
Guillaume Melquiond's avatar
Guillaume Melquiond committed
77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92

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
93
	( cd src && find . -type d -name ".coq-native" -exec cp -RT "{}" "@libdir@/{}" \; )
Guillaume Melquiond's avatar
Guillaume Melquiond committed
94 95 96 97

EXTRA_DIST = \
	configure

Guillaume Melquiond's avatar
Guillaume Melquiond committed
98 99 100 101
REMOVE_FROM_DIST = \
	src/Appli/Fappli_Axpy.v \
	src/Translate/

Guillaume Melquiond's avatar
Guillaume Melquiond committed
102 103 104 105 106 107 108 109
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
110
	for f in $(REMOVE_FROM_DIST) ; do rm -rf $PACK/$f; done
Guillaume Melquiond's avatar
Guillaume Melquiond committed
111 112 113 114 115
	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