Zulip Chat Archive

Stream: PR reviews

Topic: lean#211 don't unfold irred defs


view this post on Zulip Johan Commelin (May 04 2020 at 14:51):

Continuing discussion from https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/witt.20vectors

I suppose this PR might be somewhat controversial.

  1. It seems that it breaks mathlib in ways where before we could get away with _ and let Lean figure it out, but now we need to supply data ourselves.
  2. It's not yet clear whether this will give a speedup of slowdown of the build.
  3. Without this PR, it seems that Witt vectors are "doomed".

view this post on Zulip Kevin Buzzard (May 04 2020 at 14:53):

Are any of the core Lean experts in a position to explain why the PR makes Lean more stupid, and whether anything can be done about this stupidity whilst still enabling the Witt vectors work to compile in a reasonable amount of time?

view this post on Zulip Patrick Massot (May 04 2020 at 14:54):

I'm very worried by everything I read on this topic. I have no idea what is a Witt vector, so I guess I don't care about them. I care very much about Lean not being stupid.

view this post on Zulip Kevin Buzzard (May 04 2020 at 14:54):

Witt vectors are just a completely normal piece of algebra.

view this post on Zulip Kevin Buzzard (May 04 2020 at 14:56):

They solve the following problem. Given the ring Z/pZ, we want to define Z/p^2Z as a set by (Z/pZ)^2, and now we have to figure out how to define addition on it, so we need functions which send (a,b) in Z/pZ to 0 if a+b<0 and 1 if a+b>=p (the "carry digit"). This problem is solved by Witt polynomials, and Witt vectors are just (Z/pZ)^n with this structure of addition and multiplication. It all generalises to a large class of perfect fields.

view this post on Zulip Kevin Buzzard (May 04 2020 at 14:56):

Mathematically there is absolutely nothing remarkable about it.

view this post on Zulip Kevin Buzzard (May 04 2020 at 14:57):

You can take some limit of them, and then construct the p-adic integers Z_p from its residue field Z/pZ

view this post on Zulip Kevin Buzzard (May 04 2020 at 14:57):

Doing it with other finite fields builds a really interesting (to an arithmetician) class of complete discrete valuation rings.

view this post on Zulip Johan Commelin (May 04 2020 at 14:58):

Over at the Witt vectors topic, they seem to discuss this PR.
Here, on the topic of some technical PR, people discuss Witt vectors
/me rolls on the floor

view this post on Zulip Kevin Buzzard (May 04 2020 at 14:59):

If you start with the p-adic numbers, take an algebraic closure, take the ring of integers, reduce it mod p, perfect it, and then take the Witt vectors and invert p, you have made Fontaine's field B_{dR}, which you (Patrick) once told me was a ridiculous goal (in terms of getting Antoine to formalise it ;-) ), but actually you can see how close we are :-)

view this post on Zulip Reid Barton (May 04 2020 at 14:59):

Did someone try fixing all the errors in mathlib yet, or are we just guessing that they look pretty innocuous?

view this post on Zulip Kevin Buzzard (May 04 2020 at 15:00):

The first one looked innocuous, so by induction we should be OK.

view this post on Zulip Kevin Buzzard (May 04 2020 at 15:00):

and induction usually works great in Lean

view this post on Zulip Johan Commelin (May 04 2020 at 15:03):

I've never built C++ Lean before.

view this post on Zulip Johan Commelin (May 04 2020 at 15:03):

Let me try to do that, and try to fix mathlib.

view this post on Zulip Bryan Gin-ge Chen (May 04 2020 at 15:04):

I'm looking at them now. I've been able to fix the non-category theory ones so far.

view this post on Zulip Bryan Gin-ge Chen (May 04 2020 at 15:04):

I'll push what I have to a branch shortly.

view this post on Zulip Kevin Buzzard (May 04 2020 at 15:04):

So did filling in the _ with x * y in the algebra/opposite file solve that first problem?

view this post on Zulip Bryan Gin-ge Chen (May 04 2020 at 15:05):

For some reason x * y didn't work (maybe more coercions were needed somewhere), but _ * _ did.

