Skip to content

Commit 748fc54

Browse files
ybertotybertot
committed
Modify the build instructions to avoid relying on autoconf, make better
usage of the meta.yml file, and have the testing procedure work in a predictable manner.
1 parent 7817def commit 748fc54

File tree

9 files changed

+311
-648
lines changed

9 files changed

+311
-648
lines changed

‎.github/workflows/docker-action.yml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -16,18 +16,18 @@ jobs:
1616
runs-on: ubuntu-latest
1717
strategy:
1818
matrix:
19-
coq_version:
20-
- 'dev'
19+
image:
20+
- 'rocq/rocq-prover:dev'
2121
fail-fast: false
2222
steps:
2323
- uses: actions/checkout@v4
2424
- uses: coq-community/docker-coq-action@v1
2525
with:
2626
opam_file: 'coq-dpdgraph.opam'
27-
coq_version: ${{ matrix.coq_version }}
27+
custom_image: ${{ matrix.image }}
2828
export: 'OPAMWITHTEST'
2929
env:
30-
OPAMWITHTEST: 'true'
30+
OPAMWITHTEST: true
3131

3232
# See also:
3333
# https://github.com/coq-community/docker-coq-action#readme

‎.gitignore‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -14,13 +14,9 @@ version.ml
1414
graphdepend.ml
1515
searchdepend.ml
1616

17-
autom4te.cache
18-
configure
19-
Makefile
2017
Make_coq.conf
2118
.Make_coq.d
2219
config.log
23-
config.status
2420
*.aux
2521
*.glob
2622
*.mllib.d

‎Make_coq.local‎

