It looks as if it came from
polyml/basis/FinalPolyML.sml
Michael
On 29/4/18, 20:23, "Chun Tian" <binghe.l...@gmail.com> wrote:
Thanks for the detailed explanation. Just one more question: do you know
which code file in Poly/ML sources corresponds to tools-poly/holrepl.ML?
—Chun
> Il giorno 29 apr 2018, alle ore 11:00, michael.norr...@data61.csiro.au ha
scritto:
>
> As I said earlier, the breakage is certainly caused by the way in which
the REPL executable now includes a custom lexer (for handling the various
backquote ``....`` syntaxes), and is not the standard Poly REPL. This is
exactly the change that was implemented in the heaps-reworked branch. Having to
run a separate process just to achieve that lexing has caused many difficulties
in the past, and I am definitely not inclined to go back to it.
>
> It's possible that the Poly/ML debugging facility can be re-implemented
in the new REPL; you may be able to get useful advice about how this might be
done on the Poly/ML mailing list. Such tweaking would almost certainly have to
be done against the code in tools-poly/holrepl.ML, which is basically a
slightly adjusted copy of code from the Poly/ML sources.
>
> Michael
>
> On 29/4/18, 02:56, "Chun Tian" <binghe.l...@gmail.com> wrote:
>
> 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
>
>
>
>
------------------------------------------------------------------------------
> 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
