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