Skip to content

Commit

Permalink
Update README
Browse files Browse the repository at this point in the history
  • Loading branch information
n-osborne committed May 16, 2024
1 parent 6b9257f commit 506e072
Showing 1 changed file with 18 additions and 8 deletions.
26 changes: 18 additions & 8 deletions plugins/dune-rules/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -20,18 +20,28 @@ plugins (the qcheck-stm plugin for now). You have to give it the option you want
pass to the other plugins and some more information for dune.

Let's say you want use the [Ortac/QCheck-STM] plugin on a module interface
`lib.mli` to generate QCheck-STM tests with the `lib_conf.ml` configuration, in
the context of the `pack` package.
`lib.mli` to generate QCheck-STM tests.

Then you can run:
The best way to use Ortac/Dune is in a dune stanza:

```shell
$ ortac dune qcheck-stm lib.mli lib_conf.ml lib_tests.ml --package=pack --with-stdout-to=dune.inc
```dune
(rule
(alias runtest)
(mode promote)
(targets dune.inc)
(action
(with-stdout-to
%{targets}
(run ortac dune qcheck-stm lib.mli))))
(include dune.inc)
```

to generate the dune rules to generate and run the tests. You can then include
`dune.inc` in the `dune ` file and the next time you run `dune runtest`, your
code should be tested using QCheck-STM.
This stanza assumes that you have written the configuration for
[Ortac/QCheck-STM] in a file named `lib_config.ml` and that the `Lib` module is
part of the `lib` library. It will write the generated tests in `lib_tests.ml`.
If you want more control, you can use the `--config` `--library` and `--output`
to give custom name to these files.

[Ortac/QCheck-STM]: ../qcheck-stm/README.md

Expand Down

0 comments on commit 506e072

Please sign in to comment.