Compiler stuck computing something...

Stream: lean4

[Sofia Snow]

Hello. I tried adding the Linear definition below, noted the LSP stopped responding and all cores pegged at 100%. The compiler doesn't seem to like the inductive constructors of the Linear proposition, nor does it like it as a type.

inductive Cover : (x y z : List α) -> Type u
  | done  : Cover [] [] []
  | left  : Cover x y z -> Cover (t :: x) y (t :: z)
  | right : Cover x y z -> Cover x (t :: y) (t :: z)
  | both  : Cover x y z -> Cover (t :: x) (t :: y) (t :: z)

inductive Linear : Cover x y z -> Prop
  | done : Linear .done
  | left : Linear c -> Linear (.left c)
  | right : Linear c -> Linear (.right c)

[Sofia Snow]

Noticed on an older nightly, so I updated, running nightly-2022-09-15 now.

[Leonardo de Moura]

I can reproduce this issue. Created an issue for it https://github.com/leanprover/lean4/issues/1616

[Arthur Paulino]

Hi! I'm also facing an issue in which the compiler is getting stuck. Here's the #mwe:

import Std.Data.RBMap

abbrev MultilinearPolynomial α := Std.RBMap Nat α compare

namespace MultilinearPolynomial

/-- Instantiates a MPL from the list of raw `(b, c)` pairs -/
def ofPairs (pairs : List $ Nat × α) : MultilinearPolynomial α :=
  .ofList pairs _

end MultilinearPolynomial

abbrev Zmod (_ : Nat) : Type := Int

instance [Ord α] [Ord β] : Ord (α × β) where compare
  | (a₁, b₁), (a₂, b₂) =>
    let a := compare a₁ a₂
    if a == .eq then compare b₁ b₂ else a

