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
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
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
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
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.
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
> 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.
Thanks for your feedback!
I did what Lars suggested (96a43caa).
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).
Fabian
On 1/17/2019
On 17/01/2019 21:54, Makarius wrote:
>
> The problem behind this: Angeliki got administrative push-access to the
> Isabelle repository, without anybody at Cambridge showing her how to use it.
>
> There is of course README_REPOSITORY, but the text is long. Here is the
> ultra-short version:
>
>
On 17/01/2019 21:42, Lars Hupel wrote:
>> Strip the accidental changes from the repository?
>
> Never strip public changesets.
Indeed. "Fixing" a desaster by non-monotonic operations is a desaster
squared.
>
>> Back out the changes?
>
> You can't really back out merges, as far as I know.
>
> Strip the accidental changes from the repository?
Never strip public changesets.
> Back out the changes?
You can't really back out merges, as far as I know.
> Or do a no-op merge from a successor of the last working version?
This is also not possible, I think.
Do this instead:
$ hg revert
The changesets a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7 seem to be
the result of some mercurial/merge accident.
They break HOL-Analysis, and it is not really clear from the history why
and how to repair it.
The last working version is 56acd449da41.
Any opinions on what would be the best
12 matches
Mail list logo
