noncomputability and oleans

Stream: lean4

[Kevin Buzzard]

Intrigued by #7265 I asked Eric W which file in mathlib caused the current maxrss. He said that speedcenter doesn't store this information but suggested instead to look at olean sizes. Right now the largest olean in mathlib master is LinearAlgebra/TensorProduct/Tower.olean, which is 16 megs. I added the word noncomputable to this definition on line 420:

noncomputable def tensorTensorTensorComm :
  (M ⊗[R] N) ⊗[A] (P ⊗[R] Q) ≃ₗ[A] (M ⊗[A] P) ⊗[R] (N ⊗[R] Q) :=
(assoc R A A (M ⊗[R] N) P Q).symm
  ≪≫ₗ congr (rightComm R A M P N).symm (1 : Q ≃ₗ[R] Q)
  ≪≫ₗ assoc R _ _ (M ⊗[A] P) N Q

and recompiled, and the olean was now 11 megs (5 megs smaller). The def on master takes about 9 seconds to compile on my (fast) machine and with noncomputable it drops to under 1 second. I then added noncomputable to all the 14 or so definitions in the file, and recompiled, and the olean went down to 2.4 megs :-)

I think it's a terrible idea to go through mathlib and add noncomputable everywhere but boy will it decrease the size of the oleans. Is this expected behaviour or worth diagnosing further? Is it worth minimising or is the problem already clear to those who understand what's going on?

[Eric Wieser]

Was there a proposal at some point to separate the "proof" oleans from the "compilation" oleans?

[Kevin Buzzard]

Making all defs and instances irreducible in LinearAlgebra.TensorProduct decreases olean size from 13 megs to 3.5. These are the two largest olean files in the cache if I got it right. I'm guessing that compilation speed also goes down.

[Kevin Buzzard]

Benchmarking at #7281 but if #7265 is anything to go by the results should be fun. Not that I think this is a good PR at all! We should get to the root of the problem really.

[Jireh Loreaux]

@Kevin Buzzard #7281 doesn't build

[Kevin Buzzard]

EDIT: this red herring was user error.

What the heck does

/- The `docBlame` linter reports:
DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/
#check TensorProduct.«term_⊗_» /- definition missing documentation string -/
#check TensorProduct.«term_⊗[_]_» /- definition missing documentation string -/
#check @TensorProduct.addMonoid /- definition missing documentation string -/
#check TensorProduct.«term_⊗ₜ_» /- definition missing documentation string -/
#check TensorProduct.«term_⊗ₜ[_]_» /- definition missing documentation string -/
#check @TensorProduct.CompatibleSMul.smul_tmul /- definition missing documentation string -/

mean and why does it start happening if I just start throwing noncomputable around the place?

[Kevin Buzzard]

Searching for term_⊗_ gives no results in the file.

[Jireh Loreaux]

That's notation.

[Jireh Loreaux]

It looks like it's complaining that the notation doesn't have a docstring or @[inherit_doc].

[Kevin Buzzard]

And why is this suddenly my problem?

[Kyle Miller]

Those are pretty printers defined by notation commands, the ones with "term"

[Eric Wieser]

Kevin Buzzard said:

And why is this suddenly my problem?

Because CI discards any messages that are in the nolints.json, but #lint does not

[Eric Wieser]

Oh, this was in CI!

[Jireh Loreaux]

https://github.com/leanprover-community/mathlib4/actions/runs/6251853169/job/16973852869?pr=7281

[Ruben Van de Velde]

Did the name change? I guess not

[Alex J. Best]

Eric Wieser said:

Oh, this was in CI!

is it? There is a #lint at the bottom of the file

[Eric Wieser]

Ah, well there's the explanation then!

[Jireh Loreaux]

@Kevin Buzzard :up: you had a stray #lint that was committed and pushed. I think you have since removed it, so the docstrings foobar are no longer necessary. But the PR still doesn't build because you need to mark downstream definitions as noncomputable.

