Stream: math-comp users

Topic: ssr and Coq bullets

view this post on Zulip Paolo Giarrusso (Oct 12 2022 at 19:15):

I've always been curious about math-comp's Global Set Bullet Behavior "None". — is that an historical artifact?

I can see one downside of real bullets: they don't let you de-indent the last case by default. But { ... } does allow that...

view this post on Zulip Pierre Roux (Oct 13 2022 at 06:40):

Yes, historical reasons: ssreflect bullets were introduced before Coq ones and were just comments (i.e. the behavior of Set Bullet Behavior "None"). Adapting the whole MathComp (and reverse dependencies) would require a rather large amount of work.

As a beginner user of MathComp, I was missing the actual bullets, but in the end it's not that bad: most proofs are very short and for the few longer ones, the extensive use of have keeps the indentation level low (4 levels of indentation and more are extremely rare in MC).

TBH, it occured a few times to me (for instance during the port to hierarchy-builder) that a proof would break and I would have to go back by dichotomy and compare the number of goals with the indentation level. Whereas actual bullets would have make the breakage located directly at the right place. So actual bullets could indeed have saved a few minutes of my life in total.

view this post on Zulip Théo Zimmermann (Oct 13 2022 at 08:35):

Since SSR use of significant indentation is well-defined, we could create a strict bullet mode that is compatible with it. But I never got around to even just document this as a CEP (and probably never will).

Last updated: Feb 22 2024 at 03:02 UTC