-rw-r--r-- 1761 holtrace-20250629/doc/download.md raw
To download and unpack the latest version of the HOLTrace package:

    wget -m https://holtrace.cr.yp.to/holtrace-latest-version.txt
    version=$(cat holtrace.cr.yp.to/holtrace-latest-version.txt)
    wget -m https://holtrace.cr.yp.to/holtrace-$version.tar.gz
    tar -xzf holtrace.cr.yp.to/holtrace-$version.tar.gz
    cd holtrace-$version

Then [install](install.html)
and [test](test.html).

### Archives (reverse chronological)

[`holtrace-20250629.tar.gz`](holtrace-20250629.tar.gz) [browse](holtrace-20250629.html)

Add `ot2holtrace` tool to convert OpenTheory files to HOLTrace files.

Split `holtrace_restore_allownew` off of `holtrace_restore`.

Add `hashtt` to (optionally) patch HOL Light to precompute hashes of types and terms.

In `holtrace2ml`, reject theorem names starting with digits.

In `holtrace-verify`, allow non-tyvars to be substituted for tyvars.

Set higher recursion limits in various Python scripts.

Miscellaneous documentation improvements,
including many more citations.

[`holtrace-20250624.tar.gz`](holtrace-20250624.tar.gz) [browse](holtrace-20250624.html)

In `holtrace_restore`, allow alpha-equivalent definitions of existing constants.

Print matching+creating statistics for `holtrace_restore`.

Revamp `holtrace-verify` data structures for types and terms.
This improves code clarity and provides a slight speedup.

Print some profiling information for `holtrace-save`.

In `holtrace-save`,
actively remove `$HOLTRACE_SAVE`
to avoid potential bad interactions between a previous writer
and the new writer,
just in case the filename collides.

Add a few more test traces.

Miscellaneous documentation improvements.

[`holtrace-20250617.tar.gz`](holtrace-20250617.tar.gz) [browse](holtrace-20250617.html)

First release.