Zulip Chat Archive

the implementation of /= as simpl probably predates cbn. But is there any reason one might want to switch /= to be cbn instead? Or reasons against? Wasn't the goal of cbn to be a "better simpl"?

Janno (Apr 25 2022 at 13:53):

Reasons for:

cbn respects simpl never
cbn unfolds aliases even when they do not lead to further reduction (I find that desirable but that's just me)
cbn generally has more deterministic performance in my experience but it's been a while since I last tested it. Most of that might well be down to the first point.

Reasons against:

cbn is generally slower than simpl (unless simpl tries to do too much, see above)
The implementation of cbn seems to be complex and bugs that have been fixed have generally been tricky. I don't know that simpl is that much easier to fix but maybe it just has fewer bugs from being around longer/being used more?

Karl Palmskog (Apr 25 2022 at 13:56):

OK, would be interesting to know if there's anything MathComp-specific affected by "unfolds aliases even when they do not lead to further reduction".

I've only used cbn a bit, and I think the aliasing stuff turned my context to a mess quite a lot. But idiomatic SSR usually scopes simplification very carefully.

Janno (Apr 25 2022 at 13:58):

The good thing is that you can add simpl never to your alias and cbn will not unfold it any more

Karl Palmskog (Apr 25 2022 at 14:00):

good to know, but simpl never is not very often used in MathComp projects. I only see a few in Analysis and fourcolor

Janno (Apr 25 2022 at 14:01):

I can't deny that it is annoying, especially when it's the only reason for the entire Arguments line in the code.

Paolo Giarrusso (Apr 25 2022 at 18:25):

@Karl Palmskog there's an option to make simpl itself use cbn. But nobody has had success with it

Paolo Giarrusso (Apr 25 2022 at 18:27):

I recall @Enrico Tassi considers "cbn is a better simpl" as just wrong. There are also a few issues on the discrepancies. One has even been fixed. But they're extremely confusing... I'm kind of happy I forgot most details :-|.