search

mit-plv / fiat-crypto

Cryptographic Primitive Code Generation by Fiat
http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf
Other
720 stars 146 forks source link

Moving at level 10 notations which were originally at level 200 #1695

Closed herbelin closed 1 year ago

herbelin commented 1 year ago

This follows what was done for notations at level binder_constr in Coq PR #18014.

This should fix the compilation of fiat crypto legacy in Coq CI, but I could not fully check (I get a segfault on src/Algebra/Field.v, maybe due to a previous failure to set the ulimit??)

JasonGross commented 1 year ago

Does the docker image need to be updated? I see

File "./src/Util/Notations.v", line 138, characters 0-123:
Error:
Level 10 is already declared to have left associativity while it is now expected to have right associativity.

on master.

Maybe the segfault on Field is from par? Is it an OOM? I don't think ulimit should be essential

herbelin commented 1 year ago

Does the docker image need to be updated? I see

Sorry, I'm a bit ignorant about CI and I don't know what you are referring to by "docker image".

In any case, I pushed a fix so that, hopefully, the test against master works.

JasonGross commented 1 year ago

Sorry, I'm a bit ignorant about CI and I don't know what you are referring to by "docker image".

I mean https://github.com/coq-community/docker-coq / https://hub.docker.com/r/coqorg/coq/. I'm going to rebase the branch to make sure that failure on 8.16 / 8.17 doesn't make master fail.

JasonGross commented 1 year ago

CI says

File "./src/Specific/Framework/IntegrationTestDisplayCommon.v", line 24, characters 0-32:
Error: Notation "λ _ .. _ , _" is already defined at level 10 with arguments binder, constr at level 200 while it is now required to be at level 200 with arguments binder, constr at level 200.
herbelin commented 1 year ago

Is it the right version of Coq (it seems to say 8.master~git~202309291236+24340-0~daily386-41944f5551~ubuntu20.04.1") and the failure is on Require Import Utf8 whose current notation for λ has 10 not 200?

JasonGross commented 1 year ago

Oh, urgh, I need to update this to use docker instead of my ppa. My ppa version is blocked on https://github.com/coq/coq/pull/18105#issuecomment-1785274048

JasonGross commented 1 year ago

Rebased to use actual master now. But it seems that we might be failing with

File "./src/Experiments/SimplyTypedArithmetic.v", line 7059, characters 4-350:
Error: Anomaly "Not an unfoldable reference."
Please report at http://coq.inria.fr/bugs/.
JasonGross commented 1 year ago

This does not build, but I will merge it anyway so Coq's CI won't be blocked on this. It seems a new regression was introduced into Coq in the mean time.