[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