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
```