Re: [Hol-info] Changing thms used by computeLib

[Ramana Kumar]

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  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  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

Re: [Hol-info] Changing thms used by computeLib

[Heiko Becker]

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 > 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

[Hol-info] Changing thms used by computeLib

[Heiko Becker]

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