Stream: coq-community devs & users

Topic: Rolling back Scheme changes for Coq'Art


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Pierre Castéran (Jul 22 2022 at 14:12):

Ok, and in Hydra battles too: I'll look at these warnings

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip Karl Palmskog (Jul 22 2022 at 18:38):

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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre Castéran (Jul 22 2022 at 18:58):

Ok, I pushed into corrections(no warnings in Coq 8.15 on my computer).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jul 22 2022 at 19:04):

right, even/odd decidability changed quite a lot

view this post on Zulip 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 ...

view this post on Zulip 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 ...).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 23 2022 at 16:45):

I've seen repated deprecation warnings if the warning is inside Ltac code that backtracks...

view this post on Zulip 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.

view this post on Zulip Pierre Castéran (Jul 23 2022 at 17:00):

Ah, OK, thanks, I will check that !

view this post on Zulip 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: Feb 04 2023 at 02:03 UTC