Merge pull request #114 from SkySkimmer/nodune

Author: Alizter

.github/workflows/docker-action.yml

@@ -20,7 +20,7 @@ jobs:
           - 'coqorg/coq:dev'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v2
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-dpdgraph.opam'
@@ -29,7 +29,6 @@ jobs:
         env:
           OPAMWITHTEST: 'true'
 
-
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme
 # https://github.com/erikmd/docker-coq-github-action-demo

.gitignore

@@ -1,4 +1,47 @@
-_build
-*~
-.merlin
-*.install
+.depend
+*.annot
+*.cmo
+*.cma
+*.cmi
+*.a
+*.o
+*.cmx
+*.cmxs
+*.cmxa
+*.mlg.d
+version.ml
+graphdepend.ml
+searchdepend.ml
+
+autom4te.cache
+configure
+Makefile
+Make_coq.conf
+.Make_coq.d
+config.log
+config.status
+*.aux
+*.glob
+*.mllib.d
+*.v.d
+*.vo
+*.vok
+*.vos
+
+coqthmdep
+dpd2dot
+dpdusage
+Make_coq
+CoqMakefile.conf
+dpd_lex.ml
+dpd_parse.ml
+dpd_parse.mli
+tests/*.log
+tests/*.ok
+tests/*.dot
+tests/*.dpd
+!tests/*.err.dpd
+tests/*.glob
+tests/Test.vo
+
+META.coq-dpdgraph

Make

@@ -0,0 +1,7 @@
+-generate-meta-for-package coq-dpdgraph
+-I .
+-R . dpdgraph
+searchdepend.mlg
+graphdepend.mlg
+dpdgraph.mllib
+dpdgraph.v

Makefile

@@ -0,0 +1,306 @@
+#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+#            This file is part of the DpdGraph tools.
+#  Copyright (C) 2009-2017 Anne Pacalet ([email protected])
+#                      and Yves Bertot ([email protected])
+#                ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+#      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=@PACKAGE_NAME@
+VERSION=@PACKAGE_VERSION@
+
+BINDIR=@BINDIR@
+
+DPDPLUGIN=./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
+
+DISTRIBUTED+=dpdgraph.v
+
+ML_COMMON = version.ml $(PRE)_compute.ml $(PRE)_dot.ml \
+          $(PRE)_parse.ml  $(PRE)_lex.ml
+MLI_COMMON =  version.mli $(PRE)_compute.mli $(PRE)_dot.mli $(PRE)_lex.mli
+ML_DPD2DOT = $(PRE)2dot.ml
+MLI_DPD2DOT = $(PRE)2dot.mli
+ML_DPDUSAGE = $(PRE)usage.ml
+MLI_DPDUSAGE = $(PRE)usage.mli
+
+DISTRIBUTED+=$(MLI_COMMON) $(MLI_DPD2DOT) $(MLI_DPDUSAGE)
+
+ML_ALL = $(ML_COMMON) $(ML_DPD2DOT) $(ML_DPDUSAGE)
+
+CMIS_DPD2DOT=$(MLI_COMMON:%.ml=%.cmo) $(MLI_DPD2DOT:%.ml=%.cmo)
+CMOS_DPD2DOT=$(ML_COMMON:%.ml=%.cmo) $(ML_DPD2DOT:%.ml=%.cmo)
+CMIS_DPDUSAGE=$(MLI_COMMON:%.ml=%.cmo) $(MLI_DPDUSAGE:%.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@
+
+WARN_ERR := -warn-error +a
+OCAMLFLAGS :=  -w +a $(WARN_ERR) -g -dtypes $(INCLUDES) -c
+OCAMLFLAGS += $(OCAML_EXTRA_OPTS)
+OCAMLOPTFLAGS = -c
+
+COQ_MAKEFILE=@COQ_MAKEFILE@
+# COQDEP=$(OCAMLDEP)
+
+COQEXTFILES=searchdepend.mlg graphdepend.mlg
+
+GENERATED+=$(COQEXTFILES:%.mlg=%.o) $(COQEXTFILES:%.mlg=%.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 $< -o $@
+
+GENERATED+= Make_coq
+
+version.ml : configure
+	$(ECHO_CIBLE)
+	$(ECHO) "(* This file is generated by Makefile. Do not modify. *)" > $@
+	$(ECHO) "let version = \""$(VERSION)"\"" >> $@
+
+GENERATED+=version.ml
+
+$(DPD2DOT) : $(CMOS_DPD2DOT) $(CMIS_DPD2DOT)
+	$(ECHO_CIBLE)
+	$(OCAMLC) -g $(INCLUDES) -o $@ graph.cma $(CMOS_DPD2DOT)
+
+$(DPDUSAGE) : $(CMOS_DPDUSAGE) $(CMIS_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)/PrimitiveProjections.v\
+	  $(TESTDIR)/Morph.cmd $(TESTDIR)/Test.cmd $(TESTDIR)/search.cmd \
+          $(TESTDIR)/Polymorph.cmd $(TESTDIR)/PrimitiveProjections.cmd
+TESTS_DPD=$(TESTDIR)/graph.dpd $(TESTDIR)/graph2.dpd \
+	  $(TESTDIR)/Morph.dpd $(TESTDIR)/Morph_rw.dpd \
+	  $(TESTDIR)/Polymorph.dpd \
+          $(TESTDIR)/PrimitiveProjections.dpd \
+	  $(TESTDIR)/PrimitiveProjections2.dpd
+TESTS_DOT=$(TESTS_DPD:%.dpd=%.dot)
+TESTS_ERR_DPD=$(wildcard $(TESTDIR)/*.err.dpd)
+
+TESTS=$(TESTS_DPD) $(TESTS_DOT) $(TESTDIR)/graph.without.dot \
+      $(TESTDIR)/search  $(TESTDIR)/graph2.dpdusage \
+      $(TESTS_ERR_DPD:%.dpd=%) $(TESTDIR)/file_not_found.err
+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)
+
+.PHONY: test-suite
+test-suite:
+	rm -f tests.ok
+	($(MAKE) tests && touch tests.ok) | tee tmp.log
+	if grep DIFFERENCES tmp.log >/dev/null 2>&1 ; then \
+		for i in $$(grep DIFFERENCES tmp.log | grep -o 'diff .*' | sed s'/diff //g' | sed s'/ /~/g'); do \
+			i="$$(echo "$$i" | sed s'/~/ /g')"; \
+			echo diff $$i; \
+			diff $$i; \
+		done ; \
+	fi
+	if grep DIFFERENCES tmp.log >/dev/null 2>&1 ; then false ; else true ; fi
+	rm tests.ok
+
+$(TESTDIR)/%.dpdusage.log: $(TESTDIR)/%.dpd $(DPDUSAGE)
+	$(DPDUSAGE) $< > $@
+
+$(TESTDIR)/file_not_found.err.log: $(DPD2DOT)
+	$(DPD2DOT) file_not_found.err.dpd  > $@ 2>&1
+
+$(TESTDIR)/%.err.log: $(TESTDIR)/%.err.dpd $(DPD2DOT)
+	$(DPD2DOT) $< > $@ 2>&1
+
+%.log : %
+	cp $< $@
+
+%.vo : %.v
+	coqc -q -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
+
+$(TESTDIR)/PrimitiveProjections.dpd $(TESTDIR)/PrimitiveProjections2.dpd: \
+	             $(TESTDIR)/PrimitiveProjections.vo $(TESTDIR)/PrimitiveProjections.cmd $(DPDPLUGIN)
+	# cd to tests to generate .dpd file there.
+	cd $(TESTDIR); coqtop -R .. dpdgraph -I .. < PrimitiveProjections.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 -I . 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) "[WARNING : automatic generation of $@]"
+	$(MAKE) $*.log
+	cp $*.log $*.oracle
+
+#-------------------------------------------------------------------------------
+DISTRIBUTED+=Makefile LICENSE README.md configure Makefile.in
+
+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
+	rm -f $(TESTDIR)/Polymorph.vo $(TESTDIR)/Polymorph.glob
+	rm -f  $(TESTDIR)/.*.vo.aux
+
+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"
+
+archi_clean: clean clean_config
+
+#-------------------------------------------------------------------------------