00:00:47 <Gregor> 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 <Gregor> (Ignoring the fact that it's ridiculous to run it there ;) )
00:04:35 <Rugxulo> hmmm, Parrot's Brainf*** bench.b doesn't seem worthy of the name, doesn't do much (prints 'Z'..'A')
00:09:20 <Rugxulo> and the "QuickBasic" [sic] thing is a compiler only but seems somewhat reasonable (if the README is to be believed)
00:10:25 <Rugxulo> it has Wumpus, for example ;-)
00:12:00 <Rugxulo> huh, "Befunge" Parrot maintainer is Quelin, go figure
00:14:16 <alise> Anyone ever wondered what the worst poem ever would look like?
00:14:30 <alise> Lo, for I have penned a travesty on the topic of emacs and vi: http://pastie.org/941004.txt?key=3p1yec1kcynj1rblir8a
00:14:56 <alise> It actually took effort to write that badly.
00:15:30 <alise> Especially rhyming repent with vio-lent.
00:15:52 <alise> Also winner/dinner/winner.
00:16:18 <Sgeo> It's not normal to rhyme a word with itself, is it?
00:16:40 <alise> Hey, it breaks Notepad.
00:17:02 <Rugxulo> BTW, Notepad can edit > 64k since NT-based (XP) became common
00:17:19 <Rugxulo> not sure what "[vi] can't handle 2k" means, though
00:17:25 <alise> Rugxulo: A petty insult, clearly!
00:17:50 <Rugxulo> Notepad can't even handle *nix line endings, and it adds a UTF-8 BOM (which is invalid)
00:18:14 -!- jcp1 has joined.
00:18:17 <Rugxulo> (but I use neither, honestly)
00:19:08 <coppro> I ****ing hate the UTF-8 BOM.
00:19:13 <Rugxulo> except you didn't mention "vi vi vi" nor "free software vi is a penance"
00:19:18 <alise> It was meant to be bad!
00:19:27 <coppro> and it was spectacularly so
00:19:27 <alise> Rugxulo: Yes, well, I had to fit within the poem structure; and I'm tired.
00:19:35 <coppro> one project I work on I have to make sure I add the BOMs before I commit
00:19:48 <coppro> ****ing piece of **** Windows
00:19:49 * Rugxulo imagines this is how Beowulf was penned
00:19:51 <alise> It commits so many atrocities against proper rhyming form.
00:20:01 <alise> Also, viity is just ludicrous.
00:20:09 <Sgeo> That... makes it seem like people where you work code in Notepad or something
00:20:50 <pikhq> ... UTF-8 BOM? *What the fuck*?
00:21:03 <Rugxulo> pikhq, it's a Notepad thing ;-)
00:21:05 <Sgeo> pikhq, it's more of a magic number for UTF-8
00:21:33 <coppro> alise: Also I couldn't grasp the meter at all
00:21:37 <pikhq> Rugxulo: MURDER. MICROSOFT. DEVELOPERS.
00:21:48 <alise> coppro: That's because it has no meter.
00:21:55 <alise> I just switched to indenting when I couldn't make it rhyme.
00:22:00 <alise> Sometimes it rhymed anyway.
00:22:05 <pikhq> Oh, whaddya know. A UTF-8 BOM is actually explicitly allowed by Unicode.
00:22:15 <coppro> except Notepad REQUIRES it
00:22:17 <Rugxulo> since when? I thought they disallowed it
00:22:24 <pikhq> It is recommended you avoid it, but it is allowed.
00:22:41 <pikhq> Rugxulo: Since always, it seems.
00:22:42 <coppro> hmm... it's Friday already?
00:22:45 <Rugxulo> you sure? even in UTF-8 explicitly??
00:22:59 <Rugxulo> UTF-16, sure, but I thought it was bad for UTF-8
00:23:21 <pikhq> It's a stupid idea, but it's permitted.
00:24:06 <coppro> probably because of braindead things like No<twitch>pad
00:24:22 <Rugxulo> "Dawkins is a clown" ... eh?
00:24:33 <fizzie> The "use as a signature" thing is in the BOM FAQ, http://unicode.org/faq/utf_bom.html#BOM
00:25:33 <pikhq> However, I'd imagine that *requiring* a BOM for UTF-8 is a big violation of the spec.
00:25:36 <fizzie> Also refers to a "particular protocol (e.g. Microsoft conventions for .txt files) --"; wonder if there's any other examples.
00:25:50 <Rugxulo> right, that's what it was, the damn BOM mucks up the shell script shebang thingie
00:26:20 <Rugxulo> in fairness, why anybody would ever use Notepad for serious text editing is beyond me ...
00:26:25 <pikhq> Simple fix for that on Linux.
00:26:37 <Rugxulo> I think Notepad++ is consistently one of the most popular projects on SourceForge
00:26:38 <pikhq> Write a simple shebang parser that ignores a leading BOM.
00:27:16 <pikhq> Then, register 0xEFBBBF as a magic number for an executable format, with your shebang parser as the program to handle it.
00:27:22 <pikhq> Voila. Shebang now works.
00:27:39 <Rugxulo> or ... just don't use Notepad ;-)
00:27:43 <pikhq> (requires the miscellanous executable format module and procfs)
00:28:40 <Rugxulo> so you've got four choices on Windows: Notepad, Wordpad, edit, edlin
00:28:49 <fizzie> Hey, gcc ignores the BOM; that's at least user-friendly.
00:29:02 <fizzie> clang doesn't: test.c:1:1: error: expected identifier or '('
00:29:12 <pikhq> 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 <Rugxulo> LLVM-gcc42 ... check, Clang ... nope!
00:30:43 <fizzie> Hey, I should test if llvm 2.7's clang compiles that ff3.
00:30:51 <coppro> fizzie: clang has about 0 Unicode support currently
00:31:43 <pikhq> clang 2.7 appears to have a regression in its support of computed goto.
00:31:51 <pikhq> I'd file a bug but it appears to have been filed already.
00:32:02 <fizzie> Assembler messages: "Error: symbol `.LBA3_run_' is already defined" times 145. Aw. :/
00:32:13 <pikhq> That's the regression in question, in fact.
00:32:23 <fizzie> I noticed one bug about that, but I thought I saw the word "fixed" in there somewhere.
00:32:33 <pikhq> It fails hardcore at generating new names.
00:32:44 <pikhq> Guess I'll reopen it then.
00:32:46 <fizzie> It was an earlier thing.
00:32:56 <fizzie> Let's see what was it I found.
00:33:17 <pikhq> http://llvm.org/bugs/show_bug.cgi?id=6608 This?
00:33:54 <pikhq> Ah. Yes, it's fixed, but it's not in 2.7.
00:34:08 <pikhq> Which is retarded. I'd call that a release-breaker.
00:34:31 <fizzie> "Computed goto, that's some evil hacker-cracker thing, better not speak about it."
00:38:18 <Rugxulo> fixed over a month ago, apparently
00:40:05 <Rugxulo> 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 <Sgeo> alise, am I allowed to make a joke?
00:43:17 <alise> Rugxulo: it's very well-tested software. :)
00:43:22 <Sgeo> You should move to Reddit Island!
00:45:53 <pikhq> Rugxulo: They pride themselves on testing the code generator.
00:46:19 <Rugxulo> with what exactly? that's fairly huge for a test suite
00:47:52 <Rugxulo> obviously they didn't test computed gotos!
00:47:55 <pikhq> Rugxulo: Not compared with Sqlite.
00:48:24 <pikhq> Which actually tests for correct behavior at (and I am not kidding) each and every branch.
00:59:29 <pikhq> In Arizona, "teachers with accents" can no longer teach English.
00:59:36 <pikhq> That is so fucking dumb I cannot describe it.
00:59:52 <pikhq> You find me a person without an accent and I'll show you someone that's mute.
01:01:20 <alise> At least it'll stop people with American accents teaching English.
01:01:45 <pikhq> alise: There's a large number of incomprehensible UK accents, too.
01:02:03 <alise> But they're uncouth.
01:02:06 <Gregor> Yeah, but there's only ONE incomprehensible American accent ;)
01:02:19 <pikhq> RP speakers will be banned from teaching English too.
01:02:19 <alise> 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 <alise> But RP is a bit too posh!
01:04:40 <Rugxulo> Arizona is going a _leetle_ crazy
01:05:18 <pikhq> Recieved Pronounciation.
01:05:30 <pikhq> The "posh" and "educated" UK accent.
01:05:42 -!- coppro has quit (Remote host closed the connection).
01:06:19 <alise> Rugxulo: Received Pronunciation is the accent of the Queen.
01:06:32 <alise> Of course, it isn't actually defined as that; but it's as good a guide as any.
01:06:47 <alise> It's actually all right most of the time, but some people take it Way Too Far.
01:06:52 <alise> (Such as, say, the Queen herself.)
01:07:01 <ais523> alise: actually, the Queen's accent has been shown to slip towards Cockney over the last decade or so
01:07:06 <uorygl> Random phrase from a related article: "advocate ethnic solidarity instead of the treatment of pupils as individuals."
01:07:12 <ais523> it surprised me when I discovered that there were actually people who /measured/ these things
01:07:48 <uorygl> I find it strange that when people think of ethnic solidarity, they think of the alternative as being pupils-as-individuals.
01:08:18 <uorygl> 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 <uorygl> 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 <alise> My actual accent is extremely boring; it seems that no outside influence has passed over it.
01:09:21 <alise> So it's a very generic British accent, really.
01:09:32 <uorygl> alise just once looked at the English alphabet and came up with a sound to match each letter; that's his accent.
01:09:59 <pikhq> My accent is pretty much General American made more pedantic. :P
01:10:34 <uorygl> Judging by what people ask when they say "Why do you have a ____ accent?", I have a British accent.
01:11:55 <alise> I really dislike the American accent; it has this persistent nasal whining present all the time.
01:12:05 <uorygl> What is a nasal whining?
01:12:06 <alise> Like the average American attitude, actually.
01:12:19 <uorygl> I wonder if I have a nasal whining attitude.
01:12:21 <alise> uorygl: The sort of "ahh" - a sort of "r" vowel - repeated constantly in the background of every tone.
01:12:23 <alise> A very nasally sound.
01:12:26 <alise> Sorry; I can't explain further.
01:12:28 <alise> 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 <Rugxulo> you mean Jay Leno whining or something else?
01:13:31 <uorygl> By "tone", do you mean "vowel"?
01:14:19 * Sgeo loves this game
01:14:46 <alise> uorygl: Perhaps. I've really no idea.
01:15:16 <alise> 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 <alise> Perhaps it's only if you haven't grown up with American accents around you.
01:15:45 <Rugxulo> depends on the person ... I wouldn't consider Barry White nasally ;-)
01:16:00 <pikhq> alise: You've probably just heard the more nasaly American accents.
01:16:09 <pikhq> Some of them are, in fact, annoyingly nasal.
01:16:27 <alise> True; not being American, my exposure is biased.
01:17:01 <pikhq> Others are anything but. American accents are quite varied.
01:17:26 <alise> 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 <uorygl> This is the horrible accent: http://accent.gmu.edu/browse_language.php?function=detail&speakerid=121
01:18:05 <pikhq> alise: You got rid of rhoticism your argument is invalid.
01:18:25 <alise> I have no speakers at the moment.
01:18:56 * uorygl finds an American accent that sounds pretty good.
01:19:01 <Sgeo> http://1pd.org/play/4479_exploit.aspx
01:19:14 <pikhq> Come on, say it: "AAAARRRR".
01:19:23 <alise> pikhq: *Rhotacism.
01:19:46 <alise> 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 <alise> And that the diresis is quite honestly superior to hyphenation.
01:20:09 <pikhq> Absolutely. Most of those result from overcorrection.
01:20:17 <alise> The diresis diacritic, that is.
01:20:37 <alise> pikhq: Most of what?
01:20:48 <pikhq> Instances of "ae" and "oe" ligatures.
01:21:00 <uorygl> It's really easy to press Command-Q by accident.
01:21:11 <pikhq> Erm. Hypercorrection, even.
01:21:26 <uorygl> Can I tell Chrome to reopen all those tabs I just closed?
01:21:36 <alise> 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:57 <alise> So I'd write sthetics, not esthetics.
01:21:57 <uorygl> Nothing useful seems to be in there.
01:22:20 <alise> I don't do it for the purpose of hypercorrection though. I just think it's more, well, sthetically pleasing.
01:22:24 <alise> I don't argue for s verywher.
01:22:35 <pikhq> "æ" and "oe" become "e" in Latin in the Middle Ages. And then they got re-expanded *the wrong way*.
01:22:43 <uorygl> I use "ae" inconsistently.
01:22:57 <pikhq> And quite often the "reversion" happened *when it had never been there*.
01:23:05 <uorygl> I like aesthetics and anaesthesia, but I would never consult an encyclopaedia.
01:23:11 <alise> Do you agree that "sthetic" and "dmon" are correct?
01:23:14 <pikhq> For instance: it's fucking "fetus", not "foetus".
01:23:19 <uorygl> And I really hate paedophiles.
01:23:22 <alise> Although I'm not sure I wouldn't write "demon".
01:23:47 <alise> And encyclopdia? What about pdophilia?
01:23:57 <alise> I didn't know ftus was incorrect.
01:24:02 <alise> Is it ftus, then? :P
01:24:10 <pikhq> No, it's always been "fetus".
01:24:29 <alise> Aww, ftus looks so much better :-P
01:24:36 <alise> "The word fetus is from the Latin fetus, meaning delicious,"
01:25:09 <pikhq> "encyclopaedia" is the Latin spelling.
01:25:22 -!- Rugxulo has quit (Quit: Rugxulo).
01:25:40 <uorygl> Hey, neat, "encyclopedia" means "circular education".
01:25:41 <pikhq> "pedophilia", "paedophilia", and
01:25:50 <pikhq> "pædophilia" are all completely bizarre.
01:26:01 <pikhq> They come from "paidophilos".
01:26:43 <alise> Well I'm not spelling it paidophilia, so what should I do?
01:26:49 <alise> Also, encyclopdia is nice, so I'm going to keep spelling it that way.
01:26:59 <alise> At least encyclopaedia; I refuse to devolve into writing encyclopedia.
01:27:04 <pikhq> Also, how do you pronounce "foetus", anyways? "foe - etus"?
01:27:39 -!- Tritonio_GR has quit (Read error: Connection reset by peer).
01:27:56 <alise> Hmm, pedophilia is a hard word. (Har har)
01:28:25 <alise> It seems to have gone from Latin to paedophilia in German to pedophilia in English.
01:30:27 <alise> The Encyclopdia Britannica is a preminent encyclopdia.
01:30:27 <alise> 1. Note: The author does not actually believe this.
01:31:35 <pikhq> Mmm, delicious diaresis and actually correct uses of ligatures.
01:32:00 <alise> diarsis, you uncouth bastard.
01:32:18 <alise> The only problem with that word is that it makes me think of diarrhea.
01:32:49 <pikhq> We were both wrong.
01:33:16 <pikhq> It's "dieresis", "diaeresis", or "diæresis".
01:33:47 <alise> Anyway, can I have a lot of money? I have an urge to buy some wonderfully-printed books.
01:36:05 <pikhq> ... And Fox News goes off the deep end *again*.
01:36:13 <pikhq> Calling Mr. Rogers evil.
01:36:24 <alise> I read the reddit comments on that; apparently the evil mark was clearly a joke.
01:36:46 <alise> 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 <alise> Anyway, less jabbering, more money to me.
01:38:50 * Sgeo loves not hanging out with friends on his birthday :(
01:38:59 <alise> Quit whining and do something interesting.
01:39:11 <alise> (Good life advice most of the time, actually.)
01:39:23 <Sgeo> alise, I don't know how
01:39:32 <uorygl> It's difficult to do something interesting when you feel like something bad is going to happen.
01:39:43 <alise> Well, don't we count as friends? :P
01:39:51 <alise> Sgeo: Think about things you're interested in, then wait; Eureka, now write down what you thought.
01:39:55 <uorygl> Like right now. I feel like as a result of my choices, the outcome is going to be unacceptable.
01:40:07 <alise> uorygl: Which choices?
01:40:11 <uorygl> And so now whenever I think about doing something, I go "aiee!"
01:40:32 <uorygl> alise: choices like going to the wrong college and not doing the required work.
01:40:41 <uorygl> And also failing to take advantage of opportunities.
01:40:44 <alise> uorygl: How old are you again?
01:40:46 <uorygl> And not making friends on campus.
01:40:57 <Sgeo> I've been going to arguably the wrong college for almost 3 years
01:41:19 <alise> uorygl: Well, you are still very young, then, and your college studies have only just started.
01:41:25 <Sgeo> Also, most of my college friends approached me. I didn't ever initiate friendships
01:41:25 <ais523> alise: what am I supposed to be outraged at?
01:41:27 <alise> You can easily go to another college and work harder there with no disadvantage at all.
01:41:29 <Sgeo> Well, once, very recently
01:41:45 <ais523> wow, I'm surprisingly good at feeling generically angry
01:41:50 <ais523> as in, I surprised myself
01:41:56 <ais523> I actually am angry atm, and I have no idea what at
01:41:56 <alise> 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 <alise> ais523: MR ROGERS! HNRRRRRRRRRR!
01:42:29 <uorygl> Hmm, now I feel like I don't know what to be scared about.
01:42:45 <ais523> uorygl: oil spills off the US coast? the entire economy about to collapse? politics in general?
01:42:55 <ais523> exploding supervolcanos? the LHC creating black holes?
01:43:06 <alise> Chickens taking over the world???
01:43:08 <uorygl> There, I just thought about a project I'd like to do, and I had a little bit of an "aiee" reaction.
01:43:45 <uorygl> A mathematical prediction market and proof database.
01:43:57 <alise> Lay off the Robin Hanson.
01:44:43 <uorygl> Robin Hanson came up with a specific application of prediction markets. My project idea has nothing to do with Robin Hanson.
01:44:59 <alise> Yeah, but Hanson is a big fan of prediction markets. So there :P
01:45:20 <alise> Well, okay, O'Connor likes them too and O'Connor is cool, so you're permitted.
01:45:28 <alise> What language would the proofs be in?
01:45:35 <uorygl> Also, I'm not a person who has negative feelings about Robin Hanson.
01:45:38 <alise> Some constructive one like Coq or Isabelle?
01:45:46 <alise> Ivor is not a proof language.
01:45:51 <alise> It is just a Haskell library.
01:45:53 <alise> Do you mean Idris?
01:45:56 <alise> That is not very proof-focused at all.
01:46:14 <alise> 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:27 <alise> I'd strongly suggest Coq or Isar+Isabelle.
01:46:48 <uorygl> Well, okay. I'm not familiar with Coq whatsoever (modulo grammar), so what advantages does it have over something like Agda?
01:46:54 <alise> 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 <alise> uorygl: Here's why Agda is totally unsuitable for this:
01:47:27 <alise> - 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 <alise> It has only been proved inconsistent once, I think, and that was a bug in Coq, not the underlying theory.
01:47:47 <alise> And was very easily fixed.
01:47:54 <alise> (And the example was a very contrived one).
01:48:27 <alise> - 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 <alise> 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 <alise> And finally, Coq has actual practical proofs underlying it -- Goedel's First Incompleteness Theorem, for instance.
01:49:01 <alise> Nobody really uses Agda.
01:49:15 <alise> 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 <pikhq> 'A patent pool is being assembled to go after Theora and other “open source” codecs now.' -- Steve Jobs.
01:49:47 <pikhq> So. Fuck you, Steve Jobs. You make Microsoft look open.
01:49:51 <alise> 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 <alise> uorygl: And that's most of what I have to say on the matter!
01:50:07 <uorygl> 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 <alise> pikhq: Yup, I pretty much hate Steve Jobs now.
01:50:27 <uorygl> What you say about the interactive proving stuff makes sense.
01:50:33 <alise> 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 <ais523> alise: Steve Jobs specifically, or Apple in general?
01:50:43 <ais523> I can think of arguments for either
01:50:44 <alise> Idris is a competent dependently-typed programming language based on it, but with next to no proof infrastructure.
01:51:03 <ais523> in other news, apparently IE9 <video> supports only H.264
01:51:09 <uorygl> The fact that Ivor is a library is precisely why I wanted it.
01:51:22 <ais523> so it seems Microsoft are more afraid of Firefox than Safari
01:51:37 <uorygl> If the theory underlying Ivor is the same as that of Coq, doesn't that mean you can use Coq to create a proof and Ivor to verify it?
01:51:55 <alise> uorygl: Right, but build a tactic or declarative proof engine, with all the necessary underlying tactics and intelligence, etc., plus interactive interface?
01:52:04 <alise> Seems pointless unless you're going to add something over Coq and similar.
01:52:09 <alise> Theoretically yes, but you'd have to translate their notations etc.
01:52:22 <alise> And I think Coq has a few small extensions to the theory (that are almost-certainly-consistent; and you can disable them)
01:53:37 <alise> uorygl: Mind you, I'd wait for /my/ language which will make /everything/ great...
01:54:03 <uorygl> Mmkay, so Coq has a front-end that makes it easy to create proofs. I guess that's the important thing.
01:54:19 <pikhq> ais523: Yes, but Microsoft being Microsoft, they'll probably implement h.264 so poorly that it's actually m.264.
01:54:27 <alise> Yes. But the resulting proofs aren't all that readable. But you can step through them and understand them. They just often need more documentation than a declarative proof.
01:54:32 <uorygl> It would make me happy if I could use a language that has a direct Haskell interface, but I guess that's not necessary.
01:54:36 <alise> There is a declarative extension to Coq but it isn't much.
01:54:42 <alise> uorygl: You won't need that for proofs.
01:54:51 <alise> uorygl: Now, another suggestion I have to make: avoid Coq's standard library numerics.
01:54:53 <pikhq> No, I'm giving a name to the inevitably broken implementation they will have.
01:54:57 <alise> In fact, I'd avoid most of Coq's library altogether.
01:55:08 <pikhq> I shall stick this alongside MHTML and MCSS.
01:55:11 <alise> It is not all the formally constructed. You will want to build things up from magmas onwards.
01:55:13 <ais523> how badly /can/ you break a video codec?
01:55:25 <alise> pikhq: MJavascript = JScript
01:55:26 <ais523> without it being obviously wrong?
01:55:32 <alise> *all that formally
01:55:43 -!- Rugxulo has joined.
01:55:47 <uorygl> I wonder if I had a concrete reason for wanting to go with something written in Haskell.
01:55:57 <alise> Lunacy? Haskell addiction? :)
01:56:00 <pikhq> ais523: These are the guys who stuck 3 boolean types in their API.
01:56:22 <uorygl> I didn't want to go through all the trouble of making one program run another program? :P
01:56:28 <pikhq> One of which is only a boolean in *name*.
01:56:31 <ais523> pikhq: ok, point granted, but that seems easier to do for insane reasons than messing up a video codec such that it's broken but not obviously so
01:56:33 <alise> uorygl: I warn you that if you travel down the wondrous path of type theory-based theorem provers, you /will/ find yourself at the very bottom, musing about the turtles.
01:56:41 <alise> You might even start to believe there's an end to them... but that's just madness, isn't it?
01:56:45 <ais523> I thought they had at least 0/1, yes/no, on/off, true/false
01:56:53 <pikhq> BOOL, BOOLEAN, and TRUE_BOOLEAN
01:56:57 <alise> What I'm trying to say is expect to start taking the metainformation like quantifiers and arrows and the like from mathematical statements,
01:57:01 <alise> then removing all the rest
01:57:04 <alise> and jumbling it up a bit
01:57:12 <pikhq> int with 0 and 1, short with 0 and -1, and char with -1 and 0, IIRC.
01:57:15 <alise> and then you'll consider that just as useful & relevant.
01:57:34 <pikhq> And some functions returning BOOLEAN will also return 1.
01:57:42 <pikhq> As a third possible result.
01:58:22 <alise> Most languages have a FILE_NOT_FOUND; ⊥.
01:58:36 <Rugxulo> pikhq, who are you talking about?
01:58:43 <pikhq> alise: This is in addition to ⊥.
01:58:45 <pikhq> Rugxulo: Microsoft.
01:58:55 * uorygl decides that the gate {0 -> 0, 1 -> 1} should be called an OT gate.
01:59:11 <pikhq> uorygl: I call it "a piece of wire".
01:59:37 <uorygl> Such things actually find a useful place in electonics.
01:59:53 <uorygl> Suppose you have one gate whose output is used as the input to 65,536 other gates.
02:00:04 <alise> uorygl: Also, if you venture down constructivist ways, be expected to have your intuition defied.
02:00:05 <uorygl> One gate can't provide that much output current, so you use a bunch of OT gates to help.
02:00:05 <pikhq> Yes, wires are useful.
02:00:08 <ais523> uorygl: I call {00 -> 0, 01 -> 0, 10 -> 1, 11 -> 1} a MOV gate
02:00:11 <ais523> after the asm instruction
02:00:25 <alise> For instance, the most common construction of the subset of the reals you can construct, you can't prove the trichotomy of the reals in.
02:00:30 <uorygl> ais523: I like that name.
02:00:30 <alise> But I think there are constructions which alleviate this.
02:00:47 <pikhq> Rugxulo: Yes, those 3 types are all normal parts of the Win32 API.
02:00:52 <pikhq> *And* the Win16 API.
02:00:59 * uorygl ponders how you prove the trichotomy of the reals in Dedekind cuts.
02:01:03 <ais523> the win32 and win16 APIs have the same tpyes
02:01:07 <ais523> they're just different sizes
02:01:14 <pikhq> Oh, and note that those are uppercase typedefs.
02:01:16 <alise> uorygl: appeal to not-not, basically
02:01:29 <alise> there is no real that doesn't satisfy some horn of the trichotomy
02:01:32 <uorygl> Ooh, right, and not-not doesn't exist in intuitionistic logic.
02:01:33 <pikhq> In addition to their random hungarian typedefs and such.
02:01:34 <alise> therefore all reals satisfy it
02:01:40 <pikhq> They also have a CHARP typedef.
02:01:48 <alise> uorygl: i don't think you can do dedekind cuts in constructivist settings... dunno
02:01:48 <pikhq> It is, unsurprisingly, a char*.
02:01:53 <alise> uorygl: mostly we do it as cauchy sequences
02:02:05 <alise> f : Q+ -> Q, such that forall e1, e2:Q+, |f e1 - f e2| <= e1 + e2
02:02:05 <uorygl> Well, yeah, you'd have to pretty much write a function that takes two reals and compares them.
02:02:15 <alise> but I'm thinking a continued fraction representation might be nicer
02:02:19 <ais523> pikhq: one of the most memorable bits of the Win32 API is the way it uses lpcsz as a relatively common Hungarian prefix
02:02:25 <ais523> for "long pointer to constant zero-terminated string"
02:02:40 <alise> because i think you can prove <0 =0 >0
02:02:41 <uorygl> If you represent a real number as a predicate on rational numbers, then... darn, you don't get equality.
02:02:45 <alise> and indeed <rat =rat >rat
02:02:50 <uorygl> Lots of stuff is uncomputable, of course.
02:02:52 <alise> but not <irrat =irrat >irrat
02:02:58 <alise> (because comparing infinite structures is impossible)
02:03:04 <uorygl> I'd like to simply use a NotNot monad!
02:03:04 <alise> so, yeah, it's just all compromises
02:03:18 <ais523> alise: does the definition rule out the possibility of infinitesimals?
02:03:18 <alise> uorygl: otoh, you can just axiomatise the reals and not give a shit that there's no model of your axioms
02:03:29 <alise> ais523: infinitesimals aren't even reals in non-standard analysis.
02:03:34 <ais523> does it rule out the possibility of a smallest positive number?
02:03:38 <uorygl> I once tried to write ZFC in Agda as a term model.
02:03:42 <ais523> but that doesn't mean that axioms would necessarily rule them out
02:03:47 <ais523> unless they were written for the possibility
02:03:49 <uorygl> I like the idea of simply writing the axioms.
02:03:50 <alise> I guess inftes = [0; 0, 0, 0, ...infinite 0s..., 1]
02:03:59 <alise> uorygl: But that's very unconstructivist, and constructions are Nice.
02:04:01 <ais523> I'm trying to think of possible flaws in the axioms
02:04:12 <alise> uorygl: If you're going down that route, just add the LEM as an axiom.
02:04:32 <uorygl> Well, then half my proofs wouldn't be runnable! Which isn't much of a problem.
02:04:32 <alise> I'm interested in the best construction of the computable reals. So ask me sometime if you're interested too.
02:04:41 <uorygl> But I'd rather mark which ones are runnable and which aren't.
02:04:42 <alise> uorygl: But you also wouldn't be able to write /programs/.
02:04:52 <alise> And programs are nice, especially when they're all theoretical and shizz.
02:05:01 <alise> pikhq: most useful.
02:05:11 <alise> http://en.wikipedia.org/wiki/Tarski%27s_axiomatization_of_the_reals are pretty
02:05:20 <alise> Now back to people giving me money!
02:05:43 * pikhq gives alise $100i.
02:05:59 <uorygl> I don't know how I would feel about receiving $100i.
02:06:00 <ais523> alise: why are you demanding money?
02:06:04 <alise> I need real (actually, rational) money to buy prettily-printed books.
02:06:04 <ais523> and why are you expecting to /get/ it?
02:06:17 <alise> ais523: Because I'm adorable.
02:06:23 <ais523> uorygl: ambivalent, I suppose
02:06:31 <pikhq> uorygl: It'd certainly make your accounting complex.
02:06:37 <alise> As for your first question, because I'm trying to get some money to [waste?].
02:07:10 <uorygl> If I wanted to have exactly a certain amount of money, I would be disappointed at receiving $100i.
02:07:20 <alise> Unless you wanted $100i.
02:07:30 <ais523> uorygl: you could always give it to someone else
02:07:41 <alise> No, that'd be too complex.
02:07:42 <ais523> hmm, I wonder if you should accept $100i or not if someone offers it to you
02:07:43 <alise> It's imaginary money.
02:07:44 <uorygl> If I had a real amount of money and wanted exactly a certain real amount of money.
02:07:49 <ais523> after all, if they offer you a negative amount of money, you should refuse
02:07:54 <alise> ais523: That's a complex matter...
02:08:06 <ais523> has this turned into the IRC equivalent of a pun thread?
02:08:17 <alise> I think it's imaginary.
02:08:24 <pikhq> uorygl: I strongly suspect you want a subset of a real amount of money.
02:08:24 <alise> ...not too many puns, really.
02:08:32 <uorygl> Well, if people can simply give each other arbitrary amounts of money, positive or negative, then there's no reason to worry about money, because you can always get money.
02:09:06 <pikhq> Probably a positive real amount.
02:09:06 <uorygl> Intuitively, I think the positive amounts of money should be defined as those where the absolute value of the imaginary part is less than the real part.
02:09:08 <ais523> uorygl: well, assuming gifts can be refused
02:09:27 <uorygl> Well, you have to define the amounts of money that a person can have.
02:09:37 <uorygl> If I have $5, I can't give someone $8 and be left with $-3.
02:09:39 <pikhq> Or if you prefer being easy to deal with, a positive *computable real* amount.
02:09:42 <ais523> uorygl: but if you had an imaginary amount of imaginary money, wouldn't it have a negative absolute value?
02:09:53 <uorygl> Whatever you just said, no.
02:10:03 <pikhq> (not having a mapping to the naturals makes my computer cry)
02:10:10 <ais523> I'd love to find a mathematical theory in which that /did/ work, though
02:10:29 <uorygl> We'll say that the amount of money you have must always be an integer.
02:10:54 <uorygl> If you have $100i, you must gamble until that amount becomes an integer number of cents.
02:11:01 <uorygl> Whichever; it doesn't matter.
02:11:19 <alise> Incidentally, Ripple.
02:11:50 <pikhq> So. Zimbabwe cents then.
02:13:09 <pikhq> The metal in such a coin would be worth 30-odd orders of magnitude more than the coin itself.
02:13:24 <uorygl> Assume that you don't have access to the coin itself, just the money. :P
02:13:52 <pikhq> (mmm, 6.5*10^108% inflation...)
02:14:06 <alise> Zimbabwe reset their currency recently; then abandoned it altogether.
02:14:32 <uorygl> Anyway, we can say that anyone is allowed to gamble in any manner as long as the gamble is fair, and has no chance of causing the person's amount of money to become negative.
02:15:59 <uorygl> Then we'll define "negative" as the absolute value of the imaginary part being greater than the real part.
02:16:17 <alise> It isn't really gambling if it isn't risky. :P
02:16:33 <uorygl> If I have $100, betting $100 is risky!
02:16:37 <pikhq> "I gamble 1 billion dollars" 1 loss away "Yeah, I don't have 1 billion dollars" "You owe me all the money bitch." Bam. Negative money.
02:16:39 <ais523> alise: it is risky, because you might go from a positive ownership to a smaller positive ownership
02:16:55 <uorygl> So, suppose I have $100, and somebody gives me $100i. Now the amount of money I have is on the very border of being negative.
02:17:00 <pikhq> (or, more likely, negative life-having)
02:17:05 <uorygl> And no gamble I can make can push me away from that.
02:17:11 <ais523> pikhq: in other words, zero-equivalent?
02:17:12 <uorygl> So this seems like a pretty bad thing.
02:17:20 -!- cheater2 has quit (Ping timeout: 276 seconds).
02:17:42 <uorygl> Of course, if I have $100 + $100i (bad) and someone else has $100 - $100i (also bad), we can just trade and each end up with $100 (good).
02:18:01 <ais523> Subject: [SPAM?] ?spam? Stop spamming
02:18:06 <ais523> spammers get more creative all the time...
02:18:23 <uorygl> So in this system, having imaginary amounts of money is generally a bad thing, I think.
02:18:43 <ais523> uorygl: you've defined three quarter-planes as negative, and the other as positive
02:18:59 <uorygl> Yes, that's what I meant to do.
02:19:39 <fizzie> Sneak-peek on the current incoming spam: there's one with a RTF attachment. I haven't seen very much of that.
02:20:06 <ais523> hmm, I wonder if it contains an exploit?
02:20:31 <fizzie> Well, I looked at it with a text editor; it seems to just contain some hyperlinks to .ru URL's, and that's about it.
02:20:42 <fizzie> Also \generator Msftedit 1.32.47.3014;
02:23:15 -!- cheater2 has joined.
02:24:14 <ais523> <http://www.reddit.com/r/programming/comments/byilp/c_compilers_disprove_fermats_last_theorem/>: could some redditor point out that signed overflow in C is undefined?
02:24:18 <ais523> they all seem to have missed the fact
02:24:32 <ais523> a compiler can optimise a loop into anything at all if it can prove that it requires an integer overflow at some point
02:26:35 <fizzie> Does the original thing require an integer overflow? The a, b, c integers there are limited to be <= 1000, after all.
02:27:42 <ais523> hmm, missed the difference between MAX and INT_MAX
02:28:26 <fizzie> It does say in the text that MAX=1000 because 2*1000^3 is still <2^31.
02:34:55 <fizzie> It's a bit curious if they throw away a reasonable infinite loop like that. My version of clang doesn't.
02:35:26 <fizzie> Maybe I have just not enabled enough optimilizations.
02:49:04 -!- bsmntbombdood has joined.
02:55:58 <Rugxulo> gah, someone test that please
02:56:49 <Rugxulo> hmmm, okay, never mind, that doesn't show what I wanted anyways
02:57:08 <Rugxulo> try this: &:+.@ (where your input is -5)
02:57:42 <Rugxulo> bef = good, fbbi or ccbi = bad
03:01:18 -!- Alex3012 has quit (Disconnected by services).
03:04:25 -!- pikhq has quit (Read error: Connection reset by peer).
03:08:22 <fizzie> & does not read negative numbers.
03:08:57 <Rugxulo> the original interpreter handles it okay
03:09:08 <fizzie> "Decimal input reads and discards characters until it encounters decimal digit characters, at which point it reads a decimal number from those digits, --"
03:09:37 <Rugxulo> but Befunge inherently handles a signed 32-bit stack!
03:09:48 <Rugxulo> it can print negative numbers too, so why not accept them as input?
03:10:26 <Rugxulo> case '&': /* Input Integer */
03:10:41 <fizzie> That's even more wrong then.
03:10:59 <Rugxulo> which, the spec or the author or (God forbid) someone else ;-)
03:11:18 <fizzie> The code you pasted, w.r.t the spec.
03:11:23 <fizzie> There's a very strictly specified behaviour when the number would overflow.
03:11:48 <fizzie> Specifically, it must not read the digit that would cause an overflow.
03:12:24 <fizzie> It reads "up until (but not including) the point at which input characters stop being digits, or the point where the next digit would cause a cell overflow, whichever comes first."
03:12:57 <Rugxulo> I don't know if I agree that he strictly meant '0'..'9' as "digits" here
03:13:07 <Rugxulo> I assume he just meant signed long int
03:13:47 <fizzie> But those *are* decimal digits. And anyway I don't think fscanf would unread the digit that would cause an overflow.
03:13:55 <fizzie> I think that since the spec is so very detailed, people have generally taken it pretty literally.
03:14:09 <Rugxulo> FBBI does it like you say (apparently), and it does indeed do ungetc()
03:14:22 <Rugxulo> are you referring to B93 or B98 here?
03:14:41 <fizzie> That fscanf won't even skip the non-digits in front, just space.
03:14:59 <Rugxulo> i->a = (long)0|fgetc(stdin);
03:15:00 <Rugxulo> if ((i->a >= '0') && (i->a <= '9')) ungetc(i->a, stdin);
03:15:00 <Rugxulo> } while ((i->a < '0') || (i->a > '9'));
03:15:01 <Rugxulo> if(scanf ("%ld", &i->a) != EOF)
03:15:18 <fizzie> B98 is what I quoted, have to check B93 too.
03:15:30 <Rugxulo> that's from fbbi (just quoted)
03:16:29 <fizzie> Well, it's "get a numeric value (in decimal)" for B93, so you have much more freedom for variation there.
03:18:38 <fizzie> That fbbi code seems to properly skip non-digits until it encounters a digit, but I don't think it necessarily reads the number itself right, unless scanf's %d conversion guarantees that (it just might).
03:20:28 <fizzie> Didn't notice anything like that in my man page though.
03:24:53 <Rugxulo> but I don't see why it wouldn't let you do so, esp. if it handles signed numbers by default
03:25:32 <fizzie> The Funge-98 overflow check is not completely trivial to implement, since it isn't just a length limit; for 32-bit cells, if you've read "214748364" so far, you must read the next digit if it's 0..7, but leave it in the stream if it's 8 or 9.
03:25:49 -!- pikhq has joined.
03:25:53 -!- pikhq has quit (Read error: Connection reset by peer).
03:26:12 <Rugxulo> I don't really know C, but I thought it handled these things
03:26:13 <fizzie> And of course in C you can't let the actual overflow happen.
03:26:44 <Rugxulo> maybe I'm thinking of strtol(), I dunno
03:27:51 <fizzie> It doesn't: "if the result of the conversion cannot
03:27:55 <fizzie> be represented in the space provided, the behaviour is undefined"
03:28:32 <fizzie> (Source: interwebs; reading the standards is too awkward with the phone.)
03:29:45 <fizzie> strtol doesn't do it right either; it reads all digits and clamps the value to LONG_MAX.
03:30:20 <fizzie> Or, well, you could say that's "right", but not the Funge-98 right.
03:31:00 <fizzie> (The "it" in "it doesn't" up there was scanf.)
03:31:01 -!- pikhq has joined.
03:31:09 -!- Alex3012 has joined.
03:32:49 <Rugxulo> entering -3 billion for bef prints 1294967296
03:33:07 <Rugxulo> for fbbi, same input prints -1294967296
03:33:45 <fizzie> It should give 300 million.
03:34:14 <Rugxulo> ccbi is correct and fbbi is wrong, then
03:34:25 <fizzie> As for why it doesn't handle negative numbers: like I said, since the spec is so exact on the number-reading algorithm, people (at least those I know) have just been implementing exactly what it says there without customizations.
03:34:39 <Rugxulo> which, IMHO, is a bit suspect since I assume the original creator/author knew what he was doing ;-)
03:35:14 <fizzie> Well, it's not quite like the t case, for which the spec taken literally is quite useless.
03:36:17 * Rugxulo is also testing Parrot + their Befunge [93] a bit
03:38:01 <Rugxulo> seems they had two minor bugs, and I'm not sure I pointed out (fixed?) them correctly, honestly not sure they even *care* (argh), but anyways, done my duty trying ;-)
03:38:25 <Rugxulo> make that three bugs, but the third has to do with not loading a .dll file correctly (and I dunno why, only found silly workaround)
03:39:09 <Sgeo> Is Exploit potentially TC?
03:40:28 <fizzie> Nights, now; already around 05:40am here.
03:41:56 <alise> i love finite derivatives so much
03:51:55 -!- Rugxulo has quit (Quit: bored).
04:12:14 -!- pineapple has quit (Ping timeout: 246 seconds).
04:13:53 <alise> I need to: yawn. No, sleep.
04:13:55 <alise> Motivation stores are empty.
04:14:50 <Sgeo> Wooo! Just finished the story mode of Exploit
04:16:20 <alise> Sleep! Must sleep! -- no sleep; fuckitol.
04:17:26 * Sgeo puts alise to sleep
04:17:37 <alise> Permanenterelrely?
04:18:03 <alise> When you can extenderlongeratitionermatabilityenactingnesserateabilitynesseratinger a word, that means you are tired
04:18:31 * Sgeo is either creepy or a murderer, depending on how you look at what I said
04:18:44 <Sgeo> Hm, creepy either way, really
04:19:46 <alise> Yeah, pretty creppy
04:20:59 <alise> Federal 4:20 am it is
04:53:15 -!- lament has joined.
04:56:59 -!- lament has changed nick to melament.
04:58:50 -!- melament has changed nick to lament.
05:05:32 <alise> Gregor: ping; if you don't respond I may get so bored as to actually embed myself
05:06:48 * Sgeo embeds alise in a webpa.. that sounds WRONG, and I just wanted to sound geeky
05:08:46 -!- lament has left (?).
05:16:06 <alise> Gregor: that irex thing
05:16:15 <alise> is there anything for it with some form of handwriting recog?
05:16:37 <Gregor> Not to my knowledge, but if there's anything for GTK+ it may be portable to the IREX.
05:16:57 <alise> I'm just thinking about it as a platform for mathsy stuff.
05:17:11 <alise> Being able to scribble mathematical notation and have it interpreted would be ubernice. Still that response time though.
05:18:38 <Gregor> Frankly I think you've got a pipe dream thar :P
05:18:51 <alise> mathematical notation recognition is actually pretty alright
05:18:58 <alise> it's just the stupid eink :(
05:19:25 <alise> Hmm, you know the ... what is it, Graffiti - input thing for PDA?
05:19:32 <alise> Where you, like, draw specialised symbols.
05:19:38 <alise> Anything like that for the rexy i?
05:20:56 <Gregor> The IREX has only an onscreen keyboard as its default input method for general text.
05:21:08 <alise> Yess but has anyone ported anything else
05:22:04 <Gregor> That might be even simpler, it uses Matchbox and Matchbox has such a thing already IIRC.
05:23:02 <Gregor> The DR800 is reeeelatively new, very little has been ported to it. I was the first person to port rxvt to it, so that should give you an idea.
05:25:12 <Gregor> I don't know. Certainly the overpriced Euro one isn't, but if you can get a US one shipped, maybe.
05:27:06 <alise> I just can't bring myself to buy an internet-using, lovely-tablet-screen-having, X11-running mobile device that isn't useful for IRC.
05:27:11 <alise> So some good input method is a must.
05:28:08 <Gregor> I just ported cellwriter to it, let's see if it's useful :P
05:29:23 <alise> It's 5:28 am. you are not helping! :)
05:29:38 <alise> so given up on the wearable computing thing eh
05:29:50 <alise> "IREX Technologies is the world's leading provider of e-reading solutions" yeah sure
05:38:01 <alise> i need to know before i bludgeon myself to sleep
05:38:37 <Gregor> My porting job was sufficiently incomplete that I don't have an answer, it shows up as a full screen app and as such can't be used to actually input into anything yet :P
05:39:46 <alise> hurry up this is actually physically hurting me :P
05:39:52 <Sgeo> Hey, Android soft keyboards are fullscreen, and useful for input
05:41:18 <Gregor> That's useful on touch, not tablet.
05:43:06 <alise> fucking awesome tablet made of rocks
05:43:14 <alise> and now that is my signal that it is almost 6 am.
05:44:22 <alise> "imperviosity" rhymes with "having sex with a tree"
05:45:08 <alise> just thought you might like to know
05:48:17 <alise> also "glorious midgets that are also alteregos of a doctor" does not rhyme with "glue"
05:48:31 <alise> and at that point i ask Gregor once more before embedding myself
05:52:29 <alise> Gregor: ANSWER MY FUZUKING QUESTION YOU tree :|
05:54:48 <alise> Gregor: I will haunt you 4eva 'n eva
05:58:12 <alise> Gregor: PLEASE ANSWER ME :(
05:59:33 -!- bsmntbombdood_ has joined.
05:59:40 * Sgeo watches alise die from sleep deprivation
05:59:43 -!- Oranjer has quit (Quit: Leaving.).
06:00:16 -!- alise has quit (Remote host closed the connection).
06:03:00 -!- bsmntbombdood has quit (Ping timeout: 276 seconds).
06:05:54 -!- Oranjer has joined.
06:14:53 -!- oerjan has joined.
06:21:28 -!- sebbu2 has joined.
06:22:16 -!- sebbu has quit (Ping timeout: 240 seconds).
06:22:17 -!- sebbu2 has changed nick to sebbu.
06:27:16 -!- jcp has quit (Read error: Connection reset by peer).
06:28:21 -!- jcp has joined.
06:59:18 -!- oerjan has quit (Quit: leaving).
07:15:51 -!- Oranjer has left (?).
07:23:14 -!- bsmntbombdood_ has quit (Remote host closed the connection).
07:32:40 -!- ais523 has quit (Remote host closed the connection).
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:04:19 -!- jcp has quit (Quit: I will do anything (almost) for a new router.).
09:25:54 -!- Gracenotes has quit (Quit: Leaving).
09:27:20 -!- hiato has joined.
09:34:22 -!- Phantom_Hoover has joined.
09:34:54 -!- BeholdMyGlory has joined.
09:51:38 -!- Phantom_Hoover has quit (Remote host closed the connection).
10:00:14 <AnMaster> <Rugxulo> AnMaster, which MicroEmacs? the most "active" variant was/is JASSPA <-- good point
10:32:10 -!- adam_d has joined.
10:33:56 -!- tombom has joined.
10:37:34 -!- Gracenotes has joined.
11:09:43 -!- FireFly has joined.
11:21:05 -!- hiato has quit (Quit: underflow).
11:47:51 -!- sebbu has quit (Ping timeout: 260 seconds).
11:53:33 -!- sebbu has joined.
12:19:54 -!- hiato has joined.
12:40:26 -!- rodgort has quit (Quit: Coyote finally caught me).
12:40:34 -!- rodgort has joined.
12:48:59 -!- tombom has quit (Quit: Leaving).
13:28:10 -!- jmorrow has joined.
13:44:16 -!- augur has quit (Remote host closed the connection).
13:44:27 -!- augur has joined.
13:46:43 -!- augur has quit (Remote host closed the connection).
13:46:49 -!- augur has joined.
13:46:50 -!- augur has quit (Remote host closed the connection).
13:46:55 -!- augur has joined.
13:51:12 -!- augur has quit (Remote host closed the connection).
13:51:17 -!- augur has joined.
14:01:24 -!- hiato has quit (Quit: underflow).
14:01:44 -!- hiato has joined.
14:01:52 -!- jmorrow has quit (Quit: Leaving.).
14:20:42 -!- hiato has quit (Remote host closed the connection).
14:21:00 -!- hiato has joined.
14:24:49 -!- MizardX has joined.
14:28:58 -!- augur has quit (Remote host closed the connection).
14:29:04 -!- augur has joined.
14:42:07 -!- oerjan has joined.
14:51:34 -!- alise has joined.
14:52:39 <alise> Gregor: so did it work
14:57:47 -!- alise has quit (Ping timeout: 252 seconds).
15:08:06 -!- hiato has quit (Quit: quit quit quit quit quit quit quit).
15:24:55 -!- alise has joined.
15:53:28 -!- oerjan has quit (Quit: Reboot).
15:54:33 <alise> non-player-shmaracter
15:56:30 -!- oerjan has joined.
16:11:44 <oerjan> oh well, it's over a month since the last one
16:11:53 <oerjan> it just looks a lot when no one posts there :D
16:18:13 <oerjan> is "pushed on the stack" and "pushed to the stack" equally valid?
16:19:13 -!- pineapple has joined.
16:20:03 * oerjan is trying to proofread the Calculon article
16:21:05 <alise> oerjan: both are valid, yes
16:21:15 <alise> Pushed to sounds weird
16:21:25 <alise> 0-9 -- The value is pushed onto the stack.
16:21:54 <oerjan> AnMaster: no need to answer btw, alise already did ;)
16:22:39 <oerjan> calculon's argument order seems to be the reverse of forth
16:24:20 <AnMaster> when you can't find some well established software in debian repos you know it is some very niche you are dealing with...
16:24:33 <AnMaster> (in this case, a cycle accurate x86 simulator)
16:24:44 * oerjan changes first and last to top and bottom for clarity
16:25:02 <AnMaster> oerjan, which way does the stack grow ;P
16:25:10 <AnMaster> if it grows down this may be even more confusing
16:25:32 <oerjan> um i'm assuming "top of stack" is a standard term
16:25:45 <AnMaster> oerjan, true, was just trying to confuse you ;P
16:25:52 <oerjan> think stack of plates on a spring, is what i hear
16:26:04 <oerjan> augur: someone's new language on wiki
16:26:05 <augur> is he the new autobot that does calculus?
16:26:29 <oerjan> basically a slightly weird forth
16:27:31 <alise> botte will do calculus!
16:27:34 <alise> just as soon as i write it.
16:27:53 <oerjan> well the argument order is backwards, and it looks like looping will be a bit weird
16:28:12 <oerjan> possibly. it's still under construction
16:28:47 <augur> http://blog.regehr.org/archives/140
16:28:51 <augur> so this was linked on reddit
16:29:25 <augur> which reminds me of a discussion i had with some idiot somewhere
16:29:34 <augur> about whether or not it was possible to detect infinite loops
16:29:47 <augur> he insisted that to detect _any_ infinite loop required solving the halting problem
16:30:26 <alise> a lot of idiots think that.
16:30:34 <alise> all programs running on our computers can be halt-checked by a supersupercomputer
16:30:53 <alise> certainly I'm sure haltchecking a regular 4gb 2ghz dualcore comptuer could be done with a computer that would fit into the universe
16:31:07 <alise> obviously it could be done by a turing machine
16:31:16 <oerjan> augur: well the word "any" is ambiguous in english ;D
16:32:18 <augur> its actually not ambiguous, tho. its a choice function, so it has properties that seem like "all" and properties that seem like "some"
16:33:09 <oerjan> it's ambiguous in that particular context
16:34:05 <augur> no, like i said, its not ambiguous, it's just a choice function which means that it simultaneously has properties of both universal and existential quantification
16:34:13 <AnMaster> #CFLAGS = -O1 -g3 -march=pentium4 -mtune=k8 -falign-functions=16
16:34:13 <oerjan> it's also a weird word to norwegians, we don't really have any that work like that
16:34:24 <AnMaster> that was an interesting definition of no optimisations
16:35:14 <oerjan> (any and some are both translated as "noe(n)", usually)
16:35:33 <AnMaster> The recommended optimisation flags for this are (no this is not cfunge!, nor am I involved in this project): -O3 -g -fomit-frame-pointer -pipe -march=core2 -msse4.1 -falign-functions=16 -funroll-loops -funit-at-a-time -minline-all-stringops -fno-trapping-math -fno-stack-protector -fno-exceptions -fno-rtti -funroll-loops -mpreferred-stack-boundary=4 -fno-strict-aliasing -Wreturn-type
16:37:24 <AnMaster> oerjan, agreed. However, it is an x86 emulator. Those sometimes have special needs
16:37:31 <AnMaster> compared to "usual" programs I mean
16:37:52 <AnMaster> hm it fails to link with "undefined reference to <various libc string functions>"
16:40:26 * alise wonders what the relation to the continuum hypothesis with type theory is
16:40:37 <alise> I wonder if there are types with cardinality inbetween t and (t->bool)...
16:40:40 <AnMaster> okay it seems to be because it doesn't link to libc (duh)
16:40:48 -!- hiato has joined.
16:40:58 <AnMaster> it also uses a custom linker script as far as I can tell
16:42:10 <oerjan> alise: well of course there are, take a finite type
16:42:22 <alise> oerjan: I mean infinite t
16:42:23 <oerjan> if t has 3 elements, t -> bool has 8
16:42:28 <alise> (at least as big as the naturals)
16:42:44 <alise> because my definition of cardinality is based on it...
16:42:53 <oerjan> so the generalized continuum hypothesis, then
16:42:53 <alise> technically my beth numbers can only take naturals not ordinals atm though
16:43:03 <alise> yes. but what is its status in set theory?
16:43:29 <alise> I represent "x has cardinality beth n" (I've avoided aleph because beth is a closer match) by a bijection from x to Infin n
16:43:36 <alise> where infin is repeated ->bools over the naturals
16:43:59 <alise> so of course this only lets you express all cardinalities if the generalised continuum hypothesis holds in set theory... it probably does though
16:44:04 <alise> or at least, is a fine axiom to add
16:44:17 <oerjan> i vaguely recall some result that says you can choose the beths to be a fairly free subset of the alphas
16:44:25 <alise> I wonder how to represent ordinals; I'll need ordinally beth numbers sometime.
16:44:33 <alise> But beth n for natural n will do for now.
16:44:51 <oerjan> there are some restrictions, but a lot of leeway
16:46:08 * alise can now write "nat [has cardinality] beth 0"
16:46:47 <oerjan> alise: cantor normal form can get you a way above the naturals, at least
16:47:24 <alise> in set theory it can, nothing is certain in type theory :)
16:47:31 <alise> Theorem naturals_are_beth_zero : nat [has cardinality] beth 0.
16:47:33 <alise> apply infinite_cardinality.
16:47:33 <alise> exists (id (A:=nat)).
16:47:33 <alise> exists (id (A:=nat)).
16:47:47 <alise> now to prove something more interesting, like option A adding 1 to A's cardinality
16:47:49 <oerjan> alise: well it's pretty certain you get ordinals out of it, i should think
16:47:53 <alise> which means I need cardinal arithmetic
16:48:07 <oerjan> cantor normal form is pretty constructive afaiac
16:48:30 <alise> A [has cardinality] n -> option A [has cardinality] succard n
16:48:38 <alise> You little succard.
16:50:09 <alise> oerjan: the annoying thing is I don't just need ordinal arithmetic
16:50:15 <alise> because I have both "finite n" and "beth n" cardinalities
16:50:20 <alise> so I need separate cardinality-adding functions
16:51:49 <alise> Theorem fin_n_has_cardinality_finite_n {n} : fin n [has cardinality] finite n.
16:52:02 <alise> in_coq_we_often_repeat_ourselves : In Coq, we often repeat ourselves.
17:15:33 <AnMaster> now THIS is strange. the thing work correctly when running under strace or under gdb, but not when running stand alone
17:15:41 <AnMaster> and no there is no core to analyse, it just exits
17:15:52 <AnMaster> oh and I need -f (follow forks) for it to work under strace
17:21:36 -!- MizardX has quit (Ping timeout: 276 seconds).
17:22:56 <Sgeo> It is now legal for me to drink alcohol
17:26:01 <alise> yes, happy birthday!
17:26:05 <alise> I would have said it sooner but you hadn't spoken
17:26:07 -!- MizardX has joined.
17:26:16 <alise> also, don't drink too much booze!
17:26:48 <alise> way too high drinking age
17:27:20 <oerjan> wait it's 21 for _all_ alcohol?
17:27:36 <oerjan> in norway it's 18 for non-distilled
17:30:19 <Gregor> If you can't read Unicode, you şūċķ.
17:31:17 -!- myndzi has joined.
17:32:01 <hiato> Sgeo: happy birthday!
17:32:16 <oerjan> i can, i just have to go to the logs to do it ;)
17:32:35 <oerjan> and to do so i have to suspect the question marks actually aren't
17:33:09 <Gregor> Also, hm, drinking age is that high in Norway?
17:33:21 <Gregor> I thought in most of Europe, it was like non-distilled at 6 and distilled at 12.
17:34:26 -!- myndzi\ has quit (Ping timeout: 246 seconds).
17:34:59 <oerjan> among european countries, norway is pretty conservative in some respects
17:35:02 <Sgeo> Thank you alise and hiato
17:35:31 <alise> Gregor: in the uk it is 16. i think
17:35:41 <oerjan> i think our alcohol laws are the strictest in europe. the alcohol taxes _certainly_ are. ;)
17:35:45 -!- sebbu2 has joined.
17:38:31 <oerjan> http://en.wikipedia.org/wiki/File:Drinking_age_by_country.svg
17:38:47 -!- sebbu has quit (Ping timeout: 260 seconds).
17:38:47 -!- sebbu2 has changed nick to sebbu.
17:38:48 <oerjan> although the norwegian color is for distilled liquor
17:40:18 <oerjan> spain, italy and greece are lower, portugal isn't available
17:40:52 <oerjan> albania has no law, possibly
17:43:01 * oerjan tries a larger version
17:43:09 <oerjan> http://upload.wikimedia.org/wikipedia/commons/thumb/8/8c/Drinking_age_by_country.svg/2000px-Drinking_age_by_country.svg.png
17:43:40 <oerjan> kosovo doesn't seem to be separate from serbia in that map, afaict
17:44:21 <oerjan> (which is blue for 18+)
17:44:44 <hiato> Yeah, looks like one ountry there
17:47:36 * oerjan sees an island east of madagascar marked as orange
17:53:22 <oerjan> (which is not one of the listed colors)
18:08:15 <alise> anyone want to think about SPECIALISATION ?! 111puie4t
18:11:06 <alise> THEORETIC UNTHEORETIC, OERJAN.
18:13:18 <alise> THEOHERETIC THEOUNHERETIC UNTHEOHERETIC
18:14:27 <oerjan> HERE, ORTHOPEDIC HETERODOXIC RETROTHEORETICIANS
18:15:46 <alise> Retrotheohereticians.
18:15:58 <alise> People who are heretical with their opinions about past theoretical works.
18:16:58 <oerjan> well it's all greek to me
18:20:49 <alise> Retrotheohereticians sounds like something out of some really bad nerdcore.
18:22:30 <oerjan> you're aware that -theo- is not the same as -theor- ?
18:26:28 <oerjan> the program's a bit rotten
18:26:59 <AnMaster> oerjan, quite, I'm installing ubuntu hardy in a chroot now, there are some indications that will work
18:30:48 <Sgeo> What, exactly, is comex's involvement with iPhone stuff?
18:31:28 <oerjan> comex: you have been lied to
18:31:36 <comex> oerjan: by whom? :p
18:31:40 <alise> Sgeo: you mean that he's in #iphone-dev?
18:31:50 <alise> presumably he has an iphone, and either jailbreaks it (probably) or uses the proper SDK (unlikely)
18:31:59 <Sgeo> I notice that on Twitter, he's always talking and being mkentioned in iPhone related stuff
18:32:04 <alise> are you trying to get assurance that buying an iPhone is just fine and you can sleep at night with the recent TOS changes? :)
18:32:14 <comex> my involvement is that I'm making a jailbreak.
18:32:20 <alise> gee i guess he works for apple
18:32:26 <alise> because people talk to him about iphones
18:32:33 <alise> can't be just some random guy fucking with an iphone
18:32:53 <Sgeo> alise, it seemed more like a random guy _doing something important_ with an iPhone
18:33:05 <alise> JAILBREAKING IS OF THE UTMOST IMPORTANTANCE
18:33:08 <alise> comex is practically world-famous
18:33:32 <alise> you know it's true
18:36:59 <alise> can you get transparent touchsurfaces?
18:37:01 <alise> a touchscreen without the screen
18:38:17 <Sgeo> Better yet would be a touchscreen that's transparent in parts that aren't displaying anything
18:38:55 <alise> my idea was to put an eink display behind it
18:39:00 <alise> but yours would make that even better
18:39:07 <alise> because you can't really have selective backlight
18:39:13 <alise> with transparent slots when there's no pixels or something
18:39:15 <alise> with eink underneath
18:44:08 <Sgeo> Colored eInk sounds fun
18:44:35 -!- Tritonio_GR has joined.
18:44:57 <alise> Transparent touch-sensitive panel - Patent 4700025
18:44:58 <alise> by M Hatayama - 1987 - Cited by 9 - Related articles
18:44:58 <alise> The transparent touch-sensitive panel of claim 1, wherein said uneven surface has 100 to 10000 protrusions of 0.5 to 5 μm high per cm2. ...
18:44:58 <alise> www.freepatentsonline.com/4700025.html
18:45:01 <alise> Patents, darn, and old, so hmm.
18:45:17 <alise> I want a capacitative, transparent touch surface.
18:45:23 <pikhq> comex: Would you happen to have done anything on the Wii?
18:47:00 <pikhq> Nice work on Bannerbomb.
18:55:50 <alise> i jailbroke this channel
19:01:08 <alise> YOU GUYS DON'T BELIEVE ME
19:01:13 <alise> i totally overflowed its fuzucking buffer yeah.
19:02:20 * pikhq will overflow your horse's name
19:03:29 <oerjan> but it has such a nice flowing mane!
19:04:20 <alise> THAT'S NOT THE ONLY PART OF A HORSE YOU OVERFLOW ON A REGULAR BASIS LOL.
19:08:09 -!- ais523 has joined.
19:12:59 -!- bsmntbombdood has joined.
19:14:37 <alise> ais523: any esolang news?
19:14:42 <alise> bsmntbombdood: are you still using that ubercomputer?
19:15:00 <alise> http://esolangs.org/w/index.php?title=Main_Page&curid=1&diff=17445&oldid=17417 this is utterly pointless
19:15:09 <alise> i would but i'm god.
19:15:14 <alise> (so it wouldn't be fair)
19:16:20 <alise> bsmntbombdood: the one i specced up and you bought
19:16:40 <alise> has it broken yet :)
19:17:04 <alise> i don't /entirely/ believe you...
19:17:21 <alise> is the quantum coprocessor still accessing the qubit ram without errors?
19:17:57 <bsmntbombdood> i really think i should have gone with dual quantum coprocessors
19:18:32 <alise> the newest pi calculating algorithms have to factor a large number /and/ do a reverse lookup in a database simultaneously
19:18:33 <alise> so i can see how that would be a problem
19:19:13 <alise> I'd buy a new heatsink at the same time, because then you could run the fan a lot slower too
19:19:28 <ais523> also, where do you get quantum coprocessors?
19:19:29 <alise> quiet fan + good heatsink = $50, $60?
19:19:37 <alise> ais523: It's a secret.
19:19:48 <bsmntbombdood> i really want megahalems but i don't think they'll clear all the ram slots
19:19:48 <alise> you need a big case for the cooling system though
19:19:53 <alise> (and a government grant)
19:19:59 <alise> bsmntbombdood: yeah the megahalems are massive
19:20:13 <alise> well they are very securely tightened, but yes, they're crazy
19:20:33 <alise> you can get mid-size heatsinks though, and unless you're obsessive about noise like I am it should be just fine
19:20:40 <bsmntbombdood> it does look like people have used thermalight ultra-120s with this board though
19:20:56 <alise> i still haven't bought mine btw :P
19:21:03 <alise> concentrating on moving country first of course.
19:22:49 <bsmntbombdood> it sounds like both coolers can be made super quiet
19:24:24 -!- Mathnerd314 has joined.
19:24:59 <alise> bsmntbombdood: if you're going for tranquility you'll want to get a quieter PSU, too; and maybe even replace the case fans
19:25:03 <bsmntbombdood> going to replace the case fans too, should be able to make it pretty quiet
19:26:18 -!- Gracenotes has quit (Quit: Leaving).
19:26:38 <alise> what os are you running on it? and are you actually utilising the computational power? :P
19:28:06 <alise> wonder what's the most powerful solid state machine you could do...
19:28:12 <alise> would be unnerving, not knowing whether it's on :)
19:28:18 <alise> solid state psu is the hardest thing there
19:28:20 <alise> they just don't make them
19:29:52 <alise> http://www.quietpc.com/gb-en-gbp/products/psus-501-600/x-xp600-fl "mostly fanless"
19:30:12 <alise> http://www.scan.co.uk/Product.aspx?WebProductID=644060&source=froogle again "mostly fanless"
19:30:24 <alise> "The NightJar Fanless PSU series is available in two flavors, 300W and 450W. I'll be reviewing the Nightjar 450W Zero dBA Fanless Power Supply (SST-ST45NF) which peaks at 500W and this is more than enough power for a HTPC or a silent gaming build. This PSU uses solid state Capacitors which results in cleaner more reliable power than cheap capacitors found in many other PSUs on the market. The housing is made from thick aluminum and it acts as a heastink si
19:30:25 <alise> nce this PSU does have a fan to keep it cool. It also has plenty of ventilation holes, but it's crucial to have excellent case ventilation to insure this PSU gets adequate cooling. Watch the video to find out more."
19:30:28 <alise> no actual links though, helpful
19:33:33 -!- MizardX- has joined.
19:34:04 <pikhq> alise: You can actually get PSUs that use an external brick. ;)
19:34:22 <alise> bsmntbombdood: ah which is it
19:34:28 <alise> not the nexus 420 one is it?
19:34:51 -!- MizardX has quit (Ping timeout: 276 seconds).
19:35:02 -!- MizardX- has changed nick to MizardX.
19:35:02 <bsmntbombdood> http://www.silentpcreview.com/Coolermaster_Silent_Pro_M700W
19:35:24 <alise> 700w is a bit excessive for your stuff.
19:35:41 <alise> http://www.phoronix.com/scan.php?page=article&item=silverstone_nightjar_450&num=1 hey an /actual/ fanless psu
19:38:36 <pikhq> Man. There's an x86 emulator in Java... That appears to work at tolerable speeds.
19:38:39 <alise> your system will consume like 550w tops i bet
19:39:06 <pikhq> (20% of full-speed. Which seems slow until you realise that 200MHz is still quite usable for many OSes.)
19:39:53 <alise> [c] := ~ ([a] | [b]);
19:39:53 <alise> [0] := [0] + 1 + ([c] == 0 ? 1 : 0);
19:39:58 <alise> | is bitwise or, ~ is complement
19:40:02 <alise> you guys think this is tc?
19:40:05 <alise> semantics in english:
19:40:31 <alise> (a,b,c) means take bitwise OR [a] and [b]; then put its complement in [c]. if [c] is then 0, skip the next instruction.
19:40:59 <alise> Then what about this:
19:41:09 <alise> (a,b) means take bitwise OR [a] and [b]; then put its complement in [b]. if [b] is then 0, skip the next instruction.
19:41:36 <pikhq> "Skip the next instruction"? Well, that'd certainly be a *pain* to do actual jumps with.
19:41:52 <Deewiant> pikhq: You can always modify [0] directly with (foo,bar,0)
19:41:55 <alise> RSSB does it, pikhq
19:42:00 <alise> and what Deewiant said
19:42:08 <alise> I might just remove the [0] bit
19:42:14 <alise> but what about the two-instruction one?
19:42:18 <pikhq> Deewiant: I'm not saying it'd be impossible. Just a pain.
19:42:25 <alise> (a,b) means take bitwise OR [a] and [b]; then put its complement in [b]. if [b] is then 0, skip the next instruction.
19:42:29 <Deewiant> Well, OISCs tend to be a pain anyway
19:42:33 <alise> I think this should be about as TC as the three-instruction one.
19:44:35 <alise> so here's the ultimate version
19:44:44 <alise> [b] := ~ ([a] | [b]);
19:45:21 <Deewiant> Probably as TC as the original (a,b,c) one
19:45:31 <alise> Which is probably TC.
19:45:35 <alise> So two layers of probably.
19:45:38 <alise> So about half the probability.
19:45:41 <Gregor> http://www.kfc.com/doubledown/ GOD BLESS AMERICA
19:45:57 <alise> But that's still 50%!
19:46:02 <alise> Well actually a bit less!
19:46:05 <Deewiant> alise: But, if you'd posted only that one, I'd've said only "Probably".
19:46:08 <alise> But do you believe that one is TC?
19:46:16 <alise> You should be more specific :P
19:46:48 <Deewiant> It looks like it might be TC, but I'm not an OISC expert
19:47:03 <alise> Guess I just have to try and write programs in it.
19:47:39 <Deewiant> The easiest proof would probably implementing a known-TC OISC
19:47:48 <alise> Well, let's see; the only way to jump in this would be setting b=0.
19:47:56 <alise> [0] := ~ ([a] | [0]);
19:48:03 <alise> [0] := ~ ([a] | [0]) + 1;
19:48:18 <alise> ~(a|b) = (~a)&(~b) right?
19:48:25 <alise> DeMorgan's laws surely apply to bitwise operations.
19:48:40 <alise> [0] := ((~[a]) & (~[0])) + 1
19:48:41 <oerjan> alise: shouldn't you use [0] := [0] + 2; if an instruction has two operands?
19:48:43 <alise> Well, that is troubling.
19:48:49 <alise> oerjan: Er, yes, thanks.
19:49:01 <alise> Anyway, so, this doesn't seem very helpful
19:49:34 <oerjan> heh, to do a jump you need to know the current ip
19:49:39 <alise> If we say that [a] is ~x, then we have ~(x | [0]) I think
19:49:54 <alise> oerjan: well you can do that of course
19:49:55 <Deewiant> You always know the current ip
19:49:58 <oerjan> and you can only jump to locations that are a subset of the complement bits
19:50:01 <Deewiant> Your code just isn't position-independent
19:50:11 <alise> oerjan: that's the issue, really
19:50:35 <oerjan> oh, but that can be fixed by going via ip 0!
19:50:58 <alise> no it's okay we can move the ip
19:51:00 <AnMaster> ais523, do you happen to know any software that lets me profile TLB misses?
19:51:02 <alise> to say [-1] = [big]
19:51:14 <ais523> AnMaster: I'm not even sure what your question means
19:51:19 <ais523> I'm aware of profiling, but not of TLB misses
19:51:37 <ais523> at least, not that acronym
19:51:46 <AnMaster> ais523, ah, you know that the kernel keeps page mappings?
19:52:00 <ais523> AnMaster: obviously, what else could?
19:52:00 <AnMaster> ais523, and the CPU uses them to find the physical page
19:52:14 <ais523> and that seems a plausible feature for modern CPUs
19:52:16 <oerjan> a jump to -1 will be hard unless you are already at 0
19:52:21 <AnMaster> ais523, TLB cache is used to cache the page mappings
19:52:26 <alise> whatever, let's just say the ip is at ip
19:52:37 <alise> now the problem is
19:52:37 <ais523> surely, whether that gets hit or missed will depend on what other programs are running?
19:52:42 <AnMaster> ais523, I want to profile something to find out if hugetlb would help
19:52:44 <alise> how do we write the jumper at location 0?
19:52:50 <AnMaster> (which is an extension to make each page larger)
19:53:22 <AnMaster> because that means fewer TLB entries, which means more memory can be handled with the TLB entries in the cache
19:53:40 <oerjan> if you are at location 0, then (a,ip) will set [ip] = ~ a
19:53:46 <AnMaster> ais523, and iirc they are flushed at context switch
19:53:51 <alise> using which format oerjan?
19:53:54 <alise> [b] := ~ ([a] | [b]);
19:53:58 <ais523> alise: your OISC operation seems to be NAND
19:54:02 <AnMaster> ais523, because otherwise you would be able to access those other entries
19:54:19 <alise> so, let's call 0 "jmp"
19:54:24 <alise> so the jumping code is at [jmp]
19:54:32 <alise> now let's also call the location it uses for "loc"
19:54:39 <ais523> alise: yep, good point
19:54:43 <alise> oerjan: how do we jump to 0?
19:56:24 <AnMaster> ais523, oh btw I'm currently messing with a ubuntu hardy chroot due to bitrot...
19:56:52 <ais523> how do you get bitrot nowadays? use a computer more than 20 years old?
19:57:05 <oerjan> the post-increment makes that _hard_
19:57:14 <AnMaster> ais523, try to run something that doesn't compile on >gcc-4.2 and needs an older libc
19:57:19 <alise> oerjan: should it be pre-increment?
19:57:23 <oerjan> let's put the jump at 2 instead
19:57:23 <AnMaster> ais523, oh and that uses a custom linker script and doesn't link to libc at all
19:57:24 <ais523> AnMaster: is that bitrot, though?
19:57:31 <ais523> or just massively-old-technology?
19:57:50 <alise> how can we jump from two??
19:57:55 <AnMaster> ais523, it is an cycle accurate x86/x86_64 simulator, which *should* be able to give me some number for the TLB misses if only I get it working...
19:58:25 <ais523> AnMaster: ouch, cycle-accuracy is likely to be incredibly slow
19:58:27 <pikhq> ... Cycle accurate x86 simulator?
19:58:34 <oerjan> alise: we can jump from two to any address whose second lsb is zero
19:58:47 <alise> oerjan: well ideally we'd have arbitrary jumps :-)
19:58:48 <Sgeo> Why wouldn't it compile on newer GCC?
19:58:54 <ais523> pikhq: well, you could obviously just throw the VHDL from an x86 processor onto a VHDL simulator, if you had it
19:58:57 <AnMaster> ais523, yes, but it isn't too slow, plus it can be setup to run only those functions you are interested in that way
19:58:58 <alise> surely this would work?
19:58:58 <pikhq> ais523: I think it telling that it takes a fairly recent computer to do cycle-accurate SNES emulation on a modern machine. :)
19:58:59 <alise> [b] := ~ ([a] | [b]);
19:58:59 <ais523> so I'm pretty sure Intel and AMD have one
19:59:01 <oerjan> alise: that is _only_ possible from 0
19:59:19 <alise> [b] := ~ ([a] | [b]);
19:59:20 <ais523> pikhq: that doesn't surprise me at all
19:59:23 <alise> could we jump to 0 with this I wonder
19:59:26 <pikhq> ... "on a modern machine"? rm that.
19:59:31 <alise> [0] := ~ ([a] | [0]);
19:59:33 <ais523> hmm, is x86 or the SNES older?
19:59:34 <Sgeo> "cycle accurate"?
19:59:43 <alise> [b] := ~ ([a] | [b]);
19:59:47 <pikhq> ais523: Funny thing is, you need cycle-accurate SNES emulation to do it right.
19:59:48 <ais523> it wouldn't surprise me in the least if AnMaster's simulator actually simulated an 8086
19:59:54 <alise> so we have [0] := ~ ([a] | [0]) where [0] >= 2
19:59:54 <pikhq> Sgeo: Emulating each individual clock cycle.
19:59:56 <ais523> pikhq: yep, due to lag effects
20:00:17 <AnMaster> ais523, I don't think it does SSE4 or later, not sure about SSE3
20:00:21 <Sgeo> What's the alternative?
20:00:22 <oerjan> alise: a and b are locations from the ip before increment, right?
20:00:31 <pikhq> There were a large number of weird things that happened on SNES. For instance, you could read the result of a division *before it was done*.
20:00:46 <alise> oerjan: yes. i'll write it out more precisely
20:01:05 <Sgeo> pikhq, similar to delay/force in Scheme?
20:01:14 <Sgeo> Erm, wrong thouyght
20:01:18 <alise> [[0]-1] := ~ ([[0]-2] | [[0]-1]);
20:01:30 <alise> pikhq: partially computed?
20:01:41 <Sgeo> Similar to getting a promise of a result before the result is computed, and ... hm?
20:01:44 <AnMaster> ais523, it is also supposed to emulate cache misses correctly. Checking the mailing list there are some @amd.com addresses there so I do believe they have some experts involved
20:02:29 <AnMaster> ais523, also, for completely unknown reasons it seems to require running as root. Not even setting all the capabilities available as file caps works...
20:03:18 <pikhq> Also multiplications.
20:03:27 <oerjan> ok then it would be possible to jump to 0 with say (#-1,ip)
20:03:45 <oerjan> (# for pointer to constant)
20:03:45 <ais523> hmm, has anyone ever created a non-tape-based OISC?
20:04:15 <oerjan> and at 0 you could jump anywhere with (#~target,ip)
20:05:03 <alise> oerjan: ok, so clearly we need a memory location L such that ~[L] = target
20:05:12 <alise> the question is... can we even assign this to things we want :-)
20:05:12 <hiato> AnMaster: is this that Jasmin sim?
20:05:20 <alise> because the /last jump location/ will still be there!!!
20:05:23 <AnMaster> hiato, never heard of that. This one is called ptlsim
20:05:45 <oerjan> alise: um [a] isn't changed, a locations are pretty stable
20:06:02 <AnMaster> hiato, googling Jasmin sim doesn't give any useful results either
20:06:30 <AnMaster> great, ptlsim crashed on cfunge: "Assert false failed in ooocore.cpp:1056 (bool OutOfOrderModel::ThreadContext::handle_exception()) at 6484964 cycles, 6484964 iterations, 6597152 user commits"
20:06:36 <hiato> AnMaster: http://www.lrr.in.tum.de/~jasmin/
20:07:06 <alise> [ntarg] must be ~target
20:07:18 <alise> so before our (-1,ip) (to get to 0), we need to set [ntarg] to ~target
20:07:21 <alise> can we do this, generally?
20:07:37 <AnMaster> hiato, that seems pretty useless for doing full simulations
20:07:52 <AnMaster> to quote that page "While not implementing all the functionality of a modern Intel Processor its tutorials allow you to try and understand the basic commands and structures of assembler code."
20:08:04 <hiato> AnMaster: I only caught the last bit of this, so yes, if that,s what you're trying
20:08:06 <oerjan> alise: (#-1, ntarg) (#target, ntarg)
20:08:21 <AnMaster> hiato, I'm trying to profile TLB misses yes
20:08:27 <AnMaster> so I need fairly accurate and detailed stuff
20:08:49 <hiato> AnMaster: Haha, good luck
20:09:04 <AnMaster> hiato, ptlsim is *supposed* to be able to do that
20:09:12 <AnMaster> it is just it is a PITA to get it working
20:09:34 <hiato> AnMaster: Actually, let me know how this works out, genuinely interested
20:09:42 <alise> macro [jmp X] := {ones loc; X loc; ones ip}
20:09:51 <alise> and at the start of the program
20:10:05 <alise> then later in the program
20:10:08 <AnMaster> hiato, also it doesn't seem to read the config file (it doesn't do cmd line args, you have to create ~/.ptlsim/full/path/to/executable.conf and put the flags there
20:10:13 <ais523> ooh, Unicode works in file names in this OS
20:10:22 <ais523> this is clearly a good way to create unique extensions for esolangs
20:10:26 <hiato> AnMaster: lolwut? Where did you find this thing?
20:10:34 <AnMaster> (and they are in -this style -so why -they -arent -read -fromcommand line I don't know(
20:10:48 <alise> oerjan: so we can do unconditional jumps. But can we do conditional jumps?
20:10:54 <alise> we can't just do arithmetic on the jump location...
20:11:01 <hiato> ais523: unicode exts ftw!
20:11:03 <AnMaster> hiato, from an llvm.org publication that mentioned using it
20:11:17 <AnMaster> hiato, there is a full system variant of this that integrates with Xen
20:11:20 <oerjan> alise: let's say we have our flag as a 0,1 value somewhere
20:11:23 <AnMaster> I'm trying the user space variant
20:11:23 <hiato> AnMaster: Ah, cant say I frequent their lists
20:11:29 <ais523> so presumably it's an ext3 or ext2 feature
20:11:42 <AnMaster> hiato, nah it wasn't their mailing list, but one of the articles they put on their site
20:11:54 <hiato> AnMaster: oh, I see
20:11:55 * alise is writing this down, btw
20:12:03 <alise> ais523: all ext just store things raw
20:12:07 <alise> all apart from \0 or /
20:12:15 <oerjan> then we can jump to either of two consecutive locations - hm maybe 0,1 is a bad idea
20:12:16 <ais523> the official file extension for DownRight is now .↳
20:12:18 <alise> so the encoding is just how it's mounted
20:12:19 <AnMaster> now to figure out how to get it to read the cmd line
20:12:39 <AnMaster> ah okay, so sudo doesn't set HOME=/root
20:12:44 <hiato> AnMaster: Re-write :P
20:12:47 <alise> oerjan: maybe 0,-1
20:12:51 <alise> we should really say ~0 instead of -1.
20:13:02 <ais523> given that a DownRight program is conceptually a rectangular grid with arbitrary-size cells, I need to come up with a file format
20:13:13 <ais523> I could make it XML just to annoy people, but I don't really want to
20:13:47 <ais523> hiato: hmm, you mean their table representation?
20:13:48 <AnMaster> hiato, No I'm not messing with that code
20:13:58 <ais523> that actually isn't a bad idea, if aiming for sheer horribleness
20:13:59 <AnMaster> hiato, did you see above about it using a custom linker script?
20:14:04 <ais523> but really I want something simple
20:14:05 <AnMaster> hiato, and not linking system libc
20:14:08 <Sgeo> http://blog.regehr.org/archives/140
20:14:17 <AnMaster> hiato, oh and needing gcc-4.1 or 4.2, no other versions work
20:14:24 <hiato> AnMaster: Oh? Well that's when I walk away
20:14:26 <alise> ais523: no actually what i'd do is use the unicode box drawing characters
20:14:30 <alise> that'd be very pretty
20:14:38 <alise> ais523: failing that, | - and +
20:14:40 <hiato> ais523: Ah well, for another project perhaps
20:14:49 <ais523> CSV is probably the most plausible method, it would at least be easy to parse given what the content of the cells are
20:14:51 <oerjan> alise: ah yes 0,-1 is good
20:14:56 <AnMaster> hiato, and yes I'm in this hardy chroot because of modern libc versions (and modern binutils) breaking it
20:14:59 <alise> ais523: or if you want real minimalism, have two extra chars
20:15:00 <ais523> even better, you could make it flexible
20:15:02 <AnMaster> at least now I get it to do *something*
20:15:09 <AnMaster> under jaunty it just did *nothing*
20:15:11 <ais523> D and R for down and right are the commands
20:15:13 <alise> / goes in top left corner of cell, \ top right
20:15:20 <AnMaster> (so, miscompiled rather than compile error)
20:15:34 <ais523> the first thing that isn't D or R that's encountered is column separator
20:15:35 -!- bsmntbombdood has quit (Remote host closed the connection).
20:15:38 <ais523> the second thing is row separtor
20:15:53 <ais523> and row separators are ignored unless at least one column separator is encountered between them
20:16:01 <hiato> AnMaster: Vaporware. Walk. Away.
20:16:09 <ais523> that would work for both CSV and Unicode box drawing
20:16:23 <AnMaster> hiato, not vaporware, it seems to work now
20:16:39 <AnMaster> hiato, it actually gave me tlb stats here
20:16:55 <hiato> AnMaster: c'est ne pa possible
20:17:11 <ais523> hmm, time to go home, I'll have to discover what alise's great idea is later, or else logread
20:17:16 -!- ais523 has quit (Remote host closed the connection).
20:17:19 <alise> ais523: i'm about to paste it!
20:17:23 <alise> i just did all that work
20:17:34 <AnMaster> hiato, sure is, but a PITA to get there
20:17:52 <alise> UNGRATEFUL LOG-READING AIS523: http://pastie.org/941753.txt?key=me9yjscxo1usw2ikcaxba
20:17:54 <alise> code, and table representing it
20:17:59 <alise> key: / is top-left, \ is top-right
20:18:07 <AnMaster> hiato, it is almost as bad as opengenera...
20:18:08 <alise> from this, we can infer all the table cells of arbtirary size, intermingling
20:18:25 <alise> because we know that the first character is the one after /, then the column \ is in delimits the last column for all the lines, and also the last line
20:18:37 <alise> also, I fucked up that table
20:18:39 <hiato> AnMaster: wth is opengenera?
20:18:49 <alise> lisp machine emulator, hiato.
20:19:09 <oerjan> alise: i see some problems with this nor language - there is no simple way to access bits not mentioned in the program, unlimited memory is going to be _hard_, maybe impossible
20:19:10 <hiato> Wouldn't know. Unlike most here, I am not a masochist
20:19:11 <alise> LOG-READING AIS523: revised version - http://pastie.org/941754.txt?key=63e6jwcvawa5kfcjiuuoyg
20:19:32 <alise> oerjan: hmm, how can't you access bits not in the program?
20:19:37 <alise> it's just a matter of storing them in a norable format
20:19:45 <alise> hiato: lisp machines are nice!
20:19:46 <AnMaster> well not lisp machine, since it ran on other hardware
20:20:03 <AnMaster> hiato, see http://en.wikipedia.org/wiki/Genera_%28operating_system%29
20:20:07 <alise> it doesn't emulate the mac one
20:20:10 <alise> !sh echo it doesn't emulate the mac one
20:20:10 <Sgeo> Lisp machines don't run Scheme, do they?
20:20:15 <EgoBot> /tmp/input.5076: line 1: unexpected EOF while looking for matching `''
20:20:15 <AnMaster> now opengenera is a program to run that on modern linux
20:20:22 <alise> !sh echo "it doesn't emulate the mac one"
20:20:22 <EgoBot> it doesn't emulate the mac one
20:20:29 <oerjan> alise: by "in the program" i mean _mentioned_ in the program
20:20:36 <alise> wonder if he's already wised up and ignored egobot
20:20:46 <alise> oerjan: ah, because we cannot dereference locations
20:20:58 <AnMaster> iirc opengenera emulates the one for alpha or such, forgot the details
20:21:00 <alise> what about [b] := ~[[a] | [b]];
20:21:09 <alise> that's one extra dereference before ~ing
20:21:36 <AnMaster> anyway, it needs a complicated setup so you will basically ruin the host system (thus do it in a virtual machine), and it broke with modern ubuntu versions
20:21:56 <hiato> alise: Can you give a quick summary of where this OISC is at?
20:22:13 <alise> hiato: basically the idea is to have it based on a logical operation
20:22:15 <oerjan> alise: if the program contains no values outside -128, 127 and is also stored in there then the _only_ way to get outside is by running off the edge - and we _cannot_ initialize the outside memory first
20:22:19 <hiato> AnMaster: You lost me at the word lisp ;)
20:22:34 <AnMaster> hiato, and the complex setup included stuff like nfs and ntp to localhost iirc
20:22:52 <AnMaster> hiato, you can ask alise for more details, iirc once had it working too
20:22:54 <alise> oerjan: ouch. why that range?
20:23:25 <pikhq> alise: 8-bit twos complement
20:23:26 <oerjan> alise: it's the set of integers for which all bits past the eighth are equal
20:23:37 <alise> pikhq: I didn't say 8bit though
20:23:58 <oerjan> alise: it was just an example, -65536 .. 65535 would have the same property
20:24:08 <oerjan> and -2^n .. 2^n-1 in general
20:24:35 <alise> oerjan: but more dereferencing wouldn't fix it, would it?
20:24:52 <oerjan> alise: you cannot dereference something you cannot mention
20:25:03 <alise> i mean in the instruction set
20:25:18 <alise> [b] := [~([a] | [b])]
20:25:23 <alise> [b] := ~[[a] | [b]]
20:26:00 <Sgeo> <3 Calculus the Easy Way
20:26:34 <oerjan> alise: if you are going to get outside the range, then something inside the range must refer to something outside it, _or_ you must run off the edge and have the part outside preinitialized
20:26:45 <alise> (finite) calculus isn't hard!
20:26:46 <oerjan> alise: essentially you need an infinite memory setup
20:26:58 <alise> oerjan: heh, like the 2,3 tm
20:27:12 <AnMaster> hiato, you want to hear something really scary: Even though this thing links no standard libraries, it uses C++. It has it's own subset of STL included. And parts of klibc
20:27:18 <alise> how complex does the setup need to be, I wonder?
20:27:30 <Sgeo> There's a newer edition? o.O
20:27:31 <AnMaster> this STL is not the GNU STL either
20:27:50 <oerjan> alise: probably not that hard
20:27:59 <AnMaster> which is not completely compatible (different name space for example)
20:28:03 <alise> oerjan: would it be easier with nand?
20:28:07 <alise> an infinite memory setup is kinda lame
20:29:29 <hiato> AnMaster: wutlol? srsly? This thing is messed up man
20:29:53 <oerjan> alise: nand and nor are essentially the same here i think
20:29:55 <Sgeo> ...different name space?
20:30:10 <Sgeo> ...you can't possibly mean what I think you.. damn
20:30:16 <alise> what about or/and without the not? I guess that's even worse
20:30:25 <alise> AnMaster: that's not strange
20:30:27 <alise> even EA do that for their games
20:30:31 <alise> the stl is slow and sucky
20:30:41 <oerjan> alise: it's really about the fact that there is no interference between different bits in your operations, except for the ip increment
20:30:42 <AnMaster> hiato, but I have been unable to locate anything else to profile TLB misses with
20:30:58 <alise> oerjan: yeah... ugh
20:30:59 <alise> and this was going so well
20:31:04 <AnMaster> hiato, and I *need* to know where and if I should try to use hugetlb pages in this program
20:31:07 <oerjan> and all bitwise boolean operations have that property
20:31:11 <alise> oerjan: I assume the original, check-if-0-and-skip, three argument one is better?
20:31:12 <alise> or the same, maybe...
20:31:24 <AnMaster> but premature optimisation is bad
20:31:44 <oerjan> alise: was that also bitwise? if so probably the same
20:31:46 <hiato> AnMaster: yeah, I cant say I've really been looking, and nothing springs to mind... pen and paper? :P But seriously, I'm not sure, but best of luck
20:32:01 <alise> [c] := ~ ([a] | [b]);
20:32:01 <alise> [0] := [0] + 3 + ([c] == 0 ? 2 : 0);
20:32:26 <oerjan> alise: oh hm it occured to me, what _does_ a sequence of (0,0) actually do?
20:32:48 <alise> [0] := ~([0] | [0]);
20:32:53 <alise> [0] := ~([0] + 2);
20:32:55 -!- cheater2 has quit (Ping timeout: 265 seconds).
20:33:11 <alise> at which point it will go somewhere entirely unrelated to where you were at the start
20:33:37 -!- cheater2 has joined.
20:33:38 <oerjan> well if ip != 0 then that won't do anything much
20:34:18 <alise> it will not do much in any case!
20:34:47 <Mathnerd314> hmm... are there any esolangs with type systems?
20:34:54 <oerjan> indeed. i had hoped that by some coincidence you'd jump inside the original range _after_ having put information there about the outside
20:35:26 <alise> Mathnerd314: Haskell /ouch/
20:35:35 <alise> more seriously, yes, such as faces of the lambda cube; they're only retroactively esolangs, though
20:35:40 <oerjan> on the other hand, that seems to me like in a nutshell what you want to do for the infinite memory setup
20:35:43 <alise> Mathnerd314: C++ :-)
20:36:08 <pikhq> C++'s type system *is* an esolang.
20:36:08 <Mathnerd314> C++ is not an esolang, according to the esolang wiki
20:36:11 <oerjan> at each 2^n location, you put essentially a code to do that.
20:36:20 <pikhq> A Turing tarpit, even.
20:36:35 <oerjan> lessee, (ip, x) would be a good start.
20:37:15 <alise> Mathnerd314: it's WRONG
20:37:20 <oerjan> and then perhaps (#-1, ip).
20:37:54 <oerjan> alise: it is possible that putting a sequence ip x #-1 ip at the start of every 2^n boundary is enough
20:38:00 <AnMaster> hiato, found the issue with the file btw, out of date documentation
20:38:23 <alise> oerjan: Yes, but it's a bit of a Cheat.
20:38:35 <oerjan> then you jump back to 0, having set [x] to a pointer to the outside
20:39:00 <oerjan> and then you can extract the new fresh bit from [x] :)
20:39:25 <alise> new bits, freshly squeezed
20:39:27 <oerjan> alise: sure it's a cheat but it's much simpler than what ais523 did for t-2,3 i'm sure
20:39:31 <hiato> AnMaster: how did you manage that?
20:39:50 <AnMaster> hiato, manage what? figuring out what I was supposed to do instead?
20:39:57 <AnMaster> well, grepping source for references to this file
20:40:04 <AnMaster> (surely it has to read the file somewhere)
20:40:13 <AnMaster> noticing there *were* no such references
20:40:34 <AnMaster> checking commits since that release which *had* such references
20:40:55 <AnMaster> and then figuring out what it was supposed to do instead (pass them on cmd line arg!!!)
20:41:02 <AnMaster> (at least that is somewhat saner than the old variant!)
20:41:15 <AnMaster> (if only they would update the docs too)
20:42:36 <Mathnerd314> so no real esolangs with type systems... because types are impossible to experiment with?
20:42:45 <AnMaster> hiato, oh btw this can automatically generate comparsion tables for various statistics. In plain text and latex
20:43:02 <AnMaster> hiato, like different parameters to the simulation
20:43:12 <Sgeo> My step-mother: "You see the nice weather? God decided to give you nice weather on your birthday." I think she's just being annoying, but she might be serious
20:43:12 <AnMaster> or different binaries with same parameters
20:43:29 <AnMaster> hiato, yes, quite. But yeah a PITA to get it working indeed
20:43:36 <hiato> Sgeo: I dont think god is though
20:43:43 <oerjan> Mathnerd314: i had this insane idea once of a combinator language with overloaded monads like haskell
20:43:54 <AnMaster> hiato, they fail at the docs a bit, too few linebreaks in the pdf
20:43:56 <oerjan> nothing fleshed out though
20:44:22 <hiato> AnMaster: Yes, this was a definite walk. away. now. proggy
20:44:42 <AnMaster> hiato, nah, there was just in one place, and that seems fixed in the latex master file in git head
20:44:48 <hiato> oerjan: sounds deceptively interesting
20:44:52 <oerjan> basically slightly like unlambda, except c wasn't just call-with-current-continuation, but actually was typed in the Cont monad
20:45:30 <oerjan> and ` was not just application, but like haskell =<<
20:45:34 <hiato> AnMaster: impressive stuff, but le's see if it actually works now ;)
20:45:53 <Mathnerd314> oerjan: well, I'm thinking of a "cool" esolang where (<$>) = (.) = ($) = id
20:45:56 <AnMaster> hiato, well yes it does, I'm just trying to make sense of the statistics currently
20:46:12 <AnMaster> hiato, as in, ptlsim (the actual simulator) works
20:46:35 <oerjan> Mathnerd314: every value would be in a monad when put on the _right_ of an application (=<<) but would be unwrapped into a function on the left
20:46:35 <AnMaster> hiato, but ptlstats (takes the data dump and makes something human readable from it) I haven't figured out yet
20:46:50 <pikhq> http://www.spiegel.de/international/business/0,1518,692001,00.html Google Translate? Usable? Hah!
20:47:00 <AnMaster> hiato, well ptlstats works, but I need to figure out how to get the part of it that I need in a meaningful format
20:47:19 <pikhq> It's not far from "my nipples explode with delight"!
20:47:29 <hiato> heh, welcome to the silly wortd of machine code dumps
20:47:35 <oerjan> (the language name is liMonade, btw)
20:48:13 <AnMaster> hiato, as in, I can get it to dump the data format in a somewhat more readable format, but it seems to be miss per cache type per instruction (as in, not per instruction in the program, but merged for all instructions of a given type, say, div, add, or whatever)
20:48:19 <AnMaster> which is not quite the stat I want
20:49:12 <alise> Mathnerd314: that's just concatenative right?
20:49:54 <Mathnerd314> not really; it's something like loosely-typed Haskell
20:49:55 <hiato> AnMaster: meh. How does it sim? With a pipeline and all? clock cycles?
20:50:01 <oerjan> Mathnerd314: btw the suggestion of making (.) = (<$>) i've heard on #haskell before. in fact i think lambdabot implemented it for a while.
20:50:18 <alise> <pikhq> It's not far from "my nipples explode with delight"!
20:50:41 -!- tombom has joined.
20:50:41 <AnMaster> hiato, it is cycle accurate and you can get it to dump pipeline state for every cycle (the manual warns that the dump file will be huge if you do that)
20:50:45 <alise> Mathnerd314: well having function application be composition...
20:50:51 -!- cal153 has quit.
20:50:52 <alise> makes little sense.
20:51:04 <AnMaster> hiato, also it can switch to native execution for the parts you are uninterested in
20:51:14 <oerjan> Mathnerd314: mixing $ in is going to give some ambiguity though, even though it's the Identity monad
20:51:14 <AnMaster> hiato, like, only do the full thing for a few functions
20:51:45 <oerjan> alise: ($) = (<$>) is the identity monad i think
20:51:45 <AnMaster> hiato, oh and there is a version that integrates with Xen to do full system simulation, and the website says a kvm-based variant is currently being worked on
20:51:51 <hiato> AnMaster: this thing actually sounds pretty useful
20:52:03 <oerjan> or is it (<*>), maybe those are all the same in it
20:52:25 <AnMaster> hiato, I have only tried user space simulation, but considering how tricky THAT was... I can only imagine the pain of the full system ones
20:53:08 <AnMaster> (And I still haven't figured out what exact parameters I need to ptlstats)
20:53:21 <hiato> Haha, yeah. If the docs are anything to go by...
20:55:10 <AnMaster> hiato, I think I figured part of it out. The stats is represented as a tree. So I want something like /ooocore/dcache/<something>
20:56:23 <Mathnerd314> alise: it's overloaded juxtaposition, basically. f $ x is the same as f x, and I want f . g to be f g as well
20:57:25 <hiato> AnMaster: Really? Hmmm, well good luck finding those nodes then... that is a little silly
20:57:40 * Sgeo is worried about becoming a Google fanboy
21:01:19 <AnMaster> hiato, oh btw it does simulate an out of order core
21:01:35 <AnMaster> or optionally a sequential one
21:01:41 <AnMaster> there are various settings related to both
21:02:36 <AnMaster> hiato, and the tree system is quite sane
21:02:41 <AnMaster> since there are a lot of different stats
21:03:02 <AnMaster> doing a "flat" system would be impossible to manage
21:03:03 <hiato> AnMaster: where di you get this thing again?
21:03:28 <hiato> AnMaster: Perhaps, I envisaged a nice file prefix system, but hey
21:03:31 <AnMaster> hiato, well www.ptlsim.org is where, but before you asked how I found it, which was from llvm
21:03:47 <AnMaster> (or rather a publication of them)
21:03:56 <AnMaster> hiato, I'm using git head here
21:04:04 <Sgeo> alise, do you know anything about eBuddy?
21:04:13 <Sgeo> I'm wondering if it might be malicious
21:04:38 -!- Tritonio_GR has quit (Quit: Leaving.).
21:05:15 <alise> Sgeo: It's old and fine but, you know, shitty.
21:05:24 <alise> meebo is better imo
21:05:36 <Sgeo> Meebo keeps disconnecting
21:05:46 <Sgeo> If eBuddy is safe, I think I'll try it
21:05:53 <Sgeo> [I'm talking about on my phone btw]
21:06:56 <AnMaster> hiato, oh yeah and don't make it dump a snapshot every 100 cycles (I meant 1000 but typoed)
21:07:18 <AnMaster> hiato, the data dump I got was 552MB, and that was just for ./program --help
21:09:36 <Sgeo> "After using ebuddy, my hotmail account got attacked and it kept sending spam msgs to my entire contact list."
21:11:46 <Sgeo> from WOT: "They keep and can use you password of account"
21:12:46 <AnMaster> okay now this is strange, why are there multiple cpu nodes in there
21:13:17 <AnMaster> hiato, either it does SMP simulation and then I'm extremely impressed, or vcpu0 vcpu1 and so on mean something else
21:14:26 <hiato> AnMaster: that sounds a lot like smp to me..
21:14:44 <AnMaster> but should there be an option to control number of cpus you want then...
21:15:00 <hiato> Heh, time to read the... oh wait.
21:15:17 <alise> <Sgeo> [I'm talking about on my phone btw]
21:15:31 <alise> also, I think those are unrelated to ebuddy.
21:15:43 <Sgeo> Yes, but if eBuddy on the web is malicious, then the app would also be malicious
21:15:47 <alise> tons of people get msn viruses by being retards; the latter has no evidence provided
21:16:30 <hiato> AnMaster: the missing word was docs :P
21:16:35 <Sgeo> There are people who think geocities is malicious because one site is malicious
21:16:47 <AnMaster> hiato, I wondered if it was "source" or "docs"
21:17:49 <AnMaster> hiato, I'm building git head docs atm, lets see if that is better than website
21:18:06 * AnMaster watches pdflatex output scroll by
21:18:49 <alise> get a non-ebuddy app then
21:19:00 <AnMaster> hiato, so, the Xen one does SMP/SMT it says
21:19:47 <hiato> Well, it's donig it so far as I can tell, but what do those dumps hold? Perhaps theyre empty
21:20:32 <AnMaster> hiato, perhaps. Note it is NOT the ptlsim.log file
21:20:58 <AnMaster> (well, foo.stats is probably a better name)
21:21:10 <hiato> heh, yep. Ok, I see
21:21:46 <AnMaster> hiato, because here it needs sudo to run
21:21:59 <AnMaster> the mailing list indicates this is needed on ubuntu and a few other distros
21:22:14 <Sgeo> Meebo does seem to be a nicer interface, but it simply doesn't WORK
21:22:51 <AnMaster> oh god, this is nasty (reading source code that defines the stats tree)
21:23:35 <AnMaster> hiato, know ghc? think "ghc evil mangler" kind of nasty level...
21:24:01 <Sgeo> I can't seem to add my AIM account to eBuddy
21:27:41 <Sgeo> eBuddy doesn't warn me that I'm offline
21:31:40 <AnMaster> hiato, oh it seems it need full system simulation to do TLB stats properly, that explains the strange numbers (which were reasonable for the first small "dummy" test
21:31:57 <AnMaster> well, maybe I'll try that later, the other stats are still interesting
21:32:33 <AnMaster> that seems to be to make it use real tlb from the cpu
21:32:40 <AnMaster> I'm not sure about tlb for user space
21:33:38 <AnMaster> ah no, user space version do not model it
21:33:46 <AnMaster> and nah I'm not doing Xen this evening
21:36:43 -!- Phantom_Hoover has joined.
21:36:47 -!- hiato has quit (Ping timeout: 260 seconds).
21:40:27 <oerjan> who the heck is dr nick
21:45:33 <Phantom_Hoover> Why does Facebook discriminate against people who eschew mobile phones?
21:46:53 <alise> Facebook discriminates against intelligence.
21:47:46 <Phantom_Hoover> I know, but I wouldn't have *any* friends if I didn't use it.
21:47:58 <alise> You've got us, man.
21:48:27 <Phantom_Hoover> You suffer the crippling disadvantage of knowing more about one of my fields of interest than me.
21:50:09 <pikhq> Yeah, that'll happen. Is called "life". :P
21:50:43 * Sgeo uses Facebook >.>
21:51:19 * pikhq has for 12 freaking years now.
21:51:59 * Phantom_Hoover once had a theory that everyone was a reincarnation of myself.
21:52:29 * oerjan recalls seeing that theory somewhere recently
21:52:43 <oerjan> with a scifi reference that wasn't named
21:53:04 <oerjan> (if it wasn't here, probably reddit)
21:53:29 <oerjan> yeah but that was in a previous life *ducks*
21:54:14 <oerjan> i cannot admit what i don't remember
21:54:56 <oerjan> doesn't matter, it's 1,2,3,... everywhere
21:56:02 <alise> <Phantom_Hoover> I must know all.
21:56:03 <alise> <Phantom_Hoover> Damned Gedel...
21:59:26 -!- Phantom_Hoover has quit (Ping timeout: 265 seconds).
22:00:39 -!- Phantom_Hoover has joined.
22:02:25 <alise> I am bloody determined to come up with an OISC.
22:02:38 <alise> oerjan: hey I think my language could be salvaged
22:02:39 <alise> if we kept the basic
22:02:40 <Gregor> Do you have something against subtract-and-branch-if-negative?
22:02:45 <alise> [[0]-1] := ~ ([[0]-2] | [[0]-1]);
22:02:46 <alise> but then added more mutation
22:02:49 <alise> with an extra dereference
22:02:55 <alise> Gregor: It's called research, man.
22:03:00 <alise> Also, RSSB is better, having only one operand.
22:04:14 <alise> [[0]-1] := ~ ([[0]-2] | [[0]-1]);
22:04:14 <alise> [[[0]-2]] := something
22:04:27 <alise> since [0]-2 doesn't normally mutate with this, it lets us have something reliableish
22:04:33 <alise> only question is what's something, and is this enough
22:06:02 <alise> [[0]-1] := ~ ([[0]-2] | [[0]-1]);
22:06:02 <alise> [[[0]-2]] := [[0]-1];
22:06:08 <alise> then we get a free copy to a dynamic addres with every instruction
22:09:12 <Phantom_Hoover> RSSB just looks like the MOV system used in the Wireworld computer.
22:09:25 <alise> it's not mov is it?
22:09:54 <pikhq> Phantom_Hoover: mmap'd functionality is not unusual for OISC stuff. ;)
22:10:37 <alise> I REQUIRE OERJAN'S BOTHERSOME REALITY CRUSHING MY DREAMS
22:11:35 -!- zzo38 has joined.
22:12:56 <zzo38> How often in any programming can use "same number for multiple purposes"?
22:13:27 -!- adam_d has quit (Ping timeout: 265 seconds).
22:13:40 <pikhq> zzo38: Context por favor?
22:14:19 <zzo38> I mean like the "stroker.gb" game, I wrote, it used 0x9C for clear screen tile instead of 0x00 so that the register can be used for multiple purposes at once
22:14:51 <zzo38> And in one solitaire card program I write, it uses ASCII 32 (space) for wildcard so that it can be checked by LTRIM$ function if a pile consists entirely of wildcards
22:15:40 <zzo38> And, in code-golf, the C program is given no command-line parameters so the solution can be written: main(i){while(putchar(i++)<127);}
22:16:03 <zzo38> Yes, it might be similar in many ways
22:16:36 <pikhq> Ah. It's most common in various forms of golfing.
22:16:55 <pikhq> Or at least space optimisation.
22:17:17 <pikhq> Which *used* to be fairly common. Now, "space optimisation" consists of "-Os".
22:17:24 <zzo38> Phantom_Hoover: cat >a.out is not so good for binary files
22:17:35 <zzo38> A hex-editor would be used instead.
22:17:42 <pikhq> Phantom_Hoover: Won't handle 0x00 right.
22:18:03 <zzo38> If you have GameBoy or GameBoy emulator, you can check this game and you can see how it is used: http://zzo38computer.cjb.net/prog/GameForth/game/stroker.zip
22:18:16 <zzo38> However some bugs in some emulators mean it has to be longer than it should be
22:18:20 <pikhq> Erm. No, wait, EOF is differentiable from other characters. Never mind. :P
22:18:29 * pikhq has done too much Brainfuck.
22:19:32 <pikhq> With 8-bit cell Brainfuck, you have 2^8-1 choices for EOF.
22:19:38 <pikhq> Of those, 0 is the easiest to test against.
22:19:58 <zzo38> I prefer 0 for EOF on brainfuck, but some uses 255 because of the C program.
22:20:08 <Phantom_Hoover> True, but I always thought of it as inelegant. 0 is still a valid ASCII character.
22:20:14 <oerjan> alise: the problem is not copying to "dynamic" addresses, which you already could do perfectly well, the problem is constructing any value outside the initially provided range
22:20:37 <pikhq> *All* possible values are valid characters for normal IO in 8-bit Brainfuck.
22:21:03 <pikhq> You only start getting truly "complete" IO in greater-than-8-bit Brainfuck.
22:21:24 <pikhq> (or hacks, such as, say, interleaving IO with an "EOF" flag or some such.)
22:22:30 -!- BeholdMyGlory has quit (Remote host closed the connection).
22:24:03 <zzo38> If I make some changes in Linux I would have to add a few additional signals, such as SIGBREAK SIGCORE SIGDC1 SIGOKILL and so on.
22:24:32 <zzo38> Where SIGOKILL is like SIGKILL but overrides everything that can prevent SIGKILL from working including init process, uninterruptable sleeping, etc
22:25:20 <zzo38> Wikipedia says it doesn't.
22:26:50 <zzo38> It says SIGKILL don't kill blocked state programs, therefore SIGOKILL needs to killed even blocked state programs immediately.
22:27:31 <zzo38> Well, it never always works, is it?
22:27:59 <pikhq> zzo38: SIGKILL does, in fact, kill init.
22:28:08 <pikhq> When init is killed, the kernel panics.
22:28:15 <zzo38> Then Wikipedia is wrong.
22:28:30 <pikhq> Try it. "kill -9 1".
22:28:49 <zzo38> Or maybe it kills init only on some operating systems but on other operating systems, it doesn't.
22:29:13 <Ilari> On Linux, init is special and is immune from SIGKILL iirc.
22:29:42 <Ilari> And killing D-state programs with SIGKILL is technically possible but hairy to implement.
22:29:45 <pikhq> Ilari: Kernel panic.
22:30:32 <Ilari> IIRC, earlier versions didn't have that protection but I first noticed that logic when reading kernel sources.
22:32:22 <zzo38> In addition, SIGOKILL would prevent other programs from being notified by using another signal (such as SIGCHLD), but it can still check normally if a process exists
22:33:40 <alise> <oerjan> alise: the problem is not copying to "dynamic" addresses, which you already could do perfectly well, the problem is constructing any value outside the initially provided range
22:33:43 <alise> er just put it in the source
22:34:35 <Ilari> "kill -9 1" does nothing.
22:35:24 <alise> on os x, kill 1 reboots the system.
22:35:50 <Ilari> Well, that was on Linux 2.6.32...
22:36:59 <oerjan> alise: um i was assuming you were trying to solve the problem of accessing unbounded memory without unbounded pre-initialization, otherwise you have no _need_ for any more modification
22:37:34 <Ilari> Fun tricks: 'clone(9, NULL)'. :-)
22:37:48 <oerjan> i believe your original (a,b) version is perfectly adequate for computation with bounded memory
22:37:57 <zzo38> What is 'clone(9, NULL)'?
22:37:59 <alise> oerjan: not INFINITE preinitialisation
22:38:16 <alise> I want infinite memory + finite but unbounded initialisation
22:38:18 <Ilari> Actually, 'sys_clone(9, NULL)'.
22:38:29 <oerjan> alise: unbounded = infinite in this case
22:38:37 <zzo38> And what is 'sys_clone(9, NULL)'?
22:39:00 <Ilari> Like fork but use SIGKILL on process termination instead of SIGCHLD.
22:39:07 <alise> oerjan: but "any value you like" can go in the source
22:39:15 <alise> this also includes all possible values, because of finite bit size.
22:39:22 <alise> moving it somewhere is the problem
22:39:28 <alise> because I dereference like that
22:39:36 <alise> oerjan: then clearly I need arbitrary bit size
22:39:39 <alise> then there is no problem
22:39:45 <alise> oerjan: only one problem; with bignums, what is "all ones"?
22:40:16 <Ilari> Also using sys_clone(11, NULL); sys_exit(0); and then making the child exit could be fun...
22:40:26 <oerjan> alise: -1 in two's complement
22:40:34 <alise> oerjan: yes, but you can't have infinite sized numbers
22:40:35 <zzo38> Ilari: OK, so, that's what it is, now I know
22:40:38 <alise> this is just bignums
22:41:08 <oerjan> alise: signed bignums corresponds to any bitstring that _eventually_ becomes just 0 (positive) or just 1 (negative)
22:41:45 <alise> yes, but negative memory locations MAKE NO SENSE, BITCH
22:41:47 <oerjan> you cannot _do_ nor on bignums without sign, or something equivalent to it
22:41:48 <alise> ... I don't /think/...
22:42:11 <alise> oerjan: so with arbitrary size bits, this should work fine?
22:42:12 <zzo38> What does sys_clone exactly do, what are its parameters? (Looking on Google doesn't help much)
22:42:33 <oerjan> alise: the initialization problem remains
22:43:56 <oerjan> because if all memory is 0 outside a bounded area of -2^n .. 2^n-1, and all values of cells in that area are also -2^n .. 2^n-1, then there is no way to construct a value outside that range
22:44:29 <alise> Phantom_Hoover: no, just infinite-bits
22:44:39 <oerjan> except for [ip], but at the point ip wraps over you are executing only zeros...
22:44:42 <alise> i.e. 0, 1, 2, ..., G_64, ..., xkcd, ...,
22:44:52 <alise> xkcd + your mother's weight in kilograms,
22:45:07 <alise> oerjan: clearly all memory should start at -1 then?
22:45:07 <oerjan> now now, let's not go inconsistently large here
22:45:22 <alise> "and all values of cells in that area are also -2^n .. 2^n-1"
22:45:24 <alise> nothing is bounded
22:45:39 <oerjan> alise: sheesh you are being dense
22:45:45 <alise> oerjan: yes, I know.
22:46:10 <oerjan> if you have _finite_ initialization then there _will_ be some range that all initial values are inside
22:46:15 <alise> Phantom_Hoover: your mother is far heavier than that.
22:46:20 <alise> also, that is just 2*xkcd
22:47:26 <zzo38> What kind of numbers are G_64 and xkcd
22:47:59 <oerjan> zzo38: G_64 is graham's number, was in guiness book of records at one point as the largest specific number used in math
22:48:25 <alise> zzo38: it's the upper bound on a value that's more likely to be on the order of 20
22:48:36 <zzo38> How can it be used as a number if it is a webcomic?
22:48:43 <alise> zzo38: basically you take arrow notation i.e. x^y is exponentiation x^^y is repeated exponentiation and so on
22:48:47 <alise> then you define numbers with absurd amounts of these
22:48:55 <alise> absurd ^...an absurd number of arrows...^ absurd
22:48:56 <oerjan> xkcd made a comic referring to the even larger number A(G_64,G_64) (where A is the ackermann function)
22:49:04 <alise> and you iterate G_n+1 = substitute G_n for absurd
22:49:08 <alise> take the 64th element
22:49:13 <alise> and you get something huge
22:49:18 <alise> I assume you know what the ackermann function is
22:49:31 <zzo38> Yes, I have heard of ackermann function, I know what it is
22:49:31 <oerjan> zzo38: xkcd didn't invent either G_64 or the ackermann, it's just the kind of geeky stuff xkcd sometimes references
22:49:59 <alise> well, xkcd = A(G_64, G_64); he came up with that
22:50:15 <zzo38> OK, now I can understand why they used it like that
22:50:18 <oerjan> and xkcd is so popular among geeks that once he did it, they named it after the comic
22:50:24 <alise> the great thing is that you can't cause a vast increase in it without resorting to a longwinded procedure
22:50:32 <alise> vast as in relative to its size
22:51:19 <oerjan> incidentally A(G_64,G_64) is less than G_65, or something like that iirc, so putting A's around doesn't really help much
22:52:05 <oerjan> basically G's grow so fast that the ackermann function is insignificant in comparison
22:52:45 <zzo38> I made a solitaire card program, but it doesn't have a picture of Oscar Wilde on the wildcard, and the win screen doesn't have the vector drawing of the baker, the spider, the king. I would need to add these things if someone has the picture?
22:53:40 <zzo38> How many do you A(G_x, G_x) by "xkcd" times if x start A(G_xkcd, G_xkcd) and then x is the new value of the function after each time
22:54:03 <alise> zzo38: I think G grows far faster than that
22:54:17 <alise> because it G_n+1 has G_n arrows as its operation
22:54:23 <alise> and then feeds G_n to both sides
22:54:29 <alise> so not only are the numbers huge, it /constructs/ a huge operation
22:55:50 <zzo38> Like, x'=A(G_x,G_x) x''=A(G_x',G_x')=A(G_A(G_x,G_x),G_A(G_x,G_x)) and so on?
22:55:51 <oerjan> zzo38: i think A(G_n, G_n) <= G_(n+1) for all n, or at least from a very small size
22:56:31 <zzo38> That means surely G_x' is more larger than G_x is?
22:57:11 <oerjan> however, x'' <= G_(x'+1)
22:58:16 <alise> basically your attempts at increasing xkcd are fruitless :D
22:58:48 <zzo38> But that's xkcd''''''''''' must surely be more larger than xkcd'''' ?
22:59:20 <oerjan> oh they're all incomprehensibly larger than the previous, sure
22:59:45 <zzo38> Because xkcd''''''''''' = A(G_xkcd'''''''''',G_xkcd'''''''''')
23:00:28 <alise> Let lol_0 = G_1; lol_n = G_(G_(G_... (n+1 G_s) lol_(n-1)
23:00:39 <alise> Now consider lol_xkcd.
23:01:09 <alise> Wow, you can actually hold that number in your head?
23:01:21 <zzo38> No. but I can consider it.
23:01:35 <Phantom_Hoover> That's nothing compared to coppro's Turing-completeness.
23:02:01 <zzo38> What 's coppro's Turing completeness?
23:02:16 <alise> with your powers combined, I am Captain Turing!
23:02:23 <Phantom_Hoover> A while ago he said that his brain was Turing-complete.
23:02:28 <alise> And the digits of lol_xkcd ARE...
23:02:44 <zzo38> O, so that's what it means.
23:02:59 <zzo38> In fact I don't even know how to calculate G_ of anything
23:03:55 <oerjan> well writing down the digits of G_1 won't fit in the observable universe, anyway
23:04:09 <alise> The last ten digits of Graham's number are ...2464195387
23:04:14 <alise> didn't know we'd calculated that many.
23:04:35 <zzo38> OK, so you can partially calculate it, I suppose
23:04:47 <oerjan> alise: it's not really that difficult to calculate from the end as far as you wish
23:04:52 <alise> http://en.wikipedia.org/wiki/Kruskal%27s_theorem#Friedman.27s_finite_form ;; numbers much bigger than graham's
23:05:32 <zzo38> I know I once invented a chess variant where the number of different kind of pieces was googolplex
23:05:46 <alise> zzo38: you know knuth's arrow notation?
23:05:52 <zzo38> Exactly googolplex, not approximate.
23:06:00 <alise> x^y is exponentiation; x^^y is repeated exponentiation; x^^^y is repeated ^^iation; etc
23:06:07 <zzo38> alise: Yes I have seen arrow notation on Wikipedia before, I know what it is
23:06:26 <alise> say G_1 = 3 ^^^^ 3; G_n = 3 (G_n-1 ^s) 3
23:06:31 <alise> then Graham's number is G_64
23:06:54 <zzo38> Of course it is impossible to actually play that chess variant
23:07:08 <oerjan> alise: basically _all_ the G_n numbers end in the same sequence of digits afa our bounded universe is concerned
23:07:28 <zzo38> O, do you mean explain the chess?
23:07:32 <alise> oerjan: ah, clever.
23:07:36 <zzo38> It would take a while to explain
23:07:44 <zzo38> But I can type it later
23:07:52 -!- hiato has joined.
23:08:04 <alise> yeah "This algorithm produces the following 500 rightmost decimal digits of Graham's number (or any tower of more than 500 3s):"
23:08:34 <hiato> AnMaster: power failure. but i'll check the log tomorrow. on my phone now
23:09:20 <zzo38> But, basically, you have a 10x10 board with numbers 0 to 9 to determine how the piece is allowed to move in that direction (chosen by the position on the board) and then you assign digits 0 to 9 to each possible combination of that 10x10 board to determine how the moves of the pieces are combined together with each-other.
23:09:27 <alise> anyway, the number of digits in G_64 could not be written down in the physical universe
23:09:31 <alise> could the number of digits in G_1 be?
23:09:32 -!- hiato has changed nick to hiato-phone.
23:09:38 <alise> it's not /that/ big
23:10:09 <alise> http://mathforum.org/library/drmath/view/68592.html says no
23:10:13 <zzo38> And that includes all kind of movement such as capturing, non-capturing, promotion, Chinese cannon move, Korean cannon move, leap or ride in any direction and any amount of spaces, restriction of adjacent pieces, and so on.
23:10:14 <alise> what about the log of its log
23:10:34 <oerjan> 3 ^^^^ 3 = 3 ^^^ (3 ^^^ 3), right?
23:11:08 <hiato-phone> Isn't g1 just 3 -3 to the three to the three up arrows- 3? like, seventy billion or something
23:11:14 <alise> oerjan: i think so, yes.
23:11:32 <alise> hiato-phone: g_1 is much bigger than seventy billion
23:11:45 <alise> 3^^^3 = 3^^3^^3 = 3^^7625597484987
23:11:52 <alise> and I don't think you can write a 7625597484987-high power tower
23:12:00 <hiato-phone> Oerjan, three with seventy billion up arrows three
23:12:12 <alise> no, hiato-phone is wrong.
23:12:28 <oerjan> hiato-phone: i think the number of arrows is actually small for G_1
23:13:02 <alise> which is (3^) repeated 7625597484987 (off by one or two) times
23:13:07 <oerjan> G_2 on the other hand, is larger than what you said :D
23:13:16 <hiato-phone> I thought every level was previous level total in up arrows
23:13:19 <alise> G_2 = 3 (G_1 ^s) 3
23:13:26 <alise> yes, but G_1 is the base case
23:13:29 <alise> and it has three arrows.
23:13:55 <Phantom_Hoover> IIRC there was a Horizon documentary a while ago with someone claiming that there was a largest integer.
23:14:02 <alise> were you being dijkstra and expecting everything to start at 0 :-)
23:14:05 <alise> Phantom_Hoover: Yes.
23:14:17 <alise> A prominent ultrafinitist.
23:14:27 <alise> He's utterly crazy... but he's done some clever things.
23:14:39 <oerjan> now if you were able to calculate the _first_ digit of G_64 (or even G_1) then I think you'd have it made in mathematics.
23:14:54 <alise> He has a plane geometry textbook that a computer wrote by automatically finding proofs and writing the code for them
23:15:04 <alise> oerjan: well, that's the problem
23:15:08 <oerjan> no modulo tricks to help you there
23:15:09 <alise> calculating the first digit ~= calculating it
23:15:13 <alise> because of, you know, decimal
23:15:20 <alise> Phantom_Hoover: http://www.math.rutgers.edu/~zeilberg/GT.html take a look at it, it's pretty cool
23:15:23 <hiato-phone> Hmm... i could do it in binary with an accuracy of fifty percent off the cuff
23:15:25 -!- zzo38 has quit (Remote host closed the connection).
23:16:14 <oerjan> alise: any base other than 3^k would do, i'm sure :)
23:16:32 * pikhq votes for base G_64
23:16:38 <alise> hiato-phone: the first digit is /obviously/ 1 in binary
23:16:50 <alise> oerjan: hey i did it in binary and that's not 3^k
23:16:58 <hiato-phone> In fact, i can guarantee what it is in binary, heh, my bad. trinary with fifty percent
23:17:01 <alise> I'VE GOT IT MAAAAAAAAAADE
23:17:01 <oerjan> alise: you'll be famous!
23:17:14 <alise> what would it be in base 3^k?
23:18:30 <oerjan> but in base 3 it's obviously 1
23:18:34 -!- Phantom_Hoover has left (?).
23:18:35 <oerjan> since it's a power of 3
23:18:53 <hiato-phone> Indeterminable, i agree with alise, at least equivalent to working the entire number out
23:20:01 <oerjan> 3^(3^...) = 3^(3*3*...) = (3^3^k)^... something
23:20:13 <oerjan> so i believe in every 3^3^k base it is one
23:21:05 <alise> you could /probably/ simplify the problem from calculating /all/ of G_1
23:21:17 <alise> but you would have to calculate some large amount of context then somehow prove the rest has no affect on it
23:21:24 <alise> it seems a quite intractable problem
23:21:36 <hiato-phone> I'm not so sure, can you restate that proof type thing? it is possible that there is a power of 3 to the 3 to the k that is not a power of, say, 3 to the 3 to the 3 to the x
23:21:58 <pikhq> I wonder what the *last* digit of G_64 is. :P
23:22:01 <alise> *effect not affect
23:22:06 <oerjan> hiato-phone: G_1 = 3^3^3^3^...huge no. of 3's something
23:22:07 <alise> we know the last 500 digits, easily
23:22:16 <alise> that's why we're talking about it
23:22:25 <alise> pikhq: because after a while, the powers in the tower stop mattering
23:22:29 <alise> because they only change larger digits
23:22:32 <alise> http://en.wikipedia.org/wiki/Graham%27s_number#Rightmost_decimal_digits_of_Graham.27s_number
23:23:11 <Sgeo> Anyone here using Chrome?
23:23:27 <Sgeo> My school's website just seems to be blank
23:23:36 <hiato-phone> Reminds me of that biggest number contest on xkcd forums back in the day
23:23:38 <oerjan> hiato-phone: which is 3^3^something huge = 3^3^(k+something huge) = 3^(3^k * something huge) = (3^3^k) ^ something huge
23:24:12 <oerjan> where something huge is a natural number in each case
23:24:46 <alise> oerjan: of course all this is just silly because really busy beaver dwarfs A easily
23:24:58 <alise> but stupid people like numbers they can compute! hrmph!
23:25:06 <alise> (says the constructivist)
23:27:14 <hiato-phone> Alise- let s . x = s . x+1 if x is real, x-1 otherwise
23:27:27 <alise> s being some sort of kooky function here?
23:27:36 <alise> also, real as opposed to what, integer? rational? irrational?
23:27:58 <alise> everything is a real apart from complex numbers.
23:28:08 <hiato-phone> Real as defined, well, on wk is a good start i guess
23:28:49 <alise> We should just make a computer program that continually makes up bigger and bigger recursive ways to create numbers
23:28:58 <alise> unbeatable, given long enough
23:28:59 <hiato-phone> Ok, then let me rephrase, if x elem integers
23:29:04 <alise> I propose this one
23:29:09 <pikhq> alise: All reals are finite numbers.
23:29:25 <alise> i = 0; while (true) { printline("#" * i); i++ }
23:29:29 <hiato-phone> I think that s of anything should be as big as integers can get
23:29:35 <alise> pikhq: well infinite as in not infinite, yes...
23:29:41 <alise> although iirc there are models with infinite numbers?
23:29:49 <alise> even for the naturals
23:29:57 <pikhq> The reals are not normally such a model.
23:30:02 <alise> hiato-phone: it's just the "not definable in N words" paradox
23:30:05 <alise> pikhq: the reals are laws
23:30:07 <alise> the model is the model
23:30:16 <pikhq> As I said, "not normally".
23:30:18 <alise> the intended model of the reals has no infinities, but...
23:30:27 <alise> hiato-phone: as soon as you define s, all s(x) become "real"
23:30:28 <oerjan> if there is an infinite model, then there are models of all cardinalities, or something like that
23:30:29 <pikhq> Clearly, if you define the real differently, you get different properties.
23:30:30 <alise> because you can define them easily
23:30:37 <oerjan> *infinite cardinalities
23:30:43 <alise> oerjan: in my world the reals have pi elements.
23:30:47 <alise> pikhq: you fail at understanding models :P
23:30:55 <alise> the reals are defined by the regular definition - pick any one you want -
23:31:00 <alise> this has the intended model, which is what we think we mean
23:31:08 <alise> but there are all sorts of non-standard models, such as ones that are countable
23:31:12 <alise> ones with infinities
23:31:37 <hiato-phone> alise, the result is supposed to be real, by construction, but the 'largest'
23:31:52 <alise> hmm S(n) grows slower than ackermann?
23:31:57 <alise> hmm S(n) grows slower than G?
23:32:58 <hiato-phone> Blag, it's too late-actually early-for this stuff on my phone. cheers all
23:33:35 -!- hiato-phone has quit (Quit: used jmIrc).
23:33:48 * Sgeo has to take a PERL class at some point
23:34:04 <Sgeo> Maybe I should delay that to next year, when I will be taking a different major, and thus might not end up doing PERL
23:35:32 <pikhq> A *class* in Perl?
23:35:45 -!- tombom has quit (Quit: Leaving).
23:35:48 <pikhq> There's really not much to the language. Well. Except there is a lot to the language. :P
23:36:02 <Sgeo> BCS 316 Perl programming
23:36:21 <pikhq> But it's more "We've got a bunch of operators, a bunch of syntax, and cheap regexps" than "there's a massive number of unusual concepts to it".
23:36:36 <alise> http://search.cpan.org/~jwalt/Acme-Lingua-NIGERIAN-1.0.0/NIGERIAN.pm
23:36:39 <Sgeo> "PERL Programming" is the title
23:36:59 <alise> Sgeo: Then it is worse than useless.
23:37:07 <alise> Clearly they haven't the first idea about the language if they know not even its name.
23:37:15 <alise> Probably based on Perl 4, and manually writing CGI scripts!
23:37:33 <alise> I'd suggest just, you know, giving up on whatever uni it is you go to.
23:37:39 <Sgeo> alise, that's the plan
23:37:47 <Sgeo> After this upcoming semester, I'm transferring
23:37:56 <Sgeo> Even though this means I'll graduate much later, probably
23:38:07 <Sgeo> Since after this semester, the next year is my senior year
23:40:24 <alise> You'll like it there. ... You are gay, right?
23:40:33 <augur> no, im not at stony brook
23:40:37 <augur> Gracenotes is at stony brook tho
23:40:41 <alise> Poor Sgeo, missing out on all that rape.
23:40:45 <alise> augur: where be thou?
23:40:54 <augur> University of Maryland
23:40:57 <augur> Sgeo, where are you presently?
23:41:12 <alise> some nothing state university
23:41:20 <alise> ~50,000,000 pupils
23:41:43 <augur> man, we couldve hung out
23:42:05 <augur> you me and gracenotes couldve all hung out
23:42:05 <alise> Sgeo: that wasn't what i heard last time
23:42:06 <alise> [[tlimp: to kiss someone allergic to peanuts. as in John was tlimping all last night = John was kissing someone who is allergic to peanuts all last night]]
23:42:19 <alise> did you try and pick an unpronounceable word there
23:42:22 <augur> aww, alise, you remember :3
23:42:33 <alise> no i just looked at your site lol
23:42:43 <augur> you remembered my site!
23:42:44 <alise> you should have the blog menu on the right it's disturbing on the left./
23:42:57 <alise> like I feel like i'm constantly looking to the right
23:42:59 <alise> it's so irritating
23:43:27 <alise> http://en.wikipedia.org/wiki/State_University_of_New_York_at_Farmingdale no wait that is the one i thought of
23:43:42 -!- FireFly has quit (Quit: Hey! Listen!).
23:43:45 <alise> augur: i won't read your blog anymore
23:43:48 <alise> SHUT UP N-- oh wait
23:43:58 <Sgeo> alise, yes, that one
23:44:35 <alise> what do you mean what
23:44:37 <alise> * FireFly has quit (Quit: Hey! Listen!)
23:44:53 <alise> then you will know my pain
23:53:20 * oerjan uses finite integrals to quickly calculate f(0,x) = 1; f(n,x) = f(n-1,1) + ... + f(n-1,2*x)
23:53:47 <alise> oerjan: See, some of my genius has rubbed off on you.
23:53:53 <oerjan> that was a _huge_ improvement on the actual recursion, even with memoization (i.e. haskell lists)
23:53:55 <alise> Finite integrals are also known as "sums" :P
23:54:15 <oerjan> yeah but it's the theory that is important here
23:54:19 <alise> also why are you calculating that?
23:54:46 <alise> I love how the finite derivative of 2^x is 2^x because 2 is e rounded down
23:55:06 -!- coppro has joined.
23:55:12 <alise> oerjan: that's actually how it was found in the paper
23:55:15 <alise> they tried 2 and 3
23:55:21 <alise> because they were roundings of e
23:55:57 * oerjan is doubtful, for some _unfathomable_ reason
23:56:25 <alise> oerjan: doubtful of what?!
23:56:34 -!- Oranjer has joined.
23:56:56 <alise> i guess it's more accurate to say that e is what you get when, instead of discrete distances where 2 works, you need to handle all the turtles, all the way down
23:57:02 <oerjan> that there was a paper where someone used rounding of e to find that derivative
23:57:47 <alise> it's the paper introducing finite calculus.
23:57:56 <alise> http://www.stanford.edu/~dgleich/publications/finite-calculus.pdf
23:58:52 <oerjan> it sounded like a very silly way to guess the obvious
23:59:33 <alise> I think it's more an explanation.