Nicolas Osborne

Results 44 comments of Nicolas Osborne

This PR is based on #214, please consider only the last 5 commits. Edit: 6 last commits

Rebased on #218, please consider only the last six commits.

This PR could also include an update of the dune plugin to make it read the gospel file. Edit: let's do that in another PR.

Apparently, reading from the pre-checked `.gospel` file generate incorrect code (at least for tuples). Postponing this feature to 0.4.0 or later.

(Discussed offline with @shym) The configuration module could contain an implementation of `init_state` for the cases where it is not possible to generate it from the specifications. We should have...

More thoughs about what the configuration module should look like. The idea i snow to completely get rid of passing information other than this module's name through the command-line: that...

Note to myself: I need to add the equivalent optional argument to Ortac/Dune plugin.

Converting to draft as it is not up to date with the module-based configuration from #214