Hi Michael, I… took some time trying to find out the revision which breaks the debugging facility. After many rounds of binary searching, I found that, until the following revision
e5fc0f365922cfd11ec32c4531983d20892777a6 (Improving naming of
bit-vector signed division constants…) on Sep 11, 2017
the debugging facility still works, then after the next revision it’s broken:
69125acadde5cf629e4b9d5604bc33b226c57b5d (Merge branch
'heaps-reworked’) on Sep 13, 2017
many revisions after e5fc0f36 is not buildable under Poly/ML 5.7 (until
c52815a4 “Comment out optional(?) code that doesn't work/exist under poly5.7…”)
so I used Poly/ML 5.6 to confirm above broken revisions.
I’ll try to dig into your branch 'heaps-reworked’ to further find out the exact
changes related to the breaks of debugging facility.
Could you please make some efforts to fix this issue? I think HOL should be
considered as a normal Poly/ML with theorem proving built in, and in theory HOL
executions can be used for developing any SML-based applications, and the the
debugging facility is very important for large complex applications.
Regards,
Chun
> Il giorno 26 apr 2018, alle ore 01:22, michael.norr...@data61.csiro.au ha
> scritto:
>
> The REPL (allows great interactive unit-testing) and annotation with print
> statements.
>
> Michael
>
> On 25/4/18, 03:36, "Mario Xerxes Castelán Castro" <marioxcc...@yandex.com>
> wrote:
>
> What do you use for debugging, or instead of debugging?
>
> On 19/04/18 23: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.
> --
> 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
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
