Parsing interfaces that use external modules with Gospel

[bord-o]

Right now I’m experimenting with a new Ortac plugin, but I’m running into some limitations with gospel. Say I have an interface that needs to expose some code using an external dependency (qcheck generators in this case):

`type custom

val gen_custom : custom QCheck.arbitrary
(* gospel check custom.mli will fail on this definition *)

val id_custom : custom -> custom
(@ custom2 = id_custom custom1
ensures custom2 = custom1)`

I would expect that this would be checked by gospel just fine given the problematic line has no annotations, but instead it fails: ‘Error: No module with name QCheck’.

Is there any way that I can work around this, by way of configuring gospel to ignore certain definitions or otherwise? I couldn’t find anything in the documentation about this. It seems that the ortac-qcheck-stm plugin gets around this issue by including generators in a separate module that defines some other configuration, but I’m looking to take advantage of ppx_deriving_qcheck to make things a bit more user-friendly for pure functions, which will result in the generators being in the same module that is under test.

Any insight here would be really appreciated, this is cross posted in the ocaml forum.