Zulip Chat Archive

Stream: new members

Topic: Tracing time of type class inference


Nicolรฒ Cavalleri (May 23 2021 at 23:55):

At some point of some new code I wrote, Lean is taking a very long time (several minutes) to resolve all the type class inference. I saw I can trace the result with trace.class_instances true, but is there a way to rank all the results by the time it took lean to find them? I want to understand where exactly it is taking so long so I can try to play with priorities

Scott Morrison (May 24 2021 at 00:56):

Typically each individual step in trace.class_instances true is somewhat uniform in time. The thing you're really looking for is the parts of the typeclass search that are extremely deep (the number in parentheses), because that often indicates a combinatorial blow-up in the search tree, which is what you want to avoid.

But I'd also be happy to hear an answer to your actual question! :-)

Nicolรฒ Cavalleri (May 24 2021 at 01:10):

Well basically this is a #mwe of my problem:

import geometry.manifold.algebra.smooth_functions
import ring_theory.derivation

open_locale manifold

variables {๐•œ : Type*} [nondiscrete_normed_field ๐•œ]
{E : Type*} [normed_group E] [normed_space ๐•œ E]
{H : Type*} [topological_space H] (I : model_with_corners ๐•œ E H)
(M : Type*) [topological_space M] [charted_space H M]

variables (X : derivation ๐•œ C^โˆžโŸฎI, M; ๐•œโŸฏ C^โˆžโŸฎI, M; ๐•œโŸฏ)

structure test extends derivation ๐•œ C^โˆžโŸฎI, M; ๐•œโŸฏ C^โˆžโŸฎI, M; ๐•œโŸฏ

The last two lines both take ages to compile and in particular the last line triggers a deterministic timeout although it compiles through lean --make on the command line. I played with set_option trace.class_instances true for the past 3 hours but I still did not manage to understand where is type class inference having such a hard time...

Nicolรฒ Cavalleri (May 24 2021 at 01:12):

What priorities can I change to make this work?

Kevin Buzzard (May 24 2021 at 08:29):

import geometry.manifold.algebra.smooth_functions
import ring_theory.derivation

open_locale manifold

variables {๐•œ : Type} [nondiscrete_normed_field ๐•œ]
{E : Type} [normed_group E] [normed_space ๐•œ E]
{H : Type} [topological_space H] (I : model_with_corners ๐•œ E H)
(M : Type) [topological_space M] [charted_space H M]

def foo := @derivation ๐•œ C^โˆžโŸฎI, M; ๐•œโŸฏ _ _ -- instant

#check @derivation ๐•œ C^โˆžโŸฎI, M; ๐•œโŸฏ _ _ -- ฮ  [_inst_3_1 : algebra ๐•œ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ] ...

example : algebra ๐•œ C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ := infer_instance -- instant
example : algebra ๐•œ C^โˆžโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ := infer_instance -- instant

def bar := @derivation ๐•œ C^โˆžโŸฎI, M; ๐•œโŸฏ _ _ _
-- elaboration of bar took 3.34s

Kevin Buzzard (May 24 2021 at 08:31):

