Ortac could possibly generate a file without any commands

As a new user of Gospel and Ortac, I would have found it helpful to be able first to write an almost empty file with only type definition and make function without any commands. For now, Ortac requires at least one command to generate a valid OCaml file. Considering the following interface file.

type t
(*@ model bla: integer *)

val make: unit -> t
(*@ t = make u
    ensures t.bla = 0 *)

Because Ortac does not detect the absence of commands, it generates an incorrect file with an unclear error.

9 |     type nonrec state = {
        ^^^^
Error: Syntax error

Ortac should crash before if it does not meet all the requirements in the interface instead of generating an invalid file.

Nevertheless, it might be nice to allow users to produce a very first Ortac-generated file with only make to ensure everything is well set up, even if Ortac is doing nothing. What do you think?

Thanks!

The error comes from the fact that the function show_cmd is placed before the type nonrec state in the generated file and that the former has an empty pattern matching, which is syntactically incorrect:

$ cat > foo.mli << EOF
> type t
> (*@ model bla: integer *)
> 
> val make: unit -> t
> (*@ t = make u
>     ensures t.bla = 0 *)
> EOF
$ ortac qcheck-stm foo.mli "make ()" t | head -n 12
(* This file is generated by ortac qcheck-stm,
   edit how you run the tool instead *)
[@@@ocaml.warning "-26-27"]
open Foo
module Ortac_runtime = Ortac_runtime_qcheck_stm
module Spec =
  struct
    open STM
    type sut = t
    type cmd = |
    let show_cmd cmd__001_ = match cmd__001_ with
    type nonrec state = {

There may be two reason why the type cmd is empty:

as you say, the user is still in the process of writing the specification and he/she just want to check that the specification for the function used for init_state is understandable by Ortac/QCheckSTM
non of the specification for the functions of the module fit the Ortac/QCheckSTM requirement to generate the functions necessary for QCheckSTM tests

In the former case, Ortac/QCheckSTM will emit a warning and fail to generate any file:

$ cat > foo.mli << EOF
> type t
> (*@ model bla: integer *)
> 
> val make: unit -> t
> (*@ t = make u *)
> EOF
File "foo.mli", line 5, characters 3-15:
5 | (*@ t = make u *)
       ^^^^^^^^^^^^
Error: Unsupported INIT function make: the specification of the function
       called in the INIT expression does not specify the following fields of
       the model: bla.

Same if the specification of the type used for sut are not enough for Ortac/QCheckSTM.

The second case is why I would be relunctant to generate a file that compiles with an empty cmd type: the user can then think that the module is well tested! I know there are some warning when ortac skip a function, but there is also a --quiet flag!

I rather add an error Empty_cmd_type in Reserr and fail the same way than above (for make function).

ocaml-gospel / ortac

Ortac could possibly generate a file without any commands #213