Sequentially running selected sentences and immediately stopping when any sentence has failed

[aqjune]

Hi,

Does VSCode terminal provide a mechanism to check whether running the latest sentence failed or not? Checking 'failed or not' can be at the moment done by heuristically matching 'Error:' at the beginning of any of output lines. Actually, in the case of s2n-bignum, this is more relaxed by simply grepping 'error' or 'exception' words from the output: https://github.com/awslabs/s2n-bignum/blob/main/tools/run-proof.sh#L33 However, does VSCode terminal support getting the standard output of the running process in terminal? When I was playing with OCaml's vscode plugin, I could not find such functionality.

I was wondering because I thought it would be great if vscode-hol-light could support sequentially running selected sentences and immediately stopping when any sentence has failed. For example, assume that a user has selected this two sentences and sent it to REPL:

let x = 3 + "a";;
let y = x + x;;

Since the RHS of x is bogus, the first sentence will fail. In the current version of plugin, the second sentence is executed anyway, but if it stops immediately with some mark at first sentence there (or highlighting the first sentence differently?) a user can identify that the first sentence let x = .. was problematic.

Thanks,

[monadius]

It is possible to create a separate process for the OCaml (HOL Light) REPL which is connected to a VSCode pseudoterminal (this approach is used in the HOL4 VSCode extension). Then it will be possible to read stdout and stderr streams of the REPL and react to potential errors. But there is no easy and robust approach to recognize when the execution of a command is done by the REPL (either normally or with a failure). The OCaml REPL emits # after the command execution is done. But a command itself may print this character. Maybe it is not a serious issue. I will experiment with the separate process approach and see how well it will work for executing a sequence of commands with potential errors.

[aqjune]

I looked for a solution by myself and this indeed seems to be hard unless the toplevel implementation itself is modified to notify that evaluation is finished to the user. I think an ad-hoc workaround is to simply insert, say, print_endline "magic string";; after each statement and recognize the printed magic string as a separator. What do you think about using a pseudoterminal and omitting printing the magic string thingy in the pane visible to the user?

[aqjune]

BTW, your repo is now appearing at https://hol-light.github.io/ FYI. :)

[monadius]

It is a good idea to print some magical value after each statement. It should work for almost all cases. Unfortunately, it is not possible to detect errors in this way. But error messages can be identified with Error: ... or Exception: ....

Alternatively, it could be possible to execute all statements with Toploop.execute_phrase and Toploop.parse_toplevel_phrase functions. In this way, it should be possible to catch all exceptions.

[monadius]

BTW, your repo is now appearing at https://hol-light.github.io/ FYI. :)

I am glad to hear that. Could you also add a direct link to the Marketplace: https://marketplace.visualstudio.com/items?itemName=monadius.hol-light-simple

[aqjune]

Hi @monadius,

I have been working on writing more proofs using the latest version of this plugin for a while. The go-to definition is working flawlessly! :)

Regarding the context of this issue, I remember that our last conversation was to use an approach similar to https://github.com/aqjune/toplevel-light, but more portable in the sense that its toplevel_light.ml is simply run after the REPL is launched. I think your approach makes sense to me. Always thank your effort & let me know if you need some help!

p.s: Abdal (@abdoo8080 , I hope I found him correctly..! Hi Abdal! :D ) just also started using the plugin. :) I just wanted to introduce him.

[monadius]

Hi @aqjune

It is good to hear that everything works without any major issues and that new people are starting to use the extension (Hi Abdal!).

I am busy right now but I am going to resume my work on the extension soon. In particular, I am going to implement a pseudo terminal for the HOL Light REPL and modify the toplevel output based on the ideas from your project. It will be also possible to implement additional features by modifying the toplevel output. For example, I am thinking about special queries which can return some useful information about loaded definitions. Right now, the extension does not display any type information (unless it is explicitly given in a definition) but it may be possible to get the type information from the toplevel directly with some special commands.

[aqjune]

The pseudoterminal idea sounds exciting and I am eager to try its prototype! :)

For example, I am thinking about special queries which can return some useful information about loaded definitions. Right now, the extension does not display any type information (unless it is explicitly given in a definition) but it may be possible to get the type information from the toplevel directly with some special commands.

I think print_types_of_subterms might be helpful in this case. This option has been recently added and can have three integral values (0~2).

[abdoo8080]

Hi @monadius,

I'm an intern at AWS, currently working on constant time proofs for s2n-bignum. I recently started learning HOL Light for the project. Your VS Code extension has been invaluable in this process, especially with features like hover information, auto-completion, and go-to-definition. I hope you don’t mind if I request some additional features for the extension in the future!

it may be possible to get the type information from the toplevel

That would be super helpful!

[monadius]

Hi @abdoo8080! Feel free to request any new features or open issues if you find bugs or problems with the extension.