Documentation/tutorial for ortac-stm plugin

[n-osborne]

This PR is based on #152 in order to have to latest warning messages.

[jmid]

Thanks for doing this documentation. Writing nice documentation is a lot of work - so this is much appreciated! :pray:

I suggest toning the following a bit down:

{2 QCheck-STM own limitations}

Finally, some limitations come directly from the QCheck-STM. There is not much
to do here except from testing the skipped function with another tool.

First of all, no other tools have been released so this suggestion is not helpfui.

In

a function should have exactly one type [SUT] in its signature, and it should be as argument.

one could support 0 or 1 arguments without hitting any QCheck-STM limitations AFAIK.

More broadly, one can encode "multiple ts" in QCheck-STM, by, say letting the SUT type be a stack of actual ts. That way

• init_sut should initialize the stack
• t-consuming operations pop ts from the stack (a precond can ensure that there is enough available)
• t-producing operations push their result to the stack.

So this isn't a limitation of QCheck-STM as it is reasonably customizable.

The second one is that higher order functions are not supported yet.

In multicoretests src/lazy/stm_tests.ml contains an STM example of doing so. It is thus a matter of emitting something along these lines from the plugin.

Let me stress again that putting in limitations to get a first version working is only natural. :100: :smiley: I furthermore applaud this effort to document the limitations! :tada:

I object to listing these under QCheck-STM own limitations and I challenge the claim that There is not much to do.

To make this constructive, a suggestion could be to rewrite this to just say

Please note, the current release of the plugin has the following limitations. We expect to address these in the future.

[n-osborne]

Thanks for the review :-)

I was not completely happy with this part, now I have an idea on how to modify it!

[shym]

Thank you for the updates, LGTM. CI is happy, so I merged.