Automate packaging built copies of CakeML

[xrchz]

HOL supports packaging a built development for reuse on another machine via its relocbuild argument to build and Holmake. However, the packaging and reuse process is a bit fiddly and complicated. Some notes on how to do it are at https://github.com/CakeML/regression/blob/master/make-relocatable-tarball.sh. This issue is to automate the process with either an executable (written in CakeML) or a Holmake target. In particular, the result should support

• Downloading a built copy of the entire CakeML repo (and its corresponding HOL repo) for reuse locally
• Development (e.g., hot-fixing) on such a relocated copy, so that results can be pushed back to GitHub
• Optionally: scalability to supporting additional (CakeML-dependent) repos

The ideal workflow would be something like:

1. Download cakeml-XYZ.tar.gz and unpack it
2. Run <magic-rebuild-command> inside cakeml-XYZ
3. Now cakeml-XYZ/{HOL,cakeml} contains usable built repos on which to do further development

And on the packaging side:

1. cd cakeml-XYZ - a built (or semi-built) working copy of the CakeML repo
2. run <magic-package-command> to produce cakeml-XYZ.tar.gz for use as above

[xrchz]

@myreen says @digama0 might have an alternative way of doing this that uses proof recording