search

snu-sf / paco

A Coq library for parametric coinduction
https://github.com/snu-sf/paco
Other
43 stars 10 forks source link

Compile times for paco[N] are exponential in N #18

Closed Lysxia closed 5 years ago

Lysxia commented 5 years ago

The bulk of the compile time for the bigger files (n > 13) goes to this line: https://github.com/snu-sf/paco/blob/86dfa7c5cb40264f1c213467876eb3ff7f83ef51/src/paco15.v#L769

For each file paco[n].v, the line End Paco[n]. takes time O(2^n) to process. I have no idea why. That may be an issue inside Coq.

minkiminki commented 5 years ago

Also, I found that taken time is increased in Coq 8.8 - almost double compared to 8.7. Maybe we should report this issue to Coq developers...

minkiminki commented 5 years ago

If we move typeclass instances out of a section, the line closing the section doesn't take much time. However, defining instances outside the section takes exponential time, too. :joy: So the main bottleneck is defining typeclass instances.

jeehoonkang commented 5 years ago

Coq 8.9 was recently published. How much does it take to compile paco?

Lysxia commented 5 years ago

Coq 8.8: 170s Coq 8.9: 100s

Things are much faster!

However, the exponential behavior is still there:

# Having changed the `End PACO*` lines to
# Time End PACO16.
# Time End PACO17.
# Time End PACO18.

COQC paco16.v
Finished transaction in 3.219 secs (3.197u,0.006s) (successful)
COQC paco17.v
Finished transaction in 6.422 secs (6.394u,0.s) (successful)
COQC paco18.v
Finished transaction in 13.071 secs (13.012u,0.003s) (successful)

Since arity 18 is already quite an extremely niche case, it would be fine to close this as wontfix.

minkiminki commented 5 years ago

@Lysxia thx for testing! Did you tested with the latest commit? Since mutual coinduction was removed recently (https://github.com/snu-sf/paco/commit/7b84730e19738c94a24a6f9d84eb678406812fc1), compilation would have been much faster.

Lysxia commented 5 years ago

Oh indeed, those benchmarks were with paco 1.2.9.

With paco 2.0.0,

Coq 8.8: 100s Coq 8.9: 75s

And for the "problematic" lines:

# Time End PACO[N].
COQC paco16.v
Finished transaction in 0.472 secs (0.47u,0.s) (successful)
COQC paco17.v
Finished transaction in 0.901 secs (0.897u,0.s) (successful)
COQC paco18.v
Finished transaction in 1.838 secs (1.831u,0.s) (successful)

But of course this is hardly noticeable anymore, so you could consider this issue fixed for all practical purposes.