search

ejgallego / coq-serapi

Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Other
128 stars 39 forks source link

Run tests with MC 2 #395

Closed SnarkBoojum closed 7 months ago

SnarkBoojum commented 7 months ago

While working on my packaging for coq-serapi in Debian, I hit closed issue #373: it is in fact still a current.

I'm disabling the only failing test file for now.

ejgallego commented 7 months ago

Unfortunately math-comp 2 is a lot more heavier to install, so this is not trivial to solve without some effort, in particular about the elpi and hb deps.

I'd suggest disabling this test on debian.

ejgallego commented 7 months ago

It should be possible to rewrite the test so we don't need math-comp but just stuff in Coq.ssreflect , in fact we want to test the stuff in the Coq plugin.

ejgallego commented 7 months ago

Fixed by #399