Work log 2016-07-07

Got haskell-te tests mostly running (there are a few hundred, and it gets to about 150 before aborting).

One issue: taking a package src directory in explore (for use as standalone, to ensure we have needed deps) was failing since src dirs usually don’t contain default.nix (TIP benchmarks are the exception).

Added a call to nixedHsPkg (which I extracted from nixFromCabal) to ensure it’s made if it doesn’t already exist.

Clustering is killed for list-extras, as it takes more than 1GB of RAM. I’ve increased the cutoff of the timeout command to allow up to 2GB instead.

Rough plan:

Report <---------------+
                       +--- haskell-te tests pass
Heuristic cluster <----+
    numbers                                           +---- How to get Isabelle-usable TIP?
                                                      |
TIP on IsaPlanner <--- nix derivation for running <---+
                          TIP on IsaPlanner           |
                                                      +---- How to run IsaPlanner?

Some TIP-based haskell-te tests were failing since they were looking for equations from 1 cluster; we know this is a bad idea, and we want it to fail; if it didn’t, we could run it quite happily without clustering!

I’ve turned this into a check that we should run out of memory; we compare the value reported by timeout to that which we gave it as a limit.

Wrote resize-vdi.sh to find Hydra’s virtual HD file (.vdi), check its size to see whether it’s 100GB, and if not to nixops stop, resize it, then ./deploy.sh. THis gives us a 100GB (virtual) disk, but we still need to update the partition table and grow the ext4 filesystem (can do this with GParted).

IsaPlanner: How to run TIP?

We can run arbitrary scripts via:

docker run /bin/bash < foo

Attempt 1: Run docker build command in buildPhase of IsaPlanner; provide wrapper around dcker run in bin/

• This requires docker to be running as a system service.

Attempt 2: Add virtualisation.docker.enable = true to hydra-common.nix

Setting services.hydra.useSubstitutes is MUCH faster than building our own!

We should have the failure of 1-cluster TIP exploration cached, it it isn’t already…