[isabelle-dev] Cannot execute Poly/ML in 32bit mode
Hi list, When I start Isabelle, I get the following warning message on the console: ### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++) ### Using bulky 64bit version of Poly/ML instead Is it a problem to use the bulky 64bit version? -- Peter ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Cannot execute Poly/ML in 32bit mode
I think the main (and only) problem is that it uses significantly more memory. On 28/05/15 11:21, Peter Lammich wrote: Hi list, When I start Isabelle, I get the following warning message on the console: ### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++) ### Using bulky 64bit version of Poly/ML instead Is it a problem to use the bulky 64bit version? -- Peter ___ 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] Cannot execute Poly/ML in 32bit mode
On Thu, 28 May 2015, Peter Lammich wrote: When I start Isabelle, I get the following warning message on the console: ### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++) ### Using bulky 64bit version of Poly/ML instead Is it a problem to use the bulky 64bit version? Usually none, apart from wasting about a factor 2 of ML heap space. On http://isabelle.in.tum.de/installation.html there is snippet of explanation: 32-bit C/C++ standard libraries on 64-bit Linux (optional, for improved performance of Poly/ML) It depends on the Linux distribution which packages provide the 32-bit C/C++ standard libraries mentioned above. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Infinite loops with output
On Thu, 28 May 2015, Aymeric Bouzy wrote: I'm doing some development in SML for Isabelle, and sometimes I accidentally write an infinite loop. To try to determine where the infinite loops comes from, I often print some output, as this is the recommanded way to debug SML code I believe. Using Isabelle/ML or SML inside Isabelle is a regular isabelle-users activity, so this is off-topic on this mailing list. The problem is that Isabelle/jEdit freezes as soon as an infinite output is printed, as proven by the included file. If you use tracing instead of writeln the front-end gets a chance to survive this massive DNS attack. There is some kind of dialog at the bottom of the output window. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Infinite loops with output
Hello, I'm doing some development in SML for Isabelle, and sometimes I accidentally write an infinite loop. To try to determine where the infinite loops comes from, I often print some output, as this is the recommanded way to debug SML code I believe. The problem is that Isabelle/jEdit freezes as soon as an infinite output is printed, as proven by the included file. Development.thy Description: Binary data I haven't found a way yet to interrupt the execution of the file, so does this feature exist? and if no, could it be considered adding it? Thanks, Aymeric Bouzy___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Infinite loops with output
On 28 May 2015, at 15:38, Makarius makar...@sketis.net wrote: Using Isabelle/ML or SML inside Isabelle is a regular isabelle-users activity, so this is off-topic on this mailing list. Sorry about that, you are right. If you use tracing instead of writeln the front-end gets a chance to survive this massive DNS attack. There is some kind of dialog at the bottom of the output window. This was exactly what I was looking for ! Thanks a lot. Maybe it could be considered mentioning it in The Isabelle Cookbook in section 2.2 ? Aymeric ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Infinite loops with output
On Thu, 28 May 2015, Aymeric Bouzy wrote: Maybe it could be considered mentioning it in The Isabelle Cookbook in section 2.2 ? The Cookbook is somewhat outdated and not very precise, sometimes wrong. The official Isabelle/ML documentation is the implementation manual that is part of the standard release. It explains tracing in section 0.4 Message output channels. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
