[isabelle-dev] Duplicate theory??

Lawrence Paulson lp15 at cam.ac.uk
Mon Apr 8 18:16:51 CEST 2019


I assumed that HOL itself was broken too. Is that not so?

I’m wondering how to test my changes to HOL itself (never mind the AFP).

Larry

> On 8 Apr 2019, at 17:15, Lars Hupel <hupel at in.tum.de> wrote:
> 
>> The policy for the AFP has always been in the past: it is ok to fix
>> things a few days later. Not sure why this deserves the adjective
>> "catastrophic".
> 
> "catastrophic" because the failure prevented the *entire AFP* from being built, hence the error message.
> 
> Maybe Makarius could change that behaviour and instead of "build" refusing to build anything, only exclude malformed sessions.




More information about the isabelle-dev mailing list