From 506e072e03a0021956f46c496455056730715b0b Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Wed, 10 Apr 2024 15:13:30 +0200 Subject: [PATCH] Update README --- plugins/dune-rules/README.md | 26 ++++++++++++++++++-------- 1 file changed, 18 insertions(+), 8 deletions(-) diff --git a/plugins/dune-rules/README.md b/plugins/dune-rules/README.md index 2389278a..1b63ad65 100644 --- a/plugins/dune-rules/README.md +++ b/plugins/dune-rules/README.md @@ -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