Makefile.install

##########################################################################
##         #   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 ($(COQPREFIX),local)
install:
	@echo "Prefix not set in configure, 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
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

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
install-coqide: $(BCONTEXT)/coqide.install
	dune install --display quiet $(DESTDIRARG) --mandir="$(MANDIR)" --prefix="$(COQPREFIX)" coqide
endif

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