Create HintDBs with the discriminated option

According to the documentation https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:cmd.create-hintdb, when creating a hint database without discrimination, Coq uses the legacy implementation, which only uses Discrimination Trees for goals without evars and does not use opaqueness information. This commit switches the hint databases of stdpp to the new implementation.

Does this have any performance impact?

I don't know. I just found this feature in the documentation and @robbertkrebbers said that we should probably use it. What would be the best way to test the performance? Is there a way to test the performance of Iris with this patch? Does build-all do timing?

Does build-all do timing?

No. To measure e.g. lambda-rust, you need to push a commit like this to a branch named like ci/msammler/hintdb_discriminated. In this case, the opam-pins line would be something like

OPAM_PINS: "coq version 8.11.0   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#msammler/hintdb_discriminated"

Then you can use this dashboard to setup a comparison with the master branch.

Since these hint databases are used very little I expect no performance regressions. So we could also "hope" that what I say is true, and otherwise revert?

Fine for me, if you will take care of the fallout (if any).

Sure. I can also take care of pressing revert in case there are issues :).

@msammler Are you OK with this proposal?

Sorry for not responding earlier. I tried testing the changes locally first with lambda-rust, but OPAM_PINS does not seem to work locally and then I got caught up in other stuff. But now I tried it with lambda-rust locally and it at least still builds. So I am fine with merging and seeing what happens.

OPAM_PINS does not seem to work locally

I don't know what this statement means; OPAM_PINS is configuration that is interpreted by our CI scripts.

That is what I figured out as well. My hope was that make build-dep would also be able to interpret it, but it is not.

No that's entirely unrelated, make build-dep only "interprets" the local opam file.

Merging then.

merged

mentioned in commit 93b578a5