Symbol for `Magma.op`

Stream: Equational

[Joachim Breitner]

This was discussed before, but maybe this wasn't considered: The syntax for ∘ clashes with the syntax for Function.comp. This is bad because it means at every ∘, both are tried, leading to exponential(?) slow-down. See for your self:

universe u

class Magma (α : Type u) where
  /-- `a ∘ b` computes a binary operation of `a` and `b`. -/
  op : α → α → α

@[inherit_doc] infixl:65 " ∘ "   => Magma.op


-- 48ms
abbrev Equation374794_a (G : Type u) [Magma G] := ∀ x y z : G, x = (((y ∘ y) ∘ y) ∘ x) ∘ ((y ∘ y) ∘ z)


@[inherit_doc] infixl:65 " • "   => Magma.op

-- 2ms
abbrev Equation374794_b (G : Type u) [Magma G] := ∀ x y z : G, x = (((y • y) • y) • x) • ((y • y) • z)

-- 1ms
abbrev Equation374794__C (G : Type u) [inst: Magma G] := ∀ x y z : G, x = inst.op (inst.op (inst.op (inst.op y y)  y) x) (inst.op (inst.op y y) z)

This is so slow that I built a custom elaborator for AllEquations, which is a bit silly. I conjecture that by using unambiguous notation, we can use normal lean syntax there, which is nicer, and makes it easier to copy’n’paste from there.

Also this extra cost is paid everywhere where people type in equations in lean.

Is this bad enough to justify switching? Is • (\bu) a good alternative?

[Adam Topaz]

I know that the project has explicitly avoided using Mul, and why. But using bundled objects was never discussed as a potential option. This would be an approach to avoid diamonds in examples (e.g. where the carrier is $\N$ and the operation is addition), and would allow reuse of standard stuff from mathlib. Since this discussion is already asking about changing notation, I figured it's worthwhile to bring it up.

Of course, using bundled objects doesn't solve the psychological issue that $*$ is usually expected to be associative, but I hope that's something we can deal with :)

[Adam Topaz]

Note that we already have docs#MagmaCat in mathlib

[Michael Stoll]

Joachim Breitner said:

Is this bad enough to justify switching? Is • (\bu) a good alternative?

Would this not clash with scalar multiplication?

[Joachim Breitner]

At least not when using plain lean :-). But yes, probably not mathlib-compatible. Any available operator? Or just use Mul and be done with it ( :fingers_crossed: that the HMul-indirection doesn’t hurt)

[Shreyas Srinivas]

I have been wrestling with this question for a while. I found \oo has not been used. But there has to be a better scoping solution for this

[Michael Stoll]

Is ∗ (\ast) used (or ⁎ (\asterisk); I guess one of them is multiplciation)? ⊙ (\odot), ◆ (\dlb), ◇ (\diw) ◈ (\di.) etc.

[Shreyas Srinivas]

Otherwise Mathlib just gobbles up all useful notation

[Joachim Breitner]

grep finds

scoped infix:30 " ∗ " => Coprod

[Shreyas Srinivas]

\oo gives ⊚

[Adam Topaz]

Joachim Breitner said:

grep finds

scoped infix:30 " ∗ " => Coprod

This is the free product construction (aka the coproduct in the category of monoids/groups)

[Michael Stoll]

`⊙`: the Hadamard product `Matrix.hadamard`;

The next two (◆ and ◇)seem to be available...

[Shreyas Srinivas]

\oo has a small circle inside, instead of a dot in \odot

[Michael Stoll]

./CategoryTheory/Category/Basic.lean:local notation g ` ⊚ `:80 f:80 := category.comp f g    -- type as \oo

[Michael Stoll]

But it is local, so should not be a problem...

[Michael Stoll]

However, there is also stuff in Data and Control...

[Shreyas Srinivas]

Yes so I tried the following test : on live lean

import Mathlib

#check (· ⊚ ·) -- Error. Yay

[Shreyas Srinivas]

I wish notation was local by default

[Shreyas Srinivas]

Alternatively an overload keyword that automatically found the right priority number and locally overloaded a global notation

[Daniel Weber]

One option is having elements of the magma coerce to a function G -> G

