Allow accumulating Dbs (and other things) into Dbs

[Janno]

This change turns databases into "libraries" (see #Elpi users & devs > Calling `derive` from other elpi commands @ 💬). They can now accumulate anything that commands and programs can accumulate.

This is largely achieved by removing differences and, if that's not easily possible, copying code. The most difficult part that needed re-engineering is probably the compilation and especially caching. The current implementation is very slightly buggy and required a single re-ordering change in Accumulates in bluerock code before it would build everything. I could probably use help here.

Fixes: #889

Depends on: LPCIC/elpi#372

TODO:

• Fix bug in caching logic

Noteworthy changes

Duplicates are Pruned

The new code prunes duplicates within a database/program/command, even transitively. That's how libraries should work. It also doesn't hurt to do it for commands and programs, I think. Pruning only happens for accumulated databases and full units. Signatures currently have no useful identity so I opted to simply accumulate those multiple times.

Databases accumulate the Command Template

Some derive extensions graft clauses into predicates from coq-lib.elpi (look for before "subst:fail"). To make this work, the derive database must accumulate not just the signature but the entirety of coq-lib.elpi. Unfortunately, doing this just for derive and with just coq-lib.elpi runs into limitations of the aforementioned pruning: coq-lib.elpi is contained in elpi-command-template.elpi which is always accumulated into Commands. However, my code does not (and perhaps cannot?) see that elpi-command-template.elpi is made up of smaller files. So the two files are treated as unrelated and accumulating derive into a command (which always accumulates the template) runs into problems with duplicate clauses from coq-lib.elpi.

I opted to accumulate the entire command template into every database. This way, the files are recognized as duplicates and accumulating databases into commands works without any problem.

Everything in Dbs is SuperGlobal

To make the semantics for transitive dependencies work out, Accumulate with a database target is always superglobal. I do not understand why this is necessary. Using anything but superglobal leads to changes (Accumulates) to the DB being invisible to clients that import the module containing the changes. This might be a self-inflicted problem due to my changes. Perhaps it is also because I am still confused by #721.

Example: derive as a Database

The change also includes a change to derive which can now be first and foremost a database and just a small main shim around that database. We make use of the fact that Commands can be exported under different names to have both a vernacular command derive (actually called derive_cmd) and a database derive.