[Jireh Loreaux]

I think probably using the speedcenter is not the way to go here. I think instead you can just profile the file for maxrss before and after your changes.

[Alex J. Best]

In case it makes testing this sort of thing easier here is a basic implemenation of noncomputable theory

import Lean

open Lean Elab Command in
elab "noncomputable theory" : command =>
do
  elabCommand (← `(local macro_rules | `(def $$a : $$b := $$c) => `(noncomputable def $$a : $$b := $$c)))
  elabCommand (← `(local macro_rules | `(def $$a := $$c) => `(noncomputable def $$a := $$c)))

section

noncomputable theory

def a := 1

#eval a
end


def b := 1

#eval b

[Jireh Loreaux]

Doesn't noncomputable section already exist?

[Alex J. Best]

When I tested it it didn't seem to do anything :shrug:

[Alex J. Best]

to be clear I did

noncomputable section aa

def a := 1

#eval a

end aa

#eval a

[Kevin Buzzard]

I've had to make a bunch more definitions noncomputable in 29 files but I think I'm almost there now

[Alex J. Best]

Alex J. Best said:

When I tested it it didn't seem to do anything :shrug:

maybe the difference is that noncomputable section allows defs to be noncomputable, but what I wrote forces them to be noncomputable if that makes sense?

[Eric Wieser]

Note that's also whatnoncomputable theory meant

[Alex J. Best]

You mean the former right? noncomputable instead of noncomputable!. In that case yes its probably a misnomer, I just wanted an easy way to make a whole file actually noncomputable

[Eric Wieser]

How hard is it to make a too_slow_to_compute keyword that means the same thing as noncomputable but has a docstring that explains this performance issue?

[Kevin Buzzard]

The results are in. This compares my PR against master from about 3 commits ago.

  Benchmark                                                       Metric                 Change
  =============================================================================================
+ build                                                           .olean serialization   -10.6%
+ build                                                           compilation            -25.4%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic              instructions            -5.3%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed             instructions           -10.4%
+ ~Mathlib.Algebra.Category.Ring.Constructions                    instructions           -16.8%
+ ~Mathlib.Algebra.Lie.BaseChange                                 instructions           -87.5%
+ ~Mathlib.Algebra.Lie.TensorProduct                              instructions           -23.4%
+ ~Mathlib.Algebra.Lie.Weights                                    instructions           -80.4%
+ ~Mathlib.LinearAlgebra.BilinearForm.TensorProduct               instructions           -85.8%
+ ~Mathlib.LinearAlgebra.Contraction                              instructions            -6.9%
+ ~Mathlib.LinearAlgebra.DirectSum.Finsupp                        instructions           -76.7%
+ ~Mathlib.LinearAlgebra.DirectSum.TensorProduct                  instructions           -82.8%
+ ~Mathlib.LinearAlgebra.Multilinear.TensorProduct                instructions           -11.1%
+ ~Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries   instructions           -20.2%
+ ~Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower              instructions           -31.3%
+ ~Mathlib.LinearAlgebra.TensorPower                              instructions            -8.7%
+ ~Mathlib.LinearAlgebra.TensorProduct                            instructions           -35.7%
+ ~Mathlib.LinearAlgebra.TensorProduct.Opposite                   instructions           -14.8%
+ ~Mathlib.LinearAlgebra.TensorProduct.Prod                       instructions           -32.4%
+ ~Mathlib.LinearAlgebra.TensorProduct.Tower                      instructions           -49.9%
+ ~Mathlib.LinearAlgebra.TensorProductBasis                       instructions           -21.7%
+ ~Mathlib.RepresentationTheory.Rep                               instructions           -34.1%
+ ~Mathlib.RingTheory.Kaehler                                     instructions            -9.2%
+ ~Mathlib.RingTheory.PolynomialAlgebra                           instructions            -9.5%
+ ~Mathlib.RingTheory.TensorProduct                               instructions           -13.8%

