Re: [isabelle-dev] Sum of Squares server down?
On Thu, 11 Sep 2014, Lawrence Paulson wrote: I have installed a copy of the software locally. Would be worth making this a component? This canonical question has come up each time, after someone spent significant time with the NEOS/CSDP server. I have started to experiment myself with the binary downloads from https://projects.coin-or.org/Csdp So far it works fine, but I need to do more multi-platform tests. Despite the warnings on the download site about unoptimized executables, they are *much* faster than the server. So what is the purpose of the server anyway? It did not only waste our time in the maintenance, but also time of potential users. So the NEOS/CSDP server setup looks like a canonical candidate for deletion. That would also allow to remove Python from the Windows/Cygwin app bundle and save many MBs of disk space. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sum of Squares server down?
On 22/09/2014 16:52, Makarius wrote: On Thu, 11 Sep 2014, Lawrence Paulson wrote: I have installed a copy of the software locally. Would be worth making this a component? This canonical question has come up each time, after someone spent significant time with the NEOS/CSDP server. I have started to experiment myself with the binary downloads from https://projects.coin-or.org/Csdp So far it works fine, but I need to do more multi-platform tests. Despite the warnings on the download site about unoptimized executables, they are *much* faster than the server. So what is the purpose of the server anyway? To avoid having to the install binaries by hand. Tobias It did not only waste our time in the maintenance, but also time of potential users. So the NEOS/CSDP server setup looks like a canonical candidate for deletion. That would also allow to remove Python from the Windows/Cygwin app bundle and save many MBs of disk space. 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] Sum of Squares server down?
It is also my experience that the server is extremely slow. Larry On 22 Sep 2014, at 15:52, Makarius makar...@sketis.net wrote: On Thu, 11 Sep 2014, Lawrence Paulson wrote: I have installed a copy of the software locally. Would be worth making this a component? This canonical question has come up each time, after someone spent significant time with the NEOS/CSDP server. I have started to experiment myself with the binary downloads from https://projects.coin-or.org/Csdp So far it works fine, but I need to do more multi-platform tests. Despite the warnings on the download site about unoptimized executables, they are *much* faster than the server. So what is the purpose of the server anyway? It did not only waste our time in the maintenance, but also time of potential users. So the NEOS/CSDP server setup looks like a canonical candidate for deletion. That would also allow to remove Python from the Windows/Cygwin app bundle and save many MBs of disk space. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sum of Squares server down?
On 22/09/2014 17:55, Lawrence Paulson wrote: It is also my experience that the server is extremely slow. It's a fact. Making it a component is clearly the right thing to do. Tobias Larry On 22 Sep 2014, at 15:52, Makarius makar...@sketis.net wrote: On Thu, 11 Sep 2014, Lawrence Paulson wrote: I have installed a copy of the software locally. Would be worth making this a component? This canonical question has come up each time, after someone spent significant time with the NEOS/CSDP server. I have started to experiment myself with the binary downloads from https://projects.coin-or.org/Csdp So far it works fine, but I need to do more multi-platform tests. Despite the warnings on the download site about unoptimized executables, they are *much* faster than the server. So what is the purpose of the server anyway? It did not only waste our time in the maintenance, but also time of potential users. So the NEOS/CSDP server setup looks like a canonical candidate for deletion. That would also allow to remove Python from the Windows/Cygwin app bundle and save many MBs of disk space. 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] Sum of Squares server down?
On Mon, 22 Sep 2014, Tobias Nipkow wrote: On 22/09/2014 16:52, Makarius wrote: On Thu, 11 Sep 2014, Lawrence Paulson wrote: I have installed a copy of the software locally. Would be worth making this a component? This canonical question has come up each time, after someone spent significant time with the NEOS/CSDP server. I have started to experiment myself with the binary downloads from https://projects.coin-or.org/Csdp So far it works fine, but I need to do more multi-platform tests. To avoid having to the install binaries by hand. That *was* the purpose of the server when it was done the first time many years ago. Now we have the well-established concept of Isabelle components to avoid the IKEA-effect for users, to assemble things manually from parts. I have the component already -- it was much easier to make than the cumulative mail traffic about this topic. I merely need to test it a bit more, before it becomes a standard component for everybody. So far the conclusion on this thread: the NEOS server has no purpose anymore and can be removed. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sum of Squares server down?
On Mon, 22 Sep 2014, Makarius wrote: I have the component already -- it was much easier to make than the cumulative mail traffic about this topic. I merely need to test it a bit more, before it becomes a standard component for everybody. See also Isabelle/00bf84d3f526. So far the conclusion on this thread: the NEOS server has no purpose anymore and can be removed. As usual, I leave a bit of time to come up with reasons why the server still has a purpose, before removing it. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sum of Squares server down?
Just for the record, the server was not down. This may have merely been a timeout problem. Tobias On 11/09/2014 14:05, Jasmin Christian Blanchette wrote: Hi all, It appears that the Sum of Squares server is down. This makes the build of the HOL-Library session diverge, at least on my machine, when ISABELLE_FULL_TESTS is enabled. In addition, it appears to be at the source of the Isatest failures on mac-poly-M4 and mac-poly-M8. What's the procedure in such cases? Also, would there be a way to change this code so that it skips the tests when the server is not available? I spent literally hours trying to find out why isabelle build -b HOL-Library was getting nowhere today for me (my first suspicions were Poly/ML's memory and thread handling). Thanks, Jasmin ___ 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] Sum of Squares server down?
On 11/09/2014 14:05, Jasmin Christian Blanchette wrote: Hi all, It appears that the Sum of Squares server is down. This makes the build of the HOL-Library session diverge, at least on my machine, when ISABELLE_FULL_TESTS is enabled. In addition, it appears to be at the source of the Isatest failures on mac-poly-M4 and mac-poly-M8. What's the procedure in such cases? I will contact the service team as I have done once before. Thanks Tobias Also, would there be a way to change this code so that it skips the tests when the server is not available? I spent literally hours trying to find out why isabelle build -b HOL-Library was getting nowhere today for me (my first suspicions were Poly/ML's memory and thread handling). Thanks, Jasmin ___ 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] Sum of Squares server down?
I have installed a copy of the software locally. Would be worth making this a component? --lcp On 11 Sep 2014, at 13:07, Tobias Nipkow nip...@in.tum.de wrote: On 11/09/2014 14:05, Jasmin Christian Blanchette wrote: Hi all, It appears that the Sum of Squares server is down. This makes the build of the HOL-Library session diverge, at least on my machine, when ISABELLE_FULL_TESTS is enabled. In addition, it appears to be at the source of the Isatest failures on mac-poly-M4 and mac-poly-M8. What's the procedure in such cases? I will contact the service team as I have done once before. Thanks Tobias Also, would there be a way to change this code so that it skips the tests when the server is not available? I spent literally hours trying to find out why isabelle build -b HOL-Library was getting nowhere today for me (my first suspicions were Poly/ML's memory and thread handling). Thanks, Jasmin ___ 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 mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
