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
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
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?
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.
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
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
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
