Re: [Hol-info] Poly/ML debugging facility does not work in HOL4

2018-04-29 Thread Michael.Norrish 
It looks as if it came from 

  polyml/basis/FinalPolyML.sml

Michael

On 29/4/18, 20:23, "Chun Tian"  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"  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" 
 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

Re: [Hol-info] Poly/ML debugging facility does not work in HOL4

2018-04-29 Thread Chun Tian 
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"  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"  
>> 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



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

Re: [Hol-info] Poly/ML debugging facility does not work in HOL4

2018-04-29 Thread Michael.Norrish 
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"  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" 
 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