Stream: MetaCoq

Topic: Performance Info


view this post on Zulip Jason Gross (Apr 24 2023 at 01:20):

If anyone is interested in how long various files and components take to build, I've stuck some performance numbers in https://github.com/MetaCoq/metacoq/pull/956.

view this post on Zulip Jason Gross (Apr 24 2023 at 01:20):

Some highlights:

view this post on Zulip Jason Gross (Apr 24 2023 at 01:20):

The slowest files (those individually taking more than 1% of the total build time):

 4m18.65s | 1949996 ko | safechecker/theories/PCUICSafeConversion.vo
 2m31.74s | 1394392 ko | safechecker/theories/PCUICRetypingEnvIrrelevance.vo
 2m22.99s | 2870580 ko | erasure/theories/ErasureFunction.vo
 2m03.72s | 2119868 ko | safechecker/theories/PCUICTypeChecker.vo
 1m51.89s | 3812988 ko | test-suite/bugkncst.vo
 1m51.70s | 1652532 ko | safechecker/theories/PCUICSafeReduce.vo
 1m06.37s | 2264880 ko | pcuic/theories/PCUICConfluence.vo
 1m05.97s | 1416040 ko | pcuic/theories/PCUICParallelReductionConfluence.vo
 0m49.47s | 1332628 ko | safechecker/theories/PCUICSafeRetyping.vo
 0m46.92s | 2224172 ko | pcuic/theories/PCUICConversion.vo
 0m44.15s | 1567240 ko | pcuic/theories/PCUICSR.vo
 0m43.10s | 1028824 ko | erasure/theories/EEtaExpandedFix.vo
 0m43.06s | 1334704 ko | erasure/theories/Typed/OptimizeCorrectness.vo
 0m43.01s | 1247340 ko | pcuic/theories/PCUICExpandLetsCorrectness.vo
 0m39.85s | 1236828 ko | utils/theories/ByteCompareSpec.vo
 0m38.90s | 1297596 ko | pcuic/theories/PCUICParallelReduction.vo
 0m38.33s | 1041476 ko | pcuic/theories/PCUICSigmaCalculus.vo

Together, these files take 23m40s, which is about 38% of the overall build time

view this post on Zulip Jason Gross (Apr 24 2023 at 01:23):

pcuic, quotation, and safechecker are the slowest components, taking 16m14s, 13m50s, 12m22s respectively. (On a machine where the overall build takes 62m)
erasure is the next-slowest, taking 8m56s, the test-suite takes 3m47s

template-coq takes 2m10s, utils 1m09s, and the other components take under a minute each

view this post on Zulip Jason Gross (Apr 24 2023 at 01:26):

Memory-wise, the test-suite is the heaviest, needing 3812988 ko (for bugkncst.vo)
erasure needs 2870580 ko (for ErasureFunction.vo)
pcuic and safechecker need 2264880 ko and 2119868 ko respectively
everything else is 1402828 ko (for common) or lower

view this post on Zulip Matthieu Sozeau (Apr 24 2023 at 07:21):

We could just remove bugkncst, it's doing large work for nothing

view this post on Zulip Matthieu Sozeau (Apr 24 2023 at 07:22):

Interesting to see that erasurefunction is the most memorry intensive after that

view this post on Zulip Gaëtan Gilbert (Apr 24 2023 at 09:36):

we produce similar stats every CI run on Coq btw
eg https://gitlab.com/coq/coq/-/jobs/4140765796#L7987

view this post on Zulip Gaëtan Gilbert (Apr 24 2023 at 09:37):

     Time |   Peak Mem | File Name
----------------------------------------------------------------
45m54.55s | 2993776 ko | Total Time / Peak Mem
----------------------------------------------------------------
 2m37.22s | 1386524 ko | PCUICSafeConversion.vo
 2m27.03s | 2993776 ko | bugkncst.vo
 1m48.99s | 1858784 ko | PCUICConfluence.vo
 1m34.60s | 1434112 ko | ErasureFunction.vo
 1m19.81s | 1087308 ko | PCUICParallelReductionConfluence.vo
 1m15.47s | 1332244 ko | PCUICTypeChecker.vo
 1m09.22s | 1135192 ko | PCUICSafeReduce.vo
 1m08.68s |  912312 ko | PCUICRetypingEnvIrrelevance.vo
 1m00.17s | 1080496 ko | PCUICExpandLetsCorrectness.vo
 0m58.57s | 1208044 ko | PCUICSR.vo
...

view this post on Zulip Gaëtan Gilbert (May 12 2023 at 11:11):

bugkncst is still failing, please remove it if it's not that useful

view this post on Zulip Gaëtan Gilbert (May 12 2023 at 11:11):

eg https://gitlab.com/coq/coq/-/jobs/4254167090

view this post on Zulip Gaëtan Gilbert (May 22 2023 at 11:07):

bugkncst was removed https://github.com/MetaCoq/metacoq/pull/963


Last updated: Jul 23 2024 at 21:01 UTC