{"name":"hol","summary":"Interactive theorem prover based on Higher-Order Logic","description":"HOL4 is the latest version of the HOL interactive proof\nassistant for higher order logic: a programming environment in\nwhich theorems can be proved and proof tools\nimplemented. Built-in decision procedures and theorem provers\ncan automatically establish many simple theorems (users may have\nto prove the hard theorems themselves!) An oracle mechanism\ngives access to external programs such as SMT and BDD\nengines. HOL4 is particularly suitable as a platform for\nimplementing combinations of deduction, execution and property\nchecking.","homepage_url":"https://hol-theorem-prover.org/","license":"BSD-3-Clause","attribute_paths":["hol"],"releases":[{"version":"4-trindemossen-2","last_updated":"2026-09-29T03:29:29Z","platforms":[{"arch":"arm64","os":"macOS","system":"aarch64-darwin","attribute_path":"hol","commit_hash":"b6c8664de9b6cc07fe5666a29f91884ba81197c4","date":"2026-09-29T03:29:29Z","outputs":[{"name":"out","path":"/nix/store/v1jkcziy3ccybbahflbash7d0l7rfcsh-hol-4-trindemossen-2","default":true}],"broken":false,"insecure":false},{"arch":"arm64","os":"Linux","system":"aarch64-linux","attribute_path":"hol","commit_hash":"b6c8664de9b6cc07fe5666a29f91884ba81197c4","date":"2026-09-29T03:29:29Z","outputs":[{"name":"out","path":"/nix/store/g28h8gz13h3k4qb1m0qqw2yvf20l5v65-hol-4-trindemossen-2","default":true}],"broken":false,"insecure":false},{"arch":"x86-64","os":"Linux","system":"x86_64-linux","attribute_path":"hol","commit_hash":"b6c8664de9b6cc07fe5666a29f91884ba81197c4","date":"2026-09-29T03:29:29Z","outputs":[{"name":"out","path":"/nix/store/0f83r9gr81vmaa174rpf7ja3yacqhikw-hol-4-trindemossen-2","default":true}],"broken":false,"insecure":false}],"platforms_summary":"Linux and macOS (Apple Silicon only)","outputs_summary":"","prerelease":false,"broken":false,"insecure":false},{"version":"","last_updated":"2026-08-12T11:28:58Z","platforms":[{"arch":"arm64","os":"macOS","system":"aarch64-darwin","attribute_path":"hol","commit_hash":"044bfe75bfe4c7bbe043dc17b5e42ea823b84a09","date":"2026-08-12T11:28:58Z","outputs":[{"name":"out","path":"/nix/store/wirw6psqynqv9jn144f3q5v8ml8pif3d-hol4-k.14","default":true}],"broken":false,"insecure":false},{"arch":"arm64","os":"Linux","system":"aarch64-linux","attribute_path":"hol","commit_hash":"044bfe75bfe4c7bbe043dc17b5e42ea823b84a09","date":"2026-08-12T11:28:58Z","outputs":[{"name":"out","path":"/nix/store/1nyf7kwmiw8jpaqy11m3rpw99d93qfdb-hol4-k.14","default":true}],"broken":false,"insecure":false},{"arch":"x86-64","os":"macOS","system":"x86_64-darwin","attribute_path":"hol","commit_hash":"3d46470bb3030020f7e1361f33514854f5bfa86d","date":"2026-06-27T07:37:20Z","outputs":[{"name":"out","path":"/nix/store/cakl6p647zpfwkr5b82s71x224xm2qha-hol4-k.14","default":true}],"broken":false,"insecure":false},{"arch":"x86-64","os":"Linux","system":"x86_64-linux","attribute_path":"hol","commit_hash":"044bfe75bfe4c7bbe043dc17b5e42ea823b84a09","date":"2026-08-12T11:28:58Z","outputs":[{"name":"out","path":"/nix/store/39n38id4gaavh0z6ifvsyrag7rylay5q-hol4-k.14","default":true}],"broken":false,"insecure":false}],"platforms_summary":"Linux and macOS","outputs_summary":"","prerelease":false,"broken":false,"insecure":false}]}