search

ocaml-gospel / gospel

A tool-agnostic formal specification language for OCaml.
https://ocaml-gospel.github.io/gospel
MIT License
128 stars 16 forks source link

Run tests on the new example #362

Closed shym closed 6 months ago

mariojppereira commented 1 year ago

Hi @shym and @n-osborne, sorry for my (very) late answer. Actually, I was thinking about the folder examples to be a sort of repository for "ongoing" case studies. This means you can use put there gospel specification that does-not-even-yet type-checks. So, I guess always running sanity tests on these examples might not be the best idea.

Maybe I should try to hide this folder, or maybe give it a more suggestive name?

n-osborne commented 1 year ago

Thanks @mariojppereira.

Indeed, as a newcomer, a folder named examples would be the first place I look to learn how to write correct specifications. And I really think it is a very good idea to have that :-)

For specifications that are not (yet) corrrect, the test/issues folder may be a good place? We added it with @shym some time ago to track tests related to github issues (or at least, that was the idea, not completely sure we have been thorough with that).

Another idea would be an experiment folder (maybe test/experiment?).

shym commented 1 year ago

I agree a different name would be better for WIP specs. I don’t mind that directory being visible as long as its purpose is clear (by its name and by a README). Even for WIP specs where the typechecker will (initially) fail, I think it is important to keep track of it. Note that the tests we run do not require the file to type-check, but will just add a prologue with the gospel check error if any. This will be useful to help develop the typechecker to cover those new cases.

n-osborne commented 6 months ago

Long overdue. Merging.