setting up Emacs for HOL4

Question

I am a newbie of both HOL4 and Emacs. Apologize for the probably silly question.

I wish to set up Emacs for HOL4 following the instruction from https://hol-theorem-prover.org/HOL-interaction.pdf. I tried to start HOL process on Emacs with Alt-h h and pressed Enter, but Emacs returns Symbol’s function definition is void: if-let*. My .emacs.d/init.el is defined as follows. What should I do to fix the error? Thanks.

;; Added by Package.el.  This must come before configurations of
;; installed packages.  Don't delete this line.  If you don't want it,
;; just comment it out by adding a semicolon to the start of the line.
;; You may delete these explanatory comments.
(package-initialize)
(transient-mark-mode 1)
(load "/home/user/HOL/tools/hol-mode")
(load "/home/user/HOL/tools/hol-unicode")

Answer 1

The error message "Symbol’s function definition is void: if-let*" means the called function if-let* is not available (not "pre-loaded") at the moment of its call. Since you wrote this happened when you "tried to start HOL process", most probably this function was called by the HOL library.

In order to find where the function definition is located, type C-h f <if-let*> (command M-x describe-function) ¹. In my setup, the output starts with the following line:

if-let* is a Lisp macro in ‘subr-x.el’

This means if-let* is defined in the file subr-x.el (it exposes the library subr-x). The commentary section of this library says:

If you want to use this library, it's almost always correct to use:

(eval-when-compile (require 'subr-x))

Hence adding the following line to the .emacs.d/init.el before loading HOL library should fix the issue:

(eval-when-compile (require 'subr-x))

[Though it's common to load libraries with just (require '<library-name>).]

Note that the exact location of a function may depend on the GNU Emacs version and/or other specifics of a setup. Without this information at hand, this answer tries to explain how to approach the issue in a general way. (When asking a question it's advisable to specify the version of GNU Emacs and provide reproduction steps calling Emacs without user configurations: emacs -Q.)

---

1. Emacs Key Notation