Karl Palmskog (Aug 11 2022 at 19:00): Karl Palmskog (Aug 11 2022 at 19:00):based on the discussion in https://github.com/codewars/coq/pull/3 it seems the scope of Code Wars Coq will be 100% determined by historical accidents in how the serialization implementation (Marshal) is done in OCaml, i.e., the size of .vo files. This will essentially result in a 2000s era Coq environment...
Pierre-Marie Pédrot (Aug 11 2022 at 19:26):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?
Karl Palmskog (Aug 11 2022 at 19:27):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.
Karl Palmskog (Aug 11 2022 at 19:30):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)
Pierre-Marie Pédrot (Aug 11 2022 at 19:55):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.
Pierre-Marie Pédrot (Aug 11 2022 at 19:57):Also, zipping vo files won't result in a huge diminution of file size, because it's not very clever.
Pierre-Marie Pédrot (Aug 11 2022 at 19:58):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/)
Pierre-Marie Pédrot (Aug 11 2022 at 20:00):vo files are big not so much because of marshalling, but rather because we don't do much for it not to happen.
Pierre-Marie Pédrot (Aug 11 2022 at 20:00):Modules are responsible for a lot of duplication, notably.
Karl Palmskog (Aug 11 2022 at 20:01):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
Karl Palmskog (Aug 11 2022 at 20:02):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
Pierre-Marie Pédrot (Aug 11 2022 at 20:04):The good thing about compression with sharing is that it can be performed after the fact, you just need access to the vo.
Karl Palmskog (Aug 12 2022 at 10:48):@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?
Karl Palmskog (Aug 12 2022 at 10:50):(this may be better than having this in a random Zulip discussion, but there might already be similar issues I guess)
Pierre-Marie Pédrot (Aug 12 2022 at 11:15):please do
Karl Palmskog (Aug 12 2022 at 11:57):https://github.com/coq/coq/issues/16383
Last updated: Oct 13 2024 at 01:02 UTC