view this post on Zulip Reid Barton (May 04 2020 at 15:06):

How about another question: do we understand why these places broke? Or at least one of them?

view this post on Zulip Bryan Gin-ge Chen (May 04 2020 at 15:06):

I don't!

view this post on Zulip Reid Barton (May 04 2020 at 15:09):

Hmm, interesting. So this one looked fairly simple:

/mathlib/src/data/real/hyperreal.lean:591:11: error: "eliminator" elaborator type mismatch, term
  is_st_add
has type
  is_st ?m_1 ?m_2  is_st ?m_3 ?m_4  is_st (?m_1 + ?m_3) (?m_2 + ?m_4)
but is expected to have type
  infinitesimal x  infinitesimal y  infinitesimal (x + y)

view this post on Zulip Reid Barton (May 04 2020 at 15:09):

def infinitesimal (x : *) := is_st x 0

view this post on Zulip Reid Barton (May 04 2020 at 15:10):

Presumably this was ultimately relying on the fact that (0 : ℝ) + 0 = 0!

view this post on Zulip Reid Barton (May 04 2020 at 15:10):

lemma is_st_add {x y : *} {r s : } : is_st x r  is_st y s  is_st (x + y) (r + s)

view this post on Zulip Reid Barton (May 04 2020 at 15:11):

lemma infinitesimal_add {x y : *} :
  infinitesimal x  infinitesimal y  infinitesimal (x + y) :=
zero_add 0  is_st_add

view this post on Zulip Reid Barton (May 04 2020 at 15:11):

It's almost like @[irreducible] is an obscure feature that nobody really understands??

view this post on Zulip Johan Commelin (May 04 2020 at 15:12):

Certainly I don't

view this post on Zulip Gabriel Ebner (May 04 2020 at 15:14):

It doesn't help that Lean ≤3.10 unfolds irreducible definitions in lots of unexpected places. When checking whether two types are definitionally equal (e.g. when assigning metavariables). When inferring types. When checking that a type is a pi-type, etc.

view this post on Zulip Bryan Gin-ge Chen (May 04 2020 at 15:15):

Here's the branch: https://github.com/leanprover-community/mathlib/tree/lean_pr_211

After you build the PR branch from lean#211, use elan toolchain link local <path/to/lean/> and then the above branch should pick up the new version of Lean.

view this post on Zulip Gabriel Ebner (May 04 2020 at 15:18):

I feel a bit uncomfortable only changing the transparency in a single place. Should we change it to semireducible everywhere? This is how it is in Lean 4.

view this post on Zulip Johan Commelin (May 04 2020 at 15:19):

@Bryan Gin-ge Chen How do I undo that elan change when I'm done?

view this post on Zulip Reid Barton (May 04 2020 at 15:20):

Gabriel Ebner said:

I feel a bit uncomfortable only changing the transparency in a single place. Should we change it to semireducible everywhere? This is how it is in Lean 4.

We should at least try it I think.

view this post on Zulip Reid Barton (May 04 2020 at 15:21):

Some of these other errors, like the ones in geometry/manifold/real_instances.lean:217, are more mysterious

view this post on Zulip Bryan Gin-ge Chen (May 04 2020 at 15:21):

@Johan Commelin The elan command just creates a new toolchain which you should be able to remove with elan toolchain uninstall. It shouldn't affect anything else unless you've already got a toolchain named local.

view this post on Zulip Johan Commelin (May 04 2020 at 15:22):

Ok, so should I also change the .toml?

view this post on Zulip Johan Commelin (May 04 2020 at 15:23):

Ooh, maybe you already did.

view this post on Zulip Johan Commelin (May 04 2020 at 15:23):

