how to get start after these commands are done about hol-light HOT 6 CLOSED

There is a tutorial for HOL Light (https://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf). Its installation instruction is a bit outdated, but the remaining sections are still valid.
I typically use HOL Light VSCode plugin (https://github.com/monadius/vscode-hol-light) to edit a proof.

from hol-light.

thank you, it's really helpful.i have almost finished

vscode

I have already download vscode in my window system, and it says I needn't to download an aditional one in wsl, which have caused a collision.I ran the vscode in my wsl by a "$code" command(a error about unc host was encoutered and i fixed it by adding wsl.localhost to allowed hosts in settings).

hol-light plug-in

i installed the hol-light extension,and configured the hol-light path. then I create a hl file named "hello_world.hl" in vscode. as the extension suggest, the file can be recognised and the completion hover is offerred (but no highlight) as i'm typing.

interactive way in the CLI

i find in the pdf you offerred that i can access the hol-light in the ocaml CLI, with ocaml as the toplevel basics and hol-light being a library, just through a single use command.but i come across a sequence of errors such like "Error: Unbound module Num" ,which seems miss of num lib, caused by incomplete dependency building or something.

problems

i want to use hol-light in a script, and the only thing left is how to excute or parse it.
the uncommon highlight and the error of "use command" is irrelevant but may indicate something wrong with my deployment

from hol-light.

interactive way in the CLI

For installation, probably you will want to read README of this HOL Light repository. You can use make switch to install dependent packages.

from hol-light.

thank you. i solved the "unbound module num" problem by installing the "num" module .and eventually i have my first hol-light term defined in the interactive way.

what about the vscode-plugin. how to parse it supposing i create a file named "hello_world.hl" containing one line "x+1;;" in vscode

from hol-light.

alright, i find the solution in the extension's introduction about commands ,Alt + E can Sends selected text to HOL Light. thanks, the problems are solved

from hol-light.

Could you close this issue if the problem is resolved?

from hol-light.