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
default.nix
Description: Binary data
_______________________________________________ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev