Makefile.in

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
#            This file is part of the DpdGraph tools.
#  Copyright (C) 2009-2015 Anne Pacalet (Anne.Pacalet@free.fr)
#                      and Yves Bertot (Yves.Bertot@inria.fr)
#                ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
#      This file is distributed under the terms of the
#       GNU Lesser General Public License Version 2.1
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

.SUFFIXES:

ECHO=@echo
ECHO_CIBLE = $(ECHO) "   * build $@"

PRE=dpd

NAME=coq-dpdgraph
VERSION=$(shell cat VERSION)

BINDIR=@BINDIR@

DPDPLUGIN=./dpdgraph.cmxs ./dpdgraph.vo
DPD2DOT=./dpd2dot
DPDUSAGE=./dpdusage

INCLUDES = -I @OCAMLGRAPH_PATH@

all : $(DPDPLUGIN) $(DPD2DOT) $(DPDUSAGE)

DISTRIBUTED = $(PRE)_compute.ml $(PRE)_dot.ml \
	 $(PRE)_parse.mly  $(PRE)_lex.mll $(PRE)2dot.ml $(PRE)usage.ml

ML_COMMON = version.ml $(PRE)_compute.ml $(PRE)_dot.ml \
	 $(PRE)_parse.ml  $(PRE)_lex.ml
ML_DPD2DOT = $(PRE)2dot.ml
ML_DPDUSAGE = $(PRE)usage.ml

ML_ALL = $(ML_COMMON) $(ML_DPD2DOT) $(ML_DPDUSAGE)

CMOS_DPD2DOT=$(ML_COMMON:%.ml=%.cmo) $(ML_DPD2DOT:%.ml=%.cmo)
CMOS_DPDUSAGE=$(ML_COMMON:%.ml=%.cmo) $(ML_DPDUSAGE:%.ml=%.cmo)
CMXS=$(ML_ALL:%.ml=%.cmx)

OCAMLC=@OCAMLC@
OCAMLOPT=@OCAMLOPT@
OCAMLDEP=@OCAMLDEP@
OCAMLLEX=@OCAMLLEX@
OCAMLYACC=@OCAMLYACC@

OCAMLFLAGS =  -w +a -warn-error +a -safe-string -g -dtypes $(INCLUDES) -c
OCAMLOPTFLAGS = -c

COQ_MAKEFILE=@COQ_MAKEFILE@
# COQDEP=$(OCAMLDEP)

COQEXTFILES=searchdepend.ml4 graphdepend.ml4

GENERATED+=$(COQEXTFILES:%.ml4=%.o) $(COQEXTFILES:%.ml4=%.cmx) dpdgraph.cmxs

DISTRIBUTED+=$(COQEXTFILES) dpdgraph.mllib
DISTRIBUTED+=Make

install : Make_coq
	$(MAKE) -f $< install
	cp dpd2dot dpdusage $(BINDIR)/

$(DPDPLUGIN) : Make_coq $(DISTRIBUTED)
	$(ECHO_CIBLE)
	$(MAKE) -f $< $@

Make_coq : Make
	$(ECHO_CIBLE)
	$(COQ_MAKEFILE) -f $< > $@

GENERATED+= Make_coq

version.ml : VERSION
	$(ECHO_CIBLE)
	$(ECHO) "(* This file is generated by Makefile. Do not modify. *)" > $@
	$(ECHO) "let version = \""$(VERSION)"\"" >> $@

GENERATED+=version.ml

$(DPD2DOT) : $(CMOS_DPD2DOT)
	$(ECHO_CIBLE)
	$(OCAMLC) -g $(INCLUDES) -o $@ graph.cma $(CMOS_DPD2DOT)

$(DPDUSAGE) : $(CMOS_DPDUSAGE)
	$(ECHO_CIBLE)
	$(OCAMLC) -g $(INCLUDES) -o $@ graph.cma $(CMOS_DPDUSAGE)

%.cmo : %.ml
	$(ECHO_CIBLE)
	$(OCAMLC) $(OCAMLFLAGS) $<

%.cmx : %.ml
	$(ECHO_CIBLE)
	$(OCAMLOPT) $(OPTPACKFLAGS) $(OCAMLOPTFLAGS) $<

%.cmi : %.mli
	$(ECHO_CIBLE)
	$(OCAMLC) $(OCAMLFLAGS) $<

%.ml : %.mll
	$(ECHO_CIBLE)
	$(OCAMLLEX) $<

GENERATED+=$(PRE)_lex.ml

%.ml : %.mly
	$(ECHO_CIBLE)
	$(OCAMLYACC) $<

GENERATED+=$(PRE)_parse.ml $(PRE)_parse.mli

depend: .depend

.depend : $(ML_ALL)
	$(ECHO_CIBLE)
	$(OCAMLDEP) $(ML_ALL) *.mli > $@

include .depend

GENERATED+=.depend

#-------------------------------------------------------------------------------

TESTDIR=tests
TESTS_SRC=$(TESTDIR)/Morph.v $(TESTDIR)/Test.v $(TESTDIR)/Polymorph.v \
	  $(TESTDIR)/Morph.cmd $(TESTDIR)/Test.cmd $(TESTDIR)/search.cmd \
          $(TESTDIR)/Polymorph.cmd
TESTS_DPD=$(TESTDIR)/graph.dpd $(TESTDIR)/graph2.dpd \
	  $(TESTDIR)/Morph.dpd $(TESTDIR)/Morph_rw.dpd $(TESTDIR)/Polymorph.dpd
