partrec_code

Stream: general

[Yury G. Kudryashov]

Is def nat.partrec.code.eval slow for everyone or just me? The definition times out in with -T100000

[Yury G. Kudryashov]

I'm trying to fix compile failures in #2579 coming from mid-proof simps simplifying more than expected.

[Mario Carneiro]

If I remember the theorem you are talking about, it was slow but not that slow when I wrote it

[Mario Carneiro]

Oh, it's just the definition?

[Mario Carneiro]

there is nothing at all expensive in the definition

[Mario Carneiro]

I thought you were talking about rec_computable

[Yury G. Kudryashov]

Try to compile it in master...

[Yury G. Kudryashov]

It's hard for me to fix this because I don't understand what is happening in this file.

[Mario Carneiro]

parsing took 1.4ms
elaboration of eval took 1s
type checking of eval took 0.0133ms
decl post-processing of eval took 6.22ms

on d84de80 (12 Apr)

[Yury G. Kudryashov]

/me is downloading .oleans for this revision

[Mario Carneiro]

Confirmed timeout on master

[Mario Carneiro]

There is nothing at all remarkable about the definition. It's a recursion over the simple inductive type code, and there are no complicated elaboration problems in it

[Yury G. Kudryashov]

I'll git bisect this and come back later.

[Bryan Gin-ge Chen]

Is #2573 related?

[Mario Carneiro]

#check show ℕ →. ℕ, from λ n, n.unpair.1

this is slow

[Mario Carneiro]

aha, it's using the coercion to roption

[Mario Carneiro]

#check show ℕ →. ℕ, from λ n, roption.some (n.unpair.1)

is fine

[Mario Carneiro]

#check λ n:ℕ, (n : roption ℕ) -- also slow

[Mario Carneiro]

oh, there is no coercion to roption anymore

[Mario Carneiro]

Oh, there never was. There is a coercion from A -> B to A ->. B but the roption version of that doesn't exist because these instances don't compose:

instance : has_coe (option α) (roption α) := ⟨of_option⟩
instance coe_option {a : Type u} : has_coe_t a (option a) :=
⟨λ x, some x⟩

[Mario Carneiro]

#check ((λ n:ℕ, n : ℕ → ℕ) : ℕ →. ℕ) -- fast
#check (λ n:ℕ, n : ℕ →. ℕ) -- slow

[Mario Carneiro]

Apparently the order of operations has changed here, or there is a missing fallback or something

[Mario Carneiro]

I think it tries to coerce nat to roption nat inside the lambda instead of coercing the function types

[Mario Carneiro]

anyway, if you are in the middle of a refactor @Yury G. Kudryashov I would suggest changing those lines to

| left         := λ n, roption.some (n.unpair.1)
| right        := λ n, roption.some (n.unpair.2)

and everything else seems to still work.

[Yury G. Kudryashov]

Thank you.

[Mario Carneiro]

I think the coercion was kind of a bad idea anyway

[Yury G. Kudryashov]

↑(λ n : ℕ, n.unpair.1) is fast too

[Gabriel Ebner]

I noticed this slowness yesterday as well. I think there is a general problem with the coercion from integers to arbitrary rings see #2573. Unfortunately my PR seems to time out somewhere.

[Yury G. Kudryashov]

The first "bad" commit is ffb99a338

[Yury G. Kudryashov]

#2363

[Yury G. Kudryashov]

I have no idea why it slows down elaboration in partrec_code.

[Yury G. Kudryashov]

But in the previous commit the elaboration is much faster.

[Yury G. Kudryashov]

BTW, with an explicit ↑(λ n : ℕ, n.unpair.1) it is 10x faster than before #2363 (and 100x faster than after #2363).

[Yury G. Kudryashov]

@Gabriel Ebner Compile failed in a simp lemma in data.int.basic. I don't know why it timed out instead of failing.

[Yury G. Kudryashov]

But the whole file is still very slow compared to what we had before #2363