Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-06-20

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

All times shown according to UTC.

Time Nick Message
00:13 int-e_ joined #isabelle
00:13 ski_ joined #isabelle
00:14 JCaesar_ joined #isabelle
00:16 larsrh joined #isabelle
00:17 ezyang joined #isabelle
00:18 ertes joined #isabelle
00:20 lispy joined #isabelle
00:21 larsrh joined #isabelle
00:32 mal`` 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/
02:50 renopt joined #isabelle
08:05 wagle joined #isabelle
10:25 ammbauer so I'm working with monads right now and is there a way to tell the isabelle pretty printer to put a newline after >>=?
10:25 pruvisto Not that I know of
10:26 pruvisto you can introduce new names for sub-parts with "define" to make things more legible
10:26 pruvisto I usually just pretty print the stuff myself in a text editor
10:26 pruvisto or rewrite the entire thing in "do" notation
11:15 silver joined #isabelle
12:32 ammbauer joined #isabelle
12:59 silver joined #isabelle
13:27 JCaesar ammbauer: Hm, if you'd define a new abbreviation for >>=, you might be able to mess with the pretty printing. for latex, sure, you can insert newlines. but I don't think you can do that with Isabelle/jedit output. Maybe you can tell it that something is a good place to break.
13:54 chindy when running: "isabelle build -b HOL-AFP" I get the error "Warning - Unable to increase stack - interrupting thread
13:54 chindy HOL-AFP FAILED..." Anyone know why how to fix this?
13:59 pruvisto chindy: errr… try the 64 Bit version, perhaps?
14:06 chindy pruvisto: I know i asked this before and I am under the impression that I am on the 64 bit version. But how can I verify this and/or change this ?
14:11 larsrh $ ps aux | grep poly
14:12 larsrh it's either /polyml-5.6-1/x86-linux/poly or /polyml-5.6-1/x86-64-linux/poly
14:14 chindy as expected its the latter
14:14 chindy larsrh: ^
14:14 chindy so i guess it seems  as if i get the erorr although im on 64 bit
14:14 chindy I have these options: Might this be the rror ? ML_OPTIONS="-H 4000 --gcthreads 12 --minheap 2000 --maxheap 12000"
14:24 larsrh not sure what the units for minheap and maxheap are
14:24 larsrh but you can just remove minheap and maxheap
14:40 chindy larsrh: I got the same error without the parameters
14:56 dmiles joined #isabelle
15:10 int-e I have not seen that before... could it be the C stack? (what does  ulimit -s  say?)
15:14 int-e (it does seem rather unlikely though)
15:21 int-e in fact, that can't be the reason
15:34 int-e well, Timing HOL-AFP (12 threads, 498.953s elapsed time, 3872.432s cpu time, 452.288s GC time, factor 7.76)
15:36 int-e this is Isabelle-2016-1, afp-2016-1 commit 3e4b1a448754 (but afp-2016-12-17 should not be different, I think), and isafor commit 27426b5387d7
15:59 chindy ulimit -s says 8192
16:00 int-e yeah but it's almost certainly completely irrelevant; the "stack" here is a memory area managed by the poly/ml runtime
16:20 chindy int-e: well i did download the AFP and Isafor today... so it should be the newest commit
16:20 chindy also this is the whole error message : https://pastebin.com/MD9q6fei
16:52 int-e chindy: why is it using afp-devel?
16:53 int-e https://bitbucket.org/isa-afp/afp-devel is for the development version of Isabelle. https://bitbucket.org/isa-afp/afp-2016-1 is for Isabelle-2016-1
16:57 int-e (fortunately, Makarius is not here to admonish me for speaking of "the" development version of Isabelle)
17:47 ertes joined #isabelle
17:52 Asdfg joined #isabelle
18:10 ertes left #isabelle
18:30 larsrh int-e: everything in here is logged though :p
22:14 JCaesar_ joined #isabelle
22:14 lispy joined #isabelle
22:14 ski_ joined #isabelle
22:15 ezyang joined #isabelle
22:16 ezyang joined #isabelle
22:49 chindy int-e: ahh... yea that sealed the deal.. is there a similar thing for IsaFor/CeTA?
23:21 chindy since i have following error when "make" in IsaFoR
23:21 chindy https://pastebin.com/xs97c70r

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