TESTS_DOT=$(TESTS_DPD:%.dpd=%.dot)
TESTS=$(TESTS_DPD) $(TESTS_DOT) $(TESTDIR)/graph.without.dot \
      $(TESTDIR)/search  $(TESTDIR)/graph2.dpdusage
TESTS_LOG=$(TESTS:%=%.log)
TESTS_ORACLE=$(TESTS:%=%.oracle)
TESTS_OK=$(TESTS:%=%.ok)

DISTRIBUTED+=$(TESTS_SRC) $(TESTS_ORACLE)

.PRECIOUS : $(TESTS) $(TESTS_LOG) $(TESTS_ORACLE)

.PHONY: tests test
tests test : $(TESTS_OK)

$(TESTDIR)/%.dpdusage.log: $(TESTDIR)/%.dpd $(DPDUSAGE)
	$(DPDUSAGE) $< > $@

%.log : %
	cp $< $@

%.vo : %.v
	coqc -R . dpdgraph $<

%.html : %.v
	coqdoc $<

%.svg : %.dot
	dot -Tsvg -o$@ $<

$(TESTDIR)/Morph%.dpd : $(TESTDIR)/Morph.vo $(TESTDIR)/Morph.cmd $(DPDPLUGIN)
	# cd to tests to generate .dpd file there.
	cd $(TESTDIR); coqtop -R .. dpdgraph -I .. < Morph.cmd > /dev/null 2>&1

$(TESTDIR)/Polymorph%.dpd : $(TESTDIR)/Polymorph.vo $(TESTDIR)/Polymorph.cmd \
                            $(DPDPLUGIN)
	cd $(TESTDIR); coqtop -R .. dpdgraph -I .. < Polymorph.cmd

$(TESTDIR)/graph.dpd $(TESTDIR)/graph2.dpd: \
	             $(TESTDIR)/Test.vo $(TESTDIR)/Test.cmd $(DPDPLUGIN)
	# cd to tests to generate .dpd file there.
	cd $(TESTDIR); coqtop -R .. dpdgraph -I .. < Test.cmd > /dev/null 2>&1

%.dpd : %.vo %.cmd
	# cd to tests to generate .dpd file there.
	cd $(TESTDIR); coqtop -R .. dpdgraph -I .. < $(*F).cmd > /dev/null 2>&1

$(TESTDIR)/search.log : $(TESTDIR)/Test.vo $(TESTDIR)/search.cmd $(DPDPLUGIN)
	cat $(TESTDIR)/search.cmd | coqtop -R . dpdgraph 2> /dev/null \
	  | sed -e 's/Welcome to Coq.*/Welcome to Coq/' > $@

%.dot : %.dpd  $(DPD2DOT)
	$(DPD2DOT) $< > /dev/null

%.without.dot : %.dpd  $(DPD2DOT)
	$(DPD2DOT) -without-defs -o $@ $< > /dev/null

%.zgr : %.dot
	zgrviewer $<

%.ok : %.log %.oracle
	$(ECHO_CIBLE)
	@if diff $*.oracle $*.log > /dev/null ; then \
          echo "Bravo... Test Ok" ; \
          touch $@ ; \
        else \
          echo "DIFFERENCES : diff $*.oracle $*.log" ; \
          echo "To force a new execution of the test:" ; \
	  echo "  rm $*.log ; make $*.ok"; \
          echo "To accept the results: " ; \
          echo "  cp $*.log $*.oracle" ; \
          rm -f $@ ; \
        fi

# oracle is updated by user, but one is needed the first time
%.oracle :
	$(ECHO_CIBLE) "[ATTENTION : automatic generation of $@]"
	$(MAKE) $*.log
	cp $*.log $*.oracle

#-------------------------------------------------------------------------------
DISTRIBUTED+=Makefile LICENSE README.md VERSION

distrib : $(NAME)-$(VERSION).tgz

%.tgz : clean
	$(ECHO_CIBLE)
	rm -rf $* $@
	mkdir $*
	cp --parents $(DISTRIBUTED) $*
	tar zcvf $@ $*
	rm -rf $*
	@ echo "Don't forget to copy README.md and $@ on the server if needed"


#-------------------------------------------------------------------------------
# Configuration

Makefile: Makefile.in config.status
	$(ECHO_CIBLE)
	./config.status $@

config.status: configure
	./config.status --recheck

#-------------------------------------------------------------------------------
clean_coq : Make_coq
	$(MAKE) -f $< clean

clean_test :
	rm -f $(TESTS) $(TESTS_LOG) $(TESTS_OK)
	rm -f $(TESTDIR)/Test.vo  $(TESTDIR)/Test.glob
	rm -f $(TESTDIR)/Morph.vo  $(TESTDIR)/Morph.glob

clean_config:
	rm -rf autom4te.cache
	rm -f configure config.log config.status
	rm -r Makefile

clean : clean_coq clean_test
	rm -f $(GENERATED)
	rm -f $(CMOS_DPDUSAGE) $(CMOS_DPD2DOT) $(CMXS) $(ML_ALL:%.ml=%.o) *.cmi
	rm -f $(ML_ALL:%.ml=%.annot)
	rm -f $(DPD2DOT) $(DPDUSAGE) $(DPDPLUGIN)
	echo "Use: make clean_config to remove configuration generated files"