ocaml-gospel / ortac

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

Generated test file uses wrong module path #268

Open OlivierNicole opened 1 week ago

OlivierNicole commented 1 week ago

How to reproduce

Unpack test_int31.tar.gz and:

$ cd test_int31 
$ ortac qcheck-stm int31.mli ortac_conf.ml -o test_int31.ml
File "int31.mli", line 19, characters 0-22:
19 | val show : t -> string
     ^^^^^^^^^^^^^^^^^^^^^^
Warning: Skipping show: functions without specifications cannot be tested.
$ dune build ./test_int31.exe
File "test_int31.ml", line 4, characters 5-10:
4 | open Int31
         ^^^^^
Error: Unbound module Int31
Hint: Did you mean Int32?

The problem here is that given the Dune structure of my project, I would need Ortac to generate open Int31lib.Int31 at the top, instead of open Int31. Is there a way to fix this?

n-osborne commented 1 week ago

Thanks for raising this issue.

Indeed, we've not worked yet on handling non trivial library/module setup. In the examples folder, I've used some awk script to put things as Ortac/QCheck-STM expects them to be.

So at the moment, I'm afraid I don't have any other solution than a hackish one, like running a sed script on the generated code...

But I believe that a configuration feature like module-prefix could be handy in a number of cases.

n-osborne commented 1 week ago

I believe that version could do the trick.

$ dune exec --display=quiet -- ortac qcheck-stm ../test_int31/int31.mli ../test_int31/ortac_conf.ml --module-prefix=Bob --quiet | head
(* This file is generated by ortac qcheck-stm,
   edit how you run the tool instead *)
[@@@ocaml.warning "-26-27-69-32-38"]
open Bob.Int31
module Ortac_runtime = Ortac_runtime_qcheck_stm
let in_range i =
  try
    let __t1__001_ =
      Ortac_runtime.Gospelstdlib.(<=)
        (Ortac_runtime.Gospelstdlib.(~-)

What do you think?