From 1fd66ab8eb932bf9301b7d84dfe5e1dcb55b9594 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Jun 2015 19:28:10 +0200
Subject: [PATCH] modernize the build system to how it is in master
---
Makefile | 96 +++++-------------
lib/ModuRes/Makefile | 237 -------------------------------------------
2 files changed, 28 insertions(+), 305 deletions(-)
delete mode 100644 lib/ModuRes/Makefile
diff --git a/Makefile b/Makefile
index 1b8c801d5..4e9173dbe 100644
--- a/Makefile
+++ b/Makefile
@@ -1,21 +1,5 @@
-#############################################################################
-## v # The Coq Proof Assistant ##
-## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
-## \VV/ # ##
-## // # Makefile automagically generated by coq_makefile V8.4pl4 ##
-#############################################################################
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-
-#
-# This Makefile was generated by the command line :
-# coq_makefile lib/ModuRes -R lib/ModuRes ModuRes core_lang.v iris.v lang.v masks.v world_prop.v -o Makefile
-#
+# This Makefile started being auto-generated, but now it's hand-crafted and automatically finds all the files.
+# YOU SHOULD NOT HAVE TO EDIT THIS FILE.
.DEFAULT_GOAL := all
@@ -39,8 +23,8 @@ $(call includecmdwithout@,$(COQBIN)coqtop -config)
# #
##########################
-COQLIBS?=-I . -R lib/ModuRes ModuRes
-COQDOCLIBS?=-R lib/ModuRes ModuRes
+COQLIBS?=-I . -R . _
+COQDOCLIBS?=-I lib
##########################
# #
@@ -50,14 +34,14 @@ COQDOCLIBS?=-R lib/ModuRes ModuRes
OPT?=
-COQDEP?=$(COQBIN)coqdep -c
+COQDEP?="$(COQBIN)coqdep" -c
COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
COQCHKFLAGS?=-silent -o
COQDOCFLAGS?=-interpolate -utf8
-COQC?=$(COQBIN)coqc
-GALLINA?=$(COQBIN)gallina
-COQDOC?=$(COQBIN)coqdoc
-COQCHK?=$(COQBIN)coqchk
+COQC?="$(COQBIN)coqc"
+GALLINA?="$(COQBIN)gallina"
+COQDOC?="$(COQBIN)coqdoc"
+COQCHK?="$(COQBIN)coqchk"
##################
# #
@@ -66,12 +50,12 @@ COQCHK?=$(COQBIN)coqchk
##################
ifdef USERINSTALL
-XDG_DATA_HOME?=$(HOME)/.local/share
+XDG_DATA_HOME?="$(HOME)/.local/share"
COQLIBINSTALL=$(XDG_DATA_HOME)/coq
COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
else
-COQLIBINSTALL=${COQLIB}user-contrib
-COQDOCINSTALL=${DOCDIR}user-contrib
+COQLIBINSTALL="${COQLIB}user-contrib"
+COQDOCINSTALL="${DOCDIR}user-contrib"
endif
######################
@@ -80,16 +64,14 @@ endif
# #
######################
-VFILES:=core_lang.v\
- iris.v\
- lang.v\
- masks.v\
- world_prop.v
+LIBVFILES:=$(wildcard lib/*/*.v)
+VFILES:=$(wildcard *.v) $(LIBVFILES)
-include $(addsuffix .d,$(VFILES))
.SECONDARY: $(addsuffix .d,$(VFILES))
VOFILES:=$(VFILES:.v=.vo)
+LIBVOFILES:=$(LIBVFILES:.v=.vo)
VOFILESINC=$(filter $(wildcard ./*),$(VOFILES))
GLOBFILES:=$(VFILES:.v=.glob)
VIFILES:=$(VFILES:.v=.vi)
@@ -108,7 +90,9 @@ endif
# #
#######################################
-all: ./lib/ModuRes $(VOFILES)
+all: $(VOFILES)
+
+lib: $(LIBVOFILES)
spec: $(VIFILES)
@@ -142,16 +126,7 @@ beautify: $(VFILES:=.beautified)
@echo 'Do not do "make clean" until you are sure that everything went well!'
@echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
-.PHONY: all opt byte archclean clean install userinstall depend html validate ./lib/ModuRes
-
-###################
-# #
-# Subdirectories. #
-# #
-###################
-
-./lib/ModuRes:
- cd ./lib/ModuRes ; $(MAKE) all
+.PHONY: all lib opt byte archclean clean install userinstall depend html validate
####################
# #
@@ -168,37 +143,22 @@ opt:
userinstall:
+$(MAKE) USERINSTALL=true install
-install:
- install -d $(DSTROOT)$(COQLIBINSTALL)/ModuRes; \
- for i in $(VOFILESINC); do \
- install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/ModuRes/`basename $$i`; \
- done
- (cd ./lib/ModuRes; $(MAKE) DSTROOT=$(DSTROOT) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/./lib/ModuRes install)
-
-install-doc:
- install -d $(DSTROOT)$(COQDOCINSTALL)/ModuRes/html
- for i in html/*; do \
- install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/ModuRes/$$i;\
- done
-
clean:
rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex
- rm -rf html mlihtml
- (cd ./lib/ModuRes ; $(MAKE) clean)
archclean:
rm -f *.cmx *.o
- (cd ./lib/ModuRes ; $(MAKE) archclean)
printenv:
- @$(COQBIN)coqtop -config
- @echo CAMLC = $(CAMLC)
- @echo CAMLOPTC = $(CAMLOPTC)
- @echo PP = $(PP)
- @echo COQFLAGS = $(COQFLAGS)
- @echo COQLIBINSTALL = $(COQLIBINSTALL)
- @echo COQDOCINSTALL = $(COQDOCINSTALL)
+ @"$(COQBIN)coqtop" -config
+ @echo 'CAMLC = $(CAMLC)'
+ @echo 'CAMLOPTC = $(CAMLOPTC)'
+ @echo 'PP = $(PP)'
+ @echo 'COQFLAGS = $(COQFLAGS)'
+ @echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
+ @echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
###################
# #
@@ -225,9 +185,9 @@ printenv:
$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
%.g.html: %.v %.glob
- $(COQDOC)$(COQDOCFLAGS) -html -g $< -o $@
+ $(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@
-%.v.d: %.v
+%.v.d: %.v Makefile
$(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
%.v.beautified:
diff --git a/lib/ModuRes/Makefile b/lib/ModuRes/Makefile
deleted file mode 100644
index 0affb7285..000000000
--- a/lib/ModuRes/Makefile
+++ /dev/null
@@ -1,237 +0,0 @@
-#############################################################################
-## v # The Coq Proof Assistant ##
-## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
-## \VV/ # ##
-## // # Makefile automagically generated by coq_makefile V8.4pl4 ##
-#############################################################################
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-
-#
-# This Makefile was generated by the command line :
-# coq_makefile -R . ModuRes BI.v CBUltInst.v CSetoid.v Constr.v Finmap.v MetricCore.v MetricRec.v PCBUltInst.v PCM.v Predom.v PreoMet.v TOTInst.v UPred.v -o Makefile
-#
-
-.DEFAULT_GOAL := all
-
-#
-# This Makefile may take arguments passed as environment variables:
-# COQBIN to specify the directory where Coq binaries resides;
-# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;
-# DSTROOT to specify a prefix to install path.
-
-# Here is a hack to make $(eval $(shell works:
-define donewline
-
-
-endef
-includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; })))
-$(call includecmdwithout@,$(COQBIN)coqtop -config)
-
-##########################
-# #
-# Libraries definitions. #
-# #
-##########################
-
-COQLIBS?= -R . ModuRes
-COQDOCLIBS?=-R . ModuRes
-
-##########################
-# #
-# Variables definitions. #
-# #
-##########################
-
-
-OPT?=
-COQDEP?=$(COQBIN)coqdep -c
-COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
-COQCHKFLAGS?=-silent -o
-COQDOCFLAGS?=-interpolate -utf8
-COQC?=$(COQBIN)coqc
-GALLINA?=$(COQBIN)gallina
-COQDOC?=$(COQBIN)coqdoc
-COQCHK?=$(COQBIN)coqchk
-
-##################
-# #
-# Install Paths. #
-# #
-##################
-
-ifdef USERINSTALL
-XDG_DATA_HOME?=$(HOME)/.local/share
-COQLIBINSTALL=$(XDG_DATA_HOME)/coq
-COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
-else
-COQLIBINSTALL=${COQLIB}user-contrib
-COQDOCINSTALL=${DOCDIR}user-contrib
-endif
-
-######################
-# #
-# Files dispatching. #
-# #
-######################
-
-VFILES:=BI.v\
- CBUltInst.v\
- CSetoid.v\
- Constr.v\
- Finmap.v\
- MetricCore.v\
- MetricRec.v\
- PCBUltInst.v\
- PCM.v\
- Predom.v\
- PreoMet.v\
- TOTInst.v\
- UPred.v
-
--include $(addsuffix .d,$(VFILES))
-.SECONDARY: $(addsuffix .d,$(VFILES))
-
-VOFILES:=$(VFILES:.v=.vo)
-GLOBFILES:=$(VFILES:.v=.glob)
-VIFILES:=$(VFILES:.v=.vi)
-GFILES:=$(VFILES:.v=.g)
-HTMLFILES:=$(VFILES:.v=.html)
-GHTMLFILES:=$(VFILES:.v=.g.html)
-ifeq '$(HASNATDYNLINK)' 'true'
-HASNATDYNLINK_OR_EMPTY := yes
-else
-HASNATDYNLINK_OR_EMPTY :=
-endif
-
-#######################################
-# #
-# Definition of the toplevel targets. #
-# #
-#######################################
-
-all: $(VOFILES)
-
-spec: $(VIFILES)
-
-gallina: $(GFILES)
-
-html: $(GLOBFILES) $(VFILES)
- - mkdir -p html
- $(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)
-
-gallinahtml: $(GLOBFILES) $(VFILES)
- - mkdir -p html
- $(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)
-
-all.ps: $(VFILES)
- $(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all-gal.ps: $(VFILES)
- $(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all.pdf: $(VFILES)
- $(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all-gal.pdf: $(VFILES)
- $(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-validate: $(VOFILES)
- $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))
-
-beautify: $(VFILES:=.beautified)
- for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
- @echo 'Do not do "make clean" until you are sure that everything went well!'
- @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
-
-.PHONY: all opt byte archclean clean install userinstall depend html validate
-
-####################
-# #
-# Special targets. #
-# #
-####################
-
-byte:
- $(MAKE) all "OPT:=-byte"
-
-opt:
- $(MAKE) all "OPT:=-opt"
-
-userinstall:
- +$(MAKE) USERINSTALL=true install
-
-install:
- for i in $(VOFILES); do \
- install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/ModuRes/$$i`; \
- install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/ModuRes/$$i; \
- done
-
-install-doc:
- install -d $(DSTROOT)$(COQDOCINSTALL)/ModuRes/html
- for i in html/*; do \
- install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/ModuRes/$$i;\
- done
-
-clean:
- rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
- rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex
- - rm -rf html mlihtml
-
-archclean:
- rm -f *.cmx *.o
-
-printenv:
- @$(COQBIN)coqtop -config
- @echo CAMLC = $(CAMLC)
- @echo CAMLOPTC = $(CAMLOPTC)
- @echo PP = $(PP)
- @echo COQFLAGS = $(COQFLAGS)
- @echo COQLIBINSTALL = $(COQLIBINSTALL)
- @echo COQDOCINSTALL = $(COQDOCINSTALL)
-
-###################
-# #
-# Implicit rules. #
-# #
-###################
-
-%.vo %.glob: %.v
- $(COQC) $(COQDEBUG) $(COQFLAGS) $*
-
-%.vi: %.v
- $(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
-
-%.g: %.v
- $(GALLINA) $<
-
-%.tex: %.v
- $(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
-
-%.html: %.v %.glob
- $(COQDOC) $(COQDOCFLAGS) -html $< -o $@
-
-%.g.tex: %.v
- $(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
-
-%.g.html: %.v %.glob
- $(COQDOC)$(COQDOCFLAGS) -html -g $< -o $@
-
-%.v.d: %.v
- $(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
-
-%.v.beautified:
- $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-
--
GitLab