2010-05-01: 00:00:34 * Gregor huggles his vim 00:00:47 So I can't get ffplay to work on the IREX, and I don't know why :( 00:02:18 -!- FireFly has quit (Quit: Hey! Listen!). 00:02:20 (Ignoring the fact that it's ridiculous to run it there ;) ) 00:04:35 hmmm, Parrot's Brainf*** bench.b doesn't seem worthy of the name, doesn't do much (prints 'Z'..'A') 00:09:20 and the "QuickBasic" [sic] thing is a compiler only but seems somewhat reasonable (if the README is to be believed) 00:10:25 it has Wumpus, for example ;-) 00:12:00 huh, "Befunge" Parrot maintainer is Quelin, go figure 00:14:16 Anyone ever wondered what the worst poem ever would look like? 00:14:30 Lo, for I have penned a travesty on the topic of emacs and vi: http://pastie.org/941004.txt?key=3p1yec1kcynj1rblir8a 00:14:56 It actually took effort to write that badly. 00:15:30 Especially rhyming repent with vio-lent. 00:15:52 Also winner/dinner/winner. 00:16:18 It's not normal to rhyme a word with itself, is it? 00:16:24 lol, "Bush hid the facts" 00:16:40 Hey, it breaks Notepad. 00:16:42 Sgeo: No :P 00:17:02 BTW, Notepad can edit > 64k since NT-based (XP) became common 00:17:19 not sure what "[vi] can't handle 2k" means, though 00:17:20 Sssh. 00:17:25 Rugxulo: A petty insult, clearly! 00:17:31 rms is 2cool4u. 00:17:50 Notepad can't even handle *nix line endings, and it adds a UTF-8 BOM (which is invalid) 00:18:12 Wordpad > Notepad ;-) 00:18:14 -!- jcp1 has joined. 00:18:17 (but I use neither, honestly) 00:18:52 nicely done, alise 00:19:08 I ****ing hate the UTF-8 BOM. 00:19:13 except you didn't mention "vi vi vi" nor "free software vi is a penance" 00:19:15 Nicely done? 00:19:18 It was meant to be bad! 00:19:27 and it was spectacularly so 00:19:27 Rugxulo: Yes, well, I had to fit within the poem structure; and I'm tired. 00:19:34 Yayyy 00:19:35 one project I work on I have to make sure I add the BOMs before I commit 00:19:48 ****ing piece of **** Windows 00:19:49 * Rugxulo imagines this is how Beowulf was penned 00:19:51 It commits so many atrocities against proper rhyming form. 00:20:01 Also, viæity is just ludicrous. 00:20:09 That... makes it seem like people where you work code in Notepad or something 00:20:50 ... UTF-8 BOM? *What the fuck*? 00:21:03 pikhq, it's a Notepad thing ;-) 00:21:05 pikhq, it's more of a magic number for UTF-8 00:21:22 pikhq: yes 00:21:33 alise: Also I couldn't grasp the meter at all 00:21:37 Rugxulo: MURDER. MICROSOFT. DEVELOPERS. 00:21:48 coppro: That's because it has no meter. 00:21:55 I just switched to indenting when I couldn't make it rhyme. 00:21:58 that would do it 00:22:00 Sometimes it rhymed anyway. 00:22:05 Oh, whaddya know. A UTF-8 BOM is actually explicitly allowed by Unicode. 00:22:15 except Notepad REQUIRES it 00:22:17 since when? I thought they disallowed it 00:22:24 It is recommended you avoid it, but it is allowed. 00:22:41 Rugxulo: Since always, it seems. 00:22:42 hmm... it's Friday already? 00:22:45 you sure? even in UTF-8 explicitly?? 00:22:53 Yes. 00:22:59 UTF-16, sure, but I thought it was bad for UTF-8 00:23:21 It's a stupid idea, but it's permitted. 00:24:06 probably because of braindead things like Nopad 00:24:22 "Dawkins is a clown" ... eh? 00:24:33 The "use as a signature" thing is in the BOM FAQ, http://unicode.org/faq/utf_bom.html#BOM 00:25:33 However, I'd imagine that *requiring* a BOM for UTF-8 is a big violation of the spec. 00:25:36 Also refers to a "particular protocol (e.g. Microsoft conventions for .txt files) --"; wonder if there's any other examples. 00:25:50 right, that's what it was, the damn BOM mucks up the shell script shebang thingie 00:26:20 in fairness, why anybody would ever use Notepad for serious text editing is beyond me ... 00:26:25 Simple fix for that on Linux. 00:26:37 I think Notepad++ is consistently one of the most popular projects on SourceForge 00:26:38 Write a simple shebang parser that ignores a leading BOM. 00:27:16 Then, register 0xEFBBBF as a magic number for an executable format, with your shebang parser as the program to handle it. 00:27:22 Voila. Shebang now works. 00:27:39 or ... just don't use Notepad ;-) 00:27:43 (requires the miscellanous executable format module and procfs) 00:28:00 MS EDIT ftw!! ;-) j/k 00:28:15 edlin ftw! ;-)) 00:28:22 ed. 00:28:27 Not edlin. ed. 00:28:40 so you've got four choices on Windows: Notepad, Wordpad, edit, edlin 00:28:49 Hey, gcc ignores the BOM; that's at least user-friendly. 00:29:02 clang doesn't: test.c:1:1: error: expected identifier or '(' 00:29:12 fizzie: That's... Quite surprising *and* well-done of GCC. 00:29:21 * Rugxulo thought it odd that LLVM 2.7 doesn't have a MinGW compile of Clang 00:29:58 LLVM-gcc42 ... check, Clang ... nope! 00:30:43 Hey, I should test if llvm 2.7's clang compiles that ff3. 00:30:51 fizzie: clang has about 0 Unicode support currently 00:31:22 Clang uses "LANG=C" ? ;-) 00:31:43 clang 2.7 appears to have a regression in its support of computed goto. 00:31:51 I'd file a bug but it appears to have been filed already. 00:32:02 Assembler messages: "Error: symbol `.LBA3_run_' is already defined" times 145. Aw. :/ 00:32:07 Yes. 00:32:13 That's the regression in question, in fact. 00:32:23 I noticed one bug about that, but I thought I saw the word "fixed" in there somewhere. 00:32:33 It fails hardcore at generating new names. 00:32:37 Oh? Fixed? 00:32:44 Guess I'll reopen it then. 00:32:46 It was an earlier thing. 00:32:56 Let's see what was it I found. 00:33:17 http://llvm.org/bugs/show_bug.cgi?id=6608 This? 00:33:36 Yes, that. 00:33:54 Ah. Yes, it's fixed, but it's not in 2.7. 00:34:08 Which is retarded. I'd call that a release-breaker. 00:34:31 "Computed goto, that's some evil hacker-cracker thing, better not speak about it." 00:38:18 fixed over a month ago, apparently 00:40:05 how the heck can LLVM srcs be 8 MB but the test suite is like 68 MB ?!? 00:40:24 -!- jcp1 has quit (Quit: I will do anything (almost) for a new router.). 00:42:44 alise, am I allowed to make a joke? 00:43:10 Sure. 00:43:17 Rugxulo: it's very well-tested software. :) 00:43:22 You should move to Reddit Island! 00:45:53 Rugxulo: They pride themselves on testing the code generator. 00:46:19 with what exactly? that's fairly huge for a test suite 00:46:47 everything 00:47:52 obviously they didn't test computed gotos! 00:47:55 Rugxulo: Not compared with Sqlite. 00:48:24 Which actually tests for correct behavior at (and I am not kidding) each and every branch. 00:53:52 Ahh, computer gotos. 00:54:06 s/r/d/ 00:59:29 In Arizona, "teachers with accents" can no longer teach English. 00:59:36 That is so fucking dumb I cannot describe it. 00:59:52 You find me a person without an accent and I'll show you someone that's mute. 01:00:00 Guh? 01:01:20 At least it'll stop people with American accents teaching English. 01:01:32 Good :P 01:01:45 alise: There's a large number of incomprehensible UK accents, too. 01:01:58 Well, yes. 01:02:03 But they're uncouth. 01:02:06 Yeah, but there's only ONE incomprehensible American accent ;) 01:02:19 RP speakers will be banned from teaching English too. 01:02:19 Anyway they don't count as British because I can't even understand Geordies so they don't exist Q.E.D. 01:02:36 But RP is a bit too posh! 01:04:29 RP? 01:04:40 Arizona is going a _leetle_ crazy 01:05:18 Recieved Pronounciation. 01:05:30 which means what exactly? 01:05:30 The "posh" and "educated" UK accent. 01:05:42 -!- coppro has quit (Remote host closed the connection). 01:06:19 Rugxulo: Received Pronunciation is the accent of the Queen. 01:06:32 Of course, it isn't actually defined as that; but it's as good a guide as any. 01:06:47 It's actually all right most of the time, but some people take it Way Too Far. 01:06:52 (Such as, say, the Queen herself.) 01:07:01 alise: actually, the Queen's accent has been shown to slip towards Cockney over the last decade or so 01:07:06 Random phrase from a related article: "advocate ethnic solidarity instead of the treatment of pupils as individuals." 01:07:11 ais523: Hah 01:07:12 it surprised me when I discovered that there were actually people who /measured/ these things 01:07:13 Fair enough then. 01:07:48 I find it strange that when people think of ethnic solidarity, they think of the alternative as being pupils-as-individuals. 01:08:18 I see the alternatives as being stuff like gender solidarity, national solidarity, political solidarity, and so on. 01:08:20 -!- jcp has joined. 01:08:57 My favorite one, and the one I advocate, is universal solidarity. We're all people; let's stop fighting purely over the fact that we're different. 01:08:59 My actual accent is extremely boring; it seems that no outside influence has passed over it. 01:09:21 So it's a very generic British accent, really. 01:09:32 alise just once looked at the English alphabet and came up with a sound to match each letter; that's his accent. 01:09:51 Heh. 01:09:59 My accent is pretty much General American made more pedantic. :P 01:10:34 Judging by what people ask when they say "Why do you have a ____ accent?", I have a British accent. 01:11:55 I really dislike the American accent; it has this persistent nasal whining present all the time. 01:12:05 What is a nasal whining? 01:12:06 Like the average American attitude, actually. 01:12:19 I wonder if I have a nasal whining attitude. 01:12:21 uorygl: The sort of "ahh" - a sort of "r" vowel - repeated constantly in the background of every tone. 01:12:23 A very nasally sound. 01:12:26 Sorry; I can't explain further. 01:12:28 I don't even know IPA. 01:12:51 * uorygl ponders what sort of "ahh" a British person would consider a sort of "r" vowel. 01:13:00 you mean Jay Leno whining or something else? 01:13:31 By "tone", do you mean "vowel"? 01:14:19 * Sgeo loves this game 01:14:46 uorygl: Perhaps. I've really no idea. 01:15:16 But if you listen to, say, some BBC newsreporting, and then any American person, you'll notice a distinct sound underlying all the American's speech that does indeed seem nasal in nature that isn't present in the news report. 01:15:27 Perhaps it's only if you haven't grown up with American accents around you. 01:15:45 depends on the person ... I wouldn't consider Barry White nasally ;-) 01:15:50 Huh. 01:16:00 alise: You've probably just heard the more nasaly American accents. 01:16:09 Some of them are, in fact, annoyingly nasal. 01:16:27 True; not being American, my exposure is biased. 01:17:01 Others are anything but. American accents are quite varied. 01:17:26 But they're all inferior to British ones :P 01:17:36 * uorygl listens to a certain American accent and finds it rather horrible. 01:17:50 This is the horrible accent: http://accent.gmu.edu/browse_language.php?function=detail&speakerid=121 01:18:05 alise: You got rid of rhoticism your argument is invalid. 01:18:25 I have no speakers at the moment. 01:18:56 * uorygl finds an American accent that sounds pretty good. 01:19:01 http://1pd.org/play/4479_exploit.aspx 01:19:14 Come on, say it: "AAAARRRR". 01:19:21 Yarr! 01:19:23 pikhq: *Rhotacism. 01:19:25 * uorygl swordfights pikhq. 01:19:46 Also I truly believe that the ae and oe ligatures should be used whenever possible in all typeset works; am I barmy? 01:20:04 And that the diæresis is quite honestly superior to hyphenation. 01:20:09 Absolutely. Most of those result from overcorrection. 01:20:17 The diæresis diacritic, that is. 01:20:37 pikhq: Most of what? 01:20:48 Instances of "ae" and "oe" ligatures. 01:20:52 * uorygl blinks. 01:21:00 It's really easy to press Command-Q by accident. 01:21:11 Erm. Hypercorrection, even. 01:21:26 Can I tell Chrome to reopen all those tabs I just closed? 01:21:36 pikhq: Really? I suppose I should mention that I also think that the spelling of words that used to have "æ" but now sport "e" should be reverted, too. 01:21:45 uorygl, see History 01:21:57 So I'd write æsthetics, not esthetics. 01:21:57 Nothing useful seems to be in there. 01:22:20 I don't do it for the purpose of hypercorrection though. I just think it's more, well, æsthetically pleasing. 01:22:24 I don't argue for æs æverywheræ. 01:22:35 "æ" and "oe" become "e" in Latin in the Middle Ages. And then they got re-expanded *the wrong way*. 01:22:43 I use "ae" inconsistently. 01:22:57 And quite often the "reversion" happened *when it had never been there*. 01:23:05 I like aesthetics and anaesthesia, but I would never consult an encyclopaedia. 01:23:11 Do you agree that "æsthetic" and "dæmon" are correct? 01:23:14 For instance: it's fucking "fetus", not "foetus". 01:23:19 And I really hate paedophiles. 01:23:22 Although I'm not sure I wouldn't write "demon". 01:23:31 alise: Yes. 01:23:47 And encyclopædia? What about pædophilia? 01:23:57 I didn't know fœtus was incorrect. 01:24:02 Is it fætus, then? :P 01:24:10 No, it's always been "fetus". 01:24:20 Ah. 01:24:22 Fair enough then. 01:24:29 Aww, fœtus looks so much better :-P 01:24:36 "The word fetus is from the Latin fetus, meaning delicious," 01:25:09 "encyclopaedia" is the Latin spelling. 01:25:22 -!- Rugxulo has quit (Quit: Rugxulo). 01:25:40 Hey, neat, "encyclopedia" means "circular education". 01:25:41 "pedophilia", "paedophilia", and 01:25:50 "pædophilia" are all completely bizarre. 01:26:01 They come from "paidophilos". 01:26:43 Well I'm not spelling it paidophilia, so what should I do? 01:26:49 Also, encyclopædia is nice, so I'm going to keep spelling it that way. 01:26:59 At least encyclopaedia; I refuse to devolve into writing encyclopedia. 01:27:02 :P 01:27:04 Also, how do you pronounce "foetus", anyways? "foe - etus"? 01:27:18 Fowey eetus. 01:27:36 AAAAGH LATIN FAIL 01:27:39 -!- Tritonio_GR has quit (Read error: Connection reset by peer). 01:27:54 foëtus 01:27:56 Hmm, pedophilia is a hard word. (Har har) 01:28:25 It seems to have gone from Latin to paedophilia in German to pedophilia in English. 01:30:27 The Encyclopædia Britannica is a preëminent encyclopædia.¹ 01:30:27 1. Note: The author does not actually believe this. 01:31:35 Mmm, delicious diaresis and actually correct uses of ligatures. 01:32:00 diaræsis, you uncouth bastard. 01:32:18 The only problem with that word is that it makes me think of diarrhea. 01:32:49 We were both wrong. 01:32:55 Orally? 01:33:02 (a.k.a. O rly?) 01:33:14 Yeah it's diæresis 01:33:16 It's "dieresis", "diaeresis", or "diæresis". 01:33:47 Anyway, can I have a lot of money? I have an urge to buy some wonderfully-printed books. 01:36:05 ... And Fox News goes off the deep end *again*. 01:36:13 Calling Mr. Rogers evil. 01:36:21 Mister. Rogers. 01:36:24 I read the reddit comments on that; apparently the evil mark was clearly a joke. 01:36:27 *remark 01:36:46 I hate Fox News as much as the next sentient being, but did anyone actually watch the video before getting outraged? I know I didn't. 01:37:06 Anyway, less jabbering, more money to me. 01:38:50 * Sgeo loves not hanging out with friends on his birthday :( 01:38:59 Quit whining and do something interesting. 01:39:09 ¡Ay. 01:39:11 (Good life advice most of the time, actually.) 01:39:17 iAy, from Apple. 01:39:23 alise, I don't know how 01:39:32 It's difficult to do something interesting when you feel like something bad is going to happen. 01:39:43 Well, don't we count as friends? :P 01:39:51 Sgeo: Think about things you're interested in, then wait; Eureka, now write down what you thought. 01:39:55 Like right now. I feel like as a result of my choices, the outcome is going to be unacceptable. 01:40:07 uorygl: Which choices? 01:40:11 And so now whenever I think about doing something, I go "aiee!" 01:40:32 alise: choices like going to the wrong college and not doing the required work. 01:40:41 And also failing to take advantage of opportunities. 01:40:44 uorygl: How old are you again? 01:40:46 And not making friends on campus. 01:40:52 17, at the moment. 01:40:57 I've been going to arguably the wrong college for almost 3 years 01:41:19 uorygl: Well, you are still very young, then, and your college studies have only just started. 01:41:25 Also, most of my college friends approached me. I didn't ever initiate friendships 01:41:25 alise: what am I supposed to be outraged at? 01:41:26 * ais523 rages 01:41:27 You can easily go to another college and work harder there with no disadvantage at all. 01:41:29 Well, once, very recently 01:41:31 ais523: :-) 01:41:45 wow, I'm surprisingly good at feeling generically angry 01:41:50 as in, I surprised myself 01:41:56 I actually am angry atm, and I have no idea what at 01:41:56 uorygl: So plan that, and do it, and don't worry about it too much because in the end if you're smart it won't really matter because you'll know if you're not doing the right thing. 01:42:08 ais523: MR ROGERS! HNRRRRRRRRRR! 01:42:16 ... I think! 01:42:23 ok 01:42:29 Hmm, now I feel like I don't know what to be scared about. 01:42:45 uorygl: oil spills off the US coast? the entire economy about to collapse? politics in general? 01:42:55 exploding supervolcanos? the LHC creating black holes? 01:43:06 Chickens taking over the world??? 01:43:08 There, I just thought about a project I'd like to do, and I had a little bit of an "aiee" reaction. 01:43:18 What projekt? 01:43:45 A mathematical prediction market and proof database. 01:43:57 Lay off the Robin Hanson. 01:44:43 Robin Hanson came up with a specific application of prediction markets. My project idea has nothing to do with Robin Hanson. 01:44:59 Yeah, but Hanson is a big fan of prediction markets. So there :P 01:45:12 :P 01:45:20 Well, okay, O'Connor likes them too and O'Connor is cool, so you're permitted. 01:45:28 What language would the proofs be in? 01:45:35 Also, I'm not a person who has negative feelings about Robin Hanson. 01:45:38 Some constructive one like Coq or Isabelle? 01:45:39 I'm thinking Ivor. 01:45:42 So yes. 01:45:46 Ivor is not a proof language. 01:45:51 It is just a Haskell library. 01:45:53 Do you mean Idris? 01:45:56 That is not very proof-focused at all. 01:46:13 No, I mean Ivor. 01:46:14 I strongly suggest that if you are going to do actual proofs you should have a language with actual proof infrastructure; so Idris, Agda etc. are out. 01:46:23 Huh. 01:46:27 I'd strongly suggest Coq or Isar+Isabelle. 01:46:48 Well, okay. I'm not familiar with Coq whatsoever (modulo grammar), so what advantages does it have over something like Agda? 01:46:54 Isar has really nice proof structures actually: http://vdash.org/intro/cantor.html at least for the current crop of constructivist meanderings. 01:47:02 uorygl: Here's why Agda is totally unsuitable for this: 01:47:27 - it is not one concrete theory, just a bunch of features - admittedly so; it has been proved inconsistent several times, which is fixed by patches. Coq is based on one, very mathematically tested, tiny kernel theory. 01:47:41 It has only been proved inconsistent once, I think, and that was a bug in Coq, not the underlying theory. 01:47:47 And was very easily fixed. 01:47:54 (And the example was a very contrived one). 01:47:55 And: 01:48:27 - Agda has very little infrastructure for the actual prover; proving is basically a trial-and-error, run-and-repeat task. With Coq and similar, the proof is an interactive process that automatically shows assumptions and goals for you and lets you step and rewind proofs step by step. 01:48:43 This is amazingly useful in proving even the simplest theorems; instead of a complete spark out of nowhere, you can do proofs incrementally. 01:48:59 And finally, Coq has actual practical proofs underlying it -- Goedel's First Incompleteness Theorem, for instance. 01:49:01 Nobody really uses Agda. 01:49:15 Isar is like Coq but with a more declarative proof style; I think it is less interactive. I don't know much more about it. 01:49:25 'A patent pool is being assembled to go after Theora and other “open source†codecs now.' -- Steve Jobs. 01:49:47 So. Fuck you, Steve Jobs. You make Microsoft look open. 01:49:51 Mizar, while proprietary, has a very comprehensive database of mathematics already and a very readable declarative style. It is not constructive though. 01:49:59 uorygl: And that's most of what I have to say on the matter! 01:50:07 Mmkay. I don't know what Ivor is based on; I seemed to get the idea that it's based on some sort of formal theory, though not a specific one I've heard of. 01:50:11 pikhq: Yup, I pretty much hate Steve Jobs now. 01:50:27 What you say about the interactive proving stuff makes sense. 01:50:33 uorygl: I think it is the same one that underlies Coq. But it's really a library, a framework for building on. It's barely suitable for writing programs in directly, let alone proofs of any complexity. 01:50:37 alise: Steve Jobs specifically, or Apple in general? 01:50:43 I can think of arguments for either 01:50:44 Idris is a competent dependently-typed programming language based on it, but with next to no proof infrastructure. 01:50:46 ais523: Both. 01:51:03 in other news, apparently IE9