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
