HOL Terminal Basic Issues, Syntax and Related Commands

[jjoneslivingstone]

How do I get out of this without necessarily have to open a new OCaml prompt and reload HOL libs?

ARITH_RULE `(a + x + b * y + a * y) EXP 3 + (b * x) EXP + (a * x + b * ;;

;;
‘(a * x + b * y + a * y) EXP 3 + (b * x) EXP 3 +
( a * x + b * y + b * x) EXP 3 + (a * y) EXP 3 = (a * x + a * y + b * x) EXP 3 + (b * y) EXP 3 + (a * y + b * y + b * x) EXP 3 + (a * x) EXP 3‘;;

;;

^[
^[[D
^[[C
end
;;

[maggesi]

This often comes because you forget to close a backtick (``).
It can be solved by closing the backtick, e.g., by sending the sequence
`;;
Hope it helps.

[jjoneslivingstone]

Yes. Solved with it. It was the earliest backtick which let the issue open. Thank you.

[jjoneslivingstone]

Pardon me again: the issue was also due to the fact I was in need to correct the operator in the proposition. How may I correct a single character individuating it with the cursor instead of erasing the whole phrase till the point in question? Thank you.

[maggesi]

How may I correct a single character individuating it with the cursor instead of erasing the whole phrase till the point in question?

Short answer: it is not possible.

Long answer: there are a few workaround:

1. Use line editors such as ledit or rlwrap.
2. Use an improved OCaml toplevel such as utop.
3. Never type your commands directly in the OCaml terminal. Instead write them in a text editor and copy/paste to OCaml. Most editors can be configured give support for this.

Personally I use option 3:
I run OCaml in a VScode terminal and I use the function workbench.action.terminal.runSelectedText (that I mapped to control-alt-enter).
My current setup, based on VScode devcontainers, is here: https://github.com/maggesi/hol-light-devcontainer