Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Read gospel files #196

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
Open

Conversation

n-osborne
Copy link
Collaborator

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 n-osborne force-pushed the read-gospel-file branch 3 times, most recently from d0a9a54 to 17ef796 Compare January 24, 2024 16:23
@n-osborne n-osborne added this to the 0.2 milestone Feb 6, 2024
@n-osborne n-osborne force-pushed the read-gospel-file branch 4 times, most recently from 917435b to deb70ab Compare April 12, 2024 12:05
@n-osborne n-osborne modified the milestones: 0.2, 0.3 Apr 12, 2024
@n-osborne
Copy link
Collaborator Author

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

@n-osborne n-osborne force-pushed the read-gospel-file branch 2 times, most recently from c684ec4 to 953406c Compare June 6, 2024 10:17
@n-osborne n-osborne force-pushed the read-gospel-file branch 2 times, most recently from 9aeb63d to 8d537c0 Compare July 1, 2024 14:14
@n-osborne
Copy link
Collaborator Author

n-osborne commented Jul 1, 2024

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 n-osborne force-pushed the read-gospel-file branch 3 times, most recently from e9aa01e to acd4df3 Compare July 2, 2024 09:46
FIXME: generated code is broken on tuple translation
@n-osborne
Copy link
Collaborator Author

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

@n-osborne n-osborne removed this from the 0.3 milestone Jul 3, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant