search

ocaml-gospel / gospel

A tool-agnostic formal specification language for OCaml.
https://ocaml-gospel.github.io/gospel
MIT License
123 stars 16 forks source link

Make type checker save type information #376

Closed n-osborne closed 5 months ago

n-osborne commented 7 months ago

This PR proposes to marshall the product of the type checker and save it in a file with the .gospel file extension so that external tool does not have to run the type checker by themselves.

n-osborne commented 6 months ago

Thank you @shym for your comment :-) I've integrated your two commits and, following your suggestion, made gospel check handle .gospel files and test that reading back the typing information from a .gospel file give the same output than typing from the initial .mli file.

n-osborne commented 5 months ago

Thanks. Merging.