Improve failure message

[n-osborne]

This PR improve the state of #188

This PR is based on #197, please consider only the last 7 commits.

Basically, this PR makes postcond return the reason of the failure rather than just a boolean, so that we can print the Gospel terms being violated back to the user in case of failing test.

This lead to give another implementation of the STM_Sequential.Make functor in a new Ortac_runtime_qcheck_stm package to use this new postcond function and build and pass to QCheck the new failure message.

[n-osborne]

For demo purpose, I have pushed this branch with a failing test.

You can then see (with colours):

λ dune build @launchtests
File "plugins/qcheck-stm/test/dune.inc", line 49, characters 0-75:
49 | (rule
50 |  (alias launchtests)
51 |  (action
52 |   (run %{dep:array_stm_tests.exe} -v)))
random seed: 476198396
generated error fail pass / total     time test name
[✗]    1    0    1    0 / 1000     0.0s Array STM tests (generating)

--- Failure --------------------------------------------------------------------

Test Array STM tests failed (7 shrink steps):

   length


+++ Messages ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

Messages for test Array STM tests:

Gospel specification violation in function length

  File "array.mli", line 7, characters 12-18:
    i = 42
  
  File "array.mli", line 8, characters 12-26:
    i = t.size + 1
  
when executing the following sequence of operations:

  length : 16

================================================================================
failure (1 tests failed, 0 tests errored, ran 1 tests)

[shym]

Nice work, congratulations!
I confess that I didn’t carefully review the generated code 😅 but this looks all good to me.

Three small questions/remarks:

• I assume you went with (++) to get it infix in the generated code? I think I would prefer the fully-qualified call, just like what is done for all the Gospel operators. And I would suggest picking a different one, to avoid the confusion with Gospelstdlib.(++).
• This is really quibbling: I noticed various uses of @\n, which is better avoided according to Format’s documentation. Did you try alternatives (thinking it might make the generated output a bit more robust)?

[shym]

Typo: “providede“

[n-osborne]

Thanks!

• I assume you went with (++) to get it infix in the generated code? I think I would prefer the fully-qualified call, just like what is done for all the Gospel operators. And I would suggest picking a different one, to avoid the confusion with Gospelstdlib.(++).

Yes, I went for the infix operator to avoid things like (append (append x y) z) but the risk of confusion with another function is a good reason to not do that. And if we don't have the infix notation because we qualify (which is reasonable), no reason to not adopt append.

• This is really quibbling: I noticed various uses of @\n, which is better avoided according to Format’s documentation. Did you try alternatives (thinking it might make the generated output a bit more robust)?

This is the end-of-line that is mostly used in the project I think. Maybe we can change it with consistency in the whole repo if we find a better candidate.

[n-osborne]

CI is green, merging.
Thanks for the review @shym :-)