[isabelle-dev] HOL-Codegenerator_Test error

[Manuel Eberl]

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
>