Issues from a first-time user

[jmid]

I've just tried out the Ortac qcheck-stm plugin, taking baby steps to write a Queue specification. My efforts are in https://github.com/jmid/ortac/tree/add-queue where I mimicked the hashtbl test's files and dune rules.

When developing these I used the following invocation to get error messages

ortac qcheck-stm test/queue.mli "create ()" "char t" -o /tmp/queue_stm_tests.ml

and afterwards a dune build @launchtests or a direct invocation of _build/default/plugins/qcheck-stm/test/queue_stm_tests.exe -v to invoke the extracted tests.

There are 4 commits in there - here's feedback for these 4 steps from yours truly: a naive, well-intending, first-time user from hell :smile:

1. In c942852 - First version with wrong Not_found exception - as an end-user I was missing some information as to what call sequence caused the exception:

   
   random seed: 12175242
   generated error fail pass / total     time test name
   [✗]    0    0    0    0 / 1000     0.0s STM Lib test sequential

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

Test STM Lib test sequential failed:

ERROR: uncaught exception in generator for test STM Lib test sequential after 1000 steps: Exception: Failure("tl") Backtrace:

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

2. In 0bde84b - Right exception, but syntax error on parenthesis - I used not unreasonable syntax (I think) which was rejected:

File "test/queue.mli", line 16, characters 11-12: 16 | raises (Failure _) -> q.contents = [] ^ Error: Gospel error: Syntax error.

3. In bb57690 - Right exception, but this raises Fatal error: exception Failure("tl") - I was again missing some information as to what call sequence caused the exception:

jmi@MintPad:~/software/ortac/plugins/qcheck-stm$ ../../_build/default/plugins/qcheck-stm/test/queue_stm_tests.exe -v random seed: 363694356 generated error fail pass / total time test name [ ] 0 0 0 0 / 1000 0.0s STM Lib test sequential (generating)Fatal error: exception Failure("tl")

4. In 4263acb - This yields a warning about contents declared as modified, but with no translatable ensures clause... - I tried rewritting my spec into something more pure, but was missing feedback as to why the suggested spec was not translatable.

[jmid]

For 4. I realize now that running the Gospel tool itself might have helped me. Is that the proposed tool cycle: run gospel file && ortac ...options... file? If so, could one consider invoking Gospel from Ortac, so that end-users would only have to invoke one command?

[shym]

Thank you for your feedback, that’s very helpful!

1 and 3: Very good point! The Ortac runtime implements Gospelstdlib.List.tl (and all such partial functions) by using the equivalent OCaml function. Maybe we should implement them so that they report an Ortac-specific exception that makes it easier to understand that the specification was partial and should be fixed. :thinking:

2: I agree. I’ve been advocating for using an OCaml-compatible syntax in order to reuse the OCaml parser.

4: Hopefully, the tutorial will guide users into writing it as necessary :sweat_smile:

For 4. I realize now that running the Gospel tool itself might have helped me.

I’m not sure I follow what you are referring to: Ortac does start by running the Gospel typechecker (if only because it is using its typed AST) and that’s why it reports: Gospel error: ... with the error message as produced by the typechecker.

[jmid]

For 1. and 3. a Partial function application failed exception would help indeed. That the exception is raised during generation (which should be pure in STM) in 1. and also 3. is the reason why no cmd is printed I think. I'm not sure what would be a good fix for it though... :thinking:

2: I agree. I’ve been advocating for using an OCaml-compatible syntax in order to reuse the OCaml parser.

Fair enough :+1:

4: Hopefully, the tutorial will guide users into writing it as necessary 😅

I would expect an error message telling me which ensures clause part is not translatable, no? The tutorial should certainly help - but it shouldn't replace informative error messages?

[n-osborne]

Thanks again for the indeed very helpful feedback :-)

Regarding 4, I think that translatable is a bit confusing as the problem is not that a specific Gospel clause is not translatable into OCaml, but rather that there is not one clause that is suitable to generate the next_state case.

152 proposes a new warning message with better terminology (I hope) and a bit more explanation about what the tool expect to find in one of the ensures clauses.

[jmid]

Nice - I can see I completely misunderstood the original error message :grimacing: I think #152 is a nice improvement! :tada:

[jmid]

BTW, I have a QCheck-STM WIP patch to give a more useful error message on exceptions during next_state. This should let us print a call sequence in 1. and 3.

[jmid]

FYI, ocaml-multicore/multicoretests#400 has been released with version 0.3 of qcheck-stm https://github.com/ocaml-multicore/multicoretests/releases/tag/0.3 so a fresh install should give a more informative error message in 1. and 3. :slightly_smiling_face:

[jmid]

AFAICS, a number of improvements have come out of this experience report: :tada:

• an improved error message
• an upstream qcheck-stm improvement to print a failing cmd
• a dedicated partial function application exception

I'll close it now though, as I don't think we can get more out of it.