ACGtk developper documentation

Building ACGtk

Please refer to the installation process description to install the required Opam environment (steps 1 to 3). Then, to compile ACGtk:

• Clone the git repository

  git clone https://gitlab.inria.fr/ACG/dev/ACGtk.git
  cd ACGtk

• Install the dependencies (since acgtk-browser lives in the same git repository, this will also install acgtk-browser dependencies)

  opam install --deps-only .

• Build the binaries (this will also build acgtk-browser)

  dune build

Documentation generation and releases

When a new commit is pushed to a branch, a pipeline is launched in Gitlab-CI to verify that the code successfully compiles. This also generates the documentation and deploys it on https://acg.gitlabpages.inria.fr/dev/ACGtk/$BRANCH_NAME.

With an empty branch name, this page lists all branches with a link to their respective documentation.

The links in the README.md file use the branch name release, so each new release should be pushed on this branch, in order to update the publicly available documentation. This branch should not be used otherwise, so that the documentation stays in sync with the last release.

How to update the grammars

The following instructions apply for the Menhir grammars in directories Scripting and Grammars and DatalogLib.

1. First, modify the Menhir file. Try to compile, if some conflicts arise, fix them and recompile until the grammar is correct.
2. Then, it will probably still fail to compile, because the file parserMessages.messages does not correspond to the new grammar. To get an updated version of this file, run dune promote. It will modify parserMessages.messages in the source tree. Then, try to compile again.
3. If it still fail to compile, it means that there are new error cases in the grammar. Some dummy error messages <YOUR SYNTAX ERROR MESSAGE HERE> have been generated by Menhir and need to be replaced by real error messages. Edit the file parserMessages.messages, then try to compile, this time it should work.

Testing before updating the messages

If you need to quickly modify and test the grammar multiple times, it would be a waste of time to update the error messages each time. To this avail, it is possible to disable all checks of validity of error messages by compiling with an other profile than the default dev, e.g. dune build --profile test. This will allow to build the executables without updating the error messages.

Internal Libraries

UtilsLib

The entry point of this library is the module: UtilsLib.

This module provides general purpose utilities.

Logic

The entry point of this library is the module: Logic.

This module provides λ-terms and types utilities (type-checking, reduction, etc.).

DatalogLib

The entry point of this library is the module: DatalogLib.

This module provides a Datalog implementation.

Library AcgData

The entry point of this library is the module: AcgData.

This module provides the data structures corresponding to the signature and lexicons notions of Abstract Categorial Grammars

Grammars

The entry point of this library is the module: Grammars.

This module provides lexers and parsers to parse .acg files. It also implements the acgc grammar compiler.

Scripting

The entry point of this library is the module: Scripting.

This module implements the top-level interpreter acg that provides commands to use grammars