Home

Abstract

In order to run depenency tracking, nix-shell is requried. I think the old version is more suitable. The key point to run it is to create the ".nix-channels" file loaded by nix-shell (in home directory by default) to indicate the (old) version of nixpkgs.

Install nix

In this section, we will install the nix-shell, which is required by the dependency tracker

Use the official package (recommended if it works)

We are using the old version of nix-shell, since it already supports the latest version of the dependency tracker (and I couldn't make nix 2.1 work).

1. Download the corresponding (old) version from here The linux version is working for me, and extract.
2. Create ".nix-channels"(no quotation marks) in the home directory i.e. $HOME/ or ~/ with the following contents. The home directory may various on different systems (e.g. mac os). The point of this step is to choose the old version of nixpkgs (maybe an older version also works), which is the key point to use this old version of nix-shell.

   https://releases.nixos.org/nixpkgs/nixpkgs-17.03pre96825.497e6d2 nixpkgs
   

3. Install nix with (sh <nix installation pack directory>/install), which is the default commond according to manual (maybe required root privilege for this old version of nix-shell) or use proot:

Install with proot:

1. Create a directory: e.g. mkdir .nix
2. proot -b <path to the created dir>/.nix:/nix
3. sh <nix installation pack directory>/install

Remark

Don't forget to run . <home path, e.g. $HOME or ~ >/.nix-profile/etc/profile.d/nix.sh as advised by nix-shell installation.

Use my pre downloaded package (If the official pack doesn't work)

In this section, an alternative method is introduced, with the package copied from my dice machine:

1. Decompress and copy my package:

   1. The directory nix-1.10-x86_64-linux to ~/opt/nix-mnt/ (or anywhere, just change the address in nix.she below)
   2. The others to ~/

2. Install proot

3. Put the code below to a bash(\eg nix.sh) file.

   proot -b ~/opt/nix-mnt/nix-1.10-x86_64-linux/:/nix bash --rcfile ~/.nix-profile/etc/profile.d/nix.sh
   

4. run nix.sh

Get dependency tracking

There are two versions of dependency tracking that actually tested by myself. The new (latest) version has more features e.g. Don't serialise out term trees, nor proofs (faster, and require less disk storage), and maybe more stable. However, I remeber that its tracking has some problems. So I also recommend the old version (maybe both can be tried for a comparison).

git clone this rep or the identical: https://github.com/Chattered/HOL-Light-Deps

Use the old version below or skip and use the latest version

Old version (optional)

1. There's an old version which I'm using:

   git checkout b8eade5
   

2. See this issue: change the ocaml version according to the issue i.e. change rev = "toploop_hook"; to rev = "5fe9e6f2dae917cdde0b79ea26f259343d1b0d8d";

Update: This might have been solved, there's a pin version

Run dependency tracking

(in the nix environment mentioned above)

Follow the quitck start

Remark

Have error when loading proof script

Please read this

Robust way of using the json file

1. The tracked theorems (an entry at the top level) is a list of dictionaries, where each has an individual 'tracking_id', which should be more reliable than the index of the theorem in the list. i.e. t[i]['tracking_id'] may not be i, assume t is the list of tracked theorems.
2. This track is more through in terms of splitting conjunctions. e.g. ! n. n+0=n /\ 0+n=n is also split, although it's not strictly a conjunction.

If the theorem is renamed

There are a few theorems renamed in HOL Light core library (inevitable because you have to load the core library) see here. The rest are mainly from analysis.ml, which I have renamed the theorems. It's somehow confusing because you also need to fix the "simple_rose" stuff, so there are four versions of this file. I'll upload if you want it