How to modify the proof script for dependency tracking

The different goal types

Sometimes the dependency tracking fails, because a different goal type is used in the tracking system:

1. In HOL Light (original version), goalstate has type (term list * instantiation) * goal list * justification.
2. However, in the tracking system, the goalstate has type (term list * instantiation) * goal list * justification * (unit Meta.srced * tac_thm list) list rose_bud
3. There's one extra bit in the new goalstate, so some conversion is required. As I (we) don't know what should be added to the last bit, a naive conversion can be tried. There's a function simple_rose that has the type (term list * instantiation) * goal list * justification -> goalstate) i.e. old_goalstate->new_goalstate. I asked Phil, and he said this is the right way to do this.
4. When functions are created involving the goalstate operation, we need to change the code. So there are two cases where a modification is required:
   1. When a value in goalstate type is returned, it has to be changed to the new type e.g. here. We use simple_rose to convert the goal to new type.
   2. When a value in goalstate type is required (as input e.g. matching), it was a 3-tuple but has to be 4-tuple now. We change the matching from let (a,b,c)=d to let (a,b,c,_) =d (because we don't know how to use the last bit anyway). e.g. here

Some files I have changed

I have already changed some files, they are uploaded in this repo now:

Name	Location	Remark
The Jordan Curve Theorem	hollight/Jordan_track
IsabelleLight	hollight/IsabelleLight_tracking	For loading list Hilbert (from Phil) and the lists.ml from Petros
tools	hollight/tools_tracking	For loading lists.ml from Petros
Library/analysis.ml	hollight/analysis.ml	For loading poly.ml and Jordan Curve Theorem

Just in case you need this, the HOL Light version I'm using is 6573d7767dd769890ff21f17050a4fd6c92d207c Sun Nov 27 2016.

Since you don't want to overwrite the version in HOL Light for daily use. These files can be left in this directory (hollight) or softlinked here. I've uploaded the whole directory for these libraries, but not all files are changed and some are for setting paths. A diff command can easily find out the changes. I think simply linked all the libraries to hollight will work (i.e. link Jordan_track, IsabelleLight_tracking, and tools_tracking to Jordan, IsabelleLight, and tools). Except that the address may need to be changed for analysis.ml. analysis.ml is also required by poly.ml, so although poly.ml requires no change for the goalstate type, we need to change its first line and load the modified analysis.ml (or we load analysis.ml first and comment the file loading in poly.ml.