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 
> <marioxcc...@yandex.com> ha scritto:
> 
> 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

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail

------------------------------------------------------------------------------
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

Reply via email to