Make the Gospel type-checker modular

[shym]

Currently, when the type checker encounters a dependency, it will load and type it on the fly. So common dependencies get type-checked over and over again, uselessly. It would be nice to modularize the type-checker so that typing a module requires the digested type information of its dependencies instead of retyping them. This could be done either with dedicated type files (see #376) or trying to piggy-back on current OCaml infrastructure by storing this information in standard files (it would be possible at least in .cmti files, by encoding the information as a special global attribute; could be done in cmi files?).

The expected benefits would be:

• improved performance,
• easier integration with the standard toolchain, if we manage to have gospel check abc.mli require the same files as ocamlc -c abc.mli.

[n-osborne]

Thank you @shym for raising this issue.

As we plan to soon use ortac on larger projects this is a good time to work on performance.

This would also remove some blockers for dune integration.

I've begun to experiment with different approaches:

• On my branch n-osborne/gospel#type-check-in-ppx I run the gospel type-checker before generating the corresponding documentation attributes. We can then store the gospel type checking information in the output of the ppx. Some remarks:

  • gospel type checking can't take any arguments (as it is in a ppx)
  • .cmi files don't keep the attributes at the signature level (Psig_attributes), if I'm not mistaken. They still are in the .cmti, so we are safe.
  • For dune integration, we still ask to run a source preprocessor when building the project. This is known to not compose well with other preprocessing, so the user is limited in this area. One workaround would be to ask the user to write the gospel specification in concrete attribute syntax.

• In #376 I make the gospel type checker store the typing information in a .gospel file. Again, some remarks:

  • The main motivation of this idea is to separate the actual OCaml compilation and the gospel type-checking: we don't need to ask dune to run the source preprocessor when building the project.
  • Gospel type-checking can take arguments (like the dependencies of the module)
  • Gospel type-checking (and production of the .gospel file) can be attached to any dune alias (@build, @runtest...) as the user see fit.
  • Parsing will still be done twice (for Ocaml compilation and for Gospel type-checking), this is not ideal, but I think it is still progress.

[shym]

• gospel type checking can't take any arguments (as it is in a ppx)

It can still grab info from environment variables, I expect, which could give us a way to feed it the information we need (namely the paths where to look for dependencies, or is there something else?).

[n-osborne]

You are right, this doesn't make this option impossible. I just think that it may make things a bit more delicate.

[n-osborne]

Modularizing the type-checker is expected to break how unicity of identifier is guaranteed in the current implementation. I've raised #381 for discussing this particular topic.