Add synterp phase support for derive plugins.

[rlepigre]

This was developed and tested against our own derive commands (included in this branch). It would probably make sense to test this in the repo somehow though, maybe by adding a new deriver that creates some kind of module?

CC @Janno.

Edit:

We had to require a synterp phase for all derivers since we need to know about all of them upfront (the dep1 arguments are not enough to compute the full list, since independent derivers have no dep1). This does not seem too bad though.

We tweaked the module wrapping behaviour of derive in the following way:

• Using derive Inductive ty := ... does not automatically create a module ty anymore.
  • The original behaviour can be recovered with #[module] derive Inductive ty := ....
  • A module name can be specified with #[module="Ty"] derive Inductive ty := ....
• A custom prefix can be configured with the prefix (string) attribute.
• When a wrapper module is generated, the no_alias (boolean) attribute can be used to avoid generating alias notations.

[gares]

• Using derive Inductive ty := ... does not automatically create a module ty anymore.

  • The original behaviour can be recovered with #[module] derive Inductive ty := ....
  • A module name can be specified with #[module="Ty"] derive Inductive ty := ....

• A custom prefix can be configured with the prefix (string) attribute.

please put this text in the README.md (and fix the example there).

[gares]

TODO (for me): there is a coq.elpi.toposort but for a full graph. Fix/adapt to this use case.

[rlepigre]

Note: I fixed the generation of the alias for the type in the case where there is a wrapper module. It was named after the wrapper module name, instead of the type name.

I also took this opportunity to add a no_alias attribute that disables the generation of the aliases.

[rlepigre]

please put this text in the README.md (and fix the example there).

@gares I have given it a quick try, and it seems to me like the README.md file is not in a terribly good shape right now. I'd be surprised if the code it contains fully works on master (I found a few typos). I'm not sure how best to fix this.

[gares]

Thanks. The code should be copy/pasted from readme.v which you edited to add the #[module] attribute and that edit prompted for an update. The README says it generates a module, that now is optional.

[rlepigre]

I took care of adding a bit of documentation to apps/derive/README.md, and also squashed commits since they did not really make sense anymore on their own with all the bug fixes we pushed.