00:02:12 -!- augur has quit (Remote host closed the connection).
00:06:06 -!- madbr has joined.
00:07:37 -!- ^v has quit (Read error: Connection reset by peer).
00:08:25 -!- ^v has joined.
00:19:38 -!- ^v has quit (Read error: Connection reset by peer).
00:20:03 -!- ^v has joined.
00:20:46 -!- atslash has quit (Quit: This computer has gone to sleep).
00:29:34 -!- oerjan has quit (Quit: Nite).
00:34:02 -!- shikhin has joined.
00:37:38 <kmc> every world we reach is fungot
00:37:38 <fungot> kmc: ( i'm saying this as a cgi. use mod_lisp.) and can be left off.
00:37:48 <kmc> fungot: are you a full-time internet?
00:37:48 <fungot> kmc: that's a macro. i thought that was fnord
00:42:06 <shachaf> p. sure fungot is computer-generated imagery
00:42:07 <fungot> shachaf: what use would a variable?
00:42:12 -!- Tod-Autojoined has joined.
00:45:38 -!- TodPunk has quit (Ping timeout: 240 seconds).
00:50:58 -!- ineiros_ has quit (Ping timeout: 240 seconds).
00:51:04 -!- douglass_ has quit (Ping timeout: 240 seconds).
00:52:55 -!- boily has joined.
00:52:56 -!- douglass1 has joined.
00:52:56 -!- ineiros has joined.
00:52:57 -!- boily has quit (Client Quit).
01:01:49 -!- Tod-Autojoined has changed nick to TodPunk.
01:12:31 -!- edwardk has quit (Read error: Connection reset by peer).
01:19:29 -!- shikhout has joined.
01:19:45 -!- Phantom_Hoover has joined.
01:23:05 -!- shikhin has quit (Ping timeout: 264 seconds).
01:31:16 -!- augur has joined.
01:31:29 -!- shikhout has quit (Remote host closed the connection).
01:47:34 -!- Tod-Autojoined has joined.
01:48:07 -!- nycs has joined.
01:51:19 -!- jconn has quit (Ping timeout: 240 seconds).
01:51:20 -!- TodPunk has quit (Ping timeout: 240 seconds).
01:51:21 -!- fowl has quit (Ping timeout: 240 seconds).
01:52:30 -!- Taneb has quit (Ping timeout: 276 seconds).
01:52:33 -!- `^_^v has quit (Ping timeout: 276 seconds).
01:55:04 -!- Zerker has joined.
01:55:57 -!- Taneb has joined.
02:04:35 -!- fowl has joined.
02:05:27 -!- Tod-Autojoined has changed nick to TodPunk.
02:06:53 -!- FreeFull has quit.
02:09:42 -!- Zerker has quit (Quit: Colloquy for iPad - Timeout (10 minutes)).
02:12:24 -!- ^v has quit (Quit: http://i.imgur.com/Akc6r.gif).
02:14:08 -!- Ghoul_ has quit (Quit: Connection closed for inactivity).
02:36:00 -!- Phantom_Hoover has quit (Remote host closed the connection).
02:48:42 -!- kwertii has joined.
02:49:28 -!- kwertii has quit (Client Quit).
03:09:35 -!- tertu has quit (Disconnected by services).
03:09:35 -!- ter2 has joined.
03:15:17 -!- hk3380 has quit (Ping timeout: 264 seconds).
03:28:34 -!- copumpkin has changed nick to ubiquipumpkin.
03:32:01 -!- Sorella has quit (Quit: It is tiem!).
03:39:58 -!- conehead has quit (Quit: Computer has gone to sleep).
03:48:08 <kmc> http://dumb.domains/
03:49:41 <Bike> thank you for making this all possible, ICANN
03:52:57 <ubiquipumpkin> is there a list of all the crazy TLDs that have appeared?
03:53:16 <ubiquipumpkin> http://en.wikipedia.org/wiki/List_of_Internet_top-level_domains
03:54:25 <kmc> hark, a pumpkin
03:57:39 <shachaf> ubiquipumpkin: surely you could make it one
03:57:57 <ubiquipumpkin> I guess the requirements are significantly lower :P
03:58:48 <shachaf> there might not be .pumpkin but at least there's .bike
03:59:48 <kmc> pumpkin.co
04:00:08 <ubiquipumpkin> kmc: omg if I were publishing jvm packages I'd be all set
04:01:47 <shachaf> Entity: those who like the color red
04:01:49 -!- ubiquipumpkin has changed nick to copumpkin.
04:02:00 <shachaf> it's a high bar, copumpkin
04:03:16 -!- tertu has joined.
04:04:56 <kmc> upholste.red
04:05:50 -!- ter2 has quit (Ping timeout: 265 seconds).
04:06:29 -!- hk3380 has joined.
04:10:31 -!- EgoBot has quit (Remote host closed the connection).
04:11:27 -!- EgoBot has joined.
04:12:19 -!- FireFly has quit (Ping timeout: 240 seconds).
04:13:29 -!- tromp has quit (Ping timeout: 252 seconds).
04:14:14 -!- tromp has joined.
04:14:44 -!- Gregor has quit (Ping timeout: 240 seconds).
04:16:00 -!- EgoBot has quit (Ping timeout: 265 seconds).
04:18:07 -!- FireFly has joined.
04:18:55 -!- Gregor has joined.
04:31:00 -!- Sprocklem has joined.
04:43:44 -!- hk3380 has quit (Ping timeout: 252 seconds).
04:49:59 -!- Vorpal has quit (Quit: ZNC - http://znc.sourceforge.net).
04:59:54 -!- ^v has joined.
05:04:31 -!- Slereah has joined.
05:05:11 -!- Slereah_ has quit (Ping timeout: 252 seconds).
05:08:07 -!- password2 has joined.
05:34:58 -!- Sprocklem has quit (Ping timeout: 245 seconds).
05:45:52 -!- edwardk has joined.
05:48:40 -!- madbr has quit (Quit: Rouringu de hajikunda!).
05:51:07 -!- tromp has quit (Ping timeout: 252 seconds).
05:59:04 -!- password2 has quit (Ping timeout: 276 seconds).
06:02:54 <mroman_> FireFly: You can check for whether a cell belongs to you or the enemy
06:03:23 <mroman_> You can scan the memory and bomb every location not belonging to you
06:07:22 -!- jconn has joined.
06:09:57 <mroman_> and I see the 'C' instruction isn't documented
06:10:08 <mroman_> It was intented to allow one to copy itself
06:22:46 -!- ^v has quit (Quit: http://i.imgur.com/Akc6r.gif).
06:36:53 -!- augur has quit (Ping timeout: 258 seconds).
06:52:14 -!- conehead has joined.
07:09:00 -!- augur has joined.
07:12:43 -!- edwardk has quit (Ping timeout: 240 seconds).
07:12:45 <shachaf> oerjan: what's with the weird bolding in https://en.wikipedia.org/wiki/Booth_encoding
07:13:14 <shachaf> looks like it took three edits to mess it up
07:23:11 -!- MindlessDrone has joined.
07:29:10 -!- slereah_ has joined.
07:29:17 <slereah_> Hello is this where we learn about the magic
07:34:48 -!- KingOfKarlsruhe has joined.
08:06:54 -!- edwardk has joined.
08:17:01 <augur> https://www.google.com/patents/US20030083544?dq=finding+love&hl=en&sa=X&ei=VqxuU52KKKLjsASNloCwBA&ved=0CDUQ6AEwAA
08:27:05 -!- Patashu has joined.
08:39:45 -!- oerjan has joined.
08:42:18 -!- Bike has quit (Ping timeout: 265 seconds).
08:51:23 -!- drdanmaku has quit (Quit: Connection closed for inactivity).
08:51:48 -!- atslash has joined.
09:08:34 -!- TodPunk has quit (Ping timeout: 240 seconds).
09:15:39 <oerjan> shachaf: someone was too bold while editing hth
09:46:12 -!- shikhin has joined.
09:59:37 <mroman_> if spammers were to pay 1 cent to charity for every spam mail they send
09:59:41 <mroman_> what a world we would live in...
10:01:26 <mroman_> so far 10/10 agreed on re-return EOF and unbounded memory to the right
10:04:04 -!- mhi^ has joined.
10:06:43 <slereah_> So many are from poor countries
10:07:02 <slereah_> http://en.wikipedia.org/wiki/Spammer#Geographical_origins
10:20:37 -!- shikhin has quit (Ping timeout: 252 seconds).
10:24:02 -!- hk3380 has joined.
10:28:51 -!- KingOfKarlsruhe has quit (Read error: Connection timed out).
10:36:14 -!- edwardk_ has joined.
10:37:55 -!- edwardk has quit (Ping timeout: 276 seconds).
10:51:47 -!- Phantom_Hoover has joined.
10:56:11 -!- hk3380 has quit (Ping timeout: 255 seconds).
11:12:40 -!- Patashu has quit (Disconnected by services).
11:12:40 -!- Patashu_ has joined.
11:36:59 -!- TodPunk has joined.
11:39:32 -!- TodPunk has quit (Read error: No route to host).
11:39:39 -!- TodPunk has joined.
11:42:09 -!- Tod-Autojoined has joined.
11:44:52 -!- TodPunk has quit (Ping timeout: 276 seconds).
11:45:05 -!- edwardk_ has quit (Ping timeout: 258 seconds).
11:47:27 -!- shikhin has joined.
11:47:35 -!- Sgeo has quit (Read error: Connection reset by peer).
11:51:48 -!- yorick has joined.
11:52:07 -!- shikhin has quit (Ping timeout: 250 seconds).
11:59:41 -!- edwardk has joined.
12:08:53 -!- conehead has quit (Quit: Computer has gone to sleep).
12:15:19 -!- nucular has joined.
12:15:19 -!- nucular has quit (Changing host).
12:15:19 -!- nucular has joined.
12:21:37 -!- mhi^ has quit (Quit: Lost terminal).
12:23:39 -!- mhi^ has joined.
12:23:41 -!- mhi^ has quit (Changing host).
12:23:42 -!- mhi^ has joined.
12:46:23 -!- Sorella has joined.
12:49:29 -!- edwardk has quit (Ping timeout: 264 seconds).
12:50:34 -!- tromp has joined.
13:21:11 -!- mhi^ has quit (Quit: Lost terminal).
13:44:22 -!- nycs has changed nick to `^_^v.
13:44:23 -!- Patashu_ has quit (Ping timeout: 265 seconds).
14:00:03 -!- Phantom__Hoover has joined.
14:00:54 -!- Phantom_Hoover has quit (Ping timeout: 240 seconds).
14:17:16 -!- hk3380 has joined.
14:17:32 -!- shikhin has joined.
14:22:25 -!- conehead has joined.
14:29:14 -!- oerjan has quit (Quit: leaving).
14:29:19 -!- password2 has joined.
14:30:18 -!- g2` has joined.
14:30:44 -!- g2` has left.
14:41:58 -!- password2 has quit (Read error: Connection reset by peer).
14:47:29 -!- Sprocklem has joined.
14:55:09 -!- adu has joined.
15:01:29 -!- slereah_ has quit (Ping timeout: 264 seconds).
15:02:23 -!- slereah_ has joined.
15:04:01 -!- nooodl has joined.
15:04:19 -!- mhi^ has joined.
15:07:36 -!- MindlessDrone has quit (Read error: Connection reset by peer).
15:10:35 -!- FreeFull has joined.
15:17:50 -!- nucular has quit (Ping timeout: 258 seconds).
15:22:30 -!- nucular has joined.
15:27:54 -!- ^v has joined.
15:28:52 -!- ^v has quit (Client Quit).
15:37:19 <shachaf> oerjan: thx for fixing tdh
15:40:33 <tromp_> exercise: write non-recursive factorial for Church numerals
15:41:53 <shachaf> exercise: write non-recursive ackermann function for Chuch numerals
15:42:29 <tromp_> you sure that's possible?
15:43:04 <shachaf> it's possible for it to be an exercise
15:43:06 <tromp_> at least factorial is possible
15:44:00 <int-e> the ackermann thing is instructive.
15:44:37 <int-e> I have a typographical hint: instead of ack(n,m), write ack_n(m).
15:45:15 <Taneb> There's a slightly (very) cheaty way of doing this...
15:46:03 <tromp_> int-e: good point. now it looks not only possible, but straightforward:)
15:51:37 <tromp_> my best factorial is 78 bits
15:54:05 <shachaf> the single-argument ackermann function is usually \n -> ack(n,n)
15:57:55 -!- tertu has quit (Ping timeout: 240 seconds).
15:58:28 <int-e> so 54 bits for \n m -> Ack(n,m); 58 for \n -> Ack(n,n)
15:59:03 -!- copumpkin has quit (Remote host closed the connection).
15:59:38 <int-e> binary lambda calculus
16:00:42 -!- slereah_ has quit (Quit: Leaving).
16:02:19 <tromp_> hmm, i even have something about goodstein and ackerman on my home page at http://homepages.cwi.nl/~tromp/pearls.html#goodstein
16:05:05 -!- Sprocklem has quit (Ping timeout: 264 seconds).
16:05:14 -!- MindlessDrone has joined.
16:11:22 <tromp_> 47 bits for the Ackerman-like g i define there
16:12:04 <shachaf> is all this still non-recursive
16:12:54 <tromp_> but i doubt if the goodstein function can avoid recursion
16:16:43 -!- Sprocklem has joined.
16:17:23 <tromp_> mine is based on F cont succn facn = cont (succ succn) (succn * facn)
16:17:30 <tromp_> what's yours based on?
16:19:44 <int-e> it's \n\f. n (\f\n. n (f (succ n))) (\_. f) 1 ... it operates on f^k, where k is 1, n, n*(n-1), n*(n-1)*(n-2) etc.
16:21:29 -!- Bike has joined.
16:21:36 <Jafet> At this point you might as well brute force it
16:22:38 -!- Sprocklem has quit (Ping timeout: 240 seconds).
16:25:14 <Jafet> <a href="http://java.sun.com/">C++</a> good link
16:25:58 -!- adu has quit (Ping timeout: 240 seconds).
16:34:19 <FireFly> "Writing a BLC8 interpreter in Brainfuck, which would provide a matching upper bound in the other direction, is left as an exercise for die-hard Brainfuck programmers." ince
16:35:14 <tromp_> i dont expect anyone to ever take up that challenge:)
16:36:03 <tromp_> it's gonna be so horridly slow that you'd have trouble checking that it works
16:36:37 <tromp_> at least the direction i took is pretty efficient
16:37:25 <Jafet> c2bf might be only a few patches away from being up to the task
16:38:08 <Jafet> C is nearly as bad at memory management as brainfuck, however
16:38:49 <int-e> at least it has pointers
16:39:28 <int-e> In fact I disagree completely with that statement.
16:40:21 <int-e> In Brainfuck you find yourself playing Hilbert's Hotel games all the time. That doesn't really happen in C.
16:41:46 <Jafet> By C I mean the subset of C implemented by c2bf.
16:41:48 <int-e> ("Oh I will put this data on cells divisible by 3, that data on cells with remainder 1 modulo 3, and the cells with remainder 2 modulo 3 will be mostly zero except for one or two bookmarks to guide my code")
16:42:31 <int-e> maybe you should call it c2bf-C
16:44:39 <Jafet> Apparently, c2bf has a "heap" stride but there is no malloc. It'll probably need to be implemented using inline assembly manipulating the heap.
16:45:17 -!- AnotherTest has joined.
16:47:27 <tromp_> you can view the tape as 2-dimensional, with the ith row being cells 1*2^i,3*2^i,5*2^i ...
16:48:08 <Bike> i demand a hilbert space tapej
16:48:12 <tromp_> each successive row being twice as spread out
16:56:59 <mroman_> I demand a bf like language where +-,. are illegal on cells where |index| isn't prime .
16:58:50 <mroman_> Everything is a bf derivative .
16:59:20 <mroman_> nortti: Doesn't have to be brainfuck
16:59:28 <mroman_> but I'd wonder whether you could find your way to the next cell
17:01:14 <Jafet> The number of reachable cells is limited by the size of the program
17:03:30 <mroman_> Not if you find an algorithm that searches for the next valid cell
17:03:52 <nortti> but how do you get there if +-,. are illegal?
17:04:03 <Jafet> It cannot, because it cannot mark the cells on the way to the next valid cell
17:04:19 <Bike> isn't three-cell brainfuck turing-complete? so just use 235 for everything.
17:04:32 <int-e> Bike: that assumes unbounded cells
17:06:17 <Jafet> @oeis 2,3,7,23,89,113
17:06:18 <lambdabot> Increasing gaps between primes (lower end): primes p(k) where p(k+1)-p(k) ex...
17:07:42 <int-e> it's easy to prove that arbitrary long gaps in the sequence of primes exist, just use the CRT to find some n such that n, n+1, ..., n+k are divisible by the first k+1 primes, respectively.
17:11:39 -!- Sprocklem has joined.
17:14:29 <Jafet> > fix (\f ((p,g):ps) -> (p,g) : f (filter ((>g).snd) ps)) $ zipWith ((.)<$>(,)<*>subtract) <*> tail $ nubBy (((>1).).gcd) [2..]
17:15:00 <Jafet> > take 10 $ fix (\f ((p,g):ps) -> (p,g) : f (filter ((>g).snd) ps)) $ zipWith ((.)<$>(,)<*>subtract) <*> tail $ nubBy (((>1).).gcd) [2..]
17:15:26 <Jafet> > take 10 $ fix (\f ((p,g):ps) -> (p,g) : f (filter ((>g).snd) ps)) $ zipWith ((.)<$>(,)<*>subtract) <*> tail $ nubBy (((>1).).gcd) [2..]
17:15:28 <lambdabot> [(2,1),(3,2),(7,4),(23,6),(89,8),(113,14),(523,18),(887,20),(1129,22),(1327,...
17:18:24 <Jafet> > map (text . printf "%.3f") $ zipWith (flip (/)) <*> tail $ [2,3,7,23,89,113,523,887,1129,1327,9551,15683,19609,31397,155921]
17:18:26 <lambdabot> [1.500,2.333,3.286,3.870,1.270,4.628,1.696,1.273,1.175,7.197,1.642,1.250,1.6...
17:20:17 <HackEgo> cercoin yourchiewucoin smocoin cottscoin oisorcoin ncommecoin apfcoin cutercoin petropricoin musissivcoin brazhdcoin varspncumercoin bisc-x86coin kitcoin bradablecoin wordfuctusioncoin ihaxcoin glassendseemeditegrofrcoin kirstecoin skullacoin
17:20:27 <lambdabot> Concatenation of the prime power factors (with maximal exponent) of n; a(1) ...
17:20:43 <lambdabot> Numbers that are the sum of at most 5 positive 5-th powers.[0,1,2,3,4,5,32,3...
17:21:02 <lambdabot> Every base 6 digit of n is a base 10 digit of n.[1,2,3,4,5,35,123,154,215,33...
17:21:37 <myname> this is the reason why people complain about "find the next number" puzzles
17:21:55 <kmc> @oeis 3,1,3,3,7
17:22:00 <lambdabot> 2^A000120(n)-1.[0,1,1,3,1,3,3,7,1,3,3,7,3,7,7,15,1,3,3,7,3,7,7,15,3,7,7,15,7...
17:22:19 <myname> "1, 2, 3, 4, 5, x" "x = 6!" "don't be silly, x = 35"
17:22:27 <Jafet> Wow very much 1337
17:22:52 <kmc> @oeis 8,6,7,5,3,0,9
17:22:53 <lambdabot> Decimal expansion of (7^(e - 1/e) - 9)*Pi^2, also known as Jenny's constant....
17:22:55 <myname> let's invent a sequence
17:23:54 <kmc> @oeis 14,23,28,33,42,51,59,68,77,86,96,103,110,116,125
17:23:55 <lambdabot> Numbered stops in Manhattan on the Lexington Avenue subway.[8,14,23,28,33,42...
17:23:57 -!- conehead has quit (Ping timeout: 258 seconds).
17:24:05 -!- conehead_ has joined.
17:24:12 <mroman_> @oeis 3,6,9,21,24,27,30,33,36,42
17:24:13 <lambdabot> Numbers n such that 2*n^2 + 1 is prime.[1,3,6,9,21,24,27,30,33,36,42,45,66,7...
17:25:19 -!- conehead_ has changed nick to conehead.
17:26:30 <FireFly> I'm actually surprised there isn't a sequence for [A-Za-z]
17:27:47 <myname> @oeis 53,54,55,57,58,63,64
17:28:13 <myname> maybe it only lists infinite sequences
17:28:14 <kmc> @oeis 14,18,23,28,34,42
17:28:14 <lambdabot> Local stops on New York City Broadway line (IRT #1) subway.[14,18,23,28,34,4...
17:28:33 <kmc> the lexington avenue subway does not have an infinite number of stops
17:28:33 <myname> wait, that does kind of contradicts the subway stuff
17:28:34 <FireFly> I hope "Numbered stops in Manhattan on Lexington Avenue subway" isn't infinite
17:28:42 <kmc> space-filling subway
17:29:28 <FireFly> It's a long ride, as they say
17:30:16 <Jafet> There are also the sequences that may or may not be infinite
17:30:32 <kmc> https://www.youtube.com/watch?v=aP1bvY7IqZY
17:31:46 <lambdabot> Mersenne exponents: primes p such that 2^p - 1 is prime. Then 2^p - 1 is cal...
17:33:06 <lambdabot> Triangle of Mahonian numbers T(n,k): coefficients in expansion of Product_{i...
17:34:22 <lambdabot> Numbers n such that 2*n^2 + 3 is prime.[0,1,2,5,7,8,22,23,28,37,40,43,47,50,...
17:34:38 <mroman_> they must have a really large database
17:34:59 <Bike> well, yeah, it's been running for like a billion years too
17:35:24 <Bike> "over 220000 sequences"
17:35:26 <int-e> hmm. my brute force blc search only goes up to 38 bits (doing up to 1000 reductions on each term)
17:36:10 <int-e> (38 is as far as it gets within an hour)
17:36:32 -!- Sprocklem has quit (Quit: leaving).
17:37:13 <Jafet> Free time on the local cluster?
17:37:16 <int-e> the predecessor function (with 0 -> 0) is another hard one.
17:37:27 -!- drdanmaku has joined.
17:38:00 <int-e> (my best is 43 bits)
17:38:54 <tromp_> yes, i got 43 bits as well
17:39:40 <tromp_> i now got pictures of both pred and fac on my office wall
17:40:38 <myname> what are you talking about
17:41:09 <tromp_> about lambda diagrams http://homepages.cwi.nl/~tromp/cl/diagrams.html
17:41:14 <int-e> binary lambda calculus. again. still. I don't know.
17:45:16 -!- Tod-Autojoined has quit (Quit: This is me, signing off. Probably rebooting or something.).
17:45:30 -!- TodPunk has joined.
17:46:58 <myname> i don't get the K example
17:46:58 <Jafet> Wait, how many 38-bit blc programs are there?
17:47:19 <Taneb> Somewhere up to 2^32
17:47:50 <Jafet> Oh, I thought int-e tested 2^38 programs in one hour.
17:48:47 <Taneb> I'd imagine a lot of them are invalid or don't terminate in a nasty way
17:48:48 <tromp_> @oeis 0, 0, 0, 0, 1, 0, 1, 1, 2, 1, 6, 5, 13, 14, 37, 44, 101, 134, 298, 431, 883
17:48:48 <lambdabot> The number of closed lambda calculus terms of size n, where size(lambda x.M)...
17:49:08 <tromp_> https://oeis.org/A114852
17:49:33 <tromp_> 38071898 of size exactly 38
17:49:45 <Taneb> See, less than 2^32
17:50:44 <myname> okay, i start getting it
17:50:55 <tromp_> hmmm, https://oeis.org/search?q=brainfuck&sort=&language=&go=Search
17:54:33 <int-e> right. 82811806 total.
17:54:33 <Jafet> Hmm, I do have free time on a cluster
17:54:59 <int-e> waste of resources, one should first write a faster evaluator.
17:55:46 -!- shikhout has joined.
17:57:41 <tromp_> the ultimate blc challenge is finding more bits of the halting probability omega
17:57:52 <tromp_> i've only managed the first 4 bits
17:58:10 <tromp_> it requires deciding halting behaviour of many programs
17:58:44 -!- shikhin has quit (Ping timeout: 255 seconds).
17:58:53 <tromp_> only a finite number of omgae bits can ever be proven
17:59:11 <int-e> in a fixed, consistent logic
17:59:36 <tromp_> yes, more can be proven in inconsistent logic:)
17:59:54 <tromp_> in fact such logic proves they're all
17:59:56 <tromp_> in fact such logic proves they're all 0
18:00:22 <FireFly> I remember when that was posted to /r/haskell
18:03:09 <kmc> can you say more about why only a finite number of bits can be proven?
18:03:40 <tromp_> by a close analog of berry's paradox
18:04:11 <tromp_> let's say you can enumerate theorems of the form K(x) >= n
18:04:37 <tromp_> that give lower bounds on Kolmogorov complexity of finite strings
18:04:53 <int-e> hmm. I wonder which is the "best" memo library on hackage. (I'm using memotrie but only because that's the first usable one I found)
18:04:58 <tromp_> i.e. there is no blc program less than n bits that outputs x
18:05:41 <tromp_> then you can write a short program that enumerates such theorems until it finds one with n >= N, and outputs the corresponding x
18:06:42 <tromp_> this would show K(x) < logN + O(1), a contradition for large enough N
18:07:10 <tromp_> so any consistent theory can only prove finitely many theorems of that form
18:07:50 <tromp_> the argument for bits of omega is a little more technical
18:08:20 <tromp_> but basically, if you have the first n bits of omega, you can identify all x with K(x) <=n
18:08:36 <tromp_> and thus also an x with K() > n
18:11:11 <tromp_> i like Data.MemoCombinators
18:13:08 <tromp_> in fact i used that for the OEIS entry: https://oeis.org/A114852/a114852.hs.txt
18:14:14 <tromp_> but also for April 2014's Ponder This problem, where i needed to memoize a function on a bounded list of Integers
18:14:30 <Bike> eh, referring to memoization and dynamic programming asthe same thing...
18:15:33 <Bike> i'm disappointed that Memo.integral means integers and not, somehow, integration
18:17:08 <kmc> newest band name: Gigabit Bonghit
18:17:33 <kmc> http://gigabit.bonghit
18:18:38 <Bike> i clicked that, thinking it would lead somewhere
18:18:43 <Bike> thanks again, ICANN
18:18:47 <kmc> you can't tell anymore
18:18:58 <kmc> ICANN has cheezburger
18:20:16 <int-e> Bike: Yes that confusion happens a lot. To be fair, memoization is a very common implementation strategy for dynamic programming.
18:22:03 <Bike> unrelatedly, does anyone else think it's funny when fib is used as an example for recursion and memoization, since you can do it way better with linalg
18:22:37 <int-e> tromp_: what I like about memotrie (possibly because I came up with the same design at some point) is the split memo = untrie . trie, where 'trie' and 'untrie' give you access to the actual data structure used for memoization.
18:23:10 <int-e> tromp_: (personally I call 'trie' 'populate' and 'untrie' 'loopkup', but that's just colors of a bikeshed)
18:23:17 <shachaf> int-e: everyone came up with the same design at the same time, or so i hear
18:23:20 <Bike> i prefer salmon
18:23:51 <int-e> shachaf: not everyone; plenty of memoization libraries revolve around 'memo'.
18:24:27 <shachaf> conal and luqui released their memoization libraries within hours of each other or something
18:25:11 <Jafet> `run words --eng-1M 1000 | grep -o '\w*b' | sed 's/$/ong/' | sort | uniq | /usr/bin/paste -sd\ | head -n 20
18:25:33 <Jafet> `run words --esolangs 1000 | grep -o '\w*b' | sed 's/$/ong/' | sort | uniq | head -n 20 | /usr/bin/paste -sd\ | rainwords
18:25:38 <int-e> Bike: I think it's a fine exemple for introducing the memoization concept. You want people to think about the structure of the computation rather than the actual computed values.
18:26:12 <myname> just for my understanding: in the K lambda diagram, one could have left out the upper half of the vertical bar?
18:26:35 <Bike> it's a good example for recursion too, i just imagine a million programmers using these implementations in actual programs
18:27:03 <int-e> Bike: fortunately fibonacci numbers aren't all that useful in practice ;-)
18:27:21 <Bike> how rude! i have to simulate fuckbunnies all the time
18:27:24 <int-e> especially the larger ones where the linear algebra starts to pay off.
18:27:34 <Jafet> But memofib is such algebraic, much compositional
18:29:05 <Bike> unlike linear algebra
18:35:31 <jconn> FireFly: |value error: mp
18:36:53 <int-e> > fix ((0:) . scanl (+) 1)
18:36:54 <lambdabot> [0,1,1,2,3,5,8,13,21,34,55,89,144,233,377,610,987,1597,2584,4181,6765,10946,...
18:36:56 -!- ^v has joined.
18:38:04 <int-e> a fixed point combinator
18:38:36 <lambdabot> "*Exception: *Exception: *Exception: *Exception: *Exception: *Exception: *Ex...
18:39:19 <int-e> (Sorry, that one is getting old.)
18:41:05 <jconn> FireFly: +---+---+---+---+---+----+-----+-----+-----+-----+
18:41:05 <jconn> FireFly: |0 1|1 1|1 2|2 3|3 5|5 8| 8 13|13 21|21 34|34 55|
18:41:05 <jconn> FireFly: |1 1|1 2|2 3|3 5|5 8|8 13|13 21|21 34|34 55|55 89|
18:41:05 <jconn> FireFly: +---+---+---+---+---+----+-----+-----+-----+-----+
18:42:30 <nortti> oh of course j, the language whose linenoisiness is only beated by teco
18:42:53 <int-e> at least it's ASCII
18:42:59 <myname> what is teco? it sounds like i want to learn it
18:43:02 <Bike> can you really say that in the land of haskell oneliners...........
18:43:07 <Bike> teco is the editor emacs is based on, or something
18:43:12 <int-e> emacs = editor macros (for teco)
18:43:31 <FireFly> teco is like the esotericest esolang ever
18:43:44 <nortti> teco actually does not resemble emacs in normal use at all
18:43:45 <int-e> I understand that it (emacs) wasn't based on Lisp at that time.
18:43:55 <FireFly> and people used it seriously!
18:44:05 <int-e> I used ed seriously
18:44:19 <nortti> int-e: yep, it was basically a screen editor written in a scripting language for another editor
18:44:42 <int-e> (ok. a clone that was implemented in lpmud)
18:45:09 -!- shikhout has changed nick to shikhin.
18:46:07 <int-e> Actually that's about the fragment of vi that I know to use. I use emacs for larger edits.
18:46:28 <myname> so, emacs was written with an editor that was written in a language for a third editor?
18:46:37 <int-e> (where s/vi/vim/ because I use the cursor keys)
18:47:18 <nortti> myname: no, it run on the teco editor's scripting language
18:47:29 <int-e> and how did we end up discussing text editors anyway ... such a loaded topic is best avoided on programming channels. :)
18:48:11 <nortti> there are things to avoid. politics, religion and text editors (or is that part of the second one?)
18:49:05 <Bike> it came up because nortti mentioned it, like, five minutes ago
18:50:06 <FireFly> So, uh, thoughts on Unity?
18:50:17 * FireFly attempts to divert the channel to a less controversial topic
18:50:44 <Bike> terrible. literally the antichrist, foretold in the holy texts
18:50:57 <nortti> last I used it (12.04?) it was still kinda buggy but I could see how they could make it usable
18:51:17 <nortti> then again, I could more easily see how they could fuck it up completely
18:51:31 <int-e> I have not yet had the displeasure of using Unity, and I have no plans to change that.
18:51:42 <Bike> usability doesn't matter. it's perfect and it's evil
18:52:02 <Bike> once its market share has increased the goat shall release the third seal
18:53:29 <int-e> yay, DDG ranks the game engine before the desktop environment.
18:55:27 <Bike> probably ranks gnomes before gnome as well
18:56:06 <nortti> nope, gnome.org is the highest
18:59:46 <Melvar> I am somewhat worried that I haven’t seen a serious project to provide a waylandish xmonad-alike yet.
19:00:02 <Bike> what, is xmonad that tied to x
19:00:22 <nortti> uh, in wayland the wm itself also does display server
19:01:42 * nortti wonders into how small space can be a complete wayland impl be fitted into
19:02:05 <FireFly> I'm a bit worried about that too.. I've been meaning to try out wayland, but I've gotten too used to tiling window managers to be comfortable with weston
19:06:06 -!- tertu has joined.
19:13:22 <fungot> FireFly: i didn't mention that. i think there's my name in for a bit more
19:15:36 <kmc> this is also why i'd have a hard time switching to OS X
19:15:40 <kmc> that and the dismal state of package management
19:18:59 <Bike> what is why? because fungot didn't mention that?
19:18:59 <fungot> Bike: eck, not for efficient programming :)
19:20:08 -!- conehead_ has joined.
19:22:22 <kmc> perhaps fungot will fix my makefile
19:22:22 <fungot> kmc: i'm building off of esr's pronouncements is highly questionable.
19:23:05 -!- conehead has quit (Ping timeout: 264 seconds).
19:34:52 <fowl> they put quantum::superpositions in perl6 lol
19:35:09 -!- ^v has quit (Read error: Connection reset by peer).
19:35:14 -!- AnotherTest has quit (Ping timeout: 240 seconds).
19:35:21 <FireFly> Is that for the & and | (or whatever it was) operators?
19:35:37 -!- ^v has joined.
19:36:03 <FireFly> I never really understood them
19:37:02 <nortti> were those the ones detailed in the talk about perl and physics?
19:39:35 <FireFly> I don't know, but they're explained in http://en.wikipedia.org/wiki/Perl6#Junctions
19:47:43 -!- mhi^ has quit (Quit: Lost terminal).
19:48:29 -!- ^v has quit (Ping timeout: 252 seconds).
19:49:57 -!- ^v has joined.
19:56:35 -!- mhi^ has joined.
19:59:07 -!- Sprocklem has joined.
20:04:41 -!- ^v has quit (Quit: http://i.imgur.com/Akc6r.gif).
20:07:31 -!- tertu has quit (Ping timeout: 240 seconds).
20:16:16 -!- tertu has joined.
20:21:50 -!- quintopia has quit (Ping timeout: 255 seconds).
20:26:11 -!- tertu has quit (Disconnected by services).
20:26:11 -!- ter2 has joined.
20:31:27 -!- nucular has quit (Quit: Excess Food).
20:35:14 -!- Bike has quit (Ping timeout: 258 seconds).
20:36:51 -!- Bike has joined.
20:49:01 -!- tertu3 has joined.
20:49:14 <int-e> tromp_: would 0000101110110 = \\(0 2 1) ==> U(p,z) = <2,z> contribute to the halting probability or is it limited to closed terms?
20:50:58 -!- oerjan has joined.
20:51:27 <kmc> impl<'sink, In, Out, Hold: TreeHandle<In, Out>, Sink: TreeSink<In, Out, Hold>> TreeBuilder<'sink, Sink> {
20:52:49 -!- ter2 has quit (Ping timeout: 276 seconds).
20:52:58 <oerjan> is kmc making an esolang
20:53:17 <FireFly> Yeah, I think it's called "rust"
20:53:23 <kmc> that depends, is HTML parsing turing complete?
20:53:26 <kmc> i'm not making Rust
20:53:28 <kmc> just using it
20:53:38 <kmc> well I have a few patches in rust
20:53:54 <FireFly> Contributing to an esolang, then :P
20:54:03 <kmc> it's less eso than C++
20:54:06 <int-e> tromp_: Oh. I see you're "only" requring the <_,z> context to be in normal form. that also answers my question then.
20:55:01 <kmc> hm I have 10 commits in rust, that's more than I thought
20:55:17 <kmc> several of them are in code that no longer exists
20:55:18 <oerjan> my wild guess is that standard html parsing is not tc but that html-that's-actually-used parsing is.
20:55:23 <kmc> two of them are fixing the same thing that broke twice
20:55:31 <kmc> oerjan: the idea of HTML5 is to unify those two things
20:56:28 <oerjan> so probably uncomputable, then.
20:56:49 <kmc> it's a precise spec for how to handle even very broken content, so that all browsers will do it the same way
20:57:02 <kmc> as a result it's stupifyingly complicated
20:59:42 <monotone> The spec is really just taking the crazy way in which browsers have already been parsing broken HTML and formalizing it so that you can continue to write the same broken HTML in perpetuity.
21:00:05 <kmc> well, yes and no
21:00:14 <kmc> it specifies which constructs are considered broken
21:00:23 <kmc> conformance checkers will reject them, but their meaning is still specified
21:01:01 <tromp_> int-e: yeah, the halting prob. definition is subtle. i believe the normal form requirement is necessary to allow identifying all programs that contribute to an omega prefix
21:01:18 -!- MindlessDrone has quit (Quit: MindlessDrone).
21:01:37 <monotone> Yeah, but that's not really different than how it's been previously. The upshot is that it still renders.
21:02:47 <FireFly> IE6 somehow manages to parse tag-soup mess into where an element could have a child whose parent isn't the first element
21:03:12 <tromp_> i don't want to have U(p:z) = <z,z> in there either
21:04:41 -!- Patashu has joined.
21:05:00 <monotone> The non-tree DOM, right? Looking at the graphs for those was "fun."
21:05:26 <int-e> tromp_: Actually, why not? As long as it reaches that point without looking at the 'z' part ... hmm. Tricky.
21:06:01 <FireFly> monotone: yeah, Hixie has some fun diagrams in an old blog post: http://ln.hixie.ch/?start=1037910467&count=1
21:06:33 <int-e> tromp_: Anyway it looks to me like you have no unique definition of \Omega. The BLC.pdf draft does not mention a normal form property at all, stating that you might just as well not have it.
21:06:42 <oerjan> <tromp_> but i doubt if the goodstein function can avoid recursion <-- i wonder if the functions expressible in system F are the same as those that can be proved total in peano arithmetic, or something like that.
21:07:24 <tromp_> i want to be able to prove the famous symmetry of information thm
21:07:27 <int-e> oerjan: that excludes fix?
21:07:47 <oerjan> for this purpose, at least
21:08:00 <tromp_> that paper has an obsolete definition:(
21:08:33 <kmc> non-tree DOM? :(
21:08:44 <kmc> this is why we can't have nice things
21:09:09 <FireFly> I wonder how the HTML5 algorithm would parse that example..
21:09:17 -!- Sprocklem has quit (Quit: Watching rugby).
21:09:23 <oerjan> int-e: but importantly, it includes church numerals.
21:09:29 <tromp_> to prove symmetry of information, you must be able to take any halting computation and see if the output is a pair starting with some given x
21:09:41 <oerjan> (forall a. (a -> a) -> a -> a)
21:10:07 <int-e> tromp_: anyway, as I read it, 'z' would be a symbolic variable (to prevent the program from inspecting the input beyond the "consumed" part), but then z is also a normal form, so U(p:z) = <z,z> would be allowed.
21:13:19 <oerjan> oh hm no system F is stronger than that https://en.wikipedia.org/wiki/Second-order_arithmetic#Definable_functions_of_second-order_arithmetic
21:13:20 <tromp_> NF should be closed terms
21:15:25 <kmc> FireFly: http://www.whatwg.org/specs/web-apps/current-work/multipage/the-end.html#misnested-tags:-b-i-/b-/i
21:15:43 <tromp_> i've been meaning to rewrite that paper for ages:( always other stuff getting in the way
21:16:02 <tromp_> right now i'm preoccupied both with cuckoo cycle and 8x8 connect-4 :(
21:16:17 <kmc> what are you doing with connect 4?
21:16:24 <int-e> (is that standard? in first order term rewriting, free variables are everywhere (there's no way to bind them...))
21:17:01 <int-e> so variables as normal forms are also everywhere.
21:17:04 <kmc> as in which player wins with optimal play?
21:17:26 <int-e> width 8 ... oh that would upset my intuition about the game a lot.
21:17:36 <kmc> how are you going about it?
21:17:47 <tromp_> i should edit that article to make explicit what that i mean closed normal forms, int-e
21:18:36 <FireFly> kmc: hm, that seems to match the Mozilla behaviour from 2002
21:18:46 <tromp_> well, i have a solver that works some dozen plies into the game
21:18:57 <int-e> kmc: you should see http://homepages.cwi.nl/~tromp/c4/c4.html
21:18:58 <FireFly> the element cloning is a bit bizarre, but it's invalid to begin with so I guess it doesn't matter too much
21:19:03 <tromp_> now i need to play lots of games and build an opening library
21:19:55 <oerjan> tromp_: the last link + the first parentheses in https://en.wikipedia.org/wiki/Goodstein%27s_theorem would seem to imply that the goodstein function _can_ be expressed in system F.
21:22:34 <tromp_> you mean "The Power of a Detour via Infinity", oerjan?
21:22:57 <oerjan> no, i mean _my_ last link https://en.wikipedia.org/wiki/Second-order_arithmetic#Definable_functions_of_second-order_arithmetic
21:23:58 <oerjan> i realized my sentence was ambiguous and that's why i changed to "that"
21:24:42 <tromp_> hmm, how does definability in system F related to definability without recursion? is that equivalent?
21:24:55 <oerjan> system F has no recursion
21:25:12 <oerjan> it's rank-N typed lambda calculus
21:26:39 <tromp_> ic. so i should be able to redefine my function g without using haskell's recursion
21:27:06 <tromp_> but it may not be pretty:-(
21:27:25 -!- Patashu has quit (Ping timeout: 265 seconds).
21:27:56 <int-e> tromp_: the church numeral thing should JUST WORK, if you give church numerals the right type (forall a. (a -> a) -> a -> a)
21:28:04 <oerjan> i'd sort of expect you'd need to represent ordinals.
21:28:40 <oerjan> yes, another property of system F is that you can _define_ church numerals as the terms of that type
21:29:21 <oerjan> this also works for church representations of many other data types
21:31:30 <oerjan> e.g. the only system F terms of type forall a. a -> a -> a are the church booleans
21:32:47 <oerjan> system F is the original system with parametricity, and unlike haskell's version there are no subtle caveats for when it applies.
21:37:29 <kmc> http://s.cow
21:37:45 <kmc> https://cow
21:38:12 <oerjan> tromp_: btw if the implementation of g in system F depends heavily on higher rank types, then it's likely you may need explicit type annotations to make it compile as haskell.
21:38:29 -!- augur has quit (Ping timeout: 258 seconds).
21:38:34 <oerjan> (with ghc's rank-n extension)
21:39:17 -!- Bike has quit (Ping timeout: 264 seconds).
21:39:44 <oerjan> because haskell's type inference only infers rank-2 types with all foralls outermost.
21:40:27 <oerjan> i'm not sure if that is considered rank-2
21:41:02 -!- Bike has joined.
21:41:08 <shachaf> ghc doesn't infer rankine types hth
21:42:23 <oerjan> `frink 100 rankine -> kelvin
21:42:28 <HackEgo> Warning: undefined symbol "rankine". \ Warning: undefined symbol "rankine". \ Unconvertable expression: \ 100 rankine (undefined symbol) -> 1 K (temperature)
21:43:00 <shachaf> apparently frink doesn't support them at all
21:43:05 <shachaf> even with explicit annotations
21:44:29 -!- Phantom__Hoover has quit (Ping timeout: 250 seconds).
21:52:28 <FireFly> I didn't even know about it. Is it actually used for anything?
21:52:34 <FireFly> It seems like a terrible scale
21:54:05 <kmc> I think a lot of engineering in the US is still done with ye olde units
21:54:45 * kmc wonders if BART gauge is 1676 mm or 5'6"
21:56:42 <kmc> a difference of 400 microns
21:57:20 <kmc> 100 microns sounds much smaller than 0.1 mm
21:57:25 <Taneb> Isn't that less than the error caused by heat fluctuations?
21:57:26 -!- Phantom__Hoover has joined.
21:57:31 <kmc> Taneb: probably
21:57:57 <oerjan> <int-e> it's easy to prove that arbitrary long gaps in the sequence of primes exist, just use the CRT [...] <-- n! + i, i = 2..n hth
22:06:53 <kmc> Taneb: hm, no, I think it's about an order of magnitude larger
22:07:37 <kmc> steel expands by a factor of 13e-6 / °C; record temperature range in SF is 43 °C
22:08:04 <Taneb> What's really scary is the age of my university is of the same order of magnitude as my age
22:08:16 <kmc> top of a rail is about 7 cm
22:08:23 -!- HackEgo has quit (Remote host closed the connection).
22:08:33 -!- HackEgo has joined.
22:08:38 <kmc> which comes out to about 40 microns
22:08:53 <Taneb> > 0.01 * 7 * 43 * 13e-6
22:10:06 <lambdabot> mueval-core: L.hs: removeLink: does not exist (No such file or directory)
22:12:33 <int-e> (this reminds me that I don't know for certain why this happens. mueval copies that file to /tmp, but can several muevals run concurrently?)
22:13:57 <olsner> hmm, it copies L.hs to /tmp/L.hs?
22:14:51 <kmc> http://en.wikipedia.org/wiki/Thermal_expansion#Examples_and_applications "Thermal expansion of long continuous sections of rail tracks is the driving force for rail buckling. This phenomenon resulted in 190 train derailments during 1998–2002 in the US alone."
22:15:16 <kmc> i think that's buckling because it gets longer, not thicker
22:15:21 <int-e> olsner: sadly, yes. that's where it puts the temporary haskell file to be loaded, and it doesn't set an include path in ghci
22:15:40 <int-e> where by ghci I mean ghc-as-a-library.
22:18:16 <olsner> then I assume/hope that only one evaluation can be running at a time?
22:18:55 <olsner> is it lambdabot that copies the file and runs mueval on it, or is that in mueval?
22:18:57 <int-e> 00:10:06 <lambdabot> mueval-core: L.hs: removeLink: does not exist (No such file or directory) <-- this is evidence to the contrary
22:19:51 <int-e> which should probably create a temprary subdirectory in /tmp each time instead.
22:20:12 <int-e> just to avoid this problem. oh well.
22:21:53 -!- impomatic has quit (Ping timeout: 264 seconds).
22:26:43 -!- tertu3 has quit (Ping timeout: 240 seconds).
22:35:49 -!- impomatic has joined.
22:36:19 <oerjan> via agora http://www.loweringthebar.net/2014/05/sign-installer-cited.html
22:44:03 -!- Eritzap has joined.
22:45:46 -!- Sgeo has joined.
22:48:05 -!- Eritzap has quit (Client Quit).
22:52:15 <Sgeo> Maybe not part of here
22:53:00 <HackEgo> papacoin flumpezzycoin vergenigmationcoin dupcoin earenamcoin percoin regxcoin fullcoin adedcoin andomcoin carcoin closuricoin inctcoin funandcoin voltacoin bearecoin ozakcoin numpcoin brbcoin acrcoin
22:53:13 <kmc> I think we've seen dupcoin before.
22:53:45 -!- nooodl has quit (Ping timeout: 252 seconds).
22:54:00 <oerjan> kmc: might be a duplicate.
22:54:30 <oerjan> i also have a hunch we'll see brbcoin again
22:55:00 <Sgeo> oerjan: someone in tcl said
22:55:10 <Sgeo> "wow Sgeo i find an interesting language and you are already in channel"
22:59:11 -!- augur has joined.
22:59:54 <oerjan> Sgeo: are you in all the language channels twh
23:00:19 <Sgeo> No, but I'm in a lot of them
23:01:44 -!- yorick has quit (Read error: Connection reset by peer).
23:02:19 -!- mhi^ has quit (Quit: Lost terminal).
23:02:28 <Sgeo> Java, Prolog... actually, seem to be banned from ##prolog :(, Ada, Agda, Atomo, Atomy, Chicken, Clojure, Concatenative (Factor etc.), Dylan, Elixir, Erlang, Guile, Haskell and some associated channels, Idris, Lisp (CL), Pharo, Smalltalk, Racket, Red-lang, Retro, Scala, Scheme, Self-lang, sgeolang, Tcl
23:02:51 <kmc> how did you get banned from ##prolog
23:02:52 <Bike> haha how do you get banned
23:03:05 <kmc> was the ban message "No."?
23:03:37 <oerjan> kmc: nah they just cut him off
23:10:45 * impomatic notes that Sgeo isn't in Forth, Oberon or Pascal :-P
23:11:46 <shachaf> whoa, a language channel that banned Sgeo?
23:12:14 <shachaf> ##prolog: ban *!*@*.dyn.optonline.net
23:12:38 <HackEgo> [wiki] [[Special:Log/delete]] delete * Ehird * deleted "[[Sngscsv]]": content was: "todo" (and the only contributor was "[[Special:Contributions/Dggh|Dggh]]"); possibly spam? feel free to recreate when there's more content
23:13:21 <Sgeo> Why block an entire ISP? :(
23:16:24 <oerjan> Sgeo: if there's an ip-changing troll from there...
23:16:59 <oerjan> (also, i hear cloaks exist.)
23:17:24 <oerjan> actually, do they help against that...
23:28:25 -!- tertu3 has joined.
23:31:57 -!- ter2 has joined.
23:35:24 -!- tertu3 has quit (Ping timeout: 258 seconds).
23:49:27 -!- ter2 has quit (Read error: Connection reset by peer).
23:49:49 -!- ter2 has joined.
23:55:58 <oerjan> <int-e> (ok. a clone that was implemented in lpmud) <-- ooh me to
23:56:09 <oerjan> also i learned lpc before real c
23:56:24 -!- shikhout has joined.
23:56:57 <oerjan> that lpmud ed may be the reason i ended up a vim user
23:59:40 -!- shikhin has quit (Ping timeout: 265 seconds).