Search results

Check the expected behavior in the examples of Help/*.hlp

Status: Open.

#139 In jrh13/hol-light;

· aqjune-aws opened on May 29, 2025

Typo in help for EQT_INTRO

Status: Open.

#135 In jrh13/hol-light;

· pqnelson opened on Apr 16, 2025

instantiate can produce terms that are not parsable

Status: Open.

#68 In jrh13/hol-light;

· htzh opened on Jun 8, 2022

[INFO] HOL Light Native

Status: Open.

#65 In jrh13/hol-light;

· htzh opened on Aug 19, 2021

unable to install hol-light on mac or centos 7.4

Status: Open.

#62 In jrh13/hol-light;

· yunjiangster opened on Apr 18, 2021

Illegal begin of top_parse

Status: Open.

#60 In jrh13/hol-light;

· AI-coder opened on Oct 11, 2020

"Comms::Receive failed" when inference the whole val dataset to generate proof_log

Status: Open.

#59 In jrh13/hol-light;

· zhou745 opened on Jul 22, 2020

Forum for HOL Light questions, collaborations etc

Status: Open.

#55 In jrh13/hol-light;

· brando90 opened on Oct 22, 2019

Installing for Apple/Mac's Unix

Status: Open.

#54 In jrh13/hol-light;

· brando90 opened on Jun 2, 2019

(Maybe) a typo in Examples/prog.ml ?

Status: Open.

#43 In jrh13/hol-light;

· zidongtuili opened on Feb 21, 2018

Missing flyspeck cong

Status: Open.

#31 In jrh13/hol-light;

· ghost opened on Dec 22, 2016

Error on the installation: Cannot find file camlp5o.cma

Status: Open.

#29 In jrh13/hol-light;

· asr opened on Dec 11, 2016