Re: [isabelle-dev] not working

2015-04-28 Thread Makarius 

On Tue, 28 Apr 2015, Larry Paulson wrote:

Today I added some material about complex transcendental functions, and 
then tested as usual. Two things didn’t work: HOL-Hoare_Parallel and 
HOL-Proofs-ex. I fixed the former myself. No idea what’s wrong with the 
latter.


I am presently not on the isabelle-dev repository, but here are some 
hints nonetheless.



### theory "XML_Data"
### 20.149s elapsed time, 37.337s cpu time, 13.947s GC time
*** exception Size raised (line 173 of "./basis/LibrarySupport.sml")
*** 
*** At command "ML_val" (line 59 of "~~/src/HOL/Proofs/ex/XML_Data.thy")

Unfinished session(s): HOL-Proofs-ex


The Size exception above refers to this example:

text {* Some fairly large proof: *}

ML_val {*
  val xml = export_proof @{thm Int.times_int.abs_eq};
  val thm = import_proof thy1 xml;
  @{assert} (size (YXML.string_of_body xml) > 5000);
*}


It means that the text representation of the proof term is bigger than 
64MB, which is the limit of heap objects for Poly/ML on x86.  This may be 
seen as a reminder of invisible concrete walls that surround the whole 
game of ever growing proof libraries, walls that David Matthews has 
continuously moved further to enlarge the playground.  One day we will 
have to give up x86, though, and the entry to the game will be 16 GB 
memory.



For now it should be possible to find a different example with a smaller 
proof object instead of Int.times_int.abs_eq above, or to tune the proof 
of Int.times_int.abs_eq to reduce its recorded term size -- there might be 
something bad elsewhere that causes the sudden increase of size.



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

Re: [isabelle-dev] not working

2015-04-28 Thread Tobias Nipkow 
That was my mistake. I committed something I did not mean to commit because it 
caused too much nontermination when I tried it with testboard. Thanks for 
alerting me. I have just undone it.


However, HOL-Proofs-ex still fails in the same manner, I have no idea why.

Tobias

On 28/04/2015 17:27, Larry Paulson wrote:

Today I added some material about complex transcendental functions, and then 
tested as usual. Two things didn’t work: HOL-Hoare_Parallel and HOL-Proofs-ex. 
I fixed the former myself. No idea what’s wrong with the latter.

~/isabelle/Repos/src/HOL: hg id
bd773c47ad0b tip

Larry


val xml =
[<5><:><5><:><5><:><5><:><4><:><4>...<:><:>...<:><5><:><5>...<:><11 0="179192" 1="Nat.arity_type_nat">...<:><11 0="370383" 1="Int.arity_type_int"><:><5><:><0 0="HOL.type_class">...<:><0 0="Pure.type">...<:><:/><:><:/><:/><:><0/><:><5><:><5><:><5><:><5>...<:><5>...<:><5><:><5>...<:><11 0="370601" 
1="Int.cr_int_def">...<:><5><:><5><:><5>...<:><5>...<:><5><:><5>...<:><5>...<:><5><:><5><:><5><:><5><:><5>...<:><5>...<:><5><:><5>...<:><11 0="179192" 1="Nat.arity_type_nat">...<:><5><:><5><:><5>...<:><5>...<:><5><:><5>...<:><5>...<:><5><:><5><:><4><:><4>...<:><:>...<:><5><:><5>...<:><11 0="179192" 1="N

at.arity_type_nat">...<:><5><:><5><:><4>...<:><5>...<:><5><:><5>...<:><5>...]:

Encode.body
val thm =
"Abs_Integ ?xa * Abs_Integ ?x =
 Abs_Integ
  ((case ?xa of (x, y) => %(u, v). (x * u + y * v, x * v + y * u)) ?x)":
thm
### theory "XML_Data"
### 20.149s elapsed time, 37.337s cpu time, 13.947s GC time
*** exception Size raised (line 173 of "./basis/LibrarySupport.sml")
***
*** At command "ML_val" (line 59 of "~~/src/HOL/Proofs/ex/XML_Data.thy")
Unfinished session(s): HOL-Proofs-ex

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





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

[isabelle-dev] not working

2015-04-28 Thread Larry Paulson 
Today I added some material about complex transcendental functions, and then 
tested as usual. Two things didn’t work: HOL-Hoare_Parallel and HOL-Proofs-ex. 
I fixed the former myself. No idea what’s wrong with the latter.

~/isabelle/Repos/src/HOL: hg id
bd773c47ad0b tip

Larry


val xml =
   
[<5><:><5><:><5><:><5><:><4><:><4>...<:><:>...<:><5><:><5>...<:><11
 0="179192" 1="Nat.arity_type_nat">...<:><11 
0="370383" 1="Int.arity_type_int"><:><5><:><0 
0="HOL.type_class">...<:><0 
0="Pure.type">...<:><:/><:><:/><:/><:><0/><:><5><:><5><:><5><:><5>...<:><5>...<:><5><:><5>...<:><11
 0="370601" 
1="Int.cr_int_def">...<:><5><:><5><:><5>...<:><5>...<:><5><:><5>...<:><5>...<:><5><:><5><:><5><:><5><:><5>...<:><5>...<:><5><:><5>...<:><11
 0="179192" 
1="Nat.arity_type_nat">...<:><5><:><5><:><5>...<:><5>...<:><5><:><5>...<:><5>...<:><5><:><5><:><4><:><4>...<:><:>...<:><5><:><5>...<:><11
 0="179192" 
1="Nat.arity_type_nat">...<:><5><:><5><:><4>...<:><5>...<:><5><:><5>...<:><5>...]:
   Encode.body
val thm =
   "Abs_Integ ?xa * Abs_Integ ?x =
Abs_Integ
 ((case ?xa of (x, y) => %(u, v). (x * u + y * v, x * v + y * u)) ?x)":
   thm
### theory "XML_Data"
### 20.149s elapsed time, 37.337s cpu time, 13.947s GC time
*** exception Size raised (line 173 of "./basis/LibrarySupport.sml")
*** 
*** At command "ML_val" (line 59 of "~~/src/HOL/Proofs/ex/XML_Data.thy")
Unfinished session(s): HOL-Proofs-ex

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