Re: [isabelle-dev] Poly/ML 5.7
On 15/05/17 14:33, Makarius wrote: > On 15/05/17 12:14, Makarius wrote: >> Some results can be seen here: >> >> http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux/index.html >> http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux_2_threads/index.html >> >> The test hardware is similar or actually the same as "Linux A", but this >> needs to be investigated further. It is also important to compare >> timings for the *same* Isabelle versions, but the Poly_ML_5.7_Linux task >> is still busy digging into older history. > > Maybe I also manage to get ml_statistics into the charts soon. Then we > can look at heap, task, thread details etc. I have now done that in various changes leading to Isabelle/65e132abab1e. Moreover, I have made a fresh start for "Poly/ML 5.7" measurements, with precisely the same parameters as "Linux A" (Isabelle/d547173212d2). This explains why there are only a few data points for Poly/ML 5.7, but the situation will improve every day. This means we can now compare the measurements and analyze the (slight) performance losses of Poly/ML 5.7. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML 5.7
On 15/05/17 14:24, Makarius wrote: > On 15/05/17 12:29, Lawrence Paulson wrote: >> Version 5.7 doesn’t even build on my main workstation, though it works >> on my MacBook Pro running broadly similar software. No idea what is >> going on here, but I’m not happy about it. > > There are already some mail threads on the Poly/ML list, where various > people have helped out to consolidate the situation. > > Anyone who is proficient with C/C++ and various platforms (Linux, > Windows, Mac OS X varieties) is invited to join there -- not just now, > but also in the longer term. Some of this activity is actually on the HOL and ProofPower mailing list, apart from the Isabelle side here. We should make sure that everything relevant to Poly/ML also goes over its official mailing list: http://lists.inf.ed.ac.uk/mailman/listinfo/polyml Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML 5.7
On 15/05/17 12:14, Makarius wrote: > Some results can be seen here: > > http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux/index.html > http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux_2_threads/index.html > > The test hardware is similar or actually the same as "Linux A", but this > needs to be investigated further. It is also important to compare > timings for the *same* Isabelle versions, but the Poly_ML_5.7_Linux task > is still busy digging into older history. I have now changed that here: changeset: 65840:8d7b2ac9a245 tag: tip user:wenzelm date:Mon May 15 14:27:14 2017 +0200 files: src/Pure/Admin/isabelle_cronjob.scala description: history parameters like "Linux A", for more comparable results; Maybe I also manage to get ml_statistics into the charts soon. Then we can look at heap, task, thread details etc. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML 5.7
On 15/05/17 12:29, Lawrence Paulson wrote: > Version 5.7 doesn’t even build on my main workstation, though it works > on my MacBook Pro running broadly similar software. No idea what is > going on here, but I’m not happy about it. There are already some mail threads on the Poly/ML list, where various people have helped out to consolidate the situation. Anyone who is proficient with C/C++ and various platforms (Linux, Windows, Mac OS X varieties) is invited to join there -- not just now, but also in the longer term. Note that for Isabelle, the build process works via "isabelle build_polyml" from recent repository versions, see also http://isabelle.in.tum.de/repos/isabelle/annotate/8007f10195af/src/Pure/Admin/build_polyml.scala Going through Isabelle/Scala has the slight disadvantage of obscuring the description of the build process, but it is more robust and repeatable on all these platform variations. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML 5.7
Version 5.7 doesn’t even build on my main workstation, though it works on my MacBook Pro running broadly similar software. No idea what is going on here, but I’m not happy about it. Larry > On 15 May 2017, at 11:14, Makarius wrote: > > David Matthews has made the Poly/ML 5.7 release snapshot some weeks ago > (see https://github.com/polyml/polyml/releases/tag/v5.7), but announced > it only last week. > > I have wrapped that up as a component in Isabelle/d3c5898f1a5e, but that > is only for testing, not for production use. Some results can be seen here: > > http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux/index.html > http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux_2_threads/index.html > > The test hardware is similar or actually the same as "Linux A", but this > needs to be investigated further. It is also important to compare > timings for the *same* Isabelle versions, but the Poly_ML_5.7_Linux task > is still busy digging into older history. > > > After the substantial changes of the code generator and representation > of ML values in memory, there are various open questions concerning > performance and robustness of Isabelle applications. > > This means, we need to skip the Poly/ML 5.7 release and stay on the last > Poly/ML 5.6 until the situation becomes more clear. > > > This is how to use the polyml-5.7 component locally: > > $ edit $ISABELLE_HOME_USER/etc/settings > > init_component "$HOME/.isabelle/contrib/polyml-5.7" > > $ isabelle components -a > > > 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