Remove algebraic hierarchy from Qmetric#100
Conversation
|
@Zimmi48 Hello, do you understand this nix error ? It seems unrelated to the PR. |
|
I don't understand it (yet) but it is failing all over the place (on many projects). I will try to solve it ASAP, but if it's an issue for you, we can immediately switch to opam-based testing only. |
|
@VincentSe A priori this is fixed in #97 (to be confirmed when CI passes fully). |
|
I'd prefer to fix it by #99 or at least have a change that does not break the type classes in our work in ODEs. |
|
I've merged #97 I guess you should rebase on top of that. |
|
@spitters @Zimmi48 Before Coq 8.10, the compiler doesn't resolve the Coercion This is even stranger because all previous versions compile before this pull request, so they do resolve the coercion. This confirms that Coq's implicit machinery of coercions, canonical variables and typeclasses is very fragile. What should I do ? Remove the coercion and explicitly write |
|
Yes, I was surprised about that too! Maybe @mattam82 knows what changed in the type-class implementation between these versions. Yes, I agree inserting the st_car is the most sensible way to solve this. |
|
Why would you remove the coercion? One could just insert it in the places where it cannot be found. I'm not opposed to dropping compatibilty with older versions, but if possible it would be nice to keep it. |
|
That the coercion fails seems to be due the the algorithm not being
clever enough.
So, you should be able to help it by just putting in st_car at these places.
No need to declare the coercion again.
…On Mon, Jun 1, 2020 at 9:47 PM Vincent Semeria ***@***.***> wrote:
@spitters @mattam82 If I add Coercion st_car : RSetoid >-> Sortclass. in file UniformContinuity.v, branch master fails with
Error: st_car is already a coercion.
So how do we put the coercion back in the previous versions so that all versions compile ?
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub, or unsubscribe.
|
VincentSe
force-pushed
the
CutQmetric
branch
16 times, most recently
from
8066716 to
b28838d
Compare
VincentSe
force-pushed
the
CutQmetric
branch
6 times, most recently
from
8a7db18 to
1026895
Compare
Build fast reals Build abstract integral Build Picard Build Picard cut Metric.v Cut RSetoid Cut Metric.v
3 participants
Remove those 2 imports from Qmetric.v, then make the rest of CoRN compile
This aims at defining constructive real numbers abstractly, instead of relying on an algebraic hierarchy. All the similar imports will be progressively removed from folders reals/fast and reals/faster.