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!

[jamesmckinna]

I admire the understatement, but I think that this is (probably) why I'd rather have this as a v3.0 change... and be documented/announced/released as such.

While I agree with @JacquesCarette 's arguments on #2792 that this was a change we should not have made for v2.x, now that we have, I'd be happier if the v2.x line of stdlib were the cubical-compatible releases, but with our overall strategy for v3.0 to make clean breaks with all kinds of legacy, this one included, that we start the v3.y line with the reversion enacted here.

[JacquesCarette]

Philosophically, this makes sense.

Pragmatically, I'm afraid that v3.0 might take quite a lot of time, and so we would be waiting for the benefits quite a while. I guess if we planned to have v3.0.1, v3.0.2, v3.0.3, in quick succession, all of them being breaking before eventually stabilizing, I'd be happy with that.

But I don't want to wait a full year or more to have a released version of stdlib in its current state.

[jamesmckinna]

@JacquesCarette I absolutely agree. It's already a year (or more!) since we decided to delay v3.0 in favour of v2.4. But I maybe hoped that we could tie off v2.4 soon ('for a suitable definition of soon'), rather than wait yet another year. Maybe some of @MatthewDaggitt 's more cautious/conservative approach to these things has rubbed off on me!