Re: [isabelle-dev] Open Issues with JinjaThreads entry

2011-10-03 Thread Gerwin Klein
On 04/10/2011, at 4:59 PM, Andreas Lochbihler wrote:

>>> the traditional isatest's AFP-Test did not report any failures the last few 
>>> days,
>>> but the emerging testboard infrastructure mentions failures over the last 
>>> few versions, and the current tips
>>> 
>>> 76aec35b4898934df700ee54ce4d8fb7b99b0388:AFP,fa3715b35370fd27bc9e6bd03fad4a34b0724af3:Isabelle
>>> 
>>> still seem to be broken.
>>> 
>>> For people involved in this issue, here is a more detailed report:
>>> 
>>> http://isabelle.in.tum.de/reports/Isabelle/report/37c2d104871b443f8b6dbd0a8b8b0314
>> 
>> The report just ends with "Interrupt". Is it possible that this is a 
>> time-out or similar?
> I would not call it broken - it's just lack of resources. It important line 
> in the log is
> 
> Run out of store - interrupting threads

Ah, didn't spot that. This indeed is the usual out of memory problem.


> The tail of the output log tells me that the interrupt occured when one of 
> the huge locales get opened. On my local machine, JinjaThreads requires to 
> build in single-threaded mode about 12G of memory plus a few more when the 
> heap image is written.

Yes, I can confirm that: our server logs show a spike each night at around 12G. 
The test runs with -M 1 -q 0 -p 0 for JinjaThreads. 

Interesting to see that the spike is for opening the locale. This is one of the 
things that might hit us as well.

Cheers,
Gerwin

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


Re: [isabelle-dev] Open Issues with JinjaThreads entry

2011-10-03 Thread Andreas Lochbihler

the traditional isatest's AFP-Test did not report any failures the last few 
days,
but the emerging testboard infrastructure mentions failures over the last few 
versions, and the current tips

76aec35b4898934df700ee54ce4d8fb7b99b0388:AFP,fa3715b35370fd27bc9e6bd03fad4a34b0724af3:Isabelle

still seem to be broken.

For people involved in this issue, here is a more detailed report:

http://isabelle.in.tum.de/reports/Isabelle/report/37c2d104871b443f8b6dbd0a8b8b0314


The report just ends with "Interrupt". Is it possible that this is a time-out 
or similar?
I would not call it broken - it's just lack of resources. It important line in 
the log is


Run out of store - interrupting threads

The tail of the output log tells me that the interrupt occured when one of the 
huge locales get opened. On my local machine, JinjaThreads requires to build in 
single-threaded mode about 12G of memory plus a few more when the heap image is 
written.


Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbih...@kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum 
in der Helmholtz-Gemeinschaft

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


Re: [isabelle-dev] cs. 3911cf09899a

2011-10-03 Thread Florian Haftmann
> On 10/03/2011 04:59 PM, Florian Haftmann wrote:
>>> +text {* Definitions could be moved to Transitive_Closure if they are
>> of more general use. *}
>>
>> is there any striking reason *not* to do so in the first place?  At a
>> first glimpse I can't see anything which relates to Enum.thy in those
>> theorems.
>>
> Well, the definition is made because it is not possible to define
> recursive functions
> inlined in other definitions in Isabelle.
> Otherwise, I could have avoided it at all.

I do not doubt the necessity or purpose of the definition, which has
nothing recursive.  I just remark that it could have gone to
Transitive_Closure in the first place.

>> In my opinion it is high time to abandone the tradition of such comment
>> jokes in the HOL theories: if theorems are there, they *will* be used,
>> or at least it is not at our judgment for whom they are useful.  So it
>> is best to have the theorems where they belong to, unless bootstrap
>> reasons dictate something else.
> 
> The theorems are useful for my development, but I can't judge if they
> are useful
> in general.

Indeed.  Nobody can in first instance.

> More specifically, adding this definition correctly would also require
> to prove many
> more basic lemmas, such as introduction and elimination rules.
> In this way, I am following a long tradition of tool developers,
> defining constants for
> their "internal" purposes, which we hope are not picked up by users.
> You can find these traditions in almost every tool in the HOL image.

That's very fine.  But also those »internal« constants ought to reside
in appropriate places, e.g. internal_split in Product_Type.thy, nat_aux
in Int.thy, dummy_term and valapp in Code_Evaluation.

If a constant is supposed to be »internal«, it's good practice to hide
it in the namespace.

There have also been examples of operations which started as being
considered »internal« but later one it has been discovered that users
have defined their own variant of it.  AFAIR, Sum_Type.Projl was such a
thing.

Such a thing like ntrancl seems general enough that also users could
benefit from it and therefore I would not view it as internal, but this
is in the first place my personal opinion.  If such things are buried
somewhere users will start to define their own private copy which leads
to duplication.

The lack of fundamental proof rules is no obstacle in the first place:
experiences shows that if a definition is useful, theorems start to
agglomerate soon.

> But what you are suggesting is that anything related to some concept
> must be in that
> specific theory.

The »must« is too strict.  But I argue that if I have a bin labeled
»chocolate« and one labeled »cookies«, it is straightforward to put the
chocolate in the first bin and the cookies in the latter if nothing
speaks against it.