So how do we proceed? Some of the oleans on this branch are much smaller; is it possible to analyse the difference? Compilation -25% -- did this change make mathlib 25% faster? Is it worth trying to minimise something (this will be some work, as usual, and I'm unlikely to get to it until the weekend because term is looming but I could certainly give it a go).

[Sebastian Ullrich]

The results say that oleans shrinked by 3%, mathlib3 got faster (wall-clock) by 2%

[Henrik Böving]

No that is 25% against the previous time it took to compile, if you go to the speed center view: http://speed.lean-fro.org/mathlib4/compare/f923c955-6f71-4f1e-8cd4-142ba0fd1e48/to/78372017-b26e-4b9c-aadb-2b620036b07f you can see the absolute values in seconds.

I'm also very positively surprised by the fact that this has seemingly had no significant effect on the run time of the new compiler so it seems this slowness is to be attributed to the old one.

[Matthew Ballard]

Lint got faster by 2%? It looks like build wall clock is a little under 1%. Total CPU instructions are down a healthy 1.6%.

[Kevin Buzzard]

I'm also very positively surprised by the fact that this has seemingly had no significant effect on the run time of the new compiler so it seems this slowness is to be attributed to the old one.

So the fix is "wait for the new compiler"?

[Henrik Böving]

In a sense, but the new compiler is still in a semi frozen state so I think if you can get better perf like this this can be a reasonable workaround until it finally happens

[Kevin Buzzard]

But is another conclusion "there's no point trying to debug this any more because it will probably be fixed by the new compiler"? So basically mathlib is going to end up littered with unnecessary noncomputables? In particular should this PR actually be merged, and then reverted at some unspecified time in the future?

[Mario Carneiro]

I am not sure they are unnecessary. Arguably we should be using noncomputable a lot more aggressively, e.g. put it on everything that doesn't break the build or on request

[Mario Carneiro]

I would love it if we could find a heuristic that tracks closer to that so that we don't need to annotate everything, but I don't think one is forthcoming

[Kevin Buzzard]

we should be using noncomputable more aggressively -- on the basis that due to what may well be a bug, making a 4 line definition not noncomputable adds 5 megabytes to an olean?

[Mario Carneiro]

we should be using it more aggressively because the compiler is doing pointless work on 90% of mathlib

[Mario Carneiro]

and bloating oleans and taking compile time while it is at it

[Kevin Buzzard]

And this is because of a bug in the compiler or because this work needs to be done?

[Mario Carneiro]

this is because it doesn't know that the work doesn't need to be done

[Mario Carneiro]

there is no way it could know

[Mario Carneiro]

it's not a bug in the compiler, everything is working as designed

[Kevin Buzzard]

right, but should that work really add up to 5 megabytes for tensorTensorTensorcomm above?

[Mario Carneiro]

but mathlib is not composed of things that would be valuable in an executable and we ought to be telling lean this

[Mario Carneiro]

in fact, it might fix that "too many exported symbols" issue on windows

[Kyle Miller]

noncomputable is one way to help keep mathlib's carbon footprint lower

[Kevin Buzzard]

I have a lot of respect for Eric and I can imagine him saying that this is a big step in the wrong direction, but of course I don't care at all

[Mario Carneiro]

If the default was noncomputable I wouldn't be too concerned about mathlib PRs that make a handful of things computable so that some #eval works

[Mario Carneiro]

Kevin Buzzard said:

right, but should that work really add up to 5 megabytes for tensorTensorTensorcomm above?

This is probably a bug or some runaway work. But mathlib has some massive types and I wouldn't be surprised if this is giving the compiler a hard time just like it does everything else

[Kevin Buzzard]

It's only 1100 lines with pp.all on. Is that too big?

[Henrik Böving]

I would say its significant :P

[James Gallicchio]

worth emphasizing mario's point that the less human intensive way to do this would be to separate build oleans from compile oleans so that we can instruct lake/lean to not compile a file unless it's needed to build other files

[Henrik Böving]

No this is not something that lake has control over

[Henrik Böving]

When a you declare a definition the code generator is already doing 99% of the work such that you can run #eval on it. The thing that lake does when compiling a file is "just" turning the already fully optimized IR into C code and calling a C compiler which as from the benchmarks above is something that takes much less time than the compilation up to that point

[Henrik Böving]

(that said I did propose before that we do this on demand in some thread and there is some discussion regarding this there as well)

[Eric Wieser]

Kevin Buzzard said:

I have a lot of respect for Eric and I can imagine him saying that this is a big step in the wrong direction, but of course I don't care at all

I think it's justifiable given the potential performance/resource cost, but if this is going to spread throughout mathlib I think the name of noncomputable might start being a bad description of what's going on

[Eric Wieser]

"this can't be computed" is a much stronger claim than "this isn't sent to the compiler", and the current name implies the former

[Eric Wieser]

I guess changing the docstring of the keyword (if it has one?) would be a less dialect-forming choice

[Eric Wieser]

Kevin Buzzard said:

It's only 1100 lines with pp.all on. Is that too big?

Adding non-unital actions surely won't make this problem worse...

[Matthew Ballard]

lean4#2478 is making (?) compilation worse on OperatorNorm so #7299

[Sebastien Gouezel]

I'd really rather make whole files noncomputable, as there is no chance that anything around there will be executed any time. @Eric Wieser , you may have objections about that, so what do you think?

[Mario Carneiro]

the trouble is that mathlib does have definitions which should be computable, even when it's pure noncomputable maths, in particular notations and other internal auxiliaries

[Sebastien Gouezel]

But notations and internals wouldn't be affected by a trick like https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/noncomputability.20and.20oleans/near/392167946, right?

[Eric Wieser]

I'd be ok with Alex's trick as long as we make it clear that it's a hack for a compiler performance issue and not a statement of genuinely noncomputable concepts in the file

[Eric Wieser]

(that is, call it something different to noncomputable theory)

[Sebastien Gouezel]

(with a better name like "nonexecutable theory")

[Eric Wieser]

If anything that's better than sprinkling noncomputable everywhere because it means we can just stick a docstring on the notation and not repeat it everywhere

[Matthew Ballard]

suppress_compilation?

[Sebastien Gouezel]

Another advantage is that it is much easier to disable (globally or in a specific file) if we want to test if the issue has been solved upstream.

[Matthew Ballard]

Yes, ergonomically that approach is better

[Sebastien Gouezel]

If on master I open the file Mathlib/Analysis/NormedSpace/OperatorNorm.lean and I replace at the top the line

noncomputable theory

with Alex's trick, i.e.,

open Lean Elab Command in
elab "suppress_compilation" : command =>
do
  elabCommand (← `(local macro_rules | `(def $$a : $$b := $$c) => `(noncomputable def $$a : $$b := $$c)))
  elabCommand (← `(local macro_rules | `(def $$a := $$c) => `(noncomputable def $$a := $$c)))

suppress_compilation

then I get failures down the file, where Lean complains about a missing noncomputable modifier:

/-- The operator norm of a continuous linear map is the inf of all its bounds. -/
def opNorm (f : E →SL[σ₁₂] F) :=
  sInf { c | 0 ≤ c ∧ ∀ x, ‖f x‖ ≤ c * ‖x‖ }

gives the error

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Real.instInfSetReal', and it does not have executable code

I don't understand what is going on, because Alex's trick is precisely designed to add noncomputable to all definitions.

[Jireh Loreaux]

Is it a problem of a section ending? (Probably not, just want to rule out the obvious possibility.)

[Alex J. Best]

I think thats probably just my code not being robust enough to handle this syntax for defs for some reason, I can try and improve it, it just gets a bit mind bending for me when you have nested antiquotations lol

[Alex J. Best]

elab "suppress_compilation" : command =>
do
  elabCommand (← `(local macro_rules | `(def $$a $$b:optDeclSig := $$c) => `(noncomputable def $$a $$b := $$c)))

should be a version that actually works :wink:

[Matthew Ballard]

It doesn't like opNorm still and protected def's

[Matthew Ballard]

How hard is this try going?

private def compileDecl (decl : Declaration) : TermElabM Bool := do
  try
    Lean.compileDecl decl
  catch ex =>
    if (← read).isNoncomputableSection then
      return false
    else
      throw ex
  return true

from docs#compileDecl

[Alex J. Best]

What do you mean?

[Matthew Ballard]

I should probably just look at Lean.compileDecl to see but what are the classes of errors it throws and when does it throw them. Is there some short circuit?

Would it be a terrible thing to move the if up a couple of levels?

[Mac Malone]

Henrik Böving said:

(that said I did propose before that we do this on demand in some thread and there is some discussion regarding this there as well)

I think on-demand compilation (of IR) and a command that could request the compilation of a definition from another file (and its dependencies, if there compiled definition does not already exist0 would be great and be likely the most principled way to solve this problem in mathlib. This could be turn on/off via a lean option like compileByDefault=true/false.

[Mac Malone]

@Alex J. Best I think the reason you code may not be working in @Sebastien Gouezel's example is that it is not transferring declaration modifiers through the transformation (e.g., the doc comment).

[Matthew Ballard]

And the attributes also?

[Mac Malone]

Yeah, both attributes and doc comments are declModifiers.

[Alex J. Best]

Indeed I just don't know the syntax to fix it!

[Mac Malone]

Here is what is hopefully a working example (and a comparison of the problem):

import Lean.Elab.Declaration
open Lean Parser Elab Command

namespace ex1

scoped elab "suppress_compilation" : command => do
  elabCommand (← `(local macro_rules | `(def $$a $$b:optDeclSig := $$c) => `(noncomputable def $$a $$b := $$c)))

suppress_compilation

def foo := 0
/-- hi -/ def bar := foo -- errors
@[simp] def baz := foo --- errors

end ex1

namespace ex2

def elabSuppressCompilationDef : CommandElab := fun
| `($[$doc?:docComment]? $(attrs?)? $(vis?)? $[noncomputable]? $(unsafe?)? $(recKind?)? def $id $sig:optDeclSig := $val) => do
  elabDeclaration <| ← `($[$doc?:docComment]? $(attrs?)? $(vis?)? noncomputable $(unsafe?)? $(recKind?)? def $id $sig := $val)
| _ => throwUnsupportedSyntax

scoped macro "suppress_compilation" : command => do
  let kind := mkIdent ``declaration
  let etor := mkCIdent ``elabSuppressCompilationDef
  `(attribute [local command_elab $kind] $etor)

suppress_compilation

def foo := 0
/-- hi -/ def bar := foo -- works
@[simp] def baz := foo --- works

end ex2

[Matthew Ballard]

Nice! It looks this syntax doesn't translate directly to instance and I can't poke at right now

[Matthew Ballard]

#7316 has set_option compiler.suppress for experimentation

[Matthew Ballard]

Is there a way to set a built in option for all files in a folder?

[Eric Wieser]

Matthew Ballard said:

#7316 has set_option compiler.suppress for experimentation

Can you link to the lean4 changes?

[Matthew Ballard]

Commit

[Kyle Miller]

Sebastien Gouezel said:

with Alex's trick, i.e., [...] then I get failures down the file, where Lean complains about a missing noncomputable modifier:

/-- The operator norm of a continuous linear map is the inf of all its bounds. -/
def opNorm (f : E →SL[σ₁₂] F) :=
  sInf { c | 0 ≤ c ∧ ∀ x, ‖f x‖ ≤ c * ‖x‖ }

It's because Alex's macros don't account for docstrings. These are part of the def notation. Edit: I missed that Mac already explained this.

(@Alex J. Best Implementation note: you could define a scoped macro rule in some namespace NS and then have suppress_complication do open scoped NS, which would save you from nested quotations.)

[Sebastien Gouezel]

Thanks @Mac Malone . This works on most definitions in the file, but not all (there are always edge cases, right?): it fails on

/-- Flip the order of arguments of a continuous bilinear map.
This is a version bundled as a `LinearIsometryEquiv`.
For an unbundled version see `ContinuousLinearMap.flip`. -/
def flipₗᵢ' : (E →SL[σ₁₃] F →SL[σ₂₃] G) ≃ₗᵢ[𝕜₃] F →SL[σ₂₃] E →SL[σ₁₃] G where
  toFun := flip
  invFun := flip
  map_add' := flip_add
  map_smul' := flip_smul
  left_inv := flip_flip
  right_inv := flip_flip
  norm_map' := op_norm_flip

with the error message

compiler IR check failed at 'ContinuousLinearMap.flipₗᵢ'._rarg', error: unknown declaration 'ContinuousLinearMap.flip'

And also, I am unable to adapt your code to instances, just because I am incompetent.

[Mac Malone]

@Sebastien Gouezel Here are some additional fixes. I cannot figure out at the moment how to get an optDefDeriving in a def to match optionally so there is some undesired duplication, but everything else should be supported:

namespace ex2

def elabSuppressCompilationDecl : CommandElab := fun
| `($[$doc?:docComment]? $(attrs?)? $(vis?)? $[noncomputable]? $(unsafe?)? $(recKind?)?
    def $id $sig:optDeclSig $val:declVal $(term?)? $(decr?)?) => do
  elabDeclaration <| ← `($[$doc?:docComment]? $(attrs?)? $(vis?)? noncomputable $(unsafe?)? $(recKind?)?
    def $id $sig:optDeclSig $val:declVal $(term?)? $(decr?)?)
| `($[$doc?:docComment]? $(attrs?)? $(vis?)? $[noncomputable]? $(unsafe?)? $(recKind?)?
    def $id $sig:optDeclSig $val:declVal deriving $derivs,* $(term?)? $(decr?)?) => do
  elabDeclaration <| ← `($[$doc?:docComment]? $(attrs?)? $(vis?)? noncomputable $(unsafe?)? $(recKind?)?
    def $id $sig:optDeclSig $val:declVal deriving $derivs,* $(term?)? $(decr?)?)
| `($[$doc?:docComment]? $(attrs?)? $(vis?)? $[noncomputable]? $(unsafe?)? $(recKind?)?
    $(attrKind?)? instance $(prio?)? $(id?)? $sig:declSig $val:declVal $(term?)?) => do
  elabDeclaration <| ← `($[$doc?:docComment]? $(attrs?)? $(vis?)? noncomputable $(unsafe?)? $(recKind?)?
    $(attrKind?)? instance $(prio?)? $(id?)? $sig:declSig $val:declVal $(term?)?)
| _ => throwUnsupportedSyntax

scoped macro "suppress_compilation" : command => do
  let kind := mkIdent ``declaration
  let etor := mkCIdent ``elabSuppressCompilationDecl
  `(attribute [local command_elab $kind] $etor)

suppress_compilation

def foo := "/"
/-- hi -/ def bar := foo -- works
@[simp] def baz := foo --- works

def root : System.FilePath where -- works
  toString := foo

instance : Inhabited String := ⟨foo⟩ --- works

end ex2

def test := ex2.foo -- properly noncomputable

[Sebastien Gouezel]

Looks great, thanks!

[Trebor Huang]

Agda also seems to have this problem because cubical Agda requires extra code to be generated at every pattern matching, which in some cases drastically slows things down when the user just wants to be "cubical compatible" instead of using any cubical features.

[Sebastien Gouezel]

Implemented in #7326, and tested on OperatorNorm.lean there.