## Stream: general

### Topic: another timeout

#### 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.

#### 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.

#### 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.

#### Mario Carneiro (May 13 2019 at 10:12):

what is the type of TEMP?

#### Mario Carneiro (May 13 2019 at 10:12):

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

#### 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 : _)⟩


#### Kevin Buzzard (May 13 2019 at 10:27):

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

#### 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?

#### 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"

#### Kevin Buzzard (May 13 2019 at 10:29):

But doesn't (blah) also say that?

#### Mario Carneiro (May 13 2019 at 10:30):

blah says "use the expected type to elaborate blah"

#### Mario Carneiro (May 13 2019 at 10:30):

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

#### 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?

#### 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.

#### 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

#### 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.

#### 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

#### 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.

#### 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.

#### Mario Carneiro (May 13 2019 at 10:36):

This is often the place where the :_ trick works

#### 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

#### 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.

#### Kevin Buzzard (May 13 2019 at 10:40):

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

#### 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.

#### Mario Carneiro (May 13 2019 at 10:44):

For that one, I tried

#### 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 ?


#### Mario Carneiro (May 13 2019 at 10:45):

what is the relation between valuation_field and valued_ring?

#### 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

#### Kevin Buzzard (May 13 2019 at 10:52):

That wrapper caused us problems.

#### Kevin Buzzard (May 13 2019 at 10:53):

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

#### 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.

#### Mario Carneiro (May 13 2019 at 10:55):

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

#### Kevin Buzzard (May 13 2019 at 10:55):

The definition of what?

#### 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


#### Mario Carneiro (May 13 2019 at 10:56):

oh, actually that's not so bad

#### 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


#### Mario Carneiro (May 13 2019 at 10:57):

I need a deduplicating pp printer

#### Kevin Buzzard (May 13 2019 at 10:58):

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

#### Mario Carneiro (May 13 2019 at 10:58):

These printouts always make expressions look worse than they are

#### Kevin Buzzard (May 13 2019 at 10:58):

We just typed in normal maths

#### 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

#### Mario Carneiro (May 13 2019 at 10:59):

and stuff like timeouts is just the symptom

#### Mario Carneiro (May 13 2019 at 10:59):

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

#### 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

#### 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?

#### 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?

#### Kevin Buzzard (May 13 2019 at 11:02):

But what can we do to stop this happening?

#### Kevin Buzzard (May 13 2019 at 11:03):

You shouldn't have unfolded our wrapper!

#### 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

#### 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

#### Mario Carneiro (May 13 2019 at 11:06):

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

#### Mario Carneiro (May 13 2019 at 11:07):

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

#### 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.

#### Mario Carneiro (May 13 2019 at 11:09):

maybe you need a typeclass for that

#### Mario Carneiro (May 13 2019 at 11:09):

rather than a type constructor

#### 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

#### 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"

#### Mario Carneiro (May 13 2019 at 11:13):

aka stricklandize it

#### 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 Γ)


#### 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

#### Kevin Buzzard (May 13 2019 at 11:36):

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

#### 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.

#### 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

#### 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?

#### 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?

#### Mario Carneiro (May 13 2019 at 11:43):

I mean much worse explicitly, before any unfolding

#### Mario Carneiro (May 13 2019 at 11:43):

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

#### Kevin Buzzard (May 13 2019 at 11:45):

like unfolding valued_ring.

#### 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

#### Mario Carneiro (May 13 2019 at 11:46):

quotient is another example of this

#### Mario Carneiro (May 13 2019 at 11:46):

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

#### 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 Γ)


#### 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

#### Kevin Buzzard (May 13 2019 at 11:48):

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

#### Kevin Buzzard (May 13 2019 at 11:48):

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

#### Mario Carneiro (May 13 2019 at 11:48):

right, I'm not saying they are

Oh Ok

#### Kevin Buzzard (May 13 2019 at 11:49):

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

#### 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

Right!

#### Kevin Buzzard (May 13 2019 at 11:49):

Unfold the other one.

#### 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

#### 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.

#### 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?

No

#### Mario Carneiro (May 13 2019 at 11:50):

then you shouldn't apply this theorem

#### Kevin Buzzard (May 13 2019 at 11:50):

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

#### 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

#### 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)

#### 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.

#### Kevin Buzzard (May 13 2019 at 11:52):

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

#### Mario Carneiro (May 13 2019 at 11:52):

It's proof engineering stuff

#### Kevin Buzzard (May 13 2019 at 11:52):

So I'm a beginner here.

Yes exactly.

#### 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

#### Kevin Buzzard (May 13 2019 at 11:54):

So we keep the wrapper?

#### 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

#### 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

#### Mario Carneiro (May 13 2019 at 11:55):

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

That's right.

so you want both

#### 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.

#### 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.

#### 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

#### Mario Carneiro (May 13 2019 at 11:56):

because valuation_field is clearly not of that form

#### Johan Commelin (May 13 2019 at 11:56):

It is of that form mathematically

But not Lean-ny

#### 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.

#### 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"

#### 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

#### 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.

#### 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 _) _

#### 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

#### Johan Commelin (May 13 2019 at 11:59):

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

#### 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.

#### 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

#### 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.

#### 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.

#### 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