Ortac could possibly generate a file without any commands
Closed this issue · 1 comments
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).