Topic: euclidean names
Johan Commelin (Sep 11 2020 at 12:53):
@Joseph Myers I'm a bit worried that the long names in
euclidean/* are hampering readability, because things now often wrap to multiple lines. What do you think of the following renamings (also on all other names that contain these substrings):
Maybe there are other options out there as well.
Reid Barton (Sep 11 2020 at 12:56):
Out of context, I'm not a fan.
What are some problematic lines?
Johan Commelin (Sep 11 2020 at 12:59):
Reid Barton (Sep 11 2020 at 13:30):
In this case, maybe
orthogonal_projection could just be
Johan Commelin (Sep 11 2020 at 13:31):
I don't have a strong opinion on exactly what changes. But I think that these wrapping lines are a bit problematic
Reid Barton (Sep 11 2020 at 13:47):
Is it too crazy to use
O as a name component for
Johan Commelin (Sep 11 2020 at 13:48):
I think it's worth having a poll on that.
Kenny Lau (Sep 11 2020 at 13:53):
Reid Barton (Sep 11 2020 at 13:55):
These are the traditional letters used for the points: https://en.wikipedia.org/wiki/Triangle_center#Classical_triangle_centers
Reid Barton (Sep 11 2020 at 13:59):
another possible compression from that line is
sq--mathlib seems to use both and I can't think of another possible meaning of
Reid Barton (Sep 11 2020 at 14:00):
sq is also used to abbreviate commutative square in the category theory library, but it's still a square)
Joseph Myers (Sep 11 2020 at 14:02):
Would you also use those names in the definitions themselves, or only for lemmas, and would
G be used for
centroid not just in the Euclidean context? For example, would
circumcenter_eq_centroid (this is in namespace
affine.simplex) end up as
/-- The circumcenter of a 1-simplex equals its centroid. -/ lemma O_eq_G (s : simplex ℝ P 1) : s.O = finset.univ.G ℝ s.points :=
or would only the name of the lemma change?
Johan Commelin (Sep 11 2020 at 14:02):
Everything is open for debate (-;
Reid Barton (Sep 11 2020 at 14:03):
I was thinking only the lemma names would change, but I don't feel strongly about this
Johan Commelin (Sep 11 2020 at 14:03):
I think with good docstrings, and namespaced definitions, we could even have 1-letter definitions in this part of mathlib.
Kevin Buzzard (Sep 11 2020 at 14:09):
Kevin Buzzard (Sep 11 2020 at 14:09):
simplex.O even better!
Johan Commelin (Sep 11 2020 at 14:09):
standard_symbol.O is already taken by orthogonal matrices
Patrick Massot (Sep 11 2020 at 14:33):
I think the issue is only in lemma names, because they use several def names. But of course changing the name from def to lemma is inconsistent :sad:.
Mario Carneiro (Sep 11 2020 at 14:51):
Yep, this is why definition names should be short
Eric Wieser (Sep 11 2020 at 15:36):
On the subject of long expressions, is there a sensible way to abbreviate terms like
dist p₁ s.circumcenter * dist p₁ s.circumcenter?
let d = dist p₁ s.circumcenter in d * d? Does mathlib have a
Mario Carneiro (Sep 11 2020 at 15:36):
d ^ 2?
Eric Wieser (Sep 11 2020 at 15:39):
That then needs an extra lemma to work with, right?
pow_2_eq_mul or something
Mario Carneiro (Sep 11 2020 at 16:03):
Mario Carneiro (Sep 11 2020 at 16:04):
I would put more emphasis on keeping theorem statement size down rather than not ever needing to rewrite
Johan Commelin (Sep 12 2020 at 05:44):
So... shall we use
O? I like the idea. (I'm fine with making those names protected, if people fear name clashes otherwise.)
Johan Commelin (Sep 24 2020 at 14:00):
Johan Commelin (Oct 05 2020 at 07:33):
/poll short euclidean names
Let's change to
proj, etc... (with long names in the docstrings)
Johan Commelin (Oct 05 2020 at 07:36):
@Joseph Myers @Mario Carneiro @Reid Barton you've participated in the above discussion. Please join the vote. (Others are welcome too!)
Yury G. Kudryashov (Oct 05 2020 at 08:29):
triangle can have many one-letter
defs in its namespace.
Johan Commelin (Oct 05 2020 at 11:03):
I think that most of these names are already in very sensible namespaces. That alone will not solve the issue of having lemma names that are > 50 chars.
Gabriel Ebner (Oct 05 2020 at 11:17):
euclidean_projection.orthogonal_projection is definitely not in a useful namespace
Johan Commelin (Oct 05 2020 at 11:28):
Sure, that's true.
But I do think that this is orthogonal to getting shorter lemma names by having shorter definition names.
Johan Commelin (Oct 05 2020 at 11:29):
Also, not that for bundled morphisms, dot notation doesn't help.
Last updated: May 12 2021 at 08:14 UTC