Stream: Coq devs & plugin devs

Topic: Bad naming in practice


view this post on Zulip Karl Palmskog (Oct 09 2020 at 21:29):

QArithSternBrocot (coq-community project) broke hard in Coq 8.11. The reason was that Stdlib introduced a lemma Zsgn_1, which took priority over the local Zsgn_1 lemma (the lemmas had very similar parameters, but completely different statements). Seemingly, both Stdlib and QArithSternBrocot are full of lemma names like Z<blah>_<number>...

view this post on Zulip Paolo Giarrusso (Oct 10 2020 at 05:42):

Would it help to order stdlib imports before local imports? 8.11 changed the import semantics breaking everything...
Example fix in this style: https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/313

view this post on Zulip Karl Palmskog (Oct 10 2020 at 11:03):

it probably would help, but the project is full of Require Export ..., which makes figuring out order of imports a nightmare.


Last updated: Oct 16 2021 at 03:02 UTC