aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.install
blob: 4800f8f3faf66e778ea3cc34f47f29d1e5359b5d (plain)
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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
#######################################################################
#  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
# <O___,, #        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              #
#   \VV/  #############################################################
#    //   #      This file is distributed under the terms of the      #
#         #       GNU Lesser General Public License Version 2.1       #
#######################################################################

# 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 ($(LOCAL),true)
install:
	@echo "Nothing to install in a local build!"
else
install: install-coq install-coqide install-doc-$(WITHDOC) install-meta
endif

# NOTA: for install-coqide, see Makefile.ide

install-doc-all: install-doc
install-doc-no:

.PHONY: install install-doc-all install-doc-no

#These variables are intended to be set by the caller to make
#COQINSTALLPREFIX=
#OLDROOT=

  # Can be changed for a local installation (to make packages).
  # You must NOT put a "/" at the end (Cygnus for win32 does not like "//").

ifdef COQINSTALLPREFIX
FULLBINDIR=$(BINDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLCOQLIB=$(COQLIBINSTALL:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLCONFIGDIR=$(CONFIGDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLDATADIR=$(DATADIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLCOQDOCDIR=$(COQDOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
FULLDOCDIR=$(DOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
else
FULLBINDIR=$(BINDIR)
FULLCOQLIB=$(COQLIBINSTALL)
FULLCONFIGDIR=$(CONFIGDIR)
FULLDATADIR=$(DATADIR)
FULLMANDIR=$(MANDIR)
FULLEMACSLIB=$(EMACSLIB)
FULLCOQDOCDIR=$(COQDOCDIR)
FULLDOCDIR=$(DOCDIR)
endif

.PHONY: install-coq install-binaries install-byte install-opt
.PHONY: install-tools install-library install-devfiles
.PHONY: install-coq-info install-coq-manpages install-emacs install-latex
.PHONY: install-meta

install-coq: install-binaries install-library install-coq-info install-devfiles

ifeq ($(BEST),byte)
install-coq: install-byte
endif

install-binaries: install-tools
	$(MKDIR) $(FULLBINDIR)
	$(INSTALLBIN) $(COQC) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR)
	$(MKDIR) $(FULLCOQLIB)/toploop
ifeq ($(BEST),opt)
	$(INSTALLBIN) $(TOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/
endif

install-byte: install-coqide-byte
	$(MKDIR) $(FULLBINDIR)
	$(INSTALLBIN) $(COQTOPBYTE) $(FULLBINDIR)
	$(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/
	$(INSTALLSH) $(FULLCOQLIB) $(LINKCMO) $(PLUGINS)
ifndef CUSTOM
	$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
endif

install-tools:
	$(MKDIR) $(FULLBINDIR)
	# recopie des fichiers de style pour coqide
	$(MKDIR) $(FULLCOQLIB)/tools/coqdoc
	$(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
	$(INSTALLBIN) $(TOOLS) $(FULLBINDIR)

# The list of .cmi to install, including in particular
# - the ones obtained from .mli without .ml
# - the ones of modules in core cma's
# - the ones corresponding to packed plugins

INSTALLCMI = $(sort \
	$(filter-out checker/% ide/% tools/%, $(MLIFILES:.mli=.cmi)) \
	$(foreach lib,$(CORECMA), $(addsuffix .cmi,$($(lib:.cma=_MLLIB_DEPENDENCIES))))) \
	$(PLUGINS:.cmo=.cmi)

install-devfiles:
	$(MKDIR) $(FULLBINDIR)
	$(INSTALLBIN) $(COQMKTOP) $(FULLBINDIR)
	$(MKDIR) $(FULLCOQLIB)
	$(INSTALLSH)  $(FULLCOQLIB) $(GRAMMARCMA)
	$(INSTALLSH)  $(FULLCOQLIB) $(INSTALLCMI)
	$(INSTALLSH)  $(FULLCOQLIB) $(TOOLS_HELPERS)
ifeq ($(BEST),opt)
	$(INSTALLSH)  $(FULLCOQLIB) $(LINKCMX) $(CORECMA:.cma=.a) $(STATICPLUGINS:.cma=.a)
endif

install-library:
	$(MKDIR) $(FULLCOQLIB)
	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES)
	$(MKDIR) $(FULLCOQLIB)/user-contrib
	$(MKDIR) $(FULLCOQLIB)/kernel/byterun
ifndef CUSTOM
	$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)/kernel/byterun
endif
ifeq ($(BEST),opt)
	$(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)/kernel/byterun
	$(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT)
endif
# csdpcert is not meant to be directly called by the user; we install
# it with libraries
	-$(MKDIR) $(FULLCOQLIB)/plugins/micromega
	$(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/plugins/micromega
	rm -f $(FULLCOQLIB)/revision
	-$(INSTALLLIB) revision $(FULLCOQLIB)

install-coq-info: install-coq-manpages install-emacs install-latex

MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
	man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \
	man/coqwc.1 man/coqdoc.1 man/coqide.1 \
	man/coq_makefile.1 man/coqmktop.1 man/coqchk.1

install-coq-manpages:
	$(MKDIR) $(FULLMANDIR)/man1
	$(INSTALLLIB) $(MANPAGES) $(FULLMANDIR)/man1

install-emacs:
	$(MKDIR) $(FULLEMACSLIB)
	$(INSTALLLIB) tools/gallina-db.el tools/coq-font-lock.el tools/gallina-syntax.el tools/gallina.el tools/coq-inferior.el $(FULLEMACSLIB)

# command to update TeX' kpathsea database
#UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null

install-latex:
	$(MKDIR) $(FULLCOQDOCDIR)
	$(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR)
#	-$(UPDATETEX)

install-meta: META.coq
	$(INSTALLLIB) META.coq $(FULLCOQLIB)/META

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