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
<mailto: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 <mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
<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