Lines changed: 176 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,176 @@
1+
DPD2DOT=./dpd2dot
2+
DPDUSAGE=./dpdusage
3+
ML_COMMON = version.ml dpd_compute.ml dpd_dot.ml \
4+
dpd_parse.ml dpd_lex.ml
5+
MLI_COMMON = version.mli dpd_compute.mli dpd_dot.mli dpd_parse.mli dpd_lex.mli
6+
ML_DPD2DOT = dpd2dot.ml
7+
MLI_DPD2DOT = dpd2dot.mli
8+
ML_DPDUSAGE = dpdusage.ml
9+
MLI_DPDUSAGE = dpdusage.mli
10+
11+
DPD_COMPILE = ocamlfind opt -verbose -package ocamlgraph -linkpkg
12+
13+
post-all :: $(DPD2DOT) $(DPDUSAGE)
14+
15+
dpd_parse.mli dpd_parse.ml : dpd_parse.mly
16+
ocamlyacc $<
17+
18+
dpd_lex.ml : dpd_lex.mll
19+
ocamllex $<
20+
21+
version.ml :
22+
echo "(* This file is generated by Makefile. Do not modify. *)" > $@
23+
echo "let version = \""$(VERSION)"\"" >> $@
24+
25+
has_ocamlgraph :
26+
if ocamlfind query ocamlgraph > /dev/null 2>&1 ; then touch $@ ; else echo "ocamlgraph not installed; use opam install ocamlgraph" ; exit 1; fi
27+
28+
$(DPD2DOT) : $(MLI_COMMON) $(ML_COMMON) $(MLI_DPD2DOT) $(ML_DPD2DOT) has_ocamlgraph
29+
$(DPD_COMPILE) -o $@ $(MLI_COMMON) $(ML_COMMON) \
30+
$(MLI_DPD2DOT) $(ML_DPD2DOT)
31+
32+
$(DPDUSAGE) : $(CMOS_DPDUSAGE) $(CMIS_DPDUSAGE)
33+
$(DPD_COMPILE) -o $@ $(MLI_COMMON) $(ML_COMMON) \
34+
$(MLI_DPDUSAGE) $(ML_DPDUSAGE)
35+
36+
include Make_coq.conf
37+
38+
install-extra :: $(DPD2DOT) $(DPDUSAGE)
39+
cp $(DPD2DOT) $(DPDUSAGE) $(COQLIB)/../../bin
40+
41+
uninstall ::
42+
rm -f $(COQMF_COQLIB)/../../bin/$DPD2DOT)
43+
rm -f $(COQMF_COQLIB)/../../bin/$DPD2USAGE)
44+
45+
#-------------------------------------------------------------------------------
46+
47+
TESTDIR=tests
48+
TESTS_SRC=$(TESTDIR)/Morph.v $(TESTDIR)/Test.v $(TESTDIR)/Polymorph.v \
49+
$(TESTDIR)/PrimitiveProjections.v\
50+
$(TESTDIR)/Morph.cmd $(TESTDIR)/Test.cmd $(TESTDIR)/search.cmd \
51+
$(TESTDIR)/Polymorph.cmd $(TESTDIR)/PrimitiveProjections.cmd
52+
TESTS_DPD=$(TESTDIR)/graph.dpd $(TESTDIR)/graph2.dpd \
53+
$(TESTDIR)/Morph.dpd $(TESTDIR)/Morph_rw.dpd \
54+
$(TESTDIR)/Polymorph.dpd \
55+
$(TESTDIR)/PrimitiveProjections.dpd \
56+
$(TESTDIR)/PrimitiveProjections2.dpd
57+
TESTS_DOT=$(TESTS_DPD:%.dpd=%.dot)
58+
TESTS_ERR_DPD=$(wildcard $(TESTDIR)/*.err.dpd)
59+
60+
TESTS=$(TESTS_DPD) $(TESTS_DOT) $(TESTDIR)/graph.without.dot \
61+
$(TESTDIR)/search $(TESTDIR)/graph2.dpdusage \
62+
$(TESTS_ERR_DPD:%.dpd=%) $(TESTDIR)/file_not_found.err
63+
TESTS_LOG=$(TESTS:%=%.log)
64+
TESTS_ORACLE=$(TESTS:%=%.oracle)
65+
TESTS_OK=$(TESTS:%=%.ok)
66+
67+
clean_test :
68+
rm -f $(TESTS) $(TESTS_LOG) $(TESTS_OK)
69+
rm -f $(TESTDIR)/Test.vo $(TESTDIR)/Test.glob
70+
rm -f $(TESTDIR)/Morph.vo $(TESTDIR)/Morph.glob
71+
rm -f $(TESTDIR)/Polymorph.vo $(TESTDIR)/Polymorph.glob
72+
rm -f $(TESTDIR)/PrimitiveProjections.vo $(TESTDIR)/PrimitiveProjections.glob
73+
rm -f $(TESTDIR)/.*.vo.aux
74+
75+
.PRECIOUS : $(TESTS) $(TESTS_LOG) $(TESTS_ORACLE)
76+
77+
.PHONY: tests test
78+
test : $(TESTS_OK)
79+
80+
.PHONY: test-suite
81+
test-suite:
82+
rm -f tests.ok
83+
($(MAKE) test && touch tests.ok) | tee tmp.log
84+
if grep DIFFERENCES tmp.log >/dev/null 2>&1 ; then \
85+
for i in $$(grep DIFFERENCES tmp.log | grep -o 'diff .*' | sed s'/diff //g' | sed s'/ /~/g'); do \
86+
i="$$(echo "$$i" | sed s'/~/ /g')"; \
87+
echo diff -u $$i; \
88+
diff -u $$i; \
89+
done ; \
90+
fi
91+
if grep DIFFERENCES tmp.log >/dev/null 2>&1 ; then false ; else true ; fi
92+
rm tests.ok
93+
94+
$(TESTDIR)/%.dpdusage.log: $(TESTDIR)/%.dpd $(DPDUSAGE)
95+
$(DPDUSAGE) $< > $@
96+
97+
$(TESTDIR)/file_not_found.err.log: $(DPD2DOT)
98+
$(DPD2DOT) file_not_found.err.dpd > $@ 2>&1
99+
100+
$(TESTDIR)/%.err.log: $(TESTDIR)/%.err.dpd $(DPD2DOT)
101+
$(DPD2DOT) $< > $@ 2>&1
102+
103+
%.log : %
104+
cp $< $@
105+
106+
%.vo : %.v
107+
coqc -q -R . dpdgraph $<
108+
109+
%.html : %.v
110+
coqdoc $<
111+
112+
%.svg : %.dot
113+
dot -Tsvg -o$@ $<
114+
115+
TEST_INCLUDE= -R .. dpdgraph -I ..
116+
117+
$(TESTDIR)/Morph%.dpd : $(TESTDIR)/Morph.vo $(TESTDIR)/Morph.cmd $(DPDPLUGIN)
118+
# cd to tests to generate .dpd file there.
119+
cd $(TESTDIR); coqtop $(TEST_INCLUDE) < Morph.cmd > /dev/null 2>&1
120+
121+
$(TESTDIR)/Polymorph%.dpd : $(TESTDIR)/Polymorph.vo $(TESTDIR)/Polymorph.cmd \
122+
$(DPDPLUGIN)
123+
cd $(TESTDIR); coqtop $(TEST_INCLUDE) < Polymorph.cmd
124+
125+
$(TESTDIR)/graph.dpd $(TESTDIR)/graph2.dpd: \
126+
$(TESTDIR)/Test.vo $(TESTDIR)/Test.cmd $(DPDPLUGIN)
127+
# cd to tests to generate .dpd file there.
128+
cd $(TESTDIR); coqtop $(TEST_INCLUDE) < Test.cmd > /dev/null 2>&1
129+
130+
$(TESTDIR)/PrimitiveProjections.dpd $(TESTDIR)/PrimitiveProjections2.dpd: \
131+
$(TESTDIR)/PrimitiveProjections.vo $(TESTDIR)/PrimitiveProjections.cmd $(DPDPLUGIN)
132+
# cd to tests to generate .dpd file there.
133+
cd $(TESTDIR); coqtop $(TEST_INCLUDE) < PrimitiveProjections.cmd > /dev/null 2>&1
134+
135+
%.dpd : %.vo %.cmd
136+
# cd to tests to generate .dpd file there.
137+
cd $(TESTDIR); coqtop $(TEST_INCLUDE) < $(*F).cmd > /dev/null 2>&1
138+
139+
$(TESTDIR)/search.log : $(TESTDIR)/Test.vo $(TESTDIR)/search.cmd $(DPDPLUGIN)
140+
cd $(TESTDIR) ; coqtop $(TEST_INCLUDE) < search.cmd 2> /dev/null \
141+
| sed -e 's/Welcome to Rocq.*/Welcome to Rocq/' > ../$@
142+
143+
%.dot : %.dpd $(DPD2DOT)
144+
$(DPD2DOT) $< > /dev/null
145+
146+
%.without.dot : %.dpd $(DPD2DOT)
147+
$(DPD2DOT) -without-defs -o $@ $< > /dev/null
148+
149+
%.zgr : %.dot
150+
zgrviewer $<
151+
152+
%.ok : %.log %.oracle
153+
$(ECHO_CIBLE)
154+
@if diff $*.oracle $*.log > /dev/null ; then \
155+
echo "Bravo... Test Ok" ; \
156+
touch $@ ; \
157+
else \
158+
echo "DIFFERENCES : diff $*.oracle $*.log" ; \
159+
echo "To force a new execution of the test:" ; \
160+
echo " rm $*.log ; make $*.ok"; \
161+
echo "To accept the results: " ; \
162+
echo " cp $*.log $*.oracle" ; \
163+
rm -f $@ ; \
164+
fi
165+
166+
# oracle is updated by user, but one is needed the first time
167+
%.oracle :
168+
$(ECHO_CIBLE) "[WARNING : automatic generation of $@]"
169+
$(MAKE) $*.log
170+
cp $*.log $*.oracle
171+
172+
clean ::
173+
rm -f dpd_parse.ml dpd_parse.mli dpd_lex.ml dpd2dot.cm[ix] dpd2dot.o\
174+
dpd_compute.cm[ix] dpd_compute.o dpd_dot.cm[ix] dpd_dot.o \
175+
dpd_lex.cm[ix] dpd_lex.o dpd_parse.cm[ix] dpd_parse.o has_ocamlgraph \
176+
$(TESTS_DPD)

‎Makefile‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2+
# This file is part of the DpdGraph tools.
3+
# Copyright (C) 2009-2025 Anne Pacalet ([email protected])
4+
# and Yves Bertot ([email protected])
5+
# This file is distributed under the terms of the
6+
# GNU Lesser General Public License Version 2.1
7+
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
8+
9+
NAME=coq-dpdgraph
10+
VERSION=1.0-9.0
11+
12+
main_target : all
13+
14+
all install uninstall test test-suite clean clean_test : Make_coq
15+
make -f $< $@
16+
17+
Make_coq : Make
18+
rocq makefile -f $< -o $@
19+
20+
#-------------------------------------------------------------------------------
21+
DISTRIBUTED+=Makefile LICENSE README.md configure Makefile.in
22+
23+
distrib : $(NAME)-$(VERSION).tgz
24+
25+
%.tgz : clean
26+
$(ECHO_CIBLE)
27+
rm -rf $* $@
28+
mkdir $*
29+
cp --parents $(DISTRIBUTED) $*
30+
tar zcvf $@ $*
31+
rm -rf $*
32+
$(ECHO) "Don't forget to copy README.md and $@ on the server if needed"
33+
34+
35+
#-------------------------------------------------------------------------------
36+
# testing
37+
38+
39+
#-------------------------------------------------------------------------------
40+
clean_coq : Make_coq
41+
$(MAKE) -f $< clean
42+
43+
#-------------------------------------------------------------------------------

0 commit comments

Comments
 (0)