00:00:13 * Sgeo turns back to Slate 00:01:33 ehird: A universal property in category theory holds all extensional information about an objects behavior: the computational object is just a witness for the universal property 00:02:15 ehird: if we want to do a large scale program it seems necessary to base modules on this: Otherwise a proof might require a computation that spans several modules (and takes hours to compute) 00:02:38 j-invariant: i meant the language you thought you had enough knowledge to implement, but OK :P 00:02:41 ehird: but category theory is not entirely non-computational: So it is very difficult 00:02:53 when did I ever say I have any clue how to make it :P 00:03:46 j-invariant: well i meant presumably you have a "better-than-Haskell" in your head that's like Haskell except better :) 00:03:50 and i doubt that's based on category theory. 00:04:15 oh I don't know if I have any significant ideas to improve haskell 00:04:33 j-invariant: don't you have like 10 languages in your head at once :| 00:04:34 i do 00:04:40 i don't mean improve haskell 00:04:42 j-invariant: what i'm saying is 00:04:52 j-invariant: what language isn't based on category theory, and would be nice to implement this polynomial stuff in, in your head 00:09:11 ehird: the silly thing is, THAT is the language I was trying to implement 00:09:15 :D 00:09:15 call your language CCC+SK 00:09:22 j-invariant: with the polynomials? 00:09:26 j-invariant: hahah lmao that quadrescence post about haskell has got a followup 00:09:27 apparently, 00:09:28 ehird: anyway it's sort of an "algebra system" 00:09:32 since the monad laws aren't automatically enforced, 00:09:36 ehird: except (dependently) typed 00:09:39 and since Monad isn't a subclass of Functor, 00:09:44 Haskell is pseudo-mathematics 00:09:48 ehird: but it's not for writing proofs in, just mathematical algorithm 00:09:48 lol 00:09:49 loool 00:10:03 hmm he isn't here right now 00:10:06 i wonder if he's gone away forever 00:10:07 that would be nice 00:10:08 quadrescence is odd 00:10:17 copumpkin: we've had more than our fair share of him. 00:10:18 his last blog post was ridiculous 00:10:21 more than #haskell. 00:10:38 copumpkin: which one 00:10:45 the one about the cargo cult 00:10:46 Follow-Up to Infamous Post 00:10:48 ? 00:10:49 that's old 00:11:02 copumpkin: yeah, uh, i'm quoting from the follow up to that 00:11:03 lol 00:11:14 I figiured 00:11:16 -i 00:11:38 i started reading his uhh "book" 00:11:44 he seems to think that rewriting languages solve everything 00:11:48 *term rewriting 00:12:07 10.12.27:22:32:19 Quadrescence: can you make any constructive suggestions? 00:12:07 10.12.27:22:33:08 rename monad to something else, delete "morphism" from your vocabulary unless you have reason to need it 00:12:07 10.12.27:22:36:27 Quadrescence: that's not radical enough 00:12:08 10.12.27:22:37:56 ok, rename haskell to Fortran++ 00:12:46 lol 00:13:05 he kept bugging everyone in here to write for his blog :) 00:14:18 ehird: seen cryptol? 00:14:22 j-invariant: ages ago yes 00:14:27 it's ... kinda cool i guess? 00:14:29 ehird: a bit like that, I guess 00:14:37 "kinda cool"?? 00:14:39 :P 00:14:43 i didn't look into it much! 00:14:43 it's great 00:14:51 except non free... 00:14:56 j-invariant: if you're going to write like, a dependent CAS, then i wouldn't try and e.g. implement polynomials in haskell 00:15:00 the idea is good though: Use dependent types 00:15:05 j-invariant: I'd implement a sort-of-symbolic dependent language 00:15:07 and do the rest in that 00:15:23 -!- FireFly has quit (Quit: swatted to death). 00:15:25 dependent types are hard to implement nicely though 00:15:31 and are still hard to program in 00:15:56 ehird: why are you ehird 00:16:23 because i am 00:16:36 copumpkin: says the agda user 00:16:38 coq is soo easy :}}}} 00:16:45 lol 00:16:54 they're still hard 00:16:57 coq and agda are equally useless 00:17:03 well 00:17:08 computers are useless, let's get rid of them 00:17:11 for the specific thing I want to do 00:17:21 j-invariant: you really need your own lang for it i feel... 00:17:27 j-invariant: Axiom is kinda close to what you want in fact. 00:17:35 as in, a dependent CAS 00:17:43 Hmm. The free ATi drivers seem to be genuinely non-shitty these days. 00:19:05 pikhq: i need a unicode cross or something 00:19:06 as in X 00:19:13 or a hollow square or circle 00:19:16 FILL MY NEED 00:21:37 pikhq: . 00:21:39 j-invariant: have you seen Axiom? 00:22:05 Yup, definitely *insanely* better at video display, and I don't actually have a good OpenGL test case... 00:22:32 But as I clearly don't actually use OpenGL much, moot point. :P 00:23:03 -!- jesus_muppet has left (?). 00:23:40 ehird: no 00:23:46 j-invariant: you perhaps should 00:23:57 j-invariant: it's also a gigantic literate program :^) 00:24:42 j-invariant: basically Axiom is this crazy developed-since-1970 literate program that implements a strongly-typed, mathematical type hierarchy-based CAS 00:24:53 j-invariant: http://upload.wikimedia.org/wikipedia/commons/e/ee/Matrixinmatrix.jpg 00:24:55 j-invariant: note the Type: lines 00:25:01 -!- sebbu has joined. 00:25:10 j-invariant: fully symbolic, etc. 00:25:25 ehird: yeah really I should stop being such a hermit and just use existing software 00:25:40 j-invariant: oh i am not saying that axiom is the solution 00:25:44 j-invariant: i'm saying you should look at it :) 00:26:01 j-invariant: http://en.wikipedia.org/wiki/Axiom_(computer_algebra_system)#Documentation click a pdf and start reading :D 00:26:07 ehird: k, ignored 00:26:11 it's the literate program 00:26:14 coppro: oh grow up 00:26:26 why did coppro ignore? 00:26:36 because he's even more childish than I am 00:26:39 because this channel is better without ehird 00:26:40 -!- ehird has changed nick to eherd. 00:26:46 i'm a herd of Es 00:26:59 *this channel is almost silent without 00:27:07 and the bits that aren't silent, mostly incomprehensible one-sided conversations 00:27:32 j-invariant: I think there are probably very few systems developed since the early 70s 00:27:42 that are still in active (non-maintanence) development today 00:27:50 eherd: changing your nick is not sufficient 00:27:54 *maintenance 00:28:00 -!- sebbu2 has quit (Ping timeout: 240 seconds). 00:28:09 coppro: my ident hasn't changed 00:28:14 coppro: so if it's based on nickserv: HI. 00:28:28 -!- eherd has changed nick to ehurd. 00:28:30 Also, OMFG kernel mode setting. 00:28:31 The Axiom project focuses on the "30 Year Horizon". The primary philosophy is that Axiom needs to develop several fundamental features in order to be useful to the next generation of computational mathematicians. Knuth's literate programming technique is used throughout the source code. Axiom plans to use proof technology to prove the correctness of the algorithms (such as Coq and ACL2). 00:28:35 coppro: there's no possible way i'm still ignored now 00:28:42 lol literate programming 00:28:44 wow this is interetsing 00:28:47 I haven't not heard zzo38 today 00:28:56 It makes my framebuffer actually use the native resolution of the display! 00:28:57 :D 00:29:03 OTHER THINGS ZZO38 LIKES: BREATHING 00:29:46 ehurd: this is interesting actually, gonna check it out 00:29:57 j-invariant: "For example, Axiom’s integrator gives you the an- swer when an answer exists. If one does not, it provides a proof that there is no answer." 00:30:13 *answer 00:30:36 j-invariant: "A function can take a type as argument, and its return value can also be a type. For example, Fraction is a function, that takes an IntegralDomain as argument, and returns the field of fractions of its argument." 00:30:47 j-invariant: i think this is more like \Omega{}mega than Agda, though 00:30:54 not sure though 00:32:12 haha 00:32:15 omegamega is so stupid 00:32:53 ehurd: so apparently you have a u now 00:33:19 j-invariant: is it? 00:33:21 coppro: oh indeed 00:33:33 coppro: it's obvious that your ignore didn't fail, btw. 00:33:45 ehurd: it's just crazy, like reimplementing everything at multiple levels? 00:33:53 j-invariant: well i might be wrong 00:33:55 j-invariant: i just meant 00:34:01 j-invariant: i don't think that axiom lets you do actual dependency 00:34:04 j-invariant: i.e. pi types 00:34:08 j-invariant: sigma maybe 00:34:18 j-invariant: i don't know omegamega, so i wasn't trying to draw a strong comparison. 00:35:04 -!- poiuy_qwert has joined. 00:35:05 ehurd: it's probably dynamically checking types 00:35:10 j-invariant: no i do not think so 00:35:13 j-invariant: it's strongly-typed 00:35:24 j-invariant: which volume are you reading? 00:35:25 or are you not 00:36:30 j-invariant: ? 00:36:49 what's this "30 year horizon"? 00:37:08 it's neither sigma, nor pi, nor dynamically checking 00:37:16 -!- drakhan has quit (Quit: Wychodzi). 00:37:30 copumpkin: owhat are you talking about? :D 00:37:36 omega 00:38:57 I was talking about axiom 00:40:01 I am seeing universal properties and categories everywhre 00:40:29 categories are everywhere 00:40:36 so are universal properties! 00:40:43 coppro: I realized that divisibility forms a category 00:40:49 it's an order 00:40:59 any partial order can be made into a category 00:41:04 ^ 00:41:09 j-invariant: it's described at the top 00:41:28 j-invariant: so which volume are you reading 00:41:57 divisibility is more special than any old partial order 00:42:01 -!- pikhq has quit (Read error: Operation timed out). 00:42:43 most partial orders are more special than any old partial order :P 00:42:48 copumpkin: what 00:42:51 j-invariant: helloooo 00:42:52 in fact, we can set up a partial order of partial orders 00:42:54 by specialness 00:43:08 copumpkin: oh you crafty 00:43:14 :D 00:43:29 j-invariant: how many more times should i ping you 00:45:02 j-invariant: 00:45:05 ??? 00:45:29 j-invariant: which volume are you reading 00:45:30 of Axiom 00:45:53 I'm not 00:47:40 j-invariant: you said about the 30 year thing 00:47:43 but that's mentioned in the book 00:47:59 j-invariant: http://axiom-developer.org/axiom-website/bookvol0.pdf is the introduction book which contains all the interesting info 00:48:06 vs. all the implementation details and code in the rest more or less :P 00:48:16 j-invariant: contains the general overview of the system and cool stuff etc. 00:48:54 well ok there's more but 00:49:09 j-invariant: DID I MENTION: category theory plays a large part in axiom 00:49:11 IIRC 00:49:57 although i don't know that for _sure_ 00:52:25 yes you are 00:55:55 j-invariant: are you reading it? :p 00:56:21 j-invariant: i think it's actually surprisingly close to what you were talking about wanting, from reading this volume 0 00:57:00 j-invariant: heh it uses categories to mean something other than what category theory means by them 00:57:02 i think 00:59:31 i think j-invariant fell asleep 01:00:49 hii 01:01:04 j-invariant: are you kirby all of a sudden? 01:01:15 no 01:01:19 ok 01:02:39 ehurd: compare: 01:02:51 (10 http://www.reddit.com/r/compsci/comments/ez93s/the_future_of_software_system_correctness/c1c6ps2 01:02:54 (1) 01:03:09 j-invariant: what's 2 :P 01:03:09 (2) http://www.reddit.com/r/compsci/comments/ez93s/the_future_of_software_system_correctness/c1c7ks6 01:03:24 exactly the same thing except one guy said "prime numbers" and the other guy said "halting problem" 01:03:28 lol 01:03:40 ZOMG ALAN TURING. MUST UPVOTE 01:03:49 fuckin pathetic :/ 01:03:53 not worth getting worked up over! 01:03:57 now read the axiom introduction, it's really interesting :P 01:04:08 i'm only on page 13 and i think it's cool 01:04:09 okay, il be back in a moment 01:04:21 -!- j-invariant has quit (Quit: leaving). 01:09:15 copumpkin: you have strayed into a deadly trap 01:09:22 ? 01:09:51 copumpkin: being the only active person who doesn't have me ignored >:) 01:09:56 now watch as i force you to test my awful software 01:09:58 mwahahahahahahaha 01:10:08 lol 01:10:21 nah, I'm busy 01:10:26 busy testing, yes 01:10:31 my god, it's 381 lines 01:10:32 how did that happen 01:12:51 -!- j-invariant has joined. 01:17:11 http://www.reddit.com/r/programming/comments/cw06e/the_mercury_language_take_prolog_speed_it_up/c0vpmgg 01:18:28 Sgeo: tell me how ehird bashes it ok 01:18:41 What I linked to was a joke 01:18:58 Although yeah, I'm looking at Mercury 01:18:59 Sgeo: why does it say "Yes"? 01:19:27 j-invariant: it's funny because prolog impls print yes 01:19:37 Sgeo: prince xml was written in mercury, btw 01:19:53 and is a very advanced, complex program, sold for lots of money, with a small binary size 01:20:00 o.O 01:20:03 converts XML/HTML + CSS into PDF, basically, with very high quality 01:20:11 http://princexml.com/ 01:20:16 coppro, ehurd is not bashing Mercury. 01:20:17 proof that the language can do shit, at least 01:20:17 ehurd: no they don't? 01:20:22 Sgeo: impossible 01:20:27 j-invariant: yes they do 01:20:30 This sort of reaction is what got me interested in Factor so long ago 01:20:34 j-invariant: well... 01:20:34 he didn't mention it first 01:20:36 j-invariant: ok they actually don't 01:20:36 so it can't be good 01:20:38 but they print No! 01:20:40 and that's what matters 01:20:43 ehurd: that's some stupid SWI prolog thing 01:20:49 oh wait no it's not 01:20:59 Sgeo: well i wouldn't want to write an actual program in Mercury myself. 01:21:10 logic programming doesn't gel with me. 01:21:27 but the fact that it has no cut or side-effects is nice :) 01:21:58 j-invariant: do you want to try out the initial cled prototype :D 01:22:14 yes 01:22:36 j-invariant: http://www.vjn.fi/pb/p7989249361.txt 01:22:39 j-invariant: just run as: python cled.py 01:22:48 try not to defocus the window afterwards, it doesn't like that 01:23:06 j-invariant: most of the underlying stuff is written but not exposed as the ui... but it can manipulate integer argument lists! 01:23:15 The tutorial could use some work 01:23:33 j-invariant: quick rundown: lilac background means it's selected. j and k move around the current active object, selecting children of it, showed by highlighting with lilac. 01:23:50 j-invariant: e descends into the currently selected object. d ascends upwards from any objects. 01:24:04 j-invariant: if you descend into an integer, then you can rewrite the integer by typing a new one and hitting or d. 01:24:26 mutable inteegers... 01:24:27 j-invariant: to add a new element to a list (only in . -> things now (they're called examples)), press = to insert after the current element. + (shift-=) to insert before. 01:24:29 j-invariant: no 01:24:31 j-invariant: it's an editor 01:24:40 j-invariant: it's like seeing 42, pressing backspace twice, and typing a new on 01:24:40 e 01:24:44 it's an AST-based code editor 01:24:52 j-invariant: press x to delete an argument. 01:25:07 j-invariant: now, if you do =, it's "?", because it's waiting to decide what type you'll put in based on your input 01:25:09 this is called a box 01:25:16 if you d before entering a type, you'll see an ugly red ? in your program 01:25:21 these are call boxes, but they should be called holes. 01:25:30 they're basically just things that need objects but haven't filled in yet 01:25:36 nice it works! 01:25:39 if you try and delete the output of an example, or all the inputs, you just get a single box instead 01:25:44 that's pretty much it for now 01:25:48 note that if you ascend too far everything breaks 01:25:59 oh 01:26:06 and "r" replaces the current selected thing with a box 01:26:11 which will probably be useful somehow! 01:26:17 it's possible to descend too far?? 01:26:21 j-invariant: no 01:26:23 but you can ascend too far 01:26:37 if you try and go above the list of examples 01:27:03 j-invariant: oh and Ctrl+S prints the current program to stdout 01:27:10 note that if you have boxes, this'll be an invalid program 01:27:38 cool 01:28:10 oh and you should be able to enter [ into a hole instead of a digit or -, to get a list 01:28:12 but that doesn't work yet :) 01:28:31 j-invariant: incidentally, the programs are pretty-printed. 01:28:46 so for instance it outputs 01:28:47 depth of first ~ {. 0 -> 0 01:28:47 . 5 -> 0 } 01:28:48 depth of first ~ {:. [[1 2] [3 4]] -> 2 01:28:50 : [1 2] -> 1 01:28:52 :. [[[1 2 3] 4] 5] -> 3 01:28:54 : [[1 2 3] 4] -> 2} 01:28:56 depth of first ~ is list?; cons; car; cdr; succ; 0 01:28:58 with the right alignment everywhere 01:29:00 (that isn't generated by the code, but i know it does it properly :)) 01:29:06 (or wait i think i did feed it in at some point. anyway.) 01:30:24 j-invariant: i'm not going to be able to convince you to read the first volume of axiom, am i :D 01:30:59 -!- azaq23 has quit (Ping timeout: 255 seconds). 01:33:06 ok i'll stop bugging you about it 01:34:18 -!- BeholdMyGlory has quit (Remote host closed the connection). 01:35:16 -!- azaq23 has joined. 01:37:37 -!- copumpkin has quit (Quit: Computer has gone to sleep.). 01:40:18 ehurd: I am going to read it 01:40:25 j-invariant: \o/ 01:40:26 | 01:40:26 |\ 01:40:46 j-invariant: I don't think it does do type-checking at runtime... that would be lame anyway 01:40:54 Also I like the idea of it more if it doesn't :P 01:41:14 j-invariant: lol, you declare a module system like you do types, and even structures (like ring) 01:41:17 it's all the same mechanism 01:41:43 "Because the argument of Matrix is required to be a Ring, Axiom will not build nonsensical types such as “matrices of input files”." 01:41:47 brb implementing matrices of input files 01:41:59 j-invariant: yep, just read, it typechecks at compile times 01:42:01 *time 01:43:18 *just read that it 01:44:06 -!- poiuy_qwert has quit (Read error: Connection reset by peer). 01:45:10 ehurd: wow, both great 01:45:14 that's good 01:45:44 i'm only on page 21... wonder how much mindbending stuff is in the next 1198 pages 01:45:45 -!- poiuy_qwert has joined. 01:45:59 erm actually page 40 01:46:04 but 21 in the actual book 01:46:24 pretty huge book, considering this is only volume 0 01:46:32 i wonder if you can buy a complete set bound in leather that takes up a whole shelf 01:47:05 j-invariant: btw here's a link, mostly for my logreading benefit since i had to find it again before: axiom-developer.org/axiom-website/bookvol0.pdf 01:47:08 *http://axiom-developer.org/axiom-website/bookvol0.pdf 01:49:30 j-invariant: this seems to do a lot of stuff as polynomials, lol 01:49:39 i think you've accidentally reinvented this 01:50:02 j-invariant: mind you, i'd still like to see what you come up with 01:50:39 "The function factor can also be applied to complex numbers but the results aren’t quite so obvious as for factoring integer: 01:50:39 144 + 24*%i 01:50:39 144+24 i 01:50:41 Type: Complex Integer" 01:50:45 i smell a documentation bug 01:52:12 "Chapter XXX describes these modules in 01:52:12 more detail." 01:53:52 Sgeo: hur hur it's funny because ex 01:53:53 sex 01:53:59 No 01:54:03 what then 01:54:12 I'm just complaining about the incompleteness of the documentation 01:54:35 how is that incomplete 01:54:47 Sgeo: ? 01:55:02 Sgeo: it's a book, what's the issue 01:55:07 Those XXXs are all over the place 01:55:15 Sgeo: It's a number, isn't it. 01:55:16 30. 01:55:19 No 01:55:29 I assume you're talking about Axiom? 01:55:36 I'm talking about Mercury 01:55:38 Oh. 01:55:42 Then I don't care! Yay! 01:55:50 j-invariant: should i make my own language 01:55:58 what about it 01:57:15 -!- Wamanuz has quit (Ping timeout: 240 seconds). 01:57:18 j-invariant: semi-dependent-typing, in that it has kinds and metakinds etc. etc. etc., and kinds are automatically derived from normal data types (with the same name and constructors), /but/ nothing crosses the : 01:57:22 j-invariant: i.e., no pi types 01:57:29 because 01:57:32 that sounds easier to implement :D 01:57:40 bye 01:57:41 -!- ehurd has quit (Remote host closed the connection). 02:01:19 -!- poiuy_qwert has quit (Read error: Operation timed out). 02:01:26 -!- luatre has quit (Remote host closed the connection). 02:04:13 -!- copumpkin has joined. 02:06:16 -!- poiuy_qwert has joined. 02:11:20 -!- cheater99 has joined. 02:24:06 -!- poiuy_qwert has quit (Read error: Connection reset by peer). 02:26:26 -!- poiuy_qwert has joined. 02:27:38 Formal proof of correctness is not only tedious, time-consuming, and outlandishly expensive, it's also not necessarily effective! People commit errors when attempting a formal proof. There is no fool-proof way of determining if a proof is correct or not. -- JeffGrigg 02:28:30 uh yes there is 02:28:36 clearly he doesn't know what a formal proof is 02:29:42 lol 02:30:11 -!- oerjan has joined. 02:30:21 oerjan! 02:30:34 morning orejan 02:30:37 j-invariant: wait what? 02:30:43 j-invariant: it says "adjunction" posted that 02:30:43 oerjan 02:30:50 but adjunction clearly doesn't think that 02:30:54 because I've seen other things he posted 02:32:12 * copumpkin is confused 02:33:24 ¡coppro, oklopol 02:35:25 maybe j-invariant is adjunction 02:38:35 * Sgeo needs MORE 02:38:38 MORE LANGUAGES 02:38:39 MORE 02:38:43 * Sgeo goes nuts 02:38:54 Sgeo: learn all languages at once: Oz 02:39:04 I find myself interested in the concept of dataflow programming 02:39:15 j-invariant, is there still any work being done on Oz? 02:39:25 Last ... thingy was 2008 02:40:44 " j-invariant: yeah there is basically no way you could do recursive functions (only flow control other than branching really) with a stupid search like that" <<< actually i have a good feeling about another way to do recursion stuff, although the idea is so simple i'll want to try it before saying it might work 02:41:00 but i'm usually right, like i was right about demolishing! 02:41:11 ...wait 02:41:27 oklopol: i am incapable or ferror 02:42:04 demolishing/ 02:44:36 -!- poiuy_qwert has quit (Read error: Connection reset by peer). 02:46:01 http://en.wikipedia.org/wiki/Monad_%28category_theory%29 02:46:14 -!- poiuy_qwert has joined. 02:46:34 " 21:29 cdsmithus: EvanR-work: It's pretty easy to see. Just enumerate all the 0-length strings (finitely many), then all the 1-length, then the 2-length, and so on. Every finite string has some length, and will be reached eventually" <<< this doesn't work 02:48:25 um yes it does 02:48:34 as long as your alphabet is finite 02:48:35 PENIS 02:49:09 if your alphabet is countably infinite, though... 02:49:32 you can still enumerate it. 02:49:35 yes. 02:49:55 "Googles Go language uses a quicksort, though this is considered by some to be a bug. 02:49:56 " 02:49:57 lolwhat? 02:50:04 length + sum(ord(chr)) < n 02:50:22 Ah 02:50:22 that would be one way 02:51:13 "Somewhat typical of PHPs API, there are actually thirteen different built-in array sorting functions" 02:51:55 what is that about 02:52:04 oklopol: i am incapable or ferror <-- so, which one is it? 02:52:18 oerjan: it's both. 02:53:48 Sgeo: quicksort has bad worst-case behavior... 02:54:03 I said "Ah" after reading the compaints 02:55:01 yeah, "Ah" is such a heavily information-loaded word 03:01:15 -!- j-invariant has quit (Quit: leaving). 03:03:02 " oklopol likes Python for, like, totally different reasons to everyone else." <<< the reason i like python is i used to like it, and used it so much it's soooooooooooo easy now. this is also why my programs are so retarded in syntax and how i do things locally, i actually don't think at all, i just write 03:03:41 -!- quintopia has quit (Ping timeout: 255 seconds). 03:04:35 -!- poiuy_qwert has quit (Read error: Connection reset by peer). 03:06:13 -!- poiuy_qwert has joined. 03:06:29 ' Why don't we get people that just learned thermodynamics and join every fucking energy discussion with "YYEAH BUT YOU CANT CREATE INFINITE FREE ENERGY SO WHY BOTHER WITH WINDMILLS?"' xD 03:06:42 -!- quintopia has joined. 03:07:36 oklopol, you like Python for the same reason I do! 03:07:50 I am more practiced with Python than any other language 03:10:06 oerjan, Sgeo Java has some weird behavior. <= 7 elements it uses insertion sort and > 7 it uses quicksort 03:12:40 variable: well that's not so weird 03:12:56 it's well known that simpler sorts are faster for very short lists 03:13:07 also pure quicksort? 03:13:09 oerjan, actually it happens to be optimal for other reasons as well 03:13:09 no introsort? 03:13:11 coppro, erm no 03:13:17 I meant to say "modified quicksort" 03:13:33 and the number 7 isn't arbitrary either 03:14:06 well i'd assume without evidence that the <= 7 case is also used for sorting sublists in the quicksort? 03:14:25 oerjan, yes 03:14:54 * variable gets the source - hang on 03:16:06 oerjan, 03:16:29 Java's sort is based on http://portal.acm.org/citation.cfm?id=172710 03:17:46 " um yes it does" " as long as your alphabet is finite" <<< also the algorithm of doing nothing works. (as long as the alphabet is empty) 03:18:09 no bloody abstract 03:18:10 How long until we have non-Python languages running on CPython? 03:18:28 oklopol: BRILLIANT 03:18:40 Atomo runs on Haskell's whatever, a bunch of stuff runs on Erlang's VM, I'm pretty sure there's Ruby stuff.... 03:18:46 JVM and .NET are obvious 03:19:18 oerjan, Sgeo btw - I was talking about an array of ints 03:19:28 it uses something else (I think merge sort) for objects 03:19:35 variable: huh 03:19:47 oerjan: if you'd read context from 64 hours ago, you'd've known alphabet was just specified countable 03:20:01 oerjan, int[] array is sorted differently than Integer[] array 03:20:03 oklopol: O KAY 03:20:54 variable: i guess they are assuming comparing two elements is so much more expensive then that it affects things... 03:21:17 there should be a nonstandard set theory: \exists set S such that S^N is finite, but S is nonempty 03:21:28 (from nonstandard analysis, although that was probably clear) 03:21:38 oerjan, I don't remember exactly what they use to sort Objects. I __think__ its merge sort 03:23:15 variable: hm. i could see why they'd want to use a different cutoff but not why they'd switch to another sort for large arrays entirely 03:24:15 oerjan, I'm no Java expert - I just spent one semester too long learning Java :-\ 03:24:47 well me neither 03:24:59 i haven't even learned it properly 03:25:24 i know everything about java, but i still can't understand love 03:26:29 I love the java jive and it loves me 03:28:14 i hate the halting problem 03:28:40 it's like the least interesting piece of math ever, and everyone thinks they understand what it means on a deep philosophical level 03:29:47 it should be stripped of its popularity by force 03:30:26 oerjan so 03:30:33 ...it is the basis of most other undecidability theorems, isn't it 03:30:35 did you catch my inverse semigroup stuff 03:30:36 :D 03:30:40 NO 03:30:43 * oerjan runs away 03:30:45 oerjan: it's a very important theorem, yes 03:31:21 it shouldn't be uninvented or anything 03:31:28 there's tons of interesting stuff *on top of it* 03:32:48 it's the popularity that annoys me 03:33:03 oh, well right, it's not actually the *least* interesting piece of math ever, maybe :D 03:33:44 but it's not a particularly interesting theorem 03:34:44 and i always hate it when someone tries to add ugly technicaly philosophy to a beautiful and pure formal mathematical theorems 03:34:54 *technical 03:35:26 -!- variable has quit (*.net *.split). 03:35:35 -!- Slereah has quit (*.net *.split). 03:35:39 -!- jix has quit (*.net *.split). 03:35:49 + more random adjectives before the terms why not 03:35:51 it's like listening to a philosophy prof talk about math 03:35:58 it's almost actually painful 03:36:40 oerjan: i proved that in an inverse semigroup (so *unique* y such that x = xyx, y = yxy), idempotents form a semilattice 03:37:42 coppro: i haven't actually heard, but my dad studied philosophy, and he could recite these completely meaningless statements he'd learned for class that were some sort of explanations for the achilles paradox etc 03:37:44 mhm 03:37:51 -!- Slereah has joined. 03:37:51 -!- jix has joined. 03:38:16 well 03:38:24 maybe they weren't meaningless originally, but my dad butchered them completely :D 03:38:54 -!- calamari has quit (Quit: Leaving). 03:39:02 -!- variable has joined. 03:40:11 but in any case, who the fuck needs to learn about the achilles paradox... if i started studying philosophy, and i realized i was listening to a *lecture* about that retarded thing, i'd probably take a good look in the mirror, and kill everyone. 03:40:42 oerjan: THAT'S NOT ALL THOUGH 03:40:46 ...about inverse semigroups 03:40:48 um if you don't know any calculus and stuff then it probably _is_ somewhat mysterious 03:42:24 yes, possibly; now consider an arbitrary congruence on an inverse semigroup 03:42:34 (in the usual semigroup sense) 03:42:49 (although it does turn out that the quotient is an inverse semigroup) 03:42:59 * Sgeo surrenders and goes to install Cygwin 03:43:33 (that's not actually trivial i think, you need lallement's lemma, which says for all idempotents in the image, there is an idempotent in the preimage) 03:43:46 let's call this congruence p 03:44:37 we define x p_{min} y <=> \exists e \in E_S: xe = ye, x^-1 x p e p y^-1 y 03:45:04 that's an equivalence relation, since idempotents commute 03:45:19 wait... 03:45:42 let that be true for xe = ye, yf = zf 03:45:55 then i was thinking xef = yef = yfe = zfe = zef 03:46:05 but is the second thing true 03:46:23 oh well of course it is 03:46:44 what's E_S 03:46:49 because we know y^-1 y p f, and therefore e p f, and therefore also x^-1 x p f 03:46:51 oh sorry 03:46:52 idempotents 03:46:56 forgot to define 03:47:24 so yeah that's an eq relation, but here's the fun thing: that's actually the minimal congruence with the same trace 03:47:45 there's some = missing up there 03:47:54 where? 03:48:04 x^-1 x p e p y^-1 y 03:48:07 p is a relation 03:48:14 i mean 03:48:15 congruence 03:48:24 oh 03:48:37 * oerjan somehow started reading it as an idempotent 03:48:38 it was rho in the lecture notes, and i'm copy pasting from my head 03:48:51 the definition anyway 03:49:06 Hmm... Does ShowIP have some subtle bias: IPv4 addresses get shown as red and IPv6 addresses as green... :-) 03:49:06 so for instance, consider the trivial congruence S x S 03:49:13 let that be p 03:49:33 then, p_{min} is actually the minimal congruence q such that S/q is a group 03:49:49 because a quotient is a group if and only if idempotents are identified 03:50:18 because an inverse semigroup is a group iff it has exactly one idempotent 03:51:14 to prove that \exists e \in E_S: xe = ye, x^-1 x p e p y^-1 y is a congruence, you prove that it's a left congruence and that it's a right congruence separately, and that's actually kinda technical 03:51:23 because you have to guess the idempotent 03:52:11 but so let x p_{min} y, and e be the proof; consider xz vs. yz and the idempotent z'ez where ' is inverse 03:53:04 then xzz'ez = xezz'z = xez = yez = yezz'z = yzz'ez 03:53:12 aaaaaaand umm 03:53:15 oklopol: i don't think i'm capable of concentrating enough to follow this stuff 03:53:23 alright :P 03:53:27 did you get the actual theorem tho? 03:53:42 i think that's really nice even if i skip the proof 03:54:12 that for each congruence p, there's minimal p_{min} with the same trace, with that definition i gave 03:54:16 fuck 03:54:21 trace = what idempotents are identified 03:54:33 i'm not very organized :\ 03:54:48 that's hard too because i don't have an intuition for how "inverses" are supposed to behave 03:55:35 hm wait is x^-1 x = x x^-1 always? 03:55:46 like in groups, except that there are multiple 1-elements. 03:55:51 is my intuition 03:55:54 ok 03:56:08 x^-1 x = x x^-1 <<< no, but both are idempotent 03:56:45 idempotents commute, so often you just care about the fact you have *some* idempotent somewhere 03:57:01 should give examples maybe, have none... 03:58:59 it took me quite a while to get a grip on how inverse semigroups work 03:59:34 so i don't exactly blame you if you have no ability to follow the stuff, mainly i wanted to advertise properties of inv semigroups... :D 04:00:09 like that p_{min} thing, which is unique to inv semigroups in the semigroup monoid group etc family 04:00:16 (afaik!) 04:00:36 Fun use for ShowIP. Visit all sorts of IPv6-related sites and see which ones support IPv6. 04:00:40 (erm i mean of course it's true for groups......) 04:00:45 (but yeah) 04:01:28 alright my alarm clock is tickling. 04:02:47 Ilari: ooh, i guess we're just a week or two from exhaustion now? 04:03:11 or has it already happened 04:03:23 (that APNIC allocation thing) 04:03:34 algebra is so damn sexy really, if i was any good at it, i might even consider doing my phd out of that stuff 04:04:08 oklopol: tickling alarm clock? 04:04:38 well i mean i'm awesome at it but i don't really have an intuition on what constitutes as interesting new research 04:04:49 Not yet... Projections are turn of the month... But APNIC can justify allocation at any moment. 04:05:22 of course, i suppose you should always try to follow the road of *actually solving problems* 04:05:35 * oerjan imagines bosses at APNIC headquarters sitting rubbing their hands and cackling maniacally 04:05:43 oerjan: tickling sounds like it could mean some sort of beeping imo 04:05:55 and i already once used that word wrong in your presense 04:06:04 presence 04:06:11 oklopol: well there are already vibrating cell phones... 04:06:28 :D 04:06:37 but a tickling alarm clock would sort of have to be _in_ your bed... 04:06:51 my bed is too full of stuff to fit an alarm clock 04:06:54 well or it could be a wrist watch i guess 04:07:04 oklopol: do you have room to sleep :D 04:07:28 well, almost! 04:07:37 i should consider cleaning up this place at some poitn 04:07:39 *point 04:07:45 AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAaa 04:07:49 don't remind me 04:08:17 it's been about a week and i haven't moved any of the stuff, and since i moved from a twice bigger apartment, there's suddenly huge amounts of stuff :D 04:08:33 oh right 04:10:16 these student apartments are so crappy i'm actually considering applying for a better one, mainly due to the facts i'm never going to be able to eat food if i have to prepare it in the presence of other people, everyone hears me watch porn at night and the fact the refrigerator wakes me up at 4 am ever morning 04:10:50 the last one is actually not annoying at all, i just wanted to mention it :D 04:11:05 -!- azaq23 has quit (Ping timeout: 255 seconds). 04:11:56 but a place full of students is like the worst place to have thin walls, at 4 am on a wednesday, it's not rare to feel someone suddently yell "WHAT THE FUCK MAN?!?" 04:12:04 argh 04:16:37 It appears most dedicated IPv6 sites have IPv6 addresses... But some don't. 04:19:46 Last entry on IANA allocations for IPv6: 2006-10-03... That's over 4 years ago... 04:27:37 -!- hagb4rd has quit (Ping timeout: 240 seconds). 04:38:17 -!- quintopia has quit (Ping timeout: 264 seconds). 04:44:55 Whee... Mac OS X doesn't support DHCPv6 (according to these slides). 04:45:53 Haha... Blank slide titled "Response from Users". 04:51:08 -!- quintopia has joined. 05:17:06 -!- azaq23 has joined. 05:22:55 -!- hagb4rd has joined. 05:27:53 http://www.youtube.com/watch?v=-CGIii_eTOk 05:28:01 :'/ 05:30:32 -!- poiuy_qwert has quit (Read error: Connection reset by peer). 05:31:39 -!- Mathnerd314 has quit (Ping timeout: 264 seconds). 05:31:49 -!- poiuy_qwert has joined. 05:37:14 http://www.youtube.com/watch?v=p3bkmD-70e4&feature=related&fmt=18 05:38:28 All C#-like languages bore me 05:39:41 * Sgeo says that as he listens to a song he STRONGLY associates with Vala 05:40:08 * oerjan wonders why Sgeo adds the # 05:40:35 Because most of these highly marketed languages are closer to C# than C? 05:40:45 Although yeah, C-like bores me too 05:40:58 Not "highly" I guess. Hmm 05:41:33 -!- mycroftiv has quit (Ping timeout: 255 seconds). 05:41:47 well, it might be interesting experimenting with words, rhymes & rhytm.. but language becomes indefferent if u really want to say something 05:42:41 * oerjan was not aware that C# had spawned its own subfamily 05:43:59 Most dedicated IPv6 sites support IPv6... But seems that many don't. :-) 05:44:27 Ugh. We really need to get on the ball and start supporting IPv7. 06:02:23 Shortest IPv6 address I have seen on public webserver: 11 characters. Longest: 39 (which is the longest possible). 06:04:09 I believe the shortest possible valid IPv6 unicast address would be 9 characters... 06:05:09 Ah, actually, nope... 7. 06:05:55 -!- cal153 has quit (Read error: Connection reset by peer). 06:07:37 -!- cal153 has joined. 06:07:56 2003::1 is at least an allocated address. 06:14:15 i'll locate _your_ address 06:16:06 What happens when we run out of MAC addresses? 06:18:36 Only 2^6 organizations can make network cards? 06:19:04 64 06:19:11 64 manufacturers 06:19:16 Past that, we run out 06:23:11 2^6? 06:23:13 where'd you learn to math 06:23:17 6 HEX digits 06:23:49 mac addresses are 12 hex digits; first half is manufacturer, second is device 06:24:52 > 16^6 06:24:53 16777216 06:25:43 onoez. each manufacturer can only make 16m nics! 06:25:55 or, they can get another id 06:25:58 exactly 06:26:00 maybe they give them out in ranges 06:26:02 * myndzi shrugs 06:26:06 which is why it's stupid to break it up that way 06:26:15 gotta break it up somehow 06:26:17 16^12 06:26:21 > 16^12 06:26:22 281474976710656 06:26:29 better to hand out multiple ids to a manufacturer than give too many device ids to one and nobody can use them 06:28:18 why not just hand out ranges of MACs on a need-some-more basis and just have a public database if you really need the manufacturer? 06:28:23 it works for IPs... 06:28:36 i dunno, i just sorta guessed it was something like that 06:28:55 http://www.coffer.com/mac_find/ 06:28:58 huh how about that 06:29:07 first google result for "mac address manufacturer database" ;P 06:29:08 heh 06:29:31 http://standards.ieee.org/cgi-bin/ouisearch 06:29:36 also that 06:29:48 it does look like an as needed basis 06:29:53 intel has a bunch but they aren't consecutive 06:32:51 Oops 06:32:59 Wait 06:33:03 3com cards used to be 00:01:02, but now they have a billion (for billion = 47) vendor IDs. 06:33:17 Wikipedia says 8 bits for the manufacturer 06:33:41 There are some flags in the upper bits. 06:33:46 At least two. 06:33:54 Oh wow, I misread the image 06:34:59 Maybes I needs sleep 06:35:00 s 06:38:24 i just don't understand why they need to assign them in 16m chunks 06:38:35 not that i care all that much 06:39:26 Assigning in smaller units would mean more processing of "gimme more" forms. 06:39:46 ha 06:39:53 I guess the assumption is that if you're manufacturing chips, you're going to do a lot of them. 06:41:10 i wonder how many vendors go out of business or stop manufacturing right in the middle of a block. or right at the beginning of one even 06:44:07 They've only allocated 14503 OUIs out of the 4194304 possible, so we don't seem to be running out just ye. 06:44:17 s/ye\./yet./ 06:45:27 -!- azaq23 has quit (Quit: Leaving.). 06:45:33 What is Rexx, and why is it so low on popularity charts 06:45:37 Often lower than COBOL 07:01:28 -!- Zuu has quit (Read error: Connection reset by peer). 07:01:34 -!- Zuu has joined. 07:07:25 There are quite many Rexx-using Amigists, due to ARexx; but maybe that does not count. 07:08:01 It's not-so-uncommon as an embedded scripting language sort of thing. 07:11:00 I guess you could even call ARexx the Amiga AppleScript, except that sounds pretty silly. 07:12:51 Also I'd like to mention that I'm not an Amiga user, but some of my best friends are (er... were), and there is nothing "wrong" or "shameful" about being one, despite what some people say. 07:21:41 morning 07:22:03 or should I say night. 07:22:44 Woke up due to electric saw. Which was used due to the people here to repair the leaking water from the roof. Oh well. 07:23:02 It is already morning-time. 07:23:38 fizzie, it isn't morning until 09:00 IMO 07:23:52 fizzie, and even then only if it has to be. 07:24:16 fizzie, I was woken up by this sound at 07:33 07:24:22 I'd classify anything before 04:00 as night, after 06:00 as morning, and the part in the middle is a bit of a grey area. 07:24:29 I was woken up by an alarm clock at 07:10. 07:24:38 Well, briefly, anyway. 07:24:51 It didn't quite "take", and then I actually got up at 08:10 or so. 07:24:54 fizzie, I prefer morning to start at 10:00 and end at 11:30 07:25:14 11:30-12:00 is "förmiddag" (can't remember English word for that atm) 07:25:30 (wait, does English have afternoon but not prenoon?) 07:26:39 They sort-of have a "forenoon", but I think that's a bit rare. 07:27:19 Also WordNet conflates that with "morning". 07:27:26 1. morning, morn, morning time, forenoon -- (the time period between dawn and noon; "I spent the morning running errands") 07:27:41 OED lists it separately, but still as "The portion of the day before noon". 07:28:33 I don't think they quite separate morgon/förmiddag like we do. (That's fi: aamu/aamupäivä.) 07:30:40 Even going by the dawn-based definition of "morning", it already is that here: sunrise today is at 09:15, and it's about 09:30 now. 07:32:57 you pesky southerners and your early mornings 07:45:32 Intriguing: Trondheim (suggested by grep) is at 63.43N (10.395E) while Lieksa (the place I'm sort-of from except not quite) is at 63.32N (30.025E); that's only a 12 kilometre difference in the North-South direction. 07:48:01 heh i guess it's just the timezone difference then 07:48:37 The "from" was also in sort of an "originally from" sense; currently I'm in Helsinki, which is quite a lot southener. 07:49:01 Or more accurately Espoo, I guess. 07:49:07 oh 07:50:41 -!- drakhan has joined. 07:51:00 60.1868N 24.8218E is the location of this university building; that's 361 km southwards. (And then take a right turn and go east for a bit.) 07:51:13 (That's the 270-degree right turn.) 07:51:35 ...RIGHT 07:51:47 -!- drakhan has quit (Client Quit). 07:52:36 (I can't seem to tell my left hand from my right.) 07:52:57 WELL GET A TATOO THEN 07:53:02 *TATTOO 07:53:12 A knuckle tattoo, with the left hand saying LEFT and the other one RGHT. 07:53:23 :D 07:53:49 i call rule 34 on that, or something 07:54:22 no google, i _am_ trying to search for rght 07:54:24 oerjan: http://www.knuckletattoos.com/gunCache/t_LEFTRGHT.jpg -- it has the benefit of being also wrongly oriented! 07:54:52 ooh 07:55:09 well that's obviously photoshopped 07:55:23 Well, yes, it's a generator that makes those images. I just entered LEFTRGHT in it. 07:55:47 ah 07:56:47 sadly google seems to fail me 07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 08:14:35 -!- MigoMipo has joined. 08:16:17 -!- Wamanuz has joined. 08:30:36 -!- Vorpal has quit (Read error: Operation timed out). 08:33:46 -!- Vorpal has joined. 08:33:50 -!- Vorpal has quit (Changing host). 08:33:51 -!- Vorpal has joined. 08:36:09 -!- pikhq has joined. 08:48:33 -!- FireFly has joined. 08:49:22 -!- SimonRC has joined. 08:58:27 -!- GreaseMonkey has quit (Quit: ilua). 09:18:56 -!- oerjan has quit (Quit: leaving). 09:50:25 -!- MigoMipo has quit (Read error: Connection reset by peer). 10:19:50 -!- j-invariant has joined. 10:48:37 -!- Wamanuz has quit (Ping timeout: 240 seconds). 11:08:51 -!- mycroftiv has joined. 11:14:26 -!- cheater99 has quit (Ping timeout: 240 seconds). 11:21:02 -!- drakhan has joined. 11:29:11 -!- cheater99 has joined. 12:01:12 -!- sebbu has quit (Ping timeout: 276 seconds). 12:02:38 -!- jcp has quit (Read error: Operation timed out). 12:06:29 -!- jcp has joined. 12:07:52 -!- FireFly has quit (Quit: swatted to death). 12:12:06 -!- ais523 has joined. 12:13:24 -!- cheater00 has joined. 12:15:12 -!- cheater99 has quit (Ping timeout: 240 seconds). 12:25:10 wow, first time ever that a spam message went through all the other filters server-side and was caught by my email client 12:51:56 you should cherish this moment 12:52:03 it's obvious it was DESTINED to be 12:52:12 maybe you should read it and memorize it 13:17:21 -!- Sgeo_ has joined. 13:19:02 -!- cheater- has joined. 13:19:34 -!- Sgeo has quit (Ping timeout: 240 seconds). 13:21:58 -!- cheater00 has quit (Ping timeout: 240 seconds). 13:54:15 -!- poiuy_qwert has quit (Read error: Connection reset by peer). 13:55:51 -!- poiuy_qwert has joined. 13:56:47 Is Clean worth learning? 13:57:00 I think it's just haskell without monads? 13:59:26 -!- azaq23 has joined. 14:00:47 * Sgeo_ isn't particularly interested in Clean being faster 14:00:57 There are some things that I can imagine being interested in 14:01:08 Other than the language itself 14:01:13 huh? 14:02:35 Say, things like a more.. convenient environment to work with, etc 14:02:58 Better module system or whatnot also, although I guess that's a language thing 14:04:23 * Sgeo_ gets bored and wanders off 14:09:44 "I think that there is a market for books with fewer pages; there 14:09:44 are many people out there that need to learn computer science, but do 14:09:44 not appreciate reading" 14:09:47 Fuck you 14:10:36 ...suddenly I think this Preface is meant in jest 14:14:14 -!- poiuy_qwert has quit (Read error: Connection reset by peer). 14:15:30 Sgeo_: LOL 14:15:50 -!- poiuy_qwert has joined. 14:19:19 Grr 14:19:33 Book says to use the Everything environment. There is no Everything environment. 14:20:58 Meh 14:22:51 -!- FireFly has joined. 14:34:14 -!- poiuy_qwert has quit (Read error: Connection reset by peer). 14:35:53 -!- poiuy_qwert has joined. 14:37:40 -!- poiuy_qwert has quit (Read error: Operation timed out). 14:37:55 -!- copumpkin has quit (Quit: Computer has gone to sleep.). 14:59:39 -!- Wamanuz has joined. 15:00:44 -!- poiuy_qwert has joined. 15:00:56 -!- azaq23 has quit (Ping timeout: 272 seconds). 15:03:38 -!- copumpkin has joined. 15:03:39 -!- copumpkin has quit (Changing host). 15:03:39 -!- copumpkin has joined. 15:06:31 -!- oerjan has joined. 15:09:32 I think it's just haskell without monads? 15:09:53 iirc clean is complete capable of monads, it's just that it doesn't need them for IO 15:09:57 *completely 15:10:35 using uniqueness typing instead to thread the "world" through computations. 15:11:33 Is it interesting enough to play with? 15:11:38 And fall in love with? >.> 15:11:46 this allows many computations to be performed with in-place updating, but yet be conceptually pure 15:12:14 I think I like that thought 15:12:22 But I want more 15:12:26 Better module system etc 15:12:50 * oerjan doesn't recall what module system clean has 15:15:02 -!- MigoMipo has joined. 15:16:12 "It is also available with limited input/output capabilities and without the "Dynamics" feature for Apple Macintosh, Solaris and Linux." 15:16:13 Grah 15:16:15 That sucks 15:18:15 I like things that have a theme naming thing going on. Like the "awesome" window manager, which has a standard scripting library called "awful", a theming thing called "beautiful", widget thingies called "wicked", "obvious" and "vicious", a notification thingie called "naughty", and so on. 15:18:29 fizzie, so do you love Newspeak? 15:18:33 (To clarify: I don't like the WM that much, just the naming.) 15:18:49 Brazil, Hopscotch, MiniTest, etc 15:19:16 [Not actually sure if Hopscotch fits thematically] 15:20:02 Why didn't shutup bother me? 15:20:04 -!- Sgeo_ has changed nick to Sgeo. 15:20:07 Newspeak 15:20:10 There we go 15:20:50 -!- BeholdMyGlory has joined. 15:21:13 I can't figure out any examples of actual things that I'd like that'd have a clear naming theme right now, it's just the idea I like. 15:21:48 Well, Chicken Scheme extensions are called "eggs", and I think it has some other related terms in use. 15:22:18 -!- pikhq has quit (Ping timeout: 240 seconds). 15:24:57 -!- pikhq has joined. 15:26:41 Right, the object system (one of them) was called COOPS. 15:29:31 One of them? 15:29:35 There's several? 15:37:55 COOPS is one of those eggs 15:40:35 There are approximately 7 different object systems in the egg repository. 15:41:29 http://wiki.call-cc.org/chicken-projects/egg-index-4.html#oop 15:42:15 Are they all incompatible? 15:42:19 * Sgeo guesses so 15:42:22 That sucks 15:42:26 what? 15:44:26 They're made by different people for different purposes, I don't see why (or even how, except kludgily) they should be compatible. 15:44:48 "Procedures can have no more than 4096 arguments." --Mozart/Oz limitation 15:44:51 * Sgeo is not worried 15:47:36 heh 15:47:43 "Procedures can have no more than 4096 arguments." --Mozart/Oz limitation 15:47:50 "Procedures can have no more than 1 arguments." --Haskell limitation 15:49:07 lol 15:49:20 * j-invariant plays some minecraft 15:49:49 "Look, this isn't an argument." --Monty Python 15:50:19 I love that one 15:55:05 * Sgeo mildly deja vus 15:58:04 -!- Phantom_Hoover has joined. 15:58:04 -!- Phantom_Hoover has quit (Changing host). 15:58:04 -!- Phantom_Hoover has joined. 16:06:04 HAPPY 31 DAY 16:06:18 WAT 16:06:27 wat wat 16:06:33 it's 11111 16:06:42 O DAT 16:06:48 YA DAT 16:08:37 I hate it when people do that. 16:09:01 wat wat in the butt 16:13:45 Act like interpreting the date in binary means something. 16:14:35 Phantom_Hoover, its just for fun - get over it 16:14:41 its like pi day 16:15:20 "It's just for fun" can't be used as an all-purpose justification. 16:15:24 It's still stupid. 16:16:18 justified with empty words, the party gets better and better 16:17:08 Now, 11/11/11 11:11:11 and a ninth of a second will be the time for partying. 16:17:18 * hagb4rd went away alone, with nothing left but faith 16:17:53 Regrettably, it's 11 seconds after the Remembrance Day two-minute silence starts, so partying may be frowned upon. 16:32:33 -!- cal153 has quit (Ping timeout: 260 seconds). 16:32:37 -!- Behold has joined. 16:32:40 Phantom_Hoover, yeah the only reason to party is when you get a power of two in unix time ;) 16:33:00 RealPlayer still exists? 16:36:30 -!- BeholdMyGlory has quit (Ping timeout: 276 seconds). 16:46:08 -!- Behold has changed nick to BeholdMyGlory. 16:54:45 -!- elliott has joined. 16:54:49 hi ais523 17:03:23 -!- cal153 has joined. 17:06:36 18:30:43 j-invariant: it says "adjunction" posted that 17:06:40 copumpkin: I think j-invariant is adjunction 17:08:16 variable: excuse me, I believe your information to be inaccurate 17:08:19 variable: Java uses timsort 17:08:31 -!- asiekierka has joined. 17:08:36 hey 17:08:37 It operates by finding runs in the data. Descending runs are reversed. Then, the size of the run is checked against the minimum run size for that particular array size. The minimum run size depends on the size of the array. For an array of fewer than 64 elements, the minimum run size is the entire array, making timsort essentially a fancy insertion sort in that case. For larger arrays, a number between 32 and 64 is chosen so that the 17:08:37 size of the array divided by the minimum run size is equal to, or slightly smaller than, a power of two. The final algorithm for it simply takes the most significant six bits of the size of the array, adds one if any of the remaining bits are set, and uses that as the minimum run size. If the run is too small, insertion sort is used to increase the run until it's the minimum size. The runs are then merged together via merge sort to pr 17:08:37 oduce the final sorted array.[3] 17:08:41 variable: not quickxort-based 17:08:43 *quicksort 17:08:51 variable: well ok this is only used since Java 7 17:08:53 but still 17:09:16 19:18:10 How long until we have non-Python languages running on CPython? 17:09:20 Sgeo: um a few things do that 17:09:22 elliott: that's what I think too (I think I wrote it after that) 17:09:23 Sgeo: for instance Clue is going to 17:09:27 but still odd that he posted that 17:09:30 copumpkin: by "I think", I mean 99% sure 17:09:38 copumpkin: also, I think he was quoting it as mockery ... 17:09:45 oh okay 17:09:48 it wasn't very obviously a quote 17:09:58 except that given his other posting history, it was pretty obviously not what he thought 17:10:15 elliott, huh. Are there any languages that don't have other languages running on their... system? 17:10:33 Malbolge. 17:11:06 copumpkin: I think j-invariant was trying to see how many points it'd get :) 17:11:12 who knows 17:11:17 anyway, /me continues logreading 17:11:22 that's one thing you zany #haskellers can't do! 17:11:26 we have nice, digestible 100k logs 17:11:48 19:19:18 oerjan, Sgeo btw - I was talking about an array of ints 17:11:50 lol 17:11:52 sorting an array of ints 17:11:57 i can do that in O(n) 17:13:41 19:21:17 there should be a nonstandard set theory: \exists set S such that S^N is finite, but S is nonempty 17:13:41 19:21:28 (from nonstandard analysis, although that was probably clear) 17:13:48 oklopol: omg that would be amazing... invent that 17:19:05 21:38:28 All C#-like languages bore me 17:19:05 21:39:41 * Sgeo says that as he listens to a song he STRONGLY associates with Vala 17:19:05 how the fuck do you associate a song with Vala 17:20:02 " Phantom_Hoover, yeah the only reason to party is when you get a power of two in unix time ;)" <<< ah, all ones! 17:20:13 along the lines of "11/11/11 11:11:11 and a ninth of a second" 17:20:38 ars 17:20:51 oklopol, oh, all ones too. Which is just power of two - 1 17:21:04 elliott, by being extremely obsessed with a song and having it on loop at the same time as reading about the language 17:21:20 Sgeo: nutcase :D 17:22:45 sane cut 17:23:42 Vorpal: a power of two has more 1's than power of two - 1 17:24:17 um, no 17:24:24 xD 17:24:24 sea cont 17:24:26 *sea cunt 17:24:28 but the ones are WORTH more! 17:24:37 oklopol: so did you hear, cled is working 17:24:39 oerjan: it has infinitely many doesn't it? 17:24:39 sorta 17:24:52 what 17:24:58 1111.111111111... 17:25:03 :D 17:25:05 argh 17:25:06 oklopol: btw re first-class functions 17:25:12 that's why i explained: 'along the lines of "11/11/11 11:11:11 and a ninth of a second"' 17:25:15 oklopol: you should NOT add lambda syntax 17:25:25 but it doesn't count unless you convert it to graycode first 17:25:25 oklopol: in e.g. map, the lambda parameter must be an existing clue function :) 17:25:26 elliott: oh i was not gonna, don't worry 17:25:38 only lambada syntax 17:25:53 elliott: that was the original plan, however, how about single-example lambdas? 17:25:54 like 17:26:17 oklopol: here's how i'd do it 17:26:17 map ~ {. [] -> [] } map ~ {:. [1 2 3] -> [2 3 4] : [2 3] -> [3 4] } map ~ []; car; cdr 17:26:23 obviously can be any clue function you want 17:26:26 or like xxx ~ function 1; function 2; helper object; { . 1 -> 2. 3 -> 6 }; 17:26:39 oklopol: hmm i don't see why you'd need that? 17:26:45 clue is good at inferring functions, after all 17:27:36 just a random idea, what you said is pretty much exactly what i was thinking 17:27:48 What's with more of the < >? 17:27:49 elliott, I timsort is an interesting sort - but I don't believe Java uses it - at least not in the current implementation 17:27:55 Sgeo: because names can have spaces 17:28:09 Timsort is a hybrid sorting algorithm derived from merge sort and insertion sort, designed to perform well on many kinds of real-world data. It was invented by Tim Peters in 2002 for use in the Python programming language, and has been Python's standard sorting algorithm since version 2.3. It is now also used to sort arrays in Java SE 7,[1] and on the Android platform.[2] 17:28:11 variable: ^ 17:28:15 as of Java 7 17:28:17 so you probably want a separator that's not whitespace 17:28:29 but because whitespace is the separator, the only non-ugly way is to enclose the function name 17:28:32 oklopol: <> is nice because it used to have another meaning, so it breaks backwards compat! 17:28:38 oklopol: {} and [] are kinda taken, and () is ugly 17:28:40 which is why I picked <>s 17:28:44 What was the other meaning? 17:28:57 ugh 17:28:58 don't ask 17:28:58 :D 17:29:05 Too late 17:29:13 "just this thing having to do with the hardest thing to explain about clue" 17:29:20 not very hard really 17:29:25 i just can't manage to do it succinctly 17:29:37 -!- Behold has joined. 17:29:56 all functions are switch statement + expression with possibly recursion; <> was used to give a function used in the switch statement 17:30:05 now, that's inferred completely, as well 17:30:05 yeah and you always used 17:30:08 bcuz it was made of retard 17:30:11 (technical term) 17:30:31 -!- BeholdMyGlory has quit (Read error: Operation timed out). 17:32:01 elliott 17:32:24 j-invariant 17:32:34 http://en.wikipedia.org/wiki/Axiom_%28computer_algebra_system%29 17:32:41 verily 17:33:10 yes? :P 17:33:11 lol ~ {. {. <{. 6 -> 7} ~ succ> 3 -> 5 } 4 -> 8 } 17:33:24 wait 17:33:25 oklopol: xD i... how should i say this... no :P 17:33:30 and you missed a <> 17:33:32 and a hint list 17:33:35 hmm, i suppose you need explicit apply 17:33:42 oklopol: but um yeah why compromise purity like that ... 17:33:42 http://en.wikipedia.org/wiki/Axiom_%28computer_algebra_system%29 ← what about it? 17:33:44 because not having it would be retarded 17:33:47 oklopol: it's not like adding another function is much work 17:33:52 Phantom_Hoover: i was talking about it w/ j-invariant yesterday 17:33:56 oklopol: also, "explicit apply"? 17:34:00 you mean like, apply being a function? 17:34:03 yes 17:34:06 you need that in the bag 17:34:21 oklopol: why not cons(#0(car(#1)) @(cdr(#1))) 17:34:31 sort of thing 17:34:32 elliott, did the conversation consist of " It sucks. I agree."? 17:34:33 without apply 17:34:38 Phantom_Hoover: no, i think it's cool 17:34:46 and i think it might be what j-invariant was inventing mostly 17:34:48 elliott: because objects shouldn't have operations attached to them 17:34:51 functions are no exception 17:34:51 -!- doraemon has joined. 17:35:00 i mean 17:35:03 oklopol: surely, then, you should have to include apply in every list 17:35:12 to call all the other functions in the bag 17:35:13 -!- doraemon has changed nick to Guest32802. 17:35:25 (done by using apply in an infinite regress, naturally) 17:35:35 elliott: that is true, but see in the grand scheme of things, apply would be good, since in clue 2.0, "function tools" would be included by default 17:35:44 just like list tools would be if you were using alist 17:35:46 *a list 17:35:46 oklopol: fair enough then. 17:35:58 oklopol: i hope clue 2 doesn't break cled too horribly. 17:36:06 Hi everyone, I have a question regarding a bf converter. I'd like to write a converter that converts a given string to bf, with one small catch: I 17:36:16 I would like it to optimize the output as much as possible 17:36:23 elliott: and while apply would be in all your millions of higher-order functions, it's still possible you sometimes don't want to be able to apply 17:36:25 i.e. the shortest string of bf that it can produce 17:36:30 -!- Guest32802 has changed nick to doraemon___. 17:36:41 you might say just want to compose! wait... 17:36:45 doraemon___: It is not generally possible to prove that a string is the shortest possible. 17:36:53 doraemon___: that is provably impossible to do 17:36:56 with a general algorithm 17:36:57 Gregor: well yeah, but I mean 17:36:57 SORRY :) 17:37:08 I'd like to produce a short, optimized string 17:37:14 sure but you can't do the _shortest_ 17:37:16 Not necessarily the shortest possible :) 17:37:22 but that's what you said :P 17:37:23 Yes, I know... 17:37:24 elliott: could've been an answer to me as well D: 17:37:27 !bf_txtgen Hello, doraemon___! 17:37:28 " doraemon___: that is provably impossible to do" 17:37:35 163 +++++++++++++++[>+++++>+++++++>+++++++>+++<<<<-]>---.>----.>+++..+++.>-.------------.<<-.>.+++.-----------------.<+.++++++++.++.-.>--...>+.-----------------------. [164] 17:37:52 That's decent 17:37:53 txtgen is not a very good example, it's all yucky and non-deterministic 17:38:04 but i think all the best generators are like private projects that havent been released 17:38:05 *haven't 17:38:05 Well it's better than the dumb way 17:38:10 i've heard people doing them in here 17:38:13 doraemon___: it uses a genetic algorithm 17:38:15 of 17:38:17 some kind :D 17:38:20 oklopol lynches me now 17:38:24 it's prolly just hill-climbing 17:38:24 Yeah I was thinking about doing that 17:38:27 Using a GA 17:38:27 isn't ther ea very good way 17:38:32 To find short possibilities 17:38:34 gzip 17:38:43 yeah it's some sort of hill-climbing 17:38:53 for very small inputs direct: for larger inputs ASCII: for HUGE inputs gzip 17:38:56 i read it once, but don't really remember, it definitely wasn't genetic tho 17:39:07 My friend was using a method of predicting all the possibilities within a range, like 1...n 17:39:12 But it isn't a very good way 17:39:15 doraemon___: bf_txtgen was was written by calamari. See http://codu.org/projects/egobot/hg/index.cgi/file/tip/multibot_cmds/interps/bf_txtgen 17:39:20 It was only 16 chars shorter than my brute force method 17:39:21 use genetic algorithms to evolve a bf text generator >:D 17:39:22 SO META 17:39:29 Oh thanks Gregor :) 17:39:48 Nothing EgoBot does is secret :P 17:39:55 (And most of it isn't mine either) 17:40:06 So that's probably one of the best methods in your opinion? 17:40:20 It's the best one you can get your hands on right now. 17:40:21 Probably not :P 17:40:21 yeah Gregor can't really do anything right so he gets other people to write his code and takes all the credit 17:40:23 But yeah. 17:40:24 I have no doubt that there are better ones. 17:40:27 oklopol: Pretty much. 17:40:30 and sometimes write 1000 page books about this 17:40:32 oklopol: he tried to do that with me and cunionfs 17:40:34 all hype 17:40:35 oklopol: It's worked pretty well so far. 17:40:39 i suspect it's because he's a jew (<-- NOTE THIS IS NOT SERIOUS) 17:40:49 I conjecture that it's possible to find the optimal brainfuck program for all strings of length below 256 17:41:09 j-invariant: It is in fact /possible/ to find the optimal brainfuck program for any given string, it's just extremely expensive. 17:41:19 j-invariant: hey we're actually inching towards a place where I can yell halting problem legitiamtely 17:41:22 *legitimately 17:41:23 Gregor: not really 17:41:28 Gregor: well, with human ingenuity, yes 17:41:36 elliott: ? not really 17:41:38 j-invariant: did you know the busy beaver function hasn't been solved for was it 5 or 6 states and binary? 17:41:41 for tm's 17:41:43 elliott: Brute-force try every BF program from shortest to longest until you find one that prints the program. QED. 17:41:44 oklopol: yeah 17:41:45 but not dumb-mechanically, because that program that runs for 100 years might then print out the right string 17:41:47 Gregor: dude... 17:41:53 Gregor: what about ones that don't halt 17:42:00 elliott: prove they don't halt 17:42:01 Gregor: that works, if you have infinite time to run them all concurrently 17:42:05 j-invariant: right, so with human ingenuity 17:42:07 j-invariant: okay, just that yours seemed kind of astronomical compared to that 17:42:13 elliott: or an automated prover 17:42:15 Gregor's is stupid though :P 17:42:28 j-invariant: that could work. maybe. for 64 char strings, sure, not 256. i'd wager. 17:42:46 oklopol: I don't see a direct connection with busy beaver? 17:42:48 elliott: I think you need an Oracle to solve the halting problem :p 17:43:01 " j-invariant: It is in fact /possible/ to find the optimal brainfuck program for any given string, it's just extremely expensive." <<< there's not even a semialgorithm for this 17:43:18 !bf_txtgen Hello, world! 17:43:21 126 ++++++++++[>+++++++>++++++++++>++++>+<<<<-]>++.>+.+++++++..+++.>++++.------------.<++++++++.--------.+++.------.--------.>+.>. [958] 17:43:47 doraemon___: damn you larry ellison 17:44:39 doraemon? 17:45:06 Yes? 17:45:11 j-invariant: there's none, but i doubt there's an essential difference in the hardness of the problem, 256 needs a pretty long bf program, and i doubt you can say *anything* about certain bf programs of really short length 17:45:20 Do I know you, Sgeo? 17:45:34 oklopol: which ones? 17:45:43 Have you ever played a game.. it was a web-based game 17:45:47 j-invariant: the ones that happen to be hard 17:45:57 hm 17:45:59 I've played web-based games... sure 17:46:01 Which one, Sgeo? 17:46:04 gee i can't imagine the name Doraemon being popular 17:46:04 With battles, etc. Someone with your name (I think) was building a superweapon 17:46:08 I don't remember the name 17:46:09 -!- asiekierka has quit (Ping timeout: 272 seconds). 17:46:11 CAN'T IMAGINE 17:46:15 the shortest difficult brainfuck program I can think of is collatz 17:46:17 Hm, I'm not sure Sgeo 17:46:20 Spacefed I think? 17:46:25 Might have been a different me ;p 17:46:46 no that doesn't work 17:46:54 Space Fed Galactic Conquest 17:47:07 Hm, yeah I don't think that was me 17:47:08 * Gregor reappears. 17:47:16 Ah, darn 17:47:16 j-invariant: erm, you can implement any tm in bf with a constant size increment can't you? 17:47:20 erm 17:47:22 Sorry, Sgeo :( 17:47:47 What's the shortest brainfuck program that we don't know whether it terminates or not? 17:47:47 lawl 17:47:55 j-invariant: ,[.,] 17:47:58 ^ DEEP PHILOSOPHY SHIET 17:47:58 say keep state in n first bits in every second bit 17:48:01 that doesn't use inputs 17:48:05 DARN 17:48:11 and move that around 17:48:11 collatz i would guess 17:48:13 or some TM 17:48:20 erm what, how small is this collatz? 17:48:26 http://www.hevanet.com/cristofd/brainfuck/collatz.b 17:48:26 but 17:48:29 should make an automated prover for halting of brainfuck, then use that to kill of boring candidates 17:48:30 it takes decimals on input 17:48:32 remove the output 17:48:32 It would have been in 2003 17:48:35 * Sgeo shrugs 17:48:36 and have it just iterate through every natural 17:48:42 so 17:48:45 that should be fairly short 17:48:48 probably shorter than what's there even 17:49:17 Sgeo: funny how 2003 seems like such a long time ago now... 17:49:40 isn't that collatz only long because of parsing input 17:49:42 i mean 17:49:53 shouldn't be more than a few characters, division isn't very hard 17:50:53 but anyway, i find it unlikely that the shortest program your halting prover gets stuck in makes any sense at all, it's just a program with a random characters that happens to not have trivial behavior. 17:51:41 *-a 17:52:10 bf might certainly be especially slow at hitting something like that 17:52:39 yeah if you made it just iterate, not print, and not take input, that collatz could be tiny 17:53:05 i'll make an arbitrary conjecture: bf programs are easy to prove up up to size 38 17:53:19 place your bets now 17:53:25 Define "easy" 17:53:27 ask definitions later 17:53:30 -!- hagb4rd has quit (Read error: Connection reset by peer). 17:53:41 oklopol: how do you define SIZE 17:53:43 damn, was too slow 17:53:47 how do you define TO 17:53:54 How do you define "38"? 17:54:00 How do you define "I'll"? 17:54:03 oklopol: so can we have N-input, N-output functions 17:54:05 Gregor: the obvious way, if there's a dispute, i'm right, you're wrong 17:54:06 oklopol: specifically, 0-input ones 17:54:07 and 0-output ones 17:54:15 and i get the moneys 17:54:34 elliott: what, in these bf programs? 17:54:40 no 17:54:43 in klew 17:54:56 oh i totally didn't see that coming 17:55:20 http://www.youtube.com/watch?v=-CGIii_eTOk <<< why exactly did i have this retarded shit in my browser? 17:55:38 elliott: i don't like how 0 io looks like, syntactically 17:55:44 otherwise i'd have no potato with them 17:55:51 oklopol: sure, but it makes cled so less ugly... 17:55:54 holes are like 17:55:56 the biggest bug ever 17:56:02 maybe they are allowed in the language, but you can't actually write any? 17:56:05 you can have the ast in an invalid state, and all it does is sit there looking slightly ugly 17:56:08 oklopol: xD 17:56:17 oklopol: well let's put it this way 17:56:23 oklopol: you're going to add N+1-output functions right? 17:56:24 well 17:56:29 do you know who thinks 0 isn't a natural? 17:56:30 that's right 17:56:31 stupid people 17:56:34 and do you know what set you'd be using 17:56:36 N\{0} 17:56:37 parameters 17:56:38 now 17:56:39 what is that oklopol 17:56:41 that is 17:56:43 HIDEOUS 17:56:45 you, if you do that, are hideous 17:56:47 don't be hideous 17:56:49 N-io 17:56:53 maybe i am hideous, you haven't seen me 17:56:59 yes i have 17:57:01 you were on the map thing 17:57:07 ...oh right 17:57:10 xD 17:57:31 well i was pretty sexy in that pic so i guess i have nothing more to say 17:57:41 what you have to say is 17:57:44 OK DUDE N-INPUT-OUTPUT BITCH 17:57:57 no syntax for them must ever exist. 17:58:06 oklopol: um you're adding syntax for N-output 17:58:08 surely 17:58:16 oklopol: c'moooon :( 17:58:26 yeah, just whitespace separate the outputs 17:58:30 yes 17:58:36 lol ~ {. -> } 17:58:41 yeah that's ugly 17:58:41 oklopol: it's for the greater good dude 17:58:43 but hmm 17:58:44 yes it is 17:58:44 which is why 17:58:46 you should never write it 17:58:50 but you could also write clue code like this 17:58:57 MAYBE A SEPARATE SYNTAX FOR WRITING ZERO ARG FUNCTIONS 17:59:01 this_Is_A_Name~{: . hello->[1 2 17:59:04 :D 17:59:05 3]} this_Is_A_Name 17:59:08 ~ x;y; z 17:59:10 that is hideous 17:59:12 but you don't do that 17:59:17 because you're a good clueist 17:59:24 -!- cheater99 has joined. 17:59:27 same reason you wouldn't do "lol ~ {. -> }", not only is it useless 17:59:29 but it's fucking ugly too 17:59:47 oklopol: alternatively: remove N-inputs and just have every function take one input 17:59:48 :D 18:00:20 okay have your fucking party, i don't actually give a shit about whether {. -> } is legal 18:00:33 also..... 18:00:46 {. -> 1} will be totally useful with hardcore functions 18:00:50 by which i mean higher-order 18:00:52 wtfbbq is going on here :P 18:00:57 oklopol: i have the perfect way to write it 18:01:02 oklopol: {.-> 1} 18:01:05 yeah 18:01:08 oklopol: .-> is the lambda arrow's retarded cousin 18:01:12 :D 18:01:16 Gregor: clue 18:01:21 get one 18:01:25 -!- cheater- has quit (Ping timeout: 240 seconds). 18:01:29 DO NOT WANT 18:01:35 oklopol: anyway actually implementing that will have to wait for you to add n-outputs, so :P 18:01:36 for now i'll just 18:01:38 eliminate holes 18:01:44 and force you to replace, not delete 18:01:46 the last two elems 18:01:47 mmmm n outputs 18:01:48 why didn't i think of that 18:01:50 OH RIGHT 18:01:54 because inserting a branch is like liquid pain 18:01:56 * oklopol touches with red thing in mouth 18:02:15 Your uvula? 18:02:30 no you pervert 18:02:52 MEN DON'T UVULATE 18:03:03 :D 18:04:16 for some reason i know that word in english, but i remember i didn't know it in finnish until a friend of mine whose dad is a dentist told me 18:04:23 it's like the most useless thing ever 18:04:36 http://theorymine.co.uk/ haha what 18:05:30 elliott: so embarassing 18:05:52 -!- oerjan has quit (Quit: Drøvel drøvel drøvel). 18:05:59 i would certainly like to know what they look like 18:06:05 what's the best automated termination checker for brainfuck? 18:06:24 don't know. 18:06:26 what is this thing what 18:06:27 why does this exist 18:06:29 j-invariant: there is none :P 18:06:37 it's often trivial to prove 18:06:40 probaly just running the damn thing for 100000 iterations 18:06:51 e.g. [ on an even number with balanced > and < means it loops forever 18:07:04 well. with no nested loops 18:07:10 wait that isn't true 18:07:12 i forget the rule :D 18:07:44 yeah [-] is a counterexample 18:08:07 there's a rule 18:08:09 look at esotope for it :P 18:08:16 actually an automated termination checker for bf would be fun 18:08:41 well there are many obvious things you can do, like look at which cells it actually changed, and wait for loop 18:08:56 if you just code all the obvious rules that would be a good start 18:09:09 there's an O(1) way for certain loops 18:09:11 then you can inspect the programs it doesn't get, and learn more sophistcated rules from them 18:09:14 that can tell you it doesn't halt 18:09:21 based on extended euclidean algorithm 18:09:22 very simple 18:09:24 this is assuming 8-bit cells 18:09:33 it could easily be modified to spit out a certificate to prove it 18:09:35 if it does not halt 18:09:53 j-invariant: nice idea, but usually the first one you inspect will be completely out of your reach 18:10:08 oklopol: I doubt that, why do you say that? Think it will be a collatz type thing? 18:10:16 my experience is mostly based on trying to find the smallest aperiodic set of wang tiles in the summer 18:10:17 oklopol: if so, then that's my goal! I want to find that program 18:10:37 oklopol: wow cool how did that go? 18:10:40 we ran computer simulations, and when a tile set didn't work, we looked at it manually 18:10:41 "This really captured my imagination and I'm delighted to buy TheoryMine's first Theorem. What an inventive use of Scotland's expertise in artificial intelligence to create such a novel and fun product". — TheoryMine testimonials. 18:10:49 I AM NOT SCOTTISH SHE DOES NOT REPRESENT ME 18:10:56 and you could never say anything about them, after hours, you just ended up running the computer program for longer... 18:10:58 * Sgeo decides that The Onion Audio news suck 18:11:04 Anne Glover, Chief Scientific Officer for Scotland 18:11:05 It's the only sucky Onion thing 18:11:06 AAAAAAAAAAAAAAAAAAAAAAAAAa 18:11:24 Sgeo: the onion is good for the headlines. 18:11:25 -!- sebbu has joined. 18:11:25 Clearly she is personally responsible for the suckishness of the computing curriculum. 18:11:27 the articles are superfluous. 18:11:30 oklopol: to my knowledge, every set of wang tiles except one is based on substitution 18:11:36 lol wang 18:11:36 ahem 18:11:41 well, there was one that had something the program didn't catch: there was a way to convert it into a smaller one that would've had to be aperiodic as well 18:11:42 and the one that's not is based on irrational numbers 18:11:43 j-invariant: proposed first step in the halting checker: see if esotope produces a simple infinite loop for it 18:11:48 j-invariant: it has a bunch of checks for that, i believe 18:11:49 j-invariant: yeah, that smallest one is not based on substitution 18:11:49 so they all "come from somewhere" 18:11:52 for instanec 18:11:52 j-invariant: proposed first step in the halting checker: see if esotope 18:11:53 erm 18:11:55 233 elif len(result) == 1 and result[0][0] == result[0][1]: 18:11:56 234 if result[0][0] is None: 18:11:58 235 return Always() 18:12:00 *instance 18:12:02 from its condition code 18:12:04 and that's made by my employer 18:12:04 can't find the extended euclidean thing 18:12:12 which is why i was doing that in the sumemr 18:12:14 *summer 18:12:21 I wish that they had example theorems somewhere. 18:12:34 aha 18:12:38 Phantom_Hoover: they do 18:12:43 j-invariant: http://hg.mearie.org/esotope/bfc/file/5bdae1176f46/bfc/opt/simpleloop.py 18:12:51 (actually that's not completely true, since his colleaque changed a small detail to get one less tile, but that is a less interesting story) 18:12:58 90 # let w be the overflow value, which is 256 for char etc. 18:12:58 91 # then there are three cases in the following code: 18:12:59 92 # i = 0; for (j = 0; i != x; ++j) i += m; 18:13:00 93 # 18:13:02 94 # 1. if m = 0, it loops forever. 18:13:04 95 # 2. otherwise, the condition j * m = x (mod w) must hold. 18:13:06 96 # let u * m + v * w = gcd(m,w), and 18:13:07 elliott, where... 18:13:08 97 # 1) if x is not a multiple of gcd(m,w), it loops forever. 18:13:10 98 # 2) otherwise it terminates and j = u * (x / gcd(m,w)). 18:13:12 99 # 18:13:14 100 # we can calculate u and gcd(m,w) in the compile time, but 18:13:16 101 # x is not (yet). so we shall add simple check for now. 18:13:18 j-invariant: ^ 18:13:28 Oh, right. 18:13:42 Phantom_Hoover: also http://dream.inf.ed.ac.uk/events/automatheo-2010/papers/automatheo2010_submission_1.pdf 18:14:04 j-invariant: how is it that all these systems that seem to do better than coq get overlooked, btw? 18:14:08 j-invariant: HOL and Isabelle and stuff 18:14:14 j-invariant: yeah, the ones that people have been able to prove things about come from somewhere; that's exactly my point, when they don't come from somewhere, you're screwed 18:14:32 j-invariant: I can understand Mizar, which has a very comprehensive development, being overlooked for being proprietary and non-constructive; and Automath too for similar reasons and also being old 18:14:35 but the others? 18:14:54 for wang tiles, it seems possible that the best solution actually makes sense, since we're at 13, and 9 has been proven not to contain aperiodics afair 18:16:02 elliott: oh that was for balanced unnested? 18:16:12 well obviously that's trivial, since you just have to look at the evolution of the current cell 18:16:13 oklopol: i dunno :D 18:16:13 lol 18:16:15 but yeah 18:16:29 LOL i say 18:16:38 lo your own ol 18:16:50 -!- Zuu has quit (Read error: Connection reset by peer). 18:17:24 should prolly go to sleep 18:17:46 last week i had 28 hour days, this week they seem to be more like 20 18:17:47 elliott: help me write a brainfuck termination checker? 18:18:12 j-invariant: sure ... as long as it's not TOO hard 18:18:18 j-invariant: what proof language should the certificates be in? 18:18:27 :D 18:18:40 elliott: I always have in mind the version where all the cells can contain infinitely large integers 18:18:55 j-invariant: i dislike that version intensely 18:18:59 either that or binary, everything else is retarded 18:19:01 j-invariant: that collatz uses 8-bit cells anyway 18:19:06 so why not :P 18:19:15 j-invariant: most programs are written for 8-bit cells anyway 18:19:15 also 18:19:16 it's just the 8bit thing is so bloody confusing 18:19:19 why 18:19:22 except holding up to 37, and wrapping to 19 18:19:24 I can never get my head around that wrap around stuff 18:19:29 oklopol: xD like deadfish 18:19:30 if we have arbitrary integers, 18:19:33 then the tape must be only two long 18:19:36 that is my proclamation 18:19:43 eh 18:19:50 j-invariant: the nice thing about 8-bit integers 18:19:52 I am fine with 8 bit numbers 18:19:54 lets go with that 18:19:57 integers? 18:19:58 j-invariant: is that they make the work a bit easier 18:20:01 so they can be negative.. 18:20:03 because the tape sort of segments them out 18:20:03 ? 18:20:03 er no 18:20:09 what 18:20:10 8-bit non-negative integers 18:20:11 0 to 255 18:20:12 okay good 18:20:13 make the work easier?!? 18:20:16 oklopol: sort of :D 18:20:18 when writing a termination checker 18:20:21 hey afaict they make everything harder 18:20:23 that's just plain not true! 18:20:32 oklopol: you can't do that fancy euclidean stuff with arbitraries! 18:20:34 :D 18:20:38 -!- Zuu has joined. 18:20:38 everything gets really hairy, a mathematician would never have wrap 256 18:21:07 well a boolfuck termination checker is a lot more boring 18:21:10 elliott: umm, for infinites, that algo doesn't even need modular arithmetic 18:21:15 because there's less existing programs to poke it at 18:21:23 oklopol: hmmmmmmm 18:21:24 but 18:21:26 but things assume 8-bit 18:21:29 but 18:21:40 that is, you don't even *need* that fancy euclidean stuff 18:21:58 hmm 18:22:00 infinite things are usually much simpler than finite ones 18:22:00 but but oklopol 18:22:04 how can i feed mandelbrot.b do it 18:22:05 *to it 18:22:09 do whom? 18:22:27 good point 18:22:41 you won't be able to prove anything about the halting of mandelbrot.b anyway 18:23:01 oklopol: how do YOU know 18:23:03 maybe me and j-invariant 18:23:03 are 18:23:03 the 18:23:05 BEST 18:23:07 coders 18:23:24 i've heard j-invariant sucks at coding 18:23:37 from him, like, umm, yesterday? 18:23:46 and if he doesn't know, who will 18:23:50 i certainly won't. 18:23:51 but i do. 18:24:01 and you 18:24:02 oh 18:24:07 don't even get me started about you 18:24:07 what 18:24:11 i am 18:24:13 the BEST 18:24:26 you maybe the best, but i ask you: best at *what*? 18:24:45 oklopol: code 18:24:57 oh yeah i forgot what we were talking about 18:25:10 :D 18:26:58 so um oklopol 18:27:04 use cled for writing like 18:27:05 everything 18:27:06 okay? 18:27:18 does it play well with latex 18:27:21 18:22 < oklopol> you won't be able to prove anything about the halting of mandelbrot.b anyway 18:27:26 why not? Isn't that one pretty simple? 18:27:31 oklopol: it always uses a condom, why do you ask 18:27:39 j-invariant: i think you're a little too enthusiastic about the powers of automated proving 18:28:02 j-invariant: i don't even remember the algorithm 18:28:04 what was it? 18:28:05 elliott: isn't it basically for(int i = 0; i < 100; i++) { do stuff } 18:28:16 j-invariant: well maybe 18:28:27 then it's very possible you will be able to prove stuff about that 18:28:29 j-invariant: I think we should use esotope's code partly 18:28:32 j-invariant: it has this intermediate format 18:28:39 sure 18:28:47 does a lot of constant folding, adds arithmetic expressions 18:28:47 for loops 18:28:52 even detects some infinite loops 18:28:57 that would be a lot easier to prove on i feel 18:33:29 j-invariant: so um... what certificate lang 18:34:00 elliott: it can be anything. You choose 18:34:06 I would use Coq but that's just because I have it installed 18:34:07 j-invariant: i don't know :D 18:34:16 j-invariant: auto-generating Coq sounds a bit painful? 18:34:26 j-invariant: I think generating lambda expressions is probably the "easiest" thing 18:34:29 rather than automating tactics 18:35:05 j-invariant: so i really don't know :) 18:35:30 probably just program the whole thing in Ltac 18:35:46 nah that would be really slow 18:35:50 it does need efficiecy 18:36:00 j-invariant: yeah naw 18:36:10 j-invariant: I was thinking it'd be a Haskell program 18:36:19 j-invariant: of course we _could_ just not generate any certificates, but that's much less fun 18:36:34 elliott: yes certificate is important 18:36:36 or you could think about that when your program is ready up to that point 18:36:40 elliott: otherwise there may be a bug in the program 18:36:48 oklopol: um it's actually relevant from the start 18:36:52 -!- MigoMipo_ has joined. 18:36:54 oklopol: it has to use certificates from the very first line 18:36:56 it's not 18:37:00 yes, it is 18:37:02 not 18:37:05 because the certificates must be generated as part of the process 18:37:06 oklopol works without a safety net 18:37:08 rather than after the fact 18:37:28 why? 18:37:29 anyone here using FF 4.x ? 18:37:36 (and adblockplus) 18:37:43 oklopol: because that's how these things work? 18:37:49 otherwise it's duplicated work 18:40:04 maybe sure the actual program will have to write certificates from the start, but i don't see why you'd need to know what proof language you'll be using from the start when writing the halting checker 18:40:08 -!- MigoMipo has quit (Ping timeout: 240 seconds). 18:42:20 oklopol: because with certificate stuff, every single bit of reasoning involves a certificate 18:42:23 you can't just say 18:42:28 if foo then doesn't halt else dunno 18:42:30 you have to say 18:42:46 if foo then (doesn't halt, proof that it doesn't halt in this specific case using general theorem involving "foo") else dunno 18:53:39 i'm going to have to make my emacs font smaller 18:53:43 so what you're saying is the finding of the proofs is not actually harder compared to the proving 18:53:45 i mean 18:54:03 oklopol: the point is that you can't really do just one. 18:54:05 geh, whatever 18:54:13 but yes, doing certificates _is_ actually pretty hard 18:55:08 * Sgeo headaches 18:55:12 well given that j-invariant complains about how hard it is to prove trivial things about every second day, it's hard not to believe that 18:55:13 Maybe I should eat breakfast 18:55:25 all i'm saying is you don't have to do the search for the proof in a safe way+ 18:55:28 *-+ 18:55:32 oklopol: what do you mean 18:55:47 oklopol: also, yes, proving trivial things is hard in Coq etc. 18:55:54 no it's not hard proving trivial things is it? 18:56:00 well 18:56:03 oklopol has a very lax definition of trivial. 18:56:05 I thought I was complaining abuot not having support for certain features 18:56:08 hard to say without knowing what kind of stuff you're going to do 18:56:26 i don't think modelling category theory in type theory is 18:56:27 "trivial" 18:56:49 j-invariant: well maybe you've once complained about something and it sounded like you were complaining about something that was trivial, but actually you meant there was no nice way to do it or something 18:56:55 i was just being colorful 18:57:05 and yeah, i have a very lax definition of trivial 18:57:53 say existence of infinitely many primes is trivial 18:58:09 j-invariant: why doesn't emacs always have two copies of every buffer 18:58:11 displaye 18:58:11 d 18:58:12 well maybe i would say that's simple 18:58:14 not trivial 19:00:11 j-invariant: have you ever used teco, i think everyone should use teco 19:00:13 for 19:00:14 everything 19:00:17 including editing clue 19:00:19 who needs cled 19:00:59 it's possible that in the case of bf programs, there isn't really much of a search stage 19:01:54 but hard to say without knowing what specific things you're going to prove the halting of 19:02:49 I've heard o fit :P 19:02:53 -!- sebbu2 has joined. 19:03:17 j-invariant: it's great, because instead of using a program to program 19:03:20 j-invariant: you program to program 19:03:26 every editor operation is a little mini program :) 19:03:32 now you have two problems! 19:04:49 lol 19:05:04 -!- elliott has quit (Remote host closed the connection). 19:05:31 -!- elliott has joined. 19:05:54 -!- sebbu has quit (Ping timeout: 265 seconds). 19:07:21 oklopol: writing cled is so hard why do you do this to me 19:13:35 is for science 19:13:57 -!- BMG has joined. 19:14:34 -!- BMG has quit (Changing host). 19:14:34 -!- BMG has joined. 19:14:39 -!- BMG has changed nick to BeholdMyGlory. 19:17:01 -!- Behold has quit (Ping timeout: 246 seconds). 19:19:22 j-invariant: write a program whose only function is to output a proof that it works correctly 19:19:27 i.e., only ever outputs correct proofs 19:21:23 elliott: the more sophisticated an automatical thoerem prover for brainfuck termination is, the further away turings liar program is 19:21:43 e.g. a really simple termination checker could be reimplemented in brainfuck and lied to in maybe, 3000 symbols. 19:21:52 But a very advanced one would take 10000 symbols 19:21:59 j-invariant: i want to see that program :D 19:22:02 that i mentioned 19:22:06 /described 19:22:56 i don't get it. What does it do? 19:23:26 it would be an implementation fo the termination checker looking at this program AND a quine 19:23:46 and you fit the quine into the termination checker and do the opposite of what it says 19:24:28 j-invariant: that's not necessarily true, since the formal proof system could be implemented in 5000 symbols, making all your further efforts pointless 19:24:30 It is a simple matter to make a stronger termination checker which can detect the termination of this pathological program 19:24:42 oklopol: I don't understand 19:24:58 -!- sebbu2 has changed nick to sebbu. 19:24:59 oklopol: oh you mean godel instead of turing: Okay, I get it 19:25:30 j-invariant: yeah it's a simple matter, as long as you don't expect to find a proof in the same formal system 19:26:07 this is only termination certificates though -- the actual termination checker is written in a turing machine 19:26:21 elliott: hey we should just cut the crap and write the termination checker in brainfuck 19:26:34 j-invariant: oh yeah that sounds like a barrel of fun laughs 19:26:40 elliott: none of this python etc. 19:26:43 but i have an even better idea to do first 19:26:45 let's hang ourselves 19:26:48 or wait wait wait 19:26:48 lol 19:26:51 go bathe in a vat of acid 19:26:54 LOL 19:26:55 omg how can i decide 19:26:58 ;_; 19:27:12 maybe have all my skin removed slowly before my internal organs are devoured by an angry goat, and then my skeleton is set on fire 19:27:37 j-invariant: re i don't get it 19:27:42 j-invariant: a program X, with only one function 19:27:53 j-invariant: when X is invoked, it returns a proof certificate P 19:28:03 j-invariant: this P is a proof of the statement that X works correctly 19:28:14 j-invariant: example definition of "works correctly": 19:28:19 forall P in Ps, P 19:28:27 where Ps is the set of proofs that X outputs 19:28:29 except *IsCorrect P 19:28:31 LOL 19:28:32 you get what i mean 19:28:36 * Sgeo wonders how easy or difficult it is to make a self-hosting language 19:28:50 "I am correct" 19:28:52 so basically, it outputs a proof P that proves that every proof X outputs (of which there is only one, P) is correct 19:28:53 yep :D 19:29:00 I guess part of it really does require making a compiler, doesn't it? 19:29:09 Sgeo: kinda. 19:29:10 Sgeo: or just an interpreter 19:29:11 not really 19:29:14 you could run it all on top of python 19:29:18 like you run it all on top of x86 19:30:23 Sgeo: it's a good feeling though when you delete the original 19:30:24 But.. that's not that interesting, is it? 19:30:33 j-invariant, right, that's what I want 19:30:40 Sgeo: you should do it!!! 19:30:45 Sgeo: it's a good feeling when you delete the x86 19:30:50 after creating a processor for your language 19:30:52 and then delete physics 19:30:58 ddelete the universe :D 19:31:00 after making sure your language is hosted independently of physics 19:31:08 basically the idea is to replace everything with your language 19:31:09 EVERYTHING 19:31:10 no dependencies 19:31:10 EVER 19:31:11 the qustiion is "How low can you go" 19:31:15 language limbo 19:31:17 -!- calamari has joined. 19:31:23 ^^ GUYS GENIUS PUN? 19:31:27 I loled 19:32:12 j-invariant: deleting the original though, i would never do that 19:32:15 what if i lose my interpreter binary 19:32:30 or i find a fatal bug 19:32:36 that means all compilers have a contagious bug 19:32:38 accidental trusting trust :D 19:33:00 What did the original for gcc use? 19:33:09 umm, they just used other C compilers. 19:33:17 that's the advantage of doing it for a mostly portable language :P 19:33:20 type the assembly by hand 19:33:21 *with a 19:33:28 then type the source code 19:33:35 and check that compilation gives you back the compiler 19:33:35 j-invariant: *machine code 19:33:37 with a butterfly 19:33:42 that's what to do if no programming languages exist 19:34:06 j-invariant: assembly is a language 19:34:32 http://www.reddit.com/r/Minecraft/comments/ezzh4/why_not/c1canyy?context=1 THIS IS THE BEST WORST IDEA EVER 19:34:46 lol @ the recipe below that 19:34:49 Does compiling to LLVM make sense? 19:35:13 http://www.reddit.com/r/Minecraft/comments/ezzh4/why_not/c1cbsrt <-- haha 19:35:14 only if you're a LOSER 19:35:16 writing x86 assembly is easier 19:35:17 tbh 19:35:17 you can put these in it 19:35:31 ?? 19:35:40 Sgeo: ? 19:35:41 j-invariant: 19:35:43 j-invariant: i think that 19:35:49 j-invariant: one obsidian in the topright 19:35:52 elliott, are you serious? 19:35:56 j-invariant: tnt to the right of that 19:35:56 x86 is easier? 19:35:59 j-invariant: diamond to the right of that 19:36:00 Sgeo: yes 19:36:03 x86 asm is trivial 19:36:10 Wait 19:36:10 llvm asm is pretty complex :P 19:36:14 j-invariant: then below that 19:36:21 Compilers compile into asm? Wouldn't machine code make more sense? 19:36:21 j-invariant: a golden apple on the left 19:36:24 ... 19:36:29 Sgeo: sure, gcc outputs gnu assembly syntax 19:36:35 Sgeo: machine code is just as easy, though :P 19:36:40 if you define the instructions as names in your program 19:36:42 and registers too 19:36:45 that's like a ghetto assembler 19:37:39 If I compile to x86, then certain things will be platform-dependent 19:37:44 Erm, OS-dependent 19:37:54 Sgeo: doesn't matter. 19:38:03 syscalls are easier than anything else anyway. 19:38:07 you could just compile to C. 19:38:16 Sgeo: llvm assembly is quite platform specific anyway 19:38:18 in a lot of cases 19:38:40 elliott, you won't be able to try my super-cool language that is poorly designed and only exists to prove to myself that I can write a self-hosting language. 19:38:47 why no 19:38:48 t 19:38:55 ? 19:39:04 elliott, I'm on Windows, and not particularly likely to switch to Linux to do this 19:39:07 LOL 19:39:08 LOL 19:39:09 LOL 19:39:09 LOL 19:39:14 i don't even know if windows has syscalls 19:39:18 continuation-based backtracking! \o/ 19:39:18 | 19:39:18 |\ 19:39:19 and if they do calling them will probably be a bitch 19:39:20 well 19:39:23 you could use dos-style interrupts 19:39:26 but those are a bitch to use 19:39:29 also, all the assemblers suck 19:39:35 lol lol lol @ the idea of doing this on windows 19:40:31 Windows has syscalls but you rarely ever see them; you just call library functions instead. 19:40:45 don't they have that fucked up calling convention 19:40:46 lool 19:41:37 It's stdcall, which is a bit strange; callee cleans up the stack. 19:42:02 "nice" 19:42:12 fizzie: wait, so C functions re-push their arguments? 19:42:17 to get popped right after? 19:42:19 augur: that's so yesterday 19:42:20 that's the most brilliantly stupid thing ... ever 19:42:28 oklopol: yes but NOT FOR ME 19:42:32 i GET it 19:42:36 i grok it man 19:42:39 its intuitive 19:42:44 didn't you get it yesterday? 19:43:06 well, i thought i did 19:43:09 augur: it's also inefficient 19:43:09 but i just wrote some code 19:43:14 and figured it out 19:43:16 elliott: I don't know what that means. In foo(a,b,c) the caller does push c; push b; push a; call foo; and foo itself takes care of popping the arguments. (Unlike cdecl where the caller would adjust the stack back.) 19:43:17 elliott: oh sure, thats not the point 19:43:19 oh okay 19:43:26 the point is to understand what people have thought of 19:43:31 then it's not yesterday, then it's today 19:43:42 elliott: you know who else is inefficient? 19:43:44 fizzie: that seems actually saner for some things 19:43:47 oklopol: my butt? 19:43:50 :| 19:43:52 OH LOOK AT THAT 19:43:52 SUBVERSION 19:44:00 elliott butt x3 19:44:03 oh shit you won 19:44:06 -!- variable has quit (Read error: Connection reset by peer). 19:44:08 augur: lolpedo 19:44:14 darn wait it's ephebo now 19:44:15 It looks a bit neater; though it then breaks worse than cdecl if the caller and callee disagree about the number of arguments. 19:44:16 less catchy :( 19:44:24 And I think vararg functions are more messy somehow. 19:44:28 fizzie: Right. 19:44:35 elliott: you werent prepubescent when you were 13 either 19:44:40 but thats not the point 19:44:42 augur: HOW DO YOU KNOW 19:44:47 question: I have some coal and I want to make glass.... 19:44:56 well im guessing you're not weird 19:44:57 but should I use it to make glass or use it to find more coal? 19:45:02 liking 15yo is not really a philia 19:45:04 -!- variable has joined. 19:45:12 -!- rom9com1 has joined. 19:45:17 for oklopol, its reality! 19:45:21 :D 19:45:22 * augur licks oklopol 19:45:39 j-invariant: well 19:45:42 j-invariant: how much coal do you have 19:45:42 -!- rom9com has quit (Ping timeout: 246 seconds). 19:45:51 elliott: not sure, ilike 30 bits 19:45:53 j-invariant: i mean obviously you need to keep a lot for torches and shit 19:45:59 haha keep shity 19:46:16 j-invariant: well, 1 coal can make 8 glass out of 8 sand 19:46:27 j-invariant: but you need torches to explore, and coal is useful besides 19:46:38 j-invariant: getting e.g. 64 coal should not take long at all -- are you mining properly? 19:47:14 j-invariant: coal is very easy to find, just keep a couple boxes full of it to make sure you don't accidentally run out 19:47:26 elliott: probably not X) 19:47:36 j-invariant: how are you mining 19:47:39 oklopol: how much is a box full? 19:47:47 many, many stacks of 64. but only oklopol does that. 19:47:47 elliott: several different ways, to find out what works well 19:47:51 you accumulate tons of it naturally usually 19:48:00 The most coal I ever found was just by exploring, and noticing it on the sides of hills 19:48:07 j-invariant: use the wiki, really :) 19:48:13 j-invariant: http://www.minecraftwiki.net/wiki/Tutorials/Mining_Techniques lists all the viable mining techniques 19:48:19 j-invariant: apart from that -- you do spelunk right? 19:48:29 whats that 19:48:38 j-invariant: going into caves 19:48:40 btw I also started a quarry because I wanted obsidian 19:48:40 and cavern systems 19:48:43 and lighting them 19:48:43 but that doesn't work great 19:48:44 and mining ore there 19:48:50 quarry howso 19:48:58 My coal-box only has 7*64. :/ 19:48:59 j-invariant, if you want obsidian, find some lava 19:49:25 j-invariant: really, don't be ashamed of reading the wiki, it's not fun to be all "oh how can i get coal" :) 19:49:37 and since the game has no real objective... if it's not fun, just look it up 19:50:19 I have lots of coal 19:50:37 I was just wondering if I should use it to set up somet mine or just create glass now 19:53:18 ell? :)) 19:55:13 elliott: I should build a spiral staircase that goes right down to lava 19:55:20 j-invariant, check the wiki. Reading the wiki is fun. 19:55:42 j-invariant, a straight one works fine? Though there aren't lava lakes everywhere. They are lava lakes after all 19:55:46 i doubt i have a full box of coal even on my local 19:55:49 prolly close 19:55:59 (with emphasis on lake) 19:56:06 j-invariant: i've built a staircase that goes down to bedrock zomg :P 19:56:10 of course, i use it about once every 5 steps 19:56:57 elliott, movecraft is fun btw. Sad it doesn't handle redstone, chests or doors yet 19:57:46 on esoserver you can just mine straight down because you can't die :( 19:57:47 http://www.minecraftwiki.net/wiki/Tutorials/Quarry <-- dunno if this is a troll article or not 19:57:50 or rotating the boat/shift/aircraft/whatever for turning 19:58:12 WHERE'S THE MINECRAFT IN THAT? 19:58:20 oklopol, ? 19:58:22 to me? 19:58:24 or to j-invariant? 19:58:47 to neither, continuation to what i said earlier 19:59:17 ah 19:59:41 j-invariant, well if you are mining for cobble (which probably only happens when you are doing megascale structures) they a quarry can work well 19:59:51 if you want ores then they are useless 20:00:36 do hostile mobs spawn in trees? 20:00:59 j-invariant: the Cube is basically a gigantic quarry 20:01:00 or, well, will be 20:01:08 elliott: I have a treehouse and a zombie sometiems spawns next to the tree ontop 20:01:19 yeah my treehouse is open air :D 20:01:20 maybe a bad idae 20:01:22 idea 20:01:28 j-invariant, do they spawn on leaves or on logs only? 20:01:35 well it's the ground 20:01:43 I have a layer of mud ontop of my house to grow trees on 20:02:40 if a creeper spawns in the fucking tree i will die 20:02:44 j-invariant: mud? you mean dirt? :P 20:02:59 yes 20:03:05 elliott, add some glass walls? 20:03:12 elliott, or light up the tree? 20:03:19 Vorpal: um this is first night 20:03:22 elliott, ah 20:03:23 the tree is lit, kinda 20:03:25 i can light it more 20:03:37 elliott, well that is an easy way to protect yourself! 20:04:07 there, all lit up 20:04:23 [[In Beta, lava is less reactive with horizontal water flows. It also has a chance of forming redstone ore when water runs on top of it [citation needed]. Lava pools without a source will degrade to dirt after a given time period.]] 20:04:42 lol, skeleton in the trees >_< 20:04:46 don't shoot me 20:04:48 (another tree) 20:04:48 also once movecraft gets fixed I think a yacht might be a cool living place. But at the moment that is not viable. 20:05:00 oh god spider noise 20:05:01 is it just me 20:05:06 or do the monsters always seem to be closer 20:05:07 than they are 20:05:08 by the sounds 20:05:10 [[In Beta, lava is less reactive with horizontal water flows. It also has a chance of forming redstone ore when water runs on top of it [citation needed]. Lava pools without a source will degrade to dirt after a given time period.]] <-- that sounds made up 20:05:14 elliott: How do I lift water up? 20:05:18 j-invariant: bucket 20:05:22 e.g. to make an aquaduckt 20:05:26 elliott, the dirt think I'm pretty sure is wrong for example 20:05:31 no other way ;9 20:05:32 :( 20:05:36 j-invariant: just make bukkits 20:05:38 only requires a few iron 20:05:44 EIdon't have iron ingots 20:05:47 3 iron for a bucket 20:05:51 "When you stay in Lava for about 1-2 seconds, your character makes noises which appear to go along to "When the Saints Go Marching In."" 20:05:52 what xD 20:05:55 j-invariant, well can't be done without a bucket 20:06:02 iw onder if that's intentional 20:06:02 elliott, dude that is a troll 20:06:03 *i wonder 20:06:06 Vorpal: i don't care 20:06:08 i don't want it to be 20:06:08 also 20:06:11 your definition of troll sucks 20:06:12 joke != troll 20:06:27 elliott, well a joke should be funny. That is just pathetic 20:06:33 no, it's amusing 20:06:36 oh god why do the spiders sound so fucking close 20:06:37 are they close 20:06:43 elliott, you have no sense of humour 20:07:02 i thought he had too much of it 20:07:16 like a sixth sense of humor 20:07:19 oklopol, well maybe he has an anti-sense of humor 20:07:26 erm 20:07:38 bbl 20:07:45 do you copy words from other people too? i was just about to correct humor to humour because you used that 20:07:52 but then 20:08:00 you go and spoil it by now having used both 20:08:28 wtf pig 20:08:32 how did you get on top of that tree 20:08:32 i just totally instantiated my own oklopol 20:08:56 lol 20:09:01 but no one knows 20:09:06 he's in my CLOSURE. 20:09:19 i KNEW you were gay 20:09:28 wat 20:09:33 :D 20:09:42 maybe cheater99 is augur 20:09:45 this theory is backed by EVIDENCE 20:09:46 what sort of gay hating is that now 20:09:55 i'm only useful for 7 things, and 6 of them i can do on this channel. 20:10:08 the seventh is knitting 20:10:10 is not 20:10:19 is it not? what is the seventh then 20:10:40 elliott: not being here 20:10:45 he's good for that. 20:10:47 he can do that 20:10:50 it's called af 20:10:50 k 20:10:59 I'm useful for, um 20:11:12 yea but he can't do that on the channel 20:11:21 obviously by definition. 20:11:38 [[4.) Continue the process of mining a layer, and then another, until you hit bedrock. This may take a few days of vigorous playing to accomplish, but your earnings will make it well worth it. Most quarries yield an average of 150 stacks of coal, 50 stacks of iron ore, 20 stacks of gold ore, 5 stacks of obsidian, and a maximum of 1 stack of diamond gems, though these results vary with the width, depth and location of your quarry.[cita 20:11:38 tion needed] (see discussion section)]] 20:11:39 hmmhmm 20:11:39 4 bits of coal produce 2 glass blocks??? 20:11:46 j-invariant: dude... 20:11:54 j-invariant: 1 bit of coal = 8 output; 1 bit of sand = 1 output 20:12:01 ?? 20:12:04 j-invariant: N sand -> N glass, requiring ceil(N/8) coal 20:12:04 http://www.minecraftwiki.net/wiki/File:Smeltingmenu.png 20:12:12 j-invariant: that is in progress 20:12:16 as you can plainly see by the arrow 20:12:18 and the fires 20:12:23 it takes time to smelt 20:13:11 Why would you use coal to smelt? 20:13:26 Wood works and is renewable 20:13:34 really?? 20:13:57 Note: Just because what I said is true, doesn't make it a good idea. 20:15:14 j-invariant: Sgeo is being stuepid, coal is far more efficient & practical to use for smelting. 20:15:26 j-invariant: See http://www.minecraftwiki.net/wiki/Furnace#Fuel_efficiency. 20:15:57 Until the day you have to go on tremendously long minecart rides to get coal 20:15:58 ofc if you have some lava... :D 20:16:02 Sgeo: what 20:16:03 lava can smelt? 20:16:05 getting coal is easy 20:16:09 j-invariant: a bucket of it, yes, it also destroys the bucket 20:16:11 j-invariant: hideously impractical 20:16:14 nobody does it 20:19:52 Wood works and is renewable ← only Vorpal cares about this, and he couldn't be bothered. 20:19:59 Phantom_Hoover: http://www.minecraftforum.net/viewtopic.php?f=35&t=20891 20:20:04 Oh, has the Sustainable project been canceled, Vorpal? 20:20:07 *cancelled 20:20:25 I presume so. 20:20:26 Phantom_Hoover: tl;dr guy wipes cave sounds due to being a pussy. 20:20:27 elliott, no more cancelled than most of your code project s:P 20:20:30 projects * 20:20:31 YOU TOO COULD FOLLOW IN HIS FOOTSTEPS 20:20:33 Presume why? 20:20:41 Perhaps I should warp out to (4000,4000) and check. 20:20:43 elliott, but it is suspended 20:20:53 elliott, simply because lava is no longer renewable 20:21:02 there is no renewable light source any more 20:21:08 sure, burning log 20:21:17 Is that where it was going to be? 20:21:18 but what about making it burn in the first place? 20:21:31 it was near 4000,4000 20:21:34 not at it 20:21:40 I don't know exact coords 20:21:46 just how to walk from 4000,4000 to get there 20:21:48 -!- calamari has quit (Quit: Leaving). 20:22:00 Someone tell me in which series Red Dwarf ceases to be worth watching. 20:22:50 Phantom_Hoover: The eighth series is meant to be a bit naff. 20:25:14 getting coal is easy <-- well, sgeo is right. some day you will exhaust all coal in the area near your base. This will however take a very long time. Probably months of mining in that area non-stop. 20:25:40 in practise I doubt it will be a problem unless you keep a word for that long time 20:25:44 and I doubt that about you 20:27:27 i've just finished 50x50x3 hall under the sea 20:27:37 -!- Cocytus has joined. 20:27:59 elliott, those cave sounds are nice. They remind me of a cross between myst and nwn somehow. 20:28:36 -!- Cocytus has left (?). 20:28:57 Phantom_Hoover: HOW GOES GRAVITY.LISP. 20:29:03 nooga: That's less than 128x128x128. 20:29:13 nooga: Wait, x3? As in, only 3 tall? 20:29:14 elliott, it doesn't go at all. 20:29:18 Phantom_Hoover: PAH 20:29:27 3 metres tall is plenty! 20:29:32 :P 20:29:39 nooga: Sgeo: Buy the damn game and do drudge work on the Cube. 20:30:05 If we have enough drudge workers, we can just mine it out by hand! 20:30:07 Sgeo: http://cobolforgcc.sourceforge.net/ 20:30:18 nooga, glass? 20:30:28 nooga, if not, it isn't awesome enough for the roof 20:30:46 Phantom_Hoover: Say a miner can reach the bottom of any square of map in 100 seconds. 20:30:53 Phantom_Hoover: Say you have 10 people on the job. 20:31:08 Phantom_Hoover: There are 16,384 such squares to do. 20:31:10 What is the cube? 20:31:32 Vorpal: deep under the sea 20:31:40 j-invariant, elliott's slightly Freudian construction project. 20:31:41 around level 16 20:31:41 elliott, isn't that 45 hours per person? 20:31:43 Phantom_Hoover: tl;dr 45 and a half straight hours. 20:31:46 elliott, try again 20:31:57 elliott, what about 128 workers? 20:32:01 j-invariant: A 128 wide, 128 high, 128 deep cube in the ocean, made out of glass, lit by lava. 20:32:05 Phantom_Hoover: What's Freudian about it. 20:32:09 nooga, so not at the sea bottom? 20:32:14 no 20:32:16 elliott, COMPENSATING FOR SOMETHING? 20:32:21 nooga, not awesome enough :P 20:32:26 My genitalia are not cuboid. 20:32:31 nooga, everyone dug under the sea in terrains 20:32:48 Phantom_Hoover: But yeah, even with 10 people working on it constantly and several breakings of the laws of physics, it would take 45 hours to mine out the Cube. 20:32:52 What I'm saying is: TNT kit. 20:32:54 i hate minecraft 20:32:59 nooga: then why did you make it 20:33:15 my during the hours that took me to dig it 20:33:24 elliott, OK, but you're clearly compensating for the fact that you're 4 feet tall IRL. 20:33:28 my gf got really mad at me 20:33:38 and i didn't earn a penny 20:33:43 because coding is so boring 20:33:47 Phantom_Hoover: That is true. 20:34:12 j-invariant: MORE AWE AT THE CUBE PLZ 20:34:15 nooga, everyone dug under the sea in terrains ← terrains? 20:34:32 There should be underground biomes. 20:34:35 Phantom_Hoover, err, good questions 20:34:42 question* 20:34:59 elliott, there is that thing which fiddles with the terrain gen's internal parameters 20:34:59 Phantom_Hoover, I think I'm a bit pluralish today 20:35:14 (SSP only, though.) 20:35:18 Phantom_Hoover: BiomeTerrain or whatever? 20:35:24 No idea. 20:35:26 Phantom_Hoover: I've wanted to try that for a while now. It looks way better than Notch's generator. 20:35:35 Vorpal, everyone dug under the sea in terrain? 20:35:39 Phantom_Hoover: Generates much larger, smoother biomes and the like. Lots of tweakable parameters. 20:35:46 Phantom_Hoover, well it is /slightly/ better 20:35:55 Phantom_Hoover: That photo I linked of a highlands scene (saying it was a good argument for Better Grass) was made with it. 20:35:59 Phantom_Hoover, if you define terrain to "solid blocks" then it makes sense :P 20:36:08 elliott, I don't remember that. 20:36:16 It was literally days ago. 20:36:29 elliott, link to that photo? I don't remember seeing that photo 20:37:24 "I'm the sort of person who's done the Red Cross First Aid course twice and so I knew what to do and was almost immediately compressing his chest to the rhythm of the Bee Gees' Staying Alive with the phone operator counting along with me. No, I'm not being funny. The rhythm of that song is ideal for CPR." 20:37:33 Sgeo: Never perform CPR unless you do that. 20:38:08 elliott: sounds amazing 20:38:08 [[Alternatively, it's the same BMP as Queen's "Another One Bites the Dust" and Pink Floyd's "Another Brick in the Wall Part II".]] 20:38:20 j-invariant: yeah, we've cleared, like, 10 lines of sea :P 20:38:23 like moses, except really slow 20:38:26 10?? 20:38:29 Vorpal: You said it looked too flat, IIRC. 20:38:29 j-invariant: and excavation is... slow 20:38:30 j-invariant: yes, 10 20:38:32 I've done more than 10 20:38:34 j-invariant: as in, 10 lines of 126 long 20:38:40 j-invariant: about 10 deep each 20:38:51 j-invariant: i doubt you have 20:39:05 j-invariant: that's about 10*10*126 = 12600 blocks placed 20:39:08 to clear 20:39:13 very roughly 20:39:55 -!- Zuu has quit (*.net *.split). 20:39:59 -!- Vorpal has quit (*.net *.split). 20:40:06 -!- lifthrasiir has quit (*.net *.split). 20:40:08 -!- sftp has quit (*.net *.split). 20:40:08 -!- HackEgo has quit (*.net *.split). 20:40:08 -!- EgoBot has quit (*.net *.split). 20:40:18 -!- Ilari_antrcomp has quit (*.net *.split). 20:40:18 -!- Ilari has quit (*.net *.split). 20:40:24 Phantom_Hoover: http://imgur.com/om0iL This is fully functional, with CraftBook. 20:40:24 Discuss superiority to Vorpal's gate. 20:40:55 Clearly superior. Also irrelevant if Vorpal doesn't have CraftBook. 20:41:45 It's on his test server and he was talking about craftbook before. 20:41:47 And how awesome it was. 20:41:50 So yes, he does. 20:42:43 -!- Zuu has joined. 20:42:43 -!- Vorpal has joined. 20:42:43 -!- lifthrasiir has joined. 20:42:43 -!- sftp has joined. 20:42:43 -!- HackEgo has joined. 20:42:43 -!- EgoBot has joined. 20:42:43 -!- Ilari_antrcomp has joined. 20:42:43 -!- Ilari has joined. 20:43:18 -!- pikhq has quit (Excess Flood). 20:43:21 Phantom_Hoover: In which Notch actually responds to feedback: http://www.reddit.com/r/Minecraft/comments/ezpw5/lots_of_new_info_including_cake/c1c7grn 20:43:22 -!- pikhq_ has joined. 20:43:43 :O 20:43:56 whe n you break a bit of glass you don't get it back :( 20:44:03 j-invariant: INDEED 20:44:07 http://www.youtube.com/watch?v=2lsFN5DgoLc This is the silliest thing. 20:44:26 (Old, apparently.) 20:45:16 http://www.youtube.com/watch?v=Zv6GVDu46ls I hypothesise that sound mods are inherently hilarious. 20:45:20 Cow cow cow cow cow. 20:49:29 http://www.reddit.com/r/Minecraft/comments/drvm8/my_experiment_with_modifying_the_minecraft_sound/c12gnct ;_; 20:52:08 LOL 21:00:12 -!- jix has quit (Ping timeout: 250 seconds). 21:01:10 gcd(F_m,F_n)=F_{gcd(m,n)} 21:01:31 cool 21:01:35 now use that to compute gcd 21:03:12 hmm 21:03:23 fibonacci numbers are weird 21:09:04 -!- jix has joined. 21:11:50 elliott, is the server down? 21:12:18 hm up now anyway 21:12:18 -!- rom9com1 has left (?). 21:12:46 ineiros, are you skyping? 21:18:08 -!- calamari has joined. 21:20:07 -!- ais523 has quit (Remote host closed the connection). 21:27:15 ineiros, what the hell are you doing? 21:35:08 He's toying with you. 21:35:15 -!- Mathnerd314 has joined. 21:46:01 Phantom_Hoover: ? 21:46:16 With Vorpal. 21:47:00 Phantom_Hoover, is that supposed to be funny? It isn't really. 21:47:48 Well, now you've made it even *less* funny. 21:48:03 Phantom_Hoover, your own fault for not making it funny to begin with 21:49:04 Phantom_Hoover, besides movecraft got updated. Now doors are supposed to work (nothing done on chests yet though) 21:49:14 Phantom_Hoover, also submarines 21:49:23 j-invariant: help me design my language :P 21:49:34 what's this?? 21:49:54 j-invariant: a language! btw have you read any more of the axiom info? 21:50:02 eyah a little 21:50:20 j-invariant: is it close to what you were thinking of? 21:50:27 no 21:50:33 j-invariant: no 21:50:33 ? 21:50:51 I can learn form it 21:51:07 j-invariant: isn't it a dependent symbolic CAS? :P i mean that's my impression of it 22:01:03 j-invariant: i'm actually curious 22:01:18 elliott: youo're right 22:01:27 j-invariant: what does your design have different to axiom? :) 22:04:38 ugh i have to rename some of my methods... 22:04:51 j-invariant: can you fork ghc and add ml-style modules please, then i would always use haskell 22:05:59 elliott: Yeah I think I would change a bit moore than that :P 22:06:23 j-invariant: Well ... ML modules lets you chuck out typeclasses :P 22:06:44 Sort of. 22:08:45 elliott: yeah, something that subsumes GADTs, Typeclasses and Modules 22:08:58 j-invariant: you mean like dependent records? :P 22:09:23 not sure 22:09:33 j-invariant: sure 22:10:00 j-invariant: dependent records do powerful ML-style modules; powerful ML-style modules do typeclasses with, like, one bit of magic; and dependent inductive types are of course basically GADTs 22:10:33 j-invariant: (the one bit of magic I think is this: a module signature can specify one of its exported values is "magical"; whenever a value of that type is needed as an implicit module parameter (a notion added just for this), that value is used) 22:10:56 j-invariant: for instance, the module implementing integers would have a magical value of type Ring Z 22:11:02 and then some function might be like 22:11:27 lolRingFunction : forall T, [Ring T] -> ... 22:11:33 where [] means "magic module param" 22:11:35 then 22:11:38 lolRingFunction (some Z) 22:11:42 would auto-specify that (Ring Z) value 22:11:46 elliott: hey what about 22:11:53 lolRingFunction : Ring T, ... 22:11:54 of course having two magical values of the same type in your current module scope is verboten 22:12:03 use typeclasses *as* quantifiers 22:12:04 j-invariant: you mean as the syntax? 22:12:08 that's a nice idea 22:12:14 would keep the verbosity down 22:12:24 j-invariant: maybe something like "the" though 22:12:28 lolRingFunction : the Ring T, ... 22:15:18 j-invariant: oh god, I have created an image that could give Douglas Hofstadter an aneurysm 22:15:42 a basilisk image? 22:15:49 yes, but Hofstadter-only 22:15:54 behold 22:15:54 http://i.imgur.com/VqcIS.png 22:15:55 RECURSION 22:15:59 i hear it blows his mind 22:16:08 too bad i'm not him 22:16:12 i like being blown 22:16:16 hehe 22:16:33 -!- hiato has quit (Ping timeout: 260 seconds). 22:16:33 agh, tk 22:16:41 obviously the egytions understood recursion 22:16:53 egytions :D 22:17:03 I'm making a pyramid in minecraft 22:17:12 it's glass on the inside but sand on the outside 22:17:14 note to self, add a separate background colour for selected vs. active... hard to remove those lists without knowing what you have selected 22:18:41 editing these nested expressions is slow :D 22:18:53 j-invariant: nice 22:19:54 i would like to see an upside-down floating sand pyramid in minecraft 22:20:08 it's not upside down :( 22:24:50 oklopol: is "foo ~ {}" valid Clue? 22:25:24 -!- hiato has joined. 22:26:14 i would like to see an upside-down floating sand pyramid in minecraft <-- possible with torches 22:26:27 quintopia, if it floats just above a torch that is 22:26:36 quintopia, why not make one yourself? 22:27:50 -!- MigoMipo_ has quit (Read error: Connection reset by peer). 22:27:54 someday 22:28:20 quintopia: sometime 22:28:35 elliott, somewhere 22:29:17 (wait, is none else going to continue this chain?) 22:29:21 (bbl) 22:37:28 oklopol: so hey, cled is ugly as fuck :D 22:40:23 j-invariant: http://i.imgur.com/CP1vV.png can you figure out what's going on here :D 22:40:26 even i have troubles 22:41:29 I don't know what [] does.. looks nice though :D 22:43:40 j-invariant: it's just a list 22:43:50 j-invariant: ([] (1) (2) (3)) there is [1 2 3] 22:44:18 j-invariant: basically, that screenshot is the really ugly representation of {. 3 [7 44 1] -> [[1] 3 [7 44]] } ... with some highlighting oddities 22:44:32 j-invariant: i think i'm starting to see why this kind of editing is unpopular 22:44:33 what is cled? some derivative of clue? 22:45:10 quintopia: cled is my semantic AST editor for clue ... it happened after i wanted to write a clue-mode for emacs 22:45:15 and it's became, well, this monstrosity 22:45:18 *become, 22:45:26 time to kill it dead? 22:45:28 453 lines of folly and counting 22:45:37 quintopia: nO 22:45:38 *NO 22:45:41 it's the platonically perfect clue editor 22:45:43 it just sucks, is all 22:45:51 but i'm gonna develop it to completion anyway :D 22:45:58 good 22:46:06 only because clue sucks and not because there's anything wrong with the editor, yes? 22:46:21 quintopia: no, clue is amazing 22:46:23 my editor sucks and ROCKS! 22:46:27 and sucks 22:47:03 ehird man speak with forked tongue. need whiskey and migraine pill for good medicine. 22:47:14 Someone tell me which books of Known Space are any good. 22:47:16 concur 22:47:43 Someone point me to a list of the reasons X sucks. Someone tell me what subset of Y is good. 22:47:45 Phantom_Hoover: * 22:47:53 All of them? 22:48:16 What about the infamous third book in the Ringworld series? 22:48:17 -!- Wamanuz has quit (Ping timeout: 240 seconds). 22:48:29 http://www.minecraftforum.net/viewtopic.php?f=25&t=132717 Nice. 22:48:30 Someone point me to a list of the reasons X sucks. Someone tell me what subset of Y is good. ← BLATANT LIES 22:48:39 Phantom_Hoover: What do you mean, "what about it"? 22:48:40 FastRender: more efficient chunk queue processing. 22:48:40 UniText: a completely rewritten text renderer. It's faster and supports Unicode, although the Unicode font files are not included with this release. 22:48:40 Fewer glClears: erasing the entire screen is expensive. This mod avoids it when possible. 22:48:42 Better chunk drawing code: Removing a few useless transforms from the chunk rendering code lets all visible chunks be drawn in a straightforward manner. 22:48:47 I like this Scaevolus guy. 22:49:09 Phantom_Hoover: INCIDENTALLY, can you buy me a new GPU? 22:49:16 I plan to configure Minecraft to be utterly insane soon. 22:49:18 pikhq_, i.e. it's infamous for being a perfect instance of quality being inversely proportional to place in the series? 22:49:59 An HD texture pack if I find one I like, far distance, fancy rendering, Better Light, that shader mod with depth of field, perhaps also with that lighting shader if I can find it and make it work together... 22:50:05 Mipmapping if it helps. 22:50:53 hah 22:50:55 Phantom_Hoover: I don't recall it being bad, though. 22:50:58 my 50x50 trap works 22:51:09 Definitely not as good as the first, mind. 22:51:31 i've get approx 24 sulfur in 15 min 22:51:59 nooga: lol noob 22:52:18 ??? 22:52:24 nooga: http://www.youtube.com/watch?v=RiJh5fpWPAo 22:52:26 I have 1 sulfer after 2 weeks playing 22:52:33 j-invariant: kill creepers 22:52:37 and build a mob trap 22:52:41 again, read the wiki :P 22:53:11 nooga: build that and then come back 22:53:15 what the hell is happening in that video! LOL 22:53:29 oh 22:53:37 the reason they die is because of falling from such a height 22:53:44 yes 22:53:48 j-invariant: watch the rest of it :) 22:53:49 ummm.... that must have taken a while to build 22:53:54 j-invariant: basically: they don't spawn on steps 22:53:58 so the ground below is safe 22:54:02 and then the huge dome catches them 22:54:04 and the only way is down 22:54:09 so they walk down and then fall inside 22:54:17 resulting in loot 22:54:20 that's crazy wtf 22:54:29 how the hell did he have the patience to build it 22:54:29 since they're spawning all the time at night, they fall down at a crazy rate :) 22:54:30 well 22:54:31 er 22:54:33 they don't walk down 22:54:35 there's water 22:54:37 obviously 22:54:39 to carry them 22:54:41 j-invariant: who knows :D 22:54:55 tl;dr mobs spawn in big water slide all night, ride uncontrollably, fall down, die, drop loot. 22:55:50 j-invariant: building mob traps is not so hard though 22:56:07 j-invariant: basically, you want an easily steppable-upon bit of water that mobs will go into, which then leads down to 22:56:08 C C 22:56:09 elliott: @ this clip... i thought that mobs don't spawn on water 22:56:11 where space is nothing 22:56:15 and the two Cs are catcuses 22:56:21 nooga: dunno... i think they do 22:56:30 nooga: but besides, there's those little sticky out bits of cobbles fro them to spawn on anyway 22:56:31 *for 22:56:35 j-invariant: this crushes the mobs 22:56:39 j-invariant: and they'll drop loot into the stream 22:56:43 j-invariant: which you then route into your base 22:56:47 elliott, FWIW, that Optimine thing has mucked up Better Light. 22:56:54 Phantom_Hoover: you apply better light afterwards 22:56:57 Phantom_Hoover: not before 22:57:04 j-invariant: so basically mobs will keep walking in, getting crushed by the cactus, and their loot will float into a pool in your base 22:57:12 j-invariant: that won't be hugely fast, but it'll be pretty good 22:58:05 j-invariant: oh and 22:58:14 j-invariant: look for natural cobblestone while mining, and also mossy cobblestone 22:58:19 j-invariant: it'll be a dungeon 22:58:22 oh ok 22:58:22 j-invariant: with a mob spawner inside 22:58:31 j-invariant: now consider: dig out the floor beneath that mob spawner 22:58:45 j-invariant: so much that they die of fall damage 22:58:47 and route a path in 22:58:49 http://www.youtube.com/watch?v=H8xs53VmFjc neat 22:58:53 j-invariant: mob spawners only spawn one type of monster 22:58:54 but.. 22:59:09 [[...these people are trying to make money from an idea that does not belong to them.]] — An Idiot on the MC boards. 22:59:21 j-invariant: e.g. if it's a spider spawner 22:59:24 j-invariant: you could get shitloads of string 23:01:02 j-invariant: that door machine is hilarious 23:01:17 j-invariant: if you tab away it sounds like venetian snares... sorta 23:08:59 haha, nice video 23:13:51 -!- Phantom_Hoover has quit (Quit: Leaving). 23:14:28 j-invariant: btw: http://www.reddit.com/r/Minecraft/comments/evwk8/does_anyone_know_how_to_make_a_very_simple_but/ 23:14:31 j-invariant: stuff about mob traps 23:15:16 -!- poiuy_qwert has quit (Quit: This computer has gone to sleep). 23:20:04 guide to minecraft: http://i.imgur.com/i1YWC.png 23:25:33 Is Notch going to remove indefinitely burning logs? 23:25:50 The probability of that is somewhere in the region of 0. 23:25:58 Why? 23:26:19 Because there's something like seventeen hundred billion fireplaces, and also, very little reason to fix it :P 23:27:36 -!- marcules has quit (Quit: -). 23:27:50 nooga: pics of your trap? 23:27:51 -!- FireFly has quit (Quit: swatted to death). 23:29:02 elliott, what are your thoughts on Clean? 23:29:32 an interesting curiosity and — mere curiosity. uniqueness typing is interesting. 23:29:37 learn haskell instead. 23:29:54 also clean has some REALLY weird bits 23:29:54 like 23:29:58 you write (a -> b) -> [a] -> [b] 23:29:58 as 23:30:01 (a -> b) [a] -> [b] 23:30:02 why??? 23:30:08 that doesn't even make any sense and takes special casing 23:30:17 elliott, are Clean functions curried? 23:30:22 yes 23:30:31 also (x:xs) is [x:xs], which, again, means that a single list with the single element (x:xs) is [[x:xs]]... which is just plain confusing and stupid 23:30:36 also infix o weird me out 23:30:40 but these are all syntactical differences. 23:32:30 Maybe uniqueness typing is what will bring me back into the purely functional world 23:32:34 yea that's stupid 23:32:37 [Or maybe I'll be bored to tears] 23:32:51 Sgeo: stop talking in trivial lists. 23:33:31 elliott: I trapped some cows in a cave but they disappeared :( 23:33:37 i kind of feel embarrassed for Sgeo on behalf of... everyone 23:33:38 j-invariant: whut 23:33:39 j-invariant: howso 23:33:41 is it not possible to make a farm? 23:33:53 I just dug this small cave into a hill and trapped the cows in there 23:34:03 j-invariant: Of course it is: http://imgur.com/a/pt8v5 23:34:05 elliott, what cheater99 said was a joke, afaict. 23:34:10 I suppose they might die in low light. 23:34:12 I think 23:34:13 Sgeo: And? 23:34:31 hahaha I need one of these 23:34:37 elliott: I wonder why they disappeared 23:34:59 j-invariant: try building a small but ~5 deep pit instead 23:35:03 and put a torch on the walls 23:35:04 get them in there and see 23:35:14 j-invariant: if you walked too far away i guess they could disappear... but you'd have to walk a few chunks 23:35:16 so probably not 23:35:18 *quite a few 23:35:21 oh :( 23:35:34 elliott: yeah I roam very far so that might not be worth doing then 23:35:38 j-invariant: lol no 23:35:40 j-invariant: i doubt it 23:35:48 j-invariant: it's like 16 chunks 23:35:54 so like 23:35:57 walking 256 away maybe 23:36:01 i guess it's easy but 23:36:11 j-invariant: i think i'm wrong 23:36:54 "Mobs spawn no closer than 24 blocks and disappear if they are more than 4 chunks away from the player." 23:36:55 j-elliott: why not just play farmville? 23:37:00 j-invariant: ok if you walked far away. 23:37:07 cheater99: because minecraft is more than farming? :P 23:37:12 j-invariant: build a mob trap :D 23:37:44 im going to sleep ;) 23:37:46 yes, use minecraft to make mafiaville or whatever they call it 23:37:54 gangstaville? 23:38:04 I finished building a pyramid though 23:38:09 j-invariant: how big? 23:38:24 it's only like 6 high 23:38:52 j-invariant: really? that shouldn't have took that long to build... unless it has like a flat top and is really wide 23:38:57 screenshot? 23:39:10 no it's just a tiny pyramid 23:39:12 you should now recreate von dniken's mythology around it 23:39:27 j-invariant: how long did it take to build? 23:39:43 elliott: dunno I did other stuff in between 23:39:51 hehe 23:40:04 is there like 23:40:08 automation for minecraft? 23:40:30 cheater99: interesting 23:40:34 cheater99: there's redstone. 23:40:47 bluestone would let you build a hideously complex autominer but it doesn't exist and never will >:) 23:41:08 minecraft just sounds real fucking boring to me in that you have to sit around clicking stuff 23:41:28 it's like killing wild pigs in a forrest in wow 23:41:28 -!- hiato has quit (Read error: Operation timed out). 23:41:44 1 experience point per click or something equally dumb 23:41:51 cheater99: umm what 23:41:53 (not that i ever played wow, but you know what i mean) 23:41:55 you don't kill pigs generally 23:41:56 oh 23:42:08 well er no because in MC most of the time is spent doing shit you want 23:42:10 elliott: yeah, but that's what it feels like 23:42:11 i.e. building shit 23:42:14 no it doesn't 23:42:17 you've clearly never played 23:42:21 yeah 23:42:28 but i've seen many vids now 23:42:36 % of people who haven't played minecraft and think it's probably lame: 99 23:42:44 % of people who have played minecraft and think it's lame: much less 23:42:53 nobody cares, honestly. 23:43:06 generally in the family of minecraft-likes you'd expect a scripted way of doing things in accelerated time, or at least without user interaction 23:43:14 do you not think everyone has already heard "OMG IT SOUNDS BORING AND LAME" 100 times before 23:43:34 i'm not trying to change your mind or anything 23:43:35 DURP DURP MY INFORMED OPINION IS THAT IT'S LAME 23:43:42 or like "tell you it's lame" 23:43:44 Gregor: OH MAN THAT'S NOVEL 23:43:52 I mean literally lame though. 23:43:56 It has a limp. 23:43:57 cheater99: in response: no, automating such things would not make the game more fun. 23:44:04 Gregor: So THAT'S what the view bobbing is. 23:44:04 i'm just expressing what my impression is and wondering why you guys think different 23:44:06 that's all 23:44:14 cheater99: 'cuz it's fun 23:44:19 ya k 23:44:24 no reason to get upset there 23:44:28 i'm not upset 23:44:41 I'M NOT UPSET OK????????? 23:44:43 :p 23:44:52 ah, right, everyone who disagrees with you is upset 23:45:00 no, i'm just joking around 23:45:28 mining can be fun enough because you find caverns and dungeons, exploring caves is fun and often screenshot-worthy, exploring terrain is fun and often leads to good locations for build projects, building structures are fun, building houses is fun, building machines with redstone is fun, fighting mobs is... uh... terrifying 23:45:32 so 23:45:33 so terrifying 23:45:41 ya i can see exploring mines is fun 23:46:02 and so can exploring terrain be 23:46:06 exploring mines? you build mines, you mean caverns :P 23:46:10 oh yes 23:46:14 or other people's mines 23:46:28 also fun is building a forest-top village 23:46:31 but like.. i'm surprised there aren't scripts for say building houses or pools 23:46:31 Did I also mention that people who play Minecraft are torps and hurpadurp? 23:46:38 that just feels so droll tbh 23:47:18 what's a torp? 23:47:22 is that like a tarp? 23:48:28 Pfff 23:48:31 Such a torp question to ask. 23:48:36 HORP TORP 23:49:14 -!- drakhan has quit (Remote host closed the connection). 23:49:28 cheater99: man why aren't there machines that automate pushing pieces of lego together 23:49:38 that just feels so droll tbh 23:50:26 there are 23:50:32 cheater99: would you use them 23:50:42 j-invariant: THAT SLEEP THING IS WORKING WELL FOR YOU HUH 23:50:46 no i would just use big pieces 23:50:54 hehe 23:51:06 cheater99: ahh, so you'd rather play MINECRAFT: FOR KIDS! 23:51:16 Roblox? 23:51:19 i'd play minecraft duplo 23:51:22 minecraft is for kids X) 23:51:28 Oh, that reminds me, I want to try Roblox >.> 23:51:28 with BIG pieces 23:51:47 designed for 1-3 years of age. 23:52:08 since, like, i love to remit like that. 23:52:27 you keep using that word etc. 23:53:55 so my superdrive STILL isn't here, what is this INSOLENCE 23:54:23 -!- j-invariant has quit (Quit: leaving). 23:55:26 you have to make sure the infidels pay with their lives 23:55:50 elliott: what word? 23:56:39 ? 23:56:44 remit 23:57:21 i do? 23:57:35 anyways, some cool tricks here: http://blog.ksplice.com/2011/01/solving-problems-with-proc/ 23:57:37 no, but i do not think it means what you think it means. 23:58:25 a remission is when you go back 23:58:28 "A UNIX process refers to its open files using integers called file descriptors. When we say "standard input", we really mean "file descriptor 0". So we can use /proc/self/fd/0 as an explicit name for standard input:" 23:58:29 lolfail 23:58:30 -!- hiato has joined. 23:58:31 /dev/fd/0 23:58:53 cheater99: that's irrelevant, the fact is that afaik nobody uses "remit" like that 23:59:01 unless you, like, got cancer at the age of 3 and still have it 23:59:05 "I'm remitting back to BEFORE" 23:59:22 "Good news! I'm in remission!" "That's great!" "Yes, I love being three years old!" 23:59:25 nope, still not working 23:59:27 yeah but there's a technique in psychology called remission 23:59:29 isn't there? 23:59:44 isn't it regression you are thinking of