00:00:08 I can compute it for 2x2 and 3x3 :P 00:00:12 and I know some of the rules 00:00:16 but that's all 00:00:16 in other dimensions that doesn't work unless you use (n-1) vectors to cross 00:00:54 fax, I can compute it for arbitrarily large matrixes 00:01:07 but I hate anything larger than 3x3 00:01:15 due to the huge amount of work in it 00:01:29 finding sub-determinants and so on (if that is the English term for it) 00:02:00 oerjan, oh hm 00:02:22 oerjan, but with n-1, how could that even work? 00:02:34 oerjan, you can only take det() on a square matrix right? 00:02:59 oerjan, which means that n-1 for 5 wouldn't really work out as far as I can see 00:04:56 -!- tombom has quit (Quit: Leaving). 00:05:25 AnMaster: you let the product of v_1, ..., v_(n-1) be the unique vector x such that det (v_1,v_2,...,v_(n-1),y = x.y for all y 00:05:36 *,y) 00:05:50 * AnMaster mentally converts that to math notation 00:06:02 oerjan, I find it *extremely* hard to read ASCIIed math notation 00:06:12 But did you know that the coefficients of the characteristic polynomial of H, where H is the Hessenberg matrix from Arnoldi iteration of matrix A and vector b, turn up (with negative sign) as the last column of pinv(K)*A*K, where K is the Krylov matrix for A, b and pinv() is the "usual" pseudoinverse? 00:06:13 mind you i'm not sure if my definition has the right handedness 00:06:22 (for 3 dimensions) 00:06:37 fizzie, what is pinv? 00:06:38 if not just switch things around a bit 00:07:01 I just said, the usual (Moore-Penrose?) pseudoinverse. 00:07:02 ascii math notation is easy you're just a whiner :) 00:07:14 oerjan, how do you define handedness for more than 3 dimensions? 00:07:18 (This was a homework bit for yesterday's Matrix Computations thing.) 00:07:45 fizzie, oh right 00:08:15 AnMaster: such that the product of e_1, e_2, ..., e_(n-1) is e_n, i presume 00:08:43 (e_i being the unit vector of the i'th axis) 00:09:29 which means my handedness above was right for 3, i think 00:10:18 mhm 00:11:59 AnMaster: btw one intuition for determinant (which ignores the sign though) is that if you take the hypercube spanned by e_1,...,e_n (i.e. the cube with all coordinates in [0,1]) and apply a matrix M to it, then the _volume_ of the resulting hyperparallelogram is abs(det M). 00:12:17 -!- augur has joined. 00:12:53 oerjan, anything involving the word "hypercube" definitely doesn't feel like related to my "intuition" 00:13:12 or equivalently, the hypercube spanned by vectors v_1,...,v_n has volume abs(det(v_1,...,v_n)). 00:13:23 AnMaster: well you can use it or 2 and 3 dimensions too 00:13:26 *for 00:13:33 okay 00:13:36 what about 1? 00:13:41 well that is a trivial case I gues 00:13:46 yeah :D 00:14:11 oerjan, so for 2x2 mat, that would be ad-bc 00:14:16 but then what are the sides? 00:14:19 s/hypercube/hyperparallelogram/, last one 00:14:21 of a rectangle? 00:14:32 oh right 00:15:12 Isn't it pretty: http://www.cis.hut.fi/htkallas/hw7.pdf (Usually my homework answers are horrible handwaving, but this one is pretty explicit. Though that does steal a pretty complicated Theorem 9.7 out of the lecturer.) 00:15:34 btw hyperparallelogram is probably not the right term, although it _is_ a parallelogram in 2 dims 00:15:47 * Sgeo wants to take math courses 00:16:25 fizzie, what language is that code? 00:16:33 AnMaster: one corner of the parallelogram is the origin. two of the others are (a,b) and (c,d), the last one is their sum 00:16:58 oerjan, yeah I realised 00:17:09 after you said "hyperparallelogram" 00:17:18 AnMaster: Matlab, and the >> is just the prompt. 00:17:24 fizzie, ah 00:17:55 AnMaster: Or Octave, in this case, but with a Matlab prompt to make the recipient feel more at home. 00:18:13 ah 00:18:14 -!- augur has quit (Ping timeout: 256 seconds). 00:18:37 AnMaster: ah, 3 dims is parallelepiped 00:19:02 oerjan, well yes 00:19:06 oerjan, didn't you know? 00:19:13 somehow i hadn't quite made that a household name, though i've certainly seen it :D 00:19:21 oerjan, I admit however I was fuzzy on the spelling 00:19:28 oerjan, but I had a math teacher mention it a lot 00:19:38 during the last few weeks 00:20:25 "Coxeter called the generalization of a parallelepiped in higher dimensions a parallelotope." 00:20:31 I've got the phrase "rhombus, the neglected parallelogram!" stuck in my head, but I can't remember where I read it from. 00:20:37 _that_ i'm not sure i've heard 00:21:06 oerjan, he also loves making a huge distinction between "geometrical vectors" and "algebraic vectors" 00:21:12 -!- MigoMipo has quit (Remote host closed the connection). 00:21:20 (not sure of translations here) 00:21:48 wikipedia seems to call the former http://en.wikipedia.org/wiki/Euclidean_vector 00:22:35 fizzie, no chance it's Triangle and Robert, is it? 00:22:44 oerjan: Couldn't you just call it "paral".("le"x($dim-1))."piped"? Then you'd always have the dimension explicitly in the name. 00:23:09 well you _could_, but that would be evil. 00:23:26 Sgeo, oh that, one of the worst strips I ever started reading and then gave up after 120 or so strips 00:23:52 fizzie, how do you pronounce it? 00:24:06 fizzie, and what programming language? 00:24:22 That was the Perl notation. 00:24:25 ah 00:24:26 fizzie: that x should be ^ in my view 00:24:41 in math 00:25:17 also you would have to allow for $dim being a variable, and/or transfinite 00:25:20 Yes, but I was worried you'd think I'd just want the number there, and not actual repetitititition of lelele. 00:25:42 oerjan, in math it is $*d*i*m isn't it? ;P 00:25:53 fizzie: not a chance to avoid that once it's generalized 00:26:08 * oerjan swats AnMaster -----### 00:26:28 -!- BeholdMyGlory has quit (Read error: Connection reset by peer). 00:26:31 AnMaster: triangle and robert is great! not that i've read much 00:26:33 but f u 00:26:51 alise, we have different tastes clearly 00:26:58 well, die 00:27:02 "well drawn" is not in your list :P 00:27:07 A Pythonist would (well, could) say "paral"+"le"*(dim-1)+"piped", I believe. 00:27:18 well, not so much in mine either 00:27:36 AnMaster, I loved it 00:27:37 fizzie, is thyat string duplication with *? 00:27:47 that* 00:28:12 Yes, it does string multiplication if you give a string and a number. 00:28:32 >>> "paral"+"le"*4+"piped" 00:28:33 'parallelelelepiped' 00:28:52 alise and I have the same tastes? o.O 00:29:19 I don't *think* it was Triangle and Robert, though; I have a feeling it was a human(oid) character in some bit of fiction. 00:29:50 Right, it was just an old Nukees strip: http://www.nukees.com/comics/19980318a.gif 00:30:09 But at least that's not well drawn either. 00:30:12 Algebraic! 00:31:00 fizzie, heh 00:31:55 On rhombuses: http://www.penny-arcade.com/comic/2009/1/9/locked-brutal-combat/ 00:32:15 -!- FireFly has quit (Quit: Leaving). 00:32:35 Deewiant: You mean "rhombi", don't you? 00:32:47 Either works. 00:32:53 "Pl. rhombuses (7-8 -us's); 8 rhombi." I guess they both do, yes. 00:33:09 But it sounds better as "rhombi", though also a bit vacuum-roboty. 00:33:16 Rhoomby. 00:33:18 I had just typed "rhombus" already and it's less keypresses to add "es" than to backspace twice and add "i". 00:33:33 Rhoomba, the rhombus-shaped Roomba. 00:33:34 use rhomboi for the original greek (i think) 00:34:15 fungot: Have you read that particular Penny-Arcade comic, by the way? 00:34:15 fizzie: so i says to her, though. 00:34:27 fungot: What does that even mean? 00:34:27 fizzie: this is fantastic. maybe after this we can subjugate some indigenous peoples. or, the devil. you are a woman raised as a man. 00:34:42 Subjugating the devil sounds dangerous business. 00:34:54 :D 00:35:05 don't make me laugh out loud atm 00:35:10 people sleeping near here 00:35:37 haha you're better off using your grandma as a math forum than #math 00:35:48 "hey wanna hear about this interesting thing i came up with?" "go fuck yourself" 00:38:13 fizzie: dammit i'm laughing because of fungot but I'm trying to look all serious 00:38:13 alise: my guess? the bullshit. there's no shame in that. well, he hasn't been playing very well. and, i was pushing them, and then i saw something. something big. 00:38:16 daaaamn youuuuuuuuu 00:38:18 ^style 00:38:18 Available: agora alice c64 ct darwin discworld europarl ff7 fisher ic irc jargon lovecraft nethack pa* speeches ss wp youtube 00:38:21 fungot: A penis? 00:38:21 alise: annarchy's mother: anne claire, eat your dinner. you know, potty issues. there. he's got these friends back at the flag named earthquake and demise, right? i bet it's something bad in there. 00:39:13 ^style oa 00:39:14 Not found. 00:39:15 ^style pa 00:39:15 Selected style: pa (around 1200 transcribed Penny Arcade comics) 00:39:17 ah 00:39:27 ^style darwin 00:39:27 Selected style: darwin (Books by Charles Darwin -- you know, that evilution guy) 00:39:30 fungot, hi there 00:39:33 AnMaster: he shows " page 111) that when naturalists confine their attention to agriculture, were fnord when a species has once disappeared it never reappeared.), and no doubt every female flower which i examined appeared more like a dandy than a warrior, but he has seen/ carcasses :) dead seals. wherever these slaty feldspathic rocks abound, greenstone seems common; at/ c. persica et turcica, mr. f. fnord six feet, in proporti 00:39:43 smilies 00:39:45 yag 00:39:50 yeah* 00:40:00 ^style europarl 00:40:00 Selected style: europarl (European Parliament speeches during approx. 1996-2006) 00:40:32 fungot, this should prevent alise from laughing if he wan'ts to avoid it 00:40:34 AnMaster: mr president, ladies and gentlemen, and by the governments of both old and new member states have long since been prepared and sent to parliament. 00:40:36 want's* 00:40:51 fungot, stop being funny! 00:40:52 AnMaster: i am happy to say that any such principle needs to be stressed that the guidelines in leader+ now need to be repeated. i have to say that i have already criticised the method used for each individual, which remains and will always be positive and enriching factor for europe. 00:41:09 night 00:41:38 i was invited in this math high school thing, but i didn't go because i had a gf 00:41:39 ... 00:42:03 cuz true love is more important than math 00:42:15 we broke up when i started high school 00:42:27 "and no doubt every female flower which i examined appeared more like a dandy than a warrior, but he has seen/ carcasses :) dead seals." --Darwin 00:49:19 what about true math? 00:49:38 the mathematics that can be proved is not the true mathematics. 00:49:44 i.e., only the negations of proved things are true. 00:49:49 well, not only 00:51:27 lol what 00:51:33 -1 * -1 = -1 00:52:04 I wish I understood cubic truth :( 00:53:02 timecube? 00:53:39 -m * -n = -(m*n) clearly 00:53:46 TIME CUBE IS BETTER THAN YOUR QUEER GOD 00:53:46 therefore -1 * 1 = 1 00:54:00 http://i.imgur.com/SQHYl.jpg . Clicking a piece toggles the piece, and pieces orthogonally adjacent. THe goal is to get all pieces to be cylinders, or all pieces to be cones. This configuration should be solvable in 3 moves. How easy/hard are those moves to figure out? I know how to solve it given a live board, but it always takes me a while 00:55:14 Also, are there any unsolvable configurations? If not, I can simplify my reset algorithm a bit. Currently, it just blanks the board and simulates 3 clicks 00:57:13 Sgeo what is this made in?? 00:57:25 "Clicking a piece toggles the piece, and pieces orthogonally adjacent" -- lights out!! this game is OLD 00:57:32 some virtual world. 00:57:37 you can tell because it's sgeo and it has health meters 00:57:38 It's in Active Worlds. The code for the puzzle itself is in C# 00:57:39 and shitty 3d 00:57:41 see! 00:57:46 it's idk equations in Z2 00:57:47 I did not add the health meters 00:58:05 you can solve every solvable puzzle in a maximum of 9 clicks :D 00:58:08 * fax proves the trivial 00:58:09 Clicking a piece doesn't toggle all pieces in a row or column 00:58:38 I originally programmed it that way, since I misremembered the original game we're um, recreating 00:59:34 why is http://mathoverflow.net/questions/18696/how-to-write-if-else-as-mathematic-equation stupid? 00:59:51 * Sgeo feels vindicated by oklopol's question. 01:01:19 it's stupide because programs are alredy formal language 01:01:28 you don't have to turn everything into 'math' 01:01:31 it already IS 01:01:37 and because he clearly has no idea how booleans work 01:01:51 he seems to think everything as to be arithmetic 01:02:39 "fax: oerjan, another thing I really want to do is make a 4D (or more D..) world that you can immerse yourself in :(" <<< been wanting to do this since like forever 01:03:13 * Sgeo takes interest 01:03:26 http://eusebeia.dyndns.org/4d/vis/vis.html 01:03:31 * fax has been searching for answers 01:03:34 oklopol: The question is like asking "how do you write if-else in a program". 01:04:20 Sorry, change that. 01:04:27 "How do you write if-else in programming" 01:05:18 How do you shot if-else 01:06:18 fax: you don't know the definition of a determinant? 01:06:39 n 01:06:40 o 01:07:06 anyway definitions are overrated 01:07:19 Sgeo: if you can prove for each piece that there is a sequence of moves to toggle _just_ that piece, then all configurations are solvable, otherwise not. 01:07:22 One could, for instance, define yourself sufficiently formal psuedocode and just write "if foo then bar else baz". Or you could do that in lambda calculus. Or you could just write it as a piecewise function. Or you could do some rather clever arithmetic to get it down to a single arithmetic statement (though I doubt that's feasible with the example there) 01:07:27 if you have two equivalent characterizations of something, which one is the 'definition'? 01:07:50 the one used in practice 01:08:11 pikhq: there is an easy way to switch on 0/1 arithmetically 01:08:11 the one that places the term in a category of differentiated terms 01:08:11 because any others can be solved by combining those sequences 01:08:13 with an else clause 01:08:18 I forget the exact definition though 01:08:27 I've figured out how to toggle just the middle piece 01:08:29 alise: Ah, right. 01:08:38 by the way I saw a really gorgeous proof using iverson notation 01:08:49 in Concrete Maths 01:08:50 No, I don't think I have 01:09:05 lol oklopol has completely lost respect for me 01:09:17 Sgeo: oh wait you said just 3 moves? then what i said is not true. in fact it cannot be. 01:09:41 Sgeo I would think of the inverse problem 01:09:50 starting from the solution, what moves take you to a given state 01:09:52 Well, if I can show that it's always solvable in X moves, that's enough 01:10:02 if it should always be <= 3 moves i mean 01:10:33 It's just that due to the way I scramble the board, there's a solution in 3 moves for any state achievable by this scrambler 01:10:51 Sgeo: as fax said, 9 moves is enough for everything that can be solved 01:11:10 9 moves should be enough for anybody 01:13:48 Wait, how is that trivial? 01:14:03 Sgeo, it doesn't prove that everything has a solution 01:14:04 oh the question was about how you'd express if-then in math? i just read "what natural set of mathematical operations on reals can be used to compile if-thens to math?" 01:14:44 But I still don't see how 9 moves is enough to solve all solvable cases 01:14:59 because if you press twice on the same place that = doing nothing 01:15:01 Sgeo: because you never need to click a piece twice (just cancels out), and the order you click them doesn't matter 01:15:06 Oh 01:15:10 fax: ahem 01:15:15 fax: you just abused = 01:15:23 no I didn't 01:15:31 :))) 01:15:33 no more than i did 01:15:35 "fax: if you have two equivalent characterizations of something, which one is the 'definition'?" <<< depends on author, in this case i'd be asking for *a* definition 01:16:06 2^9 different sets of moves you can do 01:16:10 2^9 different boards.... 01:16:22 I wonder if they are equal sets though 01:17:13 If two different move sets can take you to the same board, then the answer is no, right? 01:17:22 yes 01:17:24 "fax: lol oklopol has completely lost respect for me" <<< i was just reading logs, i only lose respect for myself for not remembering definitions, from other people i just expect the capability to learn the matters at hand at a given time 01:17:42 I just don't really care about having a definition 01:17:49 because I know the important properties of it 01:17:56 fax: ahem 01:18:00 fax: CONSTRUCTIVISM BITCH 01:19:10 !haskell (9*8*7)/6 + (9*8)/2 + 9 01:19:20 "alise: fax: you just abused =" <<< why is it abusing the definitions, it's the relation a^2 = 1 in the abelian group of move sequences 01:19:24 eh 01:19:25 damn no egobot 01:19:27 "the definitions"? 01:19:30 "=". 01:19:46 my brain isn't really here, also wow i finished the log 01:19:53 oklopol: fax always whines about me abusing = 01:19:55 Sgeo: btw your problem can be solved with determinants 01:20:06 oh well i don't know much about constructivism 01:20:17 * Sgeo has worse problems than this 01:20:23 this issue is way more subtle than me 01:20:26 I can get away with not understanding this in depth 01:20:33 There's another puzzle that I can't get away with it 01:20:38 :/ 01:21:33 Also, I don't really know what determinants are? I think something to do with matrixes and solving multiple multivariable equations? 01:21:34 hey i have a Determinant.hs file. let's see... 01:23:01 fax: if you know even a few of its basic properties, you'll probably know a definition for the determinant :P 01:24:32 oklopol: constructivism: you must actually show a value that obeys certain constraints, if you want to prove such a value exists 01:24:33 Sgeo: yes. if the determinant is nonzero then every equation with that matrix is solvable. it turns out your problem can be expressed as a matrix equation. 01:24:38 you do this by removing ~~p -> p. you probably know that 01:24:49 ~~p is pretty damn strong evidence for p though :P 01:25:07 How can it be expressed as a matrix equation? o.O 01:26:12 alise: i know that much, how does that make fax's statement incorrect? 01:26:19 Sgeo: a 9*9 matrix. item M_i,j is 1 if pushing piece i toggles piece j, 0 otherwise. 01:27:16 How can we be sure that that maps to something that determinants are sensible for? 01:27:56 because they are used when solving matrix equations 01:28:36 be patient. now make a vector v of length 9 with 0's and 1's. then M v is a vector whose i'th coordinate is odd iff pushing the pieces that are 1 in v will toggle that piece. 01:28:53 oklopol: oh i was just talking about his I don't need a definition for determinants I have the properties 01:29:10 ohh 01:29:16 of course a constructivist - he's one, being a dependent folken - would demand a definition before even talking about properties 01:29:23 (folken: singular of folk) 01:29:26 of course 01:29:27 (this is really a question about the field Z_2, but we can talk about odd and even instead) 01:29:34 it stands towards reason 01:29:39 of course to "folken" 01:29:41 ooh, geometric logic proofs! 01:30:03 Where can I read tutorials about this sort of math? 01:30:25 Sgeo: now it happens to be that you can achieve _all_ vectors as M v in this way, iff det M is odd. 01:30:40 in other words all configurations are solvable iff det M is odd. 01:31:55 on the other if it isn't, then you can do some matrix operations to get a summary of exactly what configurations you can solve. 01:32:01 What does each vector represent, exactly? 01:32:14 v is what buttons you push 01:32:30 Sgeo: the original vector v represents button pushing. 0 no, 1 yes. 01:32:41 2 maybe 01:32:51 i should do a tri-valued logic that doesn't just have 3 = unknown it's boring 01:32:52 M v represents buttons toggled. odd yes, even no. 01:33:00 M is basically a function that takes a vector and returns a vector? 01:33:07 Sgeo: yes. 01:33:42 then we have to solve M v = y for v, where M is the rules of the game, and y is the desired outcome (which things are circles on the board), and if det M is odd, then we can divide by M to get M v = y <==> v = M^-1 y, and now "M^-1 y" is just an ordinary vector, which is a solution for the game 01:33:53 * Sgeo is not used to struggling with math 01:34:29 Sgeo: incidentally if det M is odd, then we can _invert_ the matrix to get all solutions. 01:34:38 (inversion mod 2 here) 01:34:46 * oklopol is trying his best to ruin oerjan's explanation by shortcutting it 01:34:54 gah 01:34:58 well more like being faster i guess 01:35:05 If M v's exist enough such that there's an M v for each configuration, all configurations are solvable 01:35:09 speed is always my problem 01:35:30 Sgeo: yes 01:35:48 well, *If v's exist 01:36:12 How do you learn what an odd and even determinant means 01:36:26 it's not about odd/even usually, it's about nonzer/zero 01:37:03 it's just we're working in Z_2 here (the space with just two objects, odd and even), so zero = even, and the only nonzero object is "odd" 01:37:17 *nonzero 01:37:21 * Sgeo wishes he asked about a more pressing problem 01:37:28 Z_2 is also known as booleans 01:37:36 :P 01:37:37 oh 01:37:47 i would say booleans are the boolean algebra formed by those two, not the field 01:38:07 hmm i guess i see the algebra as built upon the type 01:38:08 or perhaps type inference will take care of that 01:38:09 Sgeo: determinants work in any _field_. we are really working in the field Z_2 (mod 2 arithmetic) here 01:38:18 so boolean is true | false, the algebra is all the operations 01:38:19 wtf 01:38:28 * oerjan swats oklopol, then himself -----### 01:38:33 :D 01:38:36 Wait, M is just a matrix? 01:38:39 yes 01:38:50 normal matrix, but the field is Z_2 and not real numbers like usually 01:38:51 I need a tutorial on this stuff 01:39:00 Thought it was a function 01:39:06 15:37:12 However, ((int)NULL) does not necessarily equal 0. 01:39:06 oh, so that means (int)(void*)0 doesn't have to be 0, heh 01:39:14 I was like "You're dividing by a function?" 01:39:25 Sgeo: there is a one-one correspondence between matrices and linear functions between vectors 01:39:26 well it is, see matrices are in fact a representation for "linear functions", which are these simple kind of functions 01:39:30 :D 01:39:34 yay i won! 01:39:58 clearly only one of us is needed here 01:40:01 i'm going to bed 01:40:04 How do you learn all this? Better yet, how can I learn all this? 01:40:11 edumacation! 01:40:14 well f*g is clearly function composition by symbol analogy 01:40:15 well university does wonders 01:40:21 so f/g is the reverse of function composition 01:40:31 clearly 1/f gives (g,h) where f is the composition of the two 01:40:32 i'd suggest reading books 01:40:34 and clearly 1=id 01:40:37 so id/f is (g,h) 01:40:39 work out the rest yourself 01:40:40 No online stuff? 01:41:06 Sgeo: linear algebra for the matrices in general, then number theory/higher algebra for the Z_2 part 01:41:09 -!- augur has joined. 01:41:29 (ring/field theory from the higher algebra) 01:41:47 there probably is online stuff, but online tutorials for math stuff are usually only found for trivial things 01:41:52 this might belong in that category 01:42:42 well of course you can find books online but i mean these sort of quick tutorials to X you can't really find on galois cohomologies 01:42:57 (i have no idea what those are) 01:43:53 Sgeo: also read what alise said about composition, that's exactly what matrix division is, inverting the linear function represented by the matrix. 01:44:24 i know a bit of galois theory, and a bit of cohomology, but i have no idea how they combine... 01:44:28 turns out linear functions are invertible (they have normal function inverses) iff their determinant is nonzero 01:44:43 * Sgeo doesn't even recognize what "galois" is supposed to mean 01:44:52 it's a name 01:44:54 evariste galois 01:45:02 oklopol, that makes a lot of sense somehow 01:45:25 Sgeo: yes, especially if you remember the volume definition of the determinant 01:45:37 * Sgeo still doesn't quite know what a determinant is 01:45:55 well it's just a function from matrices over a field to the field itself 01:46:01 which has a few nice properties 01:46:15 Sgeo: that volume thing i explained to AnMaster earlier today 01:46:20 in special cases like reals you have, as oerjan mentioned, interesting geometric properties too 01:46:50 * Sgeo has no clue how to even get started learning this stuff 01:47:16 i'd get a book on linear algebra and do exercises like crazy 01:47:16 what stuff?? 01:47:29 yeah linear algebra is the best thign 01:47:33 but determinants arean't..... 01:47:49 nothing wrong with determinants 01:48:00 especially in Z_2 01:48:17 where you don't have any of their less useful properties, just invertibility 01:48:35 i mean most of the time we just need to know whether the determinant is nonzero 01:48:44 I suppose none of this is related to Computer Science? Maybe I should stick with this college and Minor in math 01:48:49 in fact so often it would even make sense to have a separate name for such a function 01:48:59 or maybe that's not true, just my impression 01:49:38 all you need to know is learning things is related to knowing things is related to computer science 01:50:13 i really have to go to sleep -> 01:50:16 Good night 01:50:56 * Sgeo is going to forget about everything and play a game 01:52:29 Sgeo: i calculate the determinant to be -7, thus odd, thus everything is solvable 01:57:31 -!- coppro has quit (Ping timeout: 246 seconds). 02:03:21 ok... time to get hardcore: 02:04:03 does anyone know of implementations of (P)RNGs in brainfuck? 02:04:57 or would i be better off plugging /dev/random into stdin? 02:05:37 there's a langtons ant based thing but it gives the same result every run 02:05:39 obviously 02:05:42 there's no source of entropy in bf 02:05:52 but you can use e.g. user input to seed it multiple times 02:05:58 except for input 02:07:31 Sgeo I'm trying to prove this lights out thing by brute force 02:07:37 I don't really know how long it will take 02:08:51 There is a PRNG on the esolang wiki's algorithms page. 02:09:20 But obviously you're going to find a decent source of entropy to make it even vaguely useful. 02:09:38 (I suggest "Please pound on the keyboard") 02:10:43 bah... all my decent ideas for entropy kill the use of stdin 02:11:46 Well, yeah. There aren't any other sources of input at all. 02:11:49 random numbers in brainfuck shouldn't be hard 02:11:53 pineapple: cat your entropy source and input together? 02:11:57 oh it's been done 02:12:10 fax: Brainfuck has only one non-deterministic feature. "," 02:12:22 pikhq of course I meant pseudorandom :( 02:12:43 wow I'm already through 341 of 512 cases! 02:13:10 fax: wth you're not just doing the 9 pieces? 02:13:16 oerjan just 9 02:13:32 my algorithm doesnt take into account any symmetries 02:13:45 I'm doing a formal proof by brute force 02:13:50 ein coq 02:14:07 fax: i mean, you're not just checking if you can get each single piece toggled? 02:15:12 iim trying to prove 02:15:12 Theorem complete : forall a b c d e f g h i, moves (a::b::c::d::e::f::g::h::i::nil) win. 02:15:20 which says that for every starting board you can solve it 02:15:28 by using a finite number of moves 02:15:45 oh well 02:15:46 so I could play each board and that would prove it, but I wrote a thingy that plays it for me instead 02:15:51 it's really really stupid ;D 02:16:04 now prove it for an m*n board ;D 02:16:06 I didn't even have to show that moves are comutative or doubled up cancel out 02:16:07 or symmetries 02:17:59 oerjan: yeah... :-/ 02:18:29 fax: what are your assumptions? 02:18:34 none 02:18:52 I just axiomatized what moves are valid (all 9 of them) 02:19:01 assuming that a move flips 5 cells in a + pattern, doesn't wrap around 02:19:04 as a data type 02:19:05 and which board size? 02:19:08 3x3 02:19:12 it's taken over 10 mins :D 02:19:14 ok 02:19:27 heh 02:19:37 * fax is on case 210/512 02:19:46 if I took ONE symmetry into account it would be done now 02:19:52 heh 02:19:56 and there'sa lot more than one 02:20:12 counting symmetries, there are: 02:20:18 if I proved it using a clever method that doesn't involve search..... I wonder if I would still be doing it :P 02:20:19 3 boards with 1 cell 02:20:52 7 boards with 2 cells 02:21:11 enumerate all 3 and 4 cell positions, invert for 5-8 02:21:15 and then 0 and 9 are 1 02:21:19 and solve those 02:21:46 mm 02:21:52 I should make redo this tommorw, and record it 02:22:03 (my 7 for 2 lights are: 12 13 15 16 19 25 26) 02:22:07 then I can time the porgramming time vs the pproof checking timem for all these different approaches 02:22:45 what language are you using to check them in? 02:23:09 co 02:23:10 coq 02:23:16 ? 02:23:25 PSOX? 02:23:27 this one i need to look up? 02:24:06 ooh 02:24:16 ># 02:24:17 fax: 4*4 _isn't_ all solvable 02:24:18 oops 02:24:30 (says my determinant check) 02:24:30 im glad I'm not doing 4x4 :P 02:24:37 oerjan: are you sure? 02:24:43 wait you use determinant for this lights out thing? 02:24:48 pineapple: determinant of the matrix is 0 02:24:57 yep 02:25:09 oerjan, thought someone said it was -7? 02:25:09 fax: you didn't see all the discussion above? 02:25:19 Sgeo: that was me, and for 3*3 02:25:37 :( 02:25:40 Oh, the 0 was for 4*4 02:25:45 3*4 is -9, so also all solvable, but 4*4 is 0, so not 02:26:11 I suppose it's better to randomize than to Simulate random clicks 02:26:29 Sgeo: that would depend on how hard you want to make it... 02:26:37 by the way 02:26:50 nothing 02:28:21 wow I don't understand that idea with the matrix at all 02:28:22 oerjan: ok. yeah... googling seems to confirm what you're saying... 02:28:35 what's M? (the rules of the game, but encoded how?) 02:28:44 random unsolvable 4x4 board: .XXX/...X/.XXX/.... 02:28:55 Main> lightsout 3 3 02:28:55 [[1,1,0,1,0,0,0,0,0],[1,1,1,0,1,0,0,0,0],[0,1,1,0,0,1,0,0,0],[1,0,0,1,1,0,1,0,0],[0,1,0,1,1,1,0,1,0],[0,0,1,0,1,1,0,0,1],[0,0,0,1,0,0,1,1,0],[0,0,0,0,1,0,1,1,1],[0,0,0,0,0,1,0,1,1]] :: [[Integer]] 02:29:21 fax: that's the matrix for 3*3 02:29:41 oerjan: 2x3 should give you 0 as well 02:29:49 131/512! 02:30:15 pineapple: yeah it does. interesting that those determinants are _exactly_ 0, and not just even. 02:30:23 oerjan, oh I have a data type like this but it's not a matrix 02:30:35 oh! I see what you do, that's really neat! 02:30:43 I should program this too 02:30:44 oerjan: do you get the significance of the number if it's non-zero? 02:30:44 fax: this is just a haskell list of lists, actually. 02:30:53 or do you think there isn't one 02:30:53 oerjan well I am thinking of it as a matrix 02:31:00 i had a determinant program from way before which used lists of lists 02:31:18 my computer is really REALLY struggling with a particular lights out configuration 02:31:18 also: if you can work out the determinant of a 3x3 in your head, i have the perfect game for you 02:31:47 * Sgeo has another puzzle that needs math analysis 02:31:49 pineapple: this is actually a 9*9 _matrix_ for the 3*3 game, so no :D 02:31:50 Not today though 02:32:03 oerjan: a 3x3 matrix, not a 3x3 board 02:32:11 Sgeo: feel free to try us 02:32:22 pineapple: ouch. well _maybe_ i could do it. 02:32:32 doesn't mean i feel like it... 02:32:47 i guess i'd want to use minors 02:32:53 http://www.boardgamegeek.com/thread/402843/rules-non-degenerate-or-not-quite-kramers-rule 02:33:29 minors of 3*3 are just cross products anyhow (also discussed above) 02:33:38 minors? 02:34:22 Actually, instead of asking for math help, there's probably enough analysis stuff posted somewhere. I just need to know the name 02:34:32 Sgeo: describe it 02:34:33 minors of matrices, a tool for evaluating the determinant 02:34:47 although not very useful for big ones iirc 02:35:18 There are two containers of water, a larger one [A], and a smaller one [B]. You can fill a container completely with water, transfer water from one to the other [the transfer stops when the repicient is full or the sender is empty], and drain a container 02:35:22 oerjan: if i get what you're saying... then yes, probably only useful for 3x3 02:35:32 There's a red line on container A. the goal is to get the water level of A to match the line 02:35:34 Sgeo: and aiming for a target? 02:35:35 ok 02:35:50 i know the puzzle genus 02:36:28 pineapple: the determinant being even but non-zero doesn't have any significance for lights out, but you could maybe create a similar game based on addition with a different modulus than 2, where it would be. 02:36:31 The practical problem I have is this: If I'm given the size of A and B, can I move the line and be able to make a puzzle such that a solution exists? 02:37:51 oerjan: did you click the link i gave? 02:38:22 oerjan: reason i asked about the significance of it is that... i think that 7 presses the is the max needed for 3x3 and 9 for 3x4 02:38:46 which (and i might be very wrong here) i think means that 5x5 will give -23 02:39:44 * Sgeo pokes 02:39:52 Sgeo: thinking 02:40:27 * Sgeo appends an "and if so, how" 02:40:35 pineapple: doing now 02:40:59 Sgeo: well obviously you can put the red line in the place corresponding to the volume of B 02:41:08 Sgeo: assuming that the water supply is infinite, that A > B, that A > target, and that everything is integers? 02:41:44 * fax 52 cases left!! 02:42:17 Sgeo: the obvious are nB and A-nB 02:42:25 then look at what's left 02:42:34 pineapple: um no 3*3 can require 9 presses 02:42:57 (but don't bother with the latter half if A % B == 0) 02:43:01 oerjan: hmm... ok 02:43:52 pineapple: because all configurations can be solved, _every_ push subset of the 9 must be different. so if you push all 9, there is no way to get it back without pushing them all again. 02:44:17 I'm still not sure whether everything is integers 02:44:31 Sgeo: if you assume it, it's a lot easier 02:44:34 Actually, I don't think it's a safe assumption 02:44:36 Sgeo: golden ratio might be interesting :D 02:44:52 Let me show you a picture 02:45:44 http://i.imgur.com/3CenQ.jpg The only thing I can easily change is the red line 02:45:45 oerjan: ok... doesn't all 9 invert all 9? 02:45:50 pineapple: determinant for 5*5 is 0, actually. (so not all solvable) 02:46:00 pineapple: nope 02:46:13 oerjan: weird... 02:46:21 Sgeo: where is this? 02:46:24 it toggles a diagonal cross 02:47:06 pineapple, it's supposed to be confidential, but I don't care. I'm under no contract. 02:47:12 Active Worlds 02:47:30 Sgeo: if you're under NDA, be careful... 02:47:36 Sgeo: are the containers empty at the start? 02:47:40 oerjan, yes 02:47:59 hmm... i doubt that it's properly floats... might be large intergers, though 02:48:31 * Sgeo isn't even sure how to measure them precisely 02:48:49 Sgeo: are you willing to be unsceientific? 02:49:05 If you mean with measuring, I think I have to be 02:49:11 pineapple: it's not NDA Sgeo just likes to spend time in projects where kids pretend they're professional 02:49:25 and "fire" people and make "design plans" and really they're just making some random stuff in virtual reality without pay 02:49:32 hold a ruler up to the screen, etc 02:50:07 I think the only kid in this project is the other programmer 02:51:17 yay proof complete!!! 02:51:31 so yeah you really can get every configureation 02:52:43 http://pastie.org/878074 02:52:45 -!- jcp has joined. 02:52:49 most stupid way I could think of at the time 02:53:20 So, I move the line to A-B? 02:54:02 Sgeo: easiest way, yeah... 02:54:03 btw: 02:54:24 if all numbers are integers, there's no guarantee that it's solvable for all line positions 02:55:14 if A and B aren't coprime, then the target has to be a multiple of hcf(A,B) 02:56:08 * Sgeo really needs a way to repay pineapple, oklopol, and oerjan. Thank you SO MUCH 02:56:35 I feel like I'm taking and not giving 02:56:42 And fax 02:56:43 And alise 02:57:05 fax, what language is that? 02:57:28 coq 02:57:50 I just did this because it's ridiculous to do this 02:58:02 and I wanted to do a huge proof by computation 02:58:22 even though it was a contrived one 02:59:05 [In case anybody's interested, some game music I'm writing per request: http://codu.org/tmp/gm1wipp3.ogg ] 02:59:36 -!- augur has quit (Ping timeout: 265 seconds). 02:59:51 Sgeo: (0,0)(A,0)(0,B)(A-B,B)(A,B)(B,0)(A-B,0)(B,B) are the only configurations i can get without knowing more about the relative size of A and B 03:00:11 What's the second number supposed to be? 03:00:24 -!- augur has joined. 03:00:25 (contents of A, contents of B) 03:00:44 with A and B being their max volume 03:02:29 the last two are the only ones that might give more options by doing a transfer 03:02:44 hm wait 03:03:19 but what they give depend on whether they fill up or empty first 03:04:07 (0,A-B) or (A-2B,B) vs. (2B,0) or (A,2B-A) 03:04:20 *depends 03:04:45 oerjan, I'm interested in the configuration of the ring. I think at win, the water level of B is irrelevant 03:05:02 Sgeo: tap to A; while(A isn't empty) {A to B; if (B is full) B to floor; else tap to A;} 03:05:32 will, if A and B are co-prime, eventually pass through all amounts possible in A 03:05:39 Sgeo: i need both to know what i can get _from_ there though 03:05:56 oerjan: ^ might be helpful 03:06:09 in fact, that will cycle through all possible values of B as well 03:06:16 I don't have an easy way of measuring both atm 03:06:28 Hold on, actually 03:06:33 Sgeo: that psuedocode any help? 03:06:34 pineapple: co-prime is irrelevant 03:06:55 pineapple, when the puzzle is set up, I know how [inefficiently] to solve it 03:07:02 that's just factoring out the common factor 03:07:08 oerjan: only slightly... if they aren't, then there's less possible levels that can be hit 03:07:33 Sgeo: that;s also probably the most efficient way... 03:07:47 yeah but we can probably assume the sizes are reals or rationals 03:07:51 is what oerjan meant 03:07:55 i have no idea what you're talking about 03:07:57 either that or backwards, which is filling B and pouring as much into A each time 03:07:58 pineapple: i suppose by "all amounts possible" you mean "all integer amounts between 0 and A"? 03:08:10 When the original game was around, I just kept in mind to "preserve information" 03:08:46 what does it mean that a gameboard is divided into 11 segments 03:08:55 I think A = (3/2) B 03:09:00 oerjan: yes... although if they're not integers, then eventually you will either hit all possible things or never end... 03:09:05 well i guess just that, and i should read the rest of the rules to find out moer 03:09:06 *more 03:09:18 -!- augur_ has joined. 03:09:31 what does it mean that a gameboard is divided into 11 segments - ? 03:09:47 Actually, I just thought of an exact way to measure it *facepalm* 03:09:48 pineapple: oh wait i think i see a clue there - you always tap _into_ A but _out of_ B 03:10:11 oerjan: essentially: yes... or the other way around 03:10:15 -!- augur has quit (Ping timeout: 265 seconds). 03:10:44 -!- augur_ has changed nick to augur. 03:10:52 the total amount is always between 0 and A+B 03:11:18 I'm going to go collect the exact numbers 03:12:35 i like the matrix game 03:12:55 oklopol: the one i linked to? 03:13:04 and who can't calculate a 3x3 matrix determinant, you have to be able to remember like 5 numbers 03:13:19 oklopol: actually... less i think 03:13:22 i mean i'm not saying i can do it fast enough to play the game 03:13:30 yeah that was a completely random number 03:13:49 once you have it for the opening position: you only need to look at the (broken) diagonals of the target cell 03:13:55 i'm too tired to even want to think about trying to find the correct number 03:14:15 right of course 03:14:25 ad;D 03:14:55 so what it really does is x=A; while (x) {if (x>=b) x-=b; else x+=a;} 03:15:02 A: 6 03:15:04 B: 4 03:15:14 night again 03:15:15 *x=a; 03:15:17 Night oklopol 03:15:17 ad;D? 03:15:18 -> 03:15:34 Sgeo: you pulled those numbers from the code? 03:16:06 pineapple, I moved an object to the bottom and top of each cylinder, and measured its location 03:16:22 suggest you do an svn blame (or equivalent), then yell at whoever chose those numbers 03:16:33 Um, why? 03:16:39 6/4 = 3/2, right? 03:16:42 And is 3/2 bad? 03:16:43 yes 03:17:00 How so? 03:17:09 but they've tried to implement something that they don't fully understand 03:17:41 by making a puzzle that has high marmite factor between trivial and frustrating 03:17:42 I didn't understand it enough to be able to give instructions 03:18:50 `define marmite factor 03:19:01 oerjan: never seen the tv ads? 03:19:07 I take it it's difficult to solve? 03:19:17 i don't watch tv, _and_ i'm norwegian 03:19:21 "marmite - you either love it or you hate it" - there's nothing in between 03:19:23 No output. 03:20:07 i do have a vague understanding of what marmite is, though 03:20:15 So to some it's difficult, some it's annoyingly easy? 03:20:24 Sgeo: i mean that it's either very trivial or very frustrating... and if the player can't work out that they should aim for A-B to make it trivial, then they will be very frustrated by it 03:20:49 Why don't I program it and see if it frustrates me 03:21:16 only if i choose the numbers :-) 03:21:49 Getting the person who created this to change it is probably ah.. somewhat difficult 03:22:11 -!- alise has quit. 03:22:34 Sgeo: then ask them a direct question: "what are you trying to acheive by including this puzzle? what is the point that you're trying to make?" 03:22:36 * oerjan now understands why that algorithm cycles through all possible amounts 03:22:55 -!- Oranjer has left (?). 03:23:05 pineapple, the puzzle is there because it was in the original game, but getting the numbers from the original is nigh-impossible now 03:23:15 original? 03:23:22 THe numbers are what they are because no one had a clear understanding of what they should be 03:23:45 http://wiki.activeworlds.com/index.php?title=Mutation 03:25:01 have you tried googling for spoilers, then calculating the numbers from that? 03:25:11 Original equiv puzzle: http://wiki.activeworlds.com/index.php?title=Image:Blue_crystal.PNG 03:26:06 Let me implement this, and if it really is that bad, I can convince someone to change the numbers 03:26:24 Sgeo: i take it that no-one else have even considered to measure them? 03:26:33 Correct 03:26:47 We wouldn't know how, I thinkl 03:27:03 ... 03:27:13 I mean, besides measuring pixels in a screenshot 03:27:28 Sgeo: you could use pineapple's algorithm 03:27:53 basically see how long it takes until you cycle to all 0 03:27:58 I thought pineapple was giving a solution for the puzzle, not how to generate.. OH 03:28:30 i am pretty sure you can deduce the ratio of A to B from the progression 03:28:32 well 03:28:35 taht works, yes 03:28:48 The original isn't playable anymore 03:28:50 Although we can visit 03:28:51 the other way is measure with pixels and see what numbers you get 03:28:53 assuming you manage to avoid hitting the red line 03:29:05 and if you do hit the red line 03:29:09 go the other way around 03:29:24 heh 03:29:30 Where did pineapple put his algorithm 03:29:45 pixels: a=227, b=118, target=76 03:29:49 Sgeo: /last tap 03:30:01 Sgeo: tap to A; while(A isn't empty) {A to B; if (B is full) B to floor; else tap to A;} 03:30:32 that causes the total amount to be changed by -B (mod A) at each step 03:30:34 What does tap mean? go to top? 03:30:47 yeah 03:30:49 tap to A means fill A from the tap 03:31:00 (all the way to the top) 03:31:02 * Sgeo does this by hand 03:31:13 B to floor means empty B 03:31:53 you count how many times you fill A, and how many times you empty B, until you cycle. then the ratio of times = ratio of volumes 03:32:22 I think I just hit an infini.. um 03:32:31 So this isn't how to determine how easy it is? 03:32:43 I think I hit the solution a bit too soon 03:32:47 my code is written based on C 03:32:50 it's how to determine all relevant information 03:33:07 (relevent for getting the if statement handled correctly) 03:33:10 For 6:4, tapping A, A->B is done 03:33:33 Sgeo:move the red line 03:33:51 The only positions A reaches are 0, 2, and 6 03:33:52 out of the way if you can 03:34:03 Unless I'm doing something wrong 03:34:09 Sgeo: yeah... sounds like you are 03:34:10 Sgeo: if you _know_ it's 6:4 you don't need to measure do you 03:34:34 oerjan, those are the measurements for the NEW stuff. I still don't know what the original was, but I think it was tougher than this 03:34:56 Sgeo: i'm almost certain it is, based on the screenshot 03:34:58 hang on 03:35:19 A can never reach anything other than 0, 2, and 6? 03:35:24 Sgeo: pineapple's algorithm shows that you can choose _any_ integer volumes you want 03:35:42 Sgeo: it should be able to reach 4 03:35:58 Hm 03:36:09 Um, that's even easier 03:36:59 Sgeo: the spots you can hit are the multiples of the greatest common factor of 6 and 4 (i.e. 2) 03:37:18 -!- fax has quit (Quit: Lost terminal). 03:37:24 Sgeo: nearest (smallest) interger solution for the original image, based om measurements: A=25, B=13, t=4 03:37:53 heh 03:37:57 Hm, remember, the camera was kind of at an angle 03:38:00 t? 03:38:07 target 03:38:13 wait 03:38:17 that's not right, lol 03:38:20 t=8 03:38:38 or... 03:38:42 fuck, hang on 03:39:27 no... 03:39:30 that ain't right... 03:39:36 if it were A=24, B=12 then things would be a bit awkward :D 03:39:40 -!- songhead95 has joined. 03:39:46 Hi 03:39:48 i'm getting t of 8,37 03:40:17 Maybe a more straight-on picture would be appreciated? 03:40:27 yes, very 03:40:41 in the original... did the red line move? i'm assuming not 03:41:01 It did not 03:41:04 As far as I remember 03:41:12 is there a Brainfuck interpreter that just takes input from stdin, and can be used as a shell interpreter eg. 03:41:12 #!/usr/local/bin/BRAINFUCK 03:41:21 or something 03:41:59 Should I try to make it so that the bottom edge of each cylinder is head-on? 03:42:03 songhead95: almost any interpreter should be able to do that, since all those #! characters are comment characters in BF 03:42:07 songhead95: Several. 03:42:12 Sgeo: yes 03:42:28 Might I suggest Egobfi? 03:42:33 also, as large as you can get it 03:42:59 thank you 03:44:31 http://i.imgur.com/Sn4ZE.png 03:46:15 Sgeo: AW looks positively... 90s. 03:47:16 B 157, A 283, t 93-96 (likely somewhere in the middle) 03:47:52 pikhq, it is 03:48:02 A/B gives 1.802547771 03:48:12 suggests 9/5 03:48:39 Probably better to use 9/5 than the exact original measurements 03:48:43 which puts t at 3 03:48:58 there's your answer, honey 03:49:04 tyvm 03:49:05 it's highly unscientific 03:49:12 but... that's often the best way 03:49:15 So what? Will it be playable? 03:49:59 Sgeo: all integers are playable, in principle ;D 03:50:07 Will it not be too trivial? 03:50:40 lessee 03:50:40 that should be... relatively easy 03:50:55 As long as it's not as trivial as 3/2 was 03:51:43 when B is emptued for the 3rd time, A has 3 in it 03:52:07 that's not trivial... and probably not that frustrating 03:52:14 Awesome 03:52:20 pineapple, how can I repay you? 03:52:21 5*2 == 1 (mod 9) 03:54:05 Sgeo: can't think of anything 04:09:49 -!- Asztal has quit (Ping timeout: 264 seconds). 04:26:06 -!- jcp has quit (Quit: I will do anything (almost) for a new router.). 05:15:10 -!- augur has quit (Ping timeout: 256 seconds). 05:49:08 -!- augur has joined. 05:49:20 eyo 05:56:56 So much for hoping that my code would be perfect first time 06:27:08 -!- deschutron has left (?). 06:30:58 -!- coppro has joined. 07:21:30 -!- oerjan has quit (Quit: leaving). 07:58:18 -!- Sgeo has quit (Ping timeout: 265 seconds). 07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 08:29:56 -!- coppro has quit (Quit: upgrade time). 08:53:53 -!- coppro has joined. 09:00:18 -!- coppro has quit (Quit: I am leaving. You are about to explode.). 09:33:04 -!- kar8nga has joined. 09:33:45 -!- kev_ has joined. 09:34:14 -!- kev_ has quit (Client Quit). 09:36:11 -!- pikhq has quit (Read error: Connection reset by peer). 09:37:30 -!- FireFly has joined. 09:42:48 -!- pikhq has joined. 10:06:24 -!- tombom has joined. 10:24:23 -!- nooga has joined. 10:36:52 ouch 10:37:05 i just caused panic 10:42:13 -!- BeholdMyGlory has joined. 11:11:13 -!- nooga has quit (Ping timeout: 240 seconds). 11:15:40 -!- MigoMipo has joined. 11:25:05 -!- kar8nga has quit (Read error: Connection reset by peer). 11:36:29 -!- nooga has joined. 11:45:10 -!- alise has joined. 11:45:20 Maximal antipotential. 11:45:37 07:18:59 wow, the Poincaré conjecture has been proved 11:45:43 :slowpoke: 11:46:12 the guy who solved it is awesome he denied a prize for it because he didn't think the board were qualified to assess his work 11:46:41 "According to a 2006 interview, Perelman is currently jobless, living with his mother in Saint Petersburg." 11:46:47 guess he really doesn't like money 11:49:55 ais523: to be less obtuse, the Poincare conjecture was proved 2002-2003 11:50:54 Yes, but the actual millennium prize about it seems to have been awarded to him two days ago, making this a bit topical. One has to wonder whether they bothered to ask him if he wants it, though. 11:52:17 On 18 March, 2010, Perelman was awarded a Millennium Prize for solving the problem.[14] He had previously stated that "I'm not going to decide whether to accept the prize until it is offered."[3] 11:52:21 So: I think he did accept. 11:53:04 http://www.claymath.org/poincare/index.html 11:53:12 they misromanised his name :))) 11:53:51 I don't know; New Scientists says "A million-dollar prize for solving one of toughest problems in mathematics has been awarded to a Russian mathematician, but the real puzzle is whether he'll accept it." 11:54:02 Ah; okay. 11:54:04 "The president of CMI, James Carlson, is waiting to see if Perelman will do the same for the Millennium prize. "It may be a while before he makes his decision," he says." 11:54:05 Then we will see. 11:54:29 alise: There are different romanizations, and that, AFAIK, is valid. 11:54:29 I imagine he will probably decline; why Millennium but not Fields? 11:54:43 Deewiant: Yeah, I know :P 11:54:54 Grigori is a nicer romanisation though 11:55:01 Though, billions and billions of dollars! 11:55:14 Maybe his mother goes all "you'll take that money or I'll kick you out". 11:55:17 I guess the -iy is closer to the actual pronunciation 11:55:40 Although I guess nobody English will pronounce it any differently whether it's -i, -y, or -iy 11:55:59 Billions and billions: 1 million 11:56:30 Well, those were small billions. 11:56:38 I'm pretty sure anyone who declines the Fields medal is one fucking morally certain man 11:57:05 Heh, the Fields medal only awards $15,000USD as of 2006 11:58:13 19:46:15 Sgeo: AW looks positively... 90s. 11:58:13 that's why he likes it 11:58:31 WIND OF FURY! POWER OF BLOOD! HEALING! LIGHT! BY YOUR POWERS COMBINED, I AM--- 11:58:34 (http://i.imgur.com/Sn4ZE.png) 11:58:39 ooh, I forgot MAGIC SHIELD! 12:00:16 The one that ends up with -i sounds a bit non-information-preserving; I don't know how that domanization would differentiate between Григорий and Григори; google seems to suggest that some people use the latter as a name too. 12:00:27 s/dom/rom/ 12:00:33 Fair enough. 12:00:35 DOMINATION. 12:00:36 even if i had no use for a million, i'd take it just so others don't get it 12:01:04 I might decline some prestigous prize because I'll be more famous if I do that :) 12:01:11 but i would totally have a use for a million, i've always wanted to give some homeless guy 100000 12:01:34 oklopol: Then he'll spend it all on booze and die, you man-slaughtererer. 12:01:53 :DDDD 12:01:55 Quite frankly I would enjoy money. 12:02:05 Shocking, I know. 12:02:12 i would probably choose one whose brain isn't completely melted yet 12:02:29 oh well i would probably buy a house too 12:02:35 and a few books 12:03:08 and probably give half of the rest to people i know and half in a bank of smth 12:03:10 My wife asked me what I'd do with 50 million euros (she'd buy some 14-million manor somewhere, I forget just where); the first thing I could think of was "hmm, maybe I'll buy dessert with lunch at work". (That costs 0.95 eur extra.) 12:03:35 i like books 12:03:41 dessert not so much 12:04:46 i'd prolly just hire a buncha expensive people to manage it for me and turn it into more money (they can have some so they don't run away) 12:04:53 and then I could gain money without bound, and thus I could completely ignore money as it is, over time, infinite 12:05:03 take that, capitalism 12:05:05 yes 12:05:41 Everything's so expensive nowadays since I no longer get any student discounts; apparently graduate students aren't quite as good as real students. So the lunch is now 5.40 eur as opposed to 2.55 or so. 12:05:59 hehe 12:06:47 i'd also get loads of people to build my perfect house, buying one is so boring 12:06:48 you don't work at uni? i mean if you get a salary, 5,40 is nothing 12:07:08 i want like... i don't know, cool technology. in my walls 12:07:51 oklopol: It's the principle of it! Besides, the change in lunch price pretty much ate the wage-raise I got by graduating. (It bumps the "difficulty level" pay-scale column index by one automatically.) 12:08:11 (And the change in bus ticket price did the rest.) 12:14:54 even though I dislike geometric proofs 12:14:58 Elements is so beautiful 12:15:02 the first constructivist work, I wonder? 12:15:30 also using geometry as the foundation of all mathematics amuses me... 12:16:05 weird 12:17:02 not really 12:17:17 i mean his geometry basically embeds the real numbers... 12:18:52 ha! 12:19:06 i'm going to scotland! 12:21:39 can't you do geometry on rationals? 12:23:24 i haven't actually seen an axiomatization of geometry, but i hear there were some really simple things that hadn't been realized to not be derivable from the axioms but were used as if they were, as late as late 1900's 12:23:40 because it's such a hard thing to axiomatize, given we have such strong intuitions about it 12:23:52 something like points exist between two points 12:25:35 we have a geometry course at uni, but apparently it skips some of the boring details 12:27:07 probably have to be pretty boring, because the lecturer said they were, and he was all hyper over cyclic modules "and we get this particularly fascinating fellow" he loves to personify things "if we just have one generator" 12:28:47 The Matrix Computations lecturer refers to matrices and vectors as people too, usually with the word "guy"; "and this guy here ... and we get this guy ..." and so on. 12:30:58 He also keeps laughing all the time, without any explicit jokes. 12:31:09 if there's a sum where i goes from 1 to n, the same lecturer often says "ja i kipittää 1:stä n:ään" 12:31:13 which i always find hilarious 12:31:44 where the funny thing is kipittää is a funny word 12:31:58 Some of my friends collected the best sayings of maths lecturers in notebooks; unfortunately I don't have any handy. 12:32:44 "These matrices can be... really big *ehehe*." It's very amusing to listen, though. 12:34:59 The course seems to currently be in a transition to the interesting part; the part where we no longer have a matrix A as a pile of numbers, but instead just a linear operator A that you can apply to a vector, because the matrix itself would be too large to store in memory. Now it's going to be all Krylov subspaces and whatnot. 12:35:25 what are those 12:35:35 please define them in guy terms 12:35:57 how many courses are you on usually? 12:36:01 at a given time 12:36:21 K_r(A, b) = span(b, Ab, A^2b, ..., A^(r-1)b), nothing more complicated than that. 12:36:51 I seem to have around 4-5 now. It's only something like 60 course credits for the licensiate/doctoral degree, after all. 12:37:18 so this A dude here makes all sortsa copies of itself and then all those copies have buttsex with b at the same time and a vector space is spanned 12:37:47 Yes. Except you have to worry about the numerical stability of the buttsex. 12:37:53 oh 12:39:37 whats 12:39:39 that mean 12:39:41 ' 12:40:03 4-5 is considered a lot among turkuans 12:40:28 maybe we are a crappier uni 12:41:03 I don't think it's considered "a lot" here, but it's not an especially tiny amount either, I Guess. 12:41:19 -!- tombom has quit (Quit: Leaving). 12:41:25 actually one of the professors told me people in turku are better at math usually, which he'd probably be regretting if he knew i was gonna tell it to everyone 12:41:58 Back at the beginning of the course, when he was trying to motivate the course by talking about big matrices, he was all about "the Google matrix", which is a NxN matrix where N is the size of the Internet. 12:42:23 I guess this is somehow related to the fact that you get PageRank values as eigenvalues of some sort of adjacency matrix of the Internet. 12:42:40 or the universe matrix containing for each point the points at most one meter from it?!? 12:43:06 There might've been actually some physics problem, though maybe not quite like that. 12:43:16 unless you can give out search results by multiplying with the matrix, then it would be slightly more interesting 12:43:44 have to go see ya 12:43:51 Same here, actually; boo-ya. 12:50:13 -!- oklopol has quit (Ping timeout: 276 seconds). 12:52:05 turns out linear functions are invertible (they have normal function inverses) iff their determinant is nonzero <-- makes perfect sense considering that is true for matrices. 12:53:00 I suppose none of this is related to Computer Science? Maybe I should stick with this college and Minor in math <-- well, matrices at least are used a lot in programming. Especially 3D iirc. 12:54:05 CS != programming 12:54:13 alise, well yes 12:54:22 alise, however programming is a part of CS 12:55:19 no 12:55:23 programming isn't even applied CS 12:55:44 programming, aka software engineering, is an enirely separate field that happens to use some ideas from CS 12:55:50 just like physics uses mathematics... 12:57:01 alise, however, I'm pretty sure (basic) programming is taught as part of CS courses. At least for all universities I checked. 12:57:15 alise, which is what I was talking about 12:58:00 If a CS course involves Java, C, Python - it's probably crap. 12:58:14 Well, Python can go okay, but only if it's used in an abstract way. 12:58:16 alise, I think C and lisp were the most common ones 12:58:28 pyhton at third place I think 12:58:29 Nah, Java. 12:58:33 java was very rare 12:58:34 (Almost all (mathematical term!) CS courses suck.) 12:58:36 for true CS 12:58:52 In fact I'm not sure I'd call any existing CS curriculum good. 12:58:59 MIT sorta ruined theirs by abandoning SICP and doing robots in Python instead. 12:59:05 hah 12:59:47 The xkcd effect, may I call it. 13:00:05 alise, what? 13:00:09 "Default search engine has been changed to Yahoo!" --Ubuntu.com 13:00:14 I smell money. 13:00:16 alise, joke? 13:00:37 AnMaster: xkcd glorifies "fun hacking!" and "zomg cool robots!" and "python is SO EASY!" 13:00:48 "This beta sports full removal of HAL from the boot process, making Ubuntu faster to boot and faster to resume from suspend." 13:00:48 Well, that's good. 13:00:53 alise, well sure, python *is* easy 13:00:58 "We now feature built-in integration with Twitter, identi.ca, Facebook, and other social networks with the MeMenu in the panel, which is built upon the Gwibber project, which has a completely new, more reliable backend built on top of desktopcouch. Gwibber now also supports a multi-column view for monitoring multiple feeds simultaneously." 13:00:59 Fuck me. 13:01:08 MeMenu? 13:01:11 what the heck 13:01:12 "Millions of songs are available for purchase from your Ubuntu desktop, integrated with the Rhythmbox Music Player and using Ubuntu One cloud storage for backup and easy sync. Watch http://one.ubuntu.com/blog for the public beta launch." 13:01:13 Vomit. 13:01:22 Otherwise a humdrum improvement release. 13:01:23 ouch 13:01:37 But seriously: Yahoo, social crap by default, integrated music purchasing? 13:01:37 Eat a dick. 13:01:42 alise, I think jaunty might have been the last "good" release 13:01:51 maybe karmic 13:01:53 I didn't mind 9.10. 13:02:07 Karmic's the latest release. :P 13:02:16 alise, well this new one sounds horrible 13:02:29 I only quoted the horrid bits. Obviously. 13:02:32 "Paul also noted that the most controversial aspect of the new design amongst users has been the placement of the window control buttons on the left instead of the right side of the windows" 13:02:35 alise, right 13:02:36 Copying OS X, are we? 13:02:50 mhm 13:02:59 I don't use standard theme anyway 13:03:16 Y'know what? I think I'll just stick with Windows 7 for now. 13:04:08 alise, arch linux isn't too bad 13:04:59 alise, on the plus sides it doesn't integrate music stores, nor social crap by default, and default search engine is whatever uses as upstream default 13:05:20 yeah but on a laptop? 13:05:23 CBA 13:05:27 alise, good point 13:05:48 clearly I should just instantly code ehirdOS 13:05:58 good luck 13:06:05 alise, ACPI is horrible I'm told 13:06:12 and you really need that for laptops :( 13:06:38 * alise decides to name his first proof system something along the lines of provenance 13:06:40 maybe nance 13:07:07 it'll have two components, the proof checker (basically a typechecker for some dependently-typed total lambda calculus) and the proof compiler (from a form you'd actually want to write; with niceties such as definitions) 13:07:13 so they need names 13:07:31 and also perhaps a third component, that extracts computational (non-proof) content from a proof and compiles that to some functional language 13:07:41 profchk and profc 13:07:45 for checker and compiler 13:07:48 I guess the proof checker should be prove, and the compiler nance, if I'm going by provenance 13:07:51 AnMaster: That's way boring. 13:07:55 alise, well yes 13:08:10 plus typoed 13:08:12 Maybe I should have: 13:08:15 prove -- checker 13:08:19 nance -- compiler 13:08:19 proof* for booth 13:08:32 volit -- program extractor 13:08:38 why volit? 13:08:40 The system as a whole being Provenance and Volition. 13:08:54 Because computation is like some sort of volition. 13:08:55 * AnMaster wonders what volition means 13:09:00 You're going forwards to do some sort of goal. Of such. 13:09:11 The problem is that prove is a bit of a vague name for a proof checker. 13:09:22 google result is Volition® as the third 13:09:25 just FYI 13:09:38 Eh? 13:09:46 alise, registered trademark 13:09:54 It's a bloody English word 13:09:58 You can't trademark it 13:10:02 Not like that 13:10:05 alise, well it seems to have been done :/ 13:10:05 Only in some very specific field 13:10:13 You fail at trademark law :P 13:10:19 probably 13:10:46 I should clearly write PROVE first. 13:10:50 In, eh, let's say Haskell. 13:11:06 What calculus? Perhaps the calculus of inductive constructions. 13:11:25 alise, why not in coq or agda? 13:12:22 Because I don't really know enough of Coq or Agda to do those. If I was doing it so I could prove the checker correct, then Agda would be the wrong choice; it's a very experimental, exporatory language and false has been proven in it many many times. 13:12:22 Coq I know even less than Agda. 13:12:40 Besides, volit will probably spew out (horrific) Haskell. 13:12:57 It annoys me that prove has to know about sets, and not just propositions. 13:13:36 alise, what exactly will volit do? 13:14:41 Well, nance is in many ways like a programming language. You have data types, in Type, and you have a subset of Type named Prop which contains propositional statements. 13:14:53 right 13:14:55 You prove a Prop by writing (terminating) code that constructs a value of the given Prop. 13:15:12 The values of Props are irrelevant - they are indistinguishable; for any x,y:P where P:Prop, x=y 13:15:17 but the values of Sets are not 13:15:25 alise, sounds like you are an constructivist ;O 13:15:27 ;P* 13:15:32 You don't say. 13:15:46 Through the Curry-Howard lens, we can eliminate proofs (Prop values), as they carry exactly 0 bits of information. 13:16:04 We have lambdas, as ways of proving implication and also defining functions on sets. 13:16:08 So... we have a total programming language. 13:16:14 okay 13:16:30 Sprinkle on some mechanism for IO, and you have both a programming language with dependent types and consequently proving, and a proof assistant. 13:16:47 indeed 13:17:01 and where does volit fit in 13:17:02 If you're doing proofs, you use nance and it feeds its result to prove for you; if you're programming, you use nance and it feeds its result to volit (and then, presumably, to ghc) for you. 13:17:09 ah 13:17:15 Often the files you do both to will be the same. 13:17:27 right 13:17:31 why not allow non-constructive proofs btw? 13:17:31 AnMaster: Well, the typechecker just says "Yes" or "No" in so many words. 13:17:46 Well, because I don't believe that forall p, p \/ ~p, for one. 13:17:53 Two, you can have that 13:18:02 classicalOr p q = ~(~p & ~q) 13:18:20 Or you can even just take as a parameter the law of the excluded middle, thus having LEM -> whatever. 13:18:24 Constructivism contains classical logic 13:18:25 alise, is ~ = not? 13:18:28 yes. 13:19:08 But it's simple as that I'm a constructivist, and I also believe in the computationalness of proofs and the like - total Curry-Howard disciple - so, begone LEM. 13:19:16 why don't you believe forall p, p \/ ~p ? 13:19:23 well, okay LEM I guess 13:19:30 That's law of the excluded middle. 13:19:42 AnMaster: Consider axioms like the Continuum Hypothesis (in the context of ZFC). 13:20:01 * AnMaster reads up on that one 13:20:01 You can add the axiom CH to ZFC, and yield an (almost certainly) consistent system (if ZFC is consistent that is). 13:20:05 You don't need to. 13:20:07 It's just an example. 13:20:08 You can also add the axiom ~CH to ZFC. 13:20:11 Still consistent. 13:20:16 ouch 13:20:18 So in plain ZFC without any frills: is CH true or false? 13:20:23 The answer is that it's neither. 13:20:34 alise, undecidable? 13:20:34 AnMaster: also true for large ordinal axioms 13:20:39 *large cardinal 13:20:44 AnMaster: Not undecidable. 13:20:47 hm okay 13:20:57 Consider Godel's theorem. 13:21:03 okay 13:21:05 It's not quite the same. 13:21:28 hm okay, I think I see what you mean 13:21:48 though I'm the first to admit that this is way out of my expertise. 13:22:14 AnMaster: It's simple enough: There are statements for which our formalisms do not have the mechanisms that we can apply to derive either a proof of p, or a proof of not-p. 13:22:25 Given that, where does the law of the excluded middle stand? 13:22:32 good point 13:22:43 Either p or not p -- but it cannot be shown to be either. My opinion - shared with other constructivists - is that it is neither. 13:22:51 alise, but non-constructive proofs are sexy :P 13:23:13 I think proofs of ~~p are not very interesting. :P 13:23:21 hah 13:23:24 AnMaster: Mind you, I do believe that ~~p is very strong evidence for p. 13:23:35 I just don't believe it entails it. 13:23:44 in a two-valued boolean logic at least 13:23:56 Yeah, well, propositions aren't booleans. 13:24:18 Whoever first made (x = y), (x > y) etc. booleans was a vile person. 13:24:20 computers however *work* on boolean logic basically. 13:24:30 No, they work on electricity. 13:24:41 alise, well sure, but at one level they do what I said mostly 13:25:24 for the digital logic parts of them, which makes up a rather large and crucial portion of how they work 13:26:10 Coming up with a model for inductive types is Hard. 13:26:10 of course there are analogue computers, but from what I understood they are kind of rare 13:26:22 Incidentally, nance will be where the type inferrence is. 13:26:29 interesting 13:26:37 prove will literally require an annotation for every single parameter and result. 13:26:41 alise, I suspect the output it generates then might be rather large. 13:26:49 And no variable names or anything: It takes in lambda calculus with De Bruijn indexes. 13:26:53 (Plus type annotations). 13:26:56 okay *very* large then 13:27:10 Not /that/ large. 13:27:28 I mean, GHC basically stops one step short of lambda-calculus. 13:27:34 well, I can't really predict how much it will grow compared to input 13:27:56 Not that much, really. You can't infer anything dependent anyway. 13:28:00 Well, almost anything. 13:28:09 So only trivial things will have their types inferred. 13:28:32 and well, I presume you somehow at the end can get out reasonable machine code, reasonable for an OS that is (which was your goal wasn't it?) 13:28:59 Oh, this is just my first foray into actually making one of these. 13:29:08 Nowhere near OS stage yet. 13:29:24 alise, out of interest: how will you handle the low level interaction with the architecture in your OS? Some parts must be OS specific, be it configuring memory mappings or whatever. 13:29:29 can those be proved? 13:29:36 s/OS specific/hardware specific/ 13:29:41 The machine code generated will probably not be pretty; after all, 42 will be represented by 42 nested constructors and then a unit value. 13:30:04 alise, pipe it into llvm or something and hope for the best? 13:30:13 GHC produces alright code anyway. 13:30:17 true 13:31:13 alise, still, I find the problem of proving the bits that deal with poking hardware correct quite interesting. Such as setting up memory mappings for processes and dealing with DMA or whatever. 13:31:19 AnMaster: Also, they don't need to be proved. 13:31:25 alise, oh? 13:31:26 After all, the correctness of the code depends on the hardware being correct in the first place. 13:31:32 well true 13:31:40 I was just about to say that that might be an issue as well 13:31:55 Well, I don't think FDIV ever happened again. 13:32:00 They formally verify chips nowadays. 13:32:10 iirc intel and amd both use correctness checkers for their CPUs nowdays, at least for the FPU. No one wants to see another FDIV bug 13:32:20 alise, damn you beat me to it :P 13:32:27 I love how induction <=> recursion. 13:32:56 alise, I knew they were related, but are they actually equivalent? 13:33:01 yep 13:33:14 wonderful indeed 13:33:32 I can't see how to get from one to the other exactly, but yeah they are pretty similar when you think about it 13:33:34 nat-induct : forall (P : Nat -> Prop), P 0 -> (forall (n:Nat), P n -> P (succ n)) -> forall (n:Nat), P n 13:33:43 now ignore Prop being propositions so irrelevant values just imagine it's any type 13:33:47 n:Nat? 13:33:50 then consider P x = Integer 13:33:55 AnMaster: forall naturals n 13:33:55 is that "n in N"? 13:33:57 then we have 13:33:58 right 13:34:22 integer -> (forall (n:Nat), integer -> integer) -> forall (n:Nat), integer 13:34:24 forall is the same as a function arrow 13:34:24 so 13:34:38 integer -> (Nat -> integer -> intgeer) -> (Nat -> integer) 13:34:39 so the first argument is the base case 13:34:51 the second gets the current value to consider, and also the rest of the computation (lazily) 13:34:55 and it combines the two with recursion 13:35:00 it's fold! 13:35:17 in fact you can derive a function like this for /any/ inductive data type, mechanically 13:35:44 alise, btw do you reject proofs of existence by contradiction (that is, proving something must exist, because otherwise it would result in a contradiction, without giving any way to construct said thing) 13:35:44 epigram 2 does this 13:35:45 -!- kar8nga has joined. 13:36:24 AnMaster: Something must exist, otherwise contradiction = Not something must exist, implies contradiction = Not not something must exist = Not not P = ~~P 13:36:27 So that's using ~~P to prove P. No. I do not accept that. 13:36:32 mhm 13:36:52 ah 13:37:00 building plan9port 13:37:13 alise, I think that means you end up rejecting some major parts of modern mathematics. 13:37:20 I don't remember which parts 13:37:30 but I'm pretty sure I read about that somewhere 13:37:30 you don't 13:37:41 you reject uncomputable real numbers, but nobody cares about them 13:37:50 AnMaster: consider that the four-colour theorem was proved with Coq 13:37:53 a constructivist system 13:37:59 it's very much practical 13:38:15 http://en.wikipedia.org/wiki/Existence_theorem mentions "Such pure existence results are in any case ubiquitous in contemporary mathematics. For example, for a linear problem the set of solutions will be a vector space, and some a priori calculation of its dimension may be possible. In any case where the dimension is probably at least 1, an existence assertion has been made (that a non-zero solution 13:38:15 exists.)". I don't have any clue what that means though really 13:38:39 Incidentally, interesting thing: 13:38:42 ((P?Q)?P)?P 13:38:45 This is Pierce's law. 13:38:46 erm 13:38:49 alise, what is the ? there 13:38:50 ((P->Q)->P)->P 13:38:52 ah 13:38:55 Pierce's law. 13:38:56 But! 13:39:00 It is the type of call-with-current-continuation. 13:39:17 interesting 13:39:20 The continuation is (P->Q), i.e. gimme something and I'll give you anything (it's just a dummy value computationally so you can put it anywhere) 13:39:35 and you result in a P (because whatever you pass to the continuation must be able to stand for what would normally result, typewise) 13:39:36 and it gives you a P, by constructing a continuation 13:39:37 BUT! 13:39:47 This doesn't hold in intuitionistic logic (and other similar constructivist ones) 13:39:52 call/cc is always somewhat mind bending. 13:39:52 because it implies the law of the excluded middle 13:39:58 first, know that _|_ is the type with no elements, i.e. falsity 13:40:00 alise, so no call/cc in your language? 13:40:03 and that ~p is p -> _|_ 13:40:52 ((P->_|_)->P)->P 13:41:02 "In particular, when Q is taken to be a false formula, the law says that if P must be true whenever it implies the false, then P is true. In this way Peirce's law implies the law of excluded middle." 13:41:07 specifically 13:41:09 if we have _|_ 13:41:11 we can prove anything 13:41:15 so if P is true whenever it implies the false 13:41:27 that means that P is true 13:41:29 because P implies false 13:41:32 and from false we can derive P 13:41:38 mhm 13:41:46 ergo, law of the excluded middle 13:41:58 so call/cc -> law of the excluded middle :D 13:42:06 AnMaster: no call/cc outside of something like a continuation monad 13:42:09 no biggie - haskell doesn't have it either 13:42:23 true 13:42:49 AnMaster: you know the y combinator? as in a fixed point combinator doesn't matter which one 13:42:51 fix : (a -> a) -> a 13:42:56 so fix (1:) = [1,1,1,1,1,1,...] 13:43:03 i.e. fix f = f (fix f) 13:43:07 right? 13:43:28 hm 13:43:46 AnMaster: oh please tell me you know that 13:44:10 just say yes :P 13:44:20 it is familiar, but never really used lambda calculus. 13:44:25 it's in haskell too 13:44:26 fix (1:) = 1 : fix (1:) = 1 : 1 : fix (1:) = ... 13:44:29 if it is composition? 13:44:46 fact = fix (\me n -> if n == 0 then 1 else me (n-1)) 13:45:05 fact = (\me n -> if n == 0 then 1 else me (n-1)) (fix (\me n -> if n == 0 then 1 else me (n-1))) 13:45:05 ah a quick check on wikipedia reminded me of what it was 13:45:10 yeah I read about that before 13:45:11 ages ago 13:45:14 fact = (\me n -> if n == 0 then 1 else me (n-1)) ((\me n -> if n == 0 then 1 else me (n-1)) (fix (\me n -> if n == 0 then 1 else me (n-1)))) 13:45:15 etc 13:45:18 thus allowing recursion 13:45:20 AnMaster: anyway 13:45:22 look at the type 13:45:22 okay 13:45:25 fix : forall a, (a -> a) -> a 13:45:27 consider it logically 13:45:31 (a -> a) is a tautology 13:45:34 so it's saying 13:45:35 fix : forall a, a 13:45:38 WUT! 13:45:45 and indeed using fix we can derive ANYTHING 13:45:47 id : a -> a 13:45:47 so 13:45:47 alise, (a implies a) implies a? for all a? 13:45:51 yep 13:45:51 fix id : forall a, a 13:45:59 wonderful 13:46:02 so for all p, p is true, not p is true, ... 13:46:07 fix is inconsistency in a bag! 13:46:16 ...and this, kids, is why you don't allow general recursion 13:46:33 id : a -> a <-- that seems sane to me though. id is a no-operation after all 13:46:44 wait, not if that is implies 13:46:50 of course 13:46:52 hm 13:46:53 a implies a for all a 13:46:56 id is true 13:47:03 but (a -> a) -> a is not true 13:47:07 obviously a implies itself 13:47:13 if 2 is prime, then 2 is prime 13:47:18 if 2 is not prime, then 2 is not prime 13:47:18 etc 13:47:24 proof: \x -> x 13:47:32 so in fix : (a -> a) -> a 13:47:36 alise, but considering the truth table for -> something seems wrong if id: a->a 13:47:37 we can ignore (a -> a) as it's already proved 13:47:40 so fix : forall a, a 13:47:40 if a is false 13:47:46 AnMaster: why 13:47:47 also 13:47:51 -> doesn't have a truth table 13:47:57 but even classically A -> A holds... 13:48:00 it's an axiom 13:48:04 alise, not the classical logic ->? 13:48:19 classical -> has a truth table 13:48:22 alise, yes 13:48:24 but A -> A is still always true 13:48:25 that is the one I meant 13:48:28 alise, it is 13:48:30 it reduces to !(A&!A) 13:48:37 which is the law of non-contradiction 13:48:40 Q.E.D. 13:48:42 but a -> b, says basically nothing about b if a is false 13:48:44 anyway, so 13:48:47 foo : somethingtrue -> a 13:48:49 is equivalent to 13:48:50 foo : a 13:48:55 proof: foo theproofofsomethingtrue 13:48:56 so 13:48:58 alise, yes 13:48:58 fix is equivalent to 13:49:00 forall a. a 13:49:05 mhm 13:49:10 plug in _|_ for a 13:49:12 and you get a proof of false 13:49:14 tada 13:49:35 hm indeed 13:49:53 plug in reimann-hypothesis for a, and you get a proof of that too 13:49:59 plug in ~reimann-hypothesis, and its negation appears! 13:50:07 so many THINGS we can achieve with trivialism! 13:50:30 heh 13:51:39 file extension .na is free. not any more! 13:51:41 stolen for nance 13:52:02 actually .ne looks nicer to me, so 13:53:25 hm, while I do like some of the points of total fp, I still quite like non-constructive proofs. what a dilemma this is :/ 13:54:17 alise, do you reject or accept proof by induction btw? 13:54:25 Induction is obviously true. 13:54:37 Proof: Structural recursion. 13:54:41 alise, transfinite induction? 13:54:56 yes. 13:54:59 provable 13:55:01 okay 13:55:35 Why haven't you asked me about the Axiom of Choice yet? 13:56:22 alise, hah 13:56:47 How's that funny 13:56:54 you can't prove it, that is why it is called axiom. But why are you so eager to be asked about it? 13:57:11 (at least you can't prove it from some sets of axioms) 13:58:16 alise, also since you accept transfinite induction, doesn't that mean you must accept AoC? 13:58:43 at least for uncountable sets 13:59:14 (or maybe I'm mixing this up) 14:01:35 you are mixing it up 14:01:35 Anyway, I only accept some of the Axiom of Choice: the part that is provable. 14:01:46 http://r6.ca/blog/20050604T143800Z.html 14:01:46 right 14:01:54 The intensional axiom of choice. But you know what? 14:01:57 It doesn't imply well-ordering. 14:02:08 It's Axiom of Choice without the weird shit. 14:02:08 sets vs. types iirc or such? 14:02:11 And it's provable in type theory. 14:02:33 putString : (Sigma (w : World m c). pre c) -> (World (m+1) (modify c) -> Sigma (w' : World n c'). (n > (m+1) ? post c')) 14:02:33 where pre c = stdout is open in conditions 14:02:33 modify c = c (I don't think writing to stdout should ever change conditions...) 14:02:33 post c = nothing, we require no postconditions here 14:02:33 I think. 14:02:43 oh wait, forgot the result 14:03:26 putString : (Sigma (w : World m c). pre c) -> (World (m+1) (modify c) -> Sigma (w' : World n c'). (n > (m+1) ? post c')) -> Sigma (w' : World n c'). (n > (m+1) ? post c') 14:03:26 I think 14:03:28 oh, I forgot the actual string :D 14:04:40 I can't read that, and you know that 14:05:49 putString : String -> WorldSatisfying m c stdoutOpen -> (World (m+1) c -> WorldGreater n c' (m+1)) -> World n c 14:05:49 I think 14:05:56 AnMaster: I'm just musing to myself 14:06:33 AnMaster: actual usage of this will look something like 14:06:34 okay 14:06:35 main : IO Unit 14:06:36 main = putString "Hello, world!" 14:06:43 prolly 14:06:56 AnMaster: it's just condition magic so that it's actually impossible for the program to, e.g. write to a closed handle 14:07:09 because the writing functions require the conditions of the world you give it to have that file handle to be open 14:07:26 and the close function transforms the conditions in the new world the continuation gets so that the handle is closed there 14:07:35 mhm 14:08:07 alise, it shouldn't be too hard to make it impossible to write to a closed handle in a "normal" language. (Yeah "normal" isn't really the right word, but...) 14:08:18 I'm talking at typechecking time here. 14:08:19 Not at runtime. 14:08:27 right, that is somewhat harder 14:08:32 (AnMaster slowly creeps away, defeated.) 14:08:42 AnMaster: Slight misuse of the term somewhat there 14:08:43 for runtime, something like ref counting should work 14:09:58 alise, well, perhaps. but if you in a "normal" language would require proof that a file handle could not escape a given scope, and then could prove how it is used in said scope it would be possible before runtime there too. no? 14:10:22 of course, that doesn't cover all possible situations 14:12:37 how can you require a proof in a normal language 14:12:42 you can't 14:12:58 "Recursion must be easier than recursion. Otherwise recursive programs would never terminate." 14:13:01 "QED." 14:15:22 hehe 14:16:19 bbl 14:16:40 type IO r = (Sigma (w : World m c). pre c) -> (World (m+n) (change c) -> r -> Sigma (w : World m' c'). (m' > (m+n) /\ post c')) -> World m' c' 14:16:41 I think. 14:17:34 type IO pre change post r = (Sigma (w : World m c). pre c) -> (World (m+n) (change c) -> r -> Sigma (w : World m' c'). (m' > (m+n) /\ post c')) -> World m' c' 14:17:36 I think. 14:17:41 main : IO stdoutOpen id (const ?) Unit 14:17:41 main = putString "Hello, world!" 14:17:45 That's const T there 14:17:49 main : IO stdoutOpen id (const T) Unit 14:17:49 main = putString "Hello, world!" 14:18:27 -!- fax has joined. 14:18:51 IO pre change post r -- the type of an IO interaction on a world satisfying pre, which does change to the world's conditions, and results in an r, as long as the world at the end of the hullabaloo satisfies post 14:18:53 type IO pre change post r = (Sigma (w : World m c). pre c) -> (World (m+n) (change c) -> r -> Sigma (w : World m' c'). (m' > (m+n) /\ post c')) -> World m' c' 14:19:01 oh, I need to paramaterise over n... grr 14:19:05 I'd rather not though 14:19:16 fax: simplify my io system :p 14:20:26 SIMPLIFY 14:20:29 ENHANCE 14:20:42 zoom in on his pocket, what's in that letter? 14:20:45 fax: yes. do so 14:20:56 GENERALISE 14:20:57 type IO a = a 14:22:29 I like data IO :: * -> * where Return :: a -> IO a ; (:>>=:) :: IO a -> (a -> IO b) -> IO b ; PutChar :: ... 14:22:46 you can just do something like that, except with stronger specifications in the types 14:23:22 but that breaks things when you add new IO actions 14:23:25 IMO, you should be able to write 14:23:29 postulate foo : ... some IO action ... 14:23:33 and have everything still work 14:24:59 type IO pre change post r = (Sigma (w : World m c). pre c) -> ((Sigma (w' : World m' (change c)). m' > m) -> r -> Sigma (w'' : World m'' c'). (m'' > m' /\ post c')) -> World m' c' 14:25:11 I guess I don't need to paramaterise on pre/change/post, that can just be part of the types of the actions 14:26:35 type IO r = ((Sigma (w : World m c). m > SOMETHING) -> r -> Sigma (w' : World m' c'). (m' > m /\ SOMETHING)) -> World m' c' 14:26:40 Maybe? 14:27:10 I never understood the 'realworld' stuff 14:27:17 just seemed inelegant to me 14:27:39 well here World is a very abstract thing 14:28:03 World m c is a (thing) of sequence number m (we use this to ensure you can't use the same world twice, as you have to do it increasingly), with conditions c 14:28:05 conditions are things you can do like 14:28:08 isOpen stdout c 14:28:15 as in, in the conditions c, is the file handle stdout open? 14:28:22 and also transform 14:28:24 withClosed stdout c 14:28:41 apart from that, it's completely opaque 14:28:55 c++ help super primes @_@ 14:28:56 immediate need asap : c++ help super primes @_@ 14:30:06 hmm, I guess I need postulate data structures 14:30:22 postulate IOStruct : Sigma (IO : Set). isIO IO 14:30:33 not Set 14:30:39 and I need to posulate World instead 14:30:59 postulate WorldStruct : Sigma (World : Nat -> Conditions -> Set). isWorld World 14:31:51 fax: i mean your IO data structure just doesn't handle things like FFIs and the like 14:31:55 or even added IO operations 14:32:12 yeah it does 14:32:13 fax: besides you need SOME sort of world-like structure, because you need to be able to do pre and post conditions 14:32:15 that's what the ... bit was for 14:32:32 it's put pre & post conditions in bind 14:33:00 so what is bind's type? 14:33:48 forget about IO for a moment 14:33:53 this works for any monad 14:33:53 k 14:34:59 I'm waiting 14:35:30 nevermind, it was wrong 14:36:03 lol 14:36:07 the problem with 14:36:08 type IO r = ((Sigma (w : World m c). m > SOMETHING) -> r -> Sigma (w' : World m' c'). (m' > m /\ SOMETHING)) -> World m' c' 14:36:11 is that I can't say SOMETHING 14:36:12 :) 14:36:18 heh 14:41:36 fax: http://pastie.org/878467.txt?key=babbgfpdokohtn3kjvzdnq 14:41:50 this is obviously wrong in some major way because I can't figure out how it isn't wrong 14:42:32 but I /think/ it's a totally pure, general, abstract constraint-based IO system 14:43:15 -!- pikhq has quit (Read error: Connection reset by peer). 14:43:28 this project - write hello in nance - turns out to be much harder than I ever imagined 14:44:32 fax: so how would /you/ do it :) 14:44:44 I don't do IO 14:45:21 just do pure programming in a monad then write a 10 line C/Haskell thing to drive it 14:46:31 nah the whole point of volit is to extract the program from the ... program 14:46:33 besides 14:46:36 safe io is very important 14:46:49 and i think being able to prove things about IOing programs is awesome 14:52:51 fax: what was that method you suggested for doing inductive data types? 14:53:01 ?? 14:56:12 fax: you said it yesterday 14:56:21 you axiomatise induction or something and then that gives you inductive types 14:59:05 I wish ais523 was here so I could ask him something. 15:00:02 fax: can you define coinductive data types with inductive ones? 15:00:58 I don't know 15:01:17 :| 15:01:20 u suk 15:05:22 nance foo.ne -o foo.prove && prove foo.prove && volit foo.ne -o foo.hs && ghc -O2 --make foo.hs -o foo 15:05:33 Hmm, I guess nance and volit have to share a library so they can process Nance code. 15:05:40 Although I could also have /another/ intermediate form: 15:06:44 nance foo.ne -o foo.ncr && ncr2prove foo.ncr && prove foo.ncr && volit foo.ncr -o foo.hs && ghc -O2 --make foo.hs -o foo 15:07:02 erm 15:07:11 nance foo.ne -o foo.ncr && ncr2prove foo.ncr -o foo.prv && prove foo.prv && volit foo.ncr -o foo.hs && ghc -O2 --make foo.hs -o foo 15:07:18 So ncr has enough information to distinguish things like Prop and Set easily, while prv is completely core. 15:11:21 So then to trust a Nance proof foo.ne, you have to trust that nance compiles it correctly to foo.ncr, then that ncr2prove compiles foo.ncr correctly to foo.prv, then prove checks it correctly. 15:11:38 As opposed to: to trust a Nance proof foo.ne, you have to trust that nance compiles it correctly to foo.prv, then that prove checks it correctly. 15:11:45 Prove checking it correctly is basically certain, so: 15:11:52 Trust nance & ncr2prv vs trust nance. 15:14:49 -!- pikhq has joined. 15:17:31 Hi pikhq. 15:28:39 pikhq: you there? 15:38:33 Answer: No 15:52:52 -!- atrapado has quit (Quit: Ex-Chat). 16:27:07 woo, I can use unetbootin to boot the ubuntu iso from an ntfs partition i think 16:46:28 -!- ais523 has joined. 16:50:05 Hi ais523! 16:50:10 Have you tried the 10.04 beta? 16:50:23 hi and no 16:50:26 http://1.2.3.9/bmi/news.softpedia.com/images/extra/LINUX/large/ubuntu10artwork-large_009.jpg ;; the theme is a bit pretty. 16:50:30 But it uses Yahoo! by default (?!) 16:50:39 and includes some social networking bullshit by default; sigh 16:50:42 alise: yahoo paid them more than google 16:50:47 but you can change it back easily enough 16:51:02 yes, but it exposes canonical a bit for the money-grabbing bastards they are :)) 16:51:23 I'm downloading 9.10 now just because I'd like some stability. 10.04? Maybe later. 16:51:28 When I have more bandwidth, perhaps. 16:52:46 Now if only they'd fix the subpixel rendering... 16:55:37 -!- alise_ has joined. 16:55:40 Fuck! Fuck! 16:55:43 Fucking Chrome! Shit! 16:56:00 My 3G connection dropped. Disconnected, reconnected - chrome portrays the ISO as downloaded - no resuming - fuck! 16:57:16 -!- alise has quit (Ping timeout: 256 seconds). 16:58:11 ais523: Punch me so I feel better 16:58:17 alise_: over HTTP? 16:58:27 umm, IRC? 16:58:29 Over IRC, surely 16:58:57 http://nctritech.files.wordpress.com/2008/11/tcpip_punch1.jpg 16:59:36 * alise_ ponders whether to redownload 9.10 or go for 10.04 16:59:40 alise_: I take it it didn't manage to download before the connection dropped? 16:59:49 ais523: not unless I suddenly got a 100 mbit connection 17:00:07 This is why you should use something that can resume when you're on an uncertain connection 17:00:13 (Or always, really) 17:00:16 Deewiant: I thought Chrome would be such a thing. 17:00:26 Think not; know. 17:01:01 -!- songhead95 has quit (Quit: songhead95). 17:01:13 it seems a bizzare feature for Chrome not to have 17:03:06 Deewiant: Then you will be tanasin? 17:03:09 *tanasinn 17:03:46 What does tanasinn have to do with anything :-P 17:04:11 10.04: Unstable lots of updates so network access and stuff... but nice themes and stuff, and, uh, ... 17:04:12 9.10: Yeah 17:04:25 Deewiant: "Don't think, feel. Then you will be tanasinn." 17:04:34 Right. 17:04:40 Screw "feel", just know. 17:04:49 Constructivist tanasinn. 17:04:55 :-P 17:05:48 ? : tanasinn 17:05:50 ? = feel 17:05:53 aww, stupid mirc 17:06:08 alise_: isn't 10.04 the version which puts the minimize/close/maximise buttons on the top-left of the window, in defiance of both fitts' law and common sense? 17:07:40 How does it defy Fitts's? 17:08:12 ais523: It doesn't defy Fitts', and OS X does it too 17:08:19 the close position sucks though 17:08:25 it's unfittsy there, I agree 17:08:27 alise_: the close position isn't in the corner, like it is on OS X 17:08:38 http://www.design-by-izo.com/2010/03/13/ubuntu-lucid-and-that-button-layout/ 17:08:41 also, it's very close to the menus, which has the effect of meaning you have to be more careful 17:08:55 http://www.design-by-izo.com/wp-content/uploads/2010/03/button-layout-kde.png seems like the best solution 17:09:01 it's the most fittsy of them all 17:09:52 alise_: oh, my close button's red already 17:09:55 I use the New Wave theme 17:10:00 at least, it turns red when you hover over it 17:10:06 -!- songhead95 has joined. 17:10:07 I wasn't talking about redness :P 17:10:12 and although it doesn't look like it stretches to the corner, it fdoes 17:10:14 alise_: no, but he was 17:10:21 ah 17:10:40 http://www.design-by-izo.com/wp-content/uploads/2010/03/button-layout-kde.png <-- this is a pretty kde theme, I wonder what it is 17:10:56 * alise_ just installs 9.10, I'm too lazy to do anything fancy 17:11:09 what's good for resumable windows downloads? 17:11:25 I think firefox does them, but it's a bit bloated 17:11:34 you could grab a Windows copy of wget, that would probably be ideal 17:11:37 just a downloader 17:11:51 http://1.2.3.11/bmi/www.jensroesner.de/wgetgui/wgetgui_simple.png 17:11:53 argh 17:11:58 http://www.jensroesner.de/wgetgui/wgetgui_simple.png 17:12:03 I regret googling "Windows wget ui" 17:12:39 oh, I'd say go for a command-line tool 17:12:59 also, http://1.2.3.11/ what? 17:13:07 stupid 3g broadband stick mangles all images :) 17:13:07 1.2.3.0/24 is reserved 17:13:09 (and webpages) 17:13:14 alise_: oh 17:13:22 (to add javascript so you can do shift-r/a to improve the quality of images) 17:13:26 haha, it's contributing to 1.2.3.0/24 pollution 17:13:34 you can send a certain header to stop it -- but I don't think Chrome can do that :)# 17:13:37 *:) 17:14:19 why doesn't it just use an IP in 10 or 192.168? 17:14:26 those would both be obvious choices, considering what it's doing 17:14:49 because idiots 17:15:13 ais523: The "obvious" reason for not using a private-area IP is to avoid conflicts for people who use those in their local networks, but I don't quite see how it'd apply for a 3G stick necessarily. 17:15:19 fizzie: yes 17:15:34 Don't forget 172.16/12 17:15:38 also, avoiding conflicts by using you're using an address that's specifically reserved for a different purpose, and hoping nobody else will use it either? 17:15:45 *by using 17:16:01 Deewiant: You could make some "172.16/12 - never forget!" T-shirts. 17:16:18 I could, yes 17:16:36 Deewiant: I was aware there was a /12 floating around somewhere for that purpose, but not its number 17:18:10 They have one block in each of the class A, B and C ranges, even though everything's so CIDRy nowadays. 17:19:29 Wow, there is not one shitty Windows download manager. 17:19:33 Guess I'll just use command-line wget. 17:20:36 alise_: http://www.oldversion.com/GetRight.html 17:21:19 That's was not is 17:21:39 Which is the least shitty version? :-) 17:22:03 I can't remember, to be honest 17:22:05 It's been years :-P 17:22:19 Presumably any of the ones that are there are non-shitty 17:23:10 Their official description is funny: "GetRight® is a download manager that simply improves and optimizes the files you download from the Internet." 17:23:14 Apparently 6.3 is the latest, and it has 6, so probably not 17:23:19 Not only does it download well, it even makes the content better. 17:23:22 4.5e; let's try that. 17:24:02 Wise Installation Wizard. 2002. A /bit/ too old. 17:25:32 hey, that even predates XP, somehow 17:25:42 still, I remember wise 17:25:49 more for the uninstall program, which was called unwise 17:25:52 * alise_ tries 1.3 17:25:55 -!- olsner_ has joined. 17:26:03 Really old is good; new is sometimes good. 17:26:08 In-between is shitty. Usually. For Windows. 17:26:16 --------------------------- 17:26:16 Unsupported 16-Bit Application 17:26:16 --------------------------- 17:26:16 The program or feature "\??\C:\Users\Elliott\Documents\Downloads\getright13.exe" cannot start or run due to incompatibity with 64-bit versions of Windows. Please contact the software vendor to ask if a 64-bit Windows compatible version is available. 17:26:16 --------------------------- 17:26:16 OK 17:26:17 --------------------------- 17:26:19 16-BIT?! 17:26:32 alise_: it was common back then, 32-bit programs were relatively unreliable on XP 17:26:44 I know, I always wrote 16-bit for XP because it had trouble getting 32-bit programs working correctly 17:26:47 what? 17:26:55 well, XP (before SP) and 98 17:27:00 alise_: 2002 is too old? I had probably stopped using getright by 2000 17:27:00 almost all XP programs are 32-bit. And this is really old, not XP era. 17:27:04 the issue being that half the APIs didn't work 17:27:12 Deewiant: Yeah, but Wise gives me AIDS. 17:27:14 So what do you use? 17:27:16 so you had to keep trying them more or less at random until you found one that did 17:27:22 (Yes, it gives me AIDS every single time I use it.) 17:27:34 alise_: I use a reliable Internet connection ;-) 17:27:44 Yeah, well, slight issues with that 17:28:03 1999 17:28:12 Let's try this 17:28:18 alise_: Opera probably has this stuff built in, FWIW. It tends to. 17:28:18 Let's party like it's. 17:28:22 isn't that before Windows really understood networking? 17:28:31 -!- songhead95 has quit (Quit: songhead95). 17:29:12 alise_: it was common back then, 32-bit programs were relatively unreliable on XP 17:29:14 *blink* 17:29:27 AnMaster: early versions, at least 17:29:32 ais523 is in a fantasy world of crazy 17:29:35 disregard him :) 17:29:36 ais523, that's rather hard to believe 17:29:39 hmm, either that, or it's just that my 32-bit compiler was rather unreliable 17:29:44 thinking about it, that seems a lot more plausible 17:29:47 I mean sure, for windows 95 or windows NT 4.0 17:29:48 That's probably a matter of definition; compared to 3.x, all the 9x releases have been pretty internet-savvy. I don't even think you needed a separate TCP/IP stack any more. (Or was it so that IE in 95 still had one?) 17:29:54 yes probably there it could happen 17:29:58 but XP... 17:30:13 fizzie: Certainly not in 98. Not sure about 95. 17:30:17 what is that "getright" btw? 17:30:27 Download manager. 17:30:30 mhm 17:30:35 what for? 17:30:41 Downloads? :-P 17:30:45 I mean, I never saw the point of them 17:30:55 what can they do that normal tools to download can't? 17:30:55 Deewiant: Does it do the impolite "open multiple connections to same server" thing by default?-) 17:30:57 resuming on failed connection 17:31:07 man this program is so uh... 1999 17:31:10 fizzie: I'm not sure. It might. 17:31:21 fizzie: I think the early versions didn't, at least. 17:31:28 alise_, is there no wget for windows? I'm pretty sure there was a non-cygwin port of wget 17:31:31 and wget has -c 17:31:33 to resume 17:31:52 -!- nooga has quit (Ping timeout: 240 seconds). 17:32:03 AnMaster: There is, but meh. 17:32:08 I'd prefer it automatically doing so when my connection breaks. 17:32:16 I should write a good download manager, except I won't be using Windows for much longer. 17:32:23 alise_, I'd prefer it to do when I regain connection instead ;P 17:32:29 AnMaster: Back in the day there might not have been; plus it's CLI, so a bit annoying for normal people, and thus it only handles one file at once. 17:32:30 Er, yes. 17:33:08 The interface for my download manager would be a list with filenames, progress meters, downladed/total, speed, estimated time and a cancel button to remove it from the list. Downloading would be dragging a URL to the window. 17:33:09 Deewiant, back in the day it would have been too slow to download more than one file at once 17:33:10 End of :P 17:33:22 your modem connection that is 17:33:31 well, is there a good GUI download manager even for Linux that isn't attached to a browser? 17:33:36 with zmodem you could chat /and/ download 17:33:37 alise_, like the firefox download list basically? 17:33:41 wget's an excellent /command-line/ download manager, but it isn't GUI 17:33:42 ais523: but why? linux browsers do it just fine :P 17:33:49 alise_: curiosity 17:33:49 I think firefox does do resuming 17:33:53 ais523: ooh, this links into an excellent idea I had for a GNOME UI feature 17:33:57 -!- nooga has joined. 17:33:57 ais523, pretty sure I saw a KDE one once 17:34:00 err 17:34:01 alise_, ^ 17:34:12 ais523: now you ask what it is 17:34:14 oh wait, it was ais523 who asked it in fact 17:34:17 -!- wIRC9 has joined. 17:34:17 AnMaster: Yes, which is exactly why you want a manager, so that you can queue dozens. 17:34:25 firefox queus 17:34:28 *queues 17:34:34 -!- wIRC9 has quit (Client Quit). 17:34:38 alise_, ais523: you have nicks starting on same char and of the same length 17:34:40 -_- 17:34:41 -!- songhead95 has joined. 17:34:42 please fix 17:34:46 ais523: ASK WHAT IT IS 17:34:48 AnMaster: no 17:34:51 AnMaster: your nick also starts with the same char 17:34:56 alise_: oh, what is it/ 17:34:58 Deewiant: I think it went so that plain 95 didn't include a TCP/IP stack, but they made one and distributed it with IE 2-or-so and the later 95 versions; and I think the IE dialler and stack also worked in 3.11 later on. There was also a version of Trumpet Winsock for 95. 17:34:58 and is of the same length if you pad it out! 17:35:06 ais523: I'll tell you in /msg, it's floody 17:35:07 I thought you wanted me to ask AnMaster what his KDE download manager was 17:35:10 ais523, it is of different case and nick of different length 17:35:17 ais523, I never tried it 17:35:22 AnMaster: IRC is case-insensitive 17:35:23 I just noticed that one existed 17:35:40 AnMaster: hey, I didn't ask, it was alise_ who didn't ask me to ask you! 17:35:43 ais523, well sure, but that isn't relevant to visually reading the nicks 17:35:49 Deewiant: I do remember that for a 3.11 user, the IE dialler was considerably more modern-looking than the (maybe not most current) version of Trumpet I had. 17:36:03 AnMaster: they're different colours in this client... 17:36:19 fizzie, trumpet? 17:36:44 ais523, I never liked that, most of the time it is even more confusing 17:36:49 AnMaster: Trumpet Winsock. 17:37:00 fizzie, a ppp program? 17:37:16 AnMaster: Yes, I think it could do PPP too; also SLIP. 17:37:21 heh 17:38:15 Also, I don't think you can chat and download simultaneously with (unmodified) ZMODEM, because I think the main "killer feature" of SMODEM was the chat thing. (And there was some competitors too.) 17:38:45 err 17:38:45 ok, smodem then 17:38:45 -!- alise_ has quit (Read error: Connection reset by peer). 17:38:57 wasn't smodem something used for BBS or such 17:39:02 SMODEM also does bidirectional transfers. 17:39:03 Yes. 17:39:04 rather than internet dialup 17:39:17 -!- alise_ has joined. 17:39:24 I'm not entirely sure this resume worked 17:39:33 http://en.wikipedia.org/wiki/File:SModem.png -- look, isn't it awesome! 17:39:39 oh fuck this shit, someone mail me an ubuntu cd 17:39:57 alise_, you could get them for free before iirc 17:40:01 not sure nowdays 17:41:17 yeah but it takes time 17:41:29 so does it for everyone else here too 17:41:29 -!- alise_ has quit (Read error: Connection reset by peer). 17:41:46 -!- alise_ has joined. 17:41:55 * alise_ tries wackget instead 17:43:17 Switch to the QNX Demo Disk, it's modern as anything, with a web browser and all, and yet you'd have to download just two floppies. 17:43:22 http://toastytech.com/guis/qnxdemo.html 17:43:30 You might have some problems with the 3G stick in it, though. 17:43:45 But there's the "QNX Is Cool!" demo! 17:43:50 -!- alise_ has quit (Read error: Connection reset by peer). 17:44:06 -!- alise has joined. 17:46:01 -!- alise has quit (Read error: Connection reset by peer). 17:46:37 -!- alise_ has joined. 17:47:17 That is one unreliable network. 17:48:28 -!- alise_ has quit (Read error: Connection reset by peer). 17:49:07 quite 17:49:46 -!- alise_ has joined. 17:49:48 fdgdfgdfgfdgdfg 17:50:08 afphhpfhffhpfphhnjgeul 17:53:00 -!- oerjan has joined. 17:53:24 -!- kar8nga has quit (Remote host closed the connection). 17:53:24 -!- alise_ has quit (Read error: Connection reset by peer). 17:53:42 -!- alise has joined. 17:54:59 -!- nooga has quit (Ping timeout: 260 seconds). 17:55:34 -!- alise has quit (Read error: Connection reset by peer). 17:55:51 -!- alise has joined. 17:57:49 -!- alise has quit (Read error: Connection reset by peer). 17:58:07 -!- alise has joined. 18:02:52 -!- alise has quit (Ping timeout: 276 seconds). 18:03:26 -!- songhead95 has quit (Quit: songhead95). 18:04:27 -!- alise has joined. 18:04:28 Anyone remember optbot? :) 18:04:37 yes, vaguely 18:04:40 although I can't remember what it did 18:04:56 repeated random lines from history 18:05:06 i remember it was named for me 18:05:09 yes 18:05:17 well, also AnMaster 18:05:23 AnMaster said otpbot for the erlang thing 18:05:27 opt was like 18:05:34 Oerjan's Puns Terrible or something 18:05:41 no it was Oerjan's Terrible Puns 18:05:43 that was it 18:05:45 but I kept typoing opt 18:05:47 for otp 18:05:48 so i made it opt 18:06:06 very optional 18:06:29 fungot can also repeat random lines from history, it just gets a bit confused sometimes. 18:06:32 fizzie: the question of rendered fat, the commission will clearly seek every available means to escape the current legal framework, mr president, and what we are intending to use its relationships with european partners, the non-governmental organizations which, in the coming months, the forwarding of appropriations to implement the legislation and practice. however, we must support all initiatives that aim at strengthening our 18:06:45 Oh, someone's been doing politics again. 18:07:19 16:24:03 ehird, caller() { local myvar; callee "myvar" "other arguments"; } callee() { printf -v "$1" "%s" "$2"; } 18:07:24 aieeeee 18:07:29 Bot-tweet: "About NetHack: hacking: the chamber was of a retreating nymph. 'saruman!' he cried, and treasure it as though it were a piece of v-shaped..." 18:07:34 AnMaster: can you eval in the caller's scope? 18:08:17 local is dynamically scoped, not static, if that's perl 18:08:32 (proper static is "my" iirc) 18:08:44 That doesn't look like perl; there's no sub, and no sigil for the var. 18:09:01 hm true 18:09:23 But you can eval code in the caller's scope in MATLAB, too: evalin('caller', 'x = 42'); is a rather impolite thing to do. 18:09:44 can't you do geometry on rationals? 18:09:52 no, you need square roots 18:10:11 Or even evalin('base', 'x = 42'); if you want it to be evaluated directly in the workspace of the user's session. 18:10:25 in Perl, you can't exactly eval in the caller's scope 18:10:27 the constructible numbers it's the smallest field closed under square roots 18:10:29 *is 18:10:38 but you can take the caller's local/lexical variables from the symbol table and modify them that way 18:10:58 (well, field of reals) 18:11:19 fizzie: Why would one ever want to use this? :-P 18:11:47 Deewiant: You can use it to forcibly return values, even if the caller doesn't want you to. :p 18:12:08 Well yes, you can use it to be obnoxious 18:12:09 Deewiant: There's also a curious restriction: "evalin cannot be used recursively to evaluate an expression. For example, a sequence of the form evalin('caller', 'evalin(''caller'', ''x'')') doesn't work." 18:12:10 it's bash not perl 18:12:14 eqaw4235s6etf987yg-p09uh-o]=p 18:12:39 AnMaster: can you eval in the caller's scope? <-- that is bash, but well I think I described it at the time I mentioned it 18:12:40 [#324qw56e7ri8ulp9jo[0j['0oi;pj0l98hyngtfrxeadwq4rs6hu8,ghp0oi[;0,l98gu7y6tfry5d6t4esrw3aqe4st6p0o'l[0ogy6utfd65eswra432qstdey6p[0o'0j98sw5y6gtik09y6tr4eswgr4sw6tr4efwas4uy60pytfresar6y6tr4fesw646ir4fe3r4y6eaw87tr4ef 18:12:41 Deewiant: There's also assignin() if you want to stick a value into the caller's workspace without having to turn it into a string like that. 18:12:48 but eval 18:12:50 not sure 18:13:11 fizzie: Awfully handy, I suppose 18:13:49 Deewiant: The examples do look a bit contrived. 18:13:51 alise, anyway, why aieeee? You saw it before 18:14:15 Deewiant: "The assignin function is particularly useful for these tasks: Exporting data from a function to the MATLAB workspace. Within a function, changing the value of a variable that is defined in the workspace of the caller function (such as a variable in the function argument list)." 18:14:25 in INTERCAL, you can assign variables in the caller's scope by temporarily ending scope for that variable, then resuming it again 18:14:33 scopes in INTERCAL don't actually have to be well-nested 18:14:34 Deewiant: I guess the latter part makes it a sort of a pass-by-reference mechanism. 18:15:06 Deewiant: You can do value = evalin('caller', varname) to "dereference" the "pointer", and then assignin('caller', varname, value) to set it. 18:15:26 fizzie: Contrived, yes. :-) 18:15:51 I think I prefer the INTERCAL method 18:16:07 Deewiant: Well, MATLAB's completely pass-by-value, as far as I remember, so if you want to do that sort of stuff... 18:16:45 (There's a copy-on-write thing if you pass in a large matrix.) 18:16:51 alise, as for eval in caller's scope, define what that actually would mean in terms of bash scoping please 18:17:04 pass-by-singular-reference 18:17:09 I can't figure out how the question makes sense in bash's model 18:17:12 all equal values have the same reference; passing a value passes this reference 18:17:18 mutating it mutates it in all places 18:17:53 f(x) = {x += 1}; y = 2+1; f(3); print(y) --> 4 18:18:15 alise, everything will be resolved to the first scope that has it 18:19:06 the only thing for which eval in local scope would differ from eval in own scope would be: a) making new local variables in caller b) in case of your own local variables shadowing the caller's 18:19:18 I think the answer to those is: "no you can't do that" 18:19:42 aww, why not? 18:20:04 anyone remember my language where you could goto /anywhere/? :) 18:20:09 yes, I do 18:20:09 it was beautiful 18:20:15 BASIC? 18:20:16 it was, but rather too similar to INTERCAL 18:20:23 Deewiant: no, it was structured that's the beauty 18:20:25 Deewiant: no, you could goto, say, the inside of an expression 18:20:31 returns were jumping to the right place in your caller 18:20:36 you could jump into the middle of a loop and it'd work fine 18:20:37 etc 18:20:38 actually, you can do that in Overload too 18:20:42 Asm, then ;-) 18:20:43 ais523: I wasn't sure about expressions 18:20:44 only Overload is a mess that I've abandoned 18:20:45 -!- myndzi has quit (Read error: Connection reset by peer). 18:20:46 but any statement, certainly 18:20:52 executing a pointer took you to wherever the pointer was pointing 18:21:03 fixing the callstack after that was your responsibility 18:21:05 (it used CPS) 18:21:10 (so there wasn't really a callstack) 18:21:13 aww, why not? <-- I can't think of a way to do theose 18:21:14 those* 18:21:15 that's why 18:21:16 well 18:21:17 -!- myndzi has joined. 18:21:23 if someone else know a way, please tell 18:21:24 hey, I invented CPS without realising it 18:21:37 /just now/ I have realised that Overload is CPS 18:21:43 and it's been like that for years 18:22:11 mhm 18:23:11 anyway I just realised that 16:24:03 ehird, caller() { local myvar; callee "myvar" "other arguments"; } callee() { printf -v "$1" "%s" "$2"; } 18:23:13 would break 18:23:23 if the callee had it's own local variable "myvar" defined 18:23:27 before that printf -v 18:23:55 so to ensure a roubust program, local variables should be prefixed with some sort of namespacy thingy 18:23:59 maybe like: 18:24:14 lcl__ 18:24:17 XD 18:24:35 Deewiant: Hey, the only usage example for evalin is "This example extracts the value of the variable var in the MATLAB base workspace and captures the value in the local variable v: v = evalin('base', 'var');" It doesn't really help in understanding why you'd want to use it. 18:25:49 -!- songhead95 has joined. 18:26:28 fizzie, the reason for using this sort of thing in bash 18:26:36 is that you can only return an unsigned byte 18:26:41 from functions 18:26:45 that is, an exit code 18:27:08 which means you *have* to do this way to return anything more complex 18:27:18 It's silly that way. Matlab lets you return an arbitrary number of return values, and in any case those return values can be arbitrary data structures. 18:27:23 or use some global "return_value" variable 18:27:31 but that seems even more error prone 18:28:00 fizzie, also for bash this is just a side effect of the scoping rules 18:28:05 printf -v is just "print to variable name" 18:28:14 because indirect assignment requires that or eval 18:28:34 you can't do foo=quux; $foo=bar and get bar into quux 18:29:10 for the other way around, reading a variable from the variable name you get passed as a variable there is special syntax 18:29:14 I guess in MATLAB you'd be most likely to use this as a some sort of a debugging aid; sticking an "assignin('base', 'temp', confusing_expression);" somewhere means that after executing it, you'll have the value inspectable in the session. 18:29:49 foo=bar; myvariable=foo; echo ${!myvariable} would echo bar I think 18:29:53 unless I confused the syntax 18:29:58 might have been something else than ! there 18:30:20 fizzie, does matlab have a debugger though? 18:31:04 bash 4 has associative arrays, but I "emulated" that before in bash 3.x 18:31:12 really messy 18:32:49 STUPID FUCKING PIECE OF 18:32:50 ARGH 18:32:58 alise, ? 18:33:06 fizzie, hm does C++ have anything to mess up the scoping? 18:33:35 if not, that might one of the very few sane parts of C++... (C has quite sane scoping IMO) 18:33:41 AnMaster: probably, C++ can mess up /anything/ 18:34:28 well, C99 does something strange for inline without static iirc 18:34:42 in particular extern inline, which might be a GNU extension 18:35:42 istr there was a gnu extension, and then C99 invented something with the same syntax but a different meaning 18:36:09 istr? 18:36:16 olsner, and yes that sounds familiar 18:36:27 I seem to recall 18:36:34 ah 18:36:36 afdnkjsdfn\jkfkjsdaghsdkfghjsdkjfghskjdfghdafsgdfg 18:36:39 this fucking 3g stick piece of crap 18:36:53 alise, calm down, it won't become better because you are angry at it 18:37:09 alternatively: channel your rage, and insert a really bad star wars joke 18:37:37 i've been trying to download this file for .... like three hours 18:37:42 first time almost done cut off 18:37:50 then my connection broke while trying to find ONE download manager that works 18:37:50 alise, so resume 18:37:53 wget -c would work 18:37:55 now it's just cutting off randomly after 30 seconds or so 18:37:59 Boba fet voice: kbytes will do fine 18:38:00 AnMaster: BUT NONE OF THIS SHIT IS WORKING YOU IDIOT >_< 18:38:05 alise: How big is the file? 18:38:09 alise, well on the original file 18:38:20 There is some sort of "he has no patience" starwars joke to be made here. 18:38:34 Deewiant: 600 megabytes or therewithin 18:38:36 i had to go with the "Credits will do fine" 18:38:38 joke 18:38:41 d you have to use -c the first time to use -c later? 18:38:47 not that it matters 18:38:52 6 kb/sec, wonderful 18:38:54 fizzie, that too, but I was going for the "try to convert to dark side" 18:39:05 6 kb/sec is a rather respectable modem speed. 18:39:16 ais523: ok, this will be quicker: I'm coming to Birmingham; have an Ubuntu 9.10 USB stick ready when I arrive 18:39:17 what fizzie said 18:39:19 I seem to recall some sort of "a megabyte per hour" rule of thumb. 18:39:20 sudo apt-get install sith 18:39:24 he stole my joke 18:39:32 alise: USB stick's ready already 18:39:38 and are you /serious/? 18:39:44 alise: 600 megabytes would take you several days with a modem connection; I wouldn't worry about a few hours 18:39:55 ais523: hmm... let me ask google maps 18:40:20 -!- songhead95 has quit (Quit: songhead95). 18:41:00 ais523: hmm... on public transport it'd take me anywhere between 7 and 10 hours 18:41:10 by car, only 3.5 hours 18:41:21 quick, use quantum mechanics to transfer a car here 18:41:37 seems implausible 18:41:42 do you need -c to resume later? 18:41:45 or does it work anyway 18:41:47 say it works anyway 18:41:48 please 18:42:02 You don't need -c at the first invocation, if that's what you mean. 18:42:07 Only later when you're trying to resume. 18:42:12 good because it just broke 18:42:15 now what's the thing again to resume 18:42:34 alise, wget -c foo 18:42:40 foo is url or filename 18:42:45 alise, url 18:43:01 yay 18:43:05 now let's hope it actually resumes 18:43:05 without -c wget will start downloading to .1 18:43:06 instead 18:43:23 alise, and lets hope there is no data corruption 18:43:33 no it will not resume 18:43:45 alise, I remember downloading an iso (arch or ubuntu iirc) and the data was corrupted near the start 18:43:52 since then I use bittorrent for linux iso downloads 18:43:58 much more reliable 18:44:02 fine 18:44:03 fine 18:44:04 fine 18:44:15 alise, it should resume 18:44:19 strange if it doesn't 18:44:39 alise: I don't remember where you live, but walking from Hexham (which I think was at least nearby at some point) to where I live would take you just 5 days, 13 hours. (It involves some 371 steps; you take the Newcastle-Ijmuiden-Amsterdam ferry to Netherlands, then the Hoek van Holland-Harwich ferry back to UK, then the Harwich-Esbjerg ferry to Denmark; then you just walk across Denmark (a hundred miles or so), take another ferry to Rostock, and from there to H 18:44:39 elsinki, Finland. 18:44:40 alise, does the server support not starting at the start? 18:44:54 Only 371 steps? 18:44:58 Impressive. 18:45:00 "would take you just 5 days, 13 hours. (It involves some 371 steps;" 18:45:01 I assume you mean footsteps. 18:45:04 hah 18:45:06 alise, yeah same 18:45:15 Yes, with large enough boots. 18:45:35 ...Also, why on earth would you go back to the UK? :D 18:45:49 alise: Because Google Maps says so! 18:46:26 so... UK->NL->UK->DK->FI? 18:46:38 AnMaster: You forgot Germany there. (Rostock's in Germany.) 18:46:39 which seems on crack 18:46:42 fizzie, oh 18:47:02 fizzie, not over Sweden? He is missing out on stuff then 18:47:31 AnMaster: Presumably it's because walking is so slow; it's good to find routes where you don't have much walking between ferry stops. 18:48:08 mhm 18:49:26 AnMaster: http://zem.fi/~fis/alise_walkabout.png 18:49:51 That's a funny-looking loop near the Netherlands. 18:50:39 Deewiant: I asked it for walking directions from Copenhagen to Amsterdam (our summer trip goes thereby); it gave me this really silly denmark-norway-denmark-norway-UK-holland thing. 18:50:42 fizzie, if it takes ferries, why not also take trains? 18:51:16 AnMaster: Walking directions are in beta, you see. 18:51:27 hah 18:51:42 fizzie: Walking directions might not be the best idea :-P 18:51:48 i suppose it includes ferries because sometimes you cannot avoid them, while you could always walk along the train tracks... 18:52:02 yay bittorrent download is going fast 18:52:02 Deewiant, try walking directions from new york to somewhere in Europe 18:52:11 No, I'd rather not 18:52:17 AnMaster: They removed the "swim over atlantic ocean" thing, I think. 18:52:18 no not performing it 18:52:36 fizzie, did that actually happen in it once?! 18:53:04 We could not calculate directions between new york and helsinki. 18:53:09 AnMaster: yes :) 18:53:13 wonderful 18:53:21 AnMaster: See e.g. http://www.ghacks.net/2007/04/11/google-maps-swim-across-the-atlantic-ocean/ 18:53:48 doesn't do helsinki to moscow anyway :( 18:53:50 *either 18:53:53 The car-directions hexham->helsinki make more sense 18:54:06 Walking directions to Helsinki, Finland 18:54:07 0.0 mi 18:54:07 18:54:07 Helsinki 18:54:07 Finland 18:54:07 AnMaster: It still has "Kayak across the Pacific Ocean" as a possibility. 18:54:07 1.Head east toward Simonkatu 18:54:07 0.0 mi 18:54:08 18:54:08 Helsinki 18:54:09 Finland 18:54:18 AnMaster: If you ask for "new york to sydney", for example. 18:54:28 fizzie, what? 18:54:36 fizzie, is that an easteregg then? 18:54:47 I mean, it seems unlikely to be due to an oversight 18:55:04 you don't say <_< 18:55:14 AnMaster: Most likely. It's given for the "by car" directions, anyway, and I'm not sure how you're meant to take the car with you in the kayak. 18:55:26 That's one pretty big kayak. 18:56:34 57. Take the 1st left onto Kalakaua Ave 1.9 mi 18:56:34 58. Kayak across the Pacific Ocean 18:56:34 Entering Japan 3,879 mi 18:56:34 59. Turn right toward 県道263号線 0.3 mi 18:56:35 clearly what you want is a large kon-tiki style raft big enough for a car 18:56:37 fizzie, I get it for walking between New York and Hawaii 18:56:40 753.Kayak across the Pacific Ocean 18:56:40 Entering Hawaii 18:56:41 .At the roundabout, take the 1st exit onto W Denton Way 18:56:41 Go through 1 roundabout 18:56:44 These are for the walking directions 18:56:46 o_o 18:57:05 alise: It should have a "Dodge the car's like it's Frogger!" written-in-red comment there. :p 18:57:10 Gah, "cars". 18:57:33 alise, could it be that there are sidewalks? 18:57:58 "Go THROUGH 1 roundabout" 18:58:32 Clearly Google has a psychotic AI running that. 18:59:01 Deewiant: Anyway, I asked for walking directions because the only other alternative was "by car", and we're not going to have/rent one; it doesn't do trains. (Was there some sort of limited-region public transportation thing already?) 18:59:25 http://maps.google.com/maps?f=d&source=s_d&saddr=hexham&daddr=helsinki+to:brussels&hl=en&geocode=&mra=ls&dirflg=w&sll=-5.52475,179.448463&sspn=74.498813,114.433594&ie=UTF8&ll=48.806863,8.481445&spn=13.289494,28.608398&z=5 18:59:33 Hexham, Helsinki, Brussels. 18:59:41 fizzie: You can always hitchhike. 18:59:48 It does public transport now, yes. 18:59:52 fizzie: You should have visited me. 18:59:55 to go from stockholm to london by walking 19:00:01 it tells me to visit riga on the way 19:00:24 the route is even crazier for Stockholm to Manchester 19:00:31 Deewiant: In retrospect, the "by car" instructions worked better for my "I just want some sort of time estimate for the train routes" use anyway. 19:00:40 fizzie: Yep 19:00:51 also it seems to be non-deterministic 19:01:00 I get different results when I retry the same search 19:01:16 fizzie: where are you trying to get to? 19:01:26 -!- oerjan has quit (Quit: Later). 19:01:39 pineapple: Nowhere at the moment, we have the routes all planned up already. I was just wondering back then. 19:02:50 Deewiant: It's a bit sad that I could find no sensible train routing system that'd export me a .gpx file. I toyed a bit with OpenStreetMap editors, but it seemed non-trivial to extract long-distance train route geodata from that either, since the tracks aren't very comprehensively grouped into sets, just partially-somewhere-a-bit. 19:03:35 Deewiant: In the end I just took a generic .gpx editor thing that could display openstreetmap layers, and added some manual polylines over the railway lines that we're going to take. (I wanted a map of our route to show to relatives.) 19:03:38 I might be able to sympathize if I knew what a .gpx was, but I guess it's some standard format for that. 19:04:00 Deewiant: It's a bit like Google's KML; a XML format for tracks, waypoints and such. 19:04:01 Stockholm-Rostock by walking takes you through first Tallinn then Helsinki 19:05:33 AnMaster: I'm not sure how comprehensive their ferry schedules are. They might not include those cruise-line corporations, even though those have those "route trip" style tickets in addition to the cruises. 19:05:52 mhm 19:05:52 AnMaster: Certainly you can get directly from Stockholm to Helsinki, at the very least; most likely from Stockholm to Rostock too. 19:06:03 fizzie, probably going by Åland 19:06:14 due to the tax free reasons 19:08:14 You are not able to access this service because Content Control is in place. 19:08:15 If you're 18 years or over, you can remove Content Control by contacting your mobile service provider's customer support 19:08:15 team. 19:08:15 fucking piece of shit 19:08:28 alise, what service? 19:08:37 vodafuckingfone 19:08:46 alise, no, I mean the blocked one 19:08:49 tmobile do the same but i unlocked it on that one but that one is all flutty right nw so i'm using this one 19:08:50 imgur 19:08:53 as is all other image hosts 19:09:01 this stick is PAID FOR 19:09:08 mhm 19:09:09 you have no right to fuck with the data I'M paying for, nanny 19:09:12 jesus 19:09:22 AnMaster: On the other hand, I 'm not sure you people need those ferries very much; you can just take one of those fancy-schmancy X2000 trains from Stockholm to Copenhagen, then another train from there to anywhere in Germany you'd like; that's what we're going to do, anyway. 19:09:42 fizzie, mhm. X2000 aren't really fancy 19:09:52 relatively slow compared to TGV and so on 19:09:53 alise: Is pixlr.com blocked? 19:09:53 AnMaster: With that sort of name, it almost has to be. 19:10:03 alise: If not, you can use that 19:10:04 fizzie, you never went on X2000 before? 19:10:20 http://upurs.us/image/11623.jpeg 19:10:22 AnMaster: I haven't been going round Sweden much. 19:10:22 A jpeg but who cares 19:10:25 fizzie, they are tilting trains though, might feel a bit strange when taking curves thus 19:10:35 You can almost ignore the bloat behind the screen. 19:10:51 alise, that is able to resume downloads easily enough 19:10:51 AnMaster: Yes, I think they're not much different from the local Pendolino ones. 19:11:12 Of course, I like BitTorrent. 19:11:17 But uTorrent is normally a lot less simple than that. 19:11:19 AnMaster: (Except that ours break down all the time.) 19:11:30 fizzie, so do ours sometimes 19:11:38 fizzie, like last autumn or such 19:11:47 AnMaster: Example: http://blog.consultmirror.com/wp-content/uploads/2008/10/utorrent-general-view.png 19:11:50 they had to take almost all out of service to replace the wheels 19:11:55 due to some construction issue 19:11:57 "The Finnish Pendolinos have received a lot of bad publicity in Finland for their serious reliability issues, mostly caused by technical problems with their tilting system and couplers. The train did not manage to cope with the severe winter conditions." 19:12:23 alise, I prefer that view :P 19:12:44 AnMaster: Madman. 19:12:49 alise, why? 19:13:06 It is fluff with no purpose; statistics pon for people with no IRC to waste time on. 19:13:07 *porn 19:13:20 heh 19:14:32 ehirdOS would be fine here because it would be less than 690 megabytes. 19:14:51 alise: Did you miss my QNX demo disk suggestion?-) 19:14:56 fizzie: No. :P 19:15:07 Eh, just use debug.com. 19:15:23 alise: The "QNX is Cool!" demo! How could you resist! 19:15:33 AnMaster: Lateral thinking puzzle: You have no optical drive, no USB sticks, no floppies, no storage media whatsoever. You have a hard drive, Windows and the interwebs. How do you boot the Ubuntu LiveCD to install it to the spare partition you have? 19:15:42 I worked it out. :P 19:16:20 alise, you use wubi? 19:16:40 Wubi installs to a file in an NTFS partition, and does not boot the LiveCD. 19:16:45 hrrm 19:16:50 (Yes, it literally /puts a Linux partition in a file on an NTFS partition/.) 19:16:52 (Awful.) 19:17:05 alise, well do that but to the installer instead 19:17:16 then load the whole thing into ram (hope it fits!) 19:17:23 and work from there 19:17:26 you have one go 19:17:27 No, what you said makes no sense. 19:17:29 you can't mess it up 19:17:30 Try again. 19:17:41 alise, well, repartition and put the thing there 19:17:47 then boot that 19:18:03 How? You only have NTDLR. 19:18:14 It doesn't get Linux. 19:18:15 alise, well you can chainload with ntdlr 19:18:15 It can't boot Linux. 19:18:22 so yes it is possible 19:18:25 How? 19:18:26 in fact I have done it 19:18:28 You only have Windows. 19:18:32 No LiveCD or anything to set this up. 19:18:38 You're on completely the wrong track. 19:18:40 Hmmm... Install a boot disk image that can read ISOs off of NTFS filesystems, chainload it from NTLDR, and have that boot into the LiveCD. 19:18:41 alise, topology linux works kind of like wubi does 19:18:46 it makes ntldr load grub 19:18:54 to then boot linux 19:19:01 I tried it many many years ago 19:19:17 pikhq, that might work too 19:19:18 I'll just tell you. 19:19:22 sure 19:19:24 I have done the "Linux in ntldr boot menu" thing too; it involves just extracting a 512-byte boot sector into file, and adding one line to boot.ini; or at least that's the way it worked with win2k. 19:19:35 fizzie, something like that yes 19:19:42 I was thinking you'd just run the installer in a VM, with the spare partition direct-mounted, but that doesn't solve the booting thing really, I guess. 19:19:42 Use http://unetbootin.sourceforge.net/. It fucks with NTDLR to boot Linux from an NTFS partition (part of one that is not a whole one) prepared from the .iso you want. 19:19:51 You then use this to install Ubuntu, then reboot Windows; it will undo the changes. 19:20:17 Also, I've never heard of topology linux. 19:20:21 Google shows nothing. 19:20:26 alise, ever heard of colinux? 19:20:54 alise, I guess topology linux is dead then 19:20:56 It was a Slackware-based distro that installed onto an NTFS partition, could boot either onto the straight system or via coLinux. 19:21:04 pikhq, ah yes you heard of it then 19:21:06 Been ages since I've seen it, though. 19:21:34 I seem to recall there was a Slackware installation method which puts the linux system in a FAT filesystem, not in a single file; all files are different FAT files, and there's one huge hidden metadata file to keep ownership and inode and real-filename information in. 19:21:45 And of course loadlin; I used to use loadlin to boot my first Slackware. 19:21:51 heh 19:21:55 (With an entry in a dos 6.22 boot menu to directly invoke loadlin.) 19:22:03 I suppose loadlin's no-go in modern Windowses. 19:22:14 fizzie: Yeah, DragonLinux IIRC... 19:22:16 alise, anyway I think it is likely your way will fuck up the system so you can't recover from it 19:22:27 UMSDOS is no longer maintained, so that doesn't work. ;) 19:22:42 Ah, yes, "umsdos" was the name. 19:22:42 AnMaster: why, because you say so? It is a supported method of install 19:22:47 alise, hrrm 19:22:52 I was just googling for "udos", so that was pretty close. 19:22:58 alise, what happens if the install fails when the disk is partly overwritten 19:23:30 AnMaster: Uh... you install onto a different partition. 19:23:38 alise, how do you make the partition then? 19:23:42 I mean 19:23:53 normal windows system is one huge partition 19:24:03 Yes, but this is already partitioned into two, conveniently. 19:24:12 alise, ah that helps a lot indeed 19:24:19 AnMaster: The original problem statement did involve "the spare partition you have". 19:24:26 fizzie, must have missed that 19:25:39 You can use partitionmagic to repartition anyway, if you're feeling lucky 19:25:49 Deewiant, when running from the same system!? 19:26:09 Yes, I think it can install something to do it at boot 19:26:16 ah plausible 19:26:30 would be replacing autochk entry I presume, like those "defrag on boot" tools do 19:26:31 It isn't from the same system 19:26:32 It reboots the system 19:26:41 and uses the tinkered bootloader to run the on-NTFS Linux 19:26:45 alise, we were talking about repartitioning 19:27:01 PartitionMagic does (or did, anyway) that, yes; you queue the actions, it asks you to reboot, at boot-time it does the magic. 19:27:16 fizzie, plausible but scary. 19:27:16 AnMaster: so do it from inside the ubuntu livecd 19:27:45 alise, I wouldn't like that, if the file for the livecd image had to be moved 19:27:56 AnMaster: What would be scary would be to use some sort of alpha-quality parted NTFS resize patch. (I'm not sure if there is one yet, but I'm sure there will be at some point.) 19:28:18 fizzie, you can use gparted to resize ntfs 19:28:20 works fine 19:28:33 but I wouldn't want parted running from the partition (or even disk) being resized 19:28:36 Oh? http://www.gnu.org/software/parted/features.shtml was lying to me, then. 19:28:46 fizzie, gparted invokes ntfsresize then parted 19:29:06 fizzie, so it doesn't let parted do the whole work 19:29:23 fizzie, gparted is in fact more than just a GUI frontend to parted 19:29:50 AnMaster: just dont run anything new 19:29:52 *don't 19:29:54 and it won't need to touch the disk 19:29:55 :D 19:30:08 alise, well, unlikely, any data moving will push things out of disk cache 19:30:18 due to the large amounts of data being moved 19:30:22 it loads into ram 19:30:26 maybe unetbootin copies everything to ram anyway 19:30:29 alise, so if I did it, I would do it from a ram disk indeed 19:30:30 for overwriting windows 19:30:58 alise, and what if the install failed if you *are* overwriting linux. Yeah you are into deep problems, that's my point 19:31:45 *overwriting windows 19:31:51 Then you green. 19:31:56 hrrm 19:32:07 yeah overwriting windows 19:32:08 still 19:32:21 it is easy to end up with an unbootable system and no usb drive or cd to recover it from 19:32:26 Windows 7 isn't too bad. 19:32:31 Ubuntu is nicer though. 19:35:01 alise, are you going to dual boot? 19:36:55 Yes, just in case. 19:37:03 And for lessriskiness of installation. 19:37:52 true 19:38:05 alise, how big is the disk? 19:40:38 690 mb 19:41:51 why? 19:45:11 . 19:46:36 So slow. 19:52:14 alise, err? 19:52:20 690 mb harddrive!? 19:52:46 surely you are joking 19:53:13 Netbook. 19:53:31 pikhq, even so, 690 mb. would be extreme 19:53:38 you expect 10 gb at least 19:53:53 oh 19:53:53 you didn't mean the iso 19:54:02 alise, indeed 19:54:04 no 2gb for netbooks 19:54:04 to 4gb 19:54:04 is the minimum 19:54:14 alise, says who? microsoft? 19:54:15 (minimum, note) 19:54:35 alise, so how large is your harddrive/SSD 19:54:36 it's just the minimum you see 19:54:43 e.g. the dell mini 9 comes with that by default, iirc 19:54:43 it's a 250gb hd divided in two partitions, anyway 19:54:47 WINDOWS and Data, which has hard drive recovery stuff by default 19:54:51 it's a hard drive not an ssd 19:54:59 it cost 497, not 1,500 :-) 19:55:29 -!- Gracenotes has quit (Ping timeout: 246 seconds). 19:55:35 5350 kr 19:55:40 you swedetard 19:57:39 "swedetard" 19:57:40 Wow. 19:59:38 Yes. 19:59:39 alise: Could you put that in real money? 20:00:24 Yes; sec. 20:01:05 9547252537776.06 ZW$ 20:01:16 Hmm, that may be the pre-reset Zimbabwean dollar. 20:01:30 That's a few orders of magnitude too small. 20:01:43 Then it's the post-reset one. 20:01:50 (Where $1 became old $1bn) 20:01:57 $746, anyway 20:02:03 (US) 20:02:11 the use of the dollar as an official currency was effectively abandoned on 12 April 2009 as a result of the Reserve Bank of Zimbabwe legalising the use of foreign currencies for transactions in January 2009 20:02:13 -!- cheater2 has quit (Read error: Connection reset by peer). 20:02:16 meh 20:02:26 The USD isn't real currency. I was just mocking your country's lack of Euroness. 20:03:17 Wait, it was $10bn. 20:03:25 Yeah; Sweden needs to get on the Euro bandwagon. 20:03:29 What, you meant USD?!?!?!?! 20:03:46 erm 20:03:50 What, you meant UK?!?!?!?! 20:04:02 Yes. 20:04:14 *the UK 20:04:33 Maybe I'll go to Norway, they have the Euro :P 20:04:39 Heheh. 20:04:59 -!- cheater2 has joined. 20:05:28 But they also have... shudder.. Lutefisk. 20:09:09 Yes, they have caustic food. 20:09:37 Shudder. 20:11:15 * alise notes that there don't seem to be any pirate copies of mathematica for linux on the tubes 20:11:29 Well, none of 7 anyway. 20:11:34 -!- cheater2 has quit (Ping timeout: 264 seconds). 20:12:25 You just haven't found them. 20:13:49 Rule 34.5. 20:13:51 :P 20:13:56 Mathematica porn! 20:16:43 Admittedly I don't have access to any actually decent torrent trackers. 20:16:53 Mathematica 5 2 Win Linux Mac software other operating systems applications windows 20:16:55 5.2; wonderful. 20:17:47 >200kb download speed! 20:17:51 On a 3G stick! 20:17:52 Woot! 20:18:19 And back down again :P 20:19:15 alise: Are you Google-deficient? "mathematica 7 linux torrent", top link. 20:20:38 I've never before had success using Google to find torrents. 20:21:03 Incidentally, Mathematica on OS X expands to a 4GB .app :x 20:21:06 when installed 20:22:07 I just got back and read the line: " Mathematica porn!" 20:22:13 I nearly puked 20:22:16 :P 20:23:02 alise, tpb has mathematica 7 for linux iirc 20:23:21 by pure coincidence, so have I 20:23:30 *completely* unrelated of course 20:23:45 :-P 20:24:23 -!- cheater2 has joined. 20:26:11 Does it have any Linux-related shittiness? 20:26:19 alise why the fuck would you steal mathematica 20:26:33 Oh no, not an idiotic copyright defender. 20:26:38 fuck you 20:26:40 you're the idiot 20:26:53 Firstly, copyright infringement is - apart from being an uncrime invented by idiots - not theft even if you support it. 20:27:00 Economically, nonsense. Morally, nonsense. 20:27:07 firsly: shut up, you're an idiot 20:27:20 I like how you both called each other idiots without even knowing what you were actually going to say 20:27:20 If you continue calling me an idiot without basis I will simply put you on /ignore. 20:27:40 good then you might stop telling me I suck 20:27:53 Deewiant: Well, I know he's a Wolfram fanboy and calling copyright infringement stealing along with the brash wording of "why the fuck would you steal mathematica" gave me a pretty good predictor 20:28:03 fax: I haven't done that but if you want to distort something I've said that way I won't stop you 20:28:19 alise, you're such an idiot you can't even remember something that happened this morning 20:29:43 just grepped the logs, I never said you sucked 20:30:07 okay well you could also learn to spell 20:30:32 07:00:58 I don't know 20:30:32 07:01:17 :| 20:30:32 07:01:20 u suk 20:30:36 what? 20:30:50 5.5 hours ago 20:31:01 and it's rude to be all impatient like "I'm waiting" while someones trying to think 20:31:23 wow you're pissed off because I wasn't being totally serious all the time? 20:31:30 it's not like I didn't gratuitously adorn things with emoticons either 20:31:32 -!- Slereah has quit (Ping timeout: 246 seconds). 20:31:37 you're way too hypersensitive 20:31:45 s/^ // 20:32:27 alise: redunant 20:33:02 yawn. 20:36:12 -!- Slereah has joined. 20:38:00 -!- olsner_ has quit (Quit: olsner_). 20:40:22 Does it have any Linux-related shittiness? <-- some 20:40:30 alise, if you by that means "buggy" 20:40:40 you need to disable the java stuff or it bogs down the whole system 20:40:45 and you need to get some replacement files 20:40:54 to fix other causes of bogging down the whole system 20:41:01 the java stuff is needed for the built in help stuff 20:42:07 alise be nice to me :/ 20:42:13 I haven't run into any system-bogging, and the help has worked too :-P 20:42:20 Deewiant, 64-bit edition? 20:42:28 That too, yes 20:42:32 Deewiant, check number of wakeups with powertop while mathematica is running 20:42:38 it is caused around 5000 per seconds 20:42:48 if java link is enabled 20:42:54 That's not what I'd call "bogging down the whole system" 20:42:57 Deewiant, on a laptop that just doesn't work 20:43:08 Deewiant, well true, that is what the other replacement files fix 20:43:09 It's using excessive amounts of power, but that's it 20:43:13 the 100% CPU usage 20:43:27 Yeah, see, the 100% CPU usage I haven't run into :-P 20:43:29 -!- sebbu2 has joined. 20:43:32 Deewiant, well I did 20:43:52 fax: so be nice to me 20:43:57 fuck you 20:44:10 fax: see, this is /not/ the way you ask me to be nice to you 20:44:15 fax, why do you think alise is an idiot for pirating mathematica 20:44:19 I would like to hear a reason 20:44:26 AnMaster: because he's a wolfram fanboy and calls copyright infringement "stealing" 20:44:27 AnMaster, I just called him an idiot because he said that to me 20:44:30 because this is ridiculous from both of you 20:44:33 alise you don't know anything 20:44:35 <3 Wolfram + Piracy is evil = you monster 20:44:42 seriouly just stop guessing 20:44:43 alise why the fuck would you steal mathematica 20:44:43 Oh no, not an idiotic copyright defender. 20:44:43 fuck you 20:44:43 you're the idiot 20:44:43 -!- sebbu has quit (Ping timeout: 276 seconds). 20:44:43 -!- sebbu2 has changed nick to sebbu. 20:44:44 that 20:44:46 is what I mean 20:44:53 Yeah, that's what I commented on earlier 20:44:56 fax, please explain what you meant with your first line there 20:44:57 AnMaster: yeah I just explained it 20:45:09 fax, no, you didn't 20:45:19 fax, you didn't explain "alise why the fuck would you steal mathematica" 20:45:26 what's to explain 20:45:34 fax, that statement 20:45:42 I can think of lots of reason to pirate mathematica 20:45:49 so what is your reasons not to 20:46:32 oh and wolfram is somwhat insane. He needs to get medical help before his ego kills him 20:48:45 http://upload.wikimedia.org/wikipedia/commons/0/06/Pentatope_of_70_spheres_animation_original.gif 20:54:00 -!- jcp has joined. 20:54:08 I'm going to boot into Ubuntu now. 20:54:12 -!- alise has quit. 21:00:26 i'd boot your ubu- oh. :| 21:03:02 -!- songhead95 has joined. 21:03:36 -!- songhead95 has quit (Remote host closed the connection). 21:04:18 -!- songhead95 has joined. 21:06:44 -!- MigoMipo has quit (Remote host closed the connection). 21:12:14 Deewiant: I don't suppose you happen to be on T-76.5753, incidentally? 21:12:33 No, I'm not. 21:13:23 Deewiant: Why not! 21:13:45 Too much work as it is. 21:13:59 Admittedly I had no reason to suspect you were, except that it would've been a Fancy Coincidence. 21:15:13 There's the © and ® characters in the "special characters" key-list on the N900, but no ™ :/ .. maybe because the first two are in latin-1 and that one is not, but that's not a good reason. 21:33:02 -!- MigoMipo has joined. 21:40:49 hmm, worrying that alise hasn't come back 21:46:09 does ey do this often? 21:52:31 ais523: It's the Ubuntu, it's razzling-dazzling multimedia interface has locked him into a trance. 21:52:42 heh 21:53:02 When you gaze into GNOME, the gnome also gazes at you. 21:53:12 fizzie: Your apostrophes are extraneous again 21:53:26 Deewiant: I am being very bad with them today for some reason. 21:53:49 Deewiant: I shall try to avoid all contractions, maybe that will help. 21:54:20 If you avoid possessives as well you should be fine. 22:18:26 -!- alise has joined. 22:18:30 Le puff, le pant. 22:19:49 Success, evidently. 22:19:55 Of a sort... 22:20:30 Who knew that you needed to do a forced lazy unmount of the partition the system is running on to install Ubuntu? 22:23:36 It must be part of the built-in intelligence test, to see if you are Worthy of Ubuntu. 22:24:08 Someone ping me. 22:24:11 As in highlight. 22:25:03 alise: 22:25:07 yay, you're back 22:25:10 Yay, it worked. 22:25:21 I was wondering why you took so long to come back 22:25:27 ais523: umount -f -l (a mount from the partition the system is running on) 22:25:37 hmm, I didn't need to do that to install 22:25:42 I did! 22:25:53 I don't think I used the command line at all, come to think of it 22:26:02 except afterwards, to compile the wifi card driver 22:26:25 Well, I was running the LiveCD from an NTFS partition. 22:26:30 And /cdrom was C:\ whilst / was a subset of C:\. 22:26:43 I had to force-unmount /cdrom (it refused to do so because the device was being used) and then remount it again before it got to GRUB. 22:27:06 NTFS? why? 22:27:30 because the Toshiba Satellite, as you know, has no optical drive; and I didn't have any USB sticks handy 22:27:36 aha 22:27:45 didn't realise the lack of a USB stick 22:28:05 Yes, don't you get USB sticks with breakfast cereal nowadays? 22:28:21 :) 22:28:22 I don't 22:28:27 * alise installs ttf-droid to change the UI font 22:28:32 I'm a bit bored of DejaVu Sans. 22:28:38 ok 22:28:45 Deewiant: What sort of breakfast cereal do you buy? 22:28:48 By "I'm a bit bored of", I mean "I think that a really boring font is". 22:28:59 I was going to say "what's wrong with DejaVu Sans", but boringness is a fine reason 22:29:01 Is ttf-droid the Android font? 22:29:02 fizzie: I don't. Maybe that's the problem. 22:29:17 I eat oats for breakfast, but persuade someone else to buy them 22:29:25 DejaVu Sans is a bit too wide especially. 22:29:30 fizzie: Yes. 22:29:36 It's, if nothing else, not boring. 22:29:44 ais523: what; raw oats? 22:29:55 with soya milk 22:30:03 Vegan? 22:30:09 lactose intolerant? 22:30:10 or just like it? 22:30:12 I'm not vegan, although my breakfast is by chance 22:30:16 it's lactose intolerance 22:30:21 I have the Android monospaced font on the N900 in use in the terminal; it's a lot nicer to the Nokia font. Can't really say whether I prefer it over DejaVu Sans Mono, but then again, I'm pretty boring too. 22:30:37 also, I can have a bit of lactose per week, but not too much 22:30:39 3% [1 ttf-droid 94119/2,771kB 3%] // and it freezes... 22:30:46 besides, I've been drinking soya milk for decades, now 22:31:11 and due to the way acquired tastes work, I now can't stand to drink any other sort of milk 22:31:40 i'm a goat 22:33:42 "We have commissioned a new font to be developed both for the logos of Ubuntu and Canonical, and for use in the interface. The font will be called Ubuntu, and will be a modern humanist font that is optimised for screen legibility." 22:33:45 Let's hope that's nice, then. 22:36:36 alise: is this your first time using linux? 22:36:40 Haha, no. 22:36:45 Not by a long shot. 22:36:58 First time installing it on this /machine/, yes... 22:37:06 First time installing it without an optical drive or USB stick... yeah. 22:37:15 tried anything other than ubuntu? 22:37:23 Yes. 22:38:04 I've used Debian, Arch, almost Slackware (its installer hates me; or more probably my systems), even tried getting Mastodon to work... I'd say I've tried stali, but it isn't even out yet. 22:38:14 I also tried Mandriva when I was young and naive. 22:38:22 I've also used FreeBSD. 22:38:39 * alise uses Oxford University as his Ubuntu mirror 22:38:48 At least it works. 22:38:57 Albeit rather terribly slowly. 22:39:02 Slackware (or was that Debian) had a nice, standard "install without any boot media" officially-supported installation strategy, which (I think) involved dd'ing the ISO image on the partition you were going to use for swap, then booting the installer off that (kernel with loadlin, I think; this was for from-DOS installs), and activating swap only after the installation was done. 22:39:19 pineapple: Oh, I've also used Plan 9 and researched its architecture rather extensively. 22:39:28 That is still supported in Slackware. 22:39:38 And I think the Debian install manual describes how to do the same. 22:39:47 pikhq: Can you still install Slackware from a huge pile of floppies?-) 22:40:00 fizzie: No, they stopped that a couple releases ago. 22:40:05 Aw. 22:40:10 Stop using freaky smilies man 22:40:13 ? is not eyes 22:40:23 It is a FREAKY eye. 22:40:44 Admittedly floppy distributions were getting a bit ridiculous when the number of floppies goes >20 or so. 22:40:57 Yeah. 22:41:14 Download on: 22:41:14 * DVD 22:41:14 * Floppies 22:41:41 I think they had a release of that. 22:42:26 Win95 OSR 2.1 was a 23-floppy release, it seems. (I have forgotten the exact count.) 22:42:33 26, I mean. 22:42:49 Definitely 26. 22:42:57 I actually installed it from floppy once. 22:43:07 "I know. I was THERE." 22:43:14 I wonder why it is that none of my installations ever go smoothly? 22:45:16 ais523: what's the best ubuntu mirror :x 22:45:24 i need one insanely fast because my connection sucks. 22:45:33 I use the one in Sweden when there's heavy load 22:45:47 which one? 22:45:58 atm, though, I think I'm on the default UK one 22:46:01 which should be on the menus 22:46:54 * alise tries the swedish kernel.org 22:49:11 Bah 22:52:25 mirrorservice.org is usually reliable for me 22:54:06 -!- Gracenotes has joined. 22:55:35 -!- alise has quit (Quit: Leaving). 22:56:42 -!- alise has joined. 22:56:58 -!- alise has quit (Client Quit). 23:01:44 -!- alise_ has joined. 23:01:48 Adheration. 23:03:42 What's the fanclub for Black Adder called? 23:03:44 Soya "milk". Milk comes from mammals. Soya isn't one. :-> 23:03:46 Adder Nation 23:03:46 8D 23:04:23 Ilari: well, soya milk's the usual name 23:04:26 Ilari: Milk snobbery? That is a new one. 23:05:52 milk comes from coconuts 23:06:46 ooo burn 23:08:18 There are lots of other products that are called by incorrect names. Like various "Creams" (that are really mostly water, soft fat and additives). 23:08:34 豆乳 comes from beans! 23:09:37 Ilari: I'd say something about prescriptivism, but - 23:10:16 Then there are downright oxymorons like "Fat-free mayonnaise". 23:11:01 :-D 23:12:18 -!- oklopol has joined. 23:12:25 hi oklopol 23:12:41 hi alise_ 23:12:59 i was watching a priest dance an erotic dance 23:13:11 okay. 23:16:19 oklopol -- do you know chevally warning 23:16:40 no 23:16:46 it's a good theorm :D 23:16:49 number theory 23:17:02 oklopol I cannot solve this OR thing :/ 23:17:29 well there are a few concepts you don't know that it depends on 23:18:08 i mean really basic concepts, just that you might not realize they're important 23:18:30 Oh, and then there is some misleading names like "milk drink". That's not Milk (something has been done to it so it can't be sold as milk). Oh and don't search for "soya milk" either, its "soya drink". 23:21:03 Oh, and those various "Creams" fortunately can't be sold as creams. :-) 23:23:53 Wonder what milk of Bosavi woolly rat would taste like... :-) 23:24:46 the idea was you do U=V OR U=W by either making U match with V or W, for this you'll need to have ...U... = ...V...W..., and then do some magic to make U only hit exactly one of those two. for this you'll need to at least be able to build primitive words out of U's, V's and W's 23:26:16 ofc i can give more concrete hints as well, or just show you the whole proof; there's a lot more interesting stuff to prove where this came from.... :P 23:27:55 (if anyone else is interested, the context is to represent the OR of two equations on words as one) 23:30:03 -!- coppro has joined. 23:30:28 -!- oklokok has joined. 23:31:10 oklopol, that doesn't make sense :| 23:31:15 which part 23:31:19 if U only hits one of them what happens to the rest 23:31:39 -!- alise has joined. 23:31:58 Good mrr'nng America. 23:32:12 who cares? we know it can't hit anything but either of them, if it can hit one of them, the OR is true, if it can't hit either, then it can't hit anything, and the OR is false 23:32:24 -!- alise_ has quit (Ping timeout: 252 seconds). 23:32:26 yay, ubuntu beta 23:32:57 for ...U... = ...V...W... 23:33:12 the both sides have to be the same length 23:33:25 so how can we have ... = ...V... OR ... = ...W... 23:33:26 you have to find such values for ... that U can only be on top of either V or W, then it can be on one of them iff either of the equations is solvable, we just have to make sure it can't be on top of anything else 23:33:54 err you can just have some new variables in ... that fill the rest 23:34:00 coppro: The major changes are in the GNOME version though. 23:34:03 -!- oklopol has quit (Ping timeout: 252 seconds). 23:34:13 yes 23:34:25 I don't care, I'm happy the upgrade was smooth 23:34:27 it often isn't 23:34:43 like zUz' = ...V...W..., not that i'm saying the left side can actually be that simple 23:35:24 U can be anything, so there's no way to guarantee U can't be on top of say just the left half of V 23:36:06 oh well those should be Z and Z' 23:36:19 i can't learn this convention it seems 23:36:21 :P 23:37:17 3oh 23:37:19 o 23:38:01 anyway i find this trivial because i've seen the solution, but it may have been an open problem at some point, don't really know 23:39:41 ais523: Isn't it interesting that one of the best programming /environments/, Mathematica, is paired with one of the worst programming /languages/? 23:40:01 alise: the environment is tained by the language, I think 23:40:03 *tainted 23:40:07 also, I hate the way it does line breaks 23:40:22 as in, mathematica the IDE suffers from being written in mathematica the lang 23:40:55 it isn't 23:40:57 the length of the RHS of the solution i have is 38. so you're not going to find it by any sort of brute force 23:41:04 mm... but if you don't run into the shittiness of the language, it's very nice 23:41:13 oklokok haha I'm not going to find it at all 23:41:18 :) 23:41:28 * augur grabs oklokok 23:41:40 ais523: also I think automatic formatting is obviously good but mathematica messes it up 23:41:41 :o 23:41:46 oklokok I couldn't even find the diophantine representation of complement of powers of 2 23:41:54 that one is SO EASY but I didn't get it :| 23:41:58 alise: ok, I'm happy with that opinion 23:42:27 brb 23:42:27 what's the exact problem? 23:43:06 like an equation where the solutions, restricted to X, are exactly N - {2^n | n \in N} 23:43:43 here's the set {a} of composites: a = xy 23:43:52 well that's wrong actually 23:43:54 let me correct it 23:43:59 here's the set {a} of composites: a = (x+2)(y+2) 23:44:06 since it's in natural numbers 23:44:25 right so solutions restricted to a are exactly composites 23:44:44 all positive values of a are composites 23:44:59 the general idea is D(a,x1,x2,...,xn) = 0 23:45:10 where D is some polynomial iwht integer coefficents 23:45:20 yeah, i just needed the definition of "diophantine representation" 23:46:24 so umm is it "x = (y + 3)(z + 1)"? 23:46:32 you need to have some factor that's more than 2 23:46:37 and then some other factors 23:46:42 almost 23:46:47 hmm 23:46:55 oh lol 23:47:08 you can still do 4*2 23:47:19 sorry 23:47:21 so who's watched Earth: Final Conflict? 23:52:26 oklopol, the answer is (2y + 3)(z + 1) 23:52:51 err right ofc 23:53:04 was just about to get paper 23:53:09 anyway the complement of this set (powers of two) is diophantine as well 23:53:17 but that's a hard theorem (takes a whole chapter) 23:53:25 yeah it does sound harder 23:53:48 the method is great.. he encodes a sequence (fibonacci sequence) and since that has roughly exponential growth, that proves that exponentitation can be defined too :D 23:54:04 the sequence they actually use (to make the proof more direct) isn't fibs though 23:54:32 should have said asymptotic rather than roughly 23:54:35 for "has odd factor" you just write x = odd*any, the other direction doesn't have a simple explanation with existential quantification 23:55:09 (complement isn't always diophantine, compare with the analogue of recursive languages...:)) 23:55:22 but in the case of exponentiation it is 23:55:23 well of course not 23:55:41 and proving that exponentiation was diophantine was the last piece needed to complete the proof (of hilberts 10th) 23:55:49 hmm well not sure about of course 23:57:13 oh hmm 23:57:18 right i've actually seen that 23:57:37 seen what/? 23:59:00 exponentiation, but i just realized i haven't 23:59:39 it's a pretty tough chapter, I haven't really worked through it yet just understood the general idea 23:59:48 what are you reading?