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
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)?
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
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 proof
