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
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
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
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 S
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 ne
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 debugg
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
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 ver
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
Thanks for your reply.
Here is an example session run directly (without HOL mode), using a
recent development build (commit
f65c89f20626b700f7a67ef54b5c80d65a9964d6) with the experimental kernel,
and with Poly/ML 5.7.1:
[18:26] mario@svetlana (0) [~/hacking/hol4_exp/src]
$ hol
--
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
> ha scritto:
>
> Hello.
11 matches
Mail list logo