(I'm at 70% of the Lean build) :fencing:

view this post on Zulip Reid Barton (May 04 2020 at 15:23):

The toml is changed.

view this post on Zulip Bryan Gin-ge Chen (May 04 2020 at 15:23):

I've updated the gist with the errors, marking the few I was able to fix. I won't be able to work on this until later tonight, so feel free to push arbitrary changes to either the Lean PR branch or the mathlib branch.

view this post on Zulip Gabriel Ebner (May 04 2020 at 15:24):

Another cool elan trick: if you don't want to change the toml, you can run elan override set .... in the mathlib directory where you want a different lean.

view this post on Zulip Reid Barton (May 04 2020 at 15:26):

In particular several of these errors don't seem to have anything irreducible around, which is confusing

view this post on Zulip Gabriel Ebner (May 04 2020 at 15:26):

Can you point me to one of them?

view this post on Zulip Reid Barton (May 04 2020 at 15:26):

Oh whoops I forgot op has @[irreducible]

view this post on Zulip Reid Barton (May 04 2020 at 15:26):

Let me look harder

view this post on Zulip Reid Barton (May 04 2020 at 15:27):

Maybe src/data/pfun.lean:206?

view this post on Zulip Reid Barton (May 04 2020 at 15:29):

Or the ones in src/data/padics/padic_norm.lean? This file does import data.real.cau_seq but it's not obvious to me why (it doesn't seem to use the real numbers; padic_norm itself takes rational values)

view this post on Zulip Johan Commelin (May 04 2020 at 15:30):

How can I check that I'm running the correct Lean?

view this post on Zulip Gabriel Ebner (May 04 2020 at 15:30):

lean --version in the correct directory. Then check the git revision it prints.

view this post on Zulip Johan Commelin (May 04 2020 at 15:30):

Aah, right, thanks!

view this post on Zulip Johan Commelin (May 04 2020 at 15:31):

It seems to be ok

view this post on Zulip Gabriel Ebner (May 04 2020 at 15:31):

elan show will also tell you what "active toolchain" it uses

view this post on Zulip Reid Barton (May 04 2020 at 15:31):

or the ones in src/set_theory/cofinality.lean: the set_theory directory doesn't contain irreducible and it doesn't import much else, I think

view this post on Zulip Johan Commelin (May 04 2020 at 15:31):

What is the best way to build mathlib and stop at the first error?

view this post on Zulip Reid Barton (May 04 2020 at 15:32):

I use leanpkg build 2>&1 | less for this

view this post on Zulip Johan Commelin (May 04 2020 at 15:32):

But that just collects errors, right? It doesn't kill the build

view this post on Zulip Johan Commelin (May 04 2020 at 15:32):

But maybe that's fine

view this post on Zulip Reid Barton (May 04 2020 at 15:34):

I think the remaining errors either definitely involve something irreducible (opposite, real) or it seems like too much effort to figure out (data.polynomial?)

view this post on Zulip Reid Barton (May 04 2020 at 15:36):

Though, I don't understand specifically why some of the ones that do involve irreducible things failed, yet.

view this post on Zulip Johan Commelin (May 04 2020 at 15:38):

@Gabriel Ebner Would you mind pushing your suggested semireducibility changes to a branch on top of lean#211?

view this post on Zulip Gabriel Ebner (May 04 2020 at 15:39):

I think I understand a bit what happens in pfun: right now we also unfold proofs of theorems.

view this post on Zulip Johan Commelin (May 04 2020 at 15:39):

Then we can also build that version of Lean, and see how much mathlib likes that.

view this post on Zulip Johan Commelin (May 04 2020 at 15:39):

I'll be back after dinner.

view this post on Zulip Gabriel Ebner (May 04 2020 at 15:39):

Pushed.

view this post on Zulip Johan Commelin (May 04 2020 at 15:39):

Pushed where?

view this post on Zulip Gabriel Ebner (May 04 2020 at 15:40):

To the type_context_fix branch?

view this post on Zulip Johan Commelin (May 04 2020 at 15:40):

