# -*- 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
.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"

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> && dune build -p coq && dune install -p coq"
	@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 ""
	@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 using release mode, to install a package use: "
	@echo ""
	@echo "  - 'dune install -p package'"
	@echo ""
	@echo " Example: "
	@echo ""
	@echo "  - 'dune build -p coq,coqide-server,coqide && dune install -p coq coqide-server coqide'"
	@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 @refman-html

refman-pdf:
	dune build @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 install -p PACKAGE' where"
	@echo "PACKAGE is any of the packages defined by opam files in the root dira"

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

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