search

xavierleroy / canonical-binary-tries

Coq development accompanying the paper "Efficient Extensional Binary Tries"
BSD 3-Clause "New" or "Revised" License
19 stars 2 forks source link

Make work with recent versions of Coq #1

Open robbertkrebbers opened 1 year ago

robbertkrebbers commented 1 year ago

I tried to compile and run the development with Coq 8.17 and get some errors and warnings.

The errors are about Global being missing, I will open a pull request for that.

The warnings are as follows:

Ignored instance declaration for “sym”: “forall (A : Type)
                                           (cmp : A -> A -> comparison),
                                         SymTrans cmp -> Sym cmp” is not a class

Ignored instance declaration for “tra”: “forall (A : Type)
                                           (cmp : A -> A -> comparison),
                                         SymTrans cmp -> Trans cmp” is not a class

"auto with *" was used through the default "intuition_solver" tactic.
xavierleroy commented 1 year ago

Thanks for the Global fix. The warnings are all in the vendored copy of the MMaps library, which is used only for benchmarking purposes and is now maintained upstream (https://github.com/coq-community/coq-mmaps). So the way forward is to remove the vendored MMaps and use the external library.