Observation: .agdai files recently became much bigger

[WolframKahl]

With very recent development versions, I see significantly larger .agdai files. I'd guess this is connected with some of the changes around #1923. -v profile:7 information is attached:

large_agdai_2016-04-07_AContext2_log.txt

    Alloc (MB)  Max.Res.(MB)  AllocRate   real    productivity  agdai

schroeder (Phenom II 3.20GHz 16GB):
3.26 1,015,557    2,056   1,195,935,463  15m24.551s  92.0%   39,109,826
3.32   992,514    2,467   1,080,745,467  16m32.879s  92.6%   39,760,448
3.34 1,051,980    3,593   1,181,405,815  16m20.362s  91.0%   54,049,270

heraklit: (Phenom II 2.80GHz 16GB):
3.26  1,015,556   2,056   1,174,061,435  15m28.735s  93.2%   39,109,826
3.34a 1,051,979   3,593   1,151,273,672  16m46.904s  91.0%   54,049,592

Agda-2.4.3.34 is d14b90b pulled 2016-04-07, compiled with ghc-7.10.3; with standard library pulled as sub-module: 196dcce

Agda-2.4.3.34a is bcfcd19 pulled 2016-04-06, compiled with ghc-7.10.3; with standard library pulled as sub-module: 196dcce

Agda-2.4.3.32 is 33f5bbf pulled 2016-03-31, compiled with ghc-7.10.3; with standard library pulled as sub-module: 196dcce

Agda-2.4.3.26 is e2d0a78 pulled 2016-03-03, compiled with ghc-7.10.3; with standard library pulled as sub-module: dcc2ab7

[andreasabel]

I guess we should understand why this happens before releasing it.

[UlfNorell]

I've put two new things in interfaces recently:

• set of names in scope (e628420)
• display forms (24ed64c)

The former could reasonably easily be recomputed on reading an interface. The latter, not so much. If it's the display forms that are the problem it might be that I'm storing more of them that are strictly necessary.

[WolframKahl]

On Fri, Apr 08, 2016 at 01:52:01AM -0700, Ulf Norell wrote:

I've put two new things in interfaces recently:

• set of names in scope (e628420)

Are those before dead-code elimination? If yes, that would partially undo the good effects of dead-code elimination...
(Peak memory use also appears to increase as a consequence, and typechecking run-time, too.)

[UlfNorell]

If those sets really are only the names in scope, then they would not include dead code, but of course it might be that the interfaces contain more scope data than it should really need.

Did you check that it is the name sets that are the culprits?

[WolframKahl]

On Fri, Apr 08, 2016 at 05:57:16AM -0700, Ulf Norell wrote:

Did you check that it is the name sets that are the culprits?

How do I inspect .agdai files?

[andreasabel]

That is a long standing issue, that we cannot easily see what really ends up in the agdai files. However, you can run your tests with the additional -v profile.serialize:20 flag and see which quantity increases from the older Agda version to the newer one. Thanks!

[WolframKahl]

On Fri, Apr 08, 2016 at 07:05:05AM -0700, Andreas Abel wrote:

That is a long standing issue, that we cannot easily see what really ends up in the agdai files.

Try to have somebody hack on that at AIM! 😉

However, you can run your tests with the additional `-v profile.serialize:20' flag and see which quantity increases from the older Agda version to the newer one.

I'll try.

Wolfram

[UlfNorell]

Oh.. I was thinking you would just try the two commits I gave above to see where the problem was introduced. The display forms were added after the scope stuff.

[WolframKahl]

-v profile.serialize:20 had significant allocation and time costs, but apparently did not produce any additional information. Almost the whole time difference seems to be accounted for just in Serialization. I'll probably try those two commits tonight.

With Agda-2.4.3.34:

5936366128  55697984 5163310016  0.248  0.248 1369.609 1371.244    0    0  (Gen:  0)
6333515256 204320152 5369111600  1.075  1.075 1379.479 1381.111    0    0  (Gen:  0)
1045062528 4207874000 4220869920  7.590  7.588 1388.425 1390.056    0    0  (Gen:  1)
 Finished Categoric.OCC.DirectPower.PolaritiesGC.
 Checking Categoric.OSGC.PowerRes (/var/tmp/kahl/svn/C/RATH-Agda/trunk/Categoric/OSGC/PowerRes.lagda).
 Finished Categoric.OSGC.PowerRes.
7218851400  27090112 4250775592  0.139  0.139 1397.338 1399.041    0    0  (Gen:  0)
Finished AContext2.
Total                        1,397,480ms
Miscellaneous                   12,983ms
Parsing                            827ms
Parsing.Operators               18,261ms
Import                             201ms
Deserialization                    716ms
Scoping                          8,770ms
Scoping.InverseScopeLookup       1,482ms
Typing                         104,968ms
Typing.OccursCheck               9,967ms
Typing.CheckLHS                543,202ms
Typing.CheckLHS.UnifyIndices       118ms
Termination                         92ms
Termination.RecCheck             6,221ms
Positivity                      42,309ms
Injectivity                        230ms
ProjectionLikeness               2,119ms
Coverage                           272ms
Highlighting                       926ms
Serialization                  534,304ms
Serialization.Sort               2,432ms
Serialization.BinaryEncode      29,286ms
Serialization.Compress           2,088ms
DeadCode                        75,705ms
ModuleName                           1ms

127809312      2608     86208  1.899  1.898 1399.399 1401.108    0    0  (Gen:  1)
     1144                      0.000  0.000

1,278,722,083,832 bytes allocated in the heap
  40,811,775,944 bytes copied during GC
   4,220,869,920 bytes maximum residency (11 sample(s))
      21,451,224 bytes maximum slop
           12936 MB total memory in use (209 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0       153 colls,     0 par   78.962s  78.951s     0.5160s    2.8058s
  Gen  1        11 colls,     0 par   39.254s  39.245s     3.5678s    7.5882s

  INIT    time    0.012s  (  0.012s elapsed)
  MUT     time  1279.271s  (1281.002s elapsed)
  GC      time  118.216s  (118.196s elapsed)
  EXIT    time    1.899s  (  1.899s elapsed)
  Total   time  1399.399s  (1401.108s elapsed)

  %GC     time       8.4%  (8.4% elapsed)

  Alloc rate    999,570,814 bytes per MUT second

  Productivity  91.6% of total user, 91.4% of total elapsed


real    23m21.441s
user    23m14.718s
sys     0m5.013s

[andreasabel]

Ah, sorry, this option only collects the additional information, but does not output it. Haha!
-v profile:20 should work. Mea culpa.

[andreasabel]

You should get something like

Accumlated statistics
A.Name  (fresh)                                                17
A.Name (reused)                                                60
A.QName  (fresh)                                               11
A.QName (reused)                                               79
ByteString  (fresh)                                             0
ByteString (reused)                                             0
Double  (fresh)                                                 0
Double (reused)                                                 0
Integer  (fresh)                                               19
Integer (reused)                                               64
Node  (fresh)                                                 910
Node (reused)                                               2,258
Shared Term  (fresh)                                            0
Shared Term (reused)                                            0
String  (fresh)                                                33
String (reused)                                               139
equal terms                                                    11
icode ((Maybe AbsolutePath),[Interval' ()])                    81
icode ()                                                      138
icode (Int,[Char])                                              1
icode (ModuleName,Scope)                                        6
icode (ModuleName,Section)                                      3
icode (ModuleName,Word64)            
...

[asr]

How do I inspect .agdai files?

FWIW, you can use -v main:50 which prints the .agdai file.

[WolframKahl]

Does -v main:50 print only the last .agdai file, or all those checked in the current run? (The latter compress to 50MB in the example here...)

[asr]

Only the last .agdai file.

[WolframKahl]

Now I ran -v profile:20 -v profile.serialize:20 also with Agda-2.4.3.32; the two log files are attached. The most blatant differences, from a quick look with kompare, are:

                                         2.4.3.32   2.4.3.34
icode CtxId                              78,120    3,592,879
icode DisplayForm                         9,900      454,222
icode DisplayTerm                         9,916      454,238
icode Open DisplayForm                    9,900      454,222
icode Set QName                               /       47,520
icode [(QName,[Open DisplayForm])]            /          111
icode [Term]                              9,900      454,222

2016-04-08-AContext2-Agda-2.4.3.32_profile.serialize.log.txt
2016-04-08-AContext2-Agda-2.4.3.34_profile.serialize.log.txt

[WolframKahl]

set of names in scope (e628420)

That change made .agdai files only a little bit larger, but seems to have had a beneficial effect on run time: Added a e628420 line to the summary:

       Alloc (MB)  Max.Res.(MB)  AllocRate   real    productivity  agdai

schroeder (Phenom II 3.20GHz 16GB):
3.26    1,015,557    2,056   1,195,935,463  15m24.551s  92.0%   39,109,826
3.32      992,514    2,467   1,080,745,467  16m32.879s  92.6%   39,760,448
e628420   993,412    2,489   1,215,769,528  14m43.524s  92.5%   40,493,606
3.34    1,051,980    3,593   1,181,405,815  16m20.362s  91.0%   54,049,270

[UlfNorell]

I did some pruning of exported display forms that should fix the problem. On the standard library the interface files went from 5% bigger than before 24ed64c to 0.2% bigger.

[WolframKahl]

For my example, the effect has disappeared, too: Summary with new last line for 7ba987b:

       Alloc (MB)  Max.Res.(MB)  AllocRate   real    productivity  agdai
3.26    1,015,557    2,056   1,195,935,463  15m24.551s  92.0%   39,109,826
3.32      992,514    2,467   1,080,745,467  16m32.879s  92.6%   39,760,448
e628420   993,412    2,489   1,215,769,528  14m43.524s  92.5%   40,493,606
3.34    1,051,980    3,593   1,181,405,815  16m20.362s  91.0%   54,049,270
7ba987b   988,687    2,516   1,236,226,441  14m27.983s  92.2%   40,493,758

Thank you!