As discussed in the Agda meeting today, checking the 1Lab with --save-metas runs out of memory (even on my desktop with 128 GiB!). Using --trace-imports, I narrowed this down to 1Lab/HIT/Truncation, and running with a few verbosity flags, I'm pretty sure it starts looping when running ∥-∥³-elim-set — it might eventually get past this, but I killed the save-metas run when memory usage went past 8GiB. Here is the trace; cc @AndrasKovacs.
Sorry for the awful reproducer, but also as discussed, I'm not really in a position to narrow it down any further this week (though cc @ncfavier, who wrote the explosive macro, and might have an idea). If anyone will work on this, keep in mind that the 1Lab only works with master (more specifically, it now needs the instance overlap pragmas).
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4