Developing Gillian¶

Executing a command in the test environment¶

dune lets you execute a command in an execution environment where all built binaries and installed files are correctly added to your path. In particular, Gillian-JS, Gillian-C and wisl require to be executed in this environment to work correctly and find their runtime files.

To run any command under this environment:

dune exec -- <command>

To access the different manuals, you can use:

dune exec -- gillian-js --help
dune exec -- gillian-c --help
dune exec -- wisl --help

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

dune exec -- gillian-js verify --help

Rebuilding after modifications¶

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

You can automatically rebuild on changes by running:

dune build --watch

Code style¶

You can automatically format the code by running:

dune fmt

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
```
make 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
```
make docs-watch
```