search

project-everest / everest

https://project-everest.github.io/
Apache License 2.0
193 stars 29 forks source link

introduce `everest archive` #77

Closed mtzguido closed 3 years ago

mtzguido commented 3 years ago

This PR introduces an archive subcommand to generate a compressed tarball with all the relevant sources for building (and checking) Everest. After extracting the tarball, hitting make will build all of Everest without needing an external connection--- not even for fetching vale, but working OCaml and z3 installs are required. The archive does not include any Git history, which is what saves the most space, nor any Git repos at all.

This is useful if one of us needs to reproduce a build failure and has a very poor connection (for whatever reason :-) ). The compressed archive is currently 25MB, while all of the Everest repos together take up 2GB. All the sources are about 248MB, so the compression factor is about 10x. The vale binaries, which seldom change, take up about 2MB of the final compressed size of 25MB.

I ran ./everest make on an extracted archive and got a green. Most other commands do not work since they require repos.

Some possible improvements

1- Do create Git repos in the archive, but without any history. 2- Add a flag to skip vale 3- Allow to choose compressor and compression levels? 4- Tweak the everest script in the archive so it can check that it's running on archived sources, and fail gracefully.

Commit message below

Creates an archive of the everest script along with sources of all subprojects, without any git history, which is enough to build everything from scratch via ./everest make.

mtzguido commented 3 years ago

5- Maybe removing dist/ subdirectories? I actually tried this manually and didn't observe a significant reduction in the compressed size (still 25MB), so maybe not worth it. (EDIT: it shrinks by just shy of 0.5 MB.)

msprotz commented 3 years ago

This is 100% fine by me. Out of curiosity, do you e.g. ssh into a running CI container and run this command to "grab" the whole set of files easily? Or is it to share repros with someone else?

mtzguido commented 3 years ago

Out of curiosity, do you e.g. ssh into a running CI container and run this command to "grab" the whole set of files easily? Or is it to share repros with someone else?

I was thinking on the second case, but getting them from a container is also a good idea, thanks!

I think I will implement (2) (4) and (5) and update this PR. I don't think (1) is really useful and would probably adds size. Also XZ seems the to be the best of the compressors I tried. We'd end up with a 22MB file when omitting vale/ and dist/.

mtzguido commented 3 years ago

Updated. The archived script now aborts on commands that are not meant to work (like pull), and I removed some stuff that is not essential to checking everest that takes a lot of space (e.g. MLCrypto/openssl/fuzz/corpora). I got a green with this removed. The compressed archive is now 17MB including Vale, without Vale it drops to 15MB.