I also observed the same: it was working but now it doesn’t work. Without that debugger I couldn't have finished my thesis work in which there’s a huge recursive SML function of 400+ lines [1] to compute the transitions from any CCS term and returns a theorem.
—Chun [1] https://github.com/HOL-Theorem-Prover/HOL/blob/master/examples/CCS/CCSConv.sml > Il giorno 20 apr 2018, alle ore 07:11, Thomas Tuerk <tho...@tuerk-brechen.de> > ha scritto: > > 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 version > 689b9eb3eccdebc314664a6e583c8d8bc76c0591 I get the behavior described by > Mario. > > Thomas > > > On 20.04.2018 06:02, michael.norr...@data61.csiro.au wrote: >> 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 > > > ------------------------------------------------------------------------------ > 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
signature.asc
Description: Message signed with OpenPGP
------------------------------------------------------------------------------ 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
