Zulip Chat Archive

Stream: general

Topic: olean-rs


view this post on Zulip 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?

view this post on Zulip Simon Hudon (May 06 2019 at 20:27):

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

view this post on Zulip Simon Hudon (May 06 2019 at 20:27):

Why do you need that?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 06 2019 at 20:29):

Why do you need that?

Statistics... we want statistics

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 06 2019 at 20:32):

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

view this post on Zulip 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?

view this post on Zulip Scott Morrison (May 06 2019 at 20:33):

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

view this post on Zulip Johan Commelin (May 06 2019 at 20:33):

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

view this post on Zulip Patrick Massot (May 06 2019 at 20:33):

Let me try again

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 06 2019 at 20:35):

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

view this post on Zulip Patrick Massot (May 06 2019 at 20:36):

Zulip is censoring me!

view this post on Zulip Johan Commelin (May 06 2019 at 20:36):

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

view this post on Zulip Patrick Massot (May 06 2019 at 20:36):

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

view this post on Zulip Patrick Massot (May 06 2019 at 20:36):

18631

view this post on Zulip Johan Commelin (May 06 2019 at 20:37):

That's quite a beast (-;

view this post on Zulip Kevin Buzzard (May 06 2019 at 20:37):

I don't remember using variable ↥A?

view this post on Zulip Patrick Massot (May 06 2019 at 20:37):

Your web browser is stupid

view this post on Zulip Patrick Massot (May 06 2019 at 20:37):

tell it it's UTF8

view this post on Zulip Kevin Buzzard (May 06 2019 at 20:38):

:-)

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 06 2019 at 20:40):

Yeah, there is repetition...

view this post on Zulip Simon Hudon (May 06 2019 at 20:40):

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

view this post on Zulip Johan Commelin (May 06 2019 at 20:41):

Hmm... that probably makes sense

view this post on Zulip Patrick Massot (May 06 2019 at 20:41):

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

view this post on Zulip Simon Hudon (May 06 2019 at 20:42):

Haha :D

view this post on Zulip Scott Morrison (May 06 2019 at 20:42):

I do like Johan's gzip measure.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 06 2019 at 20:45):

Thanks Scott!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Simon Hudon (May 06 2019 at 20:58):

That's a very nice graph!

view this post on Zulip Simon Hudon (May 06 2019 at 20:58):

To be honest, this is not my cup of tea

view this post on Zulip Patrick Massot (May 06 2019 at 20:59):

What is not you cup of tea?

view this post on Zulip Kevin Buzzard (May 06 2019 at 21:00):

I'm loving the graphs

view this post on Zulip Simon Hudon (May 06 2019 at 21:00):

Generating graphs

view this post on Zulip Simon Hudon (May 06 2019 at 21:00):

or doing any kind of graphical stuff

view this post on Zulip Kevin Buzzard (May 06 2019 at 21:00):

Fortunately it's Patrick's cup of tea

view this post on Zulip Patrick Massot (May 06 2019 at 21:00):

Except monad combinators ascii art, right?

view this post on Zulip Simon Hudon (May 06 2019 at 21:02):

I might be able to do that

view this post on Zulip Patrick Massot (May 06 2019 at 21:11):

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


Last updated: May 16 2021 at 05:21 UTC