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

.PHONY: help voboot states world watch check          # Main developer targets
.PHONY: coq coqide coqide-server                      # Package targets
.PHONY: quickbyte quickopt quickide                   # Partial / quick developer targets
.PHONY: refman-html stdlib-html apidoc                # Documentation targets
.PHONY: test-suite release                            # Accessory targets
.PHONY: ocheck trunk ireport clean                    # Maintenance targets

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

BUILD_CONTEXT=_build/default

help:
	@echo "Welcome to Coq's Dune-based build system. Targets are:"
	@echo ""
	@echo "  - states: build a minimal functional coqtop"
	@echo "  - world:  build all binaries and libraries"
	@echo "  - watch:  build all binaries and libraries [continuous build]"
	@echo "  - check:  build all ML files as fast as possible"
	@echo ""
	@echo "  - coq: build package Coq [toplevel compilers, tools, stdlib, no GTK]"
	@echo "  - coqide-server: build package coqide-server [XML protocol language server]"
	@echo "  - coqide: build package CoqIDE [gtk application]"
	@echo ""
	@echo "  - quickbyte: build main ML files [coqtop + plugins + ide + printers] using the bytecode compiler"
	@echo "  - quickopt:  build main ML files [coqtop + plugins + ide + printers] using the optimizing compiler"
	@echo "  - quickide:  build main IDE files [client + server + prelude] using the optimizing compiler"
	@echo ""
	@echo "  - test-suite:  run Coq's test suite"
	@echo "  - refman-html: build Coq's reference manual [HTML version]"
	@echo "  - stdlib-html: build Coq's Stdlib documentation [HTML version]"
	@echo "  - apidoc:      build ML API documentation"
	@echo "  - release:     build Coq in release mode"
	@echo ""
	@echo "  - ocheck:  build for all supported OCaml versions [requires OPAM]"
	@echo "  - trunk:   build with a configuration compatible with OCaml trunk"
	@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"

# We need to bootstrap with a dummy coq.plugins.ltac so install targets do work.
plugins/ltac/dune:
	@echo "(library (name ltac_plugin) (public_name coq.plugins.ltac) (modules_without_implementation extraargs extratactics))" > plugins/ltac/dune

voboot: plugins/ltac/dune
	dune build $(DUNEOPT) @vodeps
	dune exec ./tools/coq_dune.exe $(BUILD_CONTEXT)/.vfiles.d

states: voboot
	dune build --display=short $(DUNEOPT) dev/shim/coqtop-prelude

world: voboot
	dune build $(DUNEOPT) @install

coq: voboot
	dune build $(DUNEOPT) coq.install

coqide: voboot
	dune build $(DUNEOPT) coqide.install

coqide-server: voboot
	dune build $(DUNEOPT) coqide-server.install

watch: voboot
	dune build $(DUNEOPT) @install -w

check: voboot
	dune build $(DUNEOPT) @check

COQTOP_FILES=ide/idetop.bc ide/coqide_main.bc checker/coqchk.bc
PLUGIN_FILES=$(wildcard plugins/*/*.mlpack)
PRINTER_FILES=dev/top_printers.cma
QUICKBYTE_TARGETS=$(COQTOP_FILES) $(PLUGIN_FILES:.mlpack=.cma) $(PRINTER_FILES) topbin/coqtop_byte_bin.bc
QUICKOPT_TARGETS=$(COQTOP_FILES:.bc=.exe) $(PLUGIN_FILES:.mlpack=.cmxs) $(PRINTER_FILES:.cma=.cmxa) topbin/coqtop_bin.exe

quickbyte: voboot
	dune build $(DUNEOPT) $(QUICKBYTE_TARGETS)

quickopt: voboot
	dune build $(DUNEOPT) $(QUICKOPT_TARGETS)

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

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

refman-html: voboot
	dune build @refman-html

stdlib-html: voboot
	dune build @stdlib-html

apidoc: voboot
	dune build $(DUNEOPT) @doc

release: voboot
	dune build $(DUNEOPT) -p coq

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

trunk:
	dune build $(DUNEOPT) --profile=ocaml409 @vodeps
	dune exec coq_dune $(BUILD_CONTEXT)/.vfiles.d
	dune build $(DUNEOPT) --profile=ocaml409 coq.install coqide-server.install

ireport:
	dune clean
	dune build $(DUNEOPT) @vodeps --profile=ireport
	dune exec coq_dune $(BUILD_CONTEXT)/.vfiles.d --profile=ireport
	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