search

mit-plv / bbv

Bedrock Bit Vector Library
MIT License
27 stars 23 forks source link

Remove deprecated files in Coq.Arith #47

Closed Villetaneuse closed 1 year ago

Villetaneuse commented 1 year ago

Necessary for Coq/Coq#18164

Villetaneuse commented 1 year ago

@JasonGross This should be ok, I think.

JasonGross commented 1 year ago

@Villetaneuse I don't have permissions on this repository, I think we need @samuelgruetter @andres-erbsen here

JasonGross commented 1 year ago

Also, btw, if you write it as coq/coq#18164 (without the :), I think GitHub will autolink the issue

Villetaneuse commented 1 year ago

Also, btw, if you write it as coq/coq#18164 (without the :), I think GitHub will autolink the issue

Sorry, still quite new to this. This is edited. And thank you for the correct pings!

samuelgruetter commented 1 year ago

In Coq 8.15, this fails with 

Error: The reference Even_Odd_dec was not found in the current environment.

But, as far as I understand, the bbv library is not really used any more, except maybe for rebuilding old projects, so before anyone spends time on making it compatible with several Coq versions, maybe we should ask if we should simply take bbv out of Coq's CI?

Villetaneuse commented 1 year ago

In Coq 8.15, this fails with

Error: The reference Even_Odd_dec was not found in the current environment.

But, as far as I understand, the bbv library is not really used any more, except maybe for rebuilding old projects, so before anyone spends time on making it compatible with several Coq versions, maybe we should ask if we should simply take bbv out of Coq's CI?

Thank you, I don't know who decides such things. I'm putting a link to your post on zulip here.

JasonGross commented 1 year ago

It's used by fiat-crypto-legacy, which I'd like to keep compatible in Coq's CI, but for which multiple version compatibility is also not important, so maybe it's best to bump bbv's CI to test 8.16, 8.17, 8.18, master?

samuelgruetter commented 1 year ago

so maybe it's best to bump bbv's CI to test 8.16, 8.17, 8.18, master?

I just tried that, but it seems 8.18 is not yet available in the Ubuntu builds. Should I just do 8.16, 8.17 & master for now @JasonGross ?

JasonGross commented 1 year ago

Yes, that sounds good. I'll try to get 8.18 in Ubuntu packaging soon

samuelgruetter commented 1 year ago

Ok so I just pushed CI for 8.16, 8.17 & Coq master to bbv's master. @Villetaneuse could you please rebase this PR?

Villetaneuse commented 1 year ago

Ok so I just pushed CI for 8.16, 8.17 & Coq master to bbv's master. @Villetaneuse could you please rebase this PR?

Done.

Villetaneuse commented 1 year ago

@samuelgruetter thank you very much!