Zulip Chat Archive

Stream: general

Topic: another timeout


view this post on Zulip Kevin Buzzard (May 12 2019 at 16:58):

The perfectoid project currently compiles fine, according to Travis, but if I try it in VS Code I get deterministic timeouts! I have traced the issue back to VS Code feeding -T100000 to Lean (maximum number of memory allocations per task), but Travis not doing this.

If I have code which is timing out with -T100000 does this indicate that something is wrong with the code? Before, we had timeout issues which were fixed by making arbitrary universe changes. Maybe I'll try this now, but in general I am not sure what this means. I've seen my code give typeclass inference errors which could be fixed by changing the max depth, but this is the first time I've seen a timeout issue which could be fixed by changing the parameters.

view this post on Zulip Scott Morrison (May 12 2019 at 23:32):

Oh, I definitely get this when I let tactics go berserk. It's usually solved by splitting things into smaller lemmas.

view this post on Zulip Kevin Buzzard (May 13 2019 at 10:10):

I have managed to tame the timeouts but I don't think it's a tactic issue.

def presheaf_map {U V : opens (spa A)} (hUV : U  V) :
  presheaf_value V  presheaf_value U :=
λ f, ⟨λ rd,
let TEMP := f.val in TEMP rd.val, set.subset.trans rd.2 hUV,
--  f.val ⟨rd.val, set.subset.trans rd.2 hUV⟩, -- this times out with lean -T100000
λ rd1 rd2 h,
-- I do not particularly want to go into tactic mode right now
begin
  let TEMP2 := f.2 (rational_open_data_subsets.map hUV rd1)
    (rational_open_data_subsets.map hUV rd2) h,
  exact TEMP2,
  -- exact f.2 (rational_open_data... times out
  -- convert f.2 (rational_open_data... works
end

This should be a purely term mode proof. The first problem is that f.val ⟨rd.val, set.subset.trans rd.2 hUV⟩ times out when applied directly; this let hack fixes the first timeout. The second timeout I solve in tactic mode (it's a prop) but it's the same story; a term should work, but exact fails and it's only convert or the let which save us. A convert can be used with the first timeout too, but this causes errors later in the file for some reason.

I would like to debug this further. I do not know what is going on at all. If this is happening because we have written bad code then I'd like to write better code but I don't know which code is bad. If this is happening because of some other reason I'd still like to know what is going on. I feel a bit helpless at the minute; I have no understanding why the first let changes anything. @Sebastian Ullrich @Mario Carneiro can either of you make some educated guesses about what is happening?

A completely compiled version of the perfectoid project, all the olean files, with current mathlib master, is available here:

wwwf.imperial.ac.uk/~buzzard/xena/perfectoid_20190513.tar

If you download this, and run lean --make in src the command returns very quickly with no output. The project is all compiled and all fine. Now open it in VS Code and in src/Spa.lean on line 720 there is a timeout, which can be fixed by changing -T100000 to a higher value in VS Code settings. Lean is working far too hard to compile this lemma. Changing f.val ⟨rd.val, set.subset.trans rd.2 hUV⟩, to let TEMP := f.val in TEMP ⟨rd.val, set.subset.trans rd.2 hUV⟩, fixes everything.

view this post on Zulip Mario Carneiro (May 13 2019 at 10:12):

what is the type of TEMP?

view this post on Zulip Mario Carneiro (May 13 2019 at 10:12):

and f and ⟨rd.val, set.subset.trans rd.2 hUV⟩

view this post on Zulip Mario Carneiro (May 13 2019 at 10:21):

Here's a working term mode proof:

def presheaf_map {U V : opens (spa A)} (hUV : U  V)
  (f : presheaf_value V) : presheaf_value U :=
⟨_, λ rd1 rd2 h,
  (f.2 (rational_open_data_subsets.map hUV rd1)
    (rational_open_data_subsets.map hUV rd2) h : _)

view this post on Zulip Kevin Buzzard (May 13 2019 at 10:27):

But what's going on? How is (blah : _) any different to blah?

view this post on Zulip Kevin Buzzard (May 13 2019 at 10:29):

This is my actual question. Is the point that your code is somehow better than my code in some intrinsic way -- I should never have written my code the way I wrote it? Or is the problem that I have made some ghastly types and the fact that they're difficult to manipulate is my fault and something should be changed? Or is the problem that Lean is not very good at something and you know how to work around the deficiency? What is actually happening?

view this post on Zulip Mario Carneiro (May 13 2019 at 10:29):

(blah : _) says "ignore the expected type here, figure out the type of blah first and then unify with the goal"

view this post on Zulip Kevin Buzzard (May 13 2019 at 10:29):

But doesn't (blah) also say that?

view this post on Zulip Mario Carneiro (May 13 2019 at 10:30):

blah says "use the expected type to elaborate blah"

view this post on Zulip Mario Carneiro (May 13 2019 at 10:30):

usually this is a good thing, but occasionally it gives a bad result

view this post on Zulip Kevin Buzzard (May 13 2019 at 10:31):

Aah. So the elaboration process of a term usually takes the type of this term into account, and this is a workaround to stop it doing this?

view this post on Zulip Kevin Buzzard (May 13 2019 at 10:32):

Running Lean with -T200000 succeeds, by the way -- so everything is consistent; this is just, for some reason, a way of making Lean succeed quicker.

view this post on Zulip Mario Carneiro (May 13 2019 at 10:32):

I think I figured out the problem (and I guess you could class it as "lean is not very good at something"). If I start with

def presheaf_map {U V : opens (spa A)} (hUV : U  V)
  (f : presheaf_value V) : presheaf_value U :=
begin
  refine ⟨λ rd, _, _⟩,
  have := f.val,
end

I see that the goal has type r_o_d_completion (rd.val), and the have has type Π (rd : rational_open_data_subsets V), r_o_d_completion (rd.val). The obvious solution is to plug rd into f.val but this doesn't work because rd : rational_open_data_subsets U instead

view this post on Zulip Kevin Buzzard (May 13 2019 at 10:33):

I am deeply sorry about r_o_d_completion by the way. I got sick of typing rational_open_data. It's on my job list to change it to something more sensible.

view this post on Zulip Mario Carneiro (May 13 2019 at 10:35):

But the problem is that when you use refine f.val _ here lean thinks "okay, let's make r_o_d_completion (rd.val) =?= r_o_d_completion (?m.val). I know, let's try to make all the arguments to r_o_d_completion the same and rd =?= ?m. So I have to prove rational_open_data_subsets U =?= rational_open_data_subsets V." Lean then gets lost unfolding your tower of definitions, hoping that U doesn't actually appear in the definition so that rational_open_data_subsets U is defeq to rational_open_data_subsets V

view this post on Zulip Kevin Buzzard (May 13 2019 at 10:35):

but this doesn't work because rd : rational_open_data_subsets U instead

Right, that's what all the set.subset.trans rd.2 hUV is about.

view this post on Zulip Kevin Buzzard (May 13 2019 at 10:36):

Oh you have maybe completely debugged this. Many thanks as ever! Did you use some trace tools or was this just pure thought? I think it is worth my while thinking about what you're saying here. This is a trick I don't know yet.

view this post on Zulip Mario Carneiro (May 13 2019 at 10:36):

This is often the place where the :_ trick works

view this post on Zulip Mario Carneiro (May 13 2019 at 10:37):

I usually see this when you use congr_arg, which is another place where the heuristic f x =?= g y => f =?= g /\ x =?= y leads lean astray

view this post on Zulip Kevin Buzzard (May 13 2019 at 10:40):

I knew the maths I was formalising in the project (although as Patrick pointed out I didn't know all of the details in several places), but the timeouts were scary. Before we finished the project I was sometimes thinking "you know, Lean actually can't do this can it". I've been forced to wrestle with several timeouts.

view this post on Zulip Kevin Buzzard (May 13 2019 at 10:40):

But Lean always came through in the end, although the solutions were a bit random.

view this post on Zulip Kevin Buzzard (May 13 2019 at 10:41):

On line 744 of src/valuation/field.lean if you change Type u to Type* then Lean times out. That was the worst one. I have no idea why.

view this post on Zulip Mario Carneiro (May 13 2019 at 10:44):

For that one, I tried

view this post on Zulip Mario Carneiro (May 13 2019 at 10:45):

begin
  refine valuation.completion_extend _,
  -- try_for 10000 {
  --   exact valuation.completion_extend (valuation_field.canonical_valuation v)
  -- }
end

and it says

invalid type ascription, term has type
  valuation (ring_completion (valued_ring ?m_3 ?m_5)) ?m_1 : Type (max ? ?)
but is expected to have type
  valuation (ring_completion (valuation_field v)) (value_group v) : Type ?

view this post on Zulip Mario Carneiro (May 13 2019 at 10:45):

what is the relation between valuation_field and valued_ring?

view this post on Zulip Mario Carneiro (May 13 2019 at 10:48):

I see, valued_ring is a wrapper. This is not being very nice to lean, it has no idea what to unwrap here. I'm guessing valuation_field is much more complicated, so lean's heuristics say to unfold the more complicated one and it gets lost

view this post on Zulip Kevin Buzzard (May 13 2019 at 10:52):

That wrapper caused us problems.

view this post on Zulip Kevin Buzzard (May 13 2019 at 10:53):

It's funny that changing the universe made it work though.

view this post on Zulip Kevin Buzzard (May 13 2019 at 10:55):

In fact even with_zero caused us problems (a wrapper for option) -- we used with_zero a lot and at some point we seriously considered redefining it by just copying some option code; the option kept leaking out.

view this post on Zulip Mario Carneiro (May 13 2019 at 10:55):

have you tried printing the definition? It makes me weep to see

view this post on Zulip Kevin Buzzard (May 13 2019 at 10:55):

The definition of what?

view this post on Zulip Mario Carneiro (May 13 2019 at 10:56):

noncomputable def valuation_on_completion {R : Type u} [comm_ring R] (v : valuation R Γ) :
  valuation
    (ring_completion
      (valuation.valuation_field v))
    (value_group v) :=
valuation.completion_extend (valuation_field.canonical_valuation v)

set_option pp.all true
#print valuation_on_completion

view this post on Zulip Mario Carneiro (May 13 2019 at 10:56):

oh, actually that's not so bad

view this post on Zulip Mario Carneiro (May 13 2019 at 10:57):

this version looks much worse

begin
  have := valuation.completion_extend (valuation_field.canonical_valuation v),
  dunfold valued_ring at this,
  exact this
end

view this post on Zulip Mario Carneiro (May 13 2019 at 10:57):

I need a deduplicating pp printer

view this post on Zulip Kevin Buzzard (May 13 2019 at 10:58):

I don't really understand what you're saying.

view this post on Zulip Mario Carneiro (May 13 2019 at 10:58):

These printouts always make expressions look worse than they are

view this post on Zulip Kevin Buzzard (May 13 2019 at 10:58):

We just typed in normal maths

view this post on Zulip Mario Carneiro (May 13 2019 at 10:58):

but if expressions are much much worse under the hood than they appear then that's a bad sign

view this post on Zulip Mario Carneiro (May 13 2019 at 10:59):

and stuff like timeouts is just the symptom

view this post on Zulip Mario Carneiro (May 13 2019 at 10:59):

the moral of the story is "don't make lean work too hard"

view this post on Zulip Mario Carneiro (May 13 2019 at 11:00):

sometimes you accidentally ask lean to do something silly and then you get a timeout for no reason

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:01):

We're just extending a valuation on a ring to a valuation on its completion. What's not to like?

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:02):

You're saying we should be looking at our terms to see if any of them are getting suspiciously large?

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:02):

But what can we do to stop this happening?

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:03):

