Enrico Tassi (Jul 16 2020 at 15:20): Enrico Tassi (Jul 16 2020 at 15:20):This was asked by @Christian Doczkal and I don't know the answer.
It was introduced in the commit by @Cyril Cohen that made factory operations not suffixed with, say _f, in a HB.builers section, not sure it is related.
Cyril Cohen (Jul 16 2020 at 15:47):This is for backward compatibility reasons in case someone wrote explicitly e.g. Ring.add
Christian Doczkal (Jul 16 2020 at 16:10):I created a (minimal) example here. The Problem only shows up when importing the generated hierarchy: https://gist.github.com/chdoc/f50c3a15c41e92ec0ac89112f1e18fbe
Christian Doczkal (Jul 16 2020 at 16:12):The problem being that the reexport shadows the original notation for the relation/operation.
Cyril Cohen (Jul 17 2020 at 20:04):Indeed this is bad..., let's remove these reexports for now...
Enrico Tassi (Jul 17 2020 at 20:19):note that coq-elpi commands do understand attributes (eg #[verbose]). We could have one attribute to enable MC specific backward compatibility code.
Enrico Tassi (Jul 17 2020 at 20:22):See also https://github.com/coq/coq/issues/10824
Cyril Cohen (Jul 17 2020 at 20:22):@Enrico Tassi that's what I meant in math-comp/hierarchy-builder#85 but I do not think it makes sense for the "reexport operations" bug
Enrico Tassi (Jul 17 2020 at 20:23):My point is that I don't know if we trigger a bug, see above, or if the code for backward compat is sometimes undesired.
Cyril Cohen (Jul 17 2020 at 20:24):I think the backward compatibility code is flawed anyway
Cyril Cohen (Jul 17 2020 at 20:24):(and that we might also trigger a bug)
Christian Doczkal (Jul 17 2020 at 20:43):Well, I'm of course biased, because I don't have HB code that's older than two days. But I would be happy if HB wouldn't trash my notations :sunglasses:
Last updated: May 28 2023 at 20:30 UTC