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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
##########################################################################
## # The Coq Proof Assistant / The Coq Development Team ##
## v # Copyright INRIA, CNRS and contributors ##
## <O___,, # (see version control and CREDITS file for authors & dates) ##
## \VV/ ###############################################################
## // # This file is distributed under the terms of the ##
## # GNU Lesser General Public License Version 2.1 ##
## # (see LICENSE file for the text of the license) ##
##########################################################################
# This file calls [find] and as such is not suitable for inclusion in
# the test suite Makefile, unlike Makefile.common.
ifdef QUICK
VO=vio
else
VO=vo
endif
###########################################################################
# vo files
###########################################################################
THEORIESVO := $(patsubst %.v,%.$(VO),$(shell find theories -type f -name "*.v"))
CONTRIBVO := $(patsubst %.v,%.$(VO),$(shell find $(addprefix user-contrib/, $(USERCONTRIBDIRS)) -type f -name "*.v"))
ALLVO := $(THEORIESVO) $(CONTRIBVO)
VFILES := $(ALLVO:.$(VO)=.v)
## More specific targets
THEORIESLIGHTVO:= \
$(filter theories/Init/% theories/Logic/% theories/Unicode/% theories/Arith/%, $(THEORIESVO))
# convert a (stdlib) filename into a module name:
# remove .vo, replace stdlib by Coq, and replace slashes by dots
vo_to_mod = $(subst /,.,$(patsubst user-contrib/%,%,$(patsubst theories/%,Coq.%,$(1:.vo=))))
ALLMODS:=$(call vo_to_mod,$(ALLVO:.$(VO)=.vo))
# Converting a stdlib filename into native compiler filenames
# Used for install targets
vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%,N%, $(patsubst theories/%,NCoq_%,$(vo:.$(VO)=.cm*)))))
vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%,N%, $(patsubst theories/%,NCoq_%,$(vo:.$(VO)=.o)))))
ifdef QUICK
GLOBFILES:=
else
GLOBFILES:=$(ALLVO:.$(VO)=.glob)
endif
ifdef NATIVECOMPUTE
NATIVEFILES := $(call vo_to_cm,$(ALLVO))
ifeq ($(BEST),opt)
NATIVEFILES += $(call vo_to_obj,$(ALLVO))
endif
else
NATIVEFILES :=
endif
# For emacs:
# Local Variables:
# mode: makefile-gmake
# End:
|
