Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-04-24

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
01:48 ilbot3 joined #isabelle
01:48 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
08:08 dave24 joined #isabelle
17:34 chindy How do i set isabelle to start in 64 bit mode?
17:38 pruvisto chindy: iirc there were some settings in $ISABELLE_HOME/etc/settings
17:39 pruvisto ML_PLATFORM="$ISABELLE_PLATFORM64" ML_HOME="$ML_HOME/../$ML_PLATFORM"
17:40 pruvisto assuming you're on Linux or Mac
17:40 pruvisto not sure if it works on Windows
18:23 chindy how do increase the memory or max memory ?
18:24 chindy just editing the *.run file to start java with the right params ?
18:33 pruvisto paging larsrh
18:33 pruvisto I think there are some options for the settings file that do this
18:34 pruvisto at some point, it was JEDIT_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"
18:34 pruvisto for the Java memory
18:34 pruvisto but there are also options for the PolyML memory
18:37 int-e there's ML_OPTIONS
18:39 int-e ML_OPTIONS="-H 500 --gcthreads 2" <-- I think that's the minimum heap size in megabytes, for example
18:41 int-e ah, not quite: -H <Initial heap size (MB)> --minheap <Minimum heap size (MB)> --maxheap <Maximum heap size (MB)>
18:44 int-e (to find this information I invoked  ~/.isabelle/contrib/polyml-5.6-1/x86_64-linux/poly --help ... contributions also contain a contrib subdirectory)
18:45 chindy some i just add the line ML_OPTIONS="-H 2000 --miniheap 1000 --maxheap 14000 in ~/.isabelle/Isabelle2016-1/settings ?
18:46 chindy with or without space between H 200 ... ?
18:46 chindy int-e:
18:46 int-e with, but it's not "miniheap"
18:46 int-e (I don't know whether the space makes a difference, but it works with the space)
18:47 chindy what is it instead of miniheap/maxheap ?
18:47 int-e see above? it's min and max not mini and max
18:48 chindy .... whats gcthreads ?
18:48 int-e --gcthreads <Number of threads to use for garbage collection>
18:49 int-e (usually I put the number of physical cores there, as opposed to the number of hyperthreads)
18:50 chindy but running isabelle itself is still Isabell*.run , right ?
18:58 chindy I constantly get "cannot increase stack" or out of memory when trying to build the AFP
18:58 int-e hmm, what's that .run thing... bin/isabelle jedit  seems a better entry point for command line use
19:01 pruvisto chindy: why do you want to build the entire AFP?
19:01 int-e the .run thing also puts the heap images inside the isabelle distribution directory, eww.
19:01 chindy uh... i was simply trying originally i wanted to build Isafor
19:03 int-e chindy: be sure to follow the instructions in isafor's readme (hmm, which somehow fails to mention the COMPATIBILITY file that points to a suitable AFP version)
19:04 int-e pruvisto: Isafor defines a HOL-AFP session that contains the parts of AFP that Isafor actually uses... and yes, building that runs out of memory with the 32 bit version of Isabelle/HOL
19:37 JCaesar joined #isabelle
20:30 chindy int-e: interestingly isabelle env | grep "ML" shows that i still am in 32 bit ...
20:32 int-e chindy: where did you put the settings? they should be in ~/.isabelle/Isabelle2016-1/etc/settings , I'd assume.
20:32 chindy ML_PLATFORM="$ISABELLE_PLATFORM64"
20:32 chindy ML_HOME="$ML_HOME/../$ML_PLATFORM"
20:32 chindy ML_OPTIONS="-H 3000 --gcthreads 6 --minheap 2000 --maxheap 14000"
20:32 chindy those lines
20:33 chindy in ~/.isabelle/Isabelle2016-1/etc/settings
20:33 chindy started isabelle with Isabelle2016-1/bin/isabelle jedit
20:34 int-e I have a similar setup and it says ML_PLATFORM=x86_64-linux in isabelle env
20:35 chindy ML_PLATFORM=x86_64-linux
20:35 chindy ML_SYSTEM_64=false
20:35 chindy the bottom one is the one why i am confused
20:36 int-e oh that's the same here.
20:36 int-e so I guess it doesn't matter.
20:36 chindy interestingly enough... on my laptop it says true :/
20:38 int-e if grep "ML_system_64.*=.*true" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null
20:38 int-e ... huh.
20:41 int-e so apparently one can put  ML_system_64 = "true"  in the preferences file and get a 64 bit ML
20:41 int-e so why doesn't anybody seem to know that
20:47 pruvisto maybe this is new?
20:48 chindy Without sounding like a dick, but is there some "considerable" development in making these things "user" friendly?
20:49 int-e pruvisto: good point, it seems to have been added in Isabelle 2016
20:50 chindy It seems like isabelle made an effort to make things easy, when it comes to dependencies, installation.... but it kinda drops the ball here :/
20:52 pruvisto one reason is that Makarius considers 64 bit mode unnecessary at the moment
20:52 int-e in fact there's an "ML system" panel in the "General" Isabelle plugin settings, and the last item is "ML System 64"
20:52 pruvisto I know that it isn't
20:52 pruvisto ah, good to know!
20:52 int-e s/panel/section/
20:54 int-e Okay, I hope I won't forget about this, it's one less ugly hack to copy from each version to the next one.
20:55 int-e (it may be the last ugly hack actually, hmm. not sure.)
20:57 int-e chindy: thanks. you must have found this option at some time on your laptop :)
20:57 chindy int-e: haha yea... i can envision that. Probably somewhen late at night trying around :P
20:58 ertesx joined #isabelle

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary