search

gmalecha / mirror-core

A framework for extensible, reflective decision procedures.
Other
19 stars 5 forks source link

Compilation error Mirror-core 1.0.0 package, Coq 8.5.0 #106

Closed clarus closed 5 years ago

clarus commented 5 years ago

Hi,

I have got a compilation error with the package coq-mirror-core.1.0.0:

After some investigations I though it was because of this commit in Coq: https://github.com/coq/coq/commit/b98e4857a13a4014c65882af5321ebdb09f41890 Actually this commit never made it into 8.5.0 and it seems due to this patch file in the Coq package: image To me the fault is from this patch.

What do you think we should do? Remove the Coq patch (maybe too late)? Remove this package version? Is there an other way to install this version?

gmalecha commented 5 years ago

I can update mirror-core to be compatible with the patch if is just a simple renaming.

clarus commented 5 years ago

Ah, OK, but this is about an old version (1.0.0) and is already fixed in the next one (1.0.1). The question is more about the precise coq-mirror-core.1.0.0 package which is available on the repo but cannot install as far as I understand.

clarus commented 5 years ago

I think the simplest is to remove it.

gmalecha commented 5 years ago

Oh, sounds like a better idea if it is already fixed in 1.0.1. Do I need to do anything to remove it?

clarus commented 5 years ago

No, I can do it on the repo. This was to confirm. Thanks!