Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-12-02

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

All times shown according to UTC.

Time Nick Message
02:47 ilbot3 joined #isabelle
02:47 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/
11:00 silver joined #isabelle
15:25 JCaesar_ joined #isabelle
16:52 JCaesar_ say, is it possible that sledgehammer writes stuff to disk? Like, serveral hundred MBs?
17:05 ThreeOfEight JCaesar: I /know/ that it writes to disc if you e.g. have spying turned on
17:05 ThreeOfEight I wouldn't be surprised if it also wrote to disc on default settings for some reasons
17:05 ThreeOfEight e.g. to communicate with the solvers
17:05 ThreeOfEight quite likely actually
17:05 ThreeOfEight several hundred MBs sounds odd, but I wouldn't rule it out
17:06 ThreeOfEight What gave you that idea?
17:06 JCaesar seeing my free disk space drop by 300 mb, and raise again when sledgehammer timed out.
17:23 ThreeOfEight You can always ask on the mailing list
20:07 kyagrd joined #isabelle
21:02 larsrh or strace it
21:31 ThreeOfEight larsrh: I considered suggesting that, but then thought that that will probably also show a lot of noise
21:31 ThreeOfEight (also he probably thought about it himself already)
22:38 larsrh you can filter strace output though

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