Charlène_Gros

Unbound constructor error in Ortac-generated file

2

Ortac generated a file that did not include the constructor of the type `A` I created in the gospel (it should do the same for type `B`). ``` (*@ type...

Generate cleanup function with custom code

2

We use Ortac to test the implementation of `Mirage_kv`, a key-value store existing on a disk. To establish a connection to this disk, we utilise the interface of `Mirage_block`. If...

Parsing mistake of arrows from Gospel to Ortac in case of function declaration

1

When declaring the gospel model as a function `(string -> string option)`, Ortac misinterprets it and separates the operator `->`. It considers the arrow as a type constructor instead of...

Ortac could possibly generate a file without any commands

1

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...

Resuming Clément Pascutto's work to complete the implementation of the old operator in the wrapper plugin. This PR aims to address #201.

Users should be able to separate model definitions from the source file to make the instrumentation less invasive. An external model file also allows for easier integration of already wrapped...

The user should be warned if one of his functions is noted as a projection function (with `[@@model]`), but no gospel model has this name. For example, the following type,...