Zulip Chat Archive

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

For instance, we wrote at https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/stalk_valuation.lean#L29-L32

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

But Lean reads:

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:

Patrick Massot (May 06 2019 at 20:33):

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

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

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

Your web browser is stupid

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

tell it it's UTF8

Kevin Buzzard (May 06 2019 at 20:38):

:-)

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!

Simon Hudon (May 06 2019 at 20:42):

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

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

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