00:00:38 -!- cpressey has quit (Quit: Leaving.).
00:01:33 <scarf> botte: you convinced them in the end?
00:01:53 <botte> scarf: well, he didn't argue after i said that "dropping doesn't require ownership, right?" (along those lines)
00:01:59 <botte> probably there was typing lag
00:02:03 <botte> i.e. he hadn't read my request to drop when typing that
00:02:54 <botte> scarf: aargh, freenode doesn't allow + in emails
00:03:15 <scarf> gmail, you can put dots anywhere you like in the address
00:03:16 <botte> scarf: that only lets me punctuate with ., not add more text
00:03:17 <scarf> and it ignores them
00:03:27 <scarf> but it's good enough for address uniqueness
00:03:36 <botte> it appears to maybe allow +
00:03:38 <scarf> (bonus points if you come up with an address that punctuates both ways round)
00:03:40 <botte> perhaps it doesn't like my sha1 password
00:03:50 <scarf> use the first half, it's almost as secure
00:05:12 <scarf> oh, the "any password should be allowed" theory?
00:05:36 <botte> 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 <scarf> botte: it may be on the /input/ side that's the problem
00:05:57 <scarf> auto-ID might not work properly in many clients if the password was too long
00:06:21 <Ilari> 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 <scarf> I'd certainly expect passwords with spaces in to be rejected in IRC due to screwing up argument parsing
00:06:41 <scarf> Ilari: nah, nobody will migrate anyway
00:06:50 <scarf> they'll just NAT entire countries or something stupid like that
00:06:56 <botte> i was about to say, yeah, nat
00:07:20 <scarf> (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 <scarf> (it caused a huge row when Wikipedia blocked the IP for vandalism, not realising its significance)
00:07:38 <scarf> (and it was undone as soon as somebody noticed)
00:07:56 <botte> Qatar; the defier of usual English spelling, owner (well, royal family) of Harrods, and hater of IPs
00:08:49 <scarf> 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 <botte> a lot of them even forbid that.
00:09:20 <botte> 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 <botte> (static IP, IPv6, only intelligent people, etc.)
00:09:49 <pikhq> scarf: s/will// s/'ll// s/give/gives/
00:10:08 <botte> a bit on the pricy side though
00:10:13 <botte> (very on the pricy side)
00:10:15 <botte> moreso than last time
00:10:23 <pikhq> Some ISPs are already in the habbit of doing mass-NAT.
00:11:31 <scarf> which was especially strange as each account had its own IP anyway
00:11:34 <botte> i don't think anyone actually uses aol any more :P
00:11:41 <scarf> (you can tell they did due to the XFF headers)
00:11:59 <scarf> alise: do you have an opinion on Oracle vs. Google, btw?
00:11:59 <botte> wow, Time Warner split up with AOL
00:12:11 <botte> scarf: only that it's inane and oracle suck
00:12:21 <botte> (I don't actually know much about the suit, just that oracle are pretty much universally inane and idiotic)
00:12:27 <scarf> also, netscape.com still exists
00:12:37 <scarf> although nowadays it's AOL.com + netscape branding
00:12:37 <botte> that doesn't surprise me.
00:13:32 <scarf> I've been looking at the lawsuit
00:14:05 <scarf> 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 <botte> all technology patents are dubious
00:14:28 <botte> even by the standard of patents
00:14:30 <botte> technology = software
00:14:40 <botte> software patents specifically
00:14:46 <botte> but, you know, computer patents that aren't to do with chips
00:15:55 -!- augur has joined.
00:16:12 <Vonlebio> botte, are you becoming Thribb?
00:16:16 <scarf> the only potentially legitimate claim, other than software infringements, I think Oracle have is trademark infringement
00:16:19 <scarf> but they didn't file that one
00:16:33 <botte> Vonlebio: verily, I
00:16:38 <scarf> (I think they might legitimately be able to get an injunction against Google advertising materials claiming that Android is based on Java)
00:16:49 <botte> that i didn't knowit.
00:17:48 <botte> I defy all conventions of poetry and hereby sign my suicide note. -J
00:19:16 <botte> scarf: ugh, it /was/ a password length limit
00:19:17 <scarf> that is indeed, in a sense, poetry
00:19:30 <botte> Blank verse is easier than rhyming
00:19:33 <Vonlebio> Oh, look, the Agda people have an article on Agda vs Coq.
00:19:33 <botte> For there's no need to worry of timing.
00:19:37 <botte> The problem, you see, with blank verse, to me,
00:19:43 <Vonlebio> Their first argument is that Agda has nicer syntax.
00:19:44 <botte> is that it's just an excuse for people to write prose and call it poetry.
00:19:52 <botte> Vonlebio: They're wrong.
00:19:58 <botte> I mean, sure, nicer to look at (unless you read the stdlib -- hideous)
00:20:02 <botte> not nicer to write.
00:20:20 <scarf> non-exhaustive list of words "poetry" is not an angram of: pottery, topiary, temporary, zoetrope
00:20:38 <Vonlebio> Then something to do with writing programs in Emacs.
00:20:54 <Vonlebio> They admit that they have no tactic system, though.
00:21:29 <botte> Addendum to the non-exhaustive lists of words "poetry" is not an anagram of: pig, ontological, metaphorically, understoodingness
00:22:09 <Vonlebio> Oh, and they say that Agda is easier to learn.
00:22:15 <scarf> at least "metaphorically" contains all the letters "poetry" does
00:22:28 <botte> it just looks superficially similar to haskell
00:22:57 <scarf> hmm, "origasm" looks so much like it's a word
00:23:05 <Vonlebio> Perhaps you would just like to dismiss them all at once.
00:23:06 <Vonlebio> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVsCoq
00:23:20 <botte> Urban Dictionary: origasm
00:23:20 <botte> the sexual pleasure that one gets from either making or admiring origami.
00:23:20 <botte> www.urbandictionary.com/define.php?term=origasm - Cached - Similar
00:23:22 <scarf> it's a wiki? just edit them to be correct
00:23:23 <botte> That .. was what I had predicted.
00:23:34 <botte> Vonlebio: They're wrong and Agda users smell funny.
00:24:21 -!- zeotrope has joined.
00:24:22 <botte> 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 <scarf> I haven't used either
00:24:30 <botte> Coq can be predicative or impredicative; by default predicative.
00:24:40 <botte> Coq does support mutual definitions; perhaps not in the way the wiki means.
00:24:43 <Vonlebio> Agda might just maybe be good for pointless mucking about with dependent types.
00:24:52 <scarf> zeotrope: how can you join after I said "zoetrope" not more than 5 minutes earlier?
00:24:55 <botte> Coq's pattern matching is a hassle because it does proper dependent pattern matching; Agda does not.
00:25:04 <botte> Set Implicit Arguments is nicer.
00:25:14 <botte> Safety belts, aka "easy ways to get an inconsistent system".
00:25:25 <botte> Non-fixed system, aka "we're totally awesome and unstable"!
00:25:33 <botte> Less is more: because dependent proving is hard.
00:25:38 <botte> (It really is. So you need more.)
00:25:52 <botte> 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:26:00 <botte> Vonlebio: There you go; done.
00:26:11 <botte> Agda is interesting as a research project; nothing more.
00:26:26 <scarf> botte: what about proving via causing programs to type correctly in Haskell / some other language with type inference?
00:26:56 <scarf> 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 <botte> scarf: that's how proofs work in every dependently typed language. except you don't use inference much
00:27:05 <scarf> and claim this as some sort of achievement
00:27:20 -!- augur has quit (Ping timeout: 265 seconds).
00:27:36 <scarf> botte: saves time over writing the whole proof out by hand
00:27:51 -!- tombom has quit (Quit: Leaving).
00:28:20 <botte> my favourite tactics in Coq are "auto with arith", "trivial" and "omega"
00:28:26 <botte> type one in, press ., hope for the best
00:29:06 <Vonlebio> scarf, why did you realise that?
00:29:40 <scarf> scarf: because the people who do that sort of thing keep turning up at my department and giving seminars
00:29:55 <botte> what a strange tabcompleteo
00:30:02 * scarf wonders what sort of confusion is needed to successfully nickping /yourself/
00:30:07 <botte> (completo: like a typo, but for tab complete)
00:30:13 <botte> Vorpal: I realised that because...
00:30:24 <scarf> Vonlebio: yes, srsly
00:30:52 <scarf> it's mostly people from Microsoft Research
00:31:05 <scarf> who use C# and F#, and do something that either seems trivially easy, or makes no sense
00:31:23 <Vonlebio> Saying "we have invented a calculus that uses only anonymous functions, often called lambdas."
00:31:31 <scarf> 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 <scarf> Vonlebio: not quite that basic
00:31:42 <botte> "Hahaha. HAHAHA! HAHAHAHAHAHAHA!"
00:31:50 <botte> "What?" "You're stupid."
00:31:51 <scarf> Vonlebio: I can't remember the basis
00:31:59 <botte> "I..." "I KNOW STEPHEN WOLFRAM. PERSONALLY."
00:32:27 <scarf> hmm, do you know System-C?
00:32:28 <Vonlebio> I AM THE LOVE CHILD OF ALONZO CHURCH JR AND HASKELL CURRY'S DAUGHTER!
00:32:44 <Vonlebio> Fun fact: they supposedly dated.
00:32:51 <scarf> imagine you've invented a language
00:33:01 <Vonlebio> scarf, is it a typed lambda calculus, like System F?
00:33:02 <botte> Vonlebio: i refuse to believe
00:33:03 <botte> but i want to believe
00:33:12 <scarf> but instead of writing a parser, you instead ask people to build a parse tree at runtime in some other language
00:33:16 <scarf> Vonlebio: no, completely different
00:33:30 <coppro> he's gone from 7 to 27
00:33:44 <scarf> so, instead of having a language where you write a:=b+c
00:33:59 * Vorpal is now known as cravat
00:34:02 <scarf> you write, say, variable(a)->assign(variable(b)->add(variable(c)))
00:34:18 <scarf> and all does is builds a parsetree for later execusion
00:34:22 <Vonlebio> botte, http://importantshock.wordpress.com/2007/08/21/haskell-curry-yes-i-dated-his-daughter/
00:34:50 <botte> scarf: screw it, I'm supporting arbitrary nicks
00:35:02 <botte> http://pastie.org/1105138.txt?key=nsqexkxchx4ofd14wv3v4g
00:35:13 <scarf> 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 <botte> pastie.org/1105138.txt?key=nsqexkxchx4ofd14wv3v4g
00:35:26 <scarf> System-C is a VHDL-alike using C++ as the host lang
00:35:30 <Vonlebio> So, noöne talking at the moment uses the nick they used a month ago.
00:35:33 <botte> warning: Incredibly gnarly Python code! Only click if you're in to that sort of thing!
00:35:38 <botte> Vonlebio: this is just to register it
00:35:41 <scarf> the person in the seminar was doing something similar with CUDA and C#
00:35:43 <Vonlebio> scarf, oh, I think I heard of that.
00:35:44 -!- botte has changed nick to alise.
00:35:45 <pikhq> scarf: So, Pain + Agony.
00:35:53 <alise> <scarf> System-C is a VHDL-alike using C++ as the host lang
00:35:55 <scarf> and I remembered the comment I was laughing at
00:36:03 <scarf> well, maybe not the /worst/, but pretty bad
00:36:18 <scarf> it was something about this mechanism making the language more scalable
00:36:38 <scarf> which struck me as a slightly bold statement, given that all the loops used were inherently unrolled
00:36:53 <scarf> (as they were using a normal C# loop around the parsetree-builder_
00:36:55 <Vorpal> <scarf> System-C is a VHDL-alike using C++ as the host lang <-- I thought it was closed to Verilog than VHDL?
00:37:13 <alise> Vorpal: same thing
00:37:27 <scarf> Vorpal: VHDL and Verilog are identical apart from the syntax, for all practical purposes
00:37:42 <scarf> thus, "VHDL with different syntax" and "Verilog with different syntax" are basically the same concept
00:38:12 <Vorpal> scarf, I thought verilog lacked assignments outside processes or something like that?
00:38:20 <Vorpal> of course in practise you would get the same code...
00:38:25 <Vonlebio> Vorpal, hardly a big difference.
00:38:30 <scarf> the concept doesn't actually make sense
00:38:44 <Vorpal> scarf, no? You can write sig_out <= a or b; iir c?
00:38:45 <scarf> (you can <= outside processes in VHDL, but that's just sugar, effectively)
00:38:52 <Vorpal> 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 <scarf> s <= a or b; is sugar for begin process (a, b) s <= a or b end process
00:39:29 <scarf> (+ filling in the bits of syntax I missed out because nobody can be expected to /remember/ VHDL syntax)
00:39:38 <scarf> time to go home, anyway
00:39:43 -!- scarf has quit (Quit: Page closed).
00:42:16 -!- sshc has quit (Ping timeout: 252 seconds).
00:42:34 <alise> what's the name for a raw line of IRC text?
00:42:39 <alise> including all the syntax
00:45:56 -!- Wamanuz has quit (Remote host closed the connection).
00:48:15 <Sgeo> Congratulations alise, my current obsession is NetHack
00:48:31 <alise> 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 <Sgeo> alise, if something wasn't good, would I be obsessed?
01:07:38 <Sgeo> alise, are you still interested in NetHack?
01:07:43 <Sgeo> Or have you moved on?
01:10:40 <alise> Sgeo: I'm interested but taking a break.
01:29:24 <alise> Apparently the prefix of an IRC message is optional.
01:35:52 <pikhq> ... There exists opposition to water flouridation?
01:36:31 <pikhq> What's next, opposition to cleanliness in hospitals?
01:38:44 <pikhq> Seriously, why the hell doesn't Europe do water flouridation?
01:38:49 <Sgeo> I oppose the use of running water!
01:39:03 <pikhq> Sgeo: That's great. I'll be sure to shit upstream of you.
01:39:14 <alise> doesn't flouride worsen the taste?
01:39:20 <pikhq> alise: No, it's flavorless.
01:39:43 <alise> http://www.aquaverve.com/blog/content/binary/fluoride_water_main_600[1].jpg ;; lol wat
01:39:43 <coppro> yeah, fluoridation is pretty much awesome
01:39:43 <pikhq> Also, sl/flourid/fluorid/g
01:39:48 <pikhq> s/flourid/fluorid/g
01:39:56 <alise> i approve of adding flour to the water supply
01:40:19 <alise> 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 <alise> We do it here in the UK, I'm pretty sure.
01:40:40 <pikhq> alise: Only 10% of the population of the UK has fluoridated water.
01:40:59 <coppro> fluoridation in water supply is typically only a few ppm
01:41:00 <alise> I know that the water supply in the UK, taste-wise, varies from acceptable to yucky
01:41:08 <alise> coppro: oh, I know that, it's just the principle of the thing
01:41:18 <alise> I'd only object to fluoride as part of a wider "pure tap water" position
01:41:26 <pikhq> Only a few countries actually do water fluoridisation commonly.
01:41:29 <alise> & i know that fluoride is a Very Good Thing for teeth
01:41:40 <coppro> typically less than an order of magnitude more concentrated than ocean water
01:41:51 <pikhq> (US, Canada, Ireland, Australia... Also, France does *salt* fluoridisation.)
01:42:06 <coppro> at those levels, it's actually almost irrelevent except for the teeth of the young
01:42:16 <alise> i use a fluoridic (word?) toothpaste anyway
01:42:36 <alise> http://upload.wikimedia.org/wikipedia/commons/5/5d/Unholy_three_cropped.png
01:42:39 <coppro> as do I, plus I get a topical fluoride treatment twice a year
01:42:41 <pikhq> coppro: Which is itself fairly beneficial.
01:42:45 <alise> FLUORIDATED WATER, POLIO MONKEY SERUMS, MENTAL HYGIENE ETC.
01:42:57 <alise> <coppro> as do I, plus I get a topical fluoride treatment twice a year ;; why?
01:43:04 <alise> that seems excessive.
01:43:28 <pikhq> alise: It's a fairly routine thing; you're probably just not aware that there's topical fluoride being done.
01:43:49 <alise> what, you mean it's done in my sleep? :)
01:44:09 <pikhq> No... It's just not pointed out that it's topical application of fluoride.
01:44:26 <alise> you mean as part of a regular dentist's appointment?
01:44:58 <alise> 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 <alise> perhaps i just have teeth that make dentists unusually satisfied
01:45:49 <coppro> alise: you must not see a hygenist then
01:46:02 <Sgeo> alise, someone in #nethack wants your help
01:46:20 <coppro> here, anyways, hygenists typically work with dentists and you get the appointments one right after the other
01:46:28 <coppro> though if you have special concerns you can see either separately
01:46:35 <Sgeo> <Zarakava> any way to pacify watchmen in minetown?
01:46:35 <Sgeo> <Zarakava> I had to kick open the exit door...
01:46:41 <alise> coppro: I'm not sure that's actually common in the UK.
01:46:42 <coppro> I had a hygenist appointment yesterday because I'd had my braces off recently
01:48:41 <alise> I have a tooth that didn't go into place *awesome*
01:48:57 <alise> I should, uh, probably get one of the teeth next to it removed so it can do its dropping thang.
01:49:02 <alise> But it's been like this for, what, years now.
01:49:23 <coppro> see a dentist/orthodondist
01:49:42 <Sgeo> I should probably do that
01:49:46 <Sgeo> My teeth are all weird
01:49:47 <alise> 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 <alise> but they said there wasn't any actual badness about it apart from the look
01:49:59 <coppro> does the NHS cover either?
01:50:38 <alise> i'm not actually sure, I forget the situation wrt dentistry in the uk
01:50:47 <alise> but there's no cost issue or anything
01:51:33 <alise> coppro: do you know much about the irc spec?
01:53:22 <alise> coppro: will a server ever send a PRIVMSG?
01:53:25 <coppro> 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 <coppro> alise: I don't believe so
01:53:56 <alise> python exceptions can be irritating
01:54:07 <alise> like I don't want to create a YouCantPRIVMSGAServer exception, that's ridiculous
01:54:09 <pikhq> coppro: Clearly, we should implement a world fluoride policy.
01:54:13 <alise> but "IRCError" or something is ludicrously vague
01:54:32 <coppro> http://upload.wikimedia.org/wikipedia/commons/thumb/f/fb/FluorideTrays07-05-05.jpg/800px-FluorideTrays07-05-05.jpg
01:58:05 <Sgeo> I like Vala's system
01:58:15 <Sgeo> for exceptions
01:58:27 <alise> coppro: Gah, I use both "origin" and "sender" to mean the same thing here. :-D
01:58:45 <Sgeo> Would probably be something like IRCError.YOU_CANT_PRIVMSG_A_SERVER
01:59:07 <Sgeo> I might have a mistaken impression of Vala exceptions
01:59:26 <alise> exception @[Can't PRIVMSG a server]
01:59:32 <alise> later: raise @[Can't PRIVMSG a server]
01:59:52 <alise> exception @[division by zero]
01:59:52 <coppro> I like the system of exceptions whereby you realise that things like trying to privmsg a server shouldn't be exceptions
01:59:54 <alise> in the division code
01:59:58 <alise> raise @[division by zero]
02:00:01 <alise> coppro: Then what should it be?
02:00:37 <Sgeo> an assertion that means there's a bug in the code?
02:00:48 <Sgeo> Vala does things that way, actually)
02:01:09 <alise> "oops you did something retarded lol" is a type of exception
02:01:12 <coppro> imo, an exception should be two things a) exceptional b) not capable of being handled at the error site
02:01:27 <alise> assertions are just exceptions with bad error messages
02:01:40 <Sgeo> alise, not in Vala
02:03:34 <alise> coppro: tell me off for mixing origin and sender
02:03:39 <alise> that is, "origin" and "sender"
02:04:19 <alise> 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:05:56 * Sgeo considers trying DCSS
02:06:06 <alise> Sgeo: the map moves to keep you in the centre
02:06:08 <alise> gives me a headache
02:09:50 <alise> coppro: Got a better idea?
02:11:04 <Sgeo> alise, coppro left
02:11:33 <Sgeo> You should become a regular in ##nomic
02:12:03 <Sgeo> I'm thinking of holding office again
02:12:26 <alise> 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 <Sgeo> Is that asshole even active anymore?
02:13:16 * Sgeo can't believe he just said "asshole"
02:17:40 <Sgeo> http://www.youtube.com/watch?v=V0W7Jbc_Vhw
02:17:53 <Sgeo> alise, waitwhat?
02:18:26 <alise> Sgeo: Waitwhat how?
02:18:37 <Sgeo> How is Wooble an asshole?
02:18:50 <alise> Umm, he's a complete and utter jerk who makes regular slights at comex and me?
02:18:59 <alise> And votes against proposals for their author? And ...
02:19:06 <alise> He's an asshole because he's an asshole.
02:19:10 <alise> And also because of what he did wrt ##nomic.
02:19:38 -!- alise has changed nick to botte.
02:21:43 <botte> -NickServ- Metadata : ^ = ^
02:21:49 <botte> /msg nickserv set property foo bar
02:21:51 -!- botte has changed nick to alise.
02:26:02 <Sgeo> So I should feel a bit weird about him helping me massively wrt NetHack?
02:31:18 <Sgeo> Ok, wtf is going on with flappy?
02:36:38 <alise> botte's infrastructure progresses
02:37:26 <Sgeo> What language?
02:37:45 * pikhq can has a decent FLAC to M4A conversion script. Whoo.
02:37:48 <alise> python, it's sufficiently boring
02:38:34 <alise> pikhq: *to AAC/MPEG-4 Part 14
02:38:44 <alise> pikhq: .m4a is an Apple invention for "MPEG-4 Part 14 that's just audio".
02:38:57 <pikhq> alise: Yeah, yeah...
02:39:06 <alise> pikhq: I suggest .aac, if .mp4 is too vague for you :P
02:39:23 <alise> Meanwhile, http://i.imgur.com/v9M60.jpg
02:39:26 <pikhq> alise: .aac convinces certain tools that what's inside is a raw AAC bitstream.
02:43:43 -!- sshc_ has changed nick to sshc.
03:22:06 -!- comex has joined.
03:32:03 -!- zzo38 has joined.
03:32:08 <zzo38> Why am I out of permission?
03:32:12 <zzo38> Are you upgrading something?
03:33:59 <zzo38> Or did I put in some word in my file which is censored?
03:34:57 <zzo38> 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 <Sgeo> alise, be prepared to have an aneurseum
03:37:29 <Sgeo> You know what I _think_ may have introduced me to NetHack?
03:37:39 <zzo38> I think "<DIV" is forbidden.
03:40:07 <zzo38> Maybe you should make it that any forbidden words are not forbidden for autoconfirmed users.
03:40:43 <alise> zzo38: spambots can wait until registration completes before attacking
03:40:46 <alise> anyway, it's not in my power
03:40:54 <Sgeo> alise, User Friendly
03:47:02 <zzo38> Ha ha I inserted a <DIV> tag anyways!
03:47:26 <zzo38> http://esoteric.voxelperfect.net/wiki/User:Zzo38
03:47:33 <zzo38> (See near the bottom, the blue part)
03:50:17 -!- nooga has quit (Read error: Operation timed out).
03:50:26 <Sgeo> Wait, you actually used my BF-equivalent for one of your languages?
03:50:55 <zzo38> Sgeo: Please elaborate on what you mean?
03:51:04 <Sgeo> GrainFimple uses BF-RLE
03:51:47 <zzo38> Now can you see that the spam filter doesn't prevent anyone from inserting a <DIV> tag anyways?
03:52:25 <Sgeo> <DIV 02:45, 21 August 2010 (UTC) style="background-color:blue;color:white">
03:52:29 <Sgeo> Seems a bit broken up
03:52:40 <Sgeo> Although I guess that may be deliberate
03:53:03 <zzo38> Yes, but if you view the generated HTML code, it doesn't contain the date.
03:53:06 -!- nooga has joined.
03:53:17 <nooga> alise: go to sleep
03:55:29 * Sgeo zaps alise with a /oSleep
04:04:23 -!- augur has joined.
04:11:12 <augur> no, dont answer that
04:15:06 -!- nooga has quit (Ping timeout: 252 seconds).
04:18:16 <Sgeo> because having a weird sleep cycle can be a living hell sometimes
04:22:06 <alise> birthday on sunday, fwiw.
04:25:43 -!- Mathnerd314 has quit (Ping timeout: 260 seconds).
04:46:48 <Sgeo> 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:24:01 -!- alise has quit (Quit: Leaving).
06:16:06 -!- oerjan has joined.
07:10:11 <oerjan> !haskell foldl1 (\x -> x + 2*y) [1,1,1,1,1,1,1,1,1]
07:11:38 <oerjan> !haskell main = print $ foldl1 (\x -> 2*x + y) [1,1,1,1,1,1,1,1,1]
07:12:01 <oerjan> !haskell main = print $ foldl1 (\x y -> 2*x + y) [1,1,1,1,1,1,1,1,1]
07:12:27 <oerjan> !haskell main = print $ foldl1 (\x y -> 2*x + y) [1,1,1,1,1,1,1,1]
07:12:47 <oerjan> !haskell main = print $ foldl1 (\x y -> 5*x + y) [1,1,1,1]
07:13:04 <oerjan> !haskell main = print $ foldl1 (\x y -> 3*x + y) [1,1,1,1,1]
07:18:59 <EgoBot> 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 <oerjan> !bf >+>+>+>+>+>+>+>+<[>[-<++>]<<]>#
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 <Gregor> "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 <Sgeo> Some people's entire lives are post-2000
08:17:36 <Gregor> Yes, namely people who are 10 years and 8 months old or younger.
08:17:47 <Gregor> 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 <Vorpal> <Gregor> Most such people are not currently PhD students though :P <-- XD
10:08:29 <Gregor> I'm sure it's not "all"
10:08:44 <Vorpal> Gregor, really? Citation needed then.
10:12:13 <Gregor> 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 <Sgeo> My parents didn't want me skipping a grade due to social concerns :(
10:12:20 <Sgeo> I don't think skipping 1 grade is as severe as that
10:15:48 <Vorpal> 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.
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:17:12 <Vorpal> Phantom_Hoover, that looks like it would break if you exceed the number of elements there
15:17:27 <Vorpal> Phantom_Hoover, what a horrible back
15:17:36 <Phantom_Hoover> Tuples are only defined to a finite number of elements.
15:17:54 <Vorpal> 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 <Vorpal> sure it must be finite
15:18:04 <Vorpal> but it can be finite of any size you want
15:18:37 <oerjan> i vaguely recall the report says only tuples up to 15 elements are guaranteed to exist
15:19:17 <oerjan> and for actual class instances and supporting functions, even less.
15:19:20 <Phantom_Hoover> (,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,) seems to be as far as GHC goes.
15:19:47 <oerjan> !haskell length "(,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,)"
15:19:48 <Vorpal> 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:20:15 <Phantom_Hoover> Frankly, if you need more than 61 elements in a tuple, you're doing something wrong.
15:20:25 <Vorpal> Phantom_Hoover, well yeah
15:20:28 <oerjan> !haskell (True, True, True, True, True, True, True, True, True, False, True, True, True, True, True)
15:20:29 <EgoBot> (True,True,True,True,True,True,True,True,True,False,True,True,True,True,True)
15:20:46 <oerjan> hm maybe instances are up to 15 then.
15:20:51 <Vorpal> Phantom_Hoover, still it seems like a pointlessly arbitrary limit
15:21:16 <oerjan> Vorpal: i don't think it's _forbidden_ for implementations to support more
15:21:20 <Vorpal> Phantom_Hoover, well, limiting it by memory would be less arbitrary
15:21:32 <Vorpal> oerjan, yeah pointlessly arbitrary limit
15:21:51 <Vorpal> Phantom_Hoover, hm. How so?
15:22:00 <oerjan> Vorpal: oh i think it may be a limit for _all_ algebraic datatypes, possibly
15:23:33 <EgoBot> data (,,,) a b c d = (,,,) a b c d -- Defined in Data.Tuple
15:23:51 <oerjan> Vorpal: as in, ghc may only leave that many bits for telling the GC how long a datatype is
15:24:06 <Vorpal> 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:25:01 <oerjan> but then it _does_ have arrays...
15:25:42 <Vorpal> requires same data type for all elements though
15:26:20 -!- Phantom_Hoover_ has joined.
15:26:38 <Phantom_Hoover_> Vorpal, with algebraic data types you can have different types in an array.
15:26:41 <Vorpal> of course you could create some CharOrBoolOrWhatever type that "wraps" all the alternatives
15:27:12 <Vorpal> Phantom_Hoover_, eh? Are you not talking about [] lists or are you talking about some ghc extension to haskell?
15:27:19 <Vorpal> or did I miss out something huge
15:27:29 <oerjan> arrays are not [] lists
15:28:56 <oerjan> [] lists are linked lists, so any limit for size of a single constructor value does not apply.
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 <oerjan> while Arrays would presumably be actually consecutive in memory
15:30:08 <Vorpal> hm you could construct a linked list type where the type varied cyclically
15:30:25 -!- Sgeo has changed nick to Jabberwock.
15:30:35 -!- Jabberwock has changed nick to Sgeo.
15:30:42 <oerjan> any finite state automaton / regular expression could probably be used
15:31:02 <Vorpal> Sgeo, lucky for you ;P
15:32:03 <oerjan> also Arrays are Haskell 98 not an extension, i believe, although only immutable ones
15:32:47 -!- relet has joined.
15:33:31 <oerjan> 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 <Vorpal> 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 <Vorpal> in which case there are more efficient ways to do it
15:48:19 <Vorpal> (unless, of course, they are sparse arrays)
15:49:27 <oerjan> dammit the source links in the ghc library documentation are broken
15:49:37 <oerjan> so i cannot give you a precise answer :D
15:49:58 <Vorpal> oerjan, and you don't happen to remember?
15:50:17 <oerjan> well i'm pretty sure it's something based on consecutive values in memory
15:52:01 <Vorpal> oerjan, that would probably require special support from ghc
15:52:07 <Vorpal> as in, can't be pure haskell
15:52:34 -!- alise has joined.
15:52:59 <oerjan> dammit the source link is broken on hackage too
15:54:01 <oerjan> i'm trying to find the type definition
15:54:45 <oerjan> Vorpal was asking how ghc implements such a type, since you cannot define that directly in haskell
15:55:17 <oerjan> i am guessing it's either something ghc-specific or a wrapped C array of some sort
15:55:44 <oerjan> (directly as consecutive values in memory, that is)
15:56:39 <alise> 07:21:32 <Vorpal> oerjan, yeah pointlessly arbitrary limit
15:56:40 <alise> 07:21:34 <Vorpal> as I said
15:56:47 <alise> supporting all of them would require an infinite amount of code
15:56:50 <alise> or special compiler support
15:57:04 <alise> so it's not "pointlessly arbitrary", it's just the only sane thing to do
15:57:35 <Sgeo> alise, do IBMgraphics work for you?
15:57:44 <alise> Sgeo: only if i convert the character set
15:58:06 <alise> the only reason to is to get the upper half integral fountains :) and iirc the rogue level is screwy with them
15:58:38 <Sgeo> The halls are kind of nice
15:58:45 <oerjan> http://www.haskell.org/ghc/docs/6.12.2/html/libraries/base-4.2.0.1/src/GHC-Arr.html
15:58:48 <Sgeo> I like the DECgraphics doors better though, I think
15:58:51 <alise> Sgeo: install "konwert"
15:58:55 <alise> nethack | konwert cp437-utf8
15:59:07 <alise> the other solution doesn't work as far as i can tell
15:59:09 <Sgeo> Or, I could just have PuTTY set up to do cp437
15:59:28 <oerjan> Vorpal: it seems to wrap an Array# type, probably a ghc builtin?
15:59:33 <alise> oh, i forgot, you use an OS which actually supports that horrid character set.
15:59:42 <oerjan> the # types tend to be
16:00:10 <Sgeo> 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 <alise> for the DOS port, duh
16:00:28 <Sgeo> Or by "IBM" do they mean DOS/Windows.. ah
16:00:41 <alise> it's the IBM PC glyph set
16:00:48 <alise> from the original IBM PC
16:02:16 <alise> so julien assange has been accused of rape!
16:02:28 <alise> the cia are pretty good
16:05:58 <Sgeo> Is there any way to have Gmail show the current time?
16:06:04 <Sgeo> And also to have it use UTC
16:14:45 <alise> Sgeo: yes, look at the bottom-right corner of the screen
16:14:57 <alise> now you can read the time while using gmail
16:15:00 <Sgeo> My system clock is not in UTC
16:15:07 <alise> get another clock program
16:16:11 <alise> oh no running programs on my computer !!
16:20:22 -!- augur has joined.
16:21:14 <alise> "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 <Sgeo> My math teacher lied to me!
16:23:46 <alise> Oh gosh how horrific, what did she say.
16:23:52 <Sgeo> She said 2+2=4
16:24:35 <oerjan> ...and Sgeo finally snaps completely.
16:24:45 <alise> 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 <oerjan> just blame it on the logarithms
16:36:53 -!- augur has quit (Ping timeout: 265 seconds).
16:37:35 <alise> wait, how did it do that
16:37:48 <alise> which sounds a lot harder than multiplication to me
16:38:04 <alise> indeed even with log2 it'd have to do ^2 which is pretty clearly easiest implemented as a multiplication
16:38:48 <alise> er wait, e^ or 2^ ofc
16:47:05 <oerjan> "The secret to the LOCI was Dr. Wang's magical logarithm calculating circuit."
16:47:20 <oerjan> "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:36 <alise> lol anti-logarithms
16:47:42 -!- wareya has quit (Read error: Connection reset by peer).
16:47:56 <alise> well, it might have only done base 10.
16:48:46 -!- wareya has joined.
16:51:58 <oerjan> "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:43 <alise> http://www.oldcalculatormuseum.com/wangloci.html
16:52:48 <alise> wow it's beautiful
16:52:56 <oerjan> that's what i'm looking at
16:53:10 <alise> no integrated circuits
16:55:01 <Sgeo> Maybe I should implement it in AW
17:00:19 <oerjan> "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 <oerjan> good luck implementing that
17:00:37 <alise> emulate the circuits directly :)
17:01:50 <alise> oerjan: "Wang calculators cost in the mid-four-figures"
17:02:09 <alise> 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 <alise> "Swedish rape warrant for Wikileaks' Assange cancelled"
17:05:32 <alise> http://www.bbc.co.uk/news/world-europe-11049316
17:14:21 <Phantom_Hoover> alise, incidentally, is Agda actually good for anything?
17:16:30 <alise> it's a research project :P
17:17:42 <alise> programming "actual programs" with some dependent typing, maybe
17:17:46 <alise> coq is the best for that
17:17:57 <alise> you can write libraries + proofs that they work, then export this code to O'Caml or Haskell
17:18:11 <alise> yes, it actually spits out almost-identical datatypes and codes for the non-proof portions
17:18:20 <alise> this is known as Awesome.
17:18:21 <Phantom_Hoover> Wait, the WP article is called "Agda (theorem prover".
17:18:33 <alise> Agda (theorem prover), the programming language and theorem prover
17:18:33 <alise> Agda (Golgafrinchan), the character in The Hitchhiker's Guide to the Galaxy by Douglas Adams
17:18:33 <alise> Agda (Bishop) ( –1024), the Roman catholic bishop of Oviedo
17:18:47 <alise> Phantom_Hoover: anyway, yeah, Coq extraction: fucking awesome or amazingly fucking awesome???
17:19:25 <Phantom_Hoover> "Per Martin-Löf is an enthusiastic bird-watcher, whose first scientific publication was on the mortality rates of ringed birds."
17:19:25 <alise> Phantom_Hoover: write a coq function to do something
17:19:33 <alise> Extraction that_function.
17:19:48 <alise> even if it invokes proofs which other functions require, these will be elided in the extraction
17:20:07 <alise> Extraction Library ident.
17:20:07 <alise> 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 <alise> Recursive Extraction Library ident.
17:20:07 <alise> Extraction of the Coq library ident.v and all other modules ident.v depends on.
17:20:20 <alise> Extraction Language Ocaml.
17:20:20 <alise> Extraction Language Haskell.
17:20:20 <alise> Extraction Language Scheme.
17:20:20 <alise> Extraction Language Toplevel.
17:21:25 <oerjan> Extraction Language Brainfuck.
17:23:44 <alise> Phantom_Hoover: and in fact
17:23:47 <alise> http://hackage.haskell.org/package/meldable-heap
17:23:50 <alise> is the haskell extraction of
17:23:55 <alise> http://code.google.com/p/priority-queues/
17:24:03 <alise> + some wrappers i think
17:24:11 <Phantom_Hoover> But this may well be because it took me about 10 minutes to write fact in coqtop.
17:24:29 <alise> use proofgeneral with electric mode and three window mode
17:24:34 <alise> it is absolutely the only way to stay sane
17:25:05 <alise> with proofgeneral electric three-window you have one window for your file
17:25:13 <alise> and one for misc. output
17:25:20 <alise> you can execute a command just by "TheCommand foo."
17:25:24 <alise> and proofs proceed automatically on .
17:26:28 <alise> Phantom_Hoover: http://hackage.haskell.org/packages/archive/meldable-heap/2.0.3/doc/html/src/Data-MeldableHeap-LazyBrodalOkasakiExtract.html
17:26:28 <alise> http://hackage.haskell.org/packages/archive/meldable-heap/2.0.3/doc/html/src/Data-MeldableHeap-StrictBrodalOkasakiExtract.html
17:26:40 <alise> http://hackage.haskell.org/packages/archive/meldable-heap/2.0.3/doc/html/src/Data-MeldableHeap-Lazy.html
17:26:42 <alise> http://hackage.haskell.org/packages/archive/meldable-heap/2.0.3/doc/html/src/Data-MeldableHeap-Strict.html
17:26:46 <alise> the first two were extracted from Coq automatically
17:26:53 <alise> http://code.google.com/p/priority-queues/source/browse/#hg/brodal-okasaki the coq source
17:27:02 <alise> it is absolutely a requirement
17:27:27 <alise> just install it, set electric mode, set three window mode, make your emacs window big, and open a .v file
17:27:54 <Phantom_Hoover> Setting electric mode and setting three window mode entails what?
17:28:09 <alise> electric mode means that commands are executed on . -- you absolutely want this for proofs, so they can be interactive
17:28:14 <alise> three window mode i already explained
17:28:26 <alise> anyway, just trust me and do it, it'll be worth your while
17:28:34 <alise> after a short learning curve it's absolutely the easiest way
17:55:03 -!- Flonk has joined.
18:21:46 -!- Phantom_Hoover has quit (Ping timeout: 265 seconds).
18:30:02 <coppro> 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.
19:06:47 <coppro> alise: because Gmail can't grasp the notion of filtering individual messages when trying to run filters on existing mail
19:06:52 <coppro> it filters the entire conversation
19:07:01 <coppro> (but it doesn't do this for incoming mail... fail)
19:07:08 <alise> coppro: heh, really?
19:07:24 <alise> I'm, uh, just gonna run my own mail server asap.
19:07:34 <alise> I might use http://en.wikipedia.org/wiki/Sieve_(mail_filtering_language), but the syntax is a bit weird.
19:07:54 <alise> 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 <coppro> yeah, eventually I'll set something up of my own
19:08:14 <coppro> but Thunderbird can filter pretty well actually
19:08:20 <alise> yeah, but I hate client-dependence.
19:08:31 <alise> especially since I theoretically use a mobile too.
19:08:45 <alise> 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 <coppro> eventually I will have a mail server
19:09:06 <alise> 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 <alise> 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 <alise> I'd like to run a server from home, but I'd also like something, well, faster.
19:09:54 <alise> Ideally I'd colocate, but I Don't Have That Kind of Money.
19:09:57 <alise> So ho hum, VPSes it is.
19:10:27 * pikhq should also continue cleaning out all the crap that's in ~
19:11:07 <alise> pikhq: careful, it'll turn into my Computer Renovation Plan
19:11:20 <alise> which is actually impossible as it has a step where A depends on B and B depends on A
19:11:37 <alise> Leonidas: Yeah! Oh?
19:11:43 <alise> Dammit Leonidas, reveal your secrets!
19:12:37 <pikhq> WHY DO I HAVE SO MANY PDFs
19:12:42 <pikhq> WHY IS THERE SO MUCH IN ~?
19:13:27 -!- Wamanuz has quit (Remote host closed the connection).
19:14:00 <alise> 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 <alise> 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 <alise> pikhq: The thing is, all these happen simultaneously.
19:14:27 <pikhq> rm: cannot remove `vala-0.7.7/gee/.libs/iterable.o': Operation not permitted
19:14:31 <alise> pikhq: As a result, I have ensured that my Computer Renovation Plan will never, ever go into effect.
19:14:53 <coppro> I need to clean my ~ soon
19:15:00 <pikhq> THAT WAS DONE AS ROOT
19:15:16 <pikhq> drwS---rwt 2 205232978 2148707191 8192 Dec 29 1969 iterable.o
19:15:19 <alise> it might be hardlinked to some /dev/ device :)
19:15:22 <pikhq> Holy *frak* that's fucked up.
19:15:23 -!- Wamanuz has joined.
19:15:26 <alise> S and t, what the hell?
19:15:28 <alise> d is directory isn't it??
19:15:41 <alise> i have absolutely no clue what that permission is
19:15:43 <alise> please walk me through it
19:15:47 <alise> d is directory, right?
19:16:12 <coppro> S is setuid and t is sticky iirc
19:16:18 <alise> and d is directory?
19:16:43 <alise> "Downloading from 3 of 9 connected peers - 8.2 KiB/s"
19:17:12 <alise> there's about 30 peers total :P
19:17:22 <alise> shit now i'm uploading faster than my download, this will never download
19:18:54 <alise> wait, S isn't setuid on a directory, is it?
19:18:56 <alise> it means something else
19:19:12 <pikhq> So, what you're saying is that I should mount read-only and fsck.
19:19:18 <alise> 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 <alise> pikhq: i'd use a livecd
19:19:28 <alise> i wouldn't trust that system >_>
19:19:58 <pikhq> 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 <alise> This is why LVM sucks >_>
19:20:26 <pikhq> / is still good, /home/ just has... Some crap in it still.
19:20:42 <alise> try and cd to iterable.so
19:20:46 <alise> if it's a directory
19:21:08 <pikhq> drwS---rwt 2 205232978 2148707191 8192 Dec 29 1969 .
19:21:08 <pikhq> drwxr-xr-x 3 pikhq pikhq 4096 Aug 14 11:40 ..
19:21:37 <pikhq> zsh: operation not permitted: foo
19:21:58 <alise> I suggest (1) copying it somewhere to preserve the crazy, then (2) rmdir
19:21:58 <pikhq> zsh: operation not permitted: foo
19:22:12 <pikhq> I'll tar the crazy.
19:23:00 <pikhq> I can *create* files in there
19:23:04 <pikhq> I cannot *remove* files.
19:23:15 <alise> it'll break shit, i bet
19:23:26 <alise> there must be more to this than just the permissions
19:23:29 <alise> a file has become a directory
19:23:30 <alise> where's the file data?
19:23:36 <alise> does the directory still point to the inodes somehow?
19:23:44 <alise> pikhq: can you open() the directory?
19:23:48 <alise> maybe you can read it :D
19:24:03 <pikhq> chmod: changing permissions of `iterable.o': Operation not permitted
19:24:13 <alise> just ... just leave it there
19:24:18 <alise> how big is the filesystem?
19:24:20 <pikhq> chown: changing ownership of `iterable.o': Operation not permitted
19:24:43 <pikhq> alise: 758G, 221G free.
19:24:58 <alise> pikhq: Do you have more of that space? :P
19:25:07 <alise> Compress the whole FS up :D
19:25:26 <pikhq> alise: Most of it's videos.
19:25:42 <coppro> alise: more filtering shit
19:25:53 <alise> pikhq: yeah but you'd have to compress the whole 700 gigs
19:25:58 <alise> coppro: hmm, what?
19:26:20 <pikhq> Aaaand I only have the 1TB drive here.
19:26:20 <coppro> alise: gmail's retarded notion of tags means that client-based filtering doesn't work correctly
19:26:33 <alise> gmail w/ imap is utterly pointlessly horrible
19:26:41 <alise> pikhq: blu-ray drive? :P
19:26:44 <coppro> it's been fine for me for a long time
19:35:33 <alise> "4 hours remaining"
19:38:29 <alise> 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:44:54 * coppro starts migrating mail off of gmail
19:45:16 <coppro> UW Computer Science Club
19:45:17 <alise> you can have my VPS :-P
19:45:26 <alise> ugh, I hate university/company mail
19:45:37 -!- tombom has joined.
19:45:39 <alise> you /know/ you're not going to be there forever
19:45:41 <coppro> alise: UW CSC is imap from my homedir
19:45:49 <coppro> CSC membership is renewable indefinitely
19:46:15 <coppro> in theory, you don't even need to be a student to have signed up in the first place
19:46:26 <alise> ok, so say you move to ... australia and become a successful ... jazz musician, who plays nomic in his spare time
19:46:33 <alise> do you still want to use the CSC address? :D
19:47:10 <coppro> or migrate it, since I have access to the datatfiles
19:47:23 <alise> yeah, but still, it involves an address change
19:47:48 <coppro> yes; eventually I'll probably get a domain of my own
19:47:52 <coppro> that's not right now though
19:47:58 <coppro> and gmail broke the last straw
19:48:02 <alise> "Alexander Limi makes software easier to use. Founder of the open source project plone" ;; Plone, the height of usability and simplicity.
19:48:19 <alise> coppro: you'll be missing the ui in approx. 10 minutes
19:48:36 <coppro> alise: honestly, I rarely go on gmail proper as-is
19:49:08 <alise> i have "plans" to create the Perfect Email Application
19:49:22 <coppro> I'll ping you about it in 40 years
19:49:24 <alise> 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 <alise> i guess now it'll be all cat(1)y
19:49:40 <alise> actually, oh, i remember my latest design
19:49:42 <alise> it was really nice
19:50:01 <alise> a dual pane interface showing nested threads on the right, but on the left a conversation style view
19:50:07 <alise> and the selected item on the right changed as you scrolled the left
19:50:08 <coppro> the only time GMail's 'All Mail' folder is coming in remotely handy is when I'm moving everything off gmail
19:51:13 <alise> ATS is interesting
19:51:28 <coppro> my only question is whether I care about ancient mail...
19:51:36 <alise> coppro: you probably don't even care about recent mail
19:51:52 <alise> i'd just leave it on gmail for reference
19:52:04 <coppro> oh wait, my mail doesn't even come close to my quota
19:52:04 <alise> you probably won't need it after a couple of weeks
19:52:16 <alise> also, fuck quotas >_>
19:52:33 -!- zeotrope has joined.
19:52:36 <alise> but i'm a control freak
19:52:55 <coppro> 4GB, and it's not like it's the only computer I'm allowed to use
19:53:48 <coppro> I bet I could get it upped if I needed it, too
19:53:53 <alise> i need infinite money and a very fast symmetrical fibre-optic link
19:53:59 <alise> and a big, big house
19:54:04 <alise> then i can run EVERYTHING
19:54:18 -!- Gregor-P has joined.
19:54:33 <alise> (gregor-p gregor) => T
19:54:36 <alise> (gregor-p alise) => NIL
19:57:10 <coppro> also, I discovered a neat TB feature
19:57:19 <coppro> it has mailserver autodetection
19:57:32 <alise> tuberculosis does have some good feature
19:58:49 <alise> http://wondermark.com/650/
20:07:59 <coppro> whee, mail is being copied!
20:16:03 -!- Gregor-P has quit (Ping timeout: 265 seconds).
20:16:44 <sebbu2> http://www.osnews.com/images/comics/wtfm.jpg :)
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 <alise> oh no! a Killerkid!
20:42:08 -!- Flonk has quit (Ping timeout: 258 seconds).
20:48:47 <fizzie> (I simply can not have that though whenever there's a "oh no" anywhere.)
20:49:16 <fizzie> Can not avoid having, I mean.
20:49:32 <alise> fizzie: *thought, you mean.
20:50:34 <alise> fizzie: Did you ever played /3D Lemmings/? It's ... not good.
20:51:30 <Sgeo> Anything like 3d worms?
20:51:34 <fizzie> 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 <alise> Sgeo: Worms 3D is actually better.
20:55:19 <alise> fizzie: *was, you mean!
20:56:35 <fizzie> I no can spells and spaek.
20:57:47 -!- pikhq has quit (Quit: Rebooting).
21:00:38 -!- pikhq has joined.
21:00:45 <Ilari> 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 <alise> Ilari: http://www.theonion.com/articles/worlds-scientists-admit-they-just-dont-like-mice,1256/
21:03:48 -!- nooga has joined.
21:05:53 <nooga> i'm building chromium
21:08:22 <pikhq> alise: Fun fact: the ATI drivers work so much better than the free software ones.
21:08:34 <pikhq> Dear god I get full-screen Flash actually working well.
21:08:54 <pikhq> (which is not to say Flash is *good*, but it's... Working as intended, at least.)
21:09:01 <Phantom_Hoover> Ilari, do you plan to implement Brainfuck with the rats?
21:09:10 <alise> pikhq: Yes, indeed.
21:09:16 <alise> pikhq: Flash AV sync is still awful though.
21:09:39 <alise> 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 <alise> http://www.ats-lang.org/
21:09:51 <alise> performance and memory usage comparable to C/C++
21:09:58 <pikhq> 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 <alise> proper SMP multiprocessing too
21:10:09 <pikhq> "Let's play a few seconds worth of audio in a few frames!"
21:10:17 <pikhq> ... Which is when I kill npviewer.bin.
21:11:44 <alise> http://en.wikipedia.org/wiki/The_Adventures_of_Lomax
21:11:47 <alise> anyone ever play this
21:14:58 <Sgeo> At some point, I'm just going to start forgetting languages to make room for new ones
21:15:03 <Sgeo> (Ok, not really, but still)
21:16:12 <oerjan> hah i've forgotten more languages than you will ever learn
21:16:52 <Sgeo> Should I learn ATS or Falcon?
21:16:58 <Sgeo> (That was a joke question btw)
21:17:55 <Sgeo> Statics don't use currying functions?
21:18:19 <Sgeo> Also, they don't seem to stop to explain syntax
21:18:24 -!- zeotrope has quit (Ping timeout: 265 seconds).
21:18:28 <Sgeo> I guess it's understandable enough though
21:18:39 <alise> http://en.wikipedia.org/wiki/ATS_(programming_language)
21:19:07 <alise> http://en.wikipedia.org/wiki/ATS_(programming_language) has stuff :P
21:19:19 <Sgeo> Phantom_Hoover, ..lolwhat?
21:19:19 <Phantom_Hoover> Learning languages is boring if they use the same paradigm as something else you know.
21:19:25 <Sgeo> Why.. bother learning a ... ah
21:19:35 <Sgeo> Well, I have no previous exposure to static types
21:19:42 <Sgeo> erm, dependent
21:20:04 -!- zeotrope has joined.
21:20:17 <Sgeo> Also, maybe I'm misunderstanding something, but I can see ATS becoming a new favorite programming language
21:20:37 <alise> chris double is doing ats stuff right now http://www.bluishcoder.co.nz/
21:20:49 <alise> take a look at their proven-to-return-a-sorted-permutation quicksort though
21:20:50 <alise> http://www.ats-lang.org/EXAMPLE/MISC/listquicksort_dats.html
21:21:16 <alise> but then it does build lists from scratch
21:23:12 <alise> meh, i don't mind it
21:23:14 <alise> Sgeo: there is a tutorial btw
21:23:17 <alise> http://www.ats-lang.org/TUTORIAL/tutorial.html
21:23:40 <Sgeo> alise, that's what I'm looking at
21:23:47 <Sgeo> It's not all that comprehendible
21:24:07 <Sgeo> Where does it explain the difference between static and dynamic?
21:24:40 -!- Phantom_Hoover_ has joined.
21:25:24 <Sgeo> Is [] existential quantification a syntax thing?
21:25:26 <Phantom_Hoover_> Sgeo, why not learn Coq if you want to do dependent types?
21:25:34 <Sgeo> Or just an illustrative thing like >> in Smalltalk?
21:25:46 <Sgeo> Phantom_Hoover_, because I also want something that's practical
21:26:55 <alise> Sgeo: ATS isn't really "practical".
21:27:03 <alise> Sgeo: Coq is practical.
21:27:16 <alise> It has been used to re-prove the four colour theorem; not easy.
21:27:26 <alise> It has also been used to create quite a few libraries that have been proved correct,
21:27:30 <alise> then extracted to Haskell, O'Caml or Scheme.
21:27:45 <alise> ATS is more for the actual programs, sure, but Coq is practical too, and ATS is quite research too.
21:27:46 <Sgeo> alise, how about for, say, making a game?
21:28:07 <Phantom_Hoover_> Sgeo, well, if you want your game to be provably correct, then yes.
21:28:10 <alise> Phantom_Hoover_: no. well, you could probably model it.
21:28:14 <alise> you could probably model IO
21:28:18 <alise> and then do infinite stuff with that, too
21:28:19 -!- Phantom_Hoover has quit (Ping timeout: 265 seconds).
21:28:27 <alise> Sgeo: doing that in a formally verified way in ATS would be a gigantic impossible bitch
21:28:32 <alise> if you don't want to formally verify it ... why use these languages?
21:29:08 <alise> 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 <alise> i'm not discouraging you learning ats, just your reasons
21:29:33 <Sgeo> What about formally verifying _parts_ of the game?
21:29:47 <alise> you could write those parts in coq and extract them. it's not like they'd do any IO
21:29:54 <alise> (formally verifying SDL calls? that doesn't make any sense.)
21:30:18 <alise> 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 <alise> which converts them (barely compilation, it's a quite direct conversion) to one of those languages
21:30:45 <alise> you write some wrappers, and then just plug it in to the rest of your program
21:30:49 <alise> ats is easier to write code in than coq though
21:30:50 <Phantom_Hoover_> alise, on that topic, what if your function uses nats, for instance?
21:31:01 <alise> Phantom_Hoover_: it extracts the data types you use
21:31:15 <alise> 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:54 <alise> but uh clearly my lang is the best :)
21:31:57 <alise> i really like merd
21:32:00 <alise> even if it is shit
21:32:26 * oerjan considers swatting alise
21:32:33 <alise> no, it actually is
21:33:39 <Sgeo> Ok, static terms can be used in types?
21:33:45 <oerjan> painfully poorly punctuated puns
21:34:26 <Sgeo> It's been on hold since 2003
21:34:43 <alise> Sgeo: it isn't actually vaporware though
21:34:45 <alise> there's an implementation
21:34:51 <alise> it just doesn't do everything
21:34:55 <alise> and yeah, the project is dead
21:35:05 <alise> SEXY FUNCTIONAL LANGUAGES
21:35:22 <alise> Let me show you my Gonad typeclass.
21:35:40 <Phantom_Hoover_> That could be related to my SHOCKING TRUTH from yesterday.
21:36:49 <oerjan> class Gonad g where type Gonad h => h; copulate :: g -> h -> IO ()
21:37:12 <alise> "type Gonad h => h" ;; i forget what this does
21:37:17 * oerjan doesn't actually know how type families work
21:37:18 <alise> it just asks for another gonad?
21:37:34 <oerjan> yeah that was the idea
21:38:16 <alise> class Gonad g where nruter :: g a -> a; dnib :: a -> (g a -> b) -> b
21:38:28 <alise> challenge: find a use
21:38:35 <alise> (these are not comonads, afaik)
21:38:45 <oerjan> i was going to ask about that
21:38:55 <alise> extend :: (w a -> b) -> w a -> w b
21:39:02 <alise> so with comonads, the result is still X b
21:39:05 <alise> whereas with mine the result is b
21:39:10 <oerjan> well nruter has the type of coreturn or whatever
21:39:18 <alise> the only change is w b into b
21:39:21 <alise> mine are the direct opposite of monads
21:39:24 <Phantom_Hoover_> Well, there's no immediate way to construct a value of type g a.
21:39:27 <alise> i.e. replace "m a" with "a" and "a" with "g a"
21:39:30 <alise> Phantom_Hoover_: uhh
21:39:34 <alise> dnib :: a -> (g a -> b) -> b
21:39:54 <alise> presumably x `dnib` nruter = x
21:40:37 <alise> then nruter (x `dnib` id) = x, ofc
21:40:45 * alise renames them danoms, not gonads
21:40:48 <alise> since this is actually interesting :P
21:44:58 * Sgeo hahs at ATS's fix notation
21:47:05 <alise> instance Danom Identity where
21:47:05 <alise> nruter (Identity x) = x
21:47:05 <alise> dnib x f = f (Identity x)
21:47:14 <alise> instance Danom ((,) a) where
21:47:15 <alise> dnib x f = f (x,x) -- I do not think this one is very useful
21:48:10 <alise> can't have Danom []
21:48:12 <alise> since nruter [] = ???
21:48:31 <oerjan> 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 <derdon> alise: which language are you talking about?
21:48:45 <alise> derdon: haskell, atm
21:48:47 <oerjan> the a in the instance is not the same as the a in the dnib type
21:49:04 <derdon> alise: ah, then I detected it correctly :)
21:49:12 <alise> dnib :: a -> ((a,c) -> b) -> b
21:49:20 <derdon> alise: although Haskell is not really esoteric
21:49:28 <alise> derdon: but what we're doing is
21:49:40 <alise> oerjan: well ... it's not entirely clear what to do at all, then :D
21:49:49 <alise> could you just specify like ()?
21:49:53 <alise> or is it quantified in itself?
21:50:00 <oerjan> indeed that seems undefined, unless you use undefined
21:50:45 <oerjan> the c could be a specific type
21:50:47 <alise> data Stream a = SC a (Stream a)
21:50:47 <alise> adinf :: a -> Stream a
21:50:48 <alise> adinf x = SC x (adinf x)
21:50:48 <alise> instance Danom Stream where
21:50:48 <alise> nruter (SC x _) = x
21:50:48 <alise> dnib x f = f (adinf x)
21:50:55 <alise> not much interesting seems to happen in these
21:50:57 * alise wonders about Either
21:51:02 <Sgeo> Ok, so there's #include, and then compilation
21:51:03 <alise> nope, can't do that
21:51:08 <Sgeo> That bit seems like C/C++
21:52:31 <oerjan> no, that's the wrong type
21:52:41 <oerjan> it needs to be whatever is in Right
21:53:25 <oerjan> it's Danom (Either a) so you cannot fix it that way
21:53:25 <alise> hmm EIther a a would work
21:53:38 <alise> data BothEither a = Left a | Right a
21:54:09 <oerjan> but that's just an obscured (Bool, a)
21:54:19 <Sgeo> Ok, ATS syntax gives me a headache
21:54:37 <alise> oerjan: good enough
21:54:43 <alise> Sgeo: you give my syntax a headache
21:55:12 <alise> oerjan: ah, but should it be f (BLeft x) or f (BRight x) :P
21:55:19 <Sgeo> alise has syntax. Therefore, alise is a language. Therefore, I should learn alise.
21:56:32 <oerjan> Syntax quidquid nullam altera monstrum
21:57:14 * oerjan has very little idea what he actually said
21:57:42 <alise> Sgeo: not in the biblical sense, i hope.
21:58:05 <fizzie> Isn't that just "know" in the biblical sense?
21:58:19 <fizzie> Maybe it's transitive to learning.
21:58:28 <alise> If you learn something, you know it.
22:00:45 <Zuu> and then you forget it
22:02:29 <alise> oerjan: i think we can conclude that danoms are useless
22:02:58 <Sgeo> useless != not fun
22:03:12 <Sgeo> I think everyone in this channel should know that
22:03:15 <oerjan> maybe a little too much like _both_ monads and comonads at the same time...
22:09:00 <Sgeo> I seem to have gotten in a bit on an online argument
22:09:05 -!- oerjan has quit (Quit: Good night).
22:10:54 <Sgeo> http://www.reddit.com/r/geek/comments/d3o6c/futurama_writer_created_and_proved_a_brand_new/c0xc7rm
22:15:33 <Phantom_Hoover_> 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 <Sgeo> They didn't even come up with the conjecture
22:17:13 <Sgeo> I rewatched the episode today
22:17:29 <Sgeo> They didn't wonder "Well, given any possible mixup, is there a solution?"
22:17:34 <Sgeo> Or anything along those lines
22:19:28 <Mathnerd314> Phantom_Hoover_: because it's so _v_ erbose?
22:21:33 <alise> Mathnerd314: lemme guess, you like agda
22:21:53 <alise> Phantom_Hoover_: coq au Vin? :P
22:24:28 -!- Phantom_Hoover has joined.
22:25:36 -!- Phantom_Hoover_ has quit (Read error: Connection reset by peer).
22:25:47 <Sgeo> "No, they came up with a solution that works in all cases, as proven by the futurama guy. Stop being a dumbass.
22:29:12 <Phantom_Hoover> Sgeo, he's an idiot, and he's being overwhelmingly downvoted. Leave it.
22:31:39 <alise> "You are a pathetic person."
22:39:08 <alise> If you have them all, you have seen the episode. Why are you acting like a helpless retard?
22:39:10 <alise> 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 <alise> You are a personal insult for being a dumbass.
22:39:34 <alise> Sgeo: segoli is two removals and one swap away from sgeo!
22:41:00 <alise> Sgeo: insomniac84 is a known troll iirc
22:41:27 -!- sftp has quit (Read error: Connection reset by peer).
22:42:34 <Sgeo> 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: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 <Sgeo> Erm, indication of something dangerous
23:18:37 <Phantom_Hoover_> Everyone gets it throughout their life, so it's hardly abnormal.
23:20:14 <Sgeo> But can lack of sleep make it worse?
23:20:20 <Sgeo> And I think lack of sleep is dangerous
23:22:02 <Phantom_Hoover_> Do you end up thinking wildly incoherent thoughts, like augur thinking he was a lambda term.
23:23:00 <Sgeo> I'm not dejavuing right now, just tired
23:27:16 <Sgeo> As far as I can tell, I am not Hallu
23:27:24 <Sgeo> Or polymorphed
23:28:02 <Sgeo> Maybe this is a drea,
23:28:17 <Sgeo> pikhq, do a reality check.
23:31:43 <alise> Phantom_Hoover_: wat
23:31:56 <alise> pikhq: Music tagging adventures, part n: I have decided to simply elide "title" tags from untitled works.
23:32:38 <alise> <Phantom_Hoover_> Do you end up thinking wildly incoherent thoughts, like augur thinking he was a lambda term. ;; XD
23:33:18 <alise> I think he meant Phantom_Hoover_.
23:33:32 <alise> 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 <Sgeo> Well, if pikhq doesn't want to become lucid, he'll just drown in the raingutter
23:34:02 <Phantom_Hoover_> Trying Check reality. in a virgin environment: Error: The reference reality was not found in the current environment.
23:34:03 <alise> pikhq: Therefore, I think I will do "title=".
23:34:09 <alise> virgin environment!
23:36:21 <alise> sigh, title= doesn't work either
23:37:14 <alise> pikhq: technically, titling something the empty string isn't the same thing as not naming something, is it?
23:38:27 * Sgeo goes to read DCs say the darndest things
23:39:28 <Phantom_Hoover_> I can only assume it uses magic, or that I missed something.
23:40:21 <Sgeo> auxto is oww-to
23:40:43 <Phantom_Hoover_> 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:43:14 * Sgeo is just being an Esperanto nut
23:47:44 <Sgeo> "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:40 <Sgeo> http://www.dreamviews.com/f28/dcs-say-darndest-things-19509/index69.html#post1486806
23:49:00 <alise> <Phantom_Hoover_> I can only assume it uses magic, or that I missed something.
23:49:03 <alise> <Phantom_Hoover_> 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:11 <alise> it simply tries a bunch of common tactics
23:49:24 <alise> like things that automatically prove simple arithmetic statements, things that prove things from datatype constructions
23:50:44 <Sgeo> "Spock: [to me, raising an eyebrow] "...I am quite tasty, captain.""
23:51:28 <alise> "Well now what?" ;; hey look it's (maybe) augur