Stream: Hierarchy Builder devs & users

Topic: [Q] why structures re-export operations (as notations)


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

view this post on Zulip Cyril Cohen (Jul 16 2020 at 15:47):

This is for backward compatibility reasons in case someone wrote explicitly e.g. Ring.add

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

view this post on Zulip Christian Doczkal (Jul 16 2020 at 16:12):

The problem being that the reexport shadows the original notation for the relation/operation.

view this post on Zulip Cyril Cohen (Jul 17 2020 at 20:04):

Indeed this is bad..., let's remove these reexports for now...

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

view this post on Zulip Enrico Tassi (Jul 17 2020 at 20:22):

See also https://github.com/coq/coq/issues/10824

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

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

view this post on Zulip Cyril Cohen (Jul 17 2020 at 20:24):

I think the backward compatibility code is flawed anyway

view this post on Zulip Cyril Cohen (Jul 17 2020 at 20:24):

(and that we might also trigger a bug)

view this post on Zulip 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: Jan 29 2023 at 14:02 UTC