Re: [isabelle-dev] I don't understand isatest AFP report
On 15.05.2013, at 8:01 PM, Ondřej Kunčar kun...@in.tum.de wrote: Hi! This is the last report about AFP from isatest: The status of the following AFP entries changed or remains FAIL: [Containers] was removed. Last status was ok. [Launchbury] is new. Status is ok. Full entry status at http://afp.sourceforge.net/status.shtml AFP version: development -- hg id 3f56bba4ee3a Isabelle version: devel -- hg id e116eb9e5e17 Test ended on: macbroy2, Tue May 14 12:28:46 CEST 2013. It says that Containers was removed. But does it actually mean FAIL? Because Containers is currently broken because of my changeset but I didn't learn about it. And this web page doesn't list Containers at all (because it was removed? but it's still in the repository though): http://afp.sourceforge.net/status.shtml What's going on is that the somewhat primitive AFP test doesn't understand the output of isabelle build correctly. It's currently getting its list of sessions by scanning through the output, trying to find messages for failed or successful sessions. This worked reliably for IsaMakefiles, because there was a separate invocation for each session and there was delimiting output before/after each session. Of course, that didn't provide any parallelism or other goodies. In this instance, there was some kind of JVM problem which then caused the scan on the AFP test side to miss the Container session entirely and the tool therefore concluded that it must have been removed. We've had other failures before, were build failed globally because a file dependency was missing, and the AFP test then concluded that all sessions must have been removed. All of that is pretty unstable communication based on a lot of assumptions on my part. I should probably re-think how AFP test determines if a session was successful or not. First cut a this: - get a list of entries separately, i.e. from the thys/ROOTS file - try to identify only successful sessions from build output With that, we'd get correct removed/new messages, and failure messages when anything unexpected happens. Does this sound reasonable? Cheers, Gerwin 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] I don't understand isatest AFP report
Here's a summary of the story with Containers: AFP/db25a6127308 to AFP/58dc11da7731 add the Containers entry to AFP-devel in the version that works with Isabelle2013. In AFP/664abd899c58, Gerwin dropped the import of Code_Char_ord that Florian removed in Isabelle/599ff65b85e2. This implicitly dropped the import of Char_ord, which caused some even more errors. In AFP/599ff65b85e2, Dmitriy dropped the session Containers-Benchmarks to avoid crashes in the build tool. AFP/3f56bba4ee3a contains all the necessary adaptations to run with Isabelle/ae755fd6c883 and re-activates Containers-Benchmarks. Unfortunately, this situation lasted only for less than 4 hours. Isabelle/a4d81cdebf8b breaks Containers again, but Ondřej did not notice because the AFP test report is strange. Andreas On 15/05/13 13:09, Makarius wrote: On Wed, 15 May 2013, Ondřej Kunčar wrote: This is the last report about AFP from isatest: The status of the following AFP entries changed or remains FAIL: [Containers] was removed. Last status was ok. [Launchbury] is new. Status is ok. Full entry status at http://afp.sourceforge.net/status.shtml AFP version: development -- hg id 3f56bba4ee3a Isabelle version: devel -- hg id e116eb9e5e17 Test ended on: macbroy2, Tue May 14 12:28:46 CEST 2013. It says that Containers was removed. But does it actually mean FAIL? Because Containers is currently broken because of my changeset but I didn't learn about it. And this web page doesn't list Containers at all (because it was removed? but it's still in the repository though): http://afp.sourceforge.net/status.shtml I am also confused, and still trying to catch up with the ups and downs of this new session. Yesterday I had a working situation in Isabelle/ae755fd6c883 and AFP/0b521abc0487. I have also spent some time to robustify the Isabelle build process (leading up to Isabelle/5fdca5bfc0b4) to prevent sessions bombing the JVM by producing tons of output. Here it is via higher-order unification going amiss and producing lots of tracing messages. I guess that is actually coming from some transfer tools. We've had several surprises about HO-unification from TUM people recently, but I am still lagging behind to follow-up on all that. (Basically, fully-general HO is rather ambitious and rarely used systematically in tool implementations these days.) 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
Re: [isabelle-dev] I don't understand isatest AFP report
On Wed, 15 May 2013, Andreas Lochbihler wrote: In AFP/599ff65b85e2, Dmitriy dropped the session Containers-Benchmarks to avoid crashes in the build tool. I still have this on my list to look again, if further Isabelle/Scala robustification is needed beyond the state in Isabelle/5fdca5bfc0b4. The general attitude of Isabelle build is to manage Isabelle sessions reliably, but it requires some odd measures on the JVM side, and possibilities for break down will always remain (despite the old timeout and the new process_output_limit.) BTW, timeout was missing in thys/Containers/ROOT until AFP/0b521abc0487. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] I don't understand isatest AFP report
On Wed, 15 May 2013, Gerwin Klein wrote: What's going on is that the somewhat primitive AFP test doesn't understand the output of isabelle build correctly. It's currently getting its list of sessions by scanning through the output, trying to find messages for failed or successful sessions. This worked reliably for IsaMakefiles, because there was a separate invocation for each session and there was delimiting output before/after each session. The difference here is that make did not crash in its own right, but in exchange had less control over what was run and how it failed. Doing the management of Isabelle build by a single JVM process gives the usual advantages and disadvantages of explicit management: potentially more control (e.g. for better scheduling) and more ways of breakdown. After the bombing of the JVM by tons of tracing messages, I've briefly reconsidered the old file-system based approach, but that might then lead to bombing of some file-server, which is even worse. Instead there are now more tight timeouts (AFP/fb808eb615) and a global process_output_limit of 100MB -- the JVM can still crash trying to decode the resulting log file again (UTF-16 sucks). Do the AFP test scripts have additional resource limits? In this instance, there was some kind of JVM problem which then caused the scan on the AFP test side to miss the Container session entirely and the tool therefore concluded that it must have been removed. Basically the Isabelle build executable should follow the usual conventions of return codes: 0: all fine 1: program error, e.g. some sessions failed / remains outdated 2: systemic failure, e.g. some unexpected exception within the JVM Apart from that the stdout/stderr have a certain meaning, somewhat depending on the return code. Also note that current Isabelle/ea123790121b allows do give more resources to the JVM that is running Isabelle build. E.g. like this: ISABELLE_BUILD_JAVA_OPTIONS=-Xmx4096m -Xss2m The default is a bit more frugal, to improve chances that it works on small machines that users might have. (The JVM is very inflexible concerning resource management; it tends to misbehave for small heap size, but fails to start up for too big heaps.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Global build failures of the AFP in the testboard
On Thu, 25 Apr 2013, Dmitriy Traytel wrote: Hi all, since Containers are in the AFP mira results in global crashes of the build tool (http://isabelle.in.tum.de/testboard/Isabelle/report/2cef0644d3d7416f8d7cea92e24fd694). By global I mean that no session is built at all due to an outdated (wrt Isabelle repository, e.g. 916271d52466) import of src/HOL/Library/Efficient_Nat.thy in the session Containers-Benchmarks. That looks like a normal error reported correctly -- missing file while examining session AFP/Containers-Benchmarks -- no crash here. After failing in this static phase of examining the session specifications, there is no attempt to continue with what is left over. That would be a bit more complex to do, and such extra complexity then leads to more potential for really bad breakdowns. What is still unclear to me after so many years of testboard is how it actually used in practice. I just do isabelle build -j4 -a -d '$AFP' to see immediately how everything works out. It is also possible to make a quick integrity check via isabelle build -n -a -d '$AFP'. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Java 8 delayed
This is already old news, and in fact a running gag for several years already: Java 8 is again delayed by 6 more months at least, as explained here http://mreinhold.org/blog/hold-the-train -- see also http://openjdk.java.net/projects/jdk8/ for the current milestone situation. Java 8 might (or might not) become available early 2014. Java 6 was officially declared dead in Feb 2013. Java 7 is here right now, but needs to be taken as is. Oracle is mainly working on security problems (for applets or application servers). I will make some more efforts to work around the many GUI and platform problems of Java 7 as we see it today, it is unlikely to change much anytime soon. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Global build failures of the AFP in the testboard
Am 15.05.2013 15:48, schrieb Makarius: What is still unclear to me after so many years of testboard is how it actually used in practice. I just do isabelle build -j4 -a -d '$AFP' to see immediately how everything works out. It is also possible to make a quick integrity check via isabelle build -n -a -d '$AFP'. Actually, isabelle build -j4 -a -d '$AFP' was almost exactly what I did before I ran into this error. Here, I've used the testboard merely as a reference. Another use case is the process making SML/NJ happy. I am aware that it is currently (e.g. in 4517ceb545c1) unhappy about BNFs. But there are also heavier users of the testboard than me. Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Global build failures of the AFP in the testboard
On Wed, 15 May 2013, Dmitriy Traytel wrote: Am 15.05.2013 15:48, schrieb Makarius: What is still unclear to me after so many years of testboard is how it actually used in practice. I just do isabelle build -j4 -a -d '$AFP' to see immediately how everything works out. It is also possible to make a quick integrity check via isabelle build -n -a -d '$AFP'. Actually, isabelle build -j4 -a -d '$AFP' was almost exactly what I did before I ran into this error. Here, I've used the testboard merely as a reference. Another use case is the process making SML/NJ happy. I am aware that it is currently (e.g. in 4517ceb545c1) unhappy about BNFs. I am using the mira results on http://isabelle.in.tum.de/reports/Isabelle myself a lot to navigate quickly to points where Isabelle and AFP diverge. Is that already testboard? I thought that would be a slightly different mode of operation to check quasi-interactively if something is ready for push. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Global build failures of the AFP in the testboard
Am 15.05.2013 16:34, schrieb Makarius: On Wed, 15 May 2013, Dmitriy Traytel wrote: Am 15.05.2013 15:48, schrieb Makarius: What is still unclear to me after so many years of testboard is how it actually used in practice. I just do isabelle build -j4 -a -d '$AFP' to see immediately how everything works out. It is also possible to make a quick integrity check via isabelle build -n -a -d '$AFP'. Actually, isabelle build -j4 -a -d '$AFP' was almost exactly what I did before I ran into this error. Here, I've used the testboard merely as a reference. Another use case is the process making SML/NJ happy. I am aware that it is currently (e.g. in 4517ceb545c1) unhappy about BNFs. I am using the mira results on http://isabelle.in.tum.de/reports/Isabelle myself a lot to navigate quickly to points where Isabelle and AFP diverge. Is that already testboard? I thought that would be a slightly different mode of operation to check quasi-interactively if something is ready for push. Right, I should have referenced reports rather than testboard. From that perspective I use the testboard even less. Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Global build failures of the AFP in the testboard
On 15.05.2013 15:55, Makarius wrote: On Thu, 25 Apr 2013, Dmitriy Traytel wrote: http://isabelle.in.tum.de/testboard/Isabelle/report/2cef0644d3d7416f8d7cea92e24fd694 Side-remark about mira configuration: the log says ML_HOME=/home/polyml/polyml-svn/x86-linux but that SVN version is often fluctuating, depending on current experiments with the SVN, and usually lagging behind. The latest official release version is here: /home/polyml/polyml-5.5.0 or even just what Admin/components/main specifies. For best performance on hardware with many cores, ML options like this usually help: ML_OPTIONS=-H 1000 --gcthreads 4 or ML_OPTIONS=-H 1000 --gcthreads 8 Where are these mira/testboard options anyway? Normally the entry points for anything like that is Admin/ within the Isabelle repository, such as Admin/isatest/. The basic configuration of the Mira system is at ~isatest/testbench/mira/settings/settings.py (for testboard), resp. ~isatest/testbench-main/mira/settings/settings.py (for reports) and includes the configurations from the repositories (e.g. Isabelle:Admin/mira.py or AFP:admin/mira.py). The latter overrides the ML settings. @Alex, Gerwin: Is there any reason remaining why the AFP should not use the default PolyML version? I remember Alex and I dropped a similar override from the Isabelle tests. Caveat: The settings (both global and repository-specific) are only loaded once when the mira daemon is started. If they change it is necessary to restart the daemon. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Global build failures of the AFP in the testboard
On 16.05.2013, at 1:25 AM, Lars Noschinski nosch...@in.tum.de wrote: @Alex, Gerwin: Is there any reason remaining why the AFP should not use the default PolyML version? I remember Alex and I dropped a similar override from the Isabelle tests. Not that I am aware of. The main reason there was an explicit version mention there was to keep track of what exactly was running and where it came from. We have a record of that now with the component system, so that can be dropped. Cheers, Gerwin 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] I don't understand isatest AFP report
On 15.05.2013, at 11:33 PM, Makarius makar...@sketis.net wrote: On Wed, 15 May 2013, Gerwin Klein wrote: What's going on is that the somewhat primitive AFP test doesn't understand the output of isabelle build correctly. It's currently getting its list of sessions by scanning through the output, trying to find messages for failed or successful sessions. This worked reliably for IsaMakefiles, because there was a separate invocation for each session and there was delimiting output before/after each session. The difference here is that make did not crash in its own right, but in exchange had less control over what was run and how it failed. Yes, that's basically why this approach worked back then and I haven't really renovated it for the new setting. Do the AFP test scripts have additional resource limits? It currently doesn't. We could think of wrapping a global ulimit around the test invocation. We're probably better off if I make the AFP test more aware of global JVM crashes and better at interpreting regular output. It's good to try to reduce JVM problems, but the JVM being what it is, they will still happen from time to time. In this instance, there was some kind of JVM problem which then caused the scan on the AFP test side to miss the Container session entirely and the tool therefore concluded that it must have been removed. Basically the Isabelle build executable should follow the usual conventions of return codes: 0: all fine 1: program error, e.g. some sessions failed / remains outdated 2: systemic failure, e.g. some unexpected exception within the JVM I should definitely react better to case 2. Currently this gives just a completely confusing everything removed report. I'll have a look at that over the weekend. Cheers, Gerwin 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
