reorganization for `omega`

Stream: batteries

[Kim Morrison]

It's been suggested that I try a reorganization in Std to make it possible to use omega earlier, e.g. in Std.Data.Int.Lemmas, or even earlier. Because omega needs various lemmas about Nat and Int, this would involve some annoying reorganization.

I just did a little experiment, and determined that I currently need about 1/4 of Std.Data.Int.Lemmas in omega (presumably this could be shrunk: this is just the fraction that can't be deleted with breaking something).

I worried it would be pretty unsatisfactory to split Std.Data.Int.Lemmas into two files solely on the criterion "does omega want this"...

An alternative would be to copy and paste that 1/4 of Std.Data.Int.Lemmas into a private namespace inside omega, and not worry about the duplication. Not ideal either!

[Kim Morrison]

@Mario Carneiro, any thoughts?

[Mario Carneiro]

I think splitting big files is a good idea, big files (especially if there is a significant difference in prerequisites between the top half and the bottom half) are a major contributing factor to unnecessary imports, and even if all the theorems are independent it's a good idea to split files for additional parallelism

[Kim Morrison]

Okay, maybe I will hack at Std.Data.Int.Lemmas for a bit more.

[Mario Carneiro]

although one can conversely argue that this would add Omega as a big additional dependency of half of Std.Data.Int.Lemmas

[Kim Morrison]

Yes...

[Mario Carneiro]

I can't wait for us to be able to ship precompiled omega just like we ship precompiled simp

[Kim Morrison]

For now I will just see if I can find any reasonable splits, without actually importing omega anywhere new.

[Kim Morrison]

If you want that then I would be copy-pasting what I need out of Std into omega.

[Mario Carneiro]

what is "that"?

[Mario Carneiro]

oh you mean that if we precompiled omega in a separate library then half of Std.Data.Int.Lemmas would also be in that lib

[Kim Morrison]

Yes.

[Mario Carneiro]

ultimately I think we want to just precompile all of std

[Kim Morrison]

Definitely.

[Mario Carneiro]

so I won't make a big fuss about using omega in std

[Kim Morrison]

std4#534 is my initial attempt at a split of Std.Data.Int.Lemmas, but doesn't involve omega at all yet.

[Kim Morrison]

(ooh, great milestone, 534 is the best siteswap)

[Mario Carneiro]

what's this reference?

[Kim Morrison]

https://juggle.fandom.com/wiki/534

[Kim Morrison]

"siteswaps" is the bijection between (certain) juggling patterns and S_n x N^n.

[Kim Morrison]

And 534 is "the best" because it is fairly difficult but learnable by mortals, but possibly no one would have ever thought to try it without knowing this bijection first. :-)

[Eric Rodriguez]

What's the situation with precompiled tactics etc at the current moment?

[Eric Wieser]

Mario Carneiro said:

I can't wait for us to be able to ship precompiled omega just like we ship precompiled simp

Does this affect dependency considerations, or is it just a really-nice-to-have tangent?

[Mario Carneiro]

It lowers the cost of having dependencies. Lean itself is a pretty big dependency and the only reason we can use it (mostly) freely is because it is precompiled