search

ocaml-gospel / ortac

Runtime assertion checking based on Gospel specifications
https://ocaml-gospel.github.io/ortac/
MIT License
36 stars 10 forks source link

Move to a module based configuration #214

Closed n-osborne closed 2 months ago

n-osborne commented 5 months ago

Fixes #173

This PR proposes to move from a command-line based configuration to a module-based configuration.

It does so adopting the proposition of this comment

It is in two folds: the first 17 commits change the way Ortac/QCheck-STM is configured and the next 4 commits update the Ortac/Dune plugin and the examples.

The changes in the Ortac/Dune module also integrate some sort of fix: the ortac dune qcheck-stm command now takes the actual filenames (that is with the extensions). I find it to be more natural.

n-osborne commented 3 months ago

Thanks for the review:

The typos should be fixed.

I've splited and reordered commits regarding sorting, removing and adding constructors for reserr errors.

Regarding the use of init_sut_txt, I've removed it from the config under construction but kept it in the actual config. It was added in c6b13f6e and I believe removing it here would make a bit too much noise. But I keep it in mind for the future.

Regarding renaming, you read correctly, I gave functions the name of the node of the OCaml AST they are inspecting, not making any assumption on the information they collect. In a future PR (I know, I'm thinking backward in time here...) the value_bindings function will also collect the optional cleanup configuration. Maybe some documentation could be enough?

On the importance of testing: I indeed misplaced the STM.ty extension in the testing configuration. Well spotted! Now that it is in the right place, OCaml compiler doesn't accept the generated code! I have to investigate that a bit more.

shym commented 3 months ago

Regarding renaming […] Maybe some documentation could be enough?

Yes, some documentation to explain what the functions extract would be fine too.

On the importance of testing: I indeed misplaced the STM.ty extension in the testing configuration. Well spotted! Now that it is in the right place, OCaml compiler doesn't accept the generated code! I have to investigate that a bit more.

:sweat_smile:

n-osborne commented 2 months ago

Thanks. Reordering pp_kind is indeed a good idea. Though there is a bit too much rebase work that it is worth to include the reordering to the Reordering warnings... commit, I add one near the end of the PR.

Waiting for the CI to be green again then merging.

shym commented 2 months ago

Just need reformatting.