dev experiencehelp wantedrefactoring
Métriques du dépôt
- Stars
- (1 169 étoiles)
- Métriques de merge PR
- (Métriques PR en attente)
Description
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:
- Download
cakeml-XYZ.tar.gzand unpack it - Run
<magic-rebuild-command>insidecakeml-XYZ - Now
cakeml-XYZ/{HOL,cakeml}contains usable built repos on which to do further development
And on the packaging side:
- cd
cakeml-XYZ- a built (or semi-built) working copy of the CakeML repo - run
<magic-package-command>to producecakeml-XYZ.tar.gzfor use as above