Re: [isabelle-dev] Status of afp-2015
Confirmed: isabelle/18267ceb10b5 + afp/d8cda568cd81 pass the full build. This one took 6:52h, but was running more sequentially, I guess. Cheers, Gerwin > On 28 Apr 2015, at 11:16 pm, Makarius wrote: > > On Tue, 28 Apr 2015, Gerwin Klein wrote: > >> Have also kicked off a full test on afp-2015 now and if all goes well, I’ll >> switch it to automated once a day until the release. > >> Looks like another bit of infrastructure overhaul is needed in my scripts >> for running afp-test in parallel for an upcoming release and devel. >> >> I don’t expect that things will break much, though. > > OK. My manual test was succesful with Isabelle/18267ceb10b5 and > AFP/d8cda568cd81 -- it takes about 2.5h total. > > I don't expect significant changes to the Isabelle2015 anymore, especially > not changes in the proof tools and libraries. > > > Makarius The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Status of afp-2015
On Tue, 28 Apr 2015, Gerwin Klein wrote: Have also kicked off a full test on afp-2015 now and if all goes well, I’ll switch it to automated once a day until the release. Looks like another bit of infrastructure overhaul is needed in my scripts for running afp-test in parallel for an upcoming release and devel. I don’t expect that things will break much, though. OK. My manual test was succesful with Isabelle/18267ceb10b5 and AFP/d8cda568cd81 -- it takes about 2.5h total. I don't expect significant changes to the Isabelle2015 anymore, especially not changes in the proof tools and libraries. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Status of afp-2015
Have also kicked off a full test on afp-2015 now and if all goes well, I’ll switch it to automated once a day until the release. The email notification will probably not be working, though, because it’s running on a Linux machine in Sydney instead of Darwin in Munich (so it doesn’t interfere with the rest of the setup in Munich too much). Will check the logs manually once a day and report back if things break until I figure out something better. Looks like another bit of infrastructure overhaul is needed in my scripts for running afp-test in parallel for an upcoming release and devel. I don’t expect that things will break much, though. Cheers, Gerwin > On 28 Apr 2015, at 7:26 pm, Makarius wrote: > > On Tue, 28 Apr 2015, Gerwin Klein wrote: > >> You’re right, it is currently not tested automatically. I was going to set >> this up on the weekend, but didn’t manage to. >> >> As far as I’m aware, there weren’t any commits to afp-2015 after the fork >> apart from one update that was a leaf node that I checked manually. >> Isabelle-RC has moved, though. > > With the formal changesets, it is easy to check the true diffs, but there is > nothing significant to see. > > I've just made yet another manual test: at least one of my AFP directory > locations was on a different repository clone. Test is still running ... > > > Makarius The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] not working
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] Status of afp-2015
On Tue, 28 Apr 2015, Gerwin Klein wrote: You’re right, it is currently not tested automatically. I was going to set this up on the weekend, but didn’t manage to. As far as I’m aware, there weren’t any commits to afp-2015 after the fork apart from one update that was a leaf node that I checked manually. Isabelle-RC has moved, though. With the formal changesets, it is easy to check the true diffs, but there is nothing significant to see. I've just made yet another manual test: at least one of my AFP directory locations was on a different repository clone. Test is still running ... Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] not working
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
Re: [isabelle-dev] Status of afp-2015
These entries probably fail because of some changes of mine. However, some of them, eg KBPs work for me with afp-2014/5b629c5350bf. Tobias On 28/04/2015 15:25, Makarius wrote: I am confused about the status of afp-2015 wrt. current Isabelle2015 release candidates. According to my own post on isabelle-users, Isabelle2015-RC1 and AFP/a44a0c9e17ef correspond to each other. It was a stable point after days of chaos before entering the final release process. That relative stability seems to have been lost again: isabelle-release/18267ceb10b5 afp-2015/d8cda568cd81 Unfinished session(s): Call_Arity, Circus, Depth-First-Search, FunWithFunctions, Girth_Chromatic, KBPs, Launchbury, Markov_Models, Random_Graph_Subgraph_Threshold, Separation_Logic_Imperative_HOL, UpDown_Scheme That is without the "slow" sessions. Is afp-2015 actually tested anywhere? Makarius ___ 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
Re: [isabelle-dev] Status of afp-2015
Yes, that is precisely right. However, there were changes in the Isabelle release candidates since the fork, and these should be tested (against afp-2015). Cheers, Gerwin > On 28 Apr 2015, at 3:30 pm, Larry Paulson wrote: > > Maybe I don’t understand how this works. I was under the impression that both > the main repository and the AFP had been forked in preparation for the > release, allowing people to add new material to the repository (with > appropriate corrections to the AFP) that would be independent of the current > release and included only in the one after that. > > Larry > >> On 28 Apr 2015, at 14:25, Makarius wrote: >> >> I am confused about the status of afp-2015 wrt. current Isabelle2015 release >> candidates. >> >> According to my own post on isabelle-users, Isabelle2015-RC1 and >> AFP/a44a0c9e17ef correspond to each other. It was a stable point after days >> of chaos before entering the final release process. >> >> That relative stability seems to have been lost again: >> >> isabelle-release/18267ceb10b5 >> afp-2015/d8cda568cd81 >> >> Unfinished session(s): Call_Arity, Circus, Depth-First-Search, >> FunWithFunctions, Girth_Chromatic, KBPs, Launchbury, Markov_Models, >> Random_Graph_Subgraph_Threshold, Separation_Logic_Imperative_HOL, >> UpDown_Scheme >> >> That is without the "slow" sessions. >> >> >> Is afp-2015 actually tested anywhere? >> >> >> Makarius >> ___ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Status of afp-2015
You’re right, it is currently not tested automatically. I was going to set this up on the weekend, but didn’t manage to. As far as I’m aware, there weren’t any commits to afp-2015 after the fork apart from one update that was a leaf node that I checked manually. Isabelle-RC has moved, though. Will look at getting the test up again tonight. Cheers, Gerwin > On 28 Apr 2015, at 3:25 pm, Makarius wrote: > > I am confused about the status of afp-2015 wrt. current Isabelle2015 release > candidates. > > According to my own post on isabelle-users, Isabelle2015-RC1 and > AFP/a44a0c9e17ef correspond to each other. It was a stable point after days > of chaos before entering the final release process. > > That relative stability seems to have been lost again: > > isabelle-release/18267ceb10b5 > afp-2015/d8cda568cd81 > > Unfinished session(s): Call_Arity, Circus, Depth-First-Search, > FunWithFunctions, Girth_Chromatic, KBPs, Launchbury, Markov_Models, > Random_Graph_Subgraph_Threshold, Separation_Logic_Imperative_HOL, > UpDown_Scheme > > That is without the "slow" sessions. > > > Is afp-2015 actually tested anywhere? > > > Makarius > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] not working
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
Re: [isabelle-dev] Status of afp-2015
Maybe I don’t understand how this works. I was under the impression that both the main repository and the AFP had been forked in preparation for the release, allowing people to add new material to the repository (with appropriate corrections to the AFP) that would be independent of the current release and included only in the one after that. Larry > On 28 Apr 2015, at 14:25, Makarius wrote: > > I am confused about the status of afp-2015 wrt. current Isabelle2015 release > candidates. > > According to my own post on isabelle-users, Isabelle2015-RC1 and > AFP/a44a0c9e17ef correspond to each other. It was a stable point after days > of chaos before entering the final release process. > > That relative stability seems to have been lost again: > > isabelle-release/18267ceb10b5 > afp-2015/d8cda568cd81 > > Unfinished session(s): Call_Arity, Circus, Depth-First-Search, > FunWithFunctions, Girth_Chromatic, KBPs, Launchbury, Markov_Models, > Random_Graph_Subgraph_Threshold, Separation_Logic_Imperative_HOL, > UpDown_Scheme > > That is without the "slow" sessions. > > > Is afp-2015 actually tested anywhere? > > > Makarius > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Status of afp-2015
I am confused about the status of afp-2015 wrt. current Isabelle2015 release candidates. According to my own post on isabelle-users, Isabelle2015-RC1 and AFP/a44a0c9e17ef correspond to each other. It was a stable point after days of chaos before entering the final release process. That relative stability seems to have been lost again: isabelle-release/18267ceb10b5 afp-2015/d8cda568cd81 Unfinished session(s): Call_Arity, Circus, Depth-First-Search, FunWithFunctions, Girth_Chromatic, KBPs, Launchbury, Markov_Models, Random_Graph_Subgraph_Threshold, Separation_Logic_Imperative_HOL, UpDown_Scheme That is without the "slow" sessions. Is afp-2015 actually tested anywhere? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
