On 18/01/2019 21:55, Tobias Nipkow wrote:
> Hey, I wanted to join the party! But all bugs have been fixed now and
> Makarius will notify you of the correct changeset.
Yes, see Isabelle/b18353d3fe1a.
Despite the carnival season, I am presently working with David Matthews
to make the canononical "i
Hey, I wanted to join the party! But all bugs have been fixed now and Makarius
will notify you of the correct changeset.
Tobias
On 18/01/2019 21:42, Makarius wrote:
On 17/01/2019 22:54, Fabian Immler wrote:
Luckily, a diff with a8faf6f15 revealed quite obviously what went wrong
during the me
On 17/01/2019 22:54, Fabian Immler wrote:
>
> Luckily, a diff with a8faf6f15 revealed quite obviously what went wrong
> during the merges, so I could easily redo Angeliki's tagging (689997a8).
>
> We should be back to normal (regarding isabelle build -a).
That was Isabelle/94284d4dab98, but Tobi
Just to clarify: the merging problem was the result of certain lemmas
that had been moved around
among 3 theories (Determinants, Change_of_Vars and
Finite_Cartesian_Product) by Fabian
simultaneously with me tagging the theories.( Even though I did pull
several times daily.)
Simple merging did no
On 18/01/2019 11:42, Lars Hupel wrote:
>> The problem behind this: Angeliki got administrative push-access to the
>> Isabelle repository, without anybody at Cambridge showing her how to use it.
>
> Before we start blaming individual people, this is not a person problem,
> but a tooling problem. In
Sorry, I’m to blame for this. When Angeliki mentioned she had merge conflicts,
it turned out she didn’t have diffmerge (or anything similar) on her machine.
By the time I got everything configured and managed to resolve the conflicts
(largely by discarding her work unfortunately), I unthinkingly
> The problem behind this: Angeliki got administrative push-access to the
> Isabelle repository, without anybody at Cambridge showing her how to use it.
Before we start blaming individual people, this is not a person problem,
but a tooling problem. Industry has figured out this problem years ago.