[class_instances] caching instance for comm_ring C^โŠคโŸฎI, M; ๐“˜(๐•œ, ๐•œ), ๐•œโŸฏ
@smooth_map_comm_ring ๐•œ _inst_1 E _inst_2 _inst_3 ๐•œ
  (@normed_ring.to_normed_group ๐•œ
     (@normed_comm_ring.to_normed_ring ๐•œ
        (@normed_field.to_normed_comm_ring ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
  (@normed_field.to_normed_space ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))
  H
  _inst_4
  I
  ๐•œ
  (@uniform_space.to_topological_space ๐•œ
     (@metric_space.to_uniform_space' ๐•œ
        (@semi_normed_group.to_pseudo_metric_space ๐•œ
           (@normed_group.to_semi_normed_group ๐•œ
              (@normed_ring.to_normed_group ๐•œ
                 (@normed_comm_ring.to_normed_ring ๐•œ
                    (@normed_field.to_normed_comm_ring ๐•œ
                       (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))))))
  ๐“˜(๐•œ, ๐•œ)
  M
  _inst_5
  _inst_6
  ๐•œ
  (@semi_normed_comm_ring.to_comm_ring ๐•œ
     (@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
        (@normed_field.to_normed_comm_ring ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1))))
  (@uniform_space.to_topological_space ๐•œ
     (@metric_space.to_uniform_space' ๐•œ
        (@semi_normed_ring.to_pseudo_metric_space ๐•œ
           (@semi_normed_comm_ring.to_semi_normed_ring ๐•œ
              (@normed_comm_ring.to_semi_normed_comm_ring ๐•œ
                 (@normed_field.to_normed_comm_ring ๐•œ (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))
  (@charted_space_self ๐•œ
     (@uniform_space.to_topological_space ๐•œ
        (@metric_space.to_uniform_space' ๐•œ
           (@semi_normed_group.to_pseudo_metric_space ๐•œ
              (@normed_group.to_semi_normed_group ๐•œ
                 (@normed_ring.to_normed_group ๐•œ
                    (@normed_comm_ring.to_normed_ring ๐•œ
                       (@normed_field.to_normed_comm_ring ๐•œ
                          (@nondiscrete_normed_field.to_normed_field ๐•œ _inst_1)))))))))
  _

Kevin Buzzard (May 24 2021 at 09:21):

Hmm. Lean is looking for an is_scalar_tower instance. The type of the term that Lean is trying to find is here. It takes over 700 lines to write out with pp.all true. Let's call that term X.

The trace then looks like this:

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : X := @derivation.is_scalar_tower ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6 ?x_7 ?x_8 ?x_9 ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : X := @power_series.is_scalar_tower ?x_11 ?x_12 ?x_13 ?x_14 ?x_15 ?x_16 ?x_17 ?x_18 ?x_19 ?x_20
failed is_def_eq
[class_instances] (0) ?x_0 : X := @mv_power_series.is_scalar_tower ?x_21 ?x_22 ?x_23 ?x_24 ?x_25 ?x_26 ?x_27 ?x_28 ?x_29 ?x_30 ?x_31
failed is_def_eq
[class_instances] (0) ?x_0 : X := @continuous_multilinear_map.is_scalar_tower ?x_32 ?x_33 ?x_34 ?x_35 ?x_36 ?x_37 ?x_38 ?x_39 ?x_40 ?x_41 ?x_42 ?x_43  ?x_44  ?x_45  ?x_46  ?x_47  ?x_48  ?x_49  ?x_50  ?x_51  ?x_52  ?x_53  ?x_54  ?x_55  ?x_56  ?x_57  ?x_58  ?x_59
failed is_def_eq
[class_instances] (0) ?x_0 : X := @module.real_complex_tower ?x_60 ?x_61 ?x_62
failed is_def_eq
...

(fourteen of these, each taking up over 700 lines of output) until it finally finds @is_scalar_tower.of_ring_hom ?x_140 ?x_141 ?x_142 ?x_143 ?x_144 ?x_145 ?x_146 ?x_147 ?x_148 which it gets extremely excited about (spending well over 1000 lines of debugging output on, doing lots of hard work like finding comm_semiring instances on ๐•œ and linear_ordered_comm_ring instances and etc etc) until it eventually gives up on this, and we're back to

[class_instances] (0) ?x_0 : X := @is_scalar_tower.comap ?x_149 ?x_150 ?x_151 ?x_152 ?x_153 ?x_154 ?x_155 ?x_156
failed is_def_eq

(a reminder that each one of these lines with an X represents 715 lines of output). We then run into

[class_instances] (0) ?x_0 : X := @is_scalar_tower.right ?x_194 ?x_195 ?x_196 ?x_197 ?x_198

and Lean launches into this big search for a proof that ๐•œ is a normed field etc again, but this time it works out and Lean caches the term whose type is this gigantic X.

Ultimately this is a small number of attempts by the type class inference system (20 or so, not an unreasonable number) to find a term whose type is humungous in pp.all land, but I don't know whether that sort of thing affects speed in practice because I have no idea how type class inference actually works.

Kevin Buzzard (May 24 2021 at 09:40):

Making the following file on the command line

import geometry.manifold.algebra.smooth_functions
import ring_theory.derivation

open_locale manifold

variables {๐•œ : Type} [nondiscrete_normed_field ๐•œ]
{E : Type} [normed_group E] [normed_space ๐•œ E]
{H : Type} [topological_space H] (I : model_with_corners ๐•œ E H)
(M : Type) [topological_space M] [charted_space H M]

set_option trace.class_instances true
structure test extends derivation ๐•œ C^โˆžโŸฎI, M; ๐•œโŸฏ C^โˆžโŸฎI, M; ๐•œโŸฏ

and piping all output to a text file gives you an 11 megabyte text file. After 2 minutes it does succeed.

Kevin Buzzard (May 24 2021 at 09:46):

import geometry.manifold.algebra.smooth_functions
import ring_theory.derivation

open_locale manifold

variables {๐•œ : Type} [nondiscrete_normed_field ๐•œ]
{E : Type} [normed_group E] [normed_space ๐•œ E]
{H : Type} [topological_space H] (I : model_with_corners ๐•œ E H)
(M : Type) [topological_space M] [charted_space H M]

namespace instances

def algebra : algebra ๐•œ C^โˆžโŸฎI, M; ๐•œโŸฏ := infer_instance -- instant

attribute [instance, priority 10000] algebra

def tower : is_scalar_tower ๐•œ C^โˆžโŸฎI, M; ๐•œโŸฏ C^โˆžโŸฎI, M; ๐•œโŸฏ := infer_instance -- instant

attribute [instance, priority 10000] tower

end instances

structure test extends derivation ๐•œ C^โˆžโŸฎI, M; ๐•œโŸฏ C^โˆžโŸฎI, M; ๐•œโŸฏ

terminates in around 12 seconds on my machine

Kevin Buzzard (May 24 2021 at 09:48):

But def foo := derivation ๐•œ C^โˆžโŸฎI, M; ๐•œโŸฏ C^โˆžโŸฎI, M; ๐•œโŸฏ is essentially instant, so the issue really is with the structure command, meaning that I can't go any further.

Nicolรฒ Cavalleri (May 24 2021 at 11:55):

Thank you very much Kevin for this answer, I am learning so much from it

Kevin Buzzard (May 24 2021 at 12:01):

Unfortunately I am not learning the answer to the problem

Nicolรฒ Cavalleri (May 24 2021 at 12:04):

So first of all how did you locate that is_scalar_tower was the problem? I was looking at the output as well and I actually was doing ctrl+f to locate which instances were taking most of the lines, and I was also thinking it was probably is_scalar_tower but I was not sure because still the output file was huge and is_scalar_tower only appears in a small section of it

Nicolรฒ Cavalleri (May 24 2021 at 12:05):

Kevin Buzzard said:

Unfortunately I am not learning the answer to the problem

As for why is there a bigger issue with the structure command?

Nicolรฒ Cavalleri (May 24 2021 at 12:07):

Also what are the terms ?x_i exactly?

Kevin Buzzard (May 24 2021 at 12:11):

They're variables. Or, because Lean already has things which are called variables, it might be best to call them metavariables. They're terms whose values will be assigned later.

Nicolรฒ Cavalleri (May 24 2021 at 12:13):

Ok and then what does failed is_def_eq mean? I mean how does it conclude things are not def_eq if they depend on metavariables that have not been assigned yet?

Kevin Buzzard (May 24 2021 at 12:15):

Lean knows that mul ?x_1 ?x_2 =?= add ?x_3 ?x_4 can't ever be true by definition, if mul is just defined to be a constant and add is defined to be a different constant.

Nicolรฒ Cavalleri (May 24 2021 at 12:27):

Kevin Buzzard said:

Lean knows that mul ?x_1 ?x_2 =?= add ?x_3 ?x_4 can't ever be true by definition, if mul is just defined to be a constant and add is defined to be a different constant.

Oh I thought this was not our case because the type is is_scalar_tower on both sides but I guess the point here is that is_scalar_tower is a dependent type on other types and it is the other types that are different

Nicolรฒ Cavalleri (May 24 2021 at 12:29):

Yeah it is kind of a miracle then that def tower : is_scalar_tower ๐•œ C^โˆžโŸฎI, M; ๐•œโŸฏ C^โˆžโŸฎI, M; ๐•œโŸฏ := infer_instance is instant... I am very puzzled

Kevin Buzzard (May 24 2021 at 12:30):

I don't know how definitional equality works but I can quite believe that there is an algorithm which allows there to be holes in the terms which are checked. For example

example : โˆƒ n, n = 37 :=
begin
  existsi _,
  /-
  โŠข ?m_1 = 37

  โŠข โ„•
  -/
  { -- โŠข ?m_1 = 37
    refl },
  -- done
end

Nicolรฒ Cavalleri (May 24 2021 at 12:49):

Btw on my machine it is still taking a long time (although much better than before) and another instance that is taking very long is output.txt

Nicolรฒ Cavalleri (May 24 2021 at 12:51):

I don't know what size_of is, but is there a quick way to get a condensed expression of this type, like disableing pp_all a posteriori? There are too many parentheses for a human...

Kevin Buzzard (May 24 2021 at 12:53):

I don't think you're supposed to be messing with has_sizeof -- isn't this some internal thing?

Nicolรฒ Cavalleri (May 24 2021 at 13:00):

Ok! Can you remind me how you trace time of things?

Kevin Buzzard (May 24 2021 at 13:01):

set_option profiler true

Nicolรฒ Cavalleri (May 24 2021 at 13:02):

But can you read the output directly in visual studio? it tells me 0 messages...

Eric Rodriguez (May 24 2021 at 13:02):

it'll be hidden in All Messages

Kevin Buzzard (May 24 2021 at 13:02):

the profiler only works on stuff after the option has been set, and you can click on any blue underline to see output.

Eric Rodriguez (May 24 2021 at 13:03):

image.png

Nicolรฒ Cavalleri (May 24 2021 at 13:06):

Immagine-2021-05-24-140614.png

Nicolรฒ Cavalleri (May 24 2021 at 13:07):

Maybe does not work with structures?

Kevin Buzzard (May 24 2021 at 13:07):

I'm not sure the profiler runs on structures.

Nicolรฒ Cavalleri (May 24 2021 at 13:07):

Ok I see thanks!

Kevin Buzzard (May 24 2021 at 13:08):

I have no idea what is happening when that structure is being made, or why it takes so long. We need help. You might want to promote this thread to #general where more experts are reading. Call it something like making new structure is slow

Kevin Buzzard (May 24 2021 at 13:08):

and just post the MWE

Kevin Buzzard (May 24 2021 at 13:08):

and a link to this thread

Nicolรฒ Cavalleri (May 24 2021 at 13:17):

Well actually adding

def sizeof : has_sizeof (derivation ๐•œ C^โˆžโŸฎI, M; ๐•œโŸฏ C^โŠคโŸฎI, M; ๐•œโŸฏ) := infer_instance
attribute [instance, priority 100000] sizeof

to the namespace instances makes everything super quick

Nicolรฒ Cavalleri (May 24 2021 at 13:23):

I don't need to repeat the section namespace instances in every file as long as I import a file where it is included right?

Kevin Buzzard (May 24 2021 at 13:24):

Those instances are a hack and are not for use in a production environment.

Nicolรฒ Cavalleri (May 24 2021 at 13:25):

Kevin Buzzard said:

Those instances are a hack and are not for use in a production environment.

You mean I can't publish them to mathlib? Not even if I include everything in a section so to make it local?

Notification Bot (May 24 2021 at 13:41):

This topic was moved by Scott Morrison to #general > Tracing time of type class inference


Last updated: Dec 20 2023 at 11:08 UTC