Fix most warnings (especially in 8.13)

[palmskog]

I used Pierre-Marie Pédrot's script to add explicit locality to hints (otherwise, there is a warning in 8.13). I also fix or ignore some other warnings that are standard. This lessens the noise generated in CI considerably.

[Casteran]

There seems to be a lot of warnings of the form « Unused variable x catches more than one case » , for instance in definitions like Fixpoint mult (alpha beta : T1) :T1 := match alpha,beta with | zero, y => zero | x, zero => zero | ocons zero n _, ocons zero n' _ => ocons zero (Peano.pred((S n) * (S n'))) zero | ocons a n b, ocons zero n' b' => ocons a (Peano.pred((S n) * (S n'))) b | ocons a n b, ocons a' n' b' => ocons (a + a') n' ((ocons a n b) * b') end where "alpha * beta" := (mult alpha beta) : t1_scope. Is giving a name to an unused variable (in the right hand side of a match clause) bad style ? If so, I can replace a lot os such occurrences by the anonymous variable _. But, as readability is concerned, the second clause of the match looks like the equation x * zero = zero.

…

Le 5 janv. 2021 à 13:51, Karl Palmskog ***@***.***> a écrit : I used Pierre-Marie Pédrot's script to add explicit locality to hints (otherwise, there is a warning in 8.13). I also fix or ignore some other warnings that are standard. This lessens the noise generated in CI considerably. You can view, comment on, or merge this pull request online at: #18 <#18> Commit Summary add explicit hint locality using PMP script to avoid warnings in 8.13 fix double induction deprecation ignore MathComp-related warnings in _CoqProject and dune File Changes M _CoqProject <https://github.com/coq-community/hydra-battles/pull/18/files#diff-7bc0f432942f548a20da329bb4e45e21faeeb897fe1d7e0bc26d20210a6e38f1> (3) M theories/additions/Dichotomy.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-b47ac7d99a5dc506f1467066dd71fdfe19db6d2f295912bb043e5b884df3db67> (2) M theories/additions/Euclidean_Chains.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-33c0f5d237ab37b1a325af7f3ba6d384707be80760e4e7c3b3f327be3cda4a5f> (8) M theories/additions/Monoid_instances.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-80a19156be5ce150462e7cad6757d78c07c07f81aba618538f5cfcf0fa1c7aa9> (8) M theories/additions/More_on_positive.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-68e107b85f9e20ed6b72e6627fa1d2a4f276c2755e926c5f327886c6a966cc53> (8) M theories/additions/dune <https://github.com/coq-community/hydra-battles/pull/18/files#diff-a65f793256e07fbc65724fbad7aaf1f2d23c26758b41e740110f98ce6e4c4407> (3) M theories/ordinals/Epsilon0/Canon.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-a3c461509071085720be95b0eff989e81ad80e2286b8d0d08f41570fbb7dcbe3> (2) M theories/ordinals/Epsilon0/E0.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-c5af3c921dd03001f94a65d541d4deec780a7f1ab00d3824c742b00f407eea26> (14) M theories/ordinals/Epsilon0/Epsilon0rpo.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-523f1a085d9d1f2b2337fc4b759cb08255b5463557d6a5f0f0d3c65702ec3f1f> (18) M theories/ordinals/Epsilon0/F_alpha.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-d029435a2aa0c96fc1d0a7b48b287beb3580aad1c9856fb1b9cd456a3bff591e> (4) M theories/ordinals/Epsilon0/H_alpha.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-7a5de3758ace9509337f8e90adb5edef2b7a513d45042f380f726c99b6ce915d> (4) M theories/ordinals/Epsilon0/L_alpha.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-00ece1474a8443838722f48a0c5deb8497cee745697c2e947e75a38d26e4a4db> (2) M theories/ordinals/Epsilon0/Large_Sets_Examples.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-c7026aff7fa26a0240c8e17840dd995dea5f244c93977dd07b8875fa2ed0c227> (2) M theories/ordinals/Epsilon0/T1.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-cb1a336f3b87bd98e1d8723883ed887d63b1a6a8d4b740a55bb7fea744242a12> (30) M theories/ordinals/Gamma0/Gamma0.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-98864be563c31d95297a9f311976d5337008bbe2ba6fabaa0ad39e61f9668845> (32) M theories/ordinals/Gamma0/T2.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-2b991ee7ed06357b17ce15204fae24bf4e08b5bd3a89a7e9533939c07ce82284> (8) M theories/ordinals/Hydra/Epsilon0_Needed_Free.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-81df98a10d0f01edbbba99dd48bd01112e69d09806c7f95577707118b414de9b> (2) M theories/ordinals/Hydra/Epsilon0_Needed_Generic.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-08e9ceae459dfdc3fd911877774e8594c2439a711e2da472ead8f3d46c885d0e> (2) M theories/ordinals/Hydra/Hydra_Termination.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-4e6c87b8a125f79b1d6b2162df367e808dded503f4edacfc11e1c0fed539cc70> (2) M theories/ordinals/Hydra/Omega2_Small.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-e2856306d4d8c6c9896c772c233a808a038a952d7337863b780227dff0c28b0b> (10) M theories/ordinals/Hydra/Omega_Small.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-a87f4ba93a5a043a96f9d916ef680a40fc26d5657c7794359e28a16ee22523cd> (2) M theories/ordinals/OrdinalNotations/ON_Generic.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-b6fdbdc73a9fb963e353dd8f13beacfeba9b0cd5c1de810d365fc2b99e3c17cc> (2) M theories/ordinals/OrdinalNotations/ON_Omega2.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-87a5b1dd4c8061d2daa8ee765a522e6dcf566e7ea3e63323e8008581e724b0ba> (4) M theories/ordinals/OrdinalNotations/ON_mult.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-f27db2e205878a8a4a6c3bee4c7b6c06acb2ae4a90917774010b1da187cbb7eb> (4) M theories/ordinals/OrdinalNotations/ON_plus.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-2812a6353f847c1cd11ed782dd67195d93b5fdf2c8ea44b4fc0d6b5c8de61034> (4) M theories/ordinals/Prelude/MoreLists.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-0659422298e21526e03c893fd0475c72a53034bd1064a00bd99b1a1d46b30986> (2) M theories/ordinals/Prelude/Sort_spec.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-6cfcfcbcb03df382d7326c3ff99d5966189a657de4308527ae6364501bf1368f> (2) M theories/ordinals/Schutte/AP.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-eebbd06164415dc9298ee3f2e18b30f81a0c2ba24a63c4a6cff0a817f5adedad> (4) M theories/ordinals/Schutte/CNF.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-59d5cf7fdf342381341c40b8fa7a462bd4635d5657a3da976d603b2a555744c2> (4) M theories/ordinals/Schutte/Ordering_Functions.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-02b4875c36dfa3aa6be37f6dcdbdc075e6fb0b068ff96960da910c7990c99b29> (18) M theories/ordinals/Schutte/Schutte_basics.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-67d263a508dca5da9bc29ad35f77e3c027c8350535f0356346b9e5befb5263d5> (28) M theories/ordinals/Schutte/Well_Orders.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-748bd8981ca713c72e71886adc819d0732c81574d4ff3173f4c0d4d3455f2ca4> (2) M theories/ordinals/primrec/primRec.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-82767788342d2644cb888af55ebd24b85be211ac765428c3e795b5af2f370eca> (2) M theories/ordinals/rpo/list_permut.v <https://github.com/coq-community/hydra-battles/pull/18/files#diff-f1ca29f4b0d94949add0649072a9a86628815dd99ca47ee51c44c98c1c582c5d> (4) Patch Links: https://github.com/coq-community/hydra-battles/pull/18.patch <https://github.com/coq-community/hydra-battles/pull/18.patch> https://github.com/coq-community/hydra-battles/pull/18.diff <https://github.com/coq-community/hydra-battles/pull/18.diff> — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#18>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AJW6FCSUQZTW6JGKNFORH7TSYMDNTANCNFSM4VVCD3MA>.

[palmskog]

@Casteran indeed this seems like a very nitpicky warning, and it was only introduced in 8.13. Perhaps we should simply suppress/ignore it? This is quite simple to do by editing _CoqProject/dune. Personally, I also prefer using x or similar rather than _ in these situations.

Perhaps @Zimmi48 knows why this warning was introduced.

[Zimmi48]

See coq/coq#12762 for the rationale. Feel free to ignore this warning if you do not find it useful. Maybe the warning message should explain why it is considered a bad practice though.

[palmskog]

@Casteran what do you think of the rationale in coq/coq#12762? I'm fine with either suppressing the warning or changing the code to use underscores.

[Casteran]

I understand the rationale. Tomorrow, I can replace in master the catch-all variables with underscores.

…

Le 5 janv. 2021 à 17:13, Karl Palmskog ***@***.***> a écrit : @Casteran <https://github.com/Casteran> what do you think of the rationale in coq/coq#12762 <coq/coq#12762>? I'm fine with either suppressing the warning or changing the code to use underscores. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#18 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AJW6FCTW3F2WUFZIGLBBYJLSYM3ELANCNFSM4VVCD3MA>.

[palmskog]

OK, since the variable name change is orthogonal to this PR, I will then take the liberty to merge. The only remaining warnings were those related to the Coq issue.

[Casteran]

In fact, there were only three occurrences of the « unused variable » issue (but signaled many times). I fixed that (hope so) and pushed into master.

…

Le 5 janv. 2021 à 17:58, Karl Palmskog ***@***.***> a écrit : Merged #18 <#18> into master. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#18 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AJW6FCVLC6SJMXG6VXZYIFTSYNAKXANCNFSM4VVCD3MA>.