Revision ebcd89f9c3f3d009e7b6fd5d65f31043d2abfff1 authored by Matthieu Sozeau on 19 January 2021, 14:59:22 UTC, committed by GitHub on 19 January 2021, 14:59:22 UTC
Preparing for `coq-metacoq.1.0~beta2+8.12`
Makefile
TIMED ?=
all: template-coq pcuic safechecker erasure examples
.PHONY: all template-coq pcuic erasure install html clean mrproper .merlin test-suite translations
install: all
$(MAKE) -C template-coq install
$(MAKE) -C pcuic install
$(MAKE) -C safechecker install
$(MAKE) -C erasure install
$(MAKE) -C translations install
uninstall: all
$(MAKE) -C template-coq uninstall
$(MAKE) -C pcuic uninstall
$(MAKE) -C safechecker uninstall
$(MAKE) -C erasure uninstall
$(MAKE) -C translations uninstall
html: all
"coqdoc" -toc -utf8 -interpolate -l -html \
-R template-coq/theories MetaCoq.Template \
-R pcuic/theories MetaCoq.PCUIC \
-R safechecker/theories MetaCoq.SafeChecker \
-R erasure/theories MetaCoq.Erasure \
-R translations MetaCoq.Translations \
-d html */theories/*.v translations/*.v
clean:
$(MAKE) -C template-coq clean
$(MAKE) -C pcuic clean
$(MAKE) -C safechecker clean
$(MAKE) -C erasure clean
$(MAKE) -C examples clean
$(MAKE) -C test-suite clean
$(MAKE) -C translations clean
mrproper:
$(MAKE) -C template-coq mrproper
$(MAKE) -C pcuic mrproper
$(MAKE) -C safechecker mrproper
$(MAKE) -C erasure mrproper
$(MAKE) -C examples mrproper
$(MAKE) -C test-suite mrproper
$(MAKE) -C translations mrproper
.merlin:
$(MAKE) -C template-coq .merlin
$(MAKE) -C pcuic .merlin
$(MAKE) -C safechecker .merlin
$(MAKE) -C erasure .merlin
template-coq:
$(MAKE) -C template-coq
pcuic: template-coq
$(MAKE) -C pcuic
safechecker: template-coq pcuic
$(MAKE) -C safechecker
erasure: template-coq safechecker pcuic
$(MAKE) -C erasure
examples: checker safechecker erasure
$(MAKE) -C examples
test-suite: template-coq safechecker erasure
$(MAKE) -C test-suite
translations: template-coq
$(MAKE) -C translations
cleanplugins:
$(MAKE) -C template-coq cleanplugin
$(MAKE) -C safechecker cleanplugin
$(MAKE) -C erasure cleanplugin
ci-local:
./configure.sh local
$(MAKE) all test-suite
ci-opam:
# Use -v so that regular output is produced
opam install -v -y .
opam remove -y coq-metacoq coq-metacoq-template
Computing file changes ...