equations/Makefile at main · rocq-prover/equations · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
# One of these two files will have been generated

.PHONY: all

all:
	dune build -p rocq-equations,rocq-equations-examples @install

install:
	dune install rocq-equations rocq-equations-examples

.PHONY: install

test-suite:
	dune build -p rocq-equations-tests

.PHONY: test-suite

clean:
	dune clean

siteexamples: _build/default/examples/*.glob
	sh siteexamples.sh

doc: html
	mkdir -p html/api && ocamldoc -html -d html/api \
		`ocamlfind query -r rocq-runtime.lib rocq-runtime.kernel rocq-runtime.tactics rocq-runtime.proofs \
			rocq-runtime.toplevel rocq-runtime.ltac rocq-runtime.plugins.extraction -i-format` \
	  -I src src/*.ml

toplevel: src/equations_plugin.cma bytefiles
	"$(OCAMLFIND)" ocamlc -linkpkg -linkall -g $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
		-package rocq-runtime.toplevel,rocq-runtime.plugins.extraction \
	  $< $(COQLIB)/toplevel/coqtop_bin.ml -o coqtop_equations

ci-dune:
	dune build -p rocq-equations,rocq-equations-examples,rocq-equations-tests
	dune build -p rocq-equations,rocq-equations-examples @install
	dune install rocq-equations rocq-equations-examples

ci-hott:
	opam install -j 2 -y coq-hott.dev
	dune build -p rocq-equations,rocq-equations-hott
	dune build -p rocq-equations,rocq-equations-hott @install
	dune install rocq-equations rocq-equations-hott

.PHONY: ci-dune ci-hott