Parsing interfaces that use external modules with Gospel

Community
,
1

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.

1 Like
2

First, thank you for trying Gospel and hacking on Ortac!

I’m very curious about your new Ortac plugin!

As you are working on Ortac I believe you are using gospel.0.3.0 (the dev
version is not compatible with Ortac for now and is a complete rewrite of gospel
typechecker). So I will only refer to this specific version.

Here is what I can say after a quick inquiry.

How Gospel handles opens (or qualified symbols) is far from ideal and mainly
targets the OCaml standard library.

What happens is that when Gospel cross an open (or a qualified symbol), it
will look up its environment, and if it is a new module name, it will try to
locate it either in the OCaml standard library or in the loadpath variable.

You can add directories to the loadpath using the --load-path cli option, or
in the first argument of Ortac_core.Utils.type_check (ortac cli doesn’t
have a --load-path cli option, but it should be easy to add).

Now the problem is that Gospel uncapitalizes the name of the module to find the
.mli file, but here we want to open the QCheck.mli file (capitalized). So
Gospel should be patched to look both the uncapitalized and the original name
(in the Typing.open_file function).

After that, we still end up with an error (a crash actually) because somewhere
when inspecting QCheck.mli it encounters an extensible type (I haven’t found
where exactly though, but most likely in a dependency). Here, patching Gospel
would be a bit more involved, I don’t have a solution at the top of my head.
And as it is being rewritten I’m not sure it is worth it.

Is your Ortac plugin already working except for the generator deriving? If no,
I would suggest to continue experimenting without the use of
ppx_deriving_qcheck for now (sorry, it is a bit unsatisfactory) and see if we
can come up with a solution to this problem later.

3

Thanks for the detailed reply, good to know I’m not missing something completely.

The plugin I’m working on is mostly an exercise in getting to know Ortac and Gospel, with the rough goal of making an alternative to qcheck-stm for pure functions with as little setup overhead as possible. I think it would be really cool to push the boundaries of what property based checking can do, with regards to quantification and more complex Gospel specs.

That being said, I do have a base I can work with, putting the PPX integration on hold. I noticed the recent development on Gospel and figured I’d be waiting :slight_smile: . Did you have any reservations about something akin to a ‘gospel ignore’ annotation in interfaces? To me it seems pragmatic to allow Gospel to skip certain signatures as long as they aren’t dependencies within any other specs, but maybe that comes with a sacrifice I’m not aware of.

I’ll check out the open issues on the projects, but if you know of any other communication channels for this type of formal verification-adjacent OCaml work I’d be really interested in helping out where I can.