how to get start after these commands are done

[YoungShrank]

settings

I have build the OCaml dependences following the directions in readme file under the ubuntu subsystem of windows. and start my first ocaml project following this web

problems

i assume the next step may be open an editor,but there is no more directions.

attempts

i do have found some turials on the official web,but it seems these tips are exclusively for this project

thanks

this may be a foolish issue. i’m not a professor but interested in the prover. thank you for giving me some tips or explanations

[aqjune]

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.

[YoungShrank]

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

[aqjune]

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.

[YoungShrank]

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

[YoungShrank]

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

[aqjune]

Could you close this issue if the problem is resolved?