CakeML/cakeml

Automate packaging built copies of CakeML

オープン

#555 opened on 2018/11/18

 (1 件のコメント) (0 件のリアクション) (0 人の担当者)Standard ML (98 件のフォーク)auto 404
dev experiencehelp wantedrefactoring

Repository metrics

Stars
 (1,169 個のスター)
PR merge metrics
 (PR metrics pending)

説明

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

コントリビューターガイド