[isabelle-dev] HOL-Codegenerator_Test error
makarius at sketis.net
Tue Jan 12 15:31:49 CET 2016
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.
More information about the isabelle-dev