Moving at level 10 notations which were originally at level 200

[herbelin]

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]

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]

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]

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]

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]

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]

Oh, urgh, I need to update this to use docker instead of my ppa. My ppa version is blocked on coq/coq#18105 (comment)

[JasonGross]

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]

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.