##########################################################################
## # The Rocq Prover / The Rocq 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) ##
##########################################################################
# Dune Makefile for Rocq
.PHONY: help help-install states world rocqide watch check # Main developer targets
.PHONY: refman-html refman-pdf corelib-html apidoc # Documentation targets
.PHONY: test-suite dev-targets
.PHONY: fmt ocheck obuild ireport clean # Maintenance targets
.PHONY: dunestrap release install # Miscellaneous
# We don't allow parallel build here, this is just a placehoder for
# dune commands for the most part
.NOTPARALLEL:
###########################################################################
# The SHOW and HIDE variables control whether make will echo complete commands
# or only abbreviated versions.
# Quiet mode is ON by default except if VERBOSE=1 option is given to make
# Used only by targets which don't go through dune (eg doc_gram_rsts)
VERBOSE ?=
SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)
# use DUNEOPT=--display=short for a more verbose build
# DUNEOPT=--display=short
help:
@echo ""
@echo "Welcome to Rocq's Dune-based build system. If you are final user type"
@echo "make help-install for installation instructions. Common developer targets are:"
@echo ""
@echo " - states: build a minimal functional rocq repl"
@echo " - world: build main public binaries and libraries in developer mode (no rocqide)"
@echo " - watch: build main public binaries and libraries [continuous build]"
@echo " - rocqide: build rocqide binary in developer mode"
@echo " - check: build all ML files as fast as possible"
@echo " - test-suite: run Rocq's test suite [env NJOBS=N to set job parallelism]"
@echo " - dunestrap: Generate the dune rules for vo files"
@echo ""
@echo " Note: running ./configure is not recommended for developers,"
@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,coqtop.byte,rocqide}:"
@echo ""
@echo " - use 'dune exec -- dev/shim/\$$app args'"
@echo " Example: 'dune exec -- dev/shim/coqc file.v'"
@echo ""
@echo " Documentation targets:"
@echo ""
@echo " - refman-html: build Rocq's reference manual [HTML version]"
@echo " - refman-pdf: build Rocq's reference manual [PDF version]"
@echo " - corelib-html: build Rocq's Corelib documentation [HTML version]"
@echo " - apidoc: build ML API documentation"
@echo ""
@echo " Miscellaneous targets:"
@echo ""
@echo " - fmt: run ocamlformat on the codebase"
@echo " - ocheck: check for a selection of supported OCaml versions [requires OPAM]"
@echo " - obuild: build for a selection of 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 Rocq 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 " - theories-foo: for each directory theories/Corelib/Foo, build the vo files for it and set them up in _build/install/default."
@echo " For instance the init target builds the prelude, combined with rocq-runtime.install it produces a fully functional layout in _build/install/default."
help-install:
@echo ""
@echo "The Dune-based Rocq build is split into several packages; see Dune and dev/doc"
@echo "documentation for more details. A quick install of Rocq alone can be done with"
@echo ""
@echo " $$ make dunestrap"
@echo " $$ dune build -p rocq-runtime,coq-core,rocq-core"
@echo " $$ dune install --prefix=<install_prefix> rocq-runtime coq-core rocq-core"
@echo ""
@echo " Provided opam/dune packages are:"
@echo ""
@echo " - rocq-runtime: base Rocq package, toplevel compilers, plugins, tools, no corelib, no stdlib, no GTK"
@echo " - coq-core: compat binaries (coqc instead of rocq compile, etc)"
@echo " - rocq-core: Rocq's prelude and corelib"
@echo " - coqide-server: XML protocol language server"
@echo " - rocqide: RocqIDE gtk application"
@echo " - rocq: meta package depending on rocq-runtime rocq-core rocq-stdlib"
@echo " (also calls the test suite when using --with-test)"
@echo " - coq: meta package depending on rocq coq-core coq-stdlib"
@echo " (also calls the test suite when using --with-test)"
@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 --prefix=<install_prefix> package'"
@echo ""
@echo " Note that '--prefix' must be passed to dune install. The '-prefix' passed to"
@echo " configure tells Rocq where to look for libraries."
@echo ""
@echo " Note that building a package in release mode ignores other packages present in"
@echo " the worktree. See Dune documentation for more information."
# We setup the root even in dev mode, to avoid some problems. We used
# this in the past to workaround a bug in opam, but the bug was that
# we didn't pass `-p` to the dune build below.
#
# This would be fixed once dune can directly use `(include
# theories_dune)` in our files.
DUNESTRAPOPT=--root .
# We regenerate always as to correctly track deps, can do better
# We do a single call to dune as to avoid races and locking
ifneq ($(COQ_SPLIT),) # avoid depending on local rocq-runtime
_build/default/corelib_dune_split _build/default/ltac2_dune_split .dune-stamp: FORCE
dune build $(DUNEOPT) $(DUNESTRAPOPT) corelib_dune_split ltac2_dune_split
touch .dune-stamp
theories/Corelib/dune: .dune-stamp
cp -a _build/default/corelib_dune_split $@ && chmod +w $@
theories/Ltac2/dune: .dune-stamp
cp -a _build/default/ltac2_dune_split $@ && chmod +w $@
else
_build/default/corelib_dune _build/default/ltac2_dune .dune-stamp: FORCE
dune build $(DUNEOPT) $(DUNESTRAPOPT) corelib_dune ltac2_dune
touch .dune-stamp
theories/Corelib/dune: .dune-stamp
cp -a _build/default/corelib_dune $@ && chmod +w $@
theories/Ltac2/dune: .dune-stamp
cp -a _build/default/ltac2_dune $@ && chmod +w $@
endif
FORCE: ;
DUNE_FILES=theories/Corelib/dune theories/Ltac2/dune
dunestrap: $(DUNE_FILES)
states: dunestrap
dune build $(DUNEOPT) dev/shim/coqtop
MAIN_TARGETS:=rocq-runtime.install coq-core.install rocq-core.install \
coqide-server.install rocq-devtools.install
world: dunestrap
dune build $(DUNEOPT) $(MAIN_TARGETS)
rocqide:
dune build $(DUNEOPT) rocqide.install
watch:
dune build $(DUNEOPT) $(MAIN_TARGETS) -w
check:
dune build $(DUNEOPT) @check
test-suite: dunestrap
dune runtest --no-buffer $(DUNEOPT)
refman-html: dunestrap
dune build --no-buffer @refman-html
refman-pdf: dunestrap
dune build --no-buffer @refman-pdf
corelib-html: dunestrap
dune build @corelib-html
apidoc:
dune build $(DUNEOPT) @doc
# We define this target as to override Make's built-in one
install:
@echo "To install Rocq 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) @check --workspace=dev/dune-workspace.all
obuild: dunestrap
dune build $(DUNEOPT) @default --workspace=dev/dune-workspace.all
ireport:
dune clean
dune build $(DUNEOPT) @install --profile=ireport
clean:
rm -f .dune-stamp theories/Corelib/dune theories/Ltac2/dune
dune clean
# docgram
DOC_GRAM:=_build/default/doc/tools/docgram/doc_grammar.exe
# not worth figuring out dependencies, just leave it to dune
.PHONY: $(DOC_GRAM)
$(DOC_GRAM):
dune build $(DUNEOPT) $@
include doc/Makefile.docgram
# This requires a install layout to be available.
CONTEXT=_build/install/default
# XXX: Port this to a dune alias so the build is hygienic!
.PHONY: plugin-tutorial
plugin-tutorial: world
$(MAKE) OCAMLPATH=$(shell pwd)/$(CONTEXT)/lib/ COQBIN="$(shell pwd)/$(CONTEXT)/bin/" -C doc/plugin_tutorial
# This is broken in a very weird way with a permission error... see
# the rule in doc/plugin_tutorial/dune:
# plugin-tutorial: dunestrap
# dune build @plugin-tutorial
# 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 Rocq Dune
# build with Rocq developments that are not dunerized and thus still
# expect an install layout with a working Rocq 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/Corelib/Arith/Arith.vo` to
# have the rule install the target, we thus imitate such behavior
# using make as a helper.
# $(1) is the directory (theories/Corelib/Foo/)
# $(2) is the name (foo)
define subtarget =
.PHONY: theories-$(2)
$(2)_FILES=$$(wildcard $(1)*.v)
$(2)_FILES_PATH=$$(addprefix _build/install/default/lib/coq/, $$($(2)_FILES:.v=.vo))
theories-$(2):
@echo "DUNE $(1)*.vo"
@dune build $$($(2)_FILES_PATH)
endef
$(foreach subdir,$(wildcard theories/Corelib/*/),$(eval $(call subtarget,$(subdir),$(shell echo $(subst /,,$(subst theories/Corelib/,,$(subdir))) | tr A-Z a-z))))
# Other common dev targets:
#
# dune build rocq-runtime.install
# dune build coq.install
# dune build rocqide.install
#
# Packaging / OPAM targets:
#
# dune -p coq @install
# dune -p rocqide @install
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
*© Formatika GbR, Deutschland
|
|
