GNUmakefile 11 KB
Newer Older
1
2
# -------------------------------------------------------------------------

3
4
# This Makefile helps perform tests and prepare releases. This is *not* the
# Makefile that compiles and installs Menhir on a user's machine.
5

6
# Require bash.
7
SHELL := bash
8
9
# Prevent the built-in bash cd from displaying information.
export CDPATH=
10
11
12

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

fpottier's avatar
fpottier committed
13
# A dummy entry.
14

15
.PHONY: all
16
all:
fpottier's avatar
fpottier committed
17
	@echo Please go down into src/ if you wish to compile Menhir.
18
19
20
21

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

# Testing.
22

POTTIER Francois's avatar
POTTIER Francois committed
23
24
25
# This assumes that [make -C src everyday bootstrap] has been run
# (or that MENHIR is set and points to a Menhir executable that
# one wishes to test).
26

27
.PHONY: test
28
test:
POTTIER Francois's avatar
POTTIER Francois committed
29
	$(MAKE) -C test
30
31
32
33
34

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

# Cleaning up.

35
.PHONY: clean
36
clean:
37
	@ for i in test demos src quicktest doc ; do \
fpottier's avatar
fpottier committed
38
	  $(MAKE) -C $$i $@ ; \
39
40
41
42
43
	done

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

# Distribution.
POTTIER Francois's avatar
POTTIER Francois committed
44

fpottier's avatar
fpottier committed
45
# The version number is automatically set to the current date,
POTTIER Francois's avatar
Typo.    
POTTIER Francois committed
46
# unless DATE is defined on the command line.
47
DATE     := $(shell /bin/date +%Y%m%d)
48
DATEDASH := $(shell /bin/date +%Y-%m-%d)
fpottier's avatar
fpottier committed
49

50
51
52
53
PACKAGE  := menhir-$(DATE)
CURRENT  := $(shell pwd)
TARBALL  := $(CURRENT)/$(PACKAGE).tar.gz

54
# -------------------------------------------------------------------------
55

56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
# 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]*\#" src/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 src/$$m.{ml,mli} 2>/dev/null ; \
	                     done)

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

71
72
73
# Propagating an appropriate header into every file.

# This requires a version of headache that supports UTF-8; please use
POTTIER Francois's avatar
POTTIER Francois committed
74
# https://github.com/Frama-C/headache
75
76
77
78
79
80
81
82
83
84
85

# 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.

# Menhir's standard library (standard.mly) as well as the source files
# in MenhirLib carry the "library" license, while every other file
# carries the "regular" license.

86
87
88
89
90
91
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)
92

93
.PHONY: headache
94
headache:
95
	@ cd src && $(FIND) . -regex ".*\.ml\(i\|y\|l\)?" \
96
97
98
99
	    -exec $(HEADACHE) -h $(SRCHEAD) "{}" ";"
	@ for file in src/standard.mly $(MENHIRLIB_FILES) ; do \
	    $(HEADACHE) -h $(LIBHEAD) $$file ; \
	  done
