I commented out the code equation in question and HOL-Codegenerator_Test
runs through again.
Manuel
On 12/01/16 15:31, Makarius wrote:
On Tue, 12 Jan 2016, Manuel Eberl wrote:
From what I have seen so far, it seems like there are some lingering
issues with code generation in general and Codegenerator_Test in
particular that my rather innocuous change exposed, and that simply
deleting that one code equation that I added is not the solution we
want (not even in the short term).
I generally agree that things need to be done right, but for the
moment (3201ddb00097 and after) the main priority is to get back to a
repository where "isabelle build -a" works. There are already several
changes pushed on top of the bad state, which easily leads into a
situation that takes a long time to disentangle.
I have myself various changes waiting and cannot move forward now,
neither on main Isabelle nor AFP.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
