[isabelle-dev] Duplicate theory??

Traytel Dmitriy traytel at inf.ethz.ch
Mon Apr 8 18:12:20 CEST 2019


Thanks. I had produced exactly the same changeset to the Sort_Encoding entry, but notices upon push that you had done it too. The fixed problems with UTM, have nothing to do with my change to the Isabelle repository as far as I see.

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".

Dmitriy

> On 8 Apr 2019, at 18:04, Lars Hupel <hupel at in.tum.de> wrote:
> 
>> It's worse. The entire build doesn't work, but that's not your fault. In
>> fact, this is the first faulty changeset:
>> 
>> <https://isabelle.in.tum.de/repos/isabelle/rev/3a1b2d8c89aa>
> 
> I have pushed an update that added some session imports to the AFP:
> 
> <https://bitbucket.org/isa-afp/afp-devel/commits/440a7a60b0dc560def3861aa9899c97d0f31b23b>
> 
> This should hopefully bring our build status back from "catastrophic
> red" to "red".
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev




More information about the isabelle-dev mailing list