Skip to content

GitLab

Commit 21741c6b authored by POTTIER Francois's avatar POTTIER Francois
Browse files

The BIG SWITCH from ocamlbuild to dune. 

* Remove support for installing via ocamlfind.
* Remove PREFIX.
* Move the source of MenhirLib into lib/.
* Move the source of MenhirSdk into sdk/.
* Build and install everything using dune.
* Run all tests using dune. Reorganize the test directory.
* Move the old ocamlbuild demos to a subdirectory.
* Introduce [make versions] to test Menhir with multiple versions of OCaml.
* Update the release scripts.
parent 13e4da9f
Hide whitespace changes
Inline Side-by-side
Showing with 683 additions and 923 deletions

Too many changes to show.

To preserve performance only 1000 of 1000+ files are displayed.
Plain diff Email patch
CHANGES.md
View file @ 21741c6b
# Changes
## 2020/01/21
* There used to be a distinction between two slightly different ways of
installing Menhir, namely with and without `ocamlfind`. This distinction
disappears. The command line switch `--suggest-ocamlfind` is deprecated
and causes Menhir to print `false`.
* Menhir is now built and installed by dune. This should make life easier
for developers: in particular, `make test` and `make speed` can be run
straight away and do not requiring installing Menhir first. This should
also make compilation much faster on multi-core machines. (Contributed
by Nicolás Ojeda Bär, to whom many thanks are due.)
## 2019/09/24
* Build Menhir's standard library into the Menhir executable instead of
......
GNUmakefile deleted 100644 → 0
View file @ 13e4da9f
# -------------------------------------------------------------------------
# This Makefile helps perform tests and prepare releases. This is *not* the
# Makefile that compiles and installs Menhir on a user's machine.
# Require bash.
SHELL := bash
# Prevent the built-in bash cd from displaying information.
export CDPATH=
# -------------------------------------------------------------------------
# A dummy entry.
.PHONY: all
all:
@echo Please go down into src/ if you wish to compile Menhir.
# -------------------------------------------------------------------------
# Testing.
# 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).
.PHONY: test
test:
$(MAKE) -C test
# -------------------------------------------------------------------------
# Cleaning up.
.PHONY: clean
clean:
@ for i in test demos src quicktest 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]*\#" 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)
# -------------------------------------------------------------------------
# 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.
# 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.
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) "{}" ";"
@ for file in src/standard.mly $(MENHIRLIB_FILES) ; 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, one should run [make test],
# then [make pin] and [make -C demos].
.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
# 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)
# 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
@ make --quiet -C coq-menhirlib clean
@ 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.
@ git rm GNUmakefile HOWTO.md TODO* *.opam coq-menhirlib/descr --quiet
# 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
@ 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)
# 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 two new commits on the master branch.
@ git reset --hard HEAD~1
# -------------------------------------------------------------------------
# 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)
# -------------------------------------------------------------------------
# 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).
# You need a version of opam-publish that supports --packages-directory:
# 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
# The package name.
THIS := menhir
THAT := coq-menhirlib
# Menhir's repository URL (https).
REPO := https://gitlab.inria.fr/fpottier/$(THIS)
# The archive URL (https).
ARCHIVE := $(REPO)/repository/$(DATE)/archive.tar.gz
# Additional options for coq-menhirlib.
COQ_MENHIRLIB_PUBLISH_OPTIONS := \
--repo coq/opam-coq-archive \
--packages-directory released/packages \
.PHONY: opam
opam:
# Publish an opam description for menhir.
@ opam publish -v $(DATE) $(THIS).opam $(ARCHIVE)
# Patch coq-menhirlib.opam.
# We replace the string DATEDASH with $(DATEDASH).
# We replace the string DATE with $(DATE).
@ cat $(THAT).opam \
| sed -e 's/DATEDASH/$(DATEDASH)/g' \
| sed -e 's/DATE/$(DATE)/g' \
> $(THAT).patched.opam
# Publish an opam description for coq-menhirlib.
@ opam publish -v $(DATE) $(COQ_MENHIRLIB_PUBLISH_OPTIONS) $(THAT).patched.opam $(ARCHIVE)
@ rm $(THAT).patched.opam
# -------------------------------------------------------------------------
# Re-installing locally. This can overwrite an existing local installation.
.PHONY: pin
pin:
opam pin add menhir.dev .
.PHONY: unpin
unpin:
opam pin remove menhir
.PHONY: reinstall
reinstall:
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.
# -------------------------------------------------------------------------
# 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
MDFILES := *.md */*.md
.PHONY: mdl
mdl:
@ for f in $(MDFILES) ; do \
cp $$f $$f.bak && expand $$f.bak > $$f && rm $$f.bak ; \
done
@ mdl $(MDFILES)
HOWTO.md
View file @ 21741c6b
# Developer guide
# Developer Guide
This guide is intended for new Menhir developers, and should explain how
This guide is intended for new Menhir developers, and is supposed explain how
things work.
For the moment, there is not much information in it.
## How Menhir is Built
## Build Instructions
Menhir is built by `dune`. The build process takes place in several
stages:
There are two ways of recompiling Menhir after making a change in the sources.
* The library MenhirLib, whose source files reside in `lib`, is built.
This is the runtime support library for the parsers generated by
Menhir in `--table` mode.
To perform a single compilation pass, just go down into the `src` directory
and type `make`. This produces an executable file named `_stage1/menhir.native`.
* The library MenhirSdk, whose source files reside in `sdk`, is built.
This library allows reading automaton description (`.cmly`) files.
To go further and check that Menhir can process its own grammar,
still in the `src` directory,
type `make bootstrap`.
This produces an executable file named `_stage2/menhir.native`.
* A preliminary version of Menhir, referred to as "stage 1", is built.
In order to build Menhir's parser, `ocamlyacc` is used.
The parser and driver in `src/stage1` are used.
`make bootstrap` occasionally fails for no good reason. In that case,
use `make clean` before attempting `make bootstrap` again.
* The final version of Menhir, referred to as "stage 2", is built.
In order to build Menhir's parser, (the stage 1 version of) Menhir itself is used.
The parser and driver in `src/stage2` are used.
* As a sanity check, another version of Menhir,
referred to as "stage 3", is built.
In order to build Menhir's parser, the stage-2 Menhir is used.
The parser and driver in `src/stage2` are used again.
We check that a fixed point is reached, that is,
the stage-2 and stage-3 versions of Menhir
behave in the same way when applied to Menhir's grammar.
## Testing
To run Menhir's test suite, just go down into the `test` directory
and type `make test`. The package `functory` is required; install
it first via `opam install functory`.
To run all tests except the speed test, type `make test` in the root
directory.
To run the speed test, type `make speed` in the root directory.
The tests in the directory `test/static` test that Menhir seems to run properly,
but do not test the generated parser.
* The subdirectory `test/static/good` contains a number of correct `.mly` files.
We check that Menhir accepts these files and
compare the output of `menhir --only-preprocess` against an expected output.
We do not check that Menhir actually produces a working parser.
* The subdirectory `test/static/bad` contains a number of incorrect `.mly` files.
We checks that Menhir rejects these files
and produces the expected error message.
The tests in the directory `test/dynamic` test the generated parsers.
See the [README](test/dynamic/README.md) file there.
The demos in the directory `demos` also contain tests.
## Releasing
Prior to making a release, please take the following actions:
* Make sure `CHANGES.md` has been properly updated.
* Make sure that you are on the `master` branch and have
committed everything. No uncommitted files should remain.
* Run `make test` and `make versions` to make sure that Menhir can be compiled
and passes all tests under all supported versions of OCaml.
* Run `make speed` and have a look at the performance figures to
make sure that they are still in the right ballpark.
* Test the `opam` package by running `make pin`
(possibly in a dedicated switch, so as to avoid clobbering your
current installation of Menhir).
If `make pin` succeeds, then its effect can be undone by `make unpin`.
To create a release, run `make release`. This creates a release and commits it
to a fresh release branch. It also commits a copy of the documentation to the
master branch. The effects of this command are local; nothing is pushed or
published.
If you are happy with the outcome of `make release`, you can then proceed to
the following three steps:
* Run `make publish` to push the new release to `gitlab.inria.fr`.
The subdirectory `test/good` contains a number of correct `.mly` files.
The test suite checks that Menhir accepts these files and
compares the output of `menhir --only-preprocess` against an expected output.
It does not check that Menhir actually produces a working parser.
* Run `make export` to upload the documentation to Menhir's home page.
The subdirectory `test/bad` contains a number of incorrect `.mly` files.
The test suite checks that Menhir rejects these files
and produces the expected error message.
* Run `make opam` to create and publish a new `opam` package.
Some performance and correctness checks can be found in the directory `quicktest`;
see [quicktest/README](quicktest/README).
If you are not happy with the outcome of `make release`, you can undo it
by typing `make undo`.
## About the Module Ordering
......
INSTALLATION.md
View file @ 21741c6b
......@@ -2,46 +2,38 @@
## Requirements
You need OCaml 4.02 or later, ocamlbuild, and GNU make.
You need OCaml (version 4.02.3 or later) and `dune` (version 2.0 or later).
## Configuration Choices
### `PREFIX`
## Compilation and Installation
The value of the `PREFIX` variable can be changed to control where the software,
the standard library, and the documentation are stored. These files are copied
to the following places:
Compile and install as follows:
```
$PREFIX/bin/
$PREFIX/share/menhir/
$PREFIX/share/doc/menhir/
$PREFIX/share/man/man1/
make all # or: dune build @install
make install # or: dune install
```
`PREFIX` must be set when invoking `make all` and `make install` (see below).
The executable file `menhir` and the libraries `MenhirLib` and `MenhirSdk` are
installed by `dune`. `dune` usually figures out by itself where they should be
installed. If desired, a `--prefix` option can be passed to `dune`.
### `USE_OCAMLFIND`
## Coq support
The support libraries, `MenhirLib` and `MenhirSdk`, are installed either via
ocamlfind or directly in the directory `$PREFIX/share/menhir`. Installing via
ocamlfind is recommended (and is the default). It requires the `ocamlfind`
executable to be found in the `PATH`. An explicit choice can be made by setting
`USE_OCAMLFIND` to `true` or `false` when running `make all` (see below).
If you wish to use Menhir's Coq back-end,
which produces verified parsers,
then you must install the Coq library `coq-menhirlib`.
### `TARGET`
This is normally done via the following commands:
If your machine does not have the native code OCaml compiler (`ocamlopt`), but
does have the bytecode compiler (`ocamlc`), then you should define `TARGET=byte`
when running `make all` and `make install`.
## Compilation and Installation
```
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-menhirlib
```
Compile and install as follows:
The library can also be manually installed as follows:
```
make -f Makefile PREFIX=/usr/local USE_OCAMLFIND=true all
sudo make -f Makefile PREFIX=/usr/local install
cd coq-menhirlib
make
make install
```
If necessary, adjust `PREFIX`, `USE_OCAMLFIND` and `TARGET` as described above.
Makefile
View file @ 21741c6b
# This is the main Makefile that is shipped as part of the source package.
# Keep in mind that the hierarchy that is shipped is not identical to the
# hierarchy within the git repository. Some sub-directories are not shipped.
# The documentation (manual.pdf, menhir.1) is pre-built and stored at the root.
# This Makefile can also be used directly in the repository. In that case,
# the documentation and demos are not installed.
# The hierarchy that is shipped includes:
# demos
# menhir.1
# manual.pdf
# manual.html
# src
# Makefile (this one)
# ----------------------------------------------------------------------------
# The following variables must/can be configured.
ifndef PREFIX
$(error Please define PREFIX)
endif
ifndef TARGET
TARGET := native
endif
# ----------------------------------------------------------------------------
# By default, we attempt to use ocamlfind (if present in the PATH), but it
# is possible to prevent that externally by setting USE_OCAMLFIND to false.
# USE_OCAMLFIND is used only at build time (i.e., by "make all"). At
# (un)installation time, instead, we query menhir using --suggest-ocamlfind.
# This should protect us against people who pass USE_OCAMLFIND at build time
# and forget to pass it at (un)installation time.
ifndef USE_OCAMLFIND
USE_OCAMLFIND = ocamlfind ocamlc -v >/dev/null 2>&1
endif
# ----------------------------------------------------------------------------
# Installation paths.
# These may be overridden from outside; e.g., our opam package description
# provides its own values of docdir, libdir, and mandir.
bindir := $(PREFIX)/bin
docdir := $(PREFIX)/share/doc/menhir
libdir := $(PREFIX)/share/menhir
mandir := $(PREFIX)/share/man/man1
MANS := doc/menhir.1
DOCS := doc/manual.pdf doc/manual.html doc/manual*.png demos
# ----------------------------------------------------------------------------
# The following incantations should work on both Windows and Unix,
# and allow us to abstract away the differences.
# The extension of object files.
OBJ := $(shell ocamlc -config | sed -n '/^ext_obj:/p' | sed 's/ext_obj: //')
# The extension of executable files.
# Note: the field "ext_exe" seems to have appeared in OCaml 4.05.
# With earlier versions of OCaml, this incantation defines $(EXE)
# as the empty string, which could be a problem under Windows.
EXE := $(shell ocamlc -config | sed -n '/^ext_exe:/p' | sed 's/ext_exe: //')
# The OS type.
OS_TYPE := $(shell ocamlc -config | sed -n '/^os_type:/p' | sed 's/os_type: //')