Developing Gillian#

Executing a command in the test environment#

esy lets you execute a command in a test environment where all built binaries and installed files are correctly added to your path. In particular, Gillian-JS, Gillian-C and wisl export specific environment variables that allow them to properly find their respective runtime files.

To run any command under this environment:

esy x <command>

To access the different manuals, you can use:

esy x gillian-js --help
esy x gillian-c --help
esy x wisl --help

You can get even more precise help about specific commands; for example:

esy x gillian-js verify --help

Rebuilding after modifications#

Since esy is our build system, running the esy command without any arguments will rebuild the project after modification.

You can automatically rebuild on changes by running:

esy watch

Code style#

You can automatically format the code by running:

esy format

It’s recommended that you install the provided git hooks (by running githooks/install.ml) to enforce code style.

We advise using the _intf trick where appropriate to avoid code duplication.

When you have a function that returns an option, and an extension-raising equivalent, you should name them foo and foo_exn respectively, rather than foo_opt and foo.

A rule of thumb for choosing whether to make a function argument labeled: is the argument’s purpose obvious from its type and the name of the function? If not, it should be labeled.

(* This doesn't need labels *)
val use_query: database -> query -> query_result

(* Wait, what's this weird first argument? Better make it labeled *)
val use_query: (string -> string) -> database -> query -> query_result

(* These arguments have the same type - how do I know which one is which? *)
val copy_content: channel -> channel -> unit

(* This is better *)
val copy_content : in:channel -> out:channel -> unit

Documentation#

Gillian’s documentation is built with sphinx, with an API reference generated using odoc.

Building Documentation#

Install the prerequisites

opam install odoc
pip install sphinx furo

Build the documentation
```
esy docs
```

After building, you’ll find the sphinx documentation at _docs/sphinx, and the API reference at _docs/odoc.

Rebuild on change#

If you want to automatically rebuild on changes, take these additional steps.

Install (more) prerequisites:

apt install inotify-tools
pip install sphinx-autobuild

Watch for changes
```
esy docs:watch
```