> But there are obvious counterexamples, such as More_List, and different
> Util Theories
> that contain specific definitions and lemmas, sofar only used in those
> developments.

More_List and More_Set are things which I have on my todo list and hope
to be able to tackle after the 'a set issue.  But also these theories
have already made a step from »specific« to »general«: they came into
being by factoring out generic stuff from specific applications.

It's not clear to me to which »Util« theories you are referring to;  the
unintegrated auxiliary theories in various AFP session surely are a
problematic issue, but involve different issues of meta-organization
than the distribution.

> If you have strong feelings about this being at the wrong place, you can
> move it.

I have no »feelings«, just an educated guess that sometimes somebody
*will* move it, either by necessity or by psychological strain.  In an
amortized view, you do not save any work by leaving it as it is.

> If it hinders the efforts, it might actually be because the predicate
> and set distinction has consequences,
> we have overlooked sofar.
> 
> The definition of card(inality) is clearly related to sets.
> 
> But will there also exist a definition of the cardinality of a predicate?
> For lemmas about the tranclp predicate, one needs the number of values
> for which a relation is true (the cardinality).
> 
> So, what's the opinion on this?

Just inline the cardinality for predicates into the main theorem.  There
is no need for a separate definition.

I guess the following AFP problem results from that fundamental change:
http://isabelle.in.tum.de/reports/Isabelle/report/11aa8e74cf064dc9bb9c10f72882a9d0

Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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


Re: [isabelle-dev] cs. 3911cf09899a

2011-10-03 Thread Lukas Bulwahn

On 10/03/2011 04:59 PM, Florian Haftmann wrote:

+text {* Definitions could be moved to Transitive_Closure if they are

of more general use. *}

is there any striking reason *not* to do so in the first place?  At a
first glimpse I can't see anything which relates to Enum.thy in those
theorems.

Well, the definition is made because it is not possible to define 
recursive functions

inlined in other definitions in Isabelle.
Otherwise, I could have avoided it at all.


In my opinion it is high time to abandone the tradition of such comment
jokes in the HOL theories: if theorems are there, they *will* be used,
or at least it is not at our judgment for whom they are useful.  So it
is best to have the theorems where they belong to, unless bootstrap
reasons dictate something else.



The theorems are useful for my development, but I can't judge if they 
are useful

in general.
More specifically, adding this definition correctly would also require 
to prove many

more basic lemmas, such as introduction and elimination rules.
In this way, I am following a long tradition of tool developers, 
defining constants for

their "internal" purposes, which we hope are not picked up by users.
You can find these traditions in almost every tool in the HOL image.

But what you are suggesting is that anything related to some concept 
must be in that

specific theory.
But there are obvious counterexamples, such as More_List, and different 
Util Theories
that contain specific definitions and lemmas, sofar only used in those 
developments.


If you have strong feelings about this being at the wrong place, you can 
move it.



+subsection {* An executable card operator on finite types *}
+
+lemma
+  [code]: "card R = length (filter R enum)"
+by (simp add: distinct_length_filter[OF enum_distinct] enum_UNIV

Collect_def)

Our current efforts for having 'a set as type constrcutor will turn this
superfluous if not hindering.


I was aware of this aspect when writing this lemma.
If it hinders the efforts, it might actually be because the predicate 
and set distinction has consequences,

we have overlooked sofar.

The definition of card(inality) is clearly related to sets.

But will there also exist a definition of the cardinality of a predicate?
For lemmas about the tranclp predicate, one needs the number of values 
for which a relation is true (the cardinality).


So, what's the opinion on this?


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


[isabelle-dev] cs. 3911cf09899a, ctd.

2011-10-03 Thread Florian Haftmann
A further remark:

> 1.17 +definition ntrancl :: "('a * 'a => bool) => nat => ('a * 'a => 
> bool)"
> 1.18 +where
> 1.19 + [code del]: "ntrancl R n = (UN i : {i. 0 < i & i <= (Suc n)}. R ^^ 
> i)"

Canonically and keeping in mind the upcoming 'a set, this would be

definition ntrancl :: "nat => ('a * 'a) set => ('a * 'a) set"

Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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


[isabelle-dev] cs. 3911cf09899a

2011-10-03 Thread Florian Haftmann
Hi Lukas,

> +text {* Definitions could be moved to Transitive_Closure if they are
of more general use. *}

is there any striking reason *not* to do so in the first place?  At a
first glimpse I can't see anything which relates to Enum.thy in those
theorems.

In my opinion it is high time to abandone the tradition of such comment
jokes in the HOL theories: if theorems are there, they *will* be used,
or at least it is not at our judgment for whom they are useful.  So it
is best to have the theorems where they belong to, unless bootstrap
reasons dictate something else.

> +subsection {* An executable card operator on finite types *}
> +
> +lemma
> +  [code]: "card R = length (filter R enum)"
> +by (simp add: distinct_length_filter[OF enum_distinct] enum_UNIV
Collect_def)

Our current efforts for having 'a set as type constrcutor will turn this
superfluous if not hindering.

Florian


-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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