Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-06-21

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

All times shown according to UTC.

Time Nick Message
00:10 stoopkid joined #isabelle
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/
04:27 keep_learning joined #isabelle
06:35 int-e chindy: that's probably not an Isabelle/IsaFoR problem; error code 137 indicates that the process was killed by SIGKILL.
07:09 int-e chindy: which could be caused by the OOM killer (you can look at dmesg to figure that out)
10:12 silver joined #isabelle
13:55 chindy int-e: dmesg give this https://pastebin.com/h93PPpXU so I guess out of memory was the error... Any ide how to allocate more memory? (the laptop has 12g)
13:56 larsrh chindy: ah okay, possibly my recommendation to get rid of --maxheap was counterproductive :/
13:57 larsrh Poly/ML is quite happy to keep allocating more memory beyond what's available, without running GC
13:57 larsrh paired with the fact that Linux is also happy to assign more memory beyond what's available
13:58 int-e besides that you could try splitting the failing session (see thys/ROOT in the isafor sources) into two, which saves memory by virtue of the maximum sharing pass at the end of each session.
13:58 JCaesar mh, I guess it would be nice if you could deactivate overcommit for certain processes…
13:59 int-e But it's just possible that 12GB is too small for isafor; I believe everyone in the CL group who's seriously working with it has at least 16GB.
14:00 larsrh int-e: I thought that these days there's a checkpoint facility
14:00 larsrh where heap compaction happens during a session
14:00 int-e hmm, can that be done through a plain ROOT file?
14:01 larsrh let me find the thread ...
14:01 int-e (thanks to incremental heap images, splitting sesssions isn't as expensive as it used to be, and it's something I know how to do)
14:01 larsrh * System option "checkpoint" helps to fine-tune the global heap space
14:01 larsrh management of isabelle build. This is relevant for big sessions that may
14:01 larsrh exhaust the small 32-bit address space of the ML process (which is used
14:01 larsrh by default).
14:02 larsrh so possibly just theories [checkpoint]
14:02 larsrh indeed
14:03 int-e ah, you can have several of those  theories [checkpoint] blocks. that looks better indeed.
14:04 int-e (and one should probably only add the [checkpoint] to the second and subsequent blocks)
14:07 int-e it should work in principle; the total heap image size up to the CeTA theory is "only" 4.5GB
14:08 int-e err, CeTA session
14:20 larsrh that is ... a lot
14:20 larsrh on second thought, maybe don't submit that to the AFP :p
14:23 larsrh hmm, I can't actually say what the largest (in terms of heap image) session in the AFP is
14:23 larsrh because we don't build all the images
14:23 larsrh largest I see is Collections with 446 MB
14:31 chindy int-e: yea on my 16g comp it worked without problems.
14:33 int-e larsrh: the AFP selection used in IsaFoR (i.e., that HOL-AFP session) is 1.1GB. Note that this is using the 64bit poly/ML.
16:52 chindy int-e: how do i split the sessions?
16:52 chindy simply putt some of the things in a separate one in the root file ?
17:23 int-e apparently it's enough to put an extra  theories [checkpoint]  (starting a new theories block in the same session)
17:46 int-e hmm, actually it requires finding suitable intermediate theories to add; I was looking at HOL-AFP which includes many theories but most of the other sessions only include a single one.
18:31 chindy int-e: i am not sure if I understood correctly, but i altered the file to this https://pastebin.com/gG4SgBHN and it did not work
18:37 int-e yeah it's not so easy. I'm playing with changes like http://sprunge.us/NCIP ... explicitly mentioning an intermediate theory (or several) and doing a checkpoint after that one (and its dependencies) are complete.
19:50 chindy int-e: still got a out of memory... maybe ill be able to split some more
22:23 stoopkid joined #isabelle

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