Unfortunately I don't know anything better than "run it again".
You could also maybe try an older HOL commit (maybe prior to
d52c7d66716ddd253b6fd40bd3d38b29a238c392) and see if that's any more
reliable.
This is all speculation on my part though. The problem could have nothing
to do with pointer equality.
On 5 October 2017 at 16:15, Heiko Becker <hbec...@mpi-sws.org> wrote:
> Hello Ramana,
>
> yes, the Mk_comb error occurs non-deterministic. Is there a temporary
> workaround for this, that I could make use of?
>
> Cheers,
>
> Heiko
>
> On 10/05/2017 12:43 PM, Ramana Kumar wrote:
>
> Hi Heiko,
>
> Does it fail every time when you try to run the proofs non-interactively
> (with Holmake)?
>
> I suspect the "Mk_comb" error, if it is non-deterministic, has to do with
> pointer equality problems, which are in the middle of being fixed.
>
> Cheers,
> Ramana
>
> On 5 October 2017 at 13:22, Heiko Becker <hbec...@mpi-sws.org> wrote:
>
>> Hello,
>>
>> I have some proofs that I could previously solve by running EVAL_TAC,
>> after modifying computeLib.the_compset with
>>
>>
>> val _ = computeLib.del_funs [sptreeTheory.subspt_def]
>> val _ = computeLib.add_funs [realTheory.REAL_INV_1OVER,
>> sptreeTheory.subspt_eq]
>>
>>
>> As it turns out, the proofs still run fine when interactively run in an
>> HOL4 emacs session, but the proofs fail when run on the command line.
>>
>> The failure either is
>>
>> HOL_ERR {message = "", origin_function = "Mk_comb", origin_structure = "T$
>> m"}
>> Uncaught exception: HOL_ERR {message = "", origin_function = "Mk_comb",
>> origin_structure = "Thm"}
>>
>> or
>>
>> (∀k.
>> k = 1 ∨ k = 0 ⇒
>> lookup k (BS (BN LN (LS ())) () (LS ())) =
>> lookup k (BS LN () (LS ())))
>>
>> Previously it sufficed to have a file myComputeLib.sml declaring the
>> structure myComputeLib and adding the two val statements above there and
>> loading that file when doing the proof with "open". When trying to debug
>> this issue, I moved the val statements in a separate tactic, declaring
>>
>> val my_eval_tac =
>> let
>> val _ = computeLib.del_funs [sptreeTheory.subspt_def]
>> val _ = computeLib.add_funs [realTheory.REAL_INV_1OVER,
>> sptreeTheory.subspt_eq]
>> in
>> EVAL_TAC
>> end;
>>
>>
>> but that did not solve my problem either.
>>
>> Can someone help me resolve this or give me a hint on how to debug this
>> issue?
>>
>> Thanks,
>>
>> Heiko
>>
>>
>> ------------------------------------------------------------
>> ------------------
>> 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
