ocaml-gospel / ortac

Runtime assertion checking based on Gospel specifications
https://ocaml-gospel.github.io/ortac/
MIT License
37 stars 10 forks source link

ortac-dune plugin #190

Closed n-osborne closed 7 months ago

n-osborne commented 9 months ago

Plugin to generate dune rules for other plugins.

n-osborne commented 9 months ago

Still in draft as the plugin does not load...

n-osborne commented 9 months ago

I've put a no-changelog-needed label as this is a new not-yet-released-plugin.

n-osborne commented 8 months ago

Thanks for these remarks. 1 and 2 are just relics from the past, I'll remove them. I also agree with 3. I was wondering about a better user interface (there are a lot of arguments to give). The --include=... is easy to share and use in this plugin, and it makes a lot of sense. I am wondering about the output files, because we have two of them: the output_file option to give ortac qcheck-stm and the one to write the dune rules in. On the one hand, it doesn't make a lot of sense (I think) to have dune rules without an output file for the generated OCaml code: we want to be able to run the generated tests. On the other hand, it is easy to have to optional argument for output files: the --output=... from ortac-core for the generated OCaml code and something like --dune-output=... for the generated rules.

n-osborne commented 8 months ago

I'm also thinking about making the package argument optional.

shym commented 8 months ago

Good point, I was thinking about ortac qcheck-stm optional arguments which should stay optional, but not about the ones that should be required :sweat_smile:

shym commented 8 months ago

Do you know whether it would be possible to make an interface such as:

ortac dune -o dune.inc qcheck-stm -o ...

with cmdliner?

n-osborne commented 8 months ago

I'm guessing it is not. Here qcheck-stm is a subcommand of (the ortac's subcommand) dune. So it is build with Cmd.group which takes a Cmd.t list, but no argument terms.

n-osborne commented 8 months ago

I've renamed the --output option to --with-stdout-to to make it clearer and avoid confusion with the --output option of ortac qcheck-stm.

n-osborne commented 8 months ago

I should get rid of the ugly empty line generated where an optional argument is absent (see line 25 of the cram test).

n-osborne commented 7 months ago

Thanks for the review!

I think I've cover all of your remarks but one: the use of a functor. I totally agree that having to file that just differ by a module that is opened in them is not ideal. That being said, using a functor will bring some complexity to the dune rules:

I'd propose to postpone this feature (easy support of included files for testing functor instantiation) in order to have a clean way of dealing with them.

Also, putting the body of the current included file in a functor, abstracting over the opened file does not work out of the box: I still have an error on the type extension that I don't manage to fix for now:

File "examples/make_varray_incl.ml", line 24, characters 2-39:
24 |   type _ ty += Elt : 'a ty -> 'a elt ty
       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: In this definition, a type variable cannot be deduced
       from the type parameters.
shym commented 7 months ago

Thank you for the fix. CI is happy so I merge it.