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

贡献者指南