该文章介绍了如何使用来自dup_labels分支的HVM1版本，提到HVM1已被HVM2和bend取代，其唯一使用原因是试验lazy SUP节点，还介绍了相关用法。

🧐HVM1版本虽已过时，但可用于试验lazy SUP节点。此版本在某些特定情况下仍有其价值，为相关研究提供了一种途径。

📋文章详细说明了使用HVM1版本的步骤。首先需安装Nix，然后通过特定命令获取带有SUP标签的hvm1 shell，最后可使用HVM进行操作，如执行计算等。

⚠️使用HVM1时需注意一些问题，如-t 1参数使HVM使用单线程，这是因为HVM1的并行器存在bug。同时，还可参考HVM1指南以更好地理解相关内容。

Published on August 9, 2024 2:03 PM GMT

This repo provides an easy way to use an HVM1 version from the dup_labels branch. Note that HVM1 is deprecated in favor of HVM2 and bend. The only reason to use it is to experiment with lazy SUP nodes. See

Fast Discrete Program Search with HVM Superpositions (SUP nodes) - finding ADD-CARRYSolving SAT via interaction net superpositions

Usage:

Install Nix.Get a shell with hvm1 with SUP labels available via nix --experimental-features 'nix-command flakes' shell github:johannesCmayer/HVM1-SUP-Flake.Use HVM, e.g. hvm1 run -t 1 "(+ 2 3)" or hvm1 run -d true -t 1 "(+ 2 3)" to see all reduction steps.

-t 1 makes HVM use a single thread (There is a bug in the parallizer of HVM1).

See the HVM1 guide for more (have GPT read it and then try to understand the source code here by asking questions).

Discuss