A few performance improvements

[proux01]

Compilation of MathComp:

• before: 22:57 (1.53 GB)
  • HB.structure: 05:42
  • HB.instance: 02:31
  • HB.mixin: 00:19
  • HB.factory: 00:32
  • HB.builders: 00:23
  • HB.pack(_for): 00:15
• after: 17.22 (1.27 GB)
  • HB.structure: 01:38
  • HB.instance: 02:21
  • HB.mixin: 00:18
  • HB.factory: 00:32
  • HB.builders: 00:23
  • HB.pack(_for): 00:15
• mathcomp1: 06:16 (0.97 GB) (time x 2.77 (memory x 1.31))

Compilation of Analysis:

• before: 26:24 (2.49 GB)
  • HB.structure: 03:22
  • HB.instance: 02:56
  • HB.mixin: 00:29
  • HB.factory: 00:27
  • HB.builders: 00:18
• after: 20:54 (1.79 GB)
  • HB.structure: 01:02
  • HB.instance: 02:44
  • HB.mixin: 00:27
  • HB.factory: 00:25
  • HB.builders: 00:17
• analysis master: 07:49 (1.55 GB) with HB 1.4 (time x 2.67 (memory x 1.15))
  or 06:32 (1.25 GB) with same HB (time x 3.20 (memory x 1.43))

[gares]

Hum, I think accumulating the db first should actually be slower.
Ideally, if the new picky spilling code allows for it, it should be the very last thing, even after the main.

[gares]

But for that, great work!

About eta, I really don't recall why it is there. CC @CohenCyril

[CohenCyril]

But for that, great work!

About eta, I really don't recall why it is there. CC @CohenCyril

It's a internal way to achieve the same feature as HB.pack...

[proux01]

Hum, I think accumulating the db first should actually be slower.

Well it seems to be consistently a tad faster here (like 2-3% total compil time on MathComp) but no idea why.

Ideally, if the new picky spilling code allows for it, it should be the very last thing, even after the main.

I haven't tried that, I'll do.

[proux01]

So, I did try accumulating the db after main and it seems consistently 2 to 3% slower on MC2 compilation than accumulating the db first. No idea why. @gares why do you expect it to be faster?

[gares]

I think my original reasoning was wrong, but we can still improve over your solution in two ways.

The compilation cache is simplistic in the sense that the unit composing a command/tactics are considered in linear dependency order. So when one changes all the following ones are recompiled. Still units which are DBs are shared among programs, and apparently in HB that unit is large (or better it is made of many tiny units).

If you put the DB first, then it has no dependency on other files, so every time you change it and you run a command:

• the DB is extended (you compile the last unit which was added) and you cache it
• all the other units of the program are recompiled and cached

So next time you run the same command (assuming it does not change the DB) the cache hits.
If you run any other command, you do the second point above, but not the first one which is the most expensive.

If you put the DB last it is considered to depend on the previous files, so if you have 2 commands accumulating the DB over a different list of base files, well, these two "copies" of the DB have different dependencies and are recompiled independently (like in git, their hash also includes the hash of their ancestors, which are different).

So one way to improve is to introduce (in elpi) the notion of unit dependency but that is not immediate.
Another way is to make all commands the same, that is accumulate all sources but for the main entry point. Then accumulate the DB. Then the main entry point (which is very small, the few lines in structure.v). This would save the recompilation of the units that in your patch follow the DB, but could be moved before it. I don't know if that would save a measurable amount of time.

[proux01]

So you were right, absolutely no measurable performance impact (the accumulation time is indeed vastly dominated by the DB). I pushed the code with an explanatory comment nonetheless.

[gares]

Thanks for trying. But if in the end the time is the same, maybe it's better without the unneeded files accumulated in structure.v no? Or I misunderstood your measurement?

[proux01]

You're right, done.

[proux01]

Thanks!