-
Notifications
You must be signed in to change notification settings - Fork 1
/
Makefile.install
117 lines (97 loc) · 4.49 KB
/
Makefile.install
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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
##########################################################################
## # 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 makefile regroups installation rules
# It is included by Makefile.build
# NOTA: currently, the install rules below assume that everything needed
# has already been correctly built. In particular, this is *not* enforced
# by dependencies between rules, so do *not* try overly clever things like
# 'make world install' in one unique command
ifeq ($(COQ_INSTALL_ENABLED),false)
install:
@echo "Working on devel mode, nothing to install."
else
install: install-coq install-coqide install-doc-$(WITHDOC)
endif
# NOTA: for install-coqide, see Makefile.ide
install-doc-all: install-doc
install-doc-no:
install-byte:
.PHONY: install install-byte install-coqide install-doc-all install-doc-no
INSTALLLIB:=install -m 644
.PHONY: install-coq install-dune install-library
# Due to Windows paths not starting with / we can't just set the
# default to / and always use --destdir
ifeq ($(DESTDIR),)
DESTDIRARG=
else
DESTDIRARG=--destdir="$(DESTDIR)"
endif
# --display quiet should not produce output, dune bug:
# https://github.com/ocaml/dune/issues/4573
# Note that dune install paths are setup at dune's build time, thus
# for example a Debian-built dune will install stuff following
# Debian's FHS, an opam-built dune will differ and follow OPAM's layout.
#
# We ought to improve this, as of today the case of an opam-built dune
# installing to a global prefix such as /usr/local/ may not follow the FHS.
# For now, we respect the values given at configure's time.
ifdef DUNE_29_PLUS
install-dune: $(BCONTEXT)/coq-core.install $(BCONTEXT)/coqide-server.install
dune install --display quiet $(DESTDIRARG) --mandir="$(MANDIR)" --prefix="$(COQPREFIX)" --etcdir="$(CONFIGDIR)" --docdir="$(DOCDIR)" coq-core
dune install --display quiet $(DESTDIRARG) --mandir="$(MANDIR)" --prefix="$(COQPREFIX)" --etcdir="$(CONFIGDIR)" --docdir="$(DOCDIR)" coqide-server
else
install-dune: $(BCONTEXT)/coq-core.install $(BCONTEXT)/coqide-server.install
dune install --display quiet $(DESTDIRARG) --mandir="$(MANDIR)" --prefix="$(COQPREFIX)" coq-core
dune install --display quiet $(DESTDIRARG) --mandir="$(MANDIR)" --prefix="$(COQPREFIX)" coqide-server
endif
# IMPORTANT NOTE: before Dune 2.9, the --docdir and --etcdir options
# were not supported, if using Dune >= 2.9, Coq's configure will set
# the DUNE_29_PLUS=yes` variable to use the call with the right options.
#
# Additionally, you can also add --libdir=$(COQLIBINSTALL) if required
# by your distribution, but we recommend using the default configured
# with Dune.
install-coq: install-dune install-library
# This used to be overriden to fix very old bugs with install
INSTALLSH=./install.sh
ifeq ($(DESTDIR),)
COQLIBINSTALLDEST=$(COQLIBINSTALL)
else
COQLIBINSTALLDEST=$(DESTDIR)/$(COQLIBINSTALL)
endif
# NB: some files don't produce native files (eg Ltac2 files) as they
# don't have any Coq definitions. Makefile can't predict that so we
# use || true vos build is bugged in -quick mode, see #11195
install-library:
$(SHOW)'INSTALL VOFILES'
$(HIDE)$(MKDIR) $(COQLIBINSTALLDEST)
$(HIDE)$(INSTALLSH) $(VO_OUT_DIR) $(COQLIBINSTALLDEST) $(ALLVO:.$(VO)=.vo)
$(HIDE)$(INSTALLSH) $(VO_OUT_DIR) $(COQLIBINSTALLDEST) $(ALLVO:.$(VO)=.vos) || true
ifneq ($(NATIVECOMPUTE),)
$(HIDE)$(INSTALLSH) $(VO_OUT_DIR) $(COQLIBINSTALLDEST) $(NATIVEFILES) || true
endif
$(HIDE)$(INSTALLSH) $(VO_OUT_DIR) $(COQLIBINSTALLDEST) $(VFILES)
$(HIDE)$(INSTALLSH) $(VO_OUT_DIR) $(COQLIBINSTALLDEST) $(GLOBFILES)
$(HIDE)$(MKDIR) $(COQLIBINSTALLDEST)/user-contrib
# TODO
ifeq ($(HASCOQIDE),no)
install-coqide:
else
ifdef DUNE_29_PLUS
install-coqide: $(BCONTEXT)/coqide.install
dune install --display quiet $(DESTDIRARG) --mandir="$(MANDIR)" --prefix="$(COQPREFIX)" --etcdir="$(CONFIGDIR)" --docdir="$(DOCDIR)" coqide
else
dune install --display quiet $(DESTDIRARG) --mandir="$(MANDIR)" --prefix="$(COQPREFIX)" coqide
endif
endif
# For emacs:
# Local Variables:
# mode: makefile
# End: