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

gospel pps still detaches some documentation attributes #324

Closed n-osborne closed 1 year ago

n-osborne commented 1 year ago
$ cat > foo.mli << EOF
> (** documentation *)
> (*@ function f : (i : integer) : integer *)
> EOF
$ ocamlc -dsource -pp "gospel pps"
[@@@gospel {| function f : (i : integer) : integer |}]

The documentation comment should be turned into a documentation attribute by gospel pps.

shym commented 1 year ago

Enabling warnings with -w +a, I get:

File "/tmp/ocamlppea01be", line 1, characters 0-8:
Warning 50 [unexpected-docstring]: unattached documentation comment (ignored)
[@@@gospel {| function f : (i : integer) : integer |}]

In such a case, we might follow what OCaml does and generate something like:

[@@@gospel {| function f ... |}[@@ocaml.doc " documentation "]]

even if it is not clear yet to me what the ppx should do with the nested documentation to get it exploitable with odoc.