Skip to content
Snippets Groups Projects
Commit 1fd66ab8 authored by Ralf Jung's avatar Ralf Jung
Browse files

modernize the build system to how it is in master

parent 209ec3aa
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Makefile
+ 28
− 68
View file @ 1fd66ab8
############################################################################# # This Makefile started being auto-generated, but now it's hand-crafted and automatically finds all the files.
## v # The Coq Proof Assistant ## # YOU SHOULD NOT HAVE TO EDIT THIS FILE.
## <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
#
.DEFAULT_GOAL := all .DEFAULT_GOAL := all
...@@ -39,8 +23,8 @@ $(call includecmdwithout@,$(COQBIN)coqtop -config) ...@@ -39,8 +23,8 @@ $(call includecmdwithout@,$(COQBIN)coqtop -config)
# # # #
########################## ##########################
COQLIBS?=-I . -R lib/ModuRes ModuRes COQLIBS?=-I . -R . _
COQDOCLIBS?=-R lib/ModuRes ModuRes COQDOCLIBS?=-I lib
########################## ##########################
# # # #
...@@ -50,14 +34,14 @@ COQDOCLIBS?=-R lib/ModuRes ModuRes ...@@ -50,14 +34,14 @@ COQDOCLIBS?=-R lib/ModuRes ModuRes
OPT?= OPT?=
COQDEP?=$(COQBIN)coqdep -c COQDEP?="$(COQBIN)coqdep" -c
COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
COQCHKFLAGS?=-silent -o COQCHKFLAGS?=-silent -o
COQDOCFLAGS?=-interpolate -utf8 COQDOCFLAGS?=-interpolate -utf8
COQC?=$(COQBIN)coqc COQC?="$(COQBIN)coqc"
GALLINA?=$(COQBIN)gallina GALLINA?="$(COQBIN)gallina"
COQDOC?=$(COQBIN)coqdoc COQDOC?="$(COQBIN)coqdoc"
COQCHK?=$(COQBIN)coqchk COQCHK?="$(COQBIN)coqchk"
################## ##################
# # # #
...@@ -66,12 +50,12 @@ COQCHK?=$(COQBIN)coqchk ...@@ -66,12 +50,12 @@ COQCHK?=$(COQBIN)coqchk
################## ##################
ifdef USERINSTALL ifdef USERINSTALL
XDG_DATA_HOME?=$(HOME)/.local/share XDG_DATA_HOME?="$(HOME)/.local/share"
COQLIBINSTALL=$(XDG_DATA_HOME)/coq COQLIBINSTALL=$(XDG_DATA_HOME)/coq
COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
else else
COQLIBINSTALL=${COQLIB}user-contrib COQLIBINSTALL="${COQLIB}user-contrib"
COQDOCINSTALL=${DOCDIR}user-contrib COQDOCINSTALL="${DOCDIR}user-contrib"
endif endif
###################### ######################
...@@ -80,16 +64,14 @@ endif ...@@ -80,16 +64,14 @@ endif
# # # #
###################### ######################
VFILES:=core_lang.v\ LIBVFILES:=$(wildcard lib/*/*.v)
iris.v\ VFILES:=$(wildcard *.v) $(LIBVFILES)
lang.v\
masks.v\
world_prop.v
-include $(addsuffix .d,$(VFILES)) -include $(addsuffix .d,$(VFILES))
.SECONDARY: $(addsuffix .d,$(VFILES)) .SECONDARY: $(addsuffix .d,$(VFILES))
VOFILES:=$(VFILES:.v=.vo) VOFILES:=$(VFILES:.v=.vo)
LIBVOFILES:=$(LIBVFILES:.v=.vo)
VOFILESINC=$(filter $(wildcard ./*),$(VOFILES)) VOFILESINC=$(filter $(wildcard ./*),$(VOFILES))
GLOBFILES:=$(VFILES:.v=.glob) GLOBFILES:=$(VFILES:.v=.glob)
VIFILES:=$(VFILES:.v=.vi) VIFILES:=$(VFILES:.v=.vi)
...@@ -108,7 +90,9 @@ endif ...@@ -108,7 +90,9 @@ endif
# # # #
####################################### #######################################
all: ./lib/ModuRes $(VOFILES) all: $(VOFILES)
lib: $(LIBVOFILES)
spec: $(VIFILES) spec: $(VIFILES)
...@@ -142,16 +126,7 @@ beautify: $(VFILES:=.beautified) ...@@ -142,16 +126,7 @@ beautify: $(VFILES:=.beautified)
@echo 'Do not do "make clean" until you are sure that everything went well!' @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/' @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 .PHONY: all lib opt byte archclean clean install userinstall depend html validate
###################
# #
# Subdirectories. #
# #
###################
./lib/ModuRes:
cd ./lib/ModuRes ; $(MAKE) all
#################### ####################
# # # #
...@@ -168,37 +143,22 @@ opt: ...@@ -168,37 +143,22 @@ opt:
userinstall: userinstall:
+$(MAKE) USERINSTALL=true install +$(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: clean:
rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old) 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 -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 - rm -rf html mlihtml
(cd ./lib/ModuRes ; $(MAKE) clean)
archclean: archclean:
rm -f *.cmx *.o rm -f *.cmx *.o
(cd ./lib/ModuRes ; $(MAKE) archclean)
printenv: printenv:
@$(COQBIN)coqtop -config @"$(COQBIN)coqtop" -config
@echo CAMLC = $(CAMLC) @echo 'CAMLC = $(CAMLC)'
@echo CAMLOPTC = $(CAMLOPTC) @echo 'CAMLOPTC = $(CAMLOPTC)'
@echo PP = $(PP) @echo 'PP = $(PP)'
@echo COQFLAGS = $(COQFLAGS) @echo 'COQFLAGS = $(COQFLAGS)'
@echo COQLIBINSTALL = $(COQLIBINSTALL) @echo 'COQLIBINSTALL = $(COQLIBINSTALL)'
@echo COQDOCINSTALL = $(COQDOCINSTALL) @echo 'COQDOCINSTALL = $(COQDOCINSTALL)'
################### ###################
# # # #
...@@ -225,9 +185,9 @@ printenv: ...@@ -225,9 +185,9 @@ printenv:
$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ $(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
%.g.html: %.v %.glob %.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} ) $(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
%.v.beautified: %.v.beautified:
......
lib/ModuRes/Makefile deleted 100644 → 0
+ 0
− 237
View file @ 209ec3aa
#############################################################################
## 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
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment