Re: [isabelle-dev] Shadowing of theorem names in locales

2014-01-10 Thread Clemens Ballarin 
On 28 December, 2013 19:53 CET, Florian Haftmann 
 wrote: 
 
> HOL-Complex now builds with strict naming policy for facts (again).

Thanks, that's cool.

> I have stumbled over something which needs some consideration: with
> strict naming policy, locales can be compromised by »injecting«
> duplicate facts to imported locales.

That's not cool, but I would say that is a user error.  There are other ways of 
compromising locales, for example with the sublocale command.

> This does not exhibit itself until
> the compromised locale context is (re-)entered, and I think this is not
> desirable.  My first spontaneous thought is that strictness should not
> apply during the initialisation of a locale context.

I wouldn't want to add special treatment for this.  Currently we can only 
ensure that a locale is intact by visiting its context.  It would be better if 
integrity checking could be done in an incremental fashion.  But that would 
require much more sophistication.

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

[isabelle-dev] blast flexflex pairs

2014-01-10 Thread Makarius 
This is the continuation / conclusion of the pending thread about flexflex 
pairs in blast, see also 
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-December/msg00085.html


In Isabelle/b45b1b217f43 from 01-Jan-2014 the smashing of flexflex pairs 
is already removed, just like for any other proof tools.  The general idea 
is that global goal information like maxidx and flexflex pairs (called 
tpairs internally) accumulates monotonically, without any premature 
censorship by proof tools.  Instead the cleanup is deferred to certain 
checkpoints of the system infrastructure, e.g. the goal wrappers 
Goal.prove or goals in Isar proof text.



Here is also an exhaustive list of places where flexflex pairs accumulate 
in practice due to "blast" (or indirectly via "auto"):


Isabelle/9a52ee8cae9b
AFP/4fbb736e4e28

(line 99 of "~~/src/HOL/Cardinals/Wellorder_Embedding.thy")
(line 406 of "~~/src/HOL/Library/Ramsey.thy")
(line 408 of "~~/src/HOL/Library/Ramsey.thy")
(line 318 of "$AFP/Markov_Models/ex/PCTL.thy")
(line 1162 of "$AFP/Nat-Interval-Logic/IL_TemporalOperators.thy")
(line 376 of "$AFP/Stuttering_Equivalence/PLTL.thy")
(line 384 of "$AFP/Stuttering_Equivalence/PLTL.thy")
(line 534 of "$AFP/Stuttering_Equivalence/PLTL.thy")

These incidents are rather unexciting.  I have occasionally seen other 
proof tools like "fast" produce spurious flexflex pairs as well, without 
doing any immediate harm.



I was about to push b45b1b217f43 already last year, but it was delayed by 
mysterious total failure of existence of the test environment for 
JinjaThreads.  It is still unclear what actually happened.  It might have 
been just due to extra tracing messages emitted in the test, which are 
occasionally deadly as we know already.  JinjaThread has always defined 
the edge of what is possible at all, and thus might occasionally fall off 
that edge.


So for my part, this thread can be closed now.


Makarius

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