File: Makefile.vofiles

package info (click to toggle)
coq 8.9.0-1
  • links: PTS, VCS
  • area: main
  • in suites: buster, sid
  • size: 30,604 kB
  • sloc: ml: 192,230; sh: 2,585; python: 2,206; ansic: 1,878; makefile: 818; lisp: 202; xml: 24; sed: 2
file content (46 lines) | stat: -rw-r--r-- 1,576 bytes parent folder | download
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

# This file calls [find] and as such is not suitable for inclusion in
# the test suite Makefile, unlike Makefile.common.

###########################################################################
# vo files
###########################################################################

THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v"))
PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v"))
ALLVO := $(THEORIESVO) $(PLUGINSVO)
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 theories and plugins by Coq, and replace slashes by dots
vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=))))

ALLMODS:=$(call vo_to_mod,$(ALLVO))


# Converting a stdlib filename into native compiler filenames
# Used for install targets
vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*)))))

vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o)))))

GLOBFILES:=$(ALLVO:.vo=.glob)
ifdef NATIVECOMPUTE
NATIVEFILES := $(call vo_to_cm,$(ALLVO))
ifeq ($(BEST),opt)
NATIVEFILES += $(call vo_to_obj,$(ALLVO))
endif
else
NATIVEFILES :=
endif
LIBFILES:=$(ALLVO) $(NATIVEFILES) $(VFILES) $(GLOBFILES)

# For emacs:
# Local Variables:
# mode: makefile
# End: