## Stream: general

### Topic: olean-rs

#### Johan Commelin (May 06 2019 at 20:26):

Can one easily parse some dump of olean-rs to find the declaration that has the longest pp.implicit output?

#### Simon Hudon (May 06 2019 at 20:27):

It might be easier to add it as a feature of olean-rs

#### Simon Hudon (May 06 2019 at 20:27):

Why do you need that?

#### Patrick Massot (May 06 2019 at 20:28):

Part of the goal of the perfectoid project was to find out whether we could write innocent looking math that would hide a huge amount of implicit arguments that Lean would figure out by itself

#### Patrick Massot (May 06 2019 at 20:29):

Now we have the definition, we are looking for example of that phenomenon. Of course we know some of the stuff hiding quite a bit of complexity. But having Lean/Rust-Lean bragging a bit would help

#### Johan Commelin (May 06 2019 at 20:29):

Why do you need that?

Statistics... we want statistics

#### Patrick Massot (May 06 2019 at 20:30):

def stalk_valuation (x : spa A) :
valuation (stalk_of_rings (spa.presheaf_of_topological_rings A).to_presheaf_of_rings x)
(value_group (out x.1)) :=
valuation.comap (valuation_on_completion (out x.1)) (stalk_to_valuation_field x)


#### Patrick Massot (May 06 2019 at 20:31):

noncomputable def spa.presheaf.stalk_valuation : Π {A : Huber_pair} (x : ↥(spa A)),
@valuation
(@stalk_of_rings ↥(spa A) (spa.topological_space A)
(@presheaf_of_topological_rings.to_presheaf_of_rings ↥(spa A) (spa.topological_space A)
(spa.presheaf_of_topological_rings A))
x)
(@comm_ring.to_ring
(@stalk_of_rings ↥(spa A) (spa.topological_space A)
(@presheaf_of_topological_rings.to_presheaf_of_rings ↥(spa A) (spa.topological_space A)
(spa.presheaf_of_topological_rings A))
x)
(@stalk_of_rings_is_comm_ring ↥(spa A) (spa.topological_space A)
(@presheaf_of_topological_rings.to_presheaf_of_rings ↥(spa A) (spa.topological_space A)
(spa.presheaf_of_topological_rings A))
x))
(@valuation.value_group ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@Spv.out_Γ ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))
(@Spv.linear_ordered_comm_group ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))
(@Spv.out ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x)))
(@valuation.linear_ordered_comm_group ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@Spv.out_Γ ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))
(@Spv.linear_ordered_comm_group ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))
(@Spv.out ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))) :=
λ {A : Huber_pair} (x : ↥(spa A)),
@valuation.comap
(@valuation.value_group ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@Spv.out_Γ ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))
(@Spv.linear_ordered_comm_group ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))
(@Spv.out ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x)))
(@valuation.linear_ordered_comm_group ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@Spv.out_Γ ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))
(@Spv.linear_ordered_comm_group ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))
(@Spv.out ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x)))
(@ring_completion
(@valuation.valuation_field
(@Spv.out_Γ ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))
(@Spv.linear_ordered_comm_group ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))
↥A
(@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@Spv.out ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x)))
(@valuation_field.uniform_space
(@Spv.out_Γ ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))
(@Spv.linear_ordered_comm_group ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))
↥A
(@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@Spv.out ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))))
(@comm_ring.to_ring
(@ring_completion
(@valuation.valuation_field
(@Spv.out_Γ ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))
(@Spv.linear_ordered_comm_group ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))
↥A
(@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@Spv.out ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x)))
(@valuation_field.uniform_space
(@Spv.out_Γ ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))
(@Spv.linear_ordered_comm_group ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))
↥A
(@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@Spv.out ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))))
(@ring_completion.comm_ring
(@valuation.valuation_field
(@Spv.out_Γ ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))
(@Spv.linear_ordered_comm_group ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))), x ∈ spa A)
x))
↥A
(@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@Spv.out ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A))
(@subtype.val (@Spv ↥A (@Huber_ring.to_comm_ring ↥A (Huber_pair.Huber_ring A)))
(λ (x : @Spv ↥A (@Huber_ring.to_comm_ring ↥A (Hube


#### Patrick Massot (May 06 2019 at 20:32):

There is some repetition of course, but it's still nontrivial

#### Simon Hudon (May 06 2019 at 20:33):

Ok, so let's define what you mean by the longest pp.implicit output. Do you mean a big difference between the term of the definition as displayed with pp.implicit vs the term as displayed without it?

#### Scott Morrison (May 06 2019 at 20:33):

I don't think your message then was even complete... It truncated mid Hube.

#### Johan Commelin (May 06 2019 at 20:33):

You don't know what a Hube is? :grimacing:

Let me try again

#### Johan Commelin (May 06 2019 at 20:34):

@Simon Hudon I would be interested in the maximum ratio, and in just the term that has the absolutely largest pp.implicit output.

#### Johan Commelin (May 06 2019 at 20:35):

@Patrick Massot Just pipe it through wc -c before you paste.

#### Patrick Massot (May 06 2019 at 20:36):

Zulip is censoring me!

#### Johan Commelin (May 06 2019 at 20:36):

It won't censor it if you pipe through wc -c

#### Patrick Massot (May 06 2019 at 20:36):

https://www.math.u-psud.fr/~pmassot/implicit

18631

#### Johan Commelin (May 06 2019 at 20:37):

That's quite a beast (-;

#### Kevin Buzzard (May 06 2019 at 20:37):

I don't remember using variable â†¥A?

#### Patrick Massot (May 06 2019 at 20:37):

tell it it's UTF8

:-)

#### Johan Commelin (May 06 2019 at 20:39):

tar czf implicit.tar.gz implicit.txt && ls -l implicit.tar.gz
-rw-r--r-- 1 jmc jmc 947 May  6 22:40 implicit.tar.gz


#### Patrick Massot (May 06 2019 at 20:40):

Yeah, there is repetition...

#### Simon Hudon (May 06 2019 at 20:40):

Do you want the measure to be independent of the length of the identifiers used?

#### Johan Commelin (May 06 2019 at 20:41):

Hmm... that probably makes sense

#### Patrick Massot (May 06 2019 at 20:41):

Simon is in Santa Claus mode, we need to take the opportunity!

Haha :D

#### Scott Morrison (May 06 2019 at 20:42):

I do like Johan's gzip measure.

#### Patrick Massot (May 06 2019 at 20:42):

A goal of the project was also to provide a Lean benchmark. @Sebastian Ullrich is Lean optimized to handle repeated implicit arguments s in this example?

#### Scott Morrison (May 06 2019 at 20:43):

Yes. Immutable data structures for expr mean that repetitions are just pointers to the same sub-expression.

#### Patrick Massot (May 06 2019 at 20:45):

Dear Santa,
We have been very nice all year long, doing our best to Lean the definition of perfectoid spaces. Could you also bring a nice command translating any expression into a nice graph we could then manipulate into a graph editor? I did a crappy version for my Lean Together talk, but it was ascii art only, and not very flexible.
Patrick, for the perfectoid team

Thanks Scott!

#### Patrick Massot (May 06 2019 at 20:49):

Speaking of graphs, an approximate dependency graph of the perfectoid space definition can be found at https://www.math.u-psud.fr/~pmassot/perfectoid_big_labelled.png

#### Patrick Massot (May 06 2019 at 20:51):

It's approximate because no competent software programmer was involved, and also because I removed core.lean and logic.lean and a couple more files. Otherwise there are too many nodes linked to everybody and automatic layout and cluster coloring gets you only one big ball

#### Simon Hudon (May 06 2019 at 20:58):

That's a very nice graph!

#### Simon Hudon (May 06 2019 at 20:58):

To be honest, this is not my cup of tea

#### Patrick Massot (May 06 2019 at 20:59):

What is not you cup of tea?

#### Kevin Buzzard (May 06 2019 at 21:00):

I'm loving the graphs

#### Simon Hudon (May 06 2019 at 21:00):

Generating graphs

#### Simon Hudon (May 06 2019 at 21:00):

or doing any kind of graphical stuff

#### Kevin Buzzard (May 06 2019 at 21:00):

Fortunately it's Patrick's cup of tea

#### Patrick Massot (May 06 2019 at 21:00):

Except monad combinators ascii art, right?

#### Simon Hudon (May 06 2019 at 21:02):

I might be able to do that

#### Patrick Massot (May 06 2019 at 21:11):

Doing what? Monad combinators? I know you can do that

Last updated: Dec 20 2023 at 11:08 UTC