You shouldn't have unfolded our wrapper!

view this post on Zulip Mario Carneiro (May 13 2019 at 11:04):

The reason this happened was the first error message I posted:

invalid type ascription, term has type
  valuation (ring_completion (valued_ring ?m_3 ?m_5)) ?m_1 : Type (max ? ?)
but is expected to have type
  valuation (ring_completion (valuation_field v)) (value_group v) : Type ?

I think the problem is not actually valued_ring itself but all the instances on it

view this post on Zulip Mario Carneiro (May 13 2019 at 11:05):

valuation_field has a bunch of instances, and valued_ring has different instances, and a lot of unfolding needs to happen to see they are the same

view this post on Zulip Mario Carneiro (May 13 2019 at 11:06):

Why are you applying a theorem which isn't obviously applicable?

view this post on Zulip Mario Carneiro (May 13 2019 at 11:07):

what's the logic here? How does the stuff on valuation_field relate to valued_ring?

view this post on Zulip Johan Commelin (May 13 2019 at 11:08):

A valued ring is a ring together with a valuation. This valuation induces a topology, etc...

A valuation field is a particular example.

view this post on Zulip Mario Carneiro (May 13 2019 at 11:09):

maybe you need a typeclass for that

view this post on Zulip Mario Carneiro (May 13 2019 at 11:09):

