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 SML sources
into the standard poly REPL.
Michael
On 20/4/18, 02:44, "Mario Xerxes Castelán Castro" <marioxcc...@yandex.com>
wrote:
Hello.
When I tried to use the Poly/ML debugger as described in
<http://www.polyml.org/documentation/Tutorials/Debugging.html>
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, running “hol.bare” from the command like and
running “poly” from the command line (to confirm that debugging works as
intended without HOL). Only the later (Poly/ML without HOL4) worked.
Is there a way to use the debugger from within HOL4?
Thanks.
--
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
