-
Notifications
You must be signed in to change notification settings - Fork 3
/
Makefile
530 lines (424 loc) · 17.1 KB
/
Makefile
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
# -------------------------------------------------------------------------
# Compilation and installation rules.
.PHONY: all install uninstall clean
all:
@ dune build @install
# note: @install is smaller than @all,
# as it does not include the tests nor the stage3 executable.
uninstall:
@ dune uninstall
clean::
@ dune clean
install: all
@ dune install
# -------------------------------------------------------------------------
# The rest of this Makefile helps perform tests and prepare releases.
# These commands are intended to be used by Menhir's developers.
# Require bash.
SHELL := bash
# Prevent the built-in bash cd from displaying information.
export CDPATH=
# -------------------------------------------------------------------------
# Testing.
# [make test] runs the tests found in the test/ and demos/ directories.
# The tests declared by (rule (alias test) ...) are attached to the
# target @test. Those declared by (test (name ...)) are attached to
# the target @ runtest.
.PHONY: test
test:
@ dune build --display short @test @runtest
# [make quick] runs a subset of [make test]. One difference is that
# [make quick] runs Menhir only, whereas [make test] runs Menhir and
# compiles the code produced by Menhir's code back-end using [ocamlc].
# Also, [make quick] focuses on test/static/good, whereas [make test]
# includes tests in all directories (test/static, test/dynamic, demos,
# etc.)
.PHONY: quick
quick:
@ dune build --display short @quick
# [make demos] compiles the demos.
# Some demos require coq-menhirlib to be installed.
.PHONY: demos
demos:
@ make -C demos
# [make mono] runs [make test] with a single core. This may produce more
# reliable timing data, to be used subsequently by [make data].
.PHONY: mono
mono:
@ dune build --display short @test -j1
# [make data] extracts statistics and performance data out of the files
# produced by [make test]. Be careful: the timing data is definitely not high
# quality, because every test is run only once and because the tests are run
# in parallel on a heavily-loaded machine. Furthermore, this data is
# machine-dependent. The data is written to analysis/data.csv.
# A test that caused a TIMEOUT is excluded from the data.
# On MacOS, we require gsed instead of sed.
SED=$(shell if [[ "$$OSTYPE" == "darwin"* ]] ; then echo gsed ; else echo sed ; fi)
DATA := analysis/data.csv
.PHONY: data
data: test
@ echo "Collecting data (using $(SED))..." && \
echo "name,mode,terminals,nonterminals,lr0states,lr1states,lr1time" > $(DATA) && \
directory=_build/default/test/static/good && \
successful=0 && timedout=0 && \
for timings in $$directory/*.timings ; do \
name=$${timings%.timings} ; \
out=$$name.out ; \
name=`basename $$name` ; \
echo "Processing $${name}..." ; \
if grep --quiet "TIMEOUT after" $$out ; then \
((timedout++)) ; \
else \
((successful++)) ; \
mode=`$(SED) -n -e "s/^The construction mode is \([a-z\-]\+\)./\1/p" $$out` ; \
terminals=`$(SED) -n -e "s/^Grammar has \([0-9]\+\) terminal symbols./\1/p" $$out` ; \
nonterminals=`$(SED) -n -e "s/^Grammar has \([0-9]\+\) nonterminal symbols, among which [0-9]\+ start symbols./\1/p" $$out` ; \
lr0states=`$(SED) -n -e "s/^Built an LR(0) automaton with \([0-9]\+\) states./\1/p" $$out` ; \
lr1states=`$(SED) -n -e "s/^Built an LR(1) automaton with \([0-9]\+\) states./\1/p" $$out` ; \
lr1time=`$(SED) -n -e "s/^Construction of the LR(1) automaton: \(.*\)s/\1/p" $$timings` ; \
echo "$$name,$$mode,$$terminals,$$nonterminals,$$lr0states,$$lr1states,$$lr1time" >> $(DATA) ; \
fi \
done && \
echo "$$successful successful tests; $$timedout timed out tests." ; \
echo "The results have been written to $(DATA)."
clean::
@ rm -f $(DATA)
# [make plot] uses Rscript to plot the data extracted by [make data].
.PHONY: plot
plot:
@ echo "Running R..."
@ cd analysis && ./analysis.r
clean::
@ rm -f analysis/*.pdf
# [make benchmarks] runs the benchmarks.
.PHONY: benchmarks
benchmarks:
@ make -C benchmarks
# [make houblix] runs just the tests in test/dynamic/houblix.
.PHONY: houblix
houblix:
@ dune build @test_houblix
# [make versions] compiles and tests Menhir under many versions of
# OCaml, whose list is specified below.
# This requires appropriate opam switches to exist. A missing switch
# can be created like this:
# opam switch create 4.03.0
# eval $(opam env)
# opam install dune ppx_sexp_conv sexplib
# Because MenhirCST requires OCaml 4.08, we split the version check
# in two parts.
OLD_VERSIONS := \
4.03.0 \
4.04.2 \
4.05.0 \
4.06.1 \
4.07.1 \
4.08.1 \
4.09.1 \
4.09.0+bytecode-only \
4.10.0 \
4.11.1 \
NEW_VERSIONS := \
4.12.0 \
4.13.1 \
4.14.1 \
5.0.0 \
5.1.0 \
.PHONY: old_versions new_versions versions
old_versions:
@(echo "(lang dune 2.0)" && \
for v in $(NEW_VERSIONS) ; do \
echo "(context (opam (switch $$v)))" ; \
done) > dune-workspace.versions
@ dune build --workspace dune-workspace.versions lib sdk src
new_versions:
@(echo "(lang dune 2.0)" && \
for v in $(NEW_VERSIONS) ; do \
echo "(context (opam (switch $$v)))" ; \
done) > dune-workspace.versions
@ dune build --workspace dune-workspace.versions @install # or: @all
versions: old_versions new_versions
.PHONY: handiwork
handiwork:
@ current=`opam switch show` ; \
for v in $(VERSIONS) ; do \
opam switch $$v && \
eval $$(opam env) && \
opam install --yes sek ; \
done ; \
opam switch $$current
# [make promote] updates the contents of *all* reference files (those
# that contain the expected output of every test). This command should
# be run only when you trust that every test produces correct output.
# [make promote] can *update* existing reference files, but will not
# *create* them when they do not exist. Also, it updates *all* files;
# it cannot be used to refresh a few specific files. Both of these
# limitations can be worked around by using the script [promote.sh].
.PHONY: promote
promote:
@ dune build @test --auto-promote >/dev/null 2>&1 || true
# [make depend] regenerates the files dune.auto. This command should
# be run every time some tests are added or removed or renamed in the
# subdirectories test/static/{good,bad} and test/dynamic/semantics/data
# and test/dynamic/houblix/{tests,backends}.
.PHONY: depend
depend:
@ dune build @depend --auto-promote || true
# -------------------------------------------------------------------------
# Cleaning up.
clean::
@ find . -name "*~" -exec rm '{}' \;
@ for i in demos doc ; do \
$(MAKE) -C $$i $@ ; \
done
# -------------------------------------------------------------------------
# Distribution.
# The version number is automatically set to the current date,
# unless DATE is defined on the command line.
DATE := $(shell /bin/date +%Y%m%d)
DATEDASH := $(shell /bin/date +%Y-%m-%d)
PACKAGE := menhir-$(DATE)
CURRENT := $(shell pwd)
TARBALL := $(CURRENT)/$(PACKAGE).tar.gz
# -------------------------------------------------------------------------
# The names of the modules in MenhirLib are obtained by reading the
# non-comment lines in menhirLib.mlpack.
MENHIRLIB_MODULES := \
$(shell grep -ve "^[ \t\n\r]*\#" lib/pack/menhirLib.mlpack)
# The names of the source files in MenhirLib are obtained by adding
# an .ml or .mli extension to the module name. (We assume that the
# first letter of the file name is a capital letter.)
MENHIRLIB_FILES := \
$(shell for m in $(MENHIRLIB_MODULES) ; do \
ls lib/$$m.{ml,mli} 2>/dev/null ; \
done)
# -------------------------------------------------------------------------
# Propagating an appropriate header into every file.
# This requires a version of headache that supports UTF-8; please use
# https://github.com/Frama-C/headache
# This used to be done at release time and not in the repository, but
# it is preferable to do in it the repository too, for two reasons: 1-
# the repository is (or will be) publicly accessible; and 2- this makes
# it easier to understand the line numbers that we sometimes receive as
# part of bug reports.
# The source files in lib/ and cst/ carry the "library" header & license.
# Those in coq-menhirlib/ carry the "Coq library" header & license.
# Every other file carries the "regular" header & license.
HEADACHE := headache
SRCHEAD := $(CURRENT)/headers/regular-header
LIBHEAD := $(CURRENT)/headers/library-header
COQLIBHEAD := $(CURRENT)/headers/coq-library-header
HEADACHECOQCONF := $(CURRENT)/headers/headache-coq.conf
FIND := $(shell if command -v gfind >/dev/null ; then echo gfind ; else echo find ; fi)
.PHONY: headache
headache:
@ cd src && $(FIND) . -regex ".*\.ml\(i\|y\|l\)?" \
-exec $(HEADACHE) -h $(SRCHEAD) "{}" ";"
@ cd sdk && $(FIND) . -regex ".*\.ml\(i\|y\|l\)?" \
-exec $(HEADACHE) -h $(SRCHEAD) "{}" ";"
@ for file in $(MENHIRCST_FILES) ; do \
$(HEADACHE) -h $(LIBHEAD) $$file ; \
done
@ for file in cst/*.{ml,mli} ; do \
$(HEADACHE) -h $(LIBHEAD) $$file ; \
done
@ for file in coq-menhirlib/src/*.v ; do \
$(HEADACHE) -h $(COQLIBHEAD) -c $(HEADACHECOQCONF) $$file ; \
done
# -------------------------------------------------------------------------
# Creating a release.
# A release commit is created off the main branch, on the side, and tagged.
# Indeed, some files need to be changed or removed for a release.
BRANCH := release-branch-$(DATE)
# The documentation files $(DOC) are copied to the directory $(RELEASE) on the
# master branch. They are also copied to the directory $(WWW).
DOC := doc/manual.pdf doc/manual.html doc/manual*.png
RELEASE := releases/$(DATE)
WWW := www
# Prior to making a release, please follow this check-list:
# 1. Make sure that [CHANGES.md] has been properly updated.
# 2. Make sure that [coq-menhirlib/CHANGES.md] has been properly updated.
# 3. Run [make test] to make sure that Menhir can be compiled and works.
# 4. Run [make demos] to make sure that the demos can be compiled.
# 5. Run [make versions] to make sure that Menhir can be compiled
# under all supported versions of OCaml.
# 6. Run [make benchmarks] and have a look at the performance figures to make
# sure that they are in the right ballpark.
# You may wish to test the opam package by running [make pin]. (This
# can be done in a dedicated switch, so as to avoid clobbering your
# regular installation of Menhir.)
# You may wish to run [./compile-ocaml.sh], which checks that Menhir
# is able to compile OCaml. This test requires about 3 minutes.
.PHONY: release
release:
# Check that we have hevea.
@ if ! which hevea ; then \
echo "hevea is missing. The current opam switch is:" ; \
opam switch show ; \
exit 1; \
fi
# Check if this is the master branch.
@ if [ "$$(git symbolic-ref --short HEAD)" != "master" ] ; then \
echo "Error: this is not the master branch." ; \
git branch ; \
exit 1 ; \
fi
# Check if everything has been committed.
@ if [ -n "$$(git status --porcelain)" ] ; then \
echo "Error: there remain uncommitted changes." ; \
git status ; \
exit 1 ; \
fi
# Check the current package description.
@ opam lint
# Create a fresh git branch and switch to it.
@ echo "Preparing a release commit on a fresh release branch..."
@ git checkout -b $(BRANCH)
# Remove subdirectories that do not need to (or must not) be distributed.
@ make --quiet -C coq-menhirlib clean
@ git rm -rf analysis attic demos headers releases test www --quiet
# Remove files that do not need to (or must not) be distributed.
# Keep check-tarball.sh because it is used below.
@ git rm --quiet \
Makefile \
promote.sh \
*.md TODO* \
*.opam coq-menhirlib/descr
# Hardcode Menhir's version number in the files that need it.
@ sed -i.bak 's/unreleased/$(DATE)/' dune-project
@ rm -f dune-project.bak
@ git add dune-project
@ echo '\gdef\menhirversion{$(DATE)}' > doc/version.tex
@ git add doc/version.tex
@ echo 'Definition require_$(DATE) := tt.' > coq-menhirlib/src/Version.v
@ git add coq-menhirlib/src/Version.v
# Compile the documentation.
@ echo "Building the documentation..."
@ make --quiet -C doc clean >/dev/null
@ make --quiet -C doc all >/dev/null
@ git add -f $(DOC)
@ echo '(include dune.manual)' >> doc/dune
@ git add doc/dune
# Commit.
@ echo "Committing..."
@ git commit -m "Release $(DATE)." --quiet
# Check that the build and installation seem to work.
# We build our own archive, which is not necessarily identical to the one
# that gitlab creates for us once we publish our release. This should be
# good enough.
@ echo "Creating an archive..."
@ git archive --prefix=$(PACKAGE)/ --format=tar.gz --output=$(TARBALL) HEAD
@ echo "Checking that this archive can be compiled and installed..."
@ ./check-tarball.sh $(PACKAGE)
@ echo "Removing this archive..."
@ rm $(TARBALL)
# Create a git tag.
@ git tag -a $(DATE) -m "Release $(DATE)."
# Save a copy of the manual.
@ mkdir -p $(RELEASE)/doc
@ cp $(DOC) $(RELEASE)/doc
# Switch back to the master branch.
@ echo "Switching back to the master branch..."
@ git checkout master
# Commit a copy of the manual *in the master branch* in releases/.
@ echo "Committing a copy of the documentation..."
@ cd $(RELEASE) && git add -f $(DOC)
@ echo "Publishing the documentation online..."
@ cd $(WWW) && git rm -rf doc
@ cd $(WWW) && cp -r ../$(RELEASE)/doc .
@ cd $(WWW) && git add $(DOC)
@ git commit -m "Saved and published documentation for release $(DATE)."
# Done.
@ echo "Done."
@ echo "If happy, please type:"
@ echo " \"make publish\" to push this release to gitlab.inria.fr"
@ echo " \"make export\" to upload the manual to yquem.inria.fr"
@ echo " \"make opam\" to create a new opam package"
@ echo "Otherwise, please type:"
@ echo " \"make undo\" to undo this release"
.PHONY: publish
publish:
# Push the new branch and tag to gitlab.inria.fr.
@ git push origin $(BRANCH)
@ git push --tags
.PHONY: undo
undo:
# Delete the new branch and tag.
@ git branch -D $(BRANCH)
@ git tag -d $(DATE)
# Delete the new commit on the master branch.
@ git reset --hard HEAD~1
# -------------------------------------------------------------------------
# Copying the documentation to François' page on yquem.
# I would like to serve these files on gitlab.inria.fr,
# but I don't know how to make them look like native .html
# and .pdf files.
# Also, I don't know how to obtain a stable URL that always
# points to the latest released version of the documentation.
RSYNC := scp -p -C
TARGET := yquem.inria.fr:public_html/menhir/
# This assumes that [make release] has been run.
.PHONY: export
export:
# Copy the documentation to yquem.
$(RSYNC) $(RELEASE)/doc/* $(TARGET)
# -------------------------------------------------------------------------
# Publishing a new version of the opam packages.
# This entry assumes that [make release] has been run on the same day.
# There are two opam packages: one for menhir (part of the OCaml opam
# repository) and one for coq-menhirlib (part of the Coq opam repository).
# The following command should have been run once:
# opam publish repo add opam-coq-archive coq/opam-coq-archive
# An abbreviation.
COQLIB := coq-menhirlib
# Menhir's repository URL (https).
REPO := https://gitlab.inria.fr/fpottier/menhir
# The archive URL (https).
ARCHIVE := $(REPO)/-/archive/$(DATE)/archive.tar.gz
# NOTE: it is not clear whether the above URL is stable in time.
# The gitlab API documentation documents the following URL:
# https://gitlab.inria.fr/api/v4/projects/fpottier%2Fmenhir/repository/archive.tar.gz?sha=$(DATE)
# The documentation can be found here:
# https://gitlab.inria.fr/help/api/repositories.html#get-file-archive
# Additional options for coq-menhirlib.
COQ_MENHIRLIB_PUBLISH_OPTIONS := \
--repo coq/opam-coq-archive \
--packages-directory released/packages \
.PHONY: opam
opam:
# Publish opam descriptions for menhirCST, menhirLib, menhirSdk, menhir.
@ opam publish -v $(DATE) menhirCST.opam menhirLib.opam menhirSdk.opam menhir.opam $(ARCHIVE)
# Patch coq-menhirlib.opam.
# We replace the string DATEDASH with $(DATEDASH).
# We replace the string DATE with $(DATE).
@ cat $(COQLIB).opam \
| sed -e 's/DATEDASH/$(DATEDASH)/g' \
| sed -e 's/DATE/$(DATE)/g' \
> $(COQLIB).patched.opam
# Publish an opam description for coq-menhirlib.
@ opam publish -v $(DATE) $(COQ_MENHIRLIB_PUBLISH_OPTIONS) \
$(COQLIB).patched.opam $(ARCHIVE)
@ rm $(COQLIB).patched.opam
# -------------------------------------------------------------------------
# Re-installing locally. This can overwrite an existing local installation.
.PHONY: pin
pin:
opam pin --yes add menhirCST.dev . && \
opam pin --yes add menhirLib.dev . && \
opam pin --yes add menhirSdk.dev . && \
opam pin --yes add menhir.dev .
.PHONY: unpin
unpin:
opam pin --yes remove menhirCST menhirLib menhirSdk menhir
# -------------------------------------------------------------------------
# Running the Markdown linter on our Markdown files.
# For an explanation of mdl's error messages, see:
# https://github.com/mivok/markdownlint/blob/master/docs/RULES.md
# We use the command [expand] to expand tabs to spaces.
MDFILES = $(shell find . -name "*.md" | grep -v _build)
.PHONY: mdl
mdl:
@ for f in $(MDFILES) ; do \
cp $$f $$f.bak && expand $$f.bak > $$f && rm $$f.bak ; \
done
@ mdl $(MDFILES)