ocaml-gospel / gospel

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

Pre-processor bug #393

Closed ionchirica closed 4 months ago

ionchirica commented 4 months ago

Hi,

When the pre-processor tries to match Gospel keywords, it does not take into account white spaces afterwards and so specifications such as:

val function_example : int -> int
(*@ function_example 0 *)

Are not accepted by Gospel as it thinks that function_example matches the function keyword.

n-osborne commented 4 months ago

Thanks! Good catch!

Feel free to make a PR to add this test case to the issue directory (or even to fix it if you feel like it). Note that when fixed, there will be a second syntax error in your example as you give a constant in the gospel header.

A bit off topic but as it is on the same line of code: this made me look again at the pps.mll file and I've spotted that there is the val keyword for introducing ghost declaration. I believe this is a relic of a previous version of the language as it is used in the vocal tests and in just one example from the walkthroughs/union-find.md documentation file but not really documented as a keyword introducing a ghost value.

I'm not sure we want to keep it, as there is no appearent distinction with function and we're already wondering whether to keep predicate in #391.

n-osborne commented 4 months ago

Closed by #394