100
101
102
	@ for file in coq-menhirlib/src/*.v ; do \
	    $(HEADACHE) -h $(COQLIBHEAD) -c $(HEADACHECOQCONF) $$file ; \
	  done
103
104
105

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

106
# Creating a release.
107

108
109
# 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.
110

111
BRANCH := release-branch-$(DATE)
112

113
114
# The documentation files $(DOC) are copied to the directory $(RELEASE) on the
# master branch. They are also copied to the directory $(WWW).
115

116
117
DOC     := doc/manual.pdf doc/manual.html doc/manual*.png
RELEASE := releases/$(DATE)
118
WWW     := www
119

120
121
# Prior to making a release, one should run [make test],
# then [make pin] and [make -C demos].
122

123
124
125
126
127
128
129
130
131
132
133
134
135
136
.PHONY: release
release:
# 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
137
138
# Check the current package description.
	@ opam lint
139
140
141
142
143
144
145
146
147
148
149
150
151
# Create a fresh git branch and switch to it.
	@ echo "Preparing a release commit on a fresh release branch..."
	@ git checkout -b $(BRANCH)
# In src/_tags, remove every line tagged "my_warnings".
	@ cd src && grep -v my_warnings _tags > _tags.new && mv _tags.new _tags
	@ git add src/_tags
# The file src/installation.ml is not under version control, so won't be
# included in the archive. We nevertheless remove it, for a clean test
# build below.
	@ rm -f src/installation.ml
# Remove subdirectories that do not need to (or must not) be distributed.
	@ make --quiet -C test clean
	@ make --quiet -C quicktest clean
152
	@ make --quiet -C coq-menhirlib clean
153
154
155
	@ git rm -rf attic headers quicktest releases src/attic test --quiet
# Remove files that do not need to (or must not) be distributed.
# Keep check-tarball.sh because it is used below.
156
	@ git rm GNUmakefile HOWTO.md TODO* *.opam coq-menhirlib/descr --quiet
157
158
159
160
161
162
163
164
165
166
167
168
# Hardcode the version number in the files that mention it. These
# include version.ml, StaticVersion.{ml,mli}, version.tex, META.
	@ echo let version = \"$(DATE)\" > src/version.ml
	@ git add src/version.ml
	@ echo version = \"$(DATE)\" >> src/menhirLib.META
	@ echo version = \"$(DATE)\" >> src/menhirSdk.META
	@ git add src/menhirLib.META src/menhirSdk.META
	@ echo "let require_$(DATE) = ()" > src/StaticVersion.ml
	@ echo "val require_$(DATE) : unit" > src/StaticVersion.mli
	@ git add src/StaticVersion.ml src/StaticVersion.mli
	@ echo '\gdef\menhirversion{$(DATE)}' > doc/version.tex
	@ git add doc/version.tex
169
	@ echo 'Definition require_$(DATE) := tt.' >> coq-menhirlib/src/Version.v
170
	@ git add coq-menhirlib/src/Version.v
171
172
173
174
175
# 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)
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
# 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)."
191
192
193
# Save a copy of the manual.
	@ mkdir -p $(RELEASE)/doc
	@ cp $(DOC) $(RELEASE)/doc
194
# Switch back to the master branch.
195
196
	@ echo "Switching back to the master branch..."
	@ git checkout master
197
# Commit a copy of the manual *in the master branch* in releases/.
198
	@ echo "Committing a copy of the documentation..."
199
200
201
202
203
204
	@ 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)."
205
206
# Done.
	@ echo "Done."
207
208
209
210
211
212
	@ 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"
213
214
215
216
217
218
219
220
221
222
223
224
225

.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 two new commits on the master branch.
226
	@ git reset --hard HEAD~1
227
228
229

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

230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
# Copying the documentation to François' page on yquem.

# I would have 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/
PAGE    := /home/fpottier/dev/page

# This assumes that [make release] has been run.

.PHONY: export
export:
# Copy the documentation to yquem.
	$(RSYNC) $(RELEASE)/doc/* $(TARGET)

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

251
# Publishing a new version of the opam packages.
252
253

# This entry assumes that [make release] has been run on the same day.
254

255
256
257
# 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).

258
# You need a version of opam-publish that supports --packages-directory:
259
260
261
262
263
264
265
266
#   git clone git@github.com:fpottier/opam-publish.git
#   cd opam-publish
#   git checkout 2.0
#   opam pin add opam-publish.dev .

# The following command should have been run once:
#   opam publish repo add opam-coq-archive coq/opam-coq-archive

267
268
# The package name.
THIS     := menhir
269
THAT     := coq-menhirlib
270

271
# Menhir's repository URL (https).
272
REPO     := https://gitlab.inria.fr/fpottier/$(THIS)
273

274
275
# The archive URL (https).
ARCHIVE  := $(REPO)/repository/$(DATE)/archive.tar.gz
276

277
# Additional options for coq-menhirlib.
278
COQ_MENHIRLIB_PUBLISH_OPTIONS := \
279
  --repo coq/opam-coq-archive \
280
  --packages-directory released/packages \
281

282
.PHONY: opam
283
opam:
284
# Publish an opam description for menhir.
285
	@ opam publish -v $(DATE) $(THIS).opam $(ARCHIVE)
286
287
288
# Patch coq-menhirlib.opam.
# We replace the string DATEDASH with $(DATEDASH).
# We replace the string DATE with $(DATE).
289
	@ cat $(THAT).opam \
290
291
292
	  | sed -e 's/DATEDASH/$(DATEDASH)/g' \
	  | sed -e 's/DATE/$(DATE)/g' \
	  > $(THAT).patched.opam
293
294
295
# Publish an opam description for coq-menhirlib.
	@ opam publish -v $(DATE) $(COQ_MENHIRLIB_PUBLISH_OPTIONS) $(THAT).patched.opam $(ARCHIVE)
	@ rm $(THAT).patched.opam
296
297
298
299
300

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

# Re-installing locally. This can overwrite an existing local installation.

301
.PHONY: pin
302
pin:
303
	opam pin add menhir.dev .
304

305
.PHONY: unpin
306
307
unpin:
	opam pin remove menhir
308

POTTIER Francois's avatar
POTTIER Francois committed
309
310
.PHONY: reinstall
reinstall:
311
312
313
314
315
	opam reinstall -v --working-dir menhir
# We do not use --assume-built,
# as it would require first re-building everything using
#   make PREFIX=`pwd`/src -f Makefile all
# and that is time-consuming.
POTTIER Francois's avatar
POTTIER Francois committed
316

317
318
319
320
321
322
323
# -------------------------------------------------------------------------

# 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

324
325
MDFILES := *.md */*.md

326
.PHONY: mdl
327
mdl:
328
	@ for f in $(MDFILES) ; do \
329
330
	  cp $$f $$f.bak && expand $$f.bak > $$f && rm $$f.bak ; \
	done
331
	@ mdl $(MDFILES)