Closed ejgallego closed 1 month ago
@Alizter memory use (approx) with patch, opening a lot of files in HoTT:
So while not the panacea, the reduction in memory use seems quite useful, in particular for devs with large .vo size.
I'm very interested in seeing your numbers.
cc: @SkySkimmer @ppedrot in case you are curious about the kind of improvements we see by sharing .vo files (in stdlib that amounts to 8% faster compilation)
Loading all of HoTT in the same server: 1169 Mw to 668 Mw , quite a considerable saving @Alizter
We add a basic .vo parsing cache; this often results in large memory savings when working simultaneously with several files.
Based on work from #641 and coq/coq#17393