The size of vo files is not really related to the OCaml marshal implementation. If anything, it makes things relatively compact because it fully preserves sharing (and we hashcons preventively). Do the codewars environments also contain native compilation files, for instance?
from what I can tell, all they care about is the static Docker image size, i.e., the image generated from running the opam installation commands.
but is there really any compression applied by Marshal? We apparently don't have room for anything beyond Stdlib, because OCaml + Coq + stdlib is already above what Lean 3 requires with Mathlib (~850 MB)
Not on master, but I had a branch to compress vo files (using deflate if memory serves). It was pretty bad in terms of efficiency, because Require was taking quite an additional bit of time after that. So it's always a matter of tradeoff.
Also, zipping vo files won't result in a huge diminution of file size, because it's not very clever.
Ten years ago I wrote a small program to perform the optimal sharing of vo files, maybe we could resurrect it. (For a Rust reimplementation see https://github.com/ppedrot/kravanenn, and if you can read French there is the corresponding paper https://hal.archives-ouvertes.fr/hal-00779752/)
vo files are big not so much because of marshalling, but rather because we don't do much for it not to happen.
Modules are responsible for a lot of duplication, notably.
I don't think there are a lot of applications of Coq that care so much about space. Our only research problem with space was with
.vio I think, that could be factor 10 larger than
.vo due to all the proof state
but maybe it would be suitable for an internship or similar? It can't hurt to have it as an option to compress with sharing, if it can be done in a maintainable way
The good thing about compression with sharing is that it can be performed after the fact, you just need access to the vo.
@Pierre-Marie Pédrot do you mind if I open a Coq issue where I describe the general problem of
.vo file size and outline the possible solutions that were suggested above?
(this may be better than having this in a random Zulip discussion, but there might already be similar issues I guess)
Last updated: Jan 29 2023 at 01:02 UTC