@Pierre Castéran OK with you if I roll back the changes to
Scheme in Coq'Art code: https://github.com/coq-community/coq-art/commit/905812646d536bc8c168699199d2fc71862e313f
.. and then do a release for 8.15? Always good to have a tag for this, for people who may be stuck on some Coq version.
since the deprecations essentially only show up in 8.16, I think we can postpone a bit to fix those
OK, release done in https://github.com/coq-community/coq-art/releases/tag/v8.15.0
I think it would be good to have the Instance/Class locality and Nat operation deprecations fixed before 8.16 release (so maybe 10-20 edits required at least).
Ok, and in Hydra battles too: I'll look at these warnings
here is my current set of standard solutions for the Nat operation deprecations: https://github.com/coq-community/bertrand/pull/17/files
Looks like the command
#[global] Typeclasses Transparent RingPlus RingMult RingOne RingZero.
is not accepted in 8.14, but works in 8.15 and 8.16 . More, if the global attribute is lacking, 8.15 & 8.16 raise a warning.
- File "./tutorial_type_classes/SRC/Monoid_op_classes.v", line 445, characters 0-69: Error: - Error: This command does not support this attribute: global.
In 8.15 (on my computer) if I remove
#[global] from the same command.
Warning: The default value for Typeclasses Opaque and Typeclasses Transparent locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding typeclass transparency hints outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Typeclasses Transparent foo." [deprecated-typeclasses-transparency-without-locality,deprecated]
right, there are tradeoffs in adding localities like
#[global] for "everything". To me, it would be fine to drop support for Coq 8.14 and below (people always have the tags/releases)
a rule of thumb I typically use is: try hard to support latest two Coq versions, but only versions below when the effort is
So, we keep the 8.15 version (with the global attribute on l. 445). I will push my corrections in the branch
OK, you can let me know when you're done and I can modify the CI and opam boilerplate to drop 8.14 and lower
Ok, I pushed into
corrections(no warnings in Coq 8.15 on my computer).
@Pierre Castéran OK, all CI and so on is adjust in the
Just to double check, do we really want to use
#[global] everywhere instead of, e.g.,
#[export] for hints and instances? See my comments in the PR: https://github.com/coq-community/coq-art/pull/28
With hydra-battles, it'll probably be a little longer (I suspect there were some changes in definitions and lemmas about even/odd decidability). I will start tomorrow.
right, even/odd decidability changed quite a lot
OK, I will prepare a 8.15 warning-free branch. If <= 8.14 fail, we will see ...
Indeed, it will take a long time: many files used the old arithmetic (including division by 2). Proofs are broken if I don't require old Arith files (Div2, Mult, etc ...).
all the Mult, Div2 stuff can be ported quite nicely in my experience. The main problem is Even/Odd
Yep! it works !
Due to the Ackermann and rpo legacies, there are a lot of substitutions to do, but I'm optimistic.
Btw, when I look at the logs on github, the same warning if often repeated thrice or twice.
I've seen repeated deprecation warnings if the warning is inside Ltac code that backtracks...
This one's not so bad, but gives the warning twice. Getting it more than twice seems trickier.
#[deprecated(note="")] Notation deprecated := id. Goal True. match goal with | |- context [ deprecated ] => fail | |- _ => idtac "A" end.
Ah, OK, thanks, I will check that !
Indeed, the following message (three occurrences (for the same line)) was triggered by just a
- File "./theories/ordinals/Prelude/More_Arith.v", line 222, characters 9-17: Warning: - Warning: Notation mult_0_r is deprecated since 8.16. - The Arith.Mult file is obsolete. Use Nat.mul_0_r instead. - [deprecated-syntactic-definition,deprecated]
Last updated: Jun 06 2023 at 23:01 UTC