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

Read gospel files #196

Open n-osborne opened 7 months ago

n-osborne commented 7 months ago

This PR proposes to use the gospel (yet unmerged) new feature from #376.

Some refactoring is done a long the way (there may be room for more, but I was mainly interested - at least at first - in experimenting and see how to use the new features in the examples.

This PR only add reading the .gospel files for the qcheck-stm plugin, as it is an experimentation. But this allows to see how it goes with the dune rules in the examples/ directory.

Note that this PR is also based on #380.

n-osborne commented 3 months ago

Rebased on #218, please consider only the last six commits.

n-osborne commented 1 month ago

This PR could also include an update of the dune plugin to make it read the gospel file.

Edit: let's do that in another PR.

n-osborne commented 1 month ago

Apparently, reading from the pre-checked .gospel file generate incorrect code (at least for tuples). Postponing this feature to 0.4.0 or later.