Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298############################################################################ # 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 refman-indices 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
# unset to disable jobserver integration (-j argument of make will be ignored)WITHJOBS:=dev/tools/with-jobs.sh
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 rocq:" @echo "" @echo " - use 'dune exec -- rocq \$$subcommand args'" @echo " Example: 'dune exec -- rocq compile 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 " - refman-indices: build Rocq's JSON indices" @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 " - rocqide-server: XML protocol language server" @echo " - rocqide: RocqIDE 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 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 lockingifneq ($(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: world echo "'make states' is an alias for 'make world'"
MAIN_TARGETS:=rocq-runtime.install coq-core.install rocq-core.install \ rocqide-server.install rocq-devtools.install
world: dunestrap +$(WITHJOBS) 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)
.PHONY: doc/unreleased.rstdoc/unreleased.rst: cat doc/changelog/00-title.rst doc/changelog/*/*.rst > $@
WITHPYPATH:=PYTHONPATH=_build/default/config:doc/tools:$$PYTHONPATH
refman-html: world doc/unreleased.rst rm -rf doc/refman-html +$(WITHPYPATH) $(WITHJOBS) dune exec -- sphinx-build -q -W -b html doc/sphinx doc/refman-htmlrefman-pdf: world doc/unreleased.rst rm -rf doc/refman-pdf +$(WITHPYPATH) $(WITHJOBS) dune exec -- sphinx-build -q -W -b latex doc/sphinx doc/refman-pdf $(MAKE) -C doc/refman-pdf LATEXMKOPTS=-silent
refman-indices: world doc/unreleased.rst rm -rf doc/refman-indices +$(WITHPYPATH) $(WITHJOBS) dune exec -- sphinx-build -q -W -b indices doc/sphinx doc/refman-indices
corelib-html: dunestrap dune build @corelib-html
apidoc: dune build $(DUNEOPT) @doc
# We define this target as to override Make's built-in oneinstall: @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-tutorialplugin-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:=1export CI_PURE_DUNEinclude 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