rather than a type constructor

view this post on Zulip Mario Carneiro (May 13 2019 at 11:11):

i.e. valued_ring R v is a prop assertion that says that a topological ring is generated by a valuation

view this post on Zulip Mario Carneiro (May 13 2019 at 11:12):

that way you can assert that valuation_field is a valued ring, even though it isn't literally constructed as "adjoin this valuation to the ring"

view this post on Zulip Mario Carneiro (May 13 2019 at 11:13):

aka stricklandize it

view this post on Zulip Johan Commelin (May 13 2019 at 11:13):

Or we change it to valued_ring.mk? And we have class

class valued_ring (R : Type*) [ring R] :=
(v : valuation R Γ)

view this post on Zulip Mario Carneiro (May 13 2019 at 11:13):

I was going to say that, and then I realized that the gamma will give you problems

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:36):

Sorry, my exam just finished and I had to pick up several hundred pieces of paper

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:38):

With a random ring R there are lots of valuations, so lots of topologies. But given a valuation v we wanted a topology on R so we went with a wrapper because topological_space is a class I guess.

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:40):

invalid type ascription, term has type
  valuation (ring_completion (valued_ring ?m_3 ?m_5)) ?m_1 : Type (max ? ?)
but is expected to have type
  valuation (ring_completion (valuation_field v)) (value_group v) : Type ?

