CakeML/cakeml

Automate packaging built copies of CakeML

Aperta

#555 aperta il 18 nov 2018

 (1 commento) (0 reazioni) (0 assegnatari)Standard ML (98 fork)auto 404
dev experiencehelp wantedrefactoring

Metriche repository

Star
 (1169 stelle)
Metriche merge PR
 (Metriche PR in attesa)

Descrizione

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

Guida contributor