def multilinearLagrangePolynomialCache :
    Std.RBMap (Nat × Nat) (MultilinearPolynomial $ Zmod n) compare := .ofList [
  ((2, 3), .ofPairs [(0, 0), (1, 0), (2, 1), (3, -1), (4, 0), (5, 0), (6, -1), (7, 1)]),
  ((5, 3), .ofPairs [(0, 0), (1, 0), (2, 0), (3, 0), (4, 0), (5, 1), (6, 0), (7, -1)]),
  ((2, 1), .ofPairs [(0, 1), (1, -1)]),
  ((3, 2), .ofPairs [(0, 0), (1, 0), (2, 0), (3, 1)]),
  ((1, 3), .ofPairs [(0, 0), (1, 1), (2, 0), (3, -1), (4, 0), (5, -1), (6, 0), (7, 1)]),
  ((4, 1), .ofPairs [(0, 1), (1, -1)]),
  ((5, 4), .ofPairs [(0, 0), (1, 0), (2, 0), (3, 0), (4, 0), (5, 1), (6, 0), (7, -1), (8, 0), (9, 0), (10, 0), (11, 0), (12, 0), (13, -1), (14, 0), (15, 1)]),
  ((0, 2), .ofPairs [(0, 1), (1, -1), (2, -1), (3, 1)]),
  ((0, 1), .ofPairs [(0, 1), (1, -1)]),
  ((1, 2), .ofPairs [(0, 0), (1, 1), (2, 0), (3, -1)]),
  ((2, 2), .ofPairs [(0, 0), (1, 0), (2, 1), (3, -1)]),
  ((3, 3), .ofPairs [(0, 0), (1, 0), (2, 0), (3, 1), (4, 0), (5, 0), (6, 0), (7, -1)]),
  ((4, 2), .ofPairs [(0, 1), (1, -1), (2, -1), (3, 1)]),
  ((2, 0), .ofPairs [(0, 1)]),
  ((2, 5), .ofPairs [(0, 0), (1, 0), (2, 1), (3, -1), (4, 0), (5, 0), (6, -1), (7, 1), (8, 0), (9, 0), (10, -1), (11, 1), (12, 0), (13, 0), (14, 1), (15, -1), (16, 0), (17, 0), (18, -1), (19, 1), (20, 0), (21, 0), (22, 1), (23, -1), (24, 0), (25, 0), (26, 1), (27, -1), (28, 0), (29, 0), (30, -1), (31, 1)]),
  ((3, 1), .ofPairs [(0, 0), (1, 1)]),
  ((5, 2), .ofPairs [(0, 0), (1, 1), (2, 0), (3, -1)]),
  ((5, 1), .ofPairs [(0, 0), (1, 1)]),
  ((4, 3), .ofPairs [(0, 0), (1, 0), (2, 0), (3, 0), (4, 1), (5, -1), (6, -1), (7, 1)]),
  ((1, 0), .ofPairs [(0, 1)]),
  ((5, 5), .ofPairs [(0, 0), (1, 0), (2, 0), (3, 0), (4, 0), (5, 1), (6, 0), (7, -1), (8, 0), (9, 0), (10, 0), (11, 0), (12, 0), (13, -1), (14, 0), (15, 1), (16, 0), (17, 0), (18, 0), (19, 0), (20, 0), (21, -1), (22, 0), (23, 1), (24, 0), (25, 0), (26, 0), (27, 0), (28, 0), (29, 1), (30, 0), (31, -1)]),
  ((0, 0), .ofPairs [(0, 1)]),
  ((3, 5), .ofPairs [(0, 0), (1, 0), (2, 0), (3, 1), (4, 0), (5, 0), (6, 0), (7, -1), (8, 0), (9, 0), (10, 0), (11, -1), (12, 0), (13, 0), (14, 0), (15, 1), (16, 0), (17, 0), (18, 0), (19, -1), (20, 0), (21, 0), (22, 0), (23, 1), (24, 0), (25, 0), (26, 0), (27, 1), (28, 0), (29, 0), (30, 0), (31, -1)]),
  ((4, 4), .ofPairs [(0, 0), (1, 0), (2, 0), (3, 0), (4, 1), (5, -1), (6, -1), (7, 1), (8, 0), (9, 0), (10, 0), (11, 0), (12, -1), (13, 1), (14, 1), (15, -1)]),
  ((1, 1), .ofPairs [(0, 0), (1, 1)]),
  ((3, 4), .ofPairs [(0, 0), (1, 0), (2, 0), (3, 1), (4, 0), (5, 0), (6, 0), (7, -1), (8, 0), (9, 0), (10, 0), (11, -1), (12, 0), (13, 0), (14, 0), (15, 1)]),
  ((5, 0), .ofPairs [(0, 1)]),
  ((0, 5), .ofPairs [(0, 1), (1, -1), (2, -1), (3, 1), (4, -1), (5, 1), (6, 1), (7, -1), (8, -1), (9, 1), (10, 1), (11, -1), (12, 1), (13, -1), (14, -1), (15, 1), (16, -1), (17, 1), (18, 1), (19, -1), (20, 1), (21, -1), (22, -1), (23, 1), (24, 1), (25, -1), (26, -1), (27, 1), (28, -1), (29, 1), (30, 1), (31, -1)]),
  ((2, 4), .ofPairs [(0, 0), (1, 0), (2, 1), (3, -1), (4, 0), (5, 0), (6, -1), (7, 1), (8, 0), (9, 0), (10, -1), (11, 1), (12, 0), (13, 0), (14, 1), (15, -1)]),
  ((4, 0), .ofPairs [(0, 1)]),
  ((0, 4), .ofPairs [(0, 1), (1, -1), (2, -1), (3, 1), (4, -1), (5, 1), (6, 1), (7, -1), (8, -1), (9, 1), (10, 1), (11, -1), (12, 1), (13, -1), (14, -1), (15, 1)]),
  ((4, 5), .ofPairs [(0, 0), (1, 0), (2, 0), (3, 0), (4, 1), (5, -1), (6, -1), (7, 1), (8, 0), (9, 0), (10, 0), (11, 0), (12, -1), (13, 1), (14, 1), (15, -1), (16, 0), (17, 0), (18, 0), (19, 0), (20, -1), (21, 1), (22, 1), (23, -1), (24, 0), (25, 0), (26, 0), (27, 0), (28, 1), (29, -1), (30, -1), (31, 1)]),
  ((1, 4), .ofPairs [(0, 0), (1, 1), (2, 0), (3, -1), (4, 0), (5, -1), (6, 0), (7, 1), (8, 0), (9, -1), (10, 0), (11, 1), (12, 0), (13, 1), (14, 0), (15, -1)]),
  ((1, 5), .ofPairs [(0, 0), (1, 1), (2, 0), (3, -1), (4, 0), (5, -1), (6, 0), (7, 1), (8, 0), (9, -1), (10, 0), (11, 1), (12, 0), (13, 1), (14, 0), (15, -1), (16, 0), (17, -1), (18, 0), (19, 1), (20, 0), (21, 1), (22, 0), (23, -1), (24, 0), (25, 1), (26, 0), (27, -1), (28, 0), (29, -1), (30, 0), (31, 1)]),
  ((3, 0), .ofPairs [(0, 1)]),
  ((0, 3), .ofPairs [(0, 1), (1, -1), (2, -1), (3, 1), (4, -1), (5, 1), (6, 1), (7, -1)])
] _