valued_ring ?m_3 ?m_5 is just by definition ?m_3 but this is all about topology, and I can't put a topology on ?m_3 because it depends on ?m_5

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:42):

We mathematicians need to learn the right way to think about this stuff.

view this post on Zulip Johan Commelin (May 13 2019 at 11:42):

@Mario Carneiro Can you formulate a general principal here? Why is valued_ring a bad type wrapper, but multiplicative a good one?

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:43):

but if expressions are much much worse under the hood than they appear then that's a bad sign

Do you mean "much worse after you've unfolded absolutely everything" or something else?

view this post on Zulip Mario Carneiro (May 13 2019 at 11:43):

I mean much worse explicitly, before any unfolding

view this post on Zulip Mario Carneiro (May 13 2019 at 11:43):

or after any unfolding that needs to be done in the moment

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:45):

like unfolding valued_ring.

view this post on Zulip Mario Carneiro (May 13 2019 at 11:45):

valued_ring is not a bad type wrapper, but it's not sufficient for all things. In particular, this is the same problem we've seen before with localization. Sometimes you want to perform the construction, and sometimes you want to say that an independently constructed type is isomorphic to the construction

view this post on Zulip Mario Carneiro (May 13 2019 at 11:46):

quotient is another example of this

view this post on Zulip Mario Carneiro (May 13 2019 at 11:46):

It doesn't apply if the type isn't actually quotient bla

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:47):

I was going to say that, and then I realized that the gamma will give you problems

Because of universe issues or because we just need to input it directly with

class valued_ring (R : Type u) [ring R] :=
(Γ : Type u)
[totally_ordered_group Γ] -- or whatever we called it
(v : valuation R Γ)

view this post on Zulip Mario Carneiro (May 13 2019 at 11:47):

In this case you have valued_ring R v, the construction, and you want to apply it to valuation_field v, which after unfolding is not defined as valued_ring bla bla

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:48):

There's something a bit wrong. Those v's are perhaps not the same.

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:48):

valuation_field v has got a valuation on it but it's not v

view this post on Zulip Mario Carneiro (May 13 2019 at 11:48):

right, I'm not saying they are

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:48):

Oh Ok

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:49):

No, you're supposed to be unfolding valued_ring here, not valuation_field

view this post on Zulip Mario Carneiro (May 13 2019 at 11:49):

I'm saying that valuation_field v =?= valued_ring ?m1 ?m2 doesn't have a solution by unfolding valuation_field

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:49):

Right!

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:49):

Unfold the other one.

view this post on Zulip Mario Carneiro (May 13 2019 at 11:49):

Even if you unfold valued_ring here, it doesn't solve the problem of all the instances

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:50):

I think that you're saying that if we're going to use a wrapper type, then we must be very careful to wrap everything up.

view this post on Zulip Mario Carneiro (May 13 2019 at 11:50):

valued_ring has a bunch of instances on it, a uniform structure and so on - does valuation_field v have the same structure?

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:50):

No

view this post on Zulip Mario Carneiro (May 13 2019 at 11:50):

then you shouldn't apply this theorem

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:50):

