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

[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
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL-Algebra

[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 to be done again.

Just one oddity in HOL-Algebra: It claims canonical theory names like
"Group", "Ring", "Module". Thus the main HOL session needs to evade via
non-standard names "Groups", "Rings", "Modules" (the latter is new in
2af1f142f855).


Just for theory names, we now have session-qualifiers, i.e. HOL.Group
vs. HOL-Algebra.Group would work, but the internal name spaces are not
qualified separately, and a merge does not work.

At some point, I would like to see the long theory name also as internal
name space qualifier, e.g. "HOL-Algebra.Group", but there are some
remaining problems:

  * It needs to be implemented properly, in particular for tools that
pretend to know Isabelle name space policies (by analyzing the structure
of full names).

  * Non-identifiers as session names are bad, e.g. a constant name
HOL-Algebra.Group.group cannot be used within a term. We would have to
rename many sessions. This is particularly difficult in AFP, where
session names and entry names (with resulting URLs) should usually coincide.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[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
HOL-Library (amending 493b818e8e10)" and guessed that it might be related.

Concerning readability of the history:

  * I did not even notice that 493b818e8e10 moved FuncSet to main HOL
(such a change would usually also need a NEWS entry).

  * The log message of 2af1f142f855 does not explain anything, it is
merely a parrot of the formal diff (e.g. when viewed compactly with "hg
view").

Log messages should tell important information known at the time of the
commit, without making unfounded claims or "announcements". This is
important to understand the situation later (weeks, months, years, decades).

The commit 2af1f142f855 alone, without extra explanations, could just as
well have been motivated by "someone else noticed the move of FuncSet,
did not like it, and told me privately to amend it".


> In JinjaThreads/Common/ExternalCall.thy one can see that e.g., in definition 
> red_external_aggr, the funcset syntax → causes
> "Ambiguous input⌂ produces 32768 parse trees" and therefore takes 6 minutes 
> (instead of 1 second).

We probably need more systematic support to detect such situations.
Maybe also a campaign to get rid of unnecessary syntax ambiguity.

Even more ambitious: porting the latest generation of Earley parsing to
Isabelle/ML, see also https://jeffreykegler.github.io/Marpa-web-site


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[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 FuncSet 
> into Complex_Main).
> This was just to keep everything going, but I was well aware that I needed to 
> take a closer look at the problems caused there and resolve them properly 
> (e.g., not exposing FuncSet-syntax in Complex_Main).
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
-
Finished JinjaThreads (0:35:12 elapsed time, 2:28:07 cpu time, factor 4.21)
0:35:24 elapsed time, 2:28:07 cpu time, factor 4.18

Before it was:
isabelle/48262e3a2bde
afp/7dde4e79f45a
-
Finished JinjaThreads (0:54:35 elapsed time, 3:32:25 cpu time, factor 3.89)
0:58:01 elapsed time, 3:43:03 cpu time, factor 3.84

We will have to wait for the results on
https://isabelle.sketis.net/devel/build_status/AFP_slow_64bit_6_threads/index.html#session_JinjaThreads
to see whether this is actually back to normal or whether there are more 
performance problems.

In JinjaThreads/Common/ExternalCall.thy one can see that e.g., in definition 
red_external_aggr, the funcset syntax → causes
"Ambiguous input⌂ produces 32768 parse trees" and therefore takes 6 minutes 
(instead of 1 second).

Fabian




smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev