Restore --without-K

[Taneb]

Very rough benchmarks (running time make test after git clean -fxd:

--without-K:

real	3m29.546s
user	3m24.136s
sys	0m4.247s

--cubical-compatible

real	4m41.801s
user	4m35.818s
sys	0m4.455s

So, --without-K takes about three quarters the time of --cubical-compatible.

I don't think we have a clear use case for using --cubical-compatible. If it turns out there is one, we should put some effort into fixing the unsupported index matches, warnings for which we're currently hiding.

[jamesmckinna]

My first thoughts (on waking up this morning) are:

• great!
• but maybe wait!? (For v3.0?)

Out of interest, as well as the time gained back, is it easy to measure the comparative memory footprint of the two versions?

[Taneb]

Out of interest, as well as the time gained back, is it easy to measure the comparative memory footprint of the two versions?

I don't know how I could do that I'm afraid

[gallais]

You can throw in +RTS -s -RTS as part of your command line arguments passed to agda.

[Taneb]

without-K:

 632,621,945,376 bytes allocated in the heap
  10,200,829,160 bytes copied during GC
   1,137,914,304 bytes maximum residency (16 sample(s))
       1,348,008 bytes maximum slop
            3910 MiB total memory in use (0 MiB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0       224 colls,     0 par   19.485s  19.631s     0.0876s    0.3997s
  Gen  1        16 colls,     0 par    1.410s   1.419s     0.0887s    0.2569s

  TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)

  SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

  INIT    time    0.003s  (  0.003s elapsed)
  MUT     time  226.217s  (228.005s elapsed)
  GC      time   20.895s  ( 21.050s elapsed)
  EXIT    time    0.001s  (  0.000s elapsed)
  Total   time  247.116s  (249.059s elapsed)

  Alloc rate    2,796,530,148 bytes per MUT second

  Productivity  91.5% of total user, 91.5% of total elapsed

cubical-compatible:

 834,231,189,000 bytes allocated in the heap
  19,884,502,840 bytes copied during GC
   1,479,585,584 bytes maximum residency (22 sample(s))
       6,731,352 bytes maximum slop
            4041 MiB total memory in use (24 MiB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0       328 colls,     0 par   32.748s  32.925s     0.1004s    0.8408s
  Gen  1        22 colls,     0 par    3.504s   3.523s     0.1601s    0.5611s

  TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)

  SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

  INIT    time    0.002s  (  0.002s elapsed)
  MUT     time  278.413s  (279.927s elapsed)
  GC      time   36.252s  ( 36.448s elapsed)
  EXIT    time    0.001s  (  0.000s elapsed)
  Total   time  314.667s  (316.377s elapsed)

  Alloc rate    2,996,380,881 bytes per MUT second

  Productivity  88.5% of total user, 88.5% of total elapsed

[jamesmckinna]

OK, IIUC, the change takes 75% of time, and roughly the same for memory as well. Sold!