Re: [isabelle-dev] Failure and slowdown of JinjaThreads (due to merge desaster?)

2018-05-15 Thread Lawrence Paulson
> On 15 May 2018, at 14:51, Makarius wrote: > > Maybe also a campaign to get rid of unnecessary syntax ambiguity. Totally. Most of the time it is completely unnecessary ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] HOL-Algebra

2018-05-15 Thread Makarius
On 12/05/18 11:40, Lawrence Paulson wrote: > I’m talking about HOL-Algebra, and as I’ve seen myself, parts of it are > ancient. They desperately need updating and streamlining. > > We’ve decided that Group-Ring-Module is irremediable, and are using it > only as a list of useful results that need

Re: [isabelle-dev] Failure and slowdown of JinjaThreads (due to merge desaster?)

2018-05-15 Thread Makarius
On 15/05/18 14:31, Fabian Immler wrote: > > I did move FuncSet back to HOL-Library in isabelle/2af1f142f855 and > afp/5d961e9f8536. > It seems like this improved the performance a lot: > > isabelle/2af1f142f855 > afp/5d961e9f8536 Great, I have seen already 2af1f142f855 "move FuncSet back to

Re: [isabelle-dev] Failure and slowdown of JinjaThreads (due to merge desaster?)

2018-05-15 Thread Fabian Immler
> Am 14.05.2018 um 13:24 schrieb Fabian Immler : > > I did notice that those changes caused issues with timeouts in some AFP > sessions, and simply "fixed" those on the spot (e.g., the ones in afp/85324e3 > and afp/2ff575e hinted at problems caused by incorporating syntax for