Re: [isabelle-dev] Global build failures of the AFP in the testboard
On 17.05.2013 17:24, Makarius wrote: On Thu, 16 May 2013, Lars Noschinski wrote: - ML_PLATFORM=x86-linux ML_HOME=/home/polyml/polyml-svn/x86-linux ML_SYSTEM=polyml-5.5.0 ML_OPTIONS=-H 1000 ISABELLE_BUILD_OPTIONS=threads=4 parallel_proofs=2 - and I would simplify this to: - ML_OPTIONS=-H 1000 ISABELLE_BUILD_OPTIONS=threads=4 parallel_proofs=2 - [...] Alternatively, you could just make a general default of --gcthreads 4 for all machines as decent approximation. This is what I did now, see revision 9ce4a76615bb9. ___ 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, 16 May 2013, Lars Noschinski wrote: - ML_PLATFORM=x86-linux ML_HOME=/home/polyml/polyml-svn/x86-linux ML_SYSTEM=polyml-5.5.0 ML_OPTIONS=-H 1000 ISABELLE_BUILD_OPTIONS=threads=4 parallel_proofs=2 - and I would simplify this to: - ML_OPTIONS=-H 1000 ISABELLE_BUILD_OPTIONS=threads=4 parallel_proofs=2 - Since AFP tests run both on lxbroy10 (for the testboard) and lxbroy8 (for main); should I add a special case for lxbroy10 with --gcthreads 8? lxbroy10 has 4 CPU modules with 6 cores each, with relatively low memory bandwidth between them. So if you want to go into such details, you could say --gcthreads 6. Actual phyisical measurements would be required for more than just rules of thumb. Alternatively, you could just make a general default of --gcthreads 4 for all machines as decent approximation. 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 Wed, 15 May 2013, Gerwin Klein wrote: 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. Since it is polyml-svn and x86_64, too, I guess it is just historic. At some point we've had problems getting AFP through with some polyml-5.4.x version, and that was the result of strechting as far as possible. Now it should all work just with the component defaults. 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 16.05.2013 00:43, Gerwin Klein wrote: On 16.05.2013, at 1:25 AM, Lars Noschinskinosch...@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. Ok. Currently the options are - ML_PLATFORM=x86-linux ML_HOME=/home/polyml/polyml-svn/x86-linux ML_SYSTEM=polyml-5.5.0 ML_OPTIONS=-H 1000 ISABELLE_BUILD_OPTIONS=threads=4 parallel_proofs=2 - and I would simplify this to: - ML_OPTIONS=-H 1000 ISABELLE_BUILD_OPTIONS=threads=4 parallel_proofs=2 - Since AFP tests run both on lxbroy10 (for the testboard) and lxbroy8 (for main); should I add a special case for lxbroy10 with --gcthreads 8? -- 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 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
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
[isabelle-dev] Global build failures of the AFP in the testboard
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. For now I commented the Containers-Benchmarks session out (AFP/ 99c45df7f5af) - now the test will reveal further outdated constructs in Containers (mostly related to Florian's reform of the code generation for numerals). The question remains, whether it is possible for the build tool to proceed with other sessions if the imports of a single session are faulty. Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