Ooh, I thought we might want both versions next to each other. But maybe not (-;

view this post on Zulip Johan Commelin (May 05 2020 at 08:15):

I fixed the opposite stuff in categories

view this post on Zulip Johan Commelin (May 05 2020 at 09:11):

Fixed the hyperreals

view this post on Zulip Johan Commelin (May 05 2020 at 09:15):

@Gabriel Ebner Could this also be implemented via set_option standard_reducibility blabla?

view this post on Zulip Johan Commelin (May 05 2020 at 09:16):

Then I could just switch that option on in the witt vector file, and the rest of mathlib doesn't have to care.

view this post on Zulip Gabriel Ebner (May 05 2020 at 09:17):

I think it's the right default. Irreducible definitions should not be unfolded, that's the explicit intention behind marking them as such. Besides, that's how it's going to be in :four_leaf_clover:, so we might as well get used to it now.

view this post on Zulip Johan Commelin (May 05 2020 at 09:27):

Ok... I'll try to fix as much as I can.

view this post on Zulip Johan Commelin (May 05 2020 at 09:28):

Note that in one of my fixes I cheated: I locally marked the definition as semireducible. But in my opinion the file was building API for the definition, so then it should be fine.

view this post on Zulip Johan Commelin (May 05 2020 at 09:31):

But some of the failure doesn't seem to have anything to do with irreducible defs.

view this post on Zulip Johan Commelin (May 05 2020 at 09:32):

Ooh, wait. It does.

view this post on Zulip Johan Commelin (May 05 2020 at 09:32):

There was an op somewhere :expressionless:

view this post on Zulip Gabriel Ebner (May 05 2020 at 09:32):

Lemmas are also irreducible. :smile: In some cases, Lean was able to infer arguments by unifying proofs of lemmas...

view this post on Zulip Johan Commelin (May 05 2020 at 09:37):

It broke on refine blabla _ _...

view this post on Zulip Johan Commelin (May 05 2020 at 09:40):

simp no longer solves

((cones_hom F  cones_inv F).app X c).app limits.walking_parallel_pair.zero 
      limits.limit.π (functor.of_function F.obj) j =
    ((𝟙 (functor.cones (diagram F))).app X c).app limits.walking_parallel_pair.zero 
      limits.limit.π (functor.of_function F.obj) j

view this post on Zulip Johan Commelin (May 05 2020 at 09:41):

We probably need some help from @Scott Morrison

view this post on Zulip Gabriel Ebner (May 05 2020 at 09:41):

Which file is this in?

view this post on Zulip Johan Commelin (May 05 2020 at 09:43):

category_theory/limits/shapes/constructions/limits_of_products_and_equalizers.lean

view this post on Zulip Johan Commelin (May 05 2020 at 09:43):

It seems that convert is brutal enough to replace the more refined refine. But the problem just shifts to the next line.

view this post on Zulip Johan Commelin (May 05 2020 at 09:44):

And there even convert gives up.

view this post on Zulip Johan Commelin (May 05 2020 at 09:46):

Which is not a surprise, because we went from 2 goals to 11 goals...

view this post on Zulip Johan Commelin (May 05 2020 at 09:48):

Gabriel Ebner said:

Lemmas are also irreducible. :smile: In some cases, Lean was able to infer arguments by unifying proofs of lemmas...

So secretly we could actually pull of the mathematicians trick of "by the object constructed in the proof of Theorem 5.4"...

view this post on Zulip Johan Commelin (May 05 2020 at 09:49):

We could even do it without saying anything!

view this post on Zulip Sebastien Gouezel (May 05 2020 at 09:52):

That's not just a trick, that's a very dirty trick.

view this post on Zulip Gabriel Ebner (May 05 2020 at 10:05):

category_theory/limits/shapes/constructions/limits_of_products_and_equalizers.lean uses pi.lift c.app : X ⟶ ∏ F.obj to fill in a goal of type unop X ⟶ ∏ F.obj. I guess @Scott Morrison needs to fix this properly.

view this post on Zulip Johan Commelin (May 05 2020 at 10:05):

@Gabriel Ebner I see that you also just locally mark things reducible?

view this post on Zulip Johan Commelin (May 05 2020 at 10:06):

I just pushed a fix of geometry/manifold/real_instances. It's quite dirty again.

view this post on Zulip Johan Commelin (May 05 2020 at 10:06):

--- a/src/geometry/manifold/real_instances.lean
+++ b/src/geometry/manifold/real_instances.lean
@@ -213,8 +213,10 @@ def Icc_left_chart (x y : ℝ) [fact (x < y)] :
   end,
   open_target := begin
     have : is_open {z : ℝ | z < y - x} := is_open_Iio,
-    have : is_open {z : fin 1 → ℝ | z 0 < y - x} :=
-      (continuous_apply 0) _ this,
+    have : is_open {z : fin 1 → ℝ | z 0 < y - x},
+    { have key : _ → _ := @continuous_apply (fin 1) (λ _, ℝ) _ 0,
+      dsimp at key,
+      exact key _ this },
     exact continuous_subtype_val _ this
   end,
   continuous_to_fun := begin

view this post on Zulip Gabriel Ebner (May 05 2020 at 10:07):

If I don't see a better solution, then yes, I just mark them reducible.

view this post on Zulip Kenny Lau (May 05 2020 at 10:07):

wow, diff is a language?

view this post on Zulip Johan Commelin (May 05 2020 at 10:08):

Well, you can syntax highlight them... makes sense right?

view this post on Zulip Kenny Lau (May 05 2020 at 10:08):

it looks like magic

view this post on Zulip Johan Commelin (May 05 2020 at 10:08):

pygments doesn't do magic
— eastern wisdom

view this post on Zulip Johan Commelin (May 05 2020 at 10:13):

/me :fencing: and it's looking good so far

view this post on Zulip Johan Commelin (May 05 2020 at 10:18):

Fixed bochner integration

view this post on Zulip Gabriel Ebner (May 05 2020 at 10:22):

--- a/src/geometry/manifold/real_instances.lean
+++ b/src/geometry/manifold/real_instances.lean
@@ -213,10 +213,8 @@ def Icc_left_chart (x y : ℝ) [fact (x < y)] :
   end,
   open_target := begin
     have : is_open {z : ℝ | z < y - x} := is_open_Iio,
-    have : is_open {z : fin 1 → ℝ | z 0 < y - x},
-    { have key : _ → _ := @continuous_apply (fin 1) (λ _, ℝ) _ 0,
-      dsimp at key,
-      exact key _ this },
+    have : is_open {z : fin 1 → ℝ | z 0 < y - x} :=
+      @continuous_apply (fin 1) (λ _, ℝ) _ 0 _ this,
     exact continuous_subtype_val _ this
   end,
   continuous_to_fun := begin

view this post on Zulip Johan Commelin (May 05 2020 at 10:58):

@Gabriel Ebner I thought I tried that!

view this post on Zulip Johan Commelin (May 05 2020 at 10:58):

It seems that this stuff is subtle/fragile... :sad:

view this post on Zulip Johan Commelin (May 05 2020 at 11:16):

:tada: :fencing: :thumbs_up:
Mathlib builds for me.

view this post on Zulip Johan Commelin (May 05 2020 at 11:17):

I just pushed

view this post on Zulip Kevin Buzzard (May 05 2020 at 11:17):

Does this mean Witt vectors are back on?

view this post on Zulip Johan Commelin (May 05 2020 at 11:19):

The total number of changes aren't even too big:
https://github.com/leanprover-community/mathlib/compare/lean_pr_211?expand=1

view this post on Zulip Johan Commelin (May 05 2020 at 11:19):

Kevin Buzzard said:

Does this mean Witt vectors are back on?

Well, first we need to get lean#211 merged, and then released and then this PR has to be merged into mathlib.

view this post on Zulip Kevin Buzzard (May 05 2020 at 11:20):

But it means you are unblocked, right? :D

view this post on Zulip Reid Barton (May 05 2020 at 11:25):

Not yet though. Maybe you should formalize sober spaces while you wait.

view this post on Zulip Reid Barton (May 05 2020 at 11:27):

Soooo, what about also having Lean not unfold proofs of lemmas.

view this post on Zulip Reid Barton (May 05 2020 at 11:28):

Currently I'm forced to admit that definitional proof irrelevance is "an obscure feature that nobody really understands".

view this post on Zulip Reid Barton (May 05 2020 at 11:29):

Or, wait. Is this change fixing that too?

view this post on Zulip Patrick Massot (May 05 2020 at 11:34):

Do we have any performance benchmark here?

view this post on Zulip Johan Commelin (May 05 2020 at 11:38):

It didn't feel like Lean was slower, when compiling mathlib

view this post on Zulip Johan Commelin (May 05 2020 at 11:42):

I am now running time nice leanpkg build on this mathlib.
When I'm done, I'll also run it on regular mathlib.
Check back in ~ 4 hours (-;

view this post on Zulip Reid Barton (May 05 2020 at 11:49):

Another thing I am a bit confused about: In general, the proofs of lemmas may not be immediately available. If unification wants to unfold one of these proofs, does that mean it joins on the task computing the proof?

view this post on Zulip Johan Commelin (May 05 2020 at 12:33):

time nice leanpkg build ### building with lean#211
real    48m45.006s
user    584m25.837s
sys     7m46.827s

view this post on Zulip Johan Commelin (May 05 2020 at 12:34):

Starting the "classic" build now.

view this post on Zulip Johan Commelin (May 05 2020 at 13:20):

time nice leanpkg build ### building with lean-3.10.0
real    45m12.958s
user    571m15.583s
sys     7m42.585s

view this post on Zulip Johan Commelin (May 05 2020 at 13:21):

So the build times seem very similar. I have no idea how big the noise factor is.

view this post on Zulip Johan Commelin (May 05 2020 at 13:21):

But we do seem to get a tiny slowdown

view this post on Zulip Johan Commelin (May 05 2020 at 13:21):

I would have expected that lean is trying less stuff, more conservative. So would it have been crazy to actually see a slight speedup instead?

view this post on Zulip Mario Carneiro (May 05 2020 at 13:21):

I'm surprised it's not a speedup

view this post on Zulip Johan Commelin (May 05 2020 at 13:26):

2.3% ... are we willing to sacrifice that?

view this post on Zulip Johan Commelin (May 05 2020 at 13:29):

Maybe we should include witt vectors in the comparison?

view this post on Zulip Johan Commelin (May 05 2020 at 13:30):

But more seriously... is there anything we can say about the noise? Or whether or not this should have been a speedup?

view this post on Zulip Johan Commelin (May 05 2020 at 13:30):

@Sebastian Ullrich Do you have some wise words to say?

view this post on Zulip Gabriel Ebner (May 05 2020 at 13:31):

I bet if you build mathlib five times, you'll see a larger variance.

view this post on Zulip Gabriel Ebner (May 05 2020 at 13:31):

Also how did you build lean? Compiler version, build type (debug/release)?

view this post on Zulip Johan Commelin (May 05 2020 at 13:31):

Aaah, does that matter?

view this post on Zulip Gabriel Ebner (May 05 2020 at 13:32):

It matters about one or two percent, I would imagine.

view this post on Zulip Johan Commelin (May 05 2020 at 13:32):

I see. I just followed the build instructions. Is there some config file you would want to see?

view this post on Zulip Johan Commelin (May 05 2020 at 13:33):

If you want, I can run a number of builds tonight. But maybe we just decide that this PR is going to get merged anyway?

view this post on Zulip Gabriel Ebner (May 05 2020 at 13:33):

I vote for merge.

view this post on Zulip Sebastian Ullrich (May 05 2020 at 13:33):

Yeah, there really isn't any conceivable reason to defend the old behavior

view this post on Zulip Johan Commelin (May 05 2020 at 13:34):

Unless it would be significantly faster

view this post on Zulip Sebastian Ullrich (May 05 2020 at 13:34):

Well, then obviously something else must be broken to make it slower!

view this post on Zulip Sebastian Ullrich (May 05 2020 at 13:38):

Btw, you might already be aware of http://speedcenter.informatik.kit.edu/lean/. I can't really recommend this particular software to use for benchmarking other projects such as mathlib, but we have some students who are working on an actually usable alternative, so maybe soon...

view this post on Zulip Johan Commelin (May 05 2020 at 13:40):

I was not aware of it

view this post on Zulip Johan Commelin (May 05 2020 at 13:40):

So, thanks (-;

view this post on Zulip Johan Commelin (May 05 2020 at 13:44):

When the usable alternative is there, it would be cool to add these stats to the community website

view this post on Zulip Rob Lewis (May 05 2020 at 14:13):

I think we're long overdue for some kind of mathlib performance benchmarking. It's way too easy to introduce invisible slowdowns.

view this post on Zulip Patrick Massot (May 05 2020 at 14:14):

I think everybody agrees, but everybody seem to be measuring only noise

view this post on Zulip Rob Lewis (May 05 2020 at 14:15):

Presumably there's some kind of service we can pay for that will do this with dedicated resources, right?

view this post on Zulip Reid Barton (May 05 2020 at 14:40):

Certainly one can rent dedicated servers, though they are moderately expensive and/or require custom infrastructure (saving $ by not running the server 24/7 means more complexity managing the server).

view this post on Zulip Reid Barton (May 05 2020 at 14:41):

Not sure whether there are off-the-shelf services of this kind. Probably worth discussing with the Lean 4 team.

view this post on Zulip Reid Barton (May 05 2020 at 14:49):

Actually we are already at the point where a reasonably beefy machine would be running at a nontrivial fraction of capacity if it did nothing but build mathlib commits. I tried one of the Scaleway HC-BM1-S bare-metal instances ("2× Intel® Xeon Silver 4114", whatever that means; 20 cores) and it took about 40 minutes to build mathlib once, so if there are ~240 commits in a month that comes to 160 hours. One month is about 730 hours.

view this post on Zulip Reid Barton (May 05 2020 at 14:50):

An alternative: Pick some metric(s) that Lean can count while building, for example number of entries to is_def_eq_core or whatever, and use that as a proxy for compilation time which is not affected by the hardware.

view this post on Zulip Bryan Gin-ge Chen (May 05 2020 at 15:05):

I'm just coming back to this. It looks like Gabriel just merged lean#211 into master :tada: . Thanks to Gabriel and Johan for following up on this!

Out of curiosity, how did the changes in the "Semireducible everywhere!' commit (https://github.com/leanprover-community/lean/pull/211/commits/d9293317c8cd3b77a7f94b20f05f7fc4164467e1) affect the number of errors in the mathlib branch?

view this post on Zulip Johan Commelin (May 05 2020 at 15:06):

See https://github.com/leanprover-community/mathlib/compare/lean_pr_211?expand=1

view this post on Zulip Johan Commelin (May 05 2020 at 15:06):

I don't think it got worse

view this post on Zulip Bryan Gin-ge Chen (May 05 2020 at 15:09):

Ah, OK. Can we revert any of the fixes to mathlib that were made before that commit, or is the new Lean still unable to fill in as many underscores as Lean 3.10.0?

view this post on Zulip Johan Commelin (May 05 2020 at 15:14):

Reid Barton said:

Actually we are already at the point where a reasonably beefy machine would be running at a nontrivial fraction of capacity if it did nothing but build mathlib commits. I tried one of the Scaleway HC-BM1-S bare-metal instances ("2× Intel® Xeon Silver 4114", whatever that means; 20 cores) and it took about 40 minutes to build mathlib once, so if there are ~240 commits in a month that comes to 160 hours. One month is about 730 hours.

Maybe we can improve Scott's build bot a bit? I think he mentioned averaging the build times of the last 5 builds, for example.

view this post on Zulip Johan Commelin (May 05 2020 at 15:14):

Bryan Gin-ge Chen said:

Ah, OK. Can we revert any of the fixes to mathlib that were made before that commit, or is the new Lean still unable to fill in as many underscores as Lean 3.10.0?

I didn't try

view this post on Zulip Johan Commelin (May 05 2020 at 15:14):

Feel free to golf the PR, while I'm having dinner (-;

view this post on Zulip Bryan Gin-ge Chen (May 06 2020 at 00:11):

No luck reverting any of the earlier changes. Oh well.


Last updated: May 09 2021 at 12:14 UTC