Hi all,

I've noticed that the Vim mode for HOL, in particular this code:

https://github.com/HOL-Theorem-Prover/HOL/blob/master/tools/vim/vimhol.src#L...

has occasionally stopped passing back raised exceptions to the REPL.

From the UI perspective, this means the user gets no feedback when a

command fails (it appears as if nothing happened). I believe this change probably happened after the switch from Poly/ML's native use to QUse.use.

Looking at QUse, I notice that it calls the Poly/ML compiler function like this:

https://github.com/HOL-Theorem-Prover/HOL/blob/master/tools-poly/poly/quse.s...

Does anyone know whether this is going to have the same exception-raising behaviour as the native use function, or if it is indeed the culprit? Are there compiler flags or something else that could be passed to get the correct handling of exceptions?

Cheers, Ramana