search

affeldt-aist / infotheo

A Coq formalization of information theory and linear error-correcting codes
GNU Lesser General Public License v2.1
64 stars 15 forks source link

upd opam #111

Closed affeldt-aist closed 8 months ago

affeldt-aist commented 8 months ago

@t6s @garrigue I don't get the CI error, you might have an idea

t6s commented 8 months ago

I tried to compile infotheo with coq-mathcomp-ssreflect.1.19.0 and failed. There seems to be no algebra-tactics compatible to mc 1.19.0.

t6s commented 8 months ago

Are you asking how to control the behavior of the CI so that the tests for 1.19 gets disabled? I have no idea about that ..

t6s commented 8 months ago

| (= "dev") is bad?

affeldt-aist commented 8 months ago

it seems that the problem is no-algebra-tactics for 1.19 :-( maybe it is just a matter of updating opam with more permissive bounds

affeldt-aist commented 8 months ago

| (= "dev") is bad?

I think it is harmless.

affeldt-aist commented 8 months ago

Since infotheo seems to compile with analysis 0.7.0, I have in the meantime requested an opam update: https://github.com/coq/opam/pull/2929

affeldt-aist commented 8 months ago

it seems that the problem is no-algebra-tactics for 1.19 :-( maybe it is just a matter of updating opam with more permissive bounds

e.g.: https://github.com/coq/opam/blob/master/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.1.0/opam

affeldt-aist commented 8 months ago

Let's ask the developers: https://github.com/coq/opam/pull/2930

affeldt-aist commented 8 months ago

@t6s fixed by the opam fix!