Hmm...we could put those structures on it.

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:51):

We wrote the wrapper because for a general ring R and a general valuation v, we definitely don't want R to inherit the uniform structure from v, because often R will be fixed and v will change

view this post on Zulip Mario Carneiro (May 13 2019 at 11:51):

My guess is you want to prove is_valued_ring (valuation_field v) (valuation_field.canonical_valuation v)

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:52):

valuation_field v is exactly the point where we've manipulated the ring so much that now we'll never put another valuation on it.

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:52):

None of this conversation is about mathematics, in some sense.

view this post on Zulip Mario Carneiro (May 13 2019 at 11:52):

It's proof engineering stuff

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:52):

So I'm a beginner here.

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:52):

Yes exactly.

view this post on Zulip Mario Carneiro (May 13 2019 at 11:53):

You can have valued_ring R v as before, and prove is_valued_ring (valued_ring R v) v

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:54):

So we keep the wrapper?

view this post on Zulip Mario Carneiro (May 13 2019 at 11:54):

and then completion_extend has the type valuation (ring_completion K) Γ where is_valued_ring K v

view this post on Zulip Mario Carneiro (May 13 2019 at 11:54):

I don't know if you need the wrapper, but I imagine that sometimes you just have a ring and need to put a valuation on it

view this post on Zulip Mario Carneiro (May 13 2019 at 11:55):

rather than asserting that a pre-existing topological ring is generated by a valuation

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:55):

That's right.

view this post on Zulip Mario Carneiro (May 13 2019 at 11:55):

so you want both

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:55):

In fact I think that always we just have the ring and need to put a topology on it coming from a valuation.

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:56):

That's why we used a wrapper -- because the valuation can vary, but topological_space is a class.

view this post on Zulip Mario Carneiro (May 13 2019 at 11:56):

I think that's what you thought originally and that's why the code looks like it does, but it turns out not to be the case

view this post on Zulip Mario Carneiro (May 13 2019 at 11:56):

because valuation_field is clearly not of that form

view this post on Zulip Johan Commelin (May 13 2019 at 11:56):

It is of that form mathematically

view this post on Zulip Johan Commelin (May 13 2019 at 11:56):

But not Lean-ny

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:57):

valuation_field was a field that didn't have a valuation for most of the projects, and then I realised far too late (because I never wrote a proper roadmap) that we needed a topology on it.

view this post on Zulip Mario Carneiro (May 13 2019 at 11:57):

and that's what is_valued_ring is for, to say "this ring is generated by this valuation"

view this post on Zulip Mario Carneiro (May 13 2019 at 11:57):

You might also consider writing valuation_field so it has the form valued_ring bla bla, but that will affect other things

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:58):

Then Patrick found the part of Bourbaki that did what we wanted, and worked in what a library-builder would say was the correct generality: given a valuation on a ring, the ring gets a topology, and the valuation extends to the completion of the ring.

view this post on Zulip Johan Commelin (May 13 2019 at 11:58):

I guess an alternative would be to rename valuation_field to valuation_field.aux and then define valuation_field as valued_ring (valuation_field_aux _) _

view this post on Zulip Mario Carneiro (May 13 2019 at 11:59):

I thought about that too, but there are some nontrivial theorems here about how the topological ring structure is preserved

view this post on Zulip Johan Commelin (May 13 2019 at 11:59):

But I guess that Mario is saying that the predicate approach is better (because more flexible?)

view this post on Zulip Kevin Buzzard (May 13 2019 at 11:59):

I suspect that the only time we ever apply the valued_ring stuff is to valuation_field v (which is a field), however there were a bunch of general theorems about the topology on a ring induced by a valuation in Bourbaki and Patrick formalised those.

view this post on Zulip Mario Carneiro (May 13 2019 at 11:59):

the predicate approach means that the instances are not impacted - they are just the valuation_field instances

view this post on Zulip Kevin Buzzard (May 13 2019 at 12:00):

So Patrick was faced with the dilemma of having a ring R, and a valuation v on R, and he wanted to talk about the induced topology on R. So the wrapper was born.

view this post on Zulip Kevin Buzzard (May 13 2019 at 12:00):

This was almost certainly the correct generality for Bourbaki. But in retrospect it was more than we needed for our application.

view this post on Zulip Kevin Buzzard (May 13 2019 at 12:09):

Thanks for all these comments. I'll digest them slowly.


Last updated: May 16 2021 at 05:21 UTC