[Terence Tao]

I just wanted to say that I am not strongly attached to the \circ symbol as the Lean implementation for magmas (which need not be the same as the blueprint implementation), so if there is a consensus to shift to a different symbol, I would be fine to shift it now while the project is still small enough that a refactor is feasible.

Certainly aligning with existing Mathlib notation makes sense to me as long as it does not deter casual Lean users from being able to contribute to the project. In the very early stages pf the project it was possible to display proofs in the Lean playground but we are probably well beyond that stage now (unless we can create a dedicated playground for this project)

[Terence Tao]

/poll What is your preferred symbol for the magma operation? Feel free to add an option not listed already
∘ (\circ), the current implementation
*, so that [Magma] is essentially [Mul]
No symbol (juxtaposition)

[Terence Tao]

Ack, the * symbol in the second option got eaten, and I don't know how to edit the poll or even to remove it. Is there a way to deal with this?

[Edward van de Meent]

afaik polls can't be edited, and options can't be removed... so i'll add a new option

[Andrés Goens]

I'm curious of option 3 (justaposition), how possible would that even be technically (because then there's no function application)?

[Terence Tao]

/poll ASSUMING the magma operation is changed to *, how should [Magma] and [Mul] be related?
[Magma] is an alias of [Mul] (e.g., using abbrev)
[Magma] is deleted, and [Mul] used exclusively
[Magma] is a separate class from [Mul], but constructors and API are in place to convert from one to the other

[Shreyas Srinivas]

I voted for 3, but I'd there was an option, I would say that it depends on your end goal. If you are okay with piggy backing off mathlib theorems, then using Mul is the better choice. If you wish to track the chain of rewrites/implications in your proof and specific kinds of theorems you use (for e.g the theorems with equation_attribute), using your own version of Magma might be convenient

[Shreyas Srinivas]

If you want to prove syntactic meta theorems then the FreeMagma and MagmaLaw approach is the best.

Lastly, there is always the option of manually lifting between them. By manually, I mean not using coercion typeclasses implicitly.

[Terence Tao]

I am more interested in maximizing the number of implications proven than trying to do meta analysis of the various proofs provided, but if there is a way to do have the best of both worlds that would be great. We are going to have many metatheorems piggybacking off of mathlib so it is going to be hard to have a purely mathlib free subset of proofs in any case. (But I imagine it should not be too difficult a posteriori to convert Mathlib-reliant proofs to Mathlib-free proofs in many if not all cases, given how simple each proof should be.)

[Floris van Doorn]

We can set priority on notations, right? Can't we just set the priority for Magma.op higher than for Function.comp so that we only try the former? I think it's a tiny loss to not be able to use the notation for Function.comp.

[Terence Tao]

You could add that as another option to the first poll if that is your preferred solution. This would keep the minor psychological advantage of not suggesting associativity, but be less compatible with [Mul]. (Or we can just assume that we would do this in the first option, as it seems like a no brainer)

[Floris van Doorn]

I'm also fine with using *, it's just not necessary if all we want is to avoid overloading.

[Terence Tao]

Floris van Doorn said:

I'm also fine with using *, it's just not necessary if all we want is to avoid overloading.

Actually * has worse overloading issues than \circ. If eg you want to put an unusual magma structure on Nat you have to wrap Nat in another class to avoid a notation clash or instance diamond, especially if we identify Magma and Mul

[Adam Topaz]

Is using docs#MagmaCat off the table?

[Adam Topaz]

I guess that essentially falls under the second choice.

[Terence Tao]

ooh I forgot about that, you can add that as an additional poll option. My one concern is whether this makes formalization more difficult for casual Lean users with no expertise in Categories, or whether it is mostly invisible at the front end.

[Shreyas Srinivas]

I already used notation priority on one of the PRs I was helping with

[Shreyas Srinivas]

The problem is ofc when you want to also use function composition notation as is

[Adam Topaz]

No category theory is necessary, you can still write

import Mathlib

example (M : MagmaCat) : Prop := ∀ (x y z : M), (x * y) * z = x * (y * z)

[Adam Topaz]

And also

import Mathlib

