# -*- mode: makefile -*-
# Dune Makefile for Coq

.PHONY: help help-install states world watch check    # Main developer targets
.PHONY: refman-html refman-pdf stdlib-html apidoc     # Documentation targets
.PHONY: test-suite dev-targets
.PHONY: fmt ocheck ireport clean                      # Maintenance targets
.PHONY: voboot release install                        # Added just not to break old scripts

# use DUNEOPT=--display=short for a more verbose build
# DUNEOPT=--display=short

help:
	@echo ""
	@echo "Welcome to Coq's Dune-based build system. Common developer targets are:"
	@echo ""
	@echo "  - states: build a minimal functional coqtop"
	@echo "  - world:  build all public binaries and libraries"
	@echo "  - watch:  build all public binaries and libraries [continuous build]"
	@echo "  - check:  build all ML files as fast as possible"
	@echo "  - test-suite: run Coq's test suite [env NJOBS=N to set job parallelism]"
	@echo ""
	@echo "  Note: running ./configure is not recommended,"
	@echo "        see dev/doc/build-system.dune.md for more info"
	@echo "  Note: these targets produce a developer build, not suitable"
	@echo "        for distribution to end-users or install"
	@echo ""
	@echo " To run an \$$app \\in {coqc,coqtop,coqbyte,coqide}:"
	@echo ""
	@echo "  - use 'dune exec -- dev/shim/\$$app-prelude args'"
	@echo "    Example: 'dune exec -- dev/shim/coqc-prelude file.v'"
	@echo ""
	@echo " Documentation targets:"
	@echo ""
	@echo "  - refman-html: build Coq's reference manual [HTML version]"
	@echo "  - refman-pdf:  build Coq's reference manual [PDF version]"
	@echo "  - stdlib-html: build Coq's Stdlib documentation [HTML version]"
	@echo "  - apidoc:      build ML API documentation"
	@echo ""
	@echo " Miscellaneous targets:"
	@echo ""
	@echo "  - fmt:     run ocamlformat on the codebase"
	@echo "  - ocheck:  build for all supported OCaml versions [requires OPAM]"
	@echo "  - ireport: build with optimized flambda settings and emit an inline report"
	@echo "  - clean:   remove build directory and autogenerated files"
	@echo "  - help:    show this message"
	@echo ""
	@echo " Type 'make help-install' for installation instructions"
	@echo " Type 'make dev-targets' for more developer targets"

dev-targets:
	@echo ""
	@echo "In order to get a functional Coq install layout, the world target is required."
	@echo "However, This is often inconvenient for developers, due to the large amount of"
	@echo "files that world will build. We provide some useful subtargets here:"
	@echo ""
	@echo "  - world-prelude: build Coq's prelude and setup a functional layout on _build/install"

help-install:
	@echo ""
	@echo "The Dune-based Coq build is split in packages; see Dune and dev/doc"
	@echo "documentation for more details. A quick install of Coq alone can done with"
	@echo ""
	@echo " $ ./configure -prefix <install_prefix>"
	@echo " $ dune build -p coq-core,coq-stdlib && dune install coq-core coq-stdlib"
	@echo ""
	@echo " Provided opam/dune packages are:"
	@echo ""
	@echo "  - coq-core: base Coq package, toplevel compilers, plugins, tools, no stdlib, no GTK"
	@echo "  - coq-stdlib: Coq's standard library"
	@echo "  - coqide-server: XML protocol language server"
	@echo "  - coqide: CoqIDE gtk application"
	@echo "  - coq: meta package depending on coq-core coq-stdlib"
	@echo ""
	@echo " To build a package, you can use:"
	@echo ""
	@echo "  - 'dune build package.install' : build package in developer mode"
	@echo "  - 'dune build -p package' : build package in release mode"
	@echo ""
	@echo " Packages _must_ be installed only if built using release mode, to install a package use: "
	@echo ""
	@echo "  - 'dune install $install_opts package'"
	@echo ""
	@echo " Note that building a package in release mode ignores other packages present in"
	@echo " the worktree. See Dune documentation for more information."

voboot:
	@echo "This target is empty and not needed anymore"

states:
	dune build $(DUNEOPT) dev/shim/coqtop-prelude

NONDOC_INSTALL_TARGETS:=coq-core.install coq-stdlib.install coqide-server.install coqide.install

world:
	dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS)

watch:
	dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS) -w

check:
	dune build $(DUNEOPT) @check

test-suite:
	dune runtest --no-buffer $(DUNEOPT)

refman-html:
	dune build --no-buffer @refman-html

refman-pdf:
	dune build --no-buffer @refman-pdf

stdlib-html:
	dune build @stdlib-html

apidoc:
	dune build $(DUNEOPT) @doc

release:
	@echo "release target is deprecated, use dune directly"
	dune build $(DUNEOPT) -p coq

# We define this target as to override Make's built-in one
install:
	@echo "To install Coq using dune, use 'dune build -p P && dune install P'"
	@echo "where P is any of the packages defined by opam files in the root dir"
	@false

fmt:
	dune build @fmt --auto-promote

ocheck:
	dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all

ireport:
	dune clean
	dune build $(DUNEOPT) @install --profile=ireport

clean:
	dune clean

# ci-* targets

CI_PURE_DUNE:=1
export CI_PURE_DUNE
include Makefile.ci

# Custom targets to create subsets of the world target but with less
# compiled files. This is desired when we want to have our Coq Dune
# build with Coq developments that are not dunerized and thus still
# expect an install layout with a working Coq setup, but smaller than
# world.
#
# Unfortunately, Dune still lacks the capability to refer to install
# targets in rules, see https://github.com/ocaml/dune/issues/3192 ;
# thus we can't simply yet use `%{pkg:coq:theories/Arith/Arith.vo` to
# have the rule install the target, we thus imitate such behavior
# using make as a helper.

.PHONY: world-prelude

# We could use more refined rules like below, however it is not really
# worth it as in general ci-packages want everything in coq-core
CORE_TOOLS=coq-core.install

# Exe suffix, likely needed on windows
# EXE=
# CORE_TOOLS=coqdep coqc coq_makefile coqdoc
# CORE_TOOLS_PATH=$(addsuffix, $(EXE), $(addprefix _build/install/default/bin/, $(CORE_TOOLS)))
# CORE_FILES=_build/install/default/lib/coq-core/tools/CoqMakefile.in

# Would be nice to determine a pattern for this, but it is tricky.
# PLUGIN_FILES=$(shell ls plugins/*/*.mllib)
# PLUGIN_FILES_PATH=$(addprefix _build/install/default/lib/coq-core/, $(PLUGIN_FILES:.mllib=.cmxs))

PRELUDE_FILES=$(wildcard theories/Init/*.v)
PRELUDE_FILES_PATH=$(addprefix _build/install/default/lib/coq/, $(PRELUDE_FILES:.v=.vo))

world-prelude:
	@dune build $(CORE_TOOLS) $(PRELUDE_FILES_PATH)

# Other common dev targets:
#
# dune build coq.install
# dune build coqide.install
#
# Packaging / OPAM targets:
#
# dune -p coq @install
# dune -p coqide @install