It works with 25 polynomials but then 36 makes it get stuck. And I need a much bigger cache, maybe ~300 polynomials. I'm using 4.0.0-nightly-2022-11-14. Am I doing something in a bad way? Thanks in advance!
cc @Matej Penciak

[Mario Carneiro]

Both heap profiling and time profiling point to Lean.MetavarContext.MkBinding.{visit, elim}, although I'm not sure that says much other than that it's looking at a huge number of exprs for some reason, probably a loss of subterm sharing somewhere

[Mario Carneiro]

It seems like a bad idea that the cache used here has no upper bound that I can see

[Sebastian Ullrich]

Usually caches with upper bounds are the reason for things suddenly going south above a certain term size. When there is sharing, the memory used by the cache usually is the least concern.

[Sebastian Ullrich]

We saw MkBinding before in https://github.com/leanprover/lean4/pull/1390#issuecomment-1205107076, though the leaf spending most of the time there was elimMVars

[Arthur Paulino]

Sorry, I didn't understand. Should I use an upper bound? (how do I do that?)
And how do I make use of the sharing Sebastian mentioned?

[Mario Carneiro]

You know what, I think it's the use of .ofPairs

[Mario Carneiro]

This causes each subterm to get postponed and I think this messes everything up

[Mario Carneiro]

But also, you should be aware that lean has some known problems with large literals inside source files. You should try to use a custom elaborator to avoid some of the costs, but others can't be avoided as long as you are producing an Expr at the end. Deep expressions are also bad, and even if you use something with nice binary recursion the compiler will linearize it and die anyway

[Mario Carneiro]

Reading data externally at runtime should be fine though, e.g. loading up a huge data structure parsed from JSON

[Arthur Paulino]

I tried replacing .ofPairs by .ofList ... _ and had the same issue

[Mario Carneiro]

you're still using dot-ident there

[Mario Carneiro]

Use MultilinearPolynomial.ofPairs

[Mario Carneiro]

Lean doesn't know the type of that slot until it elaborates everything else

[Mario Carneiro]

and I think the repeated re-elaboration is generating a lot of allocations

[Arthur Paulino]

It solved the issue :open_mouth: thanks!!

[Sebastian Ullrich]

Hmm, elabDotIdent should probably suspend immediately when the expected type is not known

[Arthur Paulino]

But there's still some hanging going on. I will remove the nesting with RB stuff and just cache simple types like lists and pairs

[Mario Carneiro]

The error message here should give you some sense of what lean is having to deal with to elaborate this expression:

