diff --git a/plugins/dune-rules/doc/dune b/plugins/dune-rules/doc/dune new file mode 100644 index 00000000..88e5eb4f --- /dev/null +++ b/plugins/dune-rules/doc/dune @@ -0,0 +1,2 @@ +(documentation + (package ortac-dune)) diff --git a/plugins/dune-rules/doc/index.mld b/plugins/dune-rules/doc/index.mld new file mode 100644 index 00000000..d0ed29b1 --- /dev/null +++ b/plugins/dune-rules/doc/index.mld @@ -0,0 +1,56 @@ +{0 Ortac/Dune} + +{1 Overview} + +The [dune] plugin for [ortac] (called Ortac/Dune in order to avoid ambiguities) +generated the dune rules necesary to use other plugins. + +On the command line side, Ortac/Dune plugin provides a [dune] subcommand for +the [ortac] tool. But the [dune] subcommand has also subcommands related to the +other plugin. + +{1 [qcheck-stm] subcommand} + +For now, only the Ortac/QCheck-STM plugin is supported. So the only subcommand +available is [qcheck-stm] and the full command, without the argument yet, is: + +{@shell[ +$ ortac dune qcheck-stm +]} + +This will in turn takes some arguments. The first arguments it takes are the +argument to feed the [ortac qcheck-stm] command. The only difference is that +the output for the generated OCaml code is not optional. The [--include] +argument is still optional though. In addition to the specific [qcheck-stm] +arguments, there are two optional arguments specific to the [dune] subcommand. +You have the possibility to specify a package and the name of the file to write +the dune rules to include in your [dune] file. + +So, to sum up: + +{ol {- name of the file containing the Gospel specifications} + {- the INIT_SUT function} + {- the SUT type} + {- the filename for Ortac/QCheck-STM output} + {- [--include] optional argument for Ortac/QCheck-STM} + {- [--package] optional argument for Ortac/Dune} + {- [--with-stdout-to] optional argument for Ortac/Dune}} + +Note the if you want to use this plugin to generate your tests, you will need +to give a value to the [--with-stdout-to] optional argument. This argument is +optional only to allow experimenting with the command line and read the +generated dune rules in the standard output rather that in a file. The usual +name for such a file is [dune.inc]. But if you have to generate test rules for +multiple files, you'll have to come up with other names. For example, if you +want to generate test rules for the two files [a.mli] and [b.mli], you may want +to use [dune.a.inc] and [dune.b.inc]. + +Once you are happy with the generated rules and they are written in a file, +you'll have to include this file in the [dune file] for your tests using the +[(include )] stanza. Then [dune runtest] will generate the QCheck-STM +files according to the Gospel specifications and run them. + +As a bonus, the generated dune rules also contain the rule to generate +themselves, that is a rule for runnong the Ortac/Dune plugin with the provided +arguments. So you can edit this rule to modify how Ortac/Dune is called. +