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.

Sign up for GitHub

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

Jump to bottom

Automate proof verification in tests #3

Open
pascutto opened this issue Oct 18, 2021 · 3 comments
Open

Automate proof verification in tests #3

pascutto opened this issue Oct 18, 2021 · 3 comments
Assignees
@mariojppereira

Comments

@pascutto
Copy link
Contributor

We have tests checking that specifications are well-formed since #2, but no tests check that the proofs are still accepted (by coq, why3, ...). That should be part of dune runtest.
@pascutto pascutto mentioned this issue Oct 18, 2021
Merged
2 tasks
@mariojppereira mariojppereira self-assigned this Oct 18, 2021
@mariojppereira
Copy link
Contributor

mariojppereira commented Oct 19, 2021 •
edited
Loading

This means Vocal always depends on Why3 and Coq. Is this the intended use for the library? I mean, I am okay with rechecking the proofs, but for someone who wishes only to use the library wouldn't this be overkill?

@pascutto
Copy link
Contributor Author

This means Vocal always depends on Why3 and Coq.

Not always, just for tests, so users don't have to install them :)

@mariojppereira
Copy link
Contributor

Okay, understood :)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@mariojppereira mariojppereira

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@mariojppereira @pascutto