def multilinearLagrangePolynomialCache :
    List ((Nat × Nat) × MultilinearPolynomial (Zmod n)) := [
  ((2, 3), .ofPairs []),
  ((5, 3), .ofPairs []),
  ((2, 1), .ofPairs []),
  ((3, 2), .ofPairs []),
  ((1, 3), .ofPairs []),
  ((4, 1), .ofPairs []),
  ((5, 4), .ofPairs []),
  ((0, 2), .ofPairs []),
  ((0, 1), .ofPairs []),
  ((1, 2), .ofPairs []),
  ((2, 2), .ofPairs []),
  ((3, 3), .ofPairs []),
  ((4, 2), .ofPairs []),
  ((2, 0), .ofPairs []),
  ((2, 5), .ofPairs []),
  ((3, 1), .ofPairs []),
  ((5, 2), .ofPairs []),
  ((5, 1), .ofPairs []),
  ((4, 3), .ofPairs []),
  ((1, 0), .ofPairs []),
  ((5, 5), .ofPairs []),
  ((0, 0), .ofPairs []),
  ((3, 5), .ofPairs []),
  ((4, 4), .ofPairs []),
  ((1, 1), .ofPairs []),
  ((3, 4), .ofPairs []),
  ((5, 0), .ofPairs []),
  ((0, 5), .ofPairs []),
  ((2, 4), .ofPairs []),
  ((4, 0), .ofPairs []),
  ((0, 4), .ofPairs []),
  ((4, 5), .ofPairs []),
  ((1, 4), .ofPairs []),
  ((1, 5), .ofPairs []),
  ((3, 0), .ofPairs []),
  ((0, 3), .ofPairs [])
] _

[Mario Carneiro]

we end up with a ton of metavariables in a ton of distinct contexts because of all the let statements, which is basically a worst case for the elaborator

[Mario Carneiro]

I thought the let-macro for list literals didn't trigger until length 64 though

[Sebastian Ullrich]

elemsAndSeps.size < 64, note the And

[Arthur Paulino]

This is my plan for caching:

def multilinearLagrangePolynomialCacheData : List $ (Nat × Nat) × List (Nat × Int) := [
  ((1, 1), [(1, 1)]),
  ((3, 1), [(1, 1)]),
  ((4, 4), [(4, 1), (5, -1), (6, -1), (7, 1), (12, -1), (13, 1), (14, 1), (15, -1)]),
  ((1, 3), [(1, 1), (3, -1), (5, -1), (7, 1)]),
  ((3, 4), [(3, 1), (7, -1), (11, -1), (15, 1)]),
  ((2, 3), [(2, 1), (3, -1), (6, -1), (7, 1)]),
  ((0, 4), [(0, 1), (1, -1), (2, -1), (3, 1), (4, -1), (5, 1), (6, 1), (7, -1), (8, -1), (9, 1), (10, 1), (11, -1), (12, 1), (13, -1), (14, -1), (15, 1)]),
  ((0, 0), [(0, 1)]),
  ((3, 2), [(3, 1)]),
  ((1, 0), [(0, 1)]),
  ((3, 3), [(3, 1), (7, -1)]),
  ((2, 2), [(2, 1), (3, -1)]),
  ((1, 2), [(1, 1), (3, -1)]),
  ((3, 0), [(0, 1)]),
  ((0, 3), [(0, 1), (1, -1), (2, -1), (3, 1), (4, -1), (5, 1), (6, 1), (7, -1)]),
  ((4, 0), [(0, 1)]),
  ((4, 2), [(0, 1), (1, -1), (2, -1), (3, 1)]),
  ((0, 1), [(0, 1), (1, -1)]),
  ((2, 4), [(2, 1), (3, -1), (6, -1), (7, 1), (10, -1), (11, 1), (14, 1), (15, -1)]),
  ((0, 2), [(0, 1), (1, -1), (2, -1), (3, 1)]),
  ((4, 1), [(0, 1), (1, -1)]),
  ((2, 0), [(0, 1)]),
  ((4, 3), [(4, 1), (5, -1), (6, -1), (7, 1)]),
  ((1, 4), [(1, 1), (3, -1), (5, -1), (7, 1), (9, -1), (11, 1), (13, 1), (15, -1)]),
  ((2, 1), [(0, 1), (1, -1)])
]

That shouldn't raise any red flag, right? No metavariables involved as far as I can see

[Mario Carneiro]

Don't use long list literals if you can avoid it

[Mario Carneiro]

longer than 64 32 elements

[Arthur Paulino]

How can I cache then? I can't be in IO

[Sebastian Ullrich]

Should we simply have a custom elaborator for list literals?

[Mario Carneiro]

you can use an init declaration

[Mario Carneiro]

the macro is terrible and needs to be replaced but last time someone posted about this leo basically said this only comes up in code which is misusing lean anyway so it's not a high priority

[Mario Carneiro]

I was planning on doing just that

[Arthur Paulino]

Where can I find an example of an init declaration?

[Mario Carneiro]

initialize foo : HashMap A B <- (bla : IO (HashMap A B))

[Mario Carneiro]

It doesn't really solve the problem of storing high information content definitions in Expr though, since it's still a regular declaration

[Mario Carneiro]

but it's generally a good idea not to lean on the elaborator too hard in such definitions, write things with explicit types

[Arthur Paulino]

But the list I wrote only has simple types

[Arthur Paulino]

Should I write a custom elaborator for lists then? Is the [] syntax the issue?

[Mario Carneiro]

yes, it's a major component of the problem in this case

[Mario Carneiro]

I would use a custom DSL to make the input terser anyway

[Arthur Paulino]

Alright, thanks! I'll report back after trying it

[Arthur Paulino]

Does the #[] syntax suffer from the same issue?

[Arthur Paulino]

Hmm, I'm getting the following error with the DSL:

maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)

[Arthur Paulino]

This is the cache file with the DSL:
https://github.com/yatima-inc/YatimaStdLib.lean/blob/ap/multilinear-extension/YatimaStdLib/MLE/Cache.lean

Why is it reaching the maximum recursion depth?

[Arthur Paulino]

Well, not that version. But it crashes if I add like 100 lines

[Arthur Paulino]

Is there something I'm doing wrong in the DSL elaborator?
https://github.com/yatima-inc/YatimaStdLib.lean/blob/ap/multilinear-extension/YatimaStdLib/MLE/CacheDSL.lean

[Mario Carneiro]

Why is mkListLit not tail recursive? It should be written using a foldr

[Arthur Paulino]

You mean the function from core, right?

[Arthur Paulino]

Maybe I can make a customized version

[Arthur Paulino]

def mkListLit (type : Expr) (xs : List Expr) : MetaM Expr := do
  let u ← getDecLevel type
  let cons := .const ``List.cons [u]
  return xs.foldr (init := mkApp (mkConst ``List.nil [u]) type) fun e acc =>
    mkApp (mkApp (mkApp cons type) e) acc

[Arthur Paulino]

Still reaching maximum depth tho :dizzy:

[Arthur Paulino]

My next attempt will be using an initializer, reading the cached polynomials from a JSON file

[Mario Carneiro]

I think that's a good idea

[Mario Carneiro]

Another suggestion I have is to try using List.append in a binary tree for long enough lists; this is kind of like what the macro was doing but without all the let stuff

[Arthur Paulino]

List.append in a binary tree? How come?

[Mario Carneiro]

that is, replace [x1, ...., x2n] with [x1, ..., xn] ++ [x(n+1), ..., x2n]

[Mario Carneiro]

It decreases the depth of the expr

[Mario Carneiro]

this is important because most lean internal functions on Expr are not tail recursive, they use the C stack directly and there is no stack splitting fallback so a lot of stuff struggles not to blow the stack

[Arthur Paulino]

That's a good thing to learn! But I feel like I should just quit this strategy of caching values on a Lean file via an IO function that (over)writes Lean code

[Mario Carneiro]

oh yeah, autogenerated lean files are always hit the hardest by these kind of restrictions

[Arthur Paulino]

I might come back asking for help on initializers on another thread though. But for now I'm satisfied with my current understanding. Thanks for all the help!

[Arthur Paulino]

Arthur Paulino said:

def mkListLit (type : Expr) (xs : List Expr) : MetaM Expr := do
  let u ← getDecLevel type
  let cons := .const ``List.cons [u]
  return xs.foldr (init := mkApp (mkConst ``List.nil [u]) type) fun e acc =>
    mkApp (mkApp (mkApp cons type) e) acc

But that could be upstreamed to core regardless