make the Makefile compile the library correctly, and automatically find all the files

Makefile

@@ -24,7 +24,7 @@ $(call includecmdwithout@,$(COQBIN)coqtop -config)
 ##########################
 
 COQLIBS?=-I . -R lib/ModuRes ModuRes
-COQDOCLIBS?=-R lib/ModuRes ModuRes
+COQDOCLIBS?=-I lib
 
 ##########################
 #                        #
@@ -64,7 +64,7 @@ endif
 #                    #
 ######################
 
-VFILES:=$(wildcard *.v)
+VFILES:=$(wildcard *.v) $(wildcard lib/ModuRes/*.v)
 
 -include $(addsuffix .d,$(VFILES))
 .SECONDARY: $(addsuffix .d,$(VFILES))
@@ -88,7 +88,7 @@ endif
 #                                     #
 #######################################
 
-all: $(VOFILES) ./lib/ModuRes
+all: $(VOFILES)
 
 spec: $(VIFILES)
 
@@ -122,16 +122,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 opt byte archclean clean install userinstall depend html validate
 
 ####################
 #                  #
@@ -148,28 +139,13 @@ 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

README.txt

@@ -83,7 +83,7 @@ HOW TO COMPILE
 
   To compile the development, run
   
-  > (cd lib/ModuRes; make) && make 
+  > make -j
 
   in the folder containing this README. 
   

configure

-#!/bin/sh
-coq_makefile lib/ModuRes -R lib/ModuRes ModuRes *.v -o Makefile

lib/ModuRes/Makefile

-#############################################################################
-##  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\
-  RA.v\
-  Predom.v\
-  PreoMet.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
-