search

micro-policies / micro-policies-coq

Coq formalization accompanying the paper: Micro-Policies: A Framework for Verified, Tag-Based Security Monitors
Other
19 stars 0 forks source link

Ltac call to "by (ssrhintarg)" failed. Error: congruence failed. #1

Open catalin-hritcu opened 6 years ago

catalin-hritcu commented 6 years ago

This fails ./sealing/refinementSA.v to build for me with Coq 8.6.0, latest CoqUtils, and some unspecified mathcomp:

File "./sealing/refinementSA.v", line 134, characters 2-64:
Ltac call to "by (ssrhintarg)" failed.
Error: congruence failed.
make[1]: *** [Makefile.coq:331: sealing/refinementSA.vo] Error 1
make[1]: *** Waiting for unfinished jobs....
File "./compartmentalization/abstract.v", line 1252, characters 42-54:
Ltac call to "discriminate" failed.
Error: No primitive equality found.

Any ideas what might be going wrong here and how to fix it? Should I try to update mathcomp to something specific? Or downgrade CoqUtils? Or something else? :)

catalin-hritcu commented 6 years ago

More generally, is there any easy way to figure out what version of a Coq plugin I have installed?