[Nix-dev] Intrinsically impure build process

[Marco Maggesi]

Hi everybody,

I would like to use Nix to prepare prebuilt checkpointed binaries for
the HOL Light theorem prover.  (Ideally I would like to prepare a
virtualbox appliance with HOL Light and all the related software ready
and configured.)

[Short explanation: Checkpointing means to "freeze" a running process
(i.e., unix program) and save its status in a binary file (the
ckecpointed binary) which can be later used to restart the process at
the point it has been originally interrupted.  HOL Light is an OCaml
script.  HOL Light needs this "freezing" mechanism because it has no
built functionality for saving its status.  For this and other reason,
HOL Light is troublesome for its installation, but otherwise a great
software and I  use it for teaching.]

I use BLCR to checkpoint HOL Light on NixOS.  I have a proof of
concept script (attached to this message) which works very well in
practice.  But I have a problem due to the impurity of this process.
This impurity is due to the fact that, in general, the checkpoint
binaries are not portable across different version of the kernel and
the BLCR module where the checkpoint has been performed.  This means
that the checkpointed binaries have to be regenerated each time we
reboot the system with a different kernel.

I artificially inject this impure dependency by passing to the
derivations two things:
1. the string `uname -a`, this should help take into account the
version of the running kernel
2. the path to the BLCR commands, this should help to take into
account the version of the installed BLCR module.

Thus my nix expression starts as follows:

let
  sysver = builtins.getEnv "SYSVER";
  cr_checkpoint = <blcr/cr_checkpoint>;
  cr_run = <blcr/cr_run>;
  cr_restart = <blcr/cr_restart>;
  pkgs = import <nixpkgs> {};
....

I call this expression as follows:

export SYSVER=$(uname -a)
nix-build \
  --show-trace \
  -I "blcr=/run/current-system/sw/bin" \
  -A hol_light_core \
  -o ~/bin/hol_light_core

which is quite involute.  (Actually I have small a bash script to
perform this call).

Can you suggest a better way to do the same?

Thanks,
Marco
-------------- next part --------------
A non-text attachment was scrubbed...
Name: default.nix
Type: application/octet-stream
Size: 4059 bytes
Desc: not available
Url : http://lists.science.uu.nl/pipermail/nix-dev/attachments/20130208/246bb2f9/attachment.obj