Karl Palmskog (Jul 22 2022 at 11:44): Karl Palmskog (Jul 22 2022 at 11:44):@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.
Karl Palmskog (Jul 22 2022 at 11:44):since the deprecations essentially only show up in 8.16, I think we can postpone a bit to fix those
Karl Palmskog (Jul 22 2022 at 13:32):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).
Pierre Castéran (Jul 22 2022 at 14:12):Ok, and in Hydra battles too: I'll look at these warnings
Karl Palmskog (Jul 22 2022 at 14:24):here is my current set of standard solutions for the Nat operation deprecations: https://github.com/coq-community/bertrand/pull/17/files
Pierre Castéran (Jul 22 2022 at 18:35):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 coq-art/tutorial_type_classes/SRC/Monoid_op_classes.v
in 8.14:
- 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)
Karl Palmskog (Jul 22 2022 at 18:40):a rule of thumb I typically use is: try hard to support latest two Coq versions, but only versions below when the effort is feasible reasonable
Pierre Castéran (Jul 22 2022 at 18:45):So, we keep the 8.15 version (with the global attribute on l. 445). I will push my corrections in the branch corrections.
Karl Palmskog (Jul 22 2022 at 18:46):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
Pierre Castéran (Jul 22 2022 at 18:58):Ok, I pushed into corrections(no warnings in Coq 8.15 on my computer).
Karl Palmskog (Jul 22 2022 at 19:04):@Pierre Castéran OK, all CI and so on is adjust in the corrections branch.
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
Pierre Castéran (Jul 22 2022 at 19:04):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.
Karl Palmskog (Jul 22 2022 at 19:04):right, even/odd decidability changed quite a lot
Pierre Castéran (Jul 22 2022 at 19:08):OK, I will prepare a 8.15 warning-free branch. If <= 8.14 fail, we will see ...
Pierre Castéran (Jul 23 2022 at 12:37):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 ...).
Karl Palmskog (Jul 23 2022 at 12:43):all the Mult, Div2 stuff can be ported quite nicely in my experience. The main problem is Even/Odd
Pierre Castéran (Jul 23 2022 at 16:39):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.
Paolo Giarrusso (Jul 23 2022 at 16:45):I've seen repeated deprecation warnings if the warning is inside Ltac code that backtracks...
Paolo Giarrusso (Jul 23 2022 at 16:52):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 !
Pierre Castéran (Jul 23 2022 at 18:14):Indeed, the following message (three occurrences (for the same line)) was triggered by just a rewrite mult_0_r.
- 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