[isabelle-dev] CoreC++ broken
andreas.lochbihler at inf.ethz.ch
Tue Jan 5 08:39:46 CET 2016
I had a look and it should work now in 1cdd27b5d78a (with Isabelle2016-RC0). I do not know
what exactly went wrong or what caused the failure. The problem seems to be related to
some change in theory imports. It seems as if code_pred cannot retrieve the specification
of a constant under certain import orders, but I am not familiar enough with these
Isabelle internals to pinpoint the problem.
On 30/12/15 00:20, Makarius wrote:
> AFP/CoreC++ is broken (already quite some time).
> The current situation:
> CoreC++ FAILED
> *** Failed to load theory "CoreC++" (unresolved "Execute")
> *** No such predicate: "SubObj.path_via"
> *** At command "code_pred" (line 214 of "~/isabelle/afp-devel/thys/CoreC++/Execute.thy")
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev