OCaml compiler reports error on code generated by the preprocessor when the attribute is not at an acceptable location

[shym]

Given the following source file middle.mli with a Gospel specification appearing at an improper location (in the middle of a type):

# 1 "middle.mli"

val f : int ->
(*@ x = f y *)
int

the user will see an error reported against the generated part of the file:

$ ocamlc.opt -pp "_build/install/default/bin/gospel pps" middle.mli
File "middle.mli", line 3, characters 0-3:
3 | [@@gospel
    ^^^
Error: Syntax error

It would be nicer to be able to detect such cases and turn them into a [@@@ocaml.warning similar to OCaml warning 50.

[n-osborne]

Maybe we should use the [@@@ocaml.ppwarning] attribute. It is documented as the one to use in preprocessor.

gospel pps should then turn the middle.mli file into something like:

# 1 "middle.mli"

[@@@ocaml.ppwarning "Gospel specification in the wrong place"]
# 3 "middle.mli"
val f : int ->
(*@ y = f x *)
int

And we will have:

$ ocamlc.opt middle.mli
File "middle.mli", line 2, characters 20-61:
2 | [@@@ocaml.ppwarning "Gospel specification in the wrong place"]
                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 22 [preprocessor]: Gospel specification in the wrong place

[shym]

Indeed, well spotted!

[shym]

Sidenote: unfortunately, ppwarning will trigger a warning during OCaml typing, not parsing. And gospel relies only on parsing. So if we generate such a warning, it won’t appear in a gospel check. :thinking: