00:00:33 Night all 00:00:38 -!- cpressey has quit (Quit: Leaving.). 00:01:33 botte: you convinced them in the end? 00:01:53 scarf: well, he didn't argue after i said that "dropping doesn't require ownership, right?" (along those lines) 00:01:59 probably there was typing lag 00:02:03 i.e. he hadn't read my request to drop when typing that 00:02:54 scarf: aargh, freenode doesn't allow + in emails 00:03:05 use . then 00:03:11 or perhaps not 00:03:15 gmail, you can put dots anywhere you like in the address 00:03:16 scarf: that only lets me punctuate with ., not add more text 00:03:17 and it ignores them 00:03:20 i know that much 00:03:20 botte: yep 00:03:25 binary :-) 00:03:27 but it's good enough for address uniqueness 00:03:36 it appears to maybe allow + 00:03:38 (bonus points if you come up with an address that punctuates both ways round) 00:03:40 perhaps it doesn't like my sha1 password 00:03:50 use the first half, it's almost as secure 00:04:08 yes, but ... 00:04:57 but what? 00:05:12 oh, the "any password should be allowed" theory? 00:05:27 pretty much 00:05:36 it's not like it isn't being hashed (i bloody hope it is) 00:05:36 * scarf vaguely wonders how secure a 1-char password would be if it wasn't ASCII 00:05:47 botte: it may be on the /input/ side that's the problem 00:05:53 howso? 00:05:57 auto-ID might not work properly in many clients if the password was too long 00:05:59 for instance 00:06:21 Two IPv4 IANA pool exhaustion estimates: April 8th next year and May 28th next year... Going to get busy with IPv6 migration... 00:06:25 I'd certainly expect passwords with spaces in to be rejected in IRC due to screwing up argument parsing 00:06:29 scarf: no spaces 00:06:41 Ilari: nah, nobody will migrate anyway 00:06:50 they'll just NAT entire countries or something stupid like that 00:06:56 i was about to say, yeah, nat 00:07:20 (apparently, the entire population of some country shares one IP due to a NAT+filter; IIRC, Qatar, but it might be a different one) 00:07:32 (it caused a huge row when Wikipedia blocked the IP for vandalism, not realising its significance) 00:07:38 (and it was undone as soon as somebody noticed) 00:07:56 Qatar; the defier of usual English spelling, owner (well, royal family) of Harrods, and hater of IPs 00:08:33 *IPs! 00:08:49 the ISPs will love mass-NATting, as it'll give them an excuse to make people pay extra to run a server from home 00:08:58 a lot of them even forbid that. 00:09:20 Meanwhile, http://www.bogons.net/ is still bullshit-free (and I still haven't got around to registering yet). 00:09:32 * scarf wonders when people will finally realise they've chained too many levels of NAT and it doesn't work any more 00:09:38 (static IP, IPv6, only intelligent people, etc.) 00:09:45 (small company) 00:09:49 scarf: s/will// s/'ll// s/give/gives/ 00:10:08 a bit on the pricy side though 00:10:13 (very on the pricy side) 00:10:15 moreso than last time 00:10:23 Some ISPs are already in the habbit of doing mass-NAT. 00:10:30 s/habbit/habit/ 00:11:08 notably AOL 00:11:31 which was especially strange as each account had its own IP anyway 00:11:34 i don't think anyone actually uses aol any more :P 00:11:41 (you can tell they did due to the XFF headers) 00:11:59 alise: do you have an opinion on Oracle vs. Google, btw? 00:11:59 wow, Time Warner split up with AOL 00:12:00 scarf: only that it's inane and oracle suck 00:12:21 (I don't actually know much about the suit, just that oracle are pretty much universally inane and idiotic) 00:12:27 also, netscape.com still exists 00:12:37 although nowadays it's AOL.com + netscape branding 00:12:37 that doesn't surprise me. 00:13:32 I've been looking at the lawsuit 00:14:05 and it's hard to see what Google are supposed to have done wrong here, other than patent infringement against dubious patents 00:14:26 all technology patents are dubious 00:14:28 even by the standard of patents 00:14:30 technology = software 00:14:31 not hardware 00:14:36 that is 00:14:37 but not 00:14:40 software patents specifically 00:14:46 but, you know, computer patents that aren't to do with chips 00:15:55 -!- augur has joined. 00:16:12 botte, are you becoming Thribb? 00:16:16 the only potentially legitimate claim, other than software infringements, I think Oracle have is trademark infringement 00:16:19 but they didn't file that one 00:16:33 Vonlebio: verily, I 00:16:38 am'nt; I have 00:16:38 (I think they might legitimately be able to get an injunction against Google advertising materials claiming that Android is based on Java) 00:16:40 a lament 00:16:43 of furious 00:16:45 poets 00:16:49 that i didn't knowit. 00:17:10 Who's died lately? 00:17:19 farthunter 00:17:22 he hunted farts 00:17:25 verily 00:17:29 So 00:17:34 farewell then 00:17:38 farthunter. 00:17:47 "Prrrrt" 00:17:48 I defy all conventions of poetry and hereby sign my suicide note. -J 00:17:49 That was 00:17:53 THE POEM IS OVER. 00:19:16 scarf: ugh, it /was/ a password length limit 00:19:17 that is indeed, in a sense, poetry 00:19:30 Blank verse is easier than rhyming 00:19:33 Oh, look, the Agda people have an article on Agda vs Coq. 00:19:33 For there's no need to worry of timing. 00:19:37 The problem, you see, with blank verse, to me, 00:19:43 Their first argument is that Agda has nicer syntax. 00:19:44 is that it's just an excuse for people to write prose and call it poetry. 00:19:47 -- G. Richards 00:19:52 Vonlebio: They're wrong. 00:19:58 I mean, sure, nicer to look at (unless you read the stdlib -- hideous) 00:20:02 not nicer to write. 00:20:20 non-exhaustive list of words "poetry" is not an angram of: pottery, topiary, temporary, zoetrope 00:20:38 Then something to do with writing programs in Emacs. 00:20:54 They admit that they have no tactic system, though. 00:21:06 scarf: XD 00:21:29 Addendum to the non-exhaustive lists of words "poetry" is not an anagram of: pig, ontological, metaphorically, understoodingness 00:22:09 Oh, and they say that Agda is easier to learn. 00:22:15 at least "metaphorically" contains all the letters "poetry" does 00:22:22 Vonlebio: wrong. 00:22:28 it just looks superficially similar to haskell 00:22:38 metaphorigasm 00:22:57 hmm, "origasm" looks so much like it's a word 00:23:01 yet isn't one 00:23:05 Perhaps you would just like to dismiss them all at once. 00:23:06 http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVsCoq 00:23:20 Urban Dictionary: origasm 00:23:20 the sexual pleasure that one gets from either making or admiring origami. 00:23:20 www.urbandictionary.com/define.php?term=origasm - Cached - Similar 00:23:22 it's a wiki? just edit them to be correct 00:23:23 That .. was what I had predicted. 00:23:34 Vonlebio: They're wrong and Agda users smell funny. 00:24:17 I agree, after using Coq. 00:24:21 -!- zeotrope has joined. 00:24:22 coq's syntax is better than agda for people who actually use it. interactive development is possible with Proof General; much nicer than Agda's mode. Proving things in Agda is almost impossible; it is not developed for that at all, while Coq is built around it. ProofGeneral makes it even nicer. 00:24:27 I haven't used either 00:24:30 Coq can be predicative or impredicative; by default predicative. 00:24:40 Coq does support mutual definitions; perhaps not in the way the wiki means. 00:24:43 Agda might just maybe be good for pointless mucking about with dependent types. 00:24:52 zeotrope: how can you join after I said "zoetrope" not more than 5 minutes earlier? 00:24:55 Coq's pattern matching is a hassle because it does proper dependent pattern matching; Agda does not. 00:25:04 Set Implicit Arguments is nicer. 00:25:14 Safety belts, aka "easy ways to get an inconsistent system". 00:25:19 scarf: prescience ;) 00:25:25 Non-fixed system, aka "we're totally awesome and unstable"! 00:25:33 Less is more: because dependent proving is hard. 00:25:38 (It really is. So you need more.) 00:25:52 Learning curve: yes, you can write trivial haskell-style programs with extra dependent types in Agda quickly. but you can't get anything useful done. 00:25:57 too much spice 00:26:00 Vonlebio: There you go; done. 00:26:11 Agda is interesting as a research project; nothing more. 00:26:26 botte: what about proving via causing programs to type correctly in Haskell / some other language with type inference? 00:26:56 ugh, I just realised that at some point in the next few years, someone will prove a trivial theorem about lambda calculus by getting a C# program to compile 00:27:00 scarf: that's how proofs work in every dependently typed language. except you don't use inference much 00:27:05 and claim this as some sort of achievement 00:27:20 -!- augur has quit (Ping timeout: 265 seconds). 00:27:36 botte: saves time over writing the whole proof out by hand 00:27:51 -!- tombom has quit (Quit: Leaving). 00:27:54 scarf: heh 00:28:20 my favourite tactics in Coq are "auto with arith", "trivial" and "omega" 00:28:26 type one in, press ., hope for the best 00:29:06 scarf, why did you realise that? 00:29:40 scarf: because the people who do that sort of thing keep turning up at my department and giving seminars 00:29:48 *Vonlebio: 00:29:55 what a strange tabcompleteo 00:30:02 * scarf wonders what sort of confusion is needed to successfully nickping /yourself/ 00:30:07 (completo: like a typo, but for tab complete) 00:30:11 scarf, srsly? 00:30:13 Vorpal: I realised that because... 00:30:16 Oops, completo. 00:30:24 Vonlebio: yes, srsly 00:30:34 So what do the lectures say? 00:30:52 it's mostly people from Microsoft Research 00:31:05 who use C# and F#, and do something that either seems trivially easy, or makes no sense 00:31:23 Saying "we have invented a calculus that uses only anonymous functions, often called lambdas." 00:31:31 I got thrown out of a seminar once for laughing too much at a statement that seemed to me to be the opposite of reality 00:31:36 Vonlebio: not quite that basic 00:31:40 What was the statement? 00:31:42 "Hahaha. HAHAHA! HAHAHAHAHAHAHA!" 00:31:50 "What?" "You're stupid." 00:31:51 Vonlebio: I can't remember the basis 00:31:59 "I..." "I KNOW STEPHEN WOLFRAM. PERSONALLY." 00:31:59 The general hilarity? 00:32:03 "[whimper]" 00:32:27 hmm, do you know System-C? 00:32:28 I AM THE LOVE CHILD OF ALONZO CHURCH JR AND HASKELL CURRY'S DAUGHTER! 00:32:44 Fun fact: they supposedly dated. 00:32:51 imagine you've invented a language 00:33:01 scarf, is it a typed lambda calculus, like System F? 00:33:02 Vonlebio: i refuse to believe 00:33:03 but i want to believe 00:33:12 but instead of writing a parser, you instead ask people to build a parse tree at runtime in some other language 00:33:16 Vonlebio: no, completely different 00:33:17 scarf, ais523? 00:33:21 yes 00:33:21 yes, I'm ais523 00:33:25 right 00:33:30 he's gone from 7 to 27 00:33:37 coppro, ? 00:33:44 so, instead of having a language where you write a:=b+c 00:33:52 botte, I'll look for a link 00:33:59 * Vorpal is now known as cravat 00:34:01 scarf, ^ 00:34:02 you write, say, variable(a)->assign(variable(b)->add(variable(c))) 00:34:18 and all does is builds a parsetree for later execusion 00:34:21 *execution 00:34:22 botte, http://importantshock.wordpress.com/2007/08/21/haskell-curry-yes-i-dated-his-daughter/ 00:34:26 *all this does is 00:34:50 scarf: screw it, I'm supporting arbitrary nicks 00:35:02 http://pastie.org/1105138.txt?key=nsqexkxchx4ofd14wv3v4g 00:35:04 scarf: behold. 00:35:13 you then claim that this a) makes the syntax more familiar, and b) means the language you're creating, and the language you're writing in, are now compatible in some sense 00:35:20 pastie.org/1105138.txt?key=nsqexkxchx4ofd14wv3v4g 00:35:20 that is 00:35:26 System-C is a VHDL-alike using C++ as the host lang 00:35:30 So, noöne talking at the moment uses the nick they used a month ago. 00:35:33 warning: Incredibly gnarly Python code! Only click if you're in to that sort of thing! 00:35:38 Vonlebio: this is just to register it 00:35:41 the person in the seminar was doing something similar with CUDA and C# 00:35:43 scarf, oh, I think I heard of that. 00:35:44 -!- botte has changed nick to alise. 00:35:45 scarf: So, Pain + Agony. 00:35:53 System-C is a VHDL-alike using C++ as the host lang 00:35:55 worst idea ever 00:35:55 and I remembered the comment I was laughing at 00:35:57 alise: agreed 00:36:03 well, maybe not the /worst/, but pretty bad 00:36:18 it was something about this mechanism making the language more scalable 00:36:38 which struck me as a slightly bold statement, given that all the loops used were inherently unrolled 00:36:53 (as they were using a normal C# loop around the parsetree-builder_ 00:36:55 System-C is a VHDL-alike using C++ as the host lang <-- I thought it was closed to Verilog than VHDL? 00:37:05 s/_/)/ 00:37:13 Vorpal: same thing 00:37:15 he said -alike. 00:37:18 closer* 00:37:27 Vorpal: VHDL and Verilog are identical apart from the syntax, for all practical purposes 00:37:29 pretty much 00:37:42 thus, "VHDL with different syntax" and "Verilog with different syntax" are basically the same concept 00:37:51 hm 00:38:12 scarf, I thought verilog lacked assignments outside processes or something like that? 00:38:20 of course in practise you would get the same code... 00:38:22 so does VHDL? 00:38:25 Vorpal, hardly a big difference. 00:38:30 the concept doesn't actually make sense 00:38:44 scarf, no? You can write sig_out <= a or b; iir c? 00:38:45 (you can <= outside processes in VHDL, but that's just sugar, effectively) 00:38:46 iirc* 00:38:52 scarf, yes that is what I meant 00:38:53 -!- sshc_ has joined. 00:39:06 -!- Vonlebio has quit (Quit: Read the SHOCKING TRUTH about Church Jr. and Ms Curry in my new book!). 00:39:16 s <= a or b; is sugar for begin process (a, b) s <= a or b end process 00:39:24 scarf, hm true 00:39:29 (+ filling in the bits of syntax I missed out because nobody can be expected to /remember/ VHDL syntax) 00:39:37 scarf, same 00:39:38 time to go home, anyway 00:39:41 process begin 00:39:43 -!- scarf has quit (Quit: Page closed). 00:39:44 I think is the order 00:39:50 night 00:42:16 -!- sshc has quit (Ping timeout: 252 seconds). 00:42:29 hmm 00:42:34 what's the name for a raw line of IRC text? 00:42:39 including all the syntax 00:45:56 -!- Wamanuz has quit (Remote host closed the connection). 00:47:47 . 00:48:15 Congratulations alise, my current obsession is NetHack 00:48:26 heh 00:48:31 at least it's a good one 01:01:27 -!- Flonk has quit (Quit: ChatZilla 0.9.86 [Firefox 3.6.8/20100722155716]). 01:02:55 alise, if something wasn't good, would I be obsessed? 01:07:38 alise, are you still interested in NetHack? 01:07:43 Or have you moved on? 01:10:40 Sgeo: I'm interested but taking a break. 01:29:18 ?! 01:29:24 Apparently the prefix of an IRC message is optional. 01:35:52 ... There exists opposition to water flouridation? 01:36:31 What's next, opposition to cleanliness in hospitals? 01:38:44 Seriously, why the hell doesn't Europe do water flouridation? 01:38:49 I oppose the use of running water! 01:39:03 Sgeo: That's great. I'll be sure to shit upstream of you. 01:39:14 doesn't flouride worsen the taste? 01:39:20 alise: No, it's flavorless. 01:39:31 mm... flour 01:39:43 http://www.aquaverve.com/blog/content/binary/fluoride_water_main_600[1].jpg ;; lol wat 01:39:43 yeah, fluoridation is pretty much awesome 01:39:43 Also, sl/flourid/fluorid/g 01:39:45 Erm. 01:39:48 s/flourid/fluorid/g 01:39:56 i approve of adding flour to the water supply 01:40:19 pikhq: I dunno, fluoride is a Good Thing but I'm not sure I like the idea of an impure water supply. 01:40:25 We do it here in the UK, I'm pretty sure. 01:40:40 alise: Only 10% of the population of the UK has fluoridated water. 01:40:47 huh 01:40:59 fluoridation in water supply is typically only a few ppm 01:41:00 I know that the water supply in the UK, taste-wise, varies from acceptable to yucky 01:41:08 coppro: oh, I know that, it's just the principle of the thing 01:41:18 I'd only object to fluoride as part of a wider "pure tap water" position 01:41:26 Only a few countries actually do water fluoridisation commonly. 01:41:29 & i know that fluoride is a Very Good Thing for teeth 01:41:40 typically less than an order of magnitude more concentrated than ocean water 01:41:50 yes, i know 01:41:51 (US, Canada, Ireland, Australia... Also, France does *salt* fluoridisation.) 01:42:06 at those levels, it's actually almost irrelevent except for the teeth of the young 01:42:16 i use a fluoridic (word?) toothpaste anyway 01:42:17 :P 01:42:36 http://upload.wikimedia.org/wikipedia/commons/5/5d/Unholy_three_cropped.png 01:42:39 as do I, plus I get a topical fluoride treatment twice a year 01:42:41 coppro: Which is itself fairly beneficial. 01:42:45 FLUORIDATED WATER, POLIO MONKEY SERUMS, MENTAL HYGIENE ETC. 01:42:47 THE UNHOLY THREE 01:42:57 as do I, plus I get a topical fluoride treatment twice a year ;; why? 01:43:04 that seems excessive. 01:43:28 alise: It's a fairly routine thing; you're probably just not aware that there's topical fluoride being done. 01:43:49 what, you mean it's done in my sleep? :) 01:44:09 No... It's just not pointed out that it's topical application of fluoride. 01:44:26 you mean as part of a regular dentist's appointment? 01:44:31 Yes. 01:44:58 at least in my experience, over here that consists of them poking at your teeth with some metal and then saying "Okay, they're fine. Now go away, I want to give some poor, poor child the pain of DRILLS." 01:45:10 perhaps i just have teeth that make dentists unusually satisfied 01:45:49 alise: you must not see a hygenist then 01:45:50 (you should) 01:46:02 alise, someone in #nethack wants your help 01:46:20 here, anyways, hygenists typically work with dentists and you get the appointments one right after the other 01:46:24 Sgeo: who? 01:46:28 though if you have special concerns you can see either separately 01:46:35 any way to pacify watchmen in minetown? 01:46:35 I had to kick open the exit door... 01:46:41 coppro: I'm not sure that's actually common in the UK. 01:46:42 I had a hygenist appointment yesterday because I'd had my braces off recently 01:48:41 I have a tooth that didn't go into place *awesome* 01:48:57 I should, uh, probably get one of the teeth next to it removed so it can do its dropping thang. 01:49:02 But it's been like this for, what, years now. 01:49:23 see a dentist/orthodondist 01:49:42 I should probably do that 01:49:46 My teeth are all weird 01:49:47 I recall doing so when it first refused to drop and they said "get one of the teeth next to it removed for aesthetic reasons". 01:49:58 but they said there wasn't any actual badness about it apart from the look 01:49:59 does the NHS cover either? 01:50:38 i'm not actually sure, I forget the situation wrt dentistry in the uk 01:50:47 but there's no cost issue or anything 01:51:21 hmm 01:51:33 coppro: do you know much about the irc spec? 01:52:50 alise: a fair bit 01:53:22 coppro: will a server ever send a PRIVMSG? 01:53:25 alise: also, according to wikipedia, the treatment (called a fluoride varnish) isn't used in a lot of countries; just really some European ones and Canada 01:53:29 alise: I don't believe so 01:53:36 okie dokie 01:53:52 bleh 01:53:56 python exceptions can be irritating 01:54:07 like I don't want to create a YouCantPRIVMSGAServer exception, that's ridiculous 01:54:09 coppro: Clearly, we should implement a world fluoride policy. 01:54:09 :P 01:54:13 but "IRCError" or something is ludicrously vague 01:54:32 http://upload.wikimedia.org/wikipedia/commons/thumb/f/fb/FluorideTrays07-05-05.jpg/800px-FluorideTrays07-05-05.jpg 01:54:35 hooray 01:55:17 Gross. 01:58:05 I like Vala's system 01:58:15 for exceptions 01:58:27 coppro: Gah, I use both "origin" and "sender" to mean the same thing here. :-D 01:58:45 Would probably be something like IRCError.YOU_CANT_PRIVMSG_A_SERVER 01:58:54 Sgeo: gross 01:59:07 I might have a mistaken impression of Vala exceptions 01:59:26 exception @[Can't PRIVMSG a server] 01:59:32 later: raise @[Can't PRIVMSG a server] 01:59:32 or something 01:59:36 hm? 01:59:41 like 01:59:52 exception @[division by zero] 01:59:52 I like the system of exceptions whereby you realise that things like trying to privmsg a server shouldn't be exceptions 01:59:54 in the division code 01:59:58 raise @[division by zero] 02:00:01 coppro: Then what should it be? 02:00:04 a type error? 02:00:37 an assertion that means there's a bug in the code? 02:00:48 Vala does things that way, actually) 02:00:51 lame 02:00:56 assertion of failure 02:01:09 "oops you did something retarded lol" is a type of exception 02:01:12 imo, an exception should be two things a) exceptional b) not capable of being handled at the error site 02:01:27 assertions are just exceptions with bad error messages 02:01:29 that is 02:01:30 Exceptions 02:01:31 not Errors 02:01:40 alise, not in Vala 02:03:34 coppro: tell me off for mixing origin and sender 02:03:39 that is, "origin" and "sender" 02:04:00 alise: don't do that 02:04:19 coppro: but ctx.sender is much nicer for users of the code, yet in the parser code it's more correct to refer to it as the origin 02:04:22 Bye coppro 02:05:19 FREEish 02:05:40 Gregor: wat 02:05:46 oh, internment 02:05:49 FREEEEEEEEish 02:05:56 * Sgeo considers trying DCSS 02:05:56 amirite 02:06:06 Sgeo: the map moves to keep you in the centre 02:06:08 gives me a headache 02:09:50 coppro: Got a better idea? 02:09:53 :P 02:11:04 alise, coppro left 02:11:10 Er, when? 02:11:33 You should become a regular in ##nomic 02:11:42 No. 02:12:03 I'm thinking of holding office again 02:12:26 I'm not going to frequent a channel run by an asshole who hates my guts and who abused the inattentiveness of the incredibly-absentee channel founder to steal my op privileges. 02:13:07 Is that asshole even active anymore? 02:13:16 * Sgeo can't believe he just said "asshole" 02:16:08 You mean Wooble? 02:17:40 http://www.youtube.com/watch?v=V0W7Jbc_Vhw 02:17:53 alise, waitwhat? 02:18:26 Sgeo: Waitwhat how? 02:18:37 How is Wooble an asshole? 02:18:50 Umm, he's a complete and utter jerk who makes regular slights at comex and me? 02:18:59 And votes against proposals for their author? And ... 02:19:06 He's an asshole because he's an asshole. 02:19:10 And also because of what he did wrt ##nomic. 02:19:38 -!- alise has changed nick to botte. 02:21:43 -NickServ- Metadata : ^ = ^ 02:21:49 /msg nickserv set property foo bar 02:21:49 :P 02:21:51 -!- botte has changed nick to alise. 02:25:46 Hmm 02:26:02 So I should feel a bit weird about him helping me massively wrt NetHack? 02:27:30 Weird? Why? 02:27:46 I don't know 02:31:18 Ok, wtf is going on with flappy? 02:31:36 n/m 02:32:35 ? 02:33:00 Wrong channel 02:36:38 botte's infrastructure progresses 02:37:26 What language? 02:37:45 * pikhq can has a decent FLAC to M4A conversion script. Whoo. 02:37:48 python, it's sufficiently boring 02:38:34 pikhq: *to AAC/MPEG-4 Part 14 02:38:44 pikhq: .m4a is an Apple invention for "MPEG-4 Part 14 that's just audio". 02:38:57 alise: Yeah, yeah... 02:39:06 pikhq: I suggest .aac, if .mp4 is too vague for you :P 02:39:23 Meanwhile, http://i.imgur.com/v9M60.jpg 02:39:26 alise: .aac convinces certain tools that what's inside is a raw AAC bitstream. 02:40:24 Huh. 02:43:43 -!- sshc_ has changed nick to sshc. 03:22:06 -!- comex has joined. 03:28:10 hi comex ico 03:32:03 -!- zzo38 has joined. 03:32:08 Why am I out of permission? 03:32:12 Are you upgrading something? 03:33:59 Or did I put in some word in my file which is censored? 03:34:27 Eh? 03:34:57 Yes, just one example is forbidden, for some reason. I will have to rewrite it 03:35:01 -!- MizardX has quit (Ping timeout: 276 seconds). 03:37:19 alise, be prepared to have an aneurseum 03:37:20 Yes 03:37:29 You know what I _think_ may have introduced me to NetHack? 03:37:39 I think " That must be why. 03:40:07 Maybe you should make it that any forbidden words are not forbidden for autoconfirmed users. 03:40:43 zzo38: spambots can wait until registration completes before attacking 03:40:46 anyway, it's not in my power 03:40:54 alise, User Friendly 03:47:02 Ha ha I inserted a
tag anyways! 03:47:26 http://esoteric.voxelperfect.net/wiki/User:Zzo38 03:47:33 (See near the bottom, the blue part) 03:50:17 -!- nooga has quit (Read error: Operation timed out). 03:50:26 Wait, you actually used my BF-equivalent for one of your languages? 03:50:55 Sgeo: Please elaborate on what you mean? 03:51:04 GrainFimple uses BF-RLE 03:51:14 Sgeo: Yes. 03:51:47 Now can you see that the spam filter doesn't prevent anyone from inserting a
tag anyways? 03:52:25
03:52:29 Seems a bit broken up 03:52:40 Although I guess that may be deliberate 03:53:03 Yes, but if you view the generated HTML code, it doesn't contain the date. 03:53:06 -!- nooga has joined. 03:53:17 alise: go to sleep 03:55:29 * Sgeo zaps alise with a /oSleep 04:04:23 -!- augur has joined. 04:04:48 o hai esopeeps 04:06:11 HEYAUGUR 04:06:13 I'S FREE 04:11:07 what 04:11:12 no, dont answer that 04:11:14 im going to sleep 04:11:14 night 04:12:16 nooga: why? 04:15:06 -!- nooga has quit (Ping timeout: 252 seconds). 04:17:51 Sgeo: why? 04:18:16 because having a weird sleep cycle can be a living hell sometimes 04:21:57 meh. 04:22:06 birthday on sunday, fwiw. 04:25:43 -!- Mathnerd314 has quit (Ping timeout: 260 seconds). 04:46:48 alise, soon it's going to be very dangerous to go to Minetown 04:54:46 -!- zzo38 has quit (Quit: zzo38). 04:58:55 -!- augur has quit (Remote host closed the connection). 05:23:59 bye 05:24:01 -!- alise has quit (Quit: Leaving). 06:16:06 -!- oerjan has joined. 06:30:50 r 07:10:11 !haskell foldl1 (\x -> x + 2*y) [1,1,1,1,1,1,1,1,1] 07:11:38 !haskell main = print $ foldl1 (\x -> 2*x + y) [1,1,1,1,1,1,1,1,1] 07:11:54 duh 07:12:01 !haskell main = print $ foldl1 (\x y -> 2*x + y) [1,1,1,1,1,1,1,1,1] 07:12:04 511 07:12:27 !haskell main = print $ foldl1 (\x y -> 2*x + y) [1,1,1,1,1,1,1,1] 07:12:29 255 07:12:47 !haskell main = print $ foldl1 (\x y -> 5*x + y) [1,1,1,1] 07:12:50 156 07:13:04 !haskell main = print $ foldl1 (\x y -> 3*x + y) [1,1,1,1,1] 07:13:06 121 07:18:58 !help languages 07:18:59 languages: Esoteric: 1l 2l adjust asm axo bch befunge befunge98 bf bf8 bf16 bf32 boolfuck cintercal clcintercal dimensifuck glass glypho haskell kipple lambda lazyk linguine malbolge pbrain perl qbf rail rhotor sadol sceql trigger udage01 underload unlambda whirl. Competitive: bfjoust fyb. Other: asm c cxx forth sh. 07:19:09 !bf >+>+>+>+>+>+>+>+<[>[-<++>]<<]># 07:19:33 no debugging? :( 07:36:32 -!- oerjan has quit (Quit: Reboot). 07:51:02 -!- GreaseMonkey has quit (Quit: New quit message. Entering 2006 in style.). 07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 08:13:37 "My first six months at university I programmed on punchcards." "My entire university career was post-2000." "Whoah, is that true? Damn you young people." ; I didn't have the heart to tell him that all but four months of my high school career was also post-2000 :P 08:15:08 Some people's entire lives are post-2000 08:17:36 Yes, namely people who are 10 years and 8 months old or younger. 08:17:47 Most such people are not currently PhD students though :P 08:18:36 -!- MigoMipo has joined. 08:27:41 -!- Phantom_Hoover has joined. 09:38:09 -!- Wamanuz has joined. 09:44:09 -!- bsmntbombdood has quit (Remote host closed the connection). 10:07:16 Most such people are not currently PhD students though :P <-- XD 10:07:25 Gregor, Only most? 10:08:29 I'm sure it's not "all" 10:08:44 Gregor, really? Citation needed then. 10:12:13 You always hear these stories about 7-yr-olds in college, who then go on to do nothing because their childhood has been completely ruined and they can't live up to the unrealistic and mostly nonsense expectations of them. 10:12:14 My parents didn't want me skipping a grade due to social concerns :( 10:12:20 I don't think skipping 1 grade is as severe as that 10:13:03 Gregor, hm true 10:15:48 it is nice to have radvd working with sixxs finally, that way every computer on my lan has ipv6 (and *yes* I have a firewall of course on the tunnel endpoint, as well as on every computer) 10:33:27 -!- derdon has joined. 10:41:52 -!- Gregor has quit (Quit: Leaving). 10:52:58 -!- tombom has joined. 11:04:54 -!- zeotrope has quit (Ping timeout: 240 seconds). 11:09:11 -!- Phantom_Hoover has quit (Ping timeout: 265 seconds). 11:45:35 -!- derdon has quit (Read error: Connection reset by peer). 12:04:36 -!- tombom has quit (Quit: Leaving). 12:16:18 -!- derdon has joined. 12:43:40 -!- Phantom_Hoover has joined. 12:48:52 -!- MizardX has joined. 13:24:25 -!- MigoMipo has quit (Read error: Connection reset by peer). 13:42:40 -!- Flonk has joined. 13:42:52 blah. 13:45:45 Blah. 13:51:35 .halB 14:27:37 -!- FireFly has joined. 14:30:27 -!- Wamanuz has quit (Remote host closed the connection). 14:51:30 -!- Mathnerd314 has joined. 14:53:14 -!- oerjan has joined. 15:06:22 * Phantom_Hoover loves the way Haskell's tuples are defined manuallyesque. 15:15:17 -!- Wamanuz has joined. 15:16:06 Phantom_Hoover, what? 15:16:27 Vorpal, :i Show in GHCi. 15:16:39 !haskell :i Show 15:16:45 class Show a where 15:17:12 Phantom_Hoover, that looks like it would break if you exceed the number of elements there 15:17:20 Vorpal, it does. 15:17:27 Phantom_Hoover, what a horrible back 15:17:29 hack* 15:17:36 Tuples are only defined to a finite number of elements. 15:17:54 Phantom_Hoover, but surely you can have more elements than (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) in a tuple? 15:17:57 sure it must be finite 15:18:04 but it can be finite of any size you want 15:18:12 Phantom_Hoover, no? 15:18:23 Vorpal, no. 15:18:37 i vaguely recall the report says only tuples up to 15 elements are guaranteed to exist 15:19:17 and for actual class instances and supporting functions, even less. 15:19:20 (,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,) seems to be as far as GHC goes. 15:19:21 wtf 15:19:35 Vorpal, makes perfect sense. 15:19:47 !haskell length "(,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,)" 15:19:48 True, True, True, True, True, True, True, True, True, False, True, True, True, True, True, False) does give me an error about lack of Show instance in ghci (as expected) but apart from that it seems to work 15:19:49 63 15:20:15 Frankly, if you need more than 61 elements in a tuple, you're doing something wrong. 15:20:25 *62 15:20:25 Phantom_Hoover, well yeah 15:20:28 !haskell (True, True, True, True, True, True, True, True, True, False, True, True, True, True, True) 15:20:29 (True,True,True,True,True,True,True,True,True,False,True,True,True,True,True) 15:20:46 hm maybe instances are up to 15 then. 15:20:51 Phantom_Hoover, still it seems like a pointlessly arbitrary limit 15:21:03 Vorpal, no more arbitrary than any other. 15:21:16 Vorpal: i don't think it's _forbidden_ for implementations to support more 15:21:20 Phantom_Hoover, well, limiting it by memory would be less arbitrary 15:21:30 And at least it makes tuples proper algebraic types. 15:21:32 oerjan, yeah pointlessly arbitrary limit 15:21:34 as I said 15:21:51 Phantom_Hoover, hm. How so? 15:22:00 Vorpal: oh i think it may be a limit for _all_ algebraic datatypes, possibly 15:22:33 Vorpal, well, data (,,,) = (,,,) a b c or somesuch 15:22:59 hm okay good point 15:23:31 !haskell :i (,,,) 15:23:33 data (,,,) a b c d = (,,,) a b c d -- Defined in Data.Tuple 15:23:51 Vorpal: as in, ghc may only leave that many bits for telling the GC how long a datatype is 15:24:06 of course any specific tuple type must be finite in size. But I still don't see why you can't just make a larger finite tuple until you run out of memory 15:24:22 oerjan, ouch... right 15:25:01 but then it _does_ have arrays... 15:25:42 requires same data type for all elements though 15:25:46 yeah 15:26:20 -!- Phantom_Hoover_ has joined. 15:26:38 Vorpal, with algebraic data types you can have different types in an array. 15:26:41 of course you could create some CharOrBoolOrWhatever type that "wraps" all the alternatives 15:27:12 Phantom_Hoover_, eh? Are you not talking about [] lists or are you talking about some ghc extension to haskell? 15:27:19 or did I miss out something huge 15:27:21 Vorpal, I mean [] lists. 15:27:29 arrays are not [] lists 15:27:36 oerjan, oops. 15:27:42 oerjan, hm... 15:28:56 [] lists are linked lists, so any limit for size of a single constructor value does not apply. 15:29:08 of course 15:29:13 -!- Phantom_Hoover has quit (Ping timeout: 265 seconds). 15:29:20 -!- Phantom_Hoover_ has changed nick to Phantom_Hoover. 15:29:43 while Arrays would presumably be actually consecutive in memory 15:30:08 hm you could construct a linked list type where the type varied cyclically 15:30:16 sure 15:30:25 -!- Sgeo has changed nick to Jabberwock. 15:30:32 Bleh, registered 15:30:35 -!- Jabberwock has changed nick to Sgeo. 15:30:42 Sgeo, we did that joke ages ago. 15:30:42 any finite state automaton / regular expression could probably be used 15:31:02 Sgeo, lucky for you ;P 15:32:03 also Arrays are Haskell 98 not an extension, i believe, although only immutable ones 15:32:47 -!- relet has joined. 15:33:31 there's that whole Ix class for allowing flexible index types 15:43:24 -!- Flonk has quit (Quit: ChatZilla 0.9.86 [Firefox 3.6.8/20100722155716]). 15:46:07 oerjan, how are the arrays implemented? a binary tree is how I would do it. Unless it is implemented by special forms inside ghc itself 15:46:20 in which case there are more efficient ways to do it 15:48:19 (unless, of course, they are sparse arrays) 15:49:27 dammit the source links in the ghc library documentation are broken 15:49:37 so i cannot give you a precise answer :D 15:49:41 ah 15:49:58 oerjan, and you don't happen to remember? 15:50:17 well i'm pretty sure it's something based on consecutive values in memory 15:51:50 right 15:52:01 oerjan, that would probably require special support from ghc 15:52:07 as in, can't be pure haskell 15:52:15 right? 15:52:34 -!- alise has joined. 15:52:39 yeah. 15:52:59 dammit the source link is broken on hackage too 15:53:31 for what? 15:53:50 Data.Array 15:54:01 i'm trying to find the type definition 15:54:06 ah 15:54:12 (why?) 15:54:45 Vorpal was asking how ghc implements such a type, since you cannot define that directly in haskell 15:55:17 i am guessing it's either something ghc-specific or a wrapped C array of some sort 15:55:44 (directly as consecutive values in memory, that is) 15:56:39 07:21:32 oerjan, yeah pointlessly arbitrary limit 15:56:40 07:21:34 as I said 15:56:47 supporting all of them would require an infinite amount of code 15:56:50 or special compiler support 15:57:04 so it's not "pointlessly arbitrary", it's just the only sane thing to do 15:57:35 alise, do IBMgraphics work for you? 15:57:44 Sgeo: only if i convert the character set 15:58:06 the only reason to is to get the upper half integral fountains :) and iirc the rogue level is screwy with them 15:58:16 Sgeo, the NH wiki tells you how to set it up. 15:58:21 ah found it 15:58:38 The halls are kind of nice 15:58:45 http://www.haskell.org/ghc/docs/6.12.2/html/libraries/base-4.2.0.1/src/GHC-Arr.html 15:58:48 I like the DECgraphics doors better though, I think 15:58:51 Sgeo: install "konwert" 15:58:55 nethack | konwert cp437-utf8 15:58:56 done 15:59:07 the other solution doesn't work as far as i can tell 15:59:09 Or, I could just have PuTTY set up to do cp437 15:59:25 Which I do 15:59:28 Vorpal: it seems to wrap an Array# type, probably a ghc builtin? 15:59:33 oh, i forgot, you use an OS which actually supports that horrid character set. 15:59:42 the # types tend to be 16:00:10 WHat I don't understand is, if NetHack was mostly designed with UNIXs in mind, why they used something that seems to be a Windows thing 16:00:23 for the DOS port, duh 16:00:28 Or by "IBM" do they mean DOS/Windows.. ah 16:00:35 yes 16:00:41 it's the IBM PC glyph set 16:00:48 from the original IBM PC 16:02:16 so julien assange has been accused of rape! 16:02:28 the cia are pretty good 16:04:03 They are, aren't they? 16:05:28 Also *Julian 16:05:58 Is there any way to have Gmail show the current time? 16:06:04 And also to have it use UTC 16:14:45 Sgeo: yes, look at the bottom-right corner of the screen 16:14:57 now you can read the time while using gmail 16:15:00 My system clock is not in UTC 16:15:07 get another clock program 16:15:30 Blargh 16:16:11 oh no running programs on my computer !! 16:20:22 -!- augur has joined. 16:20:31 hi augur 16:20:44 hey alise 16:21:14 "The Wang LOCI-2 (an earlier LOCI-1 was not a real product) was introduced in 1965 and was probably the first desktop calculator capable of computing logarithms, quite an achievement for a machine without any integrated circuits.[1] The electronics included 1275 discrete transistors. It actually performed multiplication by adding logarithms, and roundoff in the display conversion was noticeable: 2 times 2 yielded 3.999999999." 16:23:33 My math teacher lied to me! 16:23:46 Oh gosh how horrific, what did she say. 16:23:52 She said 2+2=4 16:24:35 ...and Sgeo finally snaps completely. 16:24:45 Ha ha, it's funny because inaccurate results on calculators are totally unheard of, and also because you said +, not *, which breaks the joke. 16:25:03 * Sgeo failed to notice that you said times and not plus >.> 16:33:53 just blame it on the logarithms 16:35:03 lol 16:36:53 -!- augur has quit (Ping timeout: 265 seconds). 16:37:35 wait, how did it do that 16:37:42 it has to do ^e 16:37:48 which sounds a lot harder than multiplication to me 16:38:04 indeed even with log2 it'd have to do ^2 which is pretty clearly easiest implemented as a multiplication 16:38:48 er wait, e^ or 2^ ofc 16:39:06 still, eh? 16:47:05 "The secret to the LOCI was Dr. Wang's magical logarithm calculating circuit." 16:47:20 "Wang's calculator was really no more than an electronic adding machine with the key addition of the circuit that allowed logarithms and anti-logarithms to be calculated quickly and accurately." 16:47:25 the magical wang 16:47:36 lol anti-logarithms 16:47:42 aka e^ 16:47:42 -!- wareya has quit (Read error: Connection reset by peer). 16:47:56 well, it might have only done base 10. 16:48:46 -!- wareya has joined. 16:51:58 "The operator's panel layout of the LOCI-2 is probably now used as a study in how not to design for human factors." 16:52:33 xD 16:52:43 http://www.oldcalculatormuseum.com/wangloci.html 16:52:48 wow it's beautiful 16:52:56 that's what i'm looking at 16:53:10 no integrated circuits 16:53:13 quite impressive 16:55:01 Maybe I should implement it in AW 16:56:50 fff 17:00:19 "Of the nine circuit boards in the machine, only three have obvious functions. All of the rest of the boards seem to be a fairly random scattering of diode-resistor and transistor logic gate circuits and flip flops. Dr. Wang was quite protective of his designs, and rumor has it that efforts were purposely made to make it difficult to reverse-engineer the design of the machine." 17:00:26 good luck implementing that 17:00:37 emulate the circuits directly :) 17:01:50 oerjan: "Wang calculators cost in the mid-four-figures" 17:02:09 In the early seventies, Dr. Wang believed that calculators would become unprofitable low-margin commodities, and decided to exit the calculator business. 17:04:33 -!- augur has joined. 17:05:14 "Swedish rape warrant for Wikileaks' Assange cancelled" 17:05:15 good 17:05:27 link? 17:05:32 http://www.bbc.co.uk/news/world-europe-11049316 17:14:21 alise, incidentally, is Agda actually good for anything? 17:16:21 uh 17:16:25 not really 17:16:30 it's a research project :P 17:17:11 Not, as WP claims, a proof assistant? 17:17:29 hahaha 17:17:31 definitely not 17:17:38 Thought not. 17:17:42 programming "actual programs" with some dependent typing, maybe 17:17:43 but really 17:17:46 coq is the best for that 17:17:57 you can write libraries + proofs that they work, then export this code to O'Caml or Haskell 17:18:11 yes, it actually spits out almost-identical datatypes and codes for the non-proof portions 17:18:20 this is known as Awesome. 17:18:21 Wait, the WP article is called "Agda (theorem prover". 17:18:26 *) 17:18:33 Agda (theorem prover), the programming language and theorem prover 17:18:33 Agda (Golgafrinchan), the character in The Hitchhiker's Guide to the Galaxy by Douglas Adams 17:18:33 Agda (Bishop) ( –1024), the Roman catholic bishop of Oviedo 17:18:47 Phantom_Hoover: anyway, yeah, Coq extraction: fucking awesome or amazingly fucking awesome??? 17:18:57 Dunno. 17:19:25 "Per Martin-Löf is an enthusiastic bird-watcher, whose first scientific publication was on the mortality rates of ringed birds." 17:19:25 Phantom_Hoover: write a coq function to do something 17:19:27 then try 17:19:33 Extraction that_function. 17:19:48 even if it invokes proofs which other functions require, these will be elided in the extraction 17:19:57 you can even do 17:20:07 Extraction Library ident.   17:20:07 Extraction of the whole Coq library ident.v to an ML module ident.ml. In case of name clash, identifiers are here renamed using prefixes coq_ or Coq_ to ensure a session-independent renaming. 17:20:07 Recursive Extraction Library ident.   17:20:07 Extraction of the Coq library ident.v and all other modules ident.v depends on. 17:20:20 Extraction Language Ocaml. 17:20:20 Extraction Language Haskell. 17:20:20 Extraction Language Scheme. 17:20:20 Extraction Language Toplevel. 17:21:25 Extraction Language Brainfuck. 17:23:33 This is indeed cool. 17:23:44 Phantom_Hoover: and in fact 17:23:47 http://hackage.haskell.org/package/meldable-heap 17:23:49 Although it inspires no feelings of awe within me. 17:23:50 is the haskell extraction of 17:23:55 http://code.google.com/p/priority-queues/ 17:24:03 + some wrappers i think 17:24:11 But this may well be because it took me about 10 minutes to write fact in coqtop. 17:24:22 don't use coqtop 17:24:29 use proofgeneral with electric mode and three window mode 17:24:34 it is absolutely the only way to stay sane 17:24:43 These things are all COMPLICATED 17:24:54 no 17:24:55 they are easy 17:25:05 with proofgeneral electric three-window you have one window for your file 17:25:09 one for your goal 17:25:13 and one for misc. output 17:25:20 you can execute a command just by "TheCommand foo." 17:25:24 and proofs proceed automatically on . 17:26:28 Phantom_Hoover: http://hackage.haskell.org/packages/archive/meldable-heap/2.0.3/doc/html/src/Data-MeldableHeap-LazyBrodalOkasakiExtract.html 17:26:28 http://hackage.haskell.org/packages/archive/meldable-heap/2.0.3/doc/html/src/Data-MeldableHeap-StrictBrodalOkasakiExtract.html 17:26:34 wrapped by 17:26:40 http://hackage.haskell.org/packages/archive/meldable-heap/2.0.3/doc/html/src/Data-MeldableHeap-Lazy.html 17:26:42 http://hackage.haskell.org/packages/archive/meldable-heap/2.0.3/doc/html/src/Data-MeldableHeap-Strict.html 17:26:46 the first two were extracted from Coq automatically 17:26:53 http://code.google.com/p/priority-queues/source/browse/#hg/brodal-okasaki the coq source 17:26:54 alise, I haven't tried Proofgeneral yet, though. 17:26:58 do so 17:27:02 it is absolutely a requirement 17:27:27 just install it, set electric mode, set three window mode, make your emacs window big, and open a .v file 17:27:54 Setting electric mode and setting three window mode entails what? 17:28:09 electric mode means that commands are executed on . -- you absolutely want this for proofs, so they can be interactive 17:28:14 three window mode i already explained 17:28:26 anyway, just trust me and do it, it'll be worth your while 17:28:34 after a short learning curve it's absolutely the easiest way 17:29:16 brb 17:30:30 Well, customise-group proof-general doesn't help... 17:35:01 Ah, worked it out. 17:55:03 -!- Flonk has joined. 18:21:46 -!- Phantom_Hoover has quit (Ping timeout: 265 seconds). 18:29:41 dammit gmail 18:30:02 oh well, I suppose forcing me not to use gmail filters is good for me in the long run 18:40:56 -!- BeholdMyGlory has joined. 18:59:48 coppro: why? 19:06:47 alise: because Gmail can't grasp the notion of filtering individual messages when trying to run filters on existing mail 19:06:52 it filters the entire conversation 19:07:01 (but it doesn't do this for incoming mail... fail) 19:07:08 coppro: heh, really? 19:07:08 fun 19:07:24 I'm, uh, just gonna run my own mail server asap. 19:07:34 I might use http://en.wikipedia.org/wiki/Sieve_(mail_filtering_language), but the syntax is a bit weird. 19:07:54 In fact, what I might do is just make the mail server pass incoming mail into an executable (probably a shell script), which then moves it into the appropriate filesystem location. 19:08:08 yeah, eventually I'll set something up of my own 19:08:14 but Thunderbird can filter pretty well actually 19:08:20 yeah, but I hate client-dependence. 19:08:31 especially since I theoretically use a mobile too. 19:08:33 so do I 19:08:45 what happens if i didn't run my mail client recently? the whole point is to check for mail,a fter all 19:08:50 eventually I will have a mail server 19:09:06 http://en.wikipedia.org/wiki/Sieve_(mail_filtering_language)#Example ;; this does absolutely nothing that a shell script or python can't do, heh 19:09:18 basically all it does there is parse the email silently :P 19:09:22 * pikhq should get a static IP and a domain 19:09:43 I'd like to run a server from home, but I'd also like something, well, faster. 19:09:54 Ideally I'd colocate, but I Don't Have That Kind of Money. 19:09:57 So ho hum, VPSes it is. 19:10:27 * pikhq should also continue cleaning out all the crap that's in ~ 19:11:07 pikhq: careful, it'll turn into my Computer Renovation Plan 19:11:20 which is actually impossible as it has a step where A depends on B and B depends on A 19:11:28 Leonidas: Oh? 19:11:37 Leonidas: Yeah! Oh? 19:11:43 Dammit Leonidas, reveal your secrets! 19:12:18 alise: Oh? 19:12:21 XD 19:12:37 WHY DO I HAVE SO MANY PDFs 19:12:42 WHY IS THERE SO MUCH IN ~? 19:13:27 -!- Wamanuz has quit (Remote host closed the connection). 19:14:00 pikhq: The basic idea is to change all my passwords into something generated by one of those fancy password-generator-and-storers, but one that's cross-platform and doesn't stink (with browser integration), so I can finally move away from my single-not-very-secure-password system, and get that new computer, and get that new mobile, and get a perfectly tuned Linux on the new computer, and switch the Internet connection to something better, with a static IPv6 19:14:00 reverse DNSed to my domain, which I will register, and a server running on that domain, and a reverse DNS on a subdomain of that domain to my new router, and hence my new computer, and an email server running on that server, serving an email address on that domain, which the ISP is registered with. 19:14:09 pikhq: The thing is, all these happen simultaneously. 19:14:27 rm: cannot remove `vala-0.7.7/gee/.libs/iterable.o': Operation not permitted 19:14:30 What the hell? 19:14:31 pikhq: As a result, I have ensured that my Computer Renovation Plan will never, ever go into effect. 19:14:53 I need to clean my ~ soon 19:15:00 THAT WAS DONE AS ROOT 19:15:07 pikhq: ls -l it 19:15:16 drwS---rwt 2 205232978 2148707191 8192 Dec 29 1969 iterable.o 19:15:19 it might be hardlinked to some /dev/ device :) 19:15:22 Holy *frak* that's fucked up. 19:15:23 -!- Wamanuz has joined. 19:15:26 S and t, what the hell? 19:15:28 d is directory isn't it?? 19:15:38 pikhq: O_o 19:15:41 i have absolutely no clue what that permission is 19:15:41 sounds like fsck time 19:15:43 please walk me through it 19:15:47 d is directory, right? 19:16:12 S is setuid and t is sticky iirc 19:16:18 and d is directory? 19:16:43 "Downloading from 3 of 9 connected peers - 8.2 KiB/s" 19:16:46 no. faster 19:16:49 kthx 19:17:12 there's about 30 peers total :P 19:17:22 shit now i'm uploading faster than my download, this will never download 19:18:05 alise: I think so 19:18:50 that's awesome 19:18:54 wait, S isn't setuid on a directory, is it? 19:18:56 it means something else 19:19:01 maybe 19:19:12 So, what you're saying is that I should mount read-only and fsck. 19:19:18 The setuid permission set on a directory is ignored on UNIX and Linux systems [2]. FreeBSD can be configured to interpret it analogously to setgid, namely, to force all files and sub-directories to be owned by the top directory owner.[3] 19:19:24 pikhq: i'd use a livecd 19:19:28 i wouldn't trust that system >_> 19:19:58 alise: I had an incidence of filesystem corruption on /home/ in the past, courtesy of LVM so "helpfully" not actually being atomic. 19:20:17 This is why LVM sucks >_> 19:20:26 / is still good, /home/ just has... Some crap in it still. 19:20:37 wait 19:20:42 try and cd to iterable.so 19:20:42 :DD 19:20:46 if it's a directory 19:20:51 Done. 19:20:53 ls 19:20:56 then ls -l 19:20:57 :D 19:21:08 total 12 19:21:08 drwS---rwt 2 205232978 2148707191 8192 Dec 29 1969 . 19:21:08 drwxr-xr-x 3 pikhq pikhq 4096 Aug 14 11:40 .. 19:21:12 (after ls -a -l) 19:21:18 That's ... it? 19:21:24 echo hi >foo 19:21:26 ls -l :P 19:21:37 zsh: operation not permitted: foo 19:21:42 sudo -s 19:21:43 echo hi >foo 19:21:58 I suggest (1) copying it somewhere to preserve the crazy, then (2) rmdir 19:21:58 zsh: operation not permitted: foo 19:22:02 pikhq: hmm 19:22:04 try tee 19:22:05 well 19:22:08 cp /dev/stdin foo 19:22:11 hi 19:22:11 ^D 19:22:12 I'll tar the crazy. 19:22:40 And ... WAIT WHAT 19:22:49 :D:D:Dwhat 19:23:00 I can *create* files in there 19:23:04 I cannot *remove* files. 19:23:10 *Oh I know*. 19:23:10 <33 19:23:12 don't tar it 19:23:12 It's sticky. 19:23:15 it'll break shit, i bet 19:23:21 like 19:23:26 there must be more to this than just the permissions 19:23:29 a file has become a directory 19:23:30 where's the file data? 19:23:36 does the directory still point to the inodes somehow? 19:23:44 pikhq: can you open() the directory? 19:23:48 maybe you can read it :D 19:24:03 chmod: changing permissions of `iterable.o': Operation not permitted 19:24:06 WHAT THE FUCK 19:24:13 just ... just leave it there 19:24:18 how big is the filesystem? 19:24:20 chown: changing ownership of `iterable.o': Operation not permitted 19:24:25 WHAT THE FUCK 19:24:43 alise: 758G, 221G free. 19:24:58 pikhq: Do you have more of that space? :P 19:25:07 Compress the whole FS up :D 19:25:09 ARGH 19:25:11 FUCK GMAIL 19:25:20 coppro: what now? 19:25:26 alise: Most of it's videos. 19:25:42 alise: more filtering shit 19:25:53 pikhq: yeah but you'd have to compress the whole 700 gigs 19:25:58 coppro: hmm, what? 19:26:20 Aaaand I only have the 1TB drive here. 19:26:20 alise: gmail's retarded notion of tags means that client-based filtering doesn't work correctly 19:26:33 gmail w/ imap is utterly pointlessly horrible 19:26:41 pikhq: blu-ray drive? :P 19:26:44 No. 19:26:44 it's been fine for me for a long time 19:26:47 but yarrrrrgh 19:27:46 ffff 19:27:47 come on torrent 19:27:47 100 KiB/s 19:34:06 * alise looks into ATS 19:35:33 "4 hours remaining" 19:35:33 /sigh 19:38:29 Note that the symbol int is overloaded: it is both a static constant and a sort. Given an integer i (of sort int), int(i) is a singleton type containing only the integer i. So int is often called a type constructor. We now define a type constant Int as follows: 19:38:29 this is weird. 19:44:54 * coppro starts migrating mail off of gmail 19:45:04 coppro: to? 19:45:16 UW Computer Science Club 19:45:17 you can have my VPS :-P 19:45:26 ugh, I hate university/company mail 19:45:37 -!- tombom has joined. 19:45:39 you /know/ you're not going to be there forever 19:45:41 alise: UW CSC is imap from my homedir 19:45:42 nope 19:45:49 CSC membership is renewable indefinitely 19:45:51 even if not a student 19:46:15 in theory, you don't even need to be a student to have signed up in the first place 19:46:26 ok, so say you move to ... australia and become a successful ... jazz musician, who plays nomic in his spare time 19:46:33 do you still want to use the CSC address? :D 19:46:44 I can forward to it 19:47:10 or migrate it, since I have access to the datatfiles 19:47:23 yeah, but still, it involves an address change 19:47:48 yes; eventually I'll probably get a domain of my own 19:47:52 that's not right now though 19:47:58 and gmail broke the last straw 19:48:02 "Alexander Limi makes software easier to use. Founder of the open source project plone" ;; Plone, the height of usability and simplicity. 19:48:19 coppro: you'll be missing the ui in approx. 10 minutes 19:48:36 alise: honestly, I rarely go on gmail proper as-is 19:48:51 s/-// 19:49:00 s/si/s i/ 19:49:08 i have "plans" to create the Perfect Email Application 19:49:16 excellent 19:49:22 I'll ping you about it in 40 years 19:49:24 originally it was a guiy type affair with conversations and labels but, you know, better ... but that was when i was a mac guy 19:49:33 i guess now it'll be all cat(1)y 19:49:40 actually, oh, i remember my latest design 19:49:42 it was really nice 19:49:52 this is ironic 19:50:01 a dual pane interface showing nested threads on the right, but on the left a conversation style view 19:50:07 and the selected item on the right changed as you scrolled the left 19:50:08 the only time GMail's 'All Mail' folder is coming in remotely handy is when I'm moving everything off gmail 19:50:14 that was nice 19:51:13 ATS is interesting 19:51:28 my only question is whether I care about ancient mail... 19:51:36 coppro: you probably don't even care about recent mail 19:51:52 i'd just leave it on gmail for reference 19:52:04 oh wait, my mail doesn't even come close to my quota 19:52:04 you probably won't need it after a couple of weeks 19:52:04 yay 19:52:10 yes, but, time :P 19:52:16 also, fuck quotas >_> 19:52:17 quotae 19:52:27 quota is reasonable 19:52:33 -!- zeotrope has joined. 19:52:36 but i'm a control freak 19:52:55 4GB, and it's not like it's the only computer I'm allowed to use 19:53:48 I bet I could get it upped if I needed it, too 19:53:53 i need infinite money and a very fast symmetrical fibre-optic link 19:53:59 and a big, big house 19:54:04 then i can run EVERYTHING 19:54:18 -!- Gregor-P has joined. 19:54:24 hi gregor-p 19:54:33 (gregor-p gregor) => T 19:54:35 Yay airports 19:54:36 (gregor-p alise) => NIL 19:57:10 also, I discovered a neat TB feature 19:57:19 it has mailserver autodetection 19:57:32 tuberculosis does have some good feature 19:57:53 lol 19:58:49 http://wondermark.com/650/ 20:07:17 alise: NO WAI! 20:07:59 whee, mail is being copied! 20:16:03 -!- Gregor-P has quit (Ping timeout: 265 seconds). 20:16:44 http://www.osnews.com/images/comics/wtfm.jpg :) 20:21:16 antecedork 20:24:25 -!- augur has quit (Ping timeout: 240 seconds). 20:27:11 -!- Killerkid has quit (Ping timeout: 245 seconds). 20:32:53 -!- Phantom_Hoover has joined. 20:39:33 -!- BeholdMyGlory has quit (Remote host closed the connection). 20:40:06 -!- Killerkid has joined. 20:40:13 oh no! a Killerkid! 20:42:08 -!- Flonk has quit (Ping timeout: 258 seconds). 20:48:05 Oh no! More Lemmings. 20:48:47 (I simply can not have that though whenever there's a "oh no" anywhere.) 20:49:16 Can not avoid having, I mean. 20:49:32 fizzie: *thought, you mean. 20:50:34 fizzie: Did you ever played /3D Lemmings/? It's ... not good. 20:51:30 Anything like 3d worms? 20:51:34 I think I did try it out, though the details are a bit hazy. "Not good" is what I thought it were. 20:55:12 Sgeo: Worms 3D is actually better. 20:55:19 fizzie: *was, you mean! 20:56:21 Gah! 20:56:35 I no can spells and spaek. 20:57:47 -!- pikhq has quit (Quit: Rebooting). 21:00:38 -!- pikhq has joined. 21:00:45 Hah... Rat study of metabolic syndrome... The food for rats: Loads of linolic acid (some of it rancid): Check. Loads of trans fats (from hydrogenation): Check. Dihydrovitamin-K1 (what's roughly known about that substance: 1) It forms from vitamin K1 in hydrogenation, 2) it is nasty stuff): Check. 21:03:00 Ilari: http://www.theonion.com/articles/worlds-scientists-admit-they-just-dont-like-mice,1256/ 21:03:48 -!- nooga has joined. 21:03:51 yuck 21:03:56 noogie! 21:05:53 i'm building chromium 21:08:22 alise: Fun fact: the ATI drivers work so much better than the free software ones. 21:08:34 Dear god I get full-screen Flash actually working well. 21:08:54 (which is not to say Flash is *good*, but it's... Working as intended, at least.) 21:09:01 Ilari, do you plan to implement Brainfuck with the rats? 21:09:10 pikhq: Yes, indeed. 21:09:16 pikhq: Flash AV sync is still awful though. 21:09:39 pikhq: have you taken a look at ATS? it's a form of dependent types + linear types that allows raw memory access etc. safely in a strict-or-lazy functional/imperative language 21:09:43 http://www.ats-lang.org/ 21:09:51 performance and memory usage comparable to C/C++ 21:09:58 alise: The only trouble I've had with Flash's AV sync *recently* has been that every now and then it decides to completely omit the concept. 21:10:03 proper SMP multiprocessing too 21:10:04 pthreads-based 21:10:09 "Let's play a few seconds worth of audio in a few frames!" 21:10:17 ... Which is when I kill npviewer.bin. 21:11:44 http://en.wikipedia.org/wiki/The_Adventures_of_Lomax 21:11:47 anyone ever play this 21:11:52 lemmings spinoff 21:14:58 At some point, I'm just going to start forgetting languages to make room for new ones 21:15:03 (Ok, not really, but still) 21:16:12 hah i've forgotten more languages than you will ever learn 21:16:52 Should I learn ATS or Falcon? 21:16:58 (That was a joke question btw) 21:17:55 Statics don't use currying functions? 21:18:19 Also, they don't seem to stop to explain syntax 21:18:24 -!- zeotrope has quit (Ping timeout: 265 seconds). 21:18:28 I guess it's understandable enough though 21:18:39 http://en.wikipedia.org/wiki/ATS_(programming_language) 21:18:45 Sgeo, why bother? 21:19:07 http://en.wikipedia.org/wiki/ATS_(programming_language) has stuff :P 21:19:19 Phantom_Hoover, ..lolwhat? 21:19:19 Learning languages is boring if they use the same paradigm as something else you know. 21:19:25 Why.. bother learning a ... ah 21:19:35 Well, I have no previous exposure to static types 21:19:42 erm, dependent 21:20:04 -!- zeotrope has joined. 21:20:17 Also, maybe I'm misunderstanding something, but I can see ATS becoming a new favorite programming language 21:20:37 chris double is doing ats stuff right now http://www.bluishcoder.co.nz/ 21:20:49 take a look at their proven-to-return-a-sorted-permutation quicksort though 21:20:50 http://www.ats-lang.org/EXAMPLE/MISC/listquicksort_dats.html 21:20:51 gnarly! 21:21:16 but then it does build lists from scratch 21:23:02 Looking at ATS's syntax makes me feel uncomfortable. 21:23:12 meh, i don't mind it 21:23:14 Sgeo: there is a tutorial btw 21:23:17 http://www.ats-lang.org/TUTORIAL/tutorial.html 21:23:40 alise, that's what I'm looking at 21:23:47 It's not all that comprehendible 21:23:50 It's the punctuation prefixes, I think. 21:24:07 Where does it explain the difference between static and dynamic? 21:24:35 Sgeo: dunno 21:24:40 -!- Phantom_Hoover_ has joined. 21:25:24 Is [] existential quantification a syntax thing? 21:25:26 Sgeo, why not learn Coq if you want to do dependent types? 21:25:34 Or just an illustrative thing like >> in Smalltalk? 21:25:46 Phantom_Hoover_, because I also want something that's practical 21:26:55 Sgeo: ATS isn't really "practical". 21:27:03 Sgeo: Coq is practical. 21:27:16 It has been used to re-prove the four colour theorem; not easy. 21:27:26 It has also been used to create quite a few libraries that have been proved correct, 21:27:30 then extracted to Haskell, O'Caml or Scheme. 21:27:45 ATS is more for the actual programs, sure, but Coq is practical too, and ATS is quite research too. 21:27:46 alise, how about for, say, making a game? 21:27:50 alise, so can those functions be nonterminating? 21:28:07 Sgeo, well, if you want your game to be provably correct, then yes. 21:28:10 Phantom_Hoover_: no. well, you could probably model it. 21:28:14 you could probably model IO 21:28:18 and then do infinite stuff with that, too 21:28:19 -!- Phantom_Hoover has quit (Ping timeout: 265 seconds). 21:28:21 as one example 21:28:27 Sgeo: doing that in a formally verified way in ATS would be a gigantic impossible bitch 21:28:32 if you don't want to formally verify it ... why use these languages? 21:29:08 Sgeo: if you want to fall in love with a nice functional language, take a look at the (vapourware, but well-designed) http://merd.sourceforge.net/ :P 21:29:15 i'm not discouraging you learning ats, just your reasons 21:29:33 What about formally verifying _parts_ of the game? 21:29:47 you could write those parts in coq and extract them. it's not like they'd do any IO 21:29:54 (formally verifying SDL calls? that doesn't make any sense.) 21:29:59 ..extract? 21:30:04 yes. 21:30:18 with coq, you write functions and prove shit about them then extract them as a library to haskell, o'caml or scheme 21:30:34 which converts them (barely compilation, it's a quite direct conversion) to one of those languages 21:30:45 you write some wrappers, and then just plug it in to the rest of your program 21:30:49 ats is easier to write code in than coq though 21:30:50 alise, on that topic, what if your function uses nats, for instance? 21:30:50 a lot easier 21:31:01 Phantom_Hoover_: it extracts the data types you use 21:31:15 in this case it'd be peano-arithmetic nats, or you could probably do something to make it specialise to Int on extraction but i don't know how 21:31:28 alise, ah. 21:31:54 but uh clearly my lang is the best :) 21:31:57 i really like merd 21:32:00 even if it is shit 21:32:06 POOR 21:32:21 wat 21:32:26 * oerjan considers swatting alise 21:32:33 no, it actually is 21:32:34 named after that 21:33:24 alise, yes, which is why it's a poor pun. 21:33:39 Ok, static terms can be used in types? 21:33:45 painfully poorly punctuated puns 21:34:26 It's been on hold since 2003 21:34:32 Sgeo, static terms? 21:34:37 Merd 21:34:42 I assume that's ATS lingo? 21:34:43 Sgeo: it isn't actually vaporware though 21:34:45 there's an implementation 21:34:48 in ocaml 21:34:48 Or what? 21:34:51 it just doesn't do everything 21:34:55 and yeah, the project is dead 21:34:57 but it is hot 21:35:05 SEXY FUNCTIONAL LANGUAGES 21:35:06 it is teh shit 21:35:10 haskellxxx.com 21:35:22 Let me show you my Gonad typeclass. 21:35:40 That could be related to my SHOCKING TRUTH from yesterday. 21:36:04 wta 21:36:06 *wat 21:36:40 Alonzo Church Jr. and Curry's daughter? 21:36:45 ah 21:36:49 class Gonad g where type Gonad h => h; copulate :: g -> h -> IO () 21:37:03 or something 21:37:12 "type Gonad h => h" ;; i forget what this does 21:37:17 * oerjan doesn't actually know how type families work 21:37:18 it just asks for another gonad? 21:37:27 mutual gonadism 21:37:34 yeah that was the idea 21:38:16 class Gonad g where nruter :: g a -> a; dnib :: a -> (g a -> b) -> b 21:38:28 challenge: find a use 21:38:35 (these are not comonads, afaik) 21:38:45 i was going to ask about that 21:38:55 extend :: (w a -> b) -> w a -> w b 21:39:02 so with comonads, the result is still X b 21:39:05 whereas with mine the result is b 21:39:10 well nruter has the type of coreturn or whatever 21:39:14 yes 21:39:18 the only change is w b into b 21:39:21 mine are the direct opposite of monads 21:39:24 Well, there's no immediate way to construct a value of type g a. 21:39:27 i.e. replace "m a" with "a" and "a" with "g a" 21:39:30 Phantom_Hoover_: uhh 21:39:31 yes there is 21:39:34 dnib :: a -> (g a -> b) -> b 21:39:54 presumably x `dnib` nruter = x 21:40:07 alise, so x `dnib` id is more or less return? 21:40:25 seems so, yes 21:40:37 then nruter (x `dnib` id) = x, ofc 21:40:45 * alise renames them danoms, not gonads 21:40:48 since this is actually interesting :P 21:42:42 bind x f = (f (nruter x)) `dnib` id is bind, I think. 21:43:15 Actually, that dnib id mightn't be needed. 21:44:58 * Sgeo hahs at ATS's fix notation 21:46:21 No, it's not. 21:47:05 instance Danom Identity where 21:47:05 nruter (Identity x) = x 21:47:05 dnib x f = f (Identity x) 21:47:14 instance Danom ((,) a) where 21:47:15 nruter (a,b) = b 21:47:15 dnib x f = f (x,x) -- I do not think this one is very useful 21:48:10 can't have Danom [] 21:48:12 since nruter [] = ??? 21:48:24 Or Maybe, for that matter. 21:48:31 alise: erm dnib x f = f (x,x) is not the right type i think 21:48:32 * alise does it for streams 21:48:39 alise: which language are you talking about? 21:48:45 derdon: haskell, atm 21:48:46 derdon, Haskell. 21:48:47 the a in the instance is not the same as the a in the dnib type 21:48:47 oerjan: why not? 21:48:56 oh, touche 21:49:04 alise: ah, then I detected it correctly :) 21:49:12 dnib :: a -> ((a,c) -> b) -> b 21:49:20 alise: although Haskell is not really esoteric 21:49:22 no 21:49:28 (c,a) 21:49:28 derdon: but what we're doing is 21:49:33 oerjan: oh right 21:49:40 oerjan: well ... it's not entirely clear what to do at all, then :D 21:49:49 could you just specify like ()? 21:49:52 alise: I understand 21:49:53 or is it quantified in itself? 21:50:00 indeed that seems undefined, unless you use undefined 21:50:45 the c could be a specific type 21:50:47 data Stream a = SC a (Stream a) 21:50:47 adinf :: a -> Stream a 21:50:48 adinf x = SC x (adinf x) 21:50:48 instance Danom Stream where 21:50:48 nruter (SC x _) = x 21:50:48 dnib x f = f (adinf x) 21:50:55 not much interesting seems to happen in these 21:50:57 * alise wonders about Either 21:51:02 Ok, so there's #include, and then compilation 21:51:03 nope, can't do that 21:51:04 nruter 21:51:08 That bit seems like C/C++ 21:52:12 nruter (Left x) = x? 21:52:31 no, that's the wrong type 21:52:32 Although that implies instance Danom (Either a a) 21:52:41 it needs to be whatever is in Right 21:52:55 well or that 21:53:03 wait no 21:53:25 it's Danom (Either a) so you cannot fix it that way 21:53:25 hmm EIther a a would work 21:53:30 oerjan: you can 21:53:38 data BothEither a = Left a | Right a 21:53:56 well sure 21:54:09 but that's just an obscured (Bool, a) 21:54:13 (mostly) 21:54:19 Ok, ATS syntax gives me a headache 21:54:37 oerjan: good enough 21:54:43 Sgeo: you give my syntax a headache 21:55:10 dnib x f = f (Right x)? 21:55:12 oerjan: ah, but should it be f (BLeft x) or f (BRight x) :P 21:55:19 alise has syntax. Therefore, alise is a language. Therefore, I should learn alise. 21:55:37 Sgeo, learn Latin! 21:55:54 The syntax is like nothing else mainstream. 21:56:32 Syntax quidquid nullam altera monstrum 21:56:58 Syntax is like no other monster? 21:57:14 * oerjan has very little idea what he actually said 21:57:42 Sgeo: not in the biblical sense, i hope. 21:58:05 Isn't that just "know" in the biblical sense? 21:58:19 Maybe it's transitive to learning. 21:58:28 If you learn something, you know it. 22:00:45 and then you forget it 22:00:53 you can't unsex. 22:01:17 You can dnib. 22:01:57 egadnob 22:02:29 oerjan: i think we can conclude that danoms are useless 22:02:58 useless != not fun 22:03:03 alise, what relevance does that have? 22:03:12 I think everyone in this channel should know that 22:03:15 maybe a little too much like _both_ monads and comonads at the same time... 22:09:00 I seem to have gotten in a bit on an online argument 22:09:05 -!- oerjan has quit (Quit: Good night). 22:10:54 http://www.reddit.com/r/geek/comments/d3o6c/futurama_writer_created_and_proved_a_brand_new/c0xc7rm 22:15:33 I hope that's a troll, but I met a 13-year-old today who couldn't divide 6 by 3, so... 22:17:09 They didn't even come up with the conjecture 22:17:10 Does anyone why Coq uses .v for its file extension? 22:17:13 I rewatched the episode today 22:17:29 They didn't wonder "Well, given any possible mixup, is there a solution?" 22:17:34 Or anything along those lines 22:19:28 Phantom_Hoover_: because it's so _v_ erbose? 22:21:33 Mathnerd314: lemme guess, you like agda 22:21:53 Phantom_Hoover_: coq au Vin? :P 22:22:05 alise: no, just have used it more 22:24:28 -!- Phantom_Hoover has joined. 22:25:36 -!- Phantom_Hoover_ has quit (Read error: Connection reset by peer). 22:25:47 "No, they came up with a solution that works in all cases, as proven by the futurama guy. Stop being a dumbass. 22:25:47 " 22:26:54 wat 22:29:12 Sgeo, he's an idiot, and he's being overwhelmingly downvoted. Leave it. 22:31:39 "You are a pathetic person." 22:32:48 See? He knows he's wrong, so he ad homs. 22:39:08 If you have them all, you have seen the episode. Why are you acting like a helpless retard? 22:39:10 You'll notice that I said I haven't started watching the series yet. Having something and having seen it are two different things. Please don't resort to personal insults. 22:39:12 You are a personal insult for being a dumbass. 22:39:34 Sgeo: segoli is two removals and one swap away from sgeo! 22:41:00 Sgeo: insomniac84 is a known troll iirc 22:41:27 -!- sftp has quit (Read error: Connection reset by peer). 22:42:34 Well, now I have my doubts that insomniac84 has even seen the relevant episode 22:42:39 -!- sftp has joined. 22:54:24 -!- Phantom_Hoover_ has joined. 22:54:37 -!- Phantom_Hoover has quit (Read error: Connection reset by peer). 22:56:37 -!- tombom has quit (Ping timeout: 272 seconds). 23:03:49 a 23:04:09 -!- tombom has joined. 23:04:53 -!- tombom_ has joined. 23:05:28 -!- Phantom_Hoover_ has quit (Ping timeout: 265 seconds). 23:08:39 -!- tombom has quit (Ping timeout: 252 seconds). 23:08:49 -!- Phantom_Hoover_ has joined. 23:14:33 * Sgeo vaguely wonders if deja vu is dangerous 23:14:42 Erm, indication of something dangerous 23:18:15 Sgeo, no. 23:18:37 Everyone gets it throughout their life, so it's hardly abnormal. 23:20:14 But can lack of sleep make it worse? 23:20:20 And I think lack of sleep is dangerous 23:20:23 etc. 23:21:24 But then the deja vu is just a symptom. 23:22:02 Do you end up thinking wildly incoherent thoughts, like augur thinking he was a lambda term. 23:23:00 I'm not dejavuing right now, just tired 23:25:24 Hmm, what's your current obsession? 23:25:31 NetHack, right? 23:25:54 When you look in the mirror, do you see an @? 23:26:16 heh 23:26:50 Dammit Sgeo, this isn't a joke! 23:26:59 This is a matter of life or death! 23:27:16 As far as I can tell, I am not Hallu 23:27:24 Or polymorphed 23:27:33 Maybe you're hallucinating that you're not hallucinating! 23:28:02 Maybe this is a drea, 23:28:17 pikhq, do a reality check. 23:29:42 !coq Check reality. 23:31:36 reality 23:31:36 : I_have_no_idea 23:31:43 Phantom_Hoover_: wat 23:31:43 :P 23:31:56 pikhq: Music tagging adventures, part n: I have decided to simply elide "title" tags from untitled works. 23:32:38 Do you end up thinking wildly incoherent thoughts, like augur thinking he was a lambda term. ;; XD 23:33:02 alise: Hah. 23:33:07 Sgeo: ? 23:33:15 pikhq, I did it. 23:33:18 I think he meant Phantom_Hoover_. 23:33:32 pikhq: However, this is causing me to run into problems, as Quod Libet insists that such a track is actually titled "1.flac [Unknown]". 23:33:43 Well, if pikhq doesn't want to become lucid, he'll just drown in the raingutter 23:34:02 Trying Check reality. in a virgin environment: Error: The reference reality was not found in the current environment. 23:34:03 pikhq: Therefore, I think I will do "title=". 23:34:09 virgin environment! 23:36:21 sigh, title= doesn't work either 23:36:42 now it does 23:37:14 pikhq: technically, titling something the empty string isn't the same thing as not naming something, is it? 23:37:29 bürp 23:38:27 * Sgeo goes to read DCs say the darndest things 23:39:14 * Phantom_Hoover_ has come to love auto. 23:39:28 I can only assume it uses magic, or that I missed something. 23:39:52 auxto? 23:40:00 No, auto. 23:40:10 ah-ooh-to 23:40:21 auxto is oww-to 23:40:43 I /think/ it's one of Coq's built in tactics, but I think it's just something you type in after doing something to see if it completes the proof. 23:41:05 And I'd say "otto", but that's beside the point. 23:43:14 * Sgeo is just being an Esperanto nut 23:44:18 Sgeo, that's the worst kind of nut! 23:47:44 "then this slutty looking girl came up to me (her shirt didn't even cover her chest xP) and wanted me to follow her to have sex. ... Anyways, on the way to the closet, she was talking about all the STD's she had or something." 23:48:07 Sgeo, huh? 23:48:40 http://www.dreamviews.com/f28/dcs-say-darndest-things-19509/index69.html#post1486806 23:49:00 I can only assume it uses magic, or that I missed something. 23:49:01 no 23:49:03 I /think/ it's one of Coq's built in tactics, but I think it's just something you type in after doing something to see if it completes the proof. 23:49:04 no 23:49:11 it simply tries a bunch of common tactics 23:49:22 OBRING 23:49:24 like things that automatically prove simple arithmetic statements, things that prove things from datatype constructions 23:49:25 etc 23:50:23 Why can't it be MAGIC? 23:50:44 "Spock: [to me, raising an eyebrow] "...I am quite tasty, captain."" 23:51:28 "Well now what?" ;; hey look it's (maybe) augur 23:52:40 augur (\f -> (\x -> f (x x)) (\x -> f (x x)))