Re: [Hol-info] Poly/ML debugging facility does not work in HOL4

I'm also not using the Poly/ML debugger and don't think this has high priority. I was just curious and tried it with an old version I had lying around. With Poly/ML 5.6 and revision 15e37a5df6ea4b6680e57420257ba30b2e45ceac from 12 July 2017 it did still work. With the same Poly/ML and a current

Re: [Hol-info] Poly/ML debugging facility does not work in HOL4

I've never used the Poly/ML debugger. The HOL4 REPL is a custom piece of code (handling the lexing of “...” forms, for example), so I guess this interferes with what the debugger wants to do. If you wanted to use the debugger, you might be able to get things to work by manually use-ing the HOL

Re: [Hol-info] Poly/ML debugging facility does not work in HOL4

Thanks for your reply. Here is an example session run directly (without HOL mode), using a recent development build (commit f65c89f20626b700f7a67ef54b5c80d65a9964d6) with the experimental kernel, and with Poly/ML 5.7.1: [18:26] mario@svetlana (0) [~/hacking/hol4_exp/src] $ hol

Re: [Hol-info] Poly/ML debugging facility does not work in HOL4

It works for me, when I was debugging SML functions manipulating HOL terms, in whatever mode. I think you should provide details to let other help you figuring out the mistakes in your steps. —Chun > Il giorno 19/apr/2018, alle ore 20:42, Mario Xerxes Castelán Castro >

[Hol-info] Poly/ML debugging facility does not work in HOL4

Hello. When I tried to use the Poly/ML debugger as described in breakpoints do not work. “breakIn” does not raise an exception, but when applying the exception, the debugger is not entered. I check this within the HOL mode for Emacs,