Skip to content

Latest commit

 

History

History
122 lines (88 loc) · 4.96 KB

HOWTO.md

File metadata and controls

122 lines (88 loc) · 4.96 KB
Raw

Developer Guide

This guide is intended for new Menhir developers, and is supposed explain how things work.

How Menhir is Built

Menhir is built by dune. The build process takes place in several stages:

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

  • The library MenhirSdk, whose source files reside in sdk, is built. This library allows reading automaton description (.cmly) files.

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

  • 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 all tests, type make test in the root directory.

To run the benchmarks, type make benchmarks 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 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 and coq-menhirlib/CHANGES.md have 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 demos and make versions to make sure that the tests succeed and that Menhir can be compiled under all supported versions of OCaml.

  • Run make benchmarks 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.

  • Run make export to upload the documentation to Menhir's home page.

  • Run make opam to create and publish a new opam package.

If you are not happy with the outcome of make release, you can undo it by typing make undo.

About the Module Ordering

Some toplevel modules have side effects and must be executed in the following order:

Module Task
Settings parses the command line
PreFront reads the grammar description files
TokenType deals with --only-tokens and exits
Front deals with --depend, --infer, --only-preprocess, and exits
Grammar performs a number of analyses of the grammar
Middle deals with --random-sentence and exits
Lr0 constructs the LR(0) automaton
Slr determines whether the grammar is SLR
Lr1 constructs the LR(1) automaton
Conflict performs default conflict resolution and explains conflicts
Interpret deals with --interpret and exits
Freeze deals with --list-errors, etc. and exits
Invariant performs a number of analyses of the automaton
Back produces the output and exits

It is particularly important to note that conflict resolution, performed inside Conflict, alters the LR(1) automaton.

A few artificial dependencies have been added in the code in order to ensure that this ordering is respected by dune. This is admittedly not very pretty and should be fixed someday, but that may be trickier than it seems.