Documentation/tutorial for ortac-stm plugin

[n-osborne]

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

[shym]

This is a nice first draft, well done! I’m looking forward to seeing the complete version 😄

[shym]

Is that required? It’s the default behaviour, I think.

[shym]

In that case, the checks clause will be tested to check the function did raise an exception.

[jmid]

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

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. 💯 😃
I furthermore applaud this effort to document the limitations! 🎉

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]

This reads very nicely, thank you!

I’ve added 4 commits containing fixes and suggestions in my stm-plugin-documentation-plus branch. They are separate commits to help you review my proposed changes (the one for typos should really be reviewed with --color-words!) but they would be better squashed in after.
I’ve also noticed that example_ghost doesn’t contain what it is supposed to, I think.

[shym]

The example is called example_ghost.mli but this is not what it illustrates, so I’m a bit confused here. It was overwritten with the content of example_incompatible_type, it seems.

[shym]

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