example (M N : MagmaCat) : Type _ := M →ₙ* N

[Adam Topaz]

In any case, I added it as an option

[Shreyas Srinivas]

Why not make a Mul instance of FreeMagma in a separate file and import it only when it is necessary to use Mathlib theorems of Mul?

[Adam Topaz]

If the Cat in MagmaCat is intimidating, we could add alias Magma := MagmaCat so that Magma would become the type of all Magmas

[Joachim Breitner]

Is there a chance that we are overthinking this? There exists a type class in Lean core that has exactly the operation we want, with a nice-looking and convenient to type symbol. Let's just use it and move on. We can still use the Magma abbrev to make nice theorem statements.

[Terence Tao]

Are there any practical advantages of “G: MagmaCat” over “(G: Type *) [Mul G]”? (Sorry can’t do backticks on my phone)

[Adam Topaz]

The only real practical advantage is that it lets you avoid diamonds. For example here is $\N$ with the Magma structure given by addition:

example : MagmaCat where
  α := ℕ
  str := .mk (·+·)

[Adam Topaz]

Of course it's possible to do this in an unbundled way as well, e.g. as follows:

import Mathlib

def M := ℕ
instance : Mul M where mul := show ℕ → ℕ → ℕ from (·+·)

[Adam Topaz]

But it can be cumbersome to define the Mul instance, as you can see.

[Terence Tao]

Perhaps a concrete example will help clarify the issue. Consider the following counterexample currently formalized in Subgraph.lean:

 @[equational_result]
theorem Equation43_not_implies_Equation4512 : ∃ (G: Type) (_: Magma G), Equation43 G ∧ ¬ Equation4512 G := by
  let hG : Magma ℕ := { op := fun x y ↦ x * y + 1 }
  refine ⟨ℕ, hG, fun _ _ ↦ ?_, ?_⟩
  . dsimp [hG]
    ring
  · by_contra h
    specialize h 0 0 1
    simp [hG] at h

1. What would the analogous proof be if we used Mul G instead of Magma G (redefining Equation43 and Equation 4512 accordingly, of course)? Note the potential instance diamond since ℕ already has an (incompatible) [Mul ℕ] structure, which is in fact being used to construct the magma.

2. What would the analogous proof be if we used MagmaCat instead of Magma G (redefining Equation43 and Equation 4512 accordingly, of course)?

[Andrés Goens]

this works:

abbrev Mul.Equation43 (G: Type _) [Mul G] := ∀ x y : G, x * y = y * x
abbrev Mul.Equation4512 (G: Type _) [Mul G] := ∀ x y z : G, x * (y * z) = (x * y) * z

theorem Mul.Equation43_not_implies_Equation4512 : ∃ (G: Type) (_ : Mul G), Mul.Equation43 G ∧ ¬ Mul.Equation4512 G := by
  let hG : Mul ℕ := { mul := fun x y ↦ Nat.mul x y + 1 }
  refine ⟨ℕ, hG, fun _ _ ↦ ?_, ?_⟩
  . dsimp [hG, HMul.hMul, instHMul]
    have mul_comm := Nat.mul_comm
    dsimp [HMul.hMul] at mul_comm
    rw [mul_comm]
  · by_contra h
    specialize h 0 0 1
    simp [HMul.hMul, instHMul, hG] at h

Wouldn't claim it's nice though, it feels like an argument against Mul: HMul gets in the way a lot, and ring doesn't pick up on the commutative ring instance if we override Mul, and even stuff like commutativity of multiplication in Nat is stated using Mul so we have to "unpack" everything.

[Oliver Nash]

The above commits the sin of endowing ℕ with two Mul instances. You can avoid doing this by operating in a type-correct way as follows:

theorem Equation43_not_implies_Equation4512 :
    ∃ (G : Type) (_ : Mul G),
      (∀ x y : G, x * y = y * x) ∧ ¬ (∀ x y z : G, x * (y * z) = (x * y) * z) := by
  obtain ⟨G, ⟨e⟩⟩ : ∃ G : Type, Nonempty (G ≃ ℕ) := ⟨ℕ, ⟨Equiv.refl _⟩⟩
  let _i : Mul G := ⟨fun x y ↦ e.symm (e x * e y + 1)⟩
  have he (x y : G) : x * y = e.symm (e x * e y + 1) := rfl
  refine ⟨G, _i, fun x y ↦ ?_, ?_⟩
  . simp [he, mul_comm]
  · push_neg
    refine ⟨e.symm 0, e.symm 0, e.symm 1, ?_⟩
    simp [he]

[Eric Wieser]

Another option would be to provide some global

structure Wrapper (T : Type*) where val : T

and then use Wrapper ℕ whenever you want to define a theorem-local magma with a nat representation

[Eric Wieser]

Then e.symm and e above become .mk and .val or \<> and .1

[Andrés Goens]

the above was also type-correct btw, just ugly

[Terence Tao]

It seems that if we are to refactor [Magma] to [Mul] (or MagmaCat), we will need some consensus on what the best practices are for writing proofs and provide some examples. The examples provided above are, I feel, a bit trickier for a casual Lean user to create than the [Magma] based proof, for instance many potential contributors may not know the nuances of Equiv.

The fact that the move from [Magma] to [Mul] breaks tactics such as ring is a little concerning for me. Does the MagmaCat refactor fare any better in this regard?

[Terence Tao]

I just wanted to add that in the prehistory of this project (i.e., last week), I did initially start with [Mul G] but ran into all the instance diamond issues that @Andrés Goens also encountered, which is why I ended up moving to a different class [Magma G] with a different operation symbol.

I would like to offer two additional arguments to retain [Magma G] instead of [Mul G]. One is speed: as [Magma G] has a lot less API than [Mul G], there could be some small speed savings in compiling [Magma]-based proofs, which could add up as we collect millions of proofs of implications (although it seems right now the Lean compiler is not the bottleneck for the project.)

The other is that I do think that while [Magma G] and [Mul G] are syntactically isomorphic, I would argue that they are conceptually distinct. I already mentioned one distinction that [Mul G] operations would be expected to be associative, while [Magma G] operations have no such expectation. But the other conceptual distinction is that [Mul G] is expected to be the canonical multiplication operation on G, if one exists. In contrast, [Magma G] is not expected to be the canonical multiplication operation, and can then be used for some other operation not related to multiplication (though of course if one wants to study two such non-canonical operations, one still has instance diamond issues, but thankfully we are unlikely to encounter such a situation here, except possibly when studying duality in which it makes sense to reverse the order of the magma operation).

Perhaps a compromise is to leave [Magma G] largely in its current form, but include some API to coerce a [Magma G] type to a [Mul G] type and vice versa?

[Oliver Nash]

FWIW we do have non-associative Mul-bearing types in Matlhib already, e.g., docs#FreeNonUnitalNonAssocAlgebra and docs#FreeMagma

[Joachim Breitner]

If we stick to Magma, then we are maybe back to the original question: Which symbol to use?

[Andrés Goens]

to be fair, I don't find the (original) proof of Equation43_not_implies_Equation4512 to be terribly accessible either, not sure if the casual Lean user would find that one so much better. That being said, I still think the other arguments are strong enough to keep Magma instead of Mul (in my opinion).

[Terence Tao]

Joachim Breitner said:

If we stick to Magma, then we are maybe back to the original question: Which symbol to use?

I thought the proposal to retain ∘ but give it a higher priority than function composition seemed to cover most use cases. There are very few situations I can think of where we would have a [Magma G] that (a) already has a native function composition operation, and (b) we would want to actually use that function composition operation. In such rare cases we could do a wrapper-based solution similar to what has been proposed above for [Mul G].

[Joachim Breitner]

If that solves the technical issues with \circ, then sounds good to me.

[Martin Dvořák]

I didn't vote on the main issue; just one thing I want to say:
In the current implementation of Magma we have infix:65 " ∘ " => Magma.op as the operator, which does not hide any parenthesis in the Infoview. If we switch to Mul from Mathlib, we will obtain infixl instead of infix, and I don't know if it can be overriden with the variant that preserves parentheses like (x * y) * z in the Infoview.

[Terence Tao]

It does not appear that we have consensus on how to perform the transition from [Magma G] to [Mul G] that minimizes technical challenges for future users. As such, I am going to declare that we keep the status quo, though I have added equational#234 to create coercion API between [Magma] and [Mul] in case we need it and to elevate the priority of \circ. However, I will keep this thread open if there are people who wish to continue advocating for more drastic changes.

[David Renshaw]

I believe that a big part of CI wait times is currently traceable to the ∘ symbol having slow elaboration.

[David Renshaw]

My feeling is that we should use something that does not already have meaning, like the star symbol ⋆.

[David Renshaw]

When I try setting the priority higher like this

infix:10000 " ∘ " => Magma.op

that seems to break things

[Joachim Breitner]

Isn't that precedence, not priority?

[Joachim Breitner]

I.e. how to resolve a * b + c, not which syntax declaration to apply?

[David Renshaw]

I think you are correct. How do I set priority then?

[Joachim Breitner]

No idea, not my area of expertise I fear. Not even sure it exists, but I think someone else said it's possible?

[Shreyas Srinivas]

notation:precedence (priority:= 1200) ...

[Shreyas Srinivas]

infixl:65 (priority := 1100)" ∘ " => Magma.op

[Terence Tao]

Hmm, if one can empirically test (say on some test branch) the hypothesis that changing the symbol to a unique symbol significantly improves CI run time then that for me is a good reason to refactor (even if it means changing a lot of the current code).

[Shreyas Srinivas]

Whether priority can become a headache depends on how the parser uses priority. Does it check all notation defs for each occurrence of a symbol or does it precompute some notation table for each namespace?

[David Renshaw]

Homomorphisms.lean has some uses of \circ as function composition, and they break if I do

infix:65 (priority := 1100) " ∘ " => Magma.op

[Terence Tao]

Note that equational#234 is an open PR to elevate the priority of \circ, and implemented these fixes. I'm hoping this is a viable solution, but changing the operation symbol may be an even better fix perhaps.

[David Renshaw]

hm, I see that FreeMagma.lean is already using the star symbol.

[Terence Tao]

I've gone ahead and approved equational#234 for now as a provisional solution at least, but keep the discussion going here for any improved solution. Implementing star as the default magma operation (and making suitable adjustments to FreeMagma as a consequence) seems like a reasonable option; I assume star doesn't conflict with any existing global notation in Mathlib?

[Eric Wieser]

Here's an example of what using Mul could look like:

import Mathlib

@[ext]
structure NewType (α : Type u) where val : α

/-- A helper to build a new `Mul` instance on an underlying representation -/
abbrev Mul.onNewType {α} (f : α → α → α) : Mul (NewType α) where
  mul x y := ⟨f x.1 y.1⟩

/-- The reflexive law -/
abbrev Equation1 (G: Type _) [Mul G] := ∀ x : G, x = x

/-- The singleton law -/
abbrev Equation2 (G: Type _) [Mul G] := ∀ x y : G, x = y

theorem foo : ¬ Equation1.{0} ≤ Equation2 := by
  intro h
  specialize @h _ (.onNewType fun x y : Nat => x + y) (fun x => ?_)
  rfl
  specialize h ⟨1⟩ ⟨2⟩
  cases h

[David Renshaw]

I now have a branch that changes the op symbol from \circ to \di (diamond).

[David Renshaw]

I observed the time for a fresh build to go down from ~8 minutes (before equational#240 was applied) to ~1 minute 20 seconds.

[David Renshaw]

The merge of equational#240 broke the build.

[Andrés Goens]

that's a huge speedup! why would the symbol make such a difference?

[Andrés Goens]

is it because of some typeclass in the background?

[David Renshaw]

\circ already means Function.comp, so I guess unification has more possibilities to explore

[David Renshaw]

equational#249 is a big intrusive diff that changes the symbol everywhere to ◆

[David Renshaw]

I chose that symbol because it does not appear in mathlib, but is easy to type ("\di").

[David Renshaw]

I don't want to just steam-roller this change without any buy-in, but it does appear to me to be a simple way to get a very noticeable performance increase.

[David Renshaw]

... without breaking the existing Funciton.comp symbol

[David Renshaw]

The reason that equational#240 broke the build is that some stuff in Homomorphism.lean started using Function.comp \circ after equational#240 was created.

[David Renshaw]

The more minimal change would be to fix up those instance to avoid \circ.

[David Renshaw]

heh, or just revert it

[Terence Tao]

OK I have reverted equational#240 since it seems to likely be largely redundant (or need significant refactoring) after equational#249 . It also had a separate component which was to create some scoped instances between [Add], [Mul], and [Magma] but those can be re-inserted later after we sort out the symbol issue

[Terence Tao]

/poll What symbol should we use for the Magma operation?
∘ (\circ) - current implementation, conflicts with function composition

• • conflicts with [Mul]
    ◆ (\di)
    ⊙ (\odot)
    ◇ (\diw)
    ⊚ (\oo)

[Terence Tao]

Starting a poll again. And I see that I again messed up with the * option, though I think this option was unviable anyway.

[David Renshaw]

There is also the smaller hollow diamond ⋄ (\diamond), but that's a lot to type

[Terence Tao]

It wasn't clear to me whether the Hadamard product use of \odot gives it the same unification issue as \circ

[Shreyas Srinivas]

My vote for \oo is because I am certain it isn't used globally in mathlib

[Shreyas Srinivas]

I mean in a globally visible way

[David Renshaw]

I have updated equational#249 to use ◇, which I am reasonably happy with.

[David Renshaw]

I found ◆ to be somewhat grating on the eyes.

[David Renshaw]

• ◆ (\di) Screenshot from 2024-10-03 18-07-37.png
  
• ⊙ (\odot) Screenshot from 2024-10-03 18-06-43.png
  

[David Renshaw]

• ◇ (\diw) Screenshot from 2024-10-03 18-04-45.png
  
• ⊚ (\oo) Screenshot from 2024-10-03 18-05-50.png
  

[David Renshaw]

\odot and \oo are both used in mathlib, but qualfied as local or scoped, so there should be no issue. Neither \di no \diw show up in mathlib at all.

[Floris van Doorn]

In equational#254 I recovered the part of equational#240 that doesn't break stuff

[David Renshaw]

equational#249 passed CI. I think we should merge it. If any objections come up, it'll be easy enough to do another find and replace.

[Shreyas Srinivas]

Okay I will do it now

[Shreyas Srinivas]

If the CI fails we can revert it

[Floris van Doorn]

I merged master in equational#254 4 minutes ago and acquired a new (easy) merge conflict :-)

[Floris van Doorn]

(though most PRs just got merge conflicts, probably)

[Shreyas Srinivas]

I count 4 linked pull requests including yours

[Floris van Doorn]

David Renshaw said:

I observed the time for a fresh build to go down from ~8 minutes (before equational#240 was applied) to ~1 minute 20 seconds.

Maybe that was just a caching thing? The latest build (with the new Magma.op symbol) takes 7 minutes.

[David Renshaw]

on CI? that's not going to have as much parallelism as I have here.

[David Renshaw]

I did git clean -xffd and then lake exe cache get and then time lake build

[Floris van Doorn]

Yes, this was CI: https://github.com/teorth/equational_theories/actions/runs/11170684792/job/31053976339
Didn't realize you spoke about local build time.

[Floris van Doorn]

Shreyas Srinivas said:

I count 4 linked pull requests including yours

It might be prudent for other PRs to also merge master if they changed any Lean. If they used the old Magma.op notation, the build will break after merging

[Shreyas Srinivas]

Will it be simpler to handle the merge conflict if they all rebase on master and squash?

[Floris van Doorn]

it would be useful if they all merge (or rebase if you prefer) master main and see if CI still builds

[Shreyas Srinivas]

Yeah that I agree. But, especially if they are auto-generating large numbers of lemmas, I expect the merge conflict handling to be painful

[Shreyas Srinivas]

Hopefully I can notify the authors by tagging them here

[Shreyas Srinivas]

No that doesn't work. I don't know Jeremy Scanvic's zulip id

[Floris van Doorn]

If the merge conflict is with just equational#249 it's easy. Just run git merge origin -X ours (if there is an actual merge conflict) and then do a single search+replace from ∘ to ◇

[Floris van Doorn]

If you want you could manually merge their PRs with main (assuming they enabled you to push to their PRs)

[Floris van Doorn]

It would be nice if Github would have a button "merge with latest version" that you could just press, instead of git remote add + git checkout + git merge + git push.

[Shreyas Srinivas]

No that doesn't work. I don't know Jeremy Scanvic's zulip id

[Shreyas Srinivas]

@Franklin Pezzuti Dyer : your PRs equational#122 and equational#155 are likely to have merge conflicts due to the notation change for the magma operation (tl Dr; CI runs much faster)

[Shreyas Srinivas]

Could you try merging main into your PR branches and use Floris's suggestion above if you run into difficulties?

[Shreyas Srinivas]

Floris van Doorn said:

It would be nice if Github would have a button "merge with latest version" that you could just press, instead of git remote add + git checkout + git merge + git push.

That would leave the local repository still in its old state and users will still have to deal with the merge conflict there

[Floris van Doorn]

Maybe a repo admin can set the default commit message when merging PRs to pull request title and description? Then I don't have to worry about my commit messages in my PRs. (as is the default for Mathlib.)
Can be toggled in https://github.com/teorth/equational_theories/settings
image.png

[Terence Tao]

A secondary question: should we also change the human-readable portions of the project (the blueprint, README, some .txt files, etc.) to reflect this new notation change?

[Shreyas Srinivas]

I think that's already the case?

[Shreyas Srinivas]

Shreyas Srinivas said:

Floris van Doorn said:

It would be nice if Github would have a button "merge with latest version" that you could just press, instead of git remote add + git checkout + git merge + git push.

That would leave the local repository still in its old state and users will still have to deal with the merge conflict there

To add to this: github's git is no smarter than the local git, so users will have to resolve the merge conflict on GitHub as well

[Shreyas Srinivas]

Floris van Doorn said:

Maybe a repo admin can set the default commit message when merging PRs to pull request title and description? Then I don't have to worry about my commit messages in my PRs. (as is the default for Mathlib.)
Can be toggled in https://github.com/teorth/equational_theories/settings
image.png

I think this is already the default?

[Floris van Doorn]

Shreyas Srinivas said:

To add to this: github's git is no smarter than the local git, so users will have to resolve the merge conflict on GitHub as well

Sure, but the button would be helpful for all PRs that have no git merge conflict (but might have a semantic merge conflict)

[Terence Tao]

I think I managed to change the default commit message. Have to go offline now for about an hour

[Floris van Doorn]

Shreyas Srinivas said:

Floris van Doorn said:

Maybe a repo admin can set the default commit message when merging PRs to pull request title and description? Then I don't have to worry about my commit messages in my PRs. (as is the default for Mathlib.)
Can be toggled in https://github.com/teorth/equational_theories/settings
image.png

I think this is already the default?

Maybe; it wasn't the commit messages generated for https://github.com/teorth/equational_theories/commit/11a1831c8bf7cebb3391669afe102d693e96962a

[Shreyas Srinivas]

Terence Tao said:

A secondary question: should we also change the human-readable portions of the project (the blueprint, README, some .txt files, etc.) to reflect this new notation change?

I don't think the README is affected. The blueprint is likely to be the biggest place where change is needed. I suggest using a latex variable for the magma operation in the latex blueprint to ensure that future changes only have to happen at one place.

[Terence Tao]

OK, I have pushed a blueprint change (equational#257) along the lines you indicated. There are several legacy text files that use \circ but changing them over is low priority (unless they are somehow used as input for various pieces of code that might now transfer over).

[Vlad Tsyrklevich]

Wow, this is a big speed-up. Previously I was worried about adding files that were 'too slow' and thought I should really prune away past theorems that are unused in the current transitive reduction, but this has removed that concern entirely.

[Terence Tao]

OK, I am glad that the temporary disruption was worth the long term gain!

[Martin Dvořák]

In order to balance the meta, we should invent a new mathematical structure and call it "Aqua".
Obviously 💧 will be the infix operator.

[Edward van de Meent]

while we're at it, let's add Terra, Aer and Aether too :grinning_face_with_smiling_eyes: