CakeML/cakeml

Automate packaging built copies of CakeML

開放

#555 建立於 2018年11月18日

 (1 則留言) (0 個反應) (0 位負責人)Standard ML (98 個分叉)auto 404
dev experiencehelp wantedrefactoring

倉庫指標

星標
 (1,169 顆星)
PR 合併指標
 (PR 指標待抓取)

描述

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

貢獻者指南