←2011-01-29 2011-01-30 2011-01-31→ ↑2011 ↑all
00:07:26 -!- pikhq has joined.
00:15:08 <zzo38> To me, at least, GNU is more a part of the operating system than KDE is.
00:16:45 <variable> I reset my computer yesterday - so its gets a new name "befunge"
00:23:13 * Phantom_Hoover → sleep
00:27:17 -!- Phantom_Hoover has quit (Ping timeout: 240 seconds).
00:34:43 -!- variable has quit (Ping timeout: 264 seconds).
00:36:15 -!- variable has joined.
00:39:19 -!- copumpkin has changed nick to MostInterestingM.
00:39:43 -!- MostInterestingM has changed nick to copumpkin.
00:40:04 <oerjan> copumpkin: hey what is the Monad instance for that
00:40:45 -!- elliott_ has joined.
00:40:46 <copumpkin> it's too interesting to repeat
00:40:48 <copumpkin> sorry
00:40:54 <oerjan> AWW
00:41:10 -!- elliott has quit (Read error: Connection reset by peer).
00:41:12 <copumpkin> oh, the AW comonad transformer?
00:41:15 -!- elliott_ has changed nick to elliott.
00:41:17 -!- elliott has quit (Changing host).
00:41:17 -!- elliott has joined.
00:41:29 <copumpkin> doesn't really work
00:41:39 <elliott> there are comonad transformers? :D
00:42:14 <copumpkin> .
00:42:19 <copumpkin> http://hackage.haskell.org/package/comonad-transformers
00:43:12 * oerjan cunningly checks #haskell logs but is none the wiser
00:44:21 <oerjan> i'm sure Sgeo would like that AWW transformer
00:44:26 <copumpkin> lol
00:46:00 -!- cheater00 has joined.
00:49:16 -!- cheater- has quit (Ping timeout: 240 seconds).
01:02:52 -!- nddrylliog has joined.
01:04:48 <nddrylliog> ohai. anyone alive?
01:05:09 <elliott> no
01:05:10 <elliott> :)
01:05:11 <oerjan> *GASP* *GACK*
01:05:31 <oerjan> Brains...
01:07:07 <nddrylliog> nice!
01:07:18 <nddrylliog> got a crazy ideas I'd like feedback on
01:07:26 <nddrylliog> -s
01:09:46 <zzo38> What is the ideas?
01:09:51 <nddrylliog> https://docs.google.com/present/edit?id=0AakBA-t72L0TZGZncTh0aGJfMTAwZzM0cTJmYzk&hl=en&authkey=CMyQ8Qc
01:10:15 <nddrylliog> ^ here it is, in its nake beauty. Bear in mind that it's 02:23 AM.
01:10:18 <nddrylliog> +d
01:11:06 <elliott> who the fuck makes slideshows at 2:23 am
01:11:14 -!- Mathnerd314 has joined.
01:11:19 <nddrylliog> elliott: :D
01:11:28 <elliott> nddrylliog: you're disturbed!
01:11:46 <nddrylliog> elliott: oh, breaking news.
01:11:50 <elliott> :D
01:12:03 <elliott> We also know that it's probably stupid to try to access element -1, or element i > size (syntactic sugar aside).
01:12:03 <elliott> But we have to spell it out carefully so that the program won't crash and burn because we joyfully walked over the boundaries of the allocated memory.
01:12:08 <elliott> nddrylliog: you may like http://www.ats-lang.org/.
01:12:29 <nddrylliog> basically, I'm hesitating between "this has been done before" and "nobody's smart enough to implement such a compiler"
01:12:29 <elliott> nddrylliog: it's a low-level functional systems programming language with dependent types to ensure safety and correctness.
01:12:38 <nddrylliog> with option 2 being a little more hopeful than the first
01:12:59 <nddrylliog> oh yeah, ATS sounded fun
01:13:11 <elliott> http://www.bluishcoder.co.nz/tags/ats/ are probably interesting posts since most of chris double's are :P
01:13:58 <nddrylliog> elliott: but I hope you undertand from my slideshow that what I'm suggesting is way more than just pre/post conditions
01:14:04 <nddrylliog> elliott: ooor just safety
01:14:05 <elliott> well I haven't read any more yet! :D
01:14:23 <elliott> "An array has constant time access to element of index 0"
01:14:26 <elliott> and index N... but
01:14:31 <elliott> is that important for the compiler to know?
01:14:51 <nddrylliog> that comes later
01:14:56 <nddrylliog> that's just a human description
01:14:59 <nddrylliog> with redundant rules, etc.
01:15:01 <elliott> nddrylliog: looking at slide 11, i can safely say you're going to need to write proofs to program in this language
01:15:05 <nddrylliog> this part doesn't matter much, it's just examples
01:15:08 <elliott> at least in complicated cases
01:15:25 <nddrylliog> elliott: I think that's a safe assumption, yeah
01:15:31 <elliott> nddrylliog: that element inside array can be written as e.g.
01:16:08 <elliott> Record ElementOf (array : Array) := mkElement { index : nat; index_in_range : index < sizeOf array; data : something goes here }
01:16:10 <elliott> nddrylliog: in Coq
01:16:15 <elliott> where "index < sizeOf array" represents a proof of that
01:16:25 <nddrylliog> yep
01:16:32 <nddrylliog> I should really take a look at Coq, it's been teasing me for years
01:16:40 <elliott> such a Coqtease
01:16:42 <elliott> i apologise
01:16:43 <elliott> i'm sorry
01:16:46 <elliott> don't kick me oerjan
01:16:52 <elliott> i'm a good person, inside
01:17:09 <nddrylliog> goddamn, 78 google results
01:17:14 <elliott> :D
01:17:16 <nddrylliog> there are weirder people than me
01:17:27 <oerjan> i cannot kick you, i didn't get the pun
01:17:42 <elliott> oerjan: cock-tease + Coq
01:17:44 <elliott> element {
01:17:44 <elliott> 0 <= index < size
01:17:44 <elliott> data
01:17:44 <elliott> }
01:17:44 <elliott> (0 <= index < size) => exists(element e | e.index == index)
01:17:45 <elliott> nddrylliog: rephrase:
01:17:48 <elliott> element { data }
01:18:13 <elliott> (0 <= index < size) <=> isElementAt(array, index)
01:18:14 <elliott> or something
01:18:16 * oerjan wasn't aware of that word
01:18:35 <nddrylliog> elliott: right but how do you define isElementAt ?
01:18:36 <elliott> "So, what can our language do?" <-- absolutely nothing, you haven't specified any computation mechanism >:D
01:18:59 <nddrylliog> bbbahh at this point it can check for things
01:19:03 <elliott> nddrylliog: well here's an abstract array structure in Coq
01:19:20 <oerjan> also, having a good person inside is no excuse, that's true even for cannibals!
01:19:33 <elliott> Record Array (elemType:Set) := mkArray { size : nat; get : forall index:nat, (index < size) -> elemType }
01:19:51 <elliott> nddrylliog: where get is initialised by the run-time system and such
01:19:54 <elliott> i.e. this is just abstract
01:20:09 <nddrylliog> yeah but. you're missing the "consecutive" element part.
01:20:16 <elliott> nddrylliog: howso
01:20:39 <nddrylliog> grr this is the only point I wanted to get across in these slides and I failed
01:20:44 <nddrylliog> the point is
01:20:46 <elliott> :)))
01:20:48 <nddrylliog> you're not describing an array
01:20:52 <nddrylliog> you're describing any kind of list-like structure
01:21:02 <nddrylliog> I, on the other hand, I'm describing a specific implementation of a kind of list-like structure
01:21:03 <elliott> nddrylliog: sure... but that's just a stupid low-level detail :D
01:21:09 <nddrylliog> no it's not
01:21:11 <nddrylliog> that's my point
01:21:13 <elliott> OH YES IT IS
01:21:14 <nddrylliog> cache
01:21:19 <nddrylliog> ^ cache cache cache cache
01:21:22 <elliott> another stupid low-level detail, like CPUs and the universe
01:21:25 <nddrylliog> victim cache - if anyone ever does that in hardware
01:21:27 <elliott> and existence
01:21:29 <nddrylliog> TLBs
01:21:33 <nddrylliog> hit, misses, lines
01:21:34 <nddrylliog> (of coke)
01:21:42 <elliott> nddrylliog: i'm sorry, all I can see is "DETAIL DETAIL DETAIL"
01:21:47 <elliott> nddrylliog: more seriously, you might want to look at Frama-C
01:21:58 <elliott> nddrylliog: it's a theorem-proving system for C code
01:22:04 <elliott> nddrylliog: that uses Coq as a backend
01:22:21 <elliott> (I realise it's not what you want, but you could perhaps compile your language to this.)
01:22:24 <elliott> (Or even just get ideas from it.)
01:22:28 <nddrylliog> right, right
01:22:32 <nddrylliog> anything that looks like it interests me
01:22:47 <nddrylliog> but yeah, this idea is pretty much all about the details
01:22:53 <nddrylliog> that makes a program run fast, you know.
01:23:05 <nddrylliog> correctness and conciseness are just two nice side effects :)
01:23:23 <elliott> nddrylliog: "In the following code, # means belong to and something' means the future version of something" <-- go purely functional, simply return a new array satisfying an additional condition
01:23:35 <elliott> nddrylliog: this will make your language's semantics a _lot_ simpler and allow for easier implementation
01:23:49 <elliott> nddrylliog: (without significantly reducing performance -- in most cases, it is easy to turn this into mutation at the compiler level)
01:23:54 <elliott> nddrylliog: (after you verify correctness)
01:23:59 <nddrylliog> that's... what I'm doing
01:24:03 <nddrylliog> where are you seeing any modification?
01:24:16 <nddrylliog> well
01:24:23 <nddrylliog> well hmmph actually it's a bit unclear, I agree.
01:24:45 <nddrylliog> but mhm yeah I can go purely functional.
01:25:21 <elliott> nddrylliog: well
01:25:27 <elliott> array.insert (index i, data d) =>
01:25:27 <elliott> (element e | e.data == d, e.index == i) # arra
01:25:30 <elliott> nddrylliog: I would rephrase this as.
01:26:00 <elliott> nddrylliog: erm
01:26:04 <elliott> nddrylliog: dude, your element e thing is broken
01:26:08 <elliott> because it doesn't specify what array it refers to
01:26:09 <elliott> :)
01:26:23 <elliott> nddrylliog: it should be (exists e : element theArray | ...)
01:26:26 <elliott> i.e. taking the array as a type parameter
01:26:47 <elliott> here's how i would phrase it: array.insert(index i, data d) == array' => exists (e : element array' | e.index == array.size && e.data = d)
01:27:55 <elliott> "The compiler can detect edge cases itself, and optimize for them."
01:28:00 <elliott> beware the sufficiently-smart compiler argument
01:28:10 <nddrylliog> yeah I know, I know
01:28:20 <elliott> your language seems nice, but so far, you haven't provided ANY concrete details as to how any of this could be implemented :)
01:28:29 <nddrylliog> but it seems so simple from here, and we could help it for complex cases
01:28:46 <nddrylliog> yeah I know but you should know how my brain works - I have ideas how to implement that. I'm being practical
01:28:47 <elliott> as someone who's looked a lot at formal verification of software
01:28:51 <elliott> THIS IS NOT SIMPLE AT ALL :)
01:28:52 <nddrylliog> and
01:28:56 <elliott> even these simple examples you give
01:28:57 <nddrylliog> yeah it's not :)
01:29:09 <elliott> nddrylliog: well let's put it this way i think your language would advance the state of the art about 20 years.
01:29:13 <nddrylliog> but hmm your version of insert is 1) much longer 2) I don't see what's wrong with my 'element e'
01:29:26 <nddrylliog> when you first define it, it doesn't belong anywhere... yet
01:29:35 <elliott> nddrylliog: by version is much longer but much more precise and purely functional
01:29:45 <elliott> nddrylliog: also, exists (element e | e.index == n && e.data = d) is true by definition
01:29:48 <elliott> you can construct such an element structure
01:29:55 <elliott> nddrylliog: the point is that you've just said it exists, not where it is
01:29:55 <elliott> uhh
01:29:58 <nddrylliog> so "e: element array'" replaces the '#' notation
01:30:01 <elliott> basically that statement is logically nonsense.
01:30:03 <elliott> nddrylliog: no it doesn't
01:30:05 <elliott> well
01:30:05 <elliott> yes
01:30:08 <elliott> your # notation makes no sense :)
01:30:11 <elliott> at all
01:30:12 <nddrylliog> yeah
01:30:20 <nddrylliog> when I wrote that, I knew it would be a nightmare to implement
01:30:22 <elliott> well it does intuitively, but not from a logic point of view at all
01:30:36 <elliott> and it would also hold you back a bit i think as far as what propositions you could construct
01:30:57 <elliott> nddrylliog: my insert is also longer because i removed the "future value" stuff and replaced it with a saner functional approach :)
01:31:10 <elliott> nddrylliog: you may want to rephrase the whole thing as array.insert's type signature returning a certificate
01:31:21 <elliott> basically return a tuple of (array', proof of the proposition on array')
01:31:38 <elliott> (you can have language support for ignoring the proof but absorbing it into the "environment" to make actually using the function easier)
01:33:03 <nddrylliog> hmm
01:33:10 <nddrylliog> what do you mean make using the function easier?
01:33:39 -!- azaq23 has quit (Ping timeout: 240 seconds).
01:33:40 <elliott> nddrylliog: as in, without having to explicitly say "first_tuple_element result"
01:34:02 <elliott> you could e.g. say that %x takes the first element of tuple x, but remembers the second one for the proof system
01:34:07 <elliott> then you could do, like
01:34:16 <elliott> (%array.insert(42))[0]
01:34:21 <elliott> nddrylliog: oh and my insert was actually an append i just realised
01:34:25 <elliott> which is why it was different to yours
01:35:14 <nddrylliog> oh yeah, that too
01:35:21 <nddrylliog> but we can do e.index == i, no big deal
01:35:30 <nddrylliog> but hum why the [0] ?
01:36:16 <elliott> nddrylliog: just an example
01:36:24 <elliott> nddrylliog: also just saying e.index == i isn't really enough
01:36:35 <elliott> nddrylliog: you'd want to also demonstrate that every element at i and after in the original array is at i+1
01:36:39 <elliott> to make managing things easier
01:37:45 <nddrylliog> well the thing is
01:38:09 <nddrylliog> since we have (e1, e2: element array) => (e1.index != e2.index)
01:38:15 <nddrylliog> there's a conflict
01:38:23 <elliott> no there isn't
01:38:24 <nddrylliog> so either the compiler would say that insert is invalid
01:38:33 <elliott> how is there a conflict?
01:38:41 <nddrylliog> either it would figure out that the only way to do it is to move all the elements on the right of it
01:38:43 <nddrylliog> *of i
01:38:50 <nddrylliog> because then we'd have two elements with index i
01:38:58 <elliott> no we would no
01:38:59 <elliott> t
01:39:02 <elliott> here's how i would write insert's type signature, Coq-style (since Coq is less ambiguous ... :))
01:39:23 <nddrylliog> sure
01:40:22 <elliott> insert : forall (array : Array), forall (i : Index array), ElementType -> (Sigma (array' : Array), (forall (j : Index array), j < i -> ... bleh
01:40:30 <nddrylliog> oh btw, "i think your language would advance the state of the art about 20 years." => yes, I figure that it's better to work on such a language even if it's not an easy problem, rather than try to re-implement Java/C# done right (ie. ooc)
01:40:46 <elliott> nddrylliog: i think using any kind of non-opaque integer for index types is a bad idea.
01:40:54 <elliott> because the propositions get really gnarly :)
01:41:18 <elliott> nddrylliog: have an opaque index type or something
01:42:47 <nddrylliog> opaque?
01:42:57 <nddrylliog> the only opaque I know is C-struct-opaque and I don't see how it applies
01:43:10 <elliott> nddrylliog: I mean exactly that. as in, you don't know that an (Index array) is a number.
01:43:31 <nddrylliog> ah.
01:43:33 <nddrylliog> well why not
01:43:36 <nddrylliog> it doesn't change much
01:43:42 <nddrylliog> as long as it's comparable
01:44:48 <nddrylliog> then you could even implement a hashtable on top of that dynamic array, haha :)
01:46:13 <elliott> nddrylliog: it does change much
01:46:21 <elliott> because it lets your propositions be less ugly :P
01:46:32 <nddrylliog> how so?
01:46:39 <elliott> well see my line of coq above. it got ugly.
01:46:51 <elliott> nddrylliog: and the nice thing is you'd need no < relations or whatever.
01:46:58 <elliott> (Index array) is always addressable, no exceptions.
01:46:59 <elliott> or whatever.
01:47:09 <elliott> and also, you know, maybe the compiler will think of a better representation of indices for your very specific type of data, because it has to be a genius already :)
01:47:17 <nddrylliog> oh right
01:47:28 <elliott> (note: I'm interested in your ideas, don't take my mocking seriously :P)
01:47:43 <nddrylliog> 256-elements array = use chars for indices \o/ (on an 8-bit processor, obviously - otherwise we're losing the perf. improvement)
01:47:43 <myndzi> |
01:47:43 <myndzi> >\
01:48:01 <nddrylliog> elliott: I don't take it seriously :) it's very constructive so far
01:48:11 <nddrylliog> elliott: from what I can see, Coq quickly gets clumsy.. probably because it works
01:48:28 <elliott> nddrylliog: oh Coq isn't a party. but yes, it works. frama-c seems nice enough. coq is a good backend at least :P
01:49:01 <nddrylliog> elliott: let's talk about your element { data } part
01:49:05 <nddrylliog> elliott: why rewrite it that way?
01:49:07 <elliott> nddrylliog: the thing is that Coq was designed by taking a core, simple logic to ensure correctness, and then the rest was built on top of that
01:49:16 <elliott> rather than starting with convenience and ending with a mess like a lot of people :P
01:49:19 <nddrylliog> elliott: somehow it bothers me to 'declare' index inside element, because it somehow makes me think the compiler will store it
01:49:22 <elliott> nddrylliog: well i don't think your element structure even makes much sense.
01:49:39 <nddrylliog> but.. not so much because from all the constraints it can be deduced that it's unnecessary to store it
01:49:41 <elliott> elements aren't "real", there are just valid indices that you can access.
01:49:48 <elliott> really you want an index type.
01:50:10 <elliott> which could even be defined to be index array := n | 0 <= n < size array.
01:50:25 -!- pikhq has quit (Ping timeout: 255 seconds).
01:51:33 <nddrylliog> well we have to be able to express that elements belong to the array and that they have a data.. and they definitely all have an index associated
01:51:48 <nddrylliog> I'd have trouble defining the 'get' operation without element.index :)
01:52:01 <elliott> nddrylliog: no you wouldn't
01:52:10 <elliott> get : (array:Array) -> Index array -> ElementType
01:52:19 <elliott> (assuming all arrays have the same type of element for simplicity)
01:52:20 <elliott> nddrylliog: see?
01:52:45 <elliott> nddrylliog: then you can prove that "forall idx:(Index array), exists (e:ElementType), get array idx == e"
01:52:49 <elliott> because that's just a direct restatement of the function
01:52:49 <nddrylliog> s/defining/implementing
01:52:56 <elliott> well this would be easier to implement. :p
01:53:00 <elliott> probably.
01:53:13 <nddrylliog> easier to make a compiler for it, or easier to implement get in that language?
01:53:13 <elliott> you'd likely have to actually implement arrays at some level... but then your genius layer takes care of that :)
01:53:23 <nddrylliog> I'm still not seeing your implementation of get, only the function's signature
01:53:59 <nddrylliog> the point is, my (horrible, sketchy, ambiguous, not purely functional, unimplementable) language does away with that array primitive
01:54:07 <elliott> there is no implementation there.
01:54:16 <elliott> nddrylliog: no, in your language _everything_ is a primitive.
01:54:17 <nddrylliog> yep
01:54:18 <elliott> pretty much.
01:54:21 <nddrylliog> haha
01:54:24 <nddrylliog> what do you mean?
01:54:28 <elliott> nddrylliog: ok, well let's put it this way
01:54:37 <elliott> nddrylliog: let's imagine a proposition IsArray T, where T is a type.
01:55:11 <nddrylliog> yep
01:55:38 <elliott> nddrylliog: IsArray Ary := exists (Index : Ary -> Type | exists (get : Ary -> Index Ary -> ElemType))
01:55:42 <elliott> (ignoring the consecutive things FOR NOW)
01:55:54 <elliott> nddrylliog: then your language pretty much takes IsArray and comes up with a type that fits.
01:56:01 <elliott> ofc you'd likely want to specify how index behaves more.
01:56:08 <elliott> but whatever
01:57:58 <nddrylliog> nah nah nah don't "whatever" me - speak your mind
01:59:05 <elliott> nddrylliog: no no no that was me speaking my mind
01:59:06 -!- pikhq has joined.
01:59:18 <elliott> "but whatever" was just me breaking out of the train of thought as it became too complicated :)
01:59:25 <nddrylliog> right
01:59:34 <nddrylliog> but hu
01:59:36 <nddrylliog> *hum
01:59:41 <nddrylliog> embedded 'exists' = my mind hurts
02:00:46 <elliott> nddrylliog: you may want to become rather proficient with formal logic if you're embarking on this endeavour. :p
02:00:53 <elliott> Recursive call to slow_fib has principal argument equal to
02:00:53 <elliott> "S n1"
02:00:53 <elliott> instead of one of the following variables: n0 n1.
02:00:54 <elliott> oh fuck you.
02:00:58 <elliott> fuckity fuckity fuck
02:01:35 <nddrylliog> hahahahha
02:01:47 <nddrylliog> I think I have something simpler in mind :)
02:01:52 <nddrylliog> I'm going to try to implement it.
02:01:56 <nddrylliog> not necessarily right now, though
02:02:02 <elliott> nddrylliog: what simpler thing?
02:02:45 <elliott> Toplevel input, characters 142-154:
02:02:45 <elliott> Error: This clause is redundant.
02:02:46 <elliott> you're redundant.
02:03:11 <nddrylliog> haha :D. This is Coq's error messages?
02:03:20 <elliott> Fixpoint fibonacci (n:nat) : Z :=
02:03:20 <elliott> match n with
02:03:21 <elliott> | O => 1
02:03:21 <elliott> | S O => 1
02:03:21 <elliott> | S (S n as p) => fibonacci p + fibonacci n
02:03:21 <elliott> end.
02:03:23 <elliott> aha
02:03:25 <elliott> i can do it like that
02:03:27 <elliott> nddrylliog: yeah :)
02:03:33 <elliott> recursive functions in Coq have to be written... anally
02:03:37 <elliott> since it has to ensure termination
02:03:58 <nddrylliog> oooooooouch.
02:04:03 <zzo38> I have made TeX to read its own output.
02:04:15 <nddrylliog> zzo38: what' with you and TeX?
02:04:17 <nddrylliog> s
02:05:33 <elliott> it doesn't have that stupid principle argument why do you think i'm writing it like this coq
02:05:36 <elliott> what have i ever done to you
02:05:50 <zzo38> nddrylliog: What do you think?
02:05:59 -!- BeholdMyGlory has quit (Remote host closed the connection).
02:06:22 <nddrylliog> zzo38: dunno, maybe some child abuse story
02:06:29 <zzo38> nddrylliog: No.
02:06:52 -!- Slereah has joined.
02:07:14 <nddrylliog> zzo38: okay, I was messing with you. But making TeX do all sorts of weird stuff sounds extremely cool. Really.
02:07:30 <elliott> nddrylliog: he's done underload in tex
02:07:34 <elliott> which kinda puts yours to shame :P
02:07:38 <nddrylliog> yup, I remember :)
02:07:40 <nddrylliog> haha, totally
02:07:47 <nddrylliog> oh and mine doesn't work on all examples, too
02:08:16 <elliott> zzo38: isn't your current project a magic the gathering card generator based on TeX that's written in an underload-like language implemented in tex? i forget how texnicard is structured exactly
02:09:04 <zzo38> elliott: Something like that. It is not specific to Magic: the Gathering, and it uses TeX and METAFONT, but the main program is a C program (using Enhanced CWEB), it has a built-in programming language something like Underload (although more like dc than like Underload).
02:09:46 <elliott> nddrylliog: sometimes Coq's error messages are even better: "Anomaly: uncaught exception Not_found. Please report."
02:09:54 <elliott> (ok so the Program system is experimental.)
02:10:54 <Sgeo> I should learn Coq. And Standard ML. And Erlang. And Esperanto.
02:11:16 <nddrylliog> Sgeo: aaaaaaaand lojban.
02:11:40 <Sgeo> I love some Lojban words, like their "we"s. English should import those wes
02:12:17 <zzo38> (TeXnicard is less specific to Magic: the Gathering than Magic Set Editor)
02:13:18 <elliott> nddrylliog: (match Fib0 return Fib n 0 with x => x end)
02:13:20 <elliott> FUCK YEAH COQ
02:13:27 <elliott> looks like i have to prove that 0 = 0
02:13:34 <nddrylliog> elliott: ooooh. kinky
02:13:58 <nddrylliog> elliott: "prove me, baby. prove me good"
02:14:02 <elliott> hm wait i thought dependent pattern matching was meant to solve problems like this :D
02:14:05 <elliott> now how do you use it again...
02:17:01 <elliott> lol it still doesn't work
02:17:56 <nddrylliog> elliott: you're more or less scaring my ass off Coq :)
02:18:04 <elliott> nddrylliog: oh i'm actually just pretty stupid
02:18:18 <nddrylliog> elliott: not a relief - not what it looks like
02:18:23 <elliott> but coq is a great way to prove to yourself that you're stupid in general
02:18:41 <elliott> nddrylliog: well i may be giving you the misleading impression that i'm actually any good at Coq at all, which I am not
02:19:54 <elliott> wat da fak
02:19:56 <elliott> oh
02:20:00 <nddrylliog> elliott: oh I do smell the faint odor of someone trying to pretend he knows more than he does - but it's not bothering me :)
02:20:24 <nddrylliog> I'm doing it all the time anyway
02:20:36 <Sgeo> Of course Sensei's Library uses custom wiki software. Why wouldn't it?
02:20:39 * Sgeo facepalms
02:20:51 <Sgeo> Oh, it's based on PhpWiki
02:21:12 <elliott> nddrylliog: oh i make no pretensions about knowing what i'm doing
02:21:21 <Sgeo> "The source could (if at all) only be published on alt.tasteless.jokes."
02:21:25 <elliott> nddrylliog: i just know that a lot of things REALLY DON'T WORK, mostly because i tired them
02:21:53 <nddrylliog> http://bpaste.net/show/13336/
02:21:58 <nddrylliog> ^ that looks pretty compilable to me.
02:22:05 <elliott> Toplevel input, characters 1068-1072:
02:22:05 <elliott> Error:
02:22:05 <elliott> In environment
02:22:05 <elliott> slow_fib : forall n : nat, Sigma nat (Fib n)
02:22:05 <elliott> n : nat
02:22:08 <elliott> The term "Fib0" has type "Fib 0 0" while it is expected to have type
02:22:09 <elliott> "Fib ?182
02:22:11 <elliott> match ?183 with
02:22:14 <elliott> | 0 => 0
02:22:16 <elliott> | 1 => 1
02:22:17 <elliott> | S (S n as p) =>
02:22:19 <elliott> match slow_fib n with
02:22:21 <elliott> | witness fibn _ =>
02:22:24 <elliott> match slow_fib p with
02:22:26 <elliott> | witness fibp _ => fibn + fibp
02:22:27 <elliott> end
02:22:29 <elliott> end
02:22:31 <elliott> end".
02:22:34 <elliott> sorry for flooding, actually no i'm not, you all had to see that.
02:22:57 <nddrylliog> seriously, "witness" is a keyword in Coq?
02:24:03 <elliott> nddrylliog: no.
02:24:05 <elliott> that's my constructor.
02:24:30 <elliott> nddrylliog: don't worry, it doesn't feel so much like an interrogation, as a shouting match
02:25:43 <nddrylliog> haha, that's the spirit
02:25:48 <elliott> Recursive definition of slow_fib is ill-formed.
02:25:50 <elliott> not again.
02:26:05 <elliott> i know what i'll do.
02:26:11 <elliott> i'll tell it i'm going to use a termination proposition
02:26:15 <elliott> and then add it as an axiom
02:26:16 <elliott> that'll show it!
02:27:42 <nddrylliog> haha that sounds so dirty
02:29:32 <elliott> now if you'll EXCUSE me, I'm going to devote 15 minutes of my life to watching two British dolts walk around in a computer game made out of 1 m^3 blocks being confused and doing lots of silly things.
02:29:39 <elliott> because my time has no value!
02:29:43 <elliott> at least, not at 3 am.
02:31:10 <nddrylliog> haha
02:31:23 <nddrylliog> I'm probably going to die of a haha overload.
02:32:40 <elliott> hahahahaha
02:34:39 -!- augur has quit (Remote host closed the connection).
02:42:28 <nddrylliog> elliott: aauughh
02:42:37 <elliott> :wat:
02:43:51 <nddrylliog> you've haha'd me to death
02:43:57 <nddrylliog> seriously, cereals and coma sound good right now.
02:44:09 <nddrylliog> cheer(io)s o/
02:44:25 <oerjan> you've turned nddrylliog into a cereal killer!
02:45:41 <elliott> nddrylliog: and coma?
02:45:50 <elliott> "I'm going to eat cereal and then ENTER A VEGETATIVE STATE."
02:47:18 <nddrylliog> oerjan: dammit, that's my CS nick :)
02:47:29 -!- op_y_mous has quit (Quit: Quitte).
02:47:32 <nddrylliog> elliott: and ya, I can't really call that sleep, when I just pass out
02:47:35 <elliott> ah yes, the famed computer science codenames
02:47:39 <elliott> /nick TheCoqinator
02:48:20 <nddrylliog> one would think that to be rather coqy.
02:48:57 -!- asdf__ has quit (Quit: Leaving).
03:10:24 -!- nddrylliog has quit (Quit: Page closed).
03:17:08 <elliott> The term "prfp" has type "(fun H : nat => Fib ?119 ?120) n2"
03:17:08 <elliott> while it is expected to have type "Fib (S ?119) ?118".
03:17:47 -!- augur has joined.
03:23:52 <quintopia> wat
03:24:07 -!- Slereah has quit (Ping timeout: 240 seconds).
03:24:42 <oerjan> angkor
03:27:38 <quintopia> angkor wut?
03:28:23 <elliott> angkor HUGS!
03:29:22 * quintopia hugs hugs
03:29:49 <quintopia> don't let ghc get you down, hugs, you're okay with me
03:30:18 <elliott> how cute, quintopia travelled here from 2003
03:30:29 <elliott> hi quintopia, we've invented science while you're away
03:30:33 <elliott> also there's this thing called the "internet" now
03:31:05 <quintopia> elliott: even the woefully outdated need love too
03:37:40 <elliott> CANADA
03:39:07 <quintopia> yes, them.
03:47:27 <oerjan> > "CND" >>= (:"A")
03:47:28 <lambdabot> "CANADA"
04:02:44 <Sgeo> She's talking to me again
04:02:58 <Sgeo> Or, well, said one thing, but basically it said that we're talking
04:03:27 <elliott> I like how I can predict who "she" is by telepathy!
04:03:44 <variable> :-\
04:03:48 <Sgeo> elliott, or by memory
04:03:52 -!- variable has left (?).
04:03:55 -!- variable has joined.
04:04:42 <oerjan> elliott: that's because the subject is telepathetic
04:04:58 <elliott> naturally
04:05:40 <Sgeo> What? Have I talked about more than one person recently who I feared stopped talking to me?
04:08:16 <elliott> i tend to try and forget everything you say very quickl
04:08:16 <elliott> y
04:08:26 <elliott> *quickly
04:23:02 <Sgeo> The religious girl
04:25:56 -!- elliott has left (?).
04:25:59 -!- elliott has joined.
04:29:55 <zzo38> I also made TeX-js, although so far the only commands that work are \catcode and \message
04:38:31 -!- zzo38 has left (?).
04:42:11 -!- zzo38 has joined.
04:53:01 <elliott> hmm, I wonder if Kitten build scripts should be written in rc rather than sh
04:53:04 <elliott> COMMENTS ON A POSTCARD
04:53:50 <zzo38> elliott: How can I know where to mail it to?
04:54:24 <elliott> zzo38: 37.5A Cabbles Street, Vistum Street, Orkney
04:54:31 <elliott> *Cabbles House,
04:55:19 <zzo38> I have no opinion about whether they should be in rc or sh, but if someone does, they would need to know where to send the postcard.
04:55:21 -!- zzo38 has left (?).
04:56:09 <elliott> "And with that I LEAVE!"
04:59:40 -!- elliott has quit (Quit: Leaving).
05:49:55 -!- Sgeo has quit (Ping timeout: 240 seconds).
07:07:21 -!- wth has joined.
07:07:33 -!- wth has left (?).
07:22:33 -!- Wamanuz2 has quit (Remote host closed the connection).
07:23:25 -!- zzo38 has joined.
07:35:23 -!- zzo38 has quit (Remote host closed the connection).
07:38:05 -!- Wamanuz has joined.
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:20:11 -!- oerjan has quit (Quit: Good night).
08:33:32 -!- Phantom_Hoover has joined.
09:02:05 -!- MigoMipo has joined.
09:51:09 -!- acetoline has quit (Quit: Leaving).
10:18:08 -!- Wamanuz2 has joined.
10:18:13 -!- Wamanuz has quit (Ping timeout: 255 seconds).
10:19:12 <Ilari> Now the rumours are about 31st...
10:20:08 <quintopia> no reliable infos
10:40:17 <Ilari> Looks like this IPv4 depletion will be a giant clusterfuck (in the best case).
10:42:02 <quintopia> awesome!
10:43:05 <Ilari> And there's no guarantees that there won't be a RIR depletion(!) event before the World IPv6 day...
10:44:41 <Phantom_Hoover> What's RIR depletion?
10:45:40 <quintopia> regional registrars
10:47:40 <Ilari> Basically, the current official estimates for APNIC depletion are in end of September. But there have been speculations about April and May...
10:49:11 <quintopia> how much does the official estimate assume demand will rise as depletion date approaches
10:52:58 -!- cheater00 has quit (Ping timeout: 240 seconds).
10:53:04 <Ilari> IIRC, the model is exponential or quadric demand...
10:53:24 -!- cheater00 has joined.
10:55:23 <Ilari> I think one of the estimates uses exponential model and one uses quadric model. But the amount of data those use is rather large, so effects from IANA depletion (including effects before it) are not taken into account...
10:55:43 <Phantom_Hoover> Quadric? Do you mean quadratic or quartic?
10:57:03 <Ilari> 2nd order...
11:08:30 -!- Wamanuz2 has quit (Read error: Operation timed out).
11:08:57 -!- Wamanuz2 has joined.
11:21:18 -!- Wamanuz3 has joined.
11:24:08 -!- Wamanuz2 has quit (Ping timeout: 240 seconds).
11:59:15 -!- Wamanuz3 has quit (Remote host closed the connection).
12:12:31 -!- cheater00 has quit (Ping timeout: 240 seconds).
12:13:02 -!- cheater00 has joined.
12:13:15 -!- BeholdMyGlory has joined.
12:14:38 -!- Wamanuz has joined.
12:39:35 -!- wth has joined.
12:39:43 -!- wth has left (?).
13:46:06 -!- Slereah has joined.
13:51:57 -!- pikhq has quit (Ping timeout: 255 seconds).
14:02:35 -!- pikhq has joined.
14:07:43 -!- pikhq has quit (Ping timeout: 240 seconds).
14:19:02 -!- pikhq has joined.
15:06:50 -!- Phantom_Hoover has quit (Ping timeout: 240 seconds).
15:11:52 <variable> wtf with U+263A ?
15:11:59 <variable> why is that a symbol :-\]
15:51:19 -!- Sgeo has joined.
16:14:25 -!- azaq23 has joined.
16:15:01 <fizzie> variable: If you don't like the single smiley, you probably hate the 1F600 block: http://www.unicode.org/charts/PDF/U1F600.pdf
16:16:07 -!- azaq231 has joined.
16:16:22 -!- azaq231 has quit (Changing host).
16:16:22 -!- azaq231 has joined.
16:17:33 <fizzie> Includes such gems as the CAT FACE WITH TEARS OF JOY, the KISSING CAT FACE WITH CLOSED EYES, and the {SEE,HEAR,SPEAK}-NO-EVIL MONKEY triplet.
16:18:24 -!- azaq23 has quit (Ping timeout: 240 seconds).
16:19:22 <Ilari> Sadly those are astral characters... ☹
16:19:57 <fizzie> Well, we'll always have the snowman.
16:20:30 <fizzie> And the nicely zen U+26C4 SNOWMAN WITHOUT SNOW.
16:20:45 <fizzie> "What, is that, like, a man?"
16:21:08 <fizzie> (It's actually just snowman without a snowfall background.)
16:22:42 <Ilari> It is a weather symbol?
16:22:48 <fizzie> Yes.
16:23:00 <fizzie> It's for "light snow"; and the BLACK SNOWMAN is for "heavy snow".
16:29:32 <variable> its like someone said "we have all these code pages - so lets use them for our random (crappy) art!
16:35:45 -!- Phantom_Hoover has joined.
16:37:13 -!- FireFly has joined.
16:47:45 -!- Behold has joined.
16:48:37 -!- BeholdMyGlory has quit (Ping timeout: 255 seconds).
16:56:02 -!- Mannerisky has joined.
17:00:23 -!- cheater00 has quit (Ping timeout: 240 seconds).
17:01:04 -!- asiekierka has joined.
17:01:05 -!- cheater00 has joined.
17:05:22 <Vorpal> <Ilari> Sadly those are astral characters... ☹ <-- ?
17:06:04 <fizzie> Characters outside the BMP are called "astral".
17:06:10 <Vorpal> ah
17:06:16 <Vorpal> why is it sad they are outside BMP?
17:06:31 <fizzie> That I don't know; maybe because those are still often broken?
17:09:25 <Ilari> Yeah, sometimes BMP characters work but characters outside it are broken.
17:09:50 <Vorpal> mhm
17:11:58 <coppro> UTF-16 applications in particular hate astral characters
17:12:00 <fizzie> I can believe there's quite a lot of Java code that doesn't do UTF-16 properly, just assumes a "char" can hold any character.
17:12:04 <coppro> because often they're really using UCS-2
17:12:08 <coppro> like Java code
17:12:09 <coppro> or KDE
17:12:29 <coppro> also, there are no easy fonts to cover the astral planes like unifont
17:13:22 <Phantom_Hoover> Did I mention that the Scottish 5th-year computing course states in no uncertain terms that Unicode is a 16-bit character encoding?
17:13:58 <Vorpal> ......
17:14:02 <Sgeo> Lies to Children?
17:14:05 <Vorpal> anyway night →
17:14:11 <Phantom_Hoover> Sgeo, not even that.
17:14:46 <Phantom_Hoover> Lies to children are oversimplifications which are needed for basic understanding, not blatant falsehoods.
17:15:14 * Phantom_Hoover reads Boatmurdered.
17:15:20 <Phantom_Hoover> This is the funniest thing ever.
17:15:29 <olsner> and it's probably not so much lies as merely "insufficient clue when teaching was made"
17:15:31 <Phantom_Hoover> [[The Manager demanded a clear glass window in his room. To fucking look at what, I asked him. Your room doesn't have a hole leading to the outside. Your room doesn't have a view of anything. The best I can do is put in a window that is 2 feet away from a stone wall.]]
17:16:28 <coppro> Phantom_Hoover: there is one Scottish 5th-year computing course?
17:16:41 <Phantom_Hoover> coppro, yes.
17:16:54 <coppro> Phantom_Hoover: all the post-secondaries are standardized or something?
17:17:05 <Phantom_Hoover> Erm, fifth year of high school.
17:17:08 <coppro> oh
17:17:32 <coppro> write angry letters to newspapers about them teaching falsehood
17:17:36 <coppro> with detailed citations
17:17:38 <Phantom_Hoover> (Which is different in Scotland and England for hysterical raisins.)
17:20:19 -!- BeholdMyGlory has joined.
17:21:13 <Phantom_Hoover> (Well, not so much hysterical as the fact that the two have entirely separate education systems.)
17:21:15 -!- Behold has quit (Ping timeout: 265 seconds).
17:22:22 -!- cheater00 has quit (Ping timeout: 240 seconds).
17:22:46 -!- cheater00 has joined.
17:26:21 <Ilari> Hah... Post that calls Somalia "no longer a nation but an area on the map.". :-)
17:27:29 <Phantom_Hoover> I thought it'd been like that for ages.
17:27:58 <Ilari> Yeah...
17:31:23 <Phantom_Hoover> [[I've started project "Fuck The World", a top secret attempt to funnel magma to the outside. I'll kill those elephants. I'll kill *_all_* those fucking elephants.]]
17:31:43 <Phantom_Hoover> This is even funnier than Tom Francis. This is even funnier than the Yogscast.
17:32:16 <Sgeo> Phantom_Hoover, I've read Boatmurdered
17:32:35 <Phantom_Hoover> Sgeo, spoil it and you and all you care about will die.
17:42:03 <Phantom_Hoover> http://scriptor.github.com/pharen/index.html
17:42:11 <Phantom_Hoover> I feel that this person should be shot.
17:46:28 <olsner> hmm, the english for "execution by firing squad" is boring
17:46:32 <Sgeo> Isn't part of the problem with PHP the standard library?
17:53:31 <Phantom_Hoover> olsner, what's interesting about the Swedish?
17:54:42 <olsner> mostly that it's a proper word
17:55:19 <Phantom_Hoover> Obviously it's the Swede's method of choice.
17:55:37 <olsner> "arkebusering", iirc arcebus means rifle in some language like latin
17:55:56 <Phantom_Hoover> Rifling, then?
17:59:05 -!- FireFly has quit (Quit: swatted to death).
18:01:10 -!- FireFly has joined.
18:01:33 -!- cheater00 has quit (Ping timeout: 240 seconds).
18:02:00 -!- cheater00 has joined.
18:03:19 -!- Behold has joined.
18:04:21 -!- BeholdMyGlory has quit (Ping timeout: 240 seconds).
18:04:23 -!- Behold has changed nick to BeholdMyGlory.
18:05:59 <Gregor> You know who else liked invoking Godwin's law? HITLER.
18:08:16 -!- elliott has joined.
18:09:18 <Phantom_Hoover> Dwarf Fortress world generation + Minecraft gameplay: the best thing ever?
18:09:51 <elliott> Isn't DF gameplay just MC gameplay++?
18:10:15 <Phantom_Hoover> Isn't it management of AI dwarfs?
18:11:03 <elliott> 16:43:23 <variable> its like someone said "we have all these code pages - so lets use them for our random (crappy) art!
18:11:09 <elliott> variable: all the crap in unicode is for backwards-compatibility.
18:11:26 <elliott> Phantom_Hoover: I think partly, but you definitely mine a lot...
18:11:42 <variable> elliott, I know
18:11:47 <elliott> :p
18:11:54 <Phantom_Hoover> elliott, yes, but don't you mine by finding some dwarfs and telling them to go and mine?
18:12:07 <elliott> variable: for instance the emoji block was recently added to unicode for interoperability, so some unicode character names actually specify a colour now :)
18:12:10 <pikhq> elliott: And it has a roguelike mode.
18:12:15 <elliott> Phantom_Hoover: Not that I know of, no.
18:12:30 <elliott> Phantom_Hoover: I believe you act as yourself in the game, and keeping the dwarves alive is just your goal.
18:12:32 <variable> elliott, yeap
18:12:40 <pikhq> elliott: Nope.
18:12:46 <elliott> pikhq: What then. :p
18:12:52 <pikhq> elliott: You just order around the dwarves.
18:13:02 <elliott> pikhq: Hmm. But people on the subreddit talk about mining a lot.
18:13:12 <elliott> I guess you can basically order a dwarf around as a third-person-view player.
18:13:15 <Phantom_Hoover> elliott, yes, i.e. ordering dwarves to mine.
18:13:16 <pikhq> Yes, you order them to mine a lot. They're effing dwarves!
18:13:24 <variable> damn - why can't I find the real hustle online that doesn't forever to buffer :-\
18:13:37 <elliott> pikhq: Yeah, but how much mining is "manual"?
18:13:53 <Phantom_Hoover> elliott, *none*!
18:13:54 <elliott> Oh my, the Let's Play archive looks all modern now.
18:14:22 <elliott> pikhq: I mean, do you have to tell it how to branch the mine? Or does it manage it itself?
18:14:31 -!- Wamanuz has quit (Remote host closed the connection).
18:14:47 <pikhq> elliott: Well, if you don't tell it what to do it'll try doing its own thing.
18:14:55 <pikhq> Its own thing may just be bloody stupid, however.
18:14:58 <elliott> And probably die? :p
18:15:26 <pikhq> "Let's mine right next to a magma flow. That's a good OH GOD WHY IS MY FLESH MELTING! OH, THE MIASMA!"
18:15:28 <Phantom_Hoover> (This leads to one of the fundamental tenets of Boatmurdered, i.e. elephant massacres.)
18:15:41 <elliott> Phantom_Hoover: Ha, I just started reading Boatmurdered.
18:15:45 <elliott> [[In a nutshell, Dwarf Fortress is best described as a 2-D base building game in the theme of Dungeon Keeper. The concept is simple, the graphics are simple; but the depth of the game is fairly awesome. (Even more amazing when you realize it is all the product of a single man gaming company.)
18:15:45 <elliott> The dwarves you "control" are somewhat autonomous. They have likes, dislikes, and needs. While you can assign them specific duties and set basic orders, they have minds of their own and will act according to how they feel. You can give them a job, but that doesn't always mean they'll do it right away. Injuries to all animals and dwarves are tracked, down to internal organs and body parts. Dwarves have moods that are affected by the things around
18:15:45 <elliott> them. They can decide to throw a party for their friends, or they might stress out under strain and suddenly kill each other with little to no warning. Female dwarves occasionally get pregnant and, if they are exposed to trauma (say a goblin siege); they very well might miscarry. Sad thoughts caused by things of that nature can lead dwarves to tantrums or even suicide.
18:15:50 <elliott> You begin with 7 dwarves and scarce few supplies at the face of a mountain. Your only objective is to survive the elements while building yourself as cool a fortress as you possibly can before you inevitably die. Simple enough, yes?]]
18:16:29 <Phantom_Hoover> MC + DF: melt your CPU and GPU AT THE SAME TIME!
18:16:40 <elliott> MC is mainly CPU-intensive...
18:16:47 <Phantom_Hoover> Oh?
18:16:47 <elliott> (And even then not *that* much.)
18:16:51 <Phantom_Hoover> It's not even doing much...
18:16:55 <elliott> Phantom_Hoover: Sure, the GPU has a very easy job.
18:17:01 <elliott> Phantom_Hoover: It just has to render gigantic squares, not any detail at all.
18:17:11 <Phantom_Hoover> What's the CPU up to, then?
18:17:11 <elliott> Phantom_Hoover: The CPU has to simulate like 16x16 chunks.
18:17:29 <elliott> A chunk is 16x16x238.
18:17:34 <elliott> OK, the 9x9 chunks are loaded.
18:17:42 <elliott> *128
18:17:43 <elliott> So 144x144x128.
18:17:53 <elliott> Phantom_Hoover: 144*144*128 = 2,654,208.
18:18:11 <elliott> Phantom_Hoover: Answer: It's simulating MC's warped version of physics on two and a half million blocks every frame.
18:18:12 <Phantom_Hoover> Yes, but next to none of that is doing anything.
18:18:13 <elliott> Well, every tick.
18:18:23 <elliott> Phantom_Hoover: It still has to *look* at them to figure out *if* anything is happening.
18:18:34 <elliott> Phantom_Hoover: Especially water and lava flow are intensive.
18:18:49 <elliott> Yes, the game could be optimised, but it's never going to run on a 486.
18:19:45 <elliott> Phantom_Hoover: THE DWARF FORTRESS INTRO IS AMAZING
18:20:01 <elliott> Hey, the title screen gives me an even longer name with which to refer to the game!
18:20:02 <Phantom_Hoover> HAVE FUN MICROMANAGING
18:20:15 <elliott> Slaves to Armok: God of Blood, Chapter II: Dwarf Fortress: Histories of Cupidity and Diligence, v0.31.188
18:20:17 <elliott> *.18
18:20:25 * Sgeo imagines GoTris
18:20:49 * Phantom_Hoover imagines SgeoTris.
18:20:53 * Sgeo should shut up
18:20:59 <elliott> "Use 824693 to scroll."
18:21:11 * Phantom_Hoover has a numpad.
18:21:21 <elliott> Phantom_Hoover: On your /laptop/?
18:21:26 <Phantom_Hoover> YES
18:21:30 <Phantom_Hoover> IT IS SO CRAZY
18:21:38 <elliott> Phantom_Hoover: Ah, an 18" lugtop.
18:22:00 <Phantom_Hoover> How do I put it on top of a lug.
18:22:05 <Phantom_Hoover> That makes no sense.
18:22:31 <elliott> lmao, you can make a 17x17 world
18:22:35 <fizzie> They put numpads in ~16" laptops nowadays.
18:22:36 <elliott> and the largest is 257x257
18:22:39 <elliott> fizzie: Yes yes yes.
18:22:58 <fizzie> Also it could be one of those fancy external numpads.
18:23:26 <elliott> World generation is going pretty fast for me.
18:23:35 <elliott> I think it's almost done with the default settings.
18:23:46 <elliott> Done.
18:24:03 <Phantom_Hoover> There's a video on YouTube of someone massacring some elves he didn't like by opening a portal to hell and giving the flood of demons convenient stairs into their village.
18:24:17 <Phantom_Hoover> Well, not "portal".
18:24:18 <elliott> :D
18:24:52 <Phantom_Hoover> More "gaping hole in the adamantine seal over a hole in what amounts to bedrock in DF".
18:26:22 <elliott> Holy shit this is complicated.
18:26:34 <elliott> Phantom_Hoover: I've always thought that the Nether's roof should be the world's floor.
18:26:43 <elliott> And you should enter the Nether by instead somehow poking a hole in bedrock.
18:26:47 <elliott> And floating down.
18:27:24 <elliott> HOW DO YOU PLAY THIS GAME
18:27:28 <Phantom_Hoover> If the chunk height could actually be extended like that, adding the Nether beneath the world would be the least thing to do.
18:27:34 <Phantom_Hoover> http://df.magmawiki.com/index.php/DF2010:Quickstart_guide
18:27:46 -!- augur has changed nick to augur[afk].
18:27:56 <elliott> Actually the floating down should just be accomplished by putting sand down there.
18:28:03 <elliott> It's OK if things are manual, Notch.
18:28:05 <elliott> also -minecraft
18:28:41 <elliott> Oh, I did not actually realise I could customise my dwarves, so I guess I just have some random dudes.
18:29:16 <elliott> DF's music is amusing.
18:32:37 -!- Wamanuz has joined.
18:44:22 -!- Slereah has quit.
18:46:22 -!- Behold has joined.
18:47:32 -!- cheater00 has quit (Ping timeout: 240 seconds).
18:48:09 -!- cheater00 has joined.
18:49:35 -!- BeholdMyGlory has quit (Ping timeout: 250 seconds).
18:53:08 -!- oerjan has joined.
19:03:49 -!- Slereah has joined.
19:04:43 -!- augur[afk] has changed nick to augur.
19:08:19 -!- cheater00 has quit (Ping timeout: 240 seconds).
19:08:43 -!- cheater00 has joined.
19:22:34 <Sgeo> Is Disallow: /?blockme= valid in robots.txt?
19:22:52 <Sgeo> For some reason, I was under the impression it had to end with /
19:24:03 <Deewiant> The "Disallow" field specifies a partial URI that is not to be visited. This can be a full path, or a partial path; any URI that starts with this value will not be retrieved. For example, Disallow: /help disallows both /help.html and /help/index.html, whereas Disallow: /help/ would disallow /help/index.html but allow /help.html.
19:25:07 <Sgeo> ok
19:25:45 <Sgeo> Anyways, don't visit http://senseis.xmp.net/?blockme=AccessBlocked unless you want your access to Sensei's Library blocked for 48 hours
19:25:50 * Sgeo is so intensely curious
19:27:17 <elliott> Access blocked for about 1 minutes because of misbehaving mirror script.
19:27:18 <elliott> See AccessBlocked for more information once you are unblocked again.
19:27:18 <elliott> If you would like to have a local copy of Sensei's Library,
19:27:18 <elliott> do not mirror this site, but download the SL Snapshot instead.
19:27:18 <elliott> It is less trouble for everyone.
19:27:18 <elliott> /Arno, ahollosi@xmp.net
19:27:36 <elliott> Clicked the AccessBlocked link:
19:27:38 <elliott> Access blocked for about 36 hours because of misbehaving mirror script.
19:30:01 <Ilari> Before one minute timeout?
19:30:13 -!- BeholdMyGlory has joined.
19:31:32 <elliott> Ilari: Clearly :P
19:33:19 -!- Behold has quit (Ping timeout: 250 seconds).
19:35:06 -!- cheater00 has quit (Ping timeout: 240 seconds).
19:35:24 -!- cheater- has joined.
19:40:39 <Ilari> Well, Maybe "giant clusterfuck" was much too optimistic about IPv4 depletion....
19:43:44 <Sgeo> ???
19:44:39 <elliott> Sgeo: EVERYONE IS DYING
19:46:01 <Sgeo> Oh ffs. Mahjong scares me, and I don't even know what it is. Just that some craptastic collection of computer games I had as a kid included some Mahjong game
19:47:33 <oerjan> finally, a job for zzo38!
19:47:37 -!- pikhq has quit (Ping timeout: 240 seconds).
19:48:34 -!- zzo38 has joined.
19:48:55 <zzo38> Open the door and let me in!!
19:49:10 <zzo38> Open the door and let me in!!!!
19:49:21 * Gregor shuts the door.
19:49:54 -!- cheater- has quit (Ping timeout: 240 seconds).
19:49:54 <zzo38> Open the door and let me out!!!
19:50:14 <zzo38> Open the door and let me in!!!!!!!!!!
19:50:20 <Sgeo> "The eternal battle between Helvetica and Arial: the two popular fonts are nigh indistinguishable to civilians, intolerably different to font snobs"
19:51:44 <zzo38> Sgeo: Just let's use Computer Modern Sans Serif, then.
19:52:13 <zzo38> (Unless, of course, you do not like Computer Modern Sans Serif)
19:52:20 -!- pikhq has joined.
19:52:54 -!- Zuu has joined.
19:53:00 <pikhq> Ilari: Yes, "giant clusterfuck" is way too optimistic at this point.
19:53:07 -!- asiekierka has quit (Remote host closed the connection).
19:53:55 -!- Zuu has quit (Remote host closed the connection).
19:54:38 <Ilari> Now the time window to deploy it would be 7 months (and even that might be optimistic...)
19:54:45 <Ilari> *deploy IPv6
19:55:14 -!- Zuu has joined.
19:55:20 -!- cheater- has joined.
20:00:17 -!- cheater- has quit (Ping timeout: 240 seconds).
20:01:51 -!- cheater- has joined.
20:02:57 -!- Zuu has quit (Ping timeout: 260 seconds).
20:07:13 <quintopia> zzo38: i thought about the language we were talking about and instead come up with possibly the most difficult to program language ever invented. I can't even tell if it's TC.
20:07:49 <zzo38> quintopia: Did you type the description?
20:08:49 <quintopia> zzo38: not yet. it's certainly not wiki-ready
20:09:06 <zzo38> OK.
20:10:25 <quintopia> but the basic paradigm is that the only way to do computation is by rearranging the program itself, and the only non-I/O operation is "mark this character to be moved to the end of the program at the end of the next pass"
20:10:48 <quintopia> aka, the program never grows or shrinks, just permutes
20:11:12 <quintopia> need to figure out the best way to add conditionals to it to ensure maximum chances of TCness
20:11:48 <zzo38> You might need also some external memory if the program cannot grow/shrink because otherwise you have limited memory which means is not TCness
20:13:28 <quintopia> actually, that's not true. i think i did come up with a way to make the program grow...
20:13:41 <zzo38> OK. What is the way to make the program grow?
20:14:11 <quintopia> select the same character repeatedly to be moved to the end. it'll only be deleted once, but appended multiple times.
20:14:40 <zzo38> OK, that can work, I think.
20:15:31 -!- Zuu has joined.
20:15:43 <zzo38> I have been thinking of new kind of chess pieces that when your piece is capable of capturing an opponent's piece of the same kind, their piece can never capture yours (if it was their turn).
20:16:23 <zzo38> One kind is a Chinese cannon that jumps over only your own pieces, or a Chinese cannon that can jump over only opponent's pieces.
20:16:28 <quintopia> so two bishops on the same diagonal are protected from one another, basically
20:16:45 <quintopia> oh
20:17:20 <zzo38> quintopia: I am refering to new kind of pieces. One piece can capture the other but not the other way around.
20:17:27 <elliott> <Sgeo> Oh ffs. Mahjong scares me, and I don't even know what it is. Just that some craptastic collection of computer games I had as a kid included some Mahjong game
20:17:30 <elliott> "scares"?
20:17:51 <Phantom_Hoover> Does it scare him as much as perpendicular lines?
20:18:18 <quintopia> zzo38: so irreflexive attackness
20:18:18 <zzo38> quintopia: Do you know Chinese chess (Xiangqi)?
20:18:43 <quintopia> no
20:19:55 <zzo38> In Xiangqi there is one piece that can sometimes attack the opponent's piece of the same kind without being attacked back (but not always). The horse can do this. (Also, there is a way in which any piece other than the kings or advisors can, by having the target blocking the king's view; but this has to do with the rules and not with the pieces.)
20:20:51 -!- Behold has joined.
20:21:17 <zzo38> quintopia: OK. The horse in Xiangqi is like the knight in chess, but cannot jump over other pieces. The cannon moves like a rook when not capturing, but when it is capturing, there must be exactly one piece of any color in between the moving piece and the target piece.
20:21:37 -!- Zuu_ has joined.
20:22:06 <quintopia> ok
20:22:09 -!- Zuu has quit (Read error: Connection reset by peer).
20:22:40 <zzo38> Xiangqi has a few other rules too. The kings and advisors must stay inside of their own palace, the elephants are not allowed to cross the river, and the kings are not allowed to look at each other.
20:22:42 <Sgeo> "scares" was the wrong word
20:22:59 <Sgeo> It's just... it puts me in mind of .. other games such as a 3d pacman thing
20:23:08 -!- pikhq_ has joined.
20:23:09 <Sgeo> Actually, I should look for that game
20:23:37 -!- pikhq has quit (Ping timeout: 276 seconds).
20:23:44 <zzo38> Sgeo: I have played Pacman with 3D view, called 3-Demon. But other idea is to make a Pacman game with 3D grid instead.
20:23:53 <Sgeo> zzo38, that wasn't it
20:23:55 -!- Zuu_ has quit (Read error: Connection reset by peer).
20:24:10 <Sgeo> It was a 3D grid like thing
20:24:16 <Sgeo> It was nonfree in both senses, iirc
20:24:47 -!- BeholdMyGlory has quit (Ping timeout: 276 seconds).
20:25:11 <Sgeo> Found the company
20:25:15 <Sgeo> That made the pack, anyway
20:25:25 <Sgeo> But it seems to have changed focus
20:25:35 <zzo38> Sgeo: Also, some collections have game titled "Mahjong", but it is not always a real mahjong game, some are actually a different game properly called "mahjong solitaire". Mahjong solitaire is not the same game as mahjong although the same tiles are used.
20:25:56 <zzo38> (Nor is poker the same game as bridge, even though both games use the same cards.)
20:26:00 <Sgeo> zzo38, I wouldn't know whether it was real Mahjong or Mahjong solitaire
20:27:05 <zzo38> Sgeo: Real mahjong is played with four players. Mahjong solitaire is played by only one player. (Of course also they are entirely different games, but this is one way to tell the difference.)
20:27:20 <Sgeo> zzo38, I never played the thing
20:27:25 <quintopia> zzo38: we have differently-sized cards for bridge and poker
20:27:30 <Sgeo> I just saw the name in the collection and got bored and moved on
20:28:00 <Sgeo> Although the collection was for mostly single-player games, I think
20:28:02 <zzo38> quintopia: Yes there are differently sized cards, although they are basically the same kind of cards, for many card games.
20:28:10 <Sgeo> Although some of the games had multi-player modes
20:31:15 <zzo38> I also have a collection of single-player computer games, which are free and Free, but some of them require a few modifications if you want to compile them on Free compilers.
20:31:35 <zzo38> (This collection is called the CGA Collection, and it is not yet complete.)
20:33:19 -!- Zuu has joined.
20:33:19 -!- Zuu has quit (Changing host).
20:33:19 -!- Zuu has joined.
20:33:23 -!- oerjan has quit (Quit: leaving).
20:33:27 -!- Zuu has quit (Client Quit).
20:33:39 -!- Zuu has joined.
20:34:58 <zzo38> Invent a game called "Rust monsters has to eat, too"
20:36:19 <Zuu> huh?
20:38:36 <Phantom_Hoover> Is Zuu Danish?
20:38:51 <Zuu> I think he is
20:40:28 <zzo38> What country is ".dk"?
20:42:38 -!- Wamanuz has quit (Remote host closed the connection).
20:43:50 -!- Wamanuz has joined.
20:49:51 <quintopia> so how is it that database systems make complicated queries on structured files fast?
20:50:40 <zzo38> One of the best computer games I have designed is probably Xnazzyball (unfortunately using a proprietary system that works only on Windows; later I might rewrite it in C/Enhanced CWEB).
20:51:06 <zzo38> quintopia: I don't know. Maybe some index tree? Is there a book about such things?
20:51:23 <zzo38> Is there such a database program written by literate programming, then you can learn?
20:54:33 <quintopia> hahaha i doubt it
20:56:11 <elliott> quintopia: indexes
20:56:12 <elliott> :P
20:57:21 <quintopia> no tree?
20:57:27 -!- Phantom_Hoover has quit (Ping timeout: 240 seconds).
20:58:27 <elliott> well sure.
21:01:49 -!- BeholdMyGlory has joined.
21:02:23 -!- Behold has quit (Read error: Operation timed out).
21:06:45 <zzo38> Do you like PBM file? (This is what TeXnicard uses as intermediate output. It goes .cards -> .tex & .mf; .mf -> .tfm & .*gf; .tex & .tfm -> .dvi; .dvi & .*gf -> .pbm & ImageMagick command-line; .pbm & ImageMagick command-line -> various output formats.)
21:07:50 <quintopia> zzo38: how close is texnicard to being as full featured as Magic Set Editor? (in terms of the aspects that aren't specific to MTG)
21:08:30 <Sgeo> <Sgeo> bool isAnswer(int num) { return (num == 42 ? true : false);}
21:08:33 * Sgeo facepalms
21:08:50 <Sgeo> Someone else noticed...
21:09:07 <quintopia> yeah
21:09:11 <quintopia> that's pretty dumb
21:09:13 <quintopia> sry dood
21:09:19 <quintopia> you can't be awesome every time
21:09:27 <zzo38> quintopia: That is unfortunately a difficult question to answer. The best way is to look at the code and decide for yourself (since you may have different measures?).
21:09:59 <quintopia> zzo38: i've never used MSE, so i can't really compare myself :P
21:11:24 <zzo38> Unfortunately it takes a while to write (I think I have most of the core program done except for most of the GF/DVI stuff, but the Plain TeXnicard metatemplate is probably very incomplete. I am currently doing the GF/DVI stuff.
21:13:44 -!- Phantom_Hoover has joined.
21:13:53 <zzo38> quintopia: However, if you would like to help with any parts of it (including documentation, testing, templates, suggestions, discussion, etc) you can notify me and I will add your repo.or.cz username into the Extra repository.
21:14:13 <Sgeo> Phantom_Hoover, you just missed me explaining how I made a fool of myself in another channel
21:15:15 <Phantom_Hoover> Sgeo, your brain has been POISONED by IMPERATIVE THINKING.
21:16:31 <zzo38> I am not even sure of the use of the isAnswer function, except possibly where function pointers are used (and the "?true:false" part is unnecessary)
21:18:10 <zzo38> I do need some help with some parts of TeXnicard, so please notify me if you can help with this kind of stuff!!
21:19:55 <zzo38> I know one feature MSE has specific to Magic: the Gathering, is the command to export to Apprentice; I am not sure if there are others. With TeXnicard, exporting to Apprentice must be done in a template just like any other exporting must be.
21:25:37 <quintopia> kthx zzo38 but i don't care about card games really
21:28:16 <zzo38> quintopia: OK, but do you know anyone else who might help with these kind of things?
21:28:58 <elliott> I know my long lost half-brother's cousin, Melvinoid.
21:28:59 <elliott> He is an expert.
21:29:20 <zzo38> elliott: Expert at what?
21:29:32 <elliott> Everything you mentioned.
21:30:11 <zzo38> elliott: Is he on this IRC?
21:30:15 <elliott> No.
21:30:27 <elliott> I could send him some mail but he lives in Africa so the post takes a long time to arrive.
21:32:02 <elliott> zzo38: Sorry, he actually does not exist.
21:32:18 <Phantom_Hoover> zzo38, don't listen to elliott.
21:32:37 <Phantom_Hoover> He is backpedalling so that he can keep Melvinoid to himself.
21:32:38 <zzo38> elliott: Yes it is strange to know your long lost half-brother's cousin, I was partially doubting his existence.
21:33:08 <zzo38> (But it is possible some people do)
21:33:14 <Sgeo> He doesn't exist because you murdered him.
21:33:27 <Sgeo> Dammit, voices don't transmit over IRC
21:33:44 <church> hi
21:33:46 <zzo38> Sgeo: If you have a microphone in your computer, you can record it.
21:34:23 <Sgeo> church, hi
21:35:49 <church> how is everyone
21:35:51 <elliott> church: WHERE IS TURING
21:36:17 <church> dead, son.
21:36:30 <elliott> church: SO ARE YOU, ALONZO
21:36:38 <church> mwop mwop mwop
21:36:44 <church> the how am I watching SCTV
21:36:54 <church> its not even on the AAAAAAAAAAAAAAAAAAAAAAAAAAAAIR
21:37:01 <Sgeo> When did church die?
21:37:31 <church> 199jive
21:38:02 -!- church has changed nick to omen.
21:38:16 <elliott> omen: it's da truth
21:38:31 <omen> womp womp wommmp
21:38:44 <elliott> bitchen
21:38:54 <omen> so whats so esoteric about this place then
21:39:11 <zzo38> omen: Esoteric computer programming.
21:39:33 <omen> zzo38: haha, serious?
21:39:43 <zzo38> omen: Well, sort of.
21:39:47 <elliott> Yes.
21:39:50 <omen> oh
21:39:51 <omen> as in
21:39:59 <omen> a program named Esoteric?
21:40:04 <elliott> Using programs to create magicke.
21:40:06 <zzo38> omen: No.
21:40:08 <elliott> (I'm TOTALLY NOT LYING)
21:40:13 <omen> whaaaaaaaat
21:40:22 <omen> hhwaaat
21:40:22 <zzo38> omen: See the wiki for more information: http://www.esolangs.org/wiki/
21:40:59 <zzo38> However, a lot of things are discussed in this channel, not only esoteric computer programming.
21:41:38 <omen> ..
21:41:42 <omen> where do i go
21:42:04 <zzo38> omen: Read the various pages in the wiki to learn some things.
21:42:19 <zzo38> (Try the page titled "Esoteric programming language" if you want a description)
21:43:08 <zzo38> "An esoteric programming language is a computer programming language designed to experiment with weird ideas, to be hard to program in, or as a joke, rather than for practical use."
21:43:41 <zzo38> omen: Does that help?
21:43:44 <Phantom_Hoover> omen, esoteric programming is that which is too crazy to use.
21:44:10 <Sgeo> Phantom_Hoover, so BancSTAR is considered esoteric?
21:44:27 <Phantom_Hoover> OK, *and too awesome to throw up at
21:44:40 <Sgeo> So PSOX is not esoteric?
21:44:56 <zzo38> Not everyone has quite the same ideas of what is esoteric programming.
21:45:14 <zzo38> Because there is some ambiguous areas. Sometimes you can say some are quasi-esoteric.
21:46:25 <Phantom_Hoover> Is it really as bad as all that?
21:46:42 <zzo38> Phantom_Hoover: Sometimes.
21:47:01 <elliott> PSOX is just boring and lame.
21:47:30 <zzo38> PSOX is not a programming language, it is a I/O layer.
21:47:55 <Sgeo> It's still esoteric programming, just not a language
21:48:34 <elliott> Arguably, the things you send to it are programs.
21:49:24 <Sgeo> Would PSOX2, as once described here, have been more of a language? Or the same
21:50:42 <elliott> Less, I think.
21:50:47 <elliott> Since it'd just forward the input on.
21:51:11 <Sgeo> I think we're thinking of two different PSOX2s
21:51:19 <Sgeo> I meant the one with the turing-complete thingy
21:54:45 <elliott> I was talking about the one that is catbus.
21:55:35 <zzo38> There is also things, such as, dc has something similar to the STASH and RETRIEVE commands in INTERCAL, as well as something similar to the RESUME command in INTERCAL.
21:56:28 <omen> so
21:58:12 <zzo38> omen: Do you know dc or INTERCAL? INTERCAL is the first esoteric programming language, while dc is a UNIX arbitrary precision desk calculator program.
22:00:20 <omen> no
22:00:30 <omen> never heard of this
22:00:53 <zzo38> Learn INTERCAL, then: http://esolangs.org/wiki/INTERCAL
22:01:06 <omen> zzo38: ...
22:01:19 <omen> and why would I do that
22:01:32 <omen> especially if you are already so informed
22:01:33 <elliott> omen sounds boring, let's scare him away.
22:01:44 <omen> haha
22:01:51 -!- elliott has set topic: For the intelligent (and not-so-intelligent) discussion of ESOTERIC PROGRAMMING LANGUAGES ONLY |
22:01:53 <omen> you can try
22:01:56 <zzo38> omen: Just in case you are interested, that is only.
22:02:00 <elliott> omen: That line was not a line about esoteric programming languages.
22:02:23 -!- zzo38 has set topic: For the intelligent (and not-so-intelligent) discussion of ESOTERIC PROGRAMMING LANGUAGES ONLY | | http://tunes.org/~nef/logs/esoteric/?C=M;O=D.
22:04:33 -!- FireFly has quit (Quit: swatted to death).
22:06:08 <omen> for the record
22:06:20 <omen> more melancholy and bored
22:06:25 <omen> than scared, thanks.
22:06:30 -!- omen has left (?).
22:06:33 <Sgeo> DAMMIT
22:06:37 * Sgeo shoots elliott
22:06:56 <elliott> Sgeo: what?
22:07:13 <Sgeo> Deliberately pshing people away annoys me
22:07:16 <elliott> he obviously had not interest in programming or esolangs
22:07:18 <elliott> *no
22:07:27 <elliott> also
22:07:31 <elliott> <church> mwop mwop mwop
22:07:31 <elliott> <church> the how am I watching SCTV
22:07:31 <elliott> <church> its not even on the AAAAAAAAAAAAAAAAAAAAAAAAAAAAIR
22:07:31 <elliott> <Sgeo> When did church die?
22:07:32 <elliott> <church> 199jive
22:07:38 <elliott> ^^^ anybody who says these lines is a terrible person
22:08:01 <elliott> evidence of no interest, apart from the fact that he had no idea what the channel was about:
22:08:01 <elliott> <zzo38> Learn INTERCAL, then: http://esolangs.org/wiki/INTERCAL
22:08:01 <elliott> <omen> zzo38: ...
22:08:02 <elliott> <omen> and why would I do that
22:08:02 <elliott> <omen> especially if you are already so informed
22:08:31 <olsner> http://www.youtube.com/watch?v=0L40f39bPII
22:08:44 <elliott> Sgeo: ergo...
22:09:09 <olsner> (yes, that's me posting one of those "funny youtube videos")
22:09:47 <Sgeo> Emu root?
22:09:50 <elliott> olsner: Maybe this is what Vorpal is really like.
22:09:58 <olsner> elliott: one can only hope
22:10:12 <elliott> olsner: IRC is the only place he can act normal. well ok vaguely normal.
22:10:47 <Sgeo> What.
22:11:48 <elliott> Sgeo: what
22:11:52 <olsner> What.
22:11:58 <Sgeo> What.
22:12:02 <elliott> in the butt
22:13:12 <olsner> "what what what what in the butt"? I don't think that's how it goes
22:15:28 <elliott> :D
22:19:03 -!- MigoMipo has quit (Read error: Connection reset by peer).
22:31:51 -!- Phantom_Hoover has quit (Remote host closed the connection).
22:32:38 <Ilari> Huston said failure rate of 6to4 is 15% on reverse path... That would imply total failure rate of something like 30%...
22:34:31 -!- pikhq_ has changed nick to pikhq.
22:34:46 <pikhq> Ilari: Dang.
22:35:50 <Ilari> Wonder what's failure rate on backward path if forward path is good...
22:39:55 <Ilari> Of course, for provoding "native" IPv6, there's choice of "last mile" technology...
22:59:26 -!- th3b0m has joined.
23:09:07 <Ilari> What a freaking CF was handling that swine flu... Major shoot-in-the-foot for vaccination programs...
23:11:55 <Sgeo> hmm?
23:17:05 <th3b0m> hello
23:17:10 <th3b0m> could someone help me?
23:17:22 <zzo38> th3b0m: With what?
23:17:36 <th3b0m> i wanna make a permanent irc channel...
23:17:47 <zzo38> th3b0m: On Freenode?
23:17:53 <th3b0m> yeah
23:18:10 <zzo38> First you need to register with NS REGISTER and then register the channel with CS REGISTER.
23:18:18 <elliott> th3b0m: #freenode
23:18:21 <elliott> this is not a support channel
23:18:32 <zzo38> (Use NS HELP REGISTER for help about registration of nickname, and CS HELP REGISTER for help about registration of channel.)
23:18:42 <zzo38> And, like elliott said, the support channel is #freenode not this one.
23:18:54 <th3b0m> so ok thankyou for helping me
23:19:42 <th3b0m> NS HELP REGISTER
23:20:16 <th3b0m> i just tryed doing that and it said i hadnt joined a channel...
23:20:30 <zzo38> th3b0m: You might have to enter /RAW before the command, some IRC clients require that.
23:20:31 <th3b0m> join #freenode
23:20:42 <th3b0m> ok
23:20:51 <zzo38> Or you might have to use a menu. Some IRC clients use menus.
23:24:51 <th3b0m> ok
23:25:11 <th3b0m> well, i got the registration of my nickname working correctly
23:25:32 -!- yorick has quit (K-Lined).
23:25:41 <zzo38> th3b0m: You need to complete the verification.
23:25:46 <th3b0m> it was : /RAW NS REGISTER (password) (my email)
23:25:59 <zzo38> You should receive an email message that contains the verification code and instruction about how to complete verificiation.
23:26:06 <th3b0m> yeah i no but the e-mail hasnt arrived yet
23:26:20 <zzo38> OK, then you must wait for that before you can register the channel.
23:26:33 <th3b0m> yea
23:26:41 <th3b0m> and can i password protect the channel?
23:26:46 <zzo38> Remember this IRC network is meant for Free software/Open source projects, so most channels created should have something to do with that.
23:27:01 <zzo38> th3b0m: Yes, you can password protect the channel: MODE (channelname) +k (password)
23:27:08 <zzo38> (Again, enter /RAW before the command)
23:27:14 <th3b0m> yeah my channel does
23:27:16 <th3b0m> ok
23:27:49 <th3b0m> i no stuff about hacking, and coding not irc stuff lol
23:27:59 <th3b0m> so thanks for ur help
23:28:21 <zzo38> th3b0m: Good, because computer programming is the main purpose of this IRC network.
23:28:33 <th3b0m> uhhu
23:28:48 <th3b0m> and our prposes for this channel
23:28:53 <th3b0m> should support
23:28:55 <th3b0m> it
23:29:30 <zzo38> OK. However, although I can help you on this channel, the proper channel for discussing inquiries about this IRC network is the #freenode channel.
23:29:32 <elliott> th3b0m: "hacking".
23:29:53 <elliott> 1337 hax0rz? W3 are l00king for Dz33em!
23:30:05 <th3b0m> 4r3 y0u
23:30:06 <th3b0m> ?
23:30:39 <elliott> th3b0m: y3sZ
23:30:39 <zzo38> You can discuss hacking on your channel too, as long as it is related to the Free software and that you are not discussing anything illegal.
23:30:52 <th3b0m> ok
23:30:53 <zzo38> Do not use this network for illegal discussion.
23:31:15 <elliott> th3b0m: j01n us... type /j #2,000
23:31:22 <elliott> bcause we are two thousand str0ng
23:31:27 <th3b0m> 0k
23:31:57 <th3b0m> did t work?
23:32:06 <elliott> th3b0m: hmm, no
23:32:18 <elliott> th3b0m: there is a secret way to get in, try /join 0
23:32:25 <elliott> don't tell anybody ;)
23:32:28 -!- th3b0m has left (?).
23:32:43 <zzo38> This channel is logged anyone can read that. And anyways that won't work
23:32:53 <elliott> thank god
23:33:03 <elliott> we've got a lot of off-topic morons today...
23:33:13 -!- th3b0m has joined.
23:33:20 <zzo38> elliott: Yes we have.
23:33:24 <th3b0m> it failed...
23:33:30 <elliott> th3b0m: no it worked, you have to wait five minutes after doing it
23:33:36 <zzo38> th3b0m: No it won't work.
23:33:49 <zzo38> The correct way is to type "#freenode" instead of "0"
23:34:15 <th3b0m> do can u give me the exact code for me to use?
23:34:21 <th3b0m> so itll join me
23:34:56 -!- th3b0m has set topic.
23:35:03 <zzo38> th3b0m: I don't know the name of your channel.
23:35:04 <th3b0m> whoops!
23:35:06 <elliott> th3b0m: yes, type this: /part of us
23:35:06 <th3b0m> ill fix it
23:35:15 -!- Deewiant has set topic: For the intelligent (and not-so-intelligent) discussion of ESOTERIC PROGRAMMING LANGUAGES ONLY | | http://tunes.org/~nef/logs/esoteric/?C=M;O=D.
23:35:17 -!- th3b0m has set topic: For the intelligent (and not-so-intelligent) discussion of ESOTERIC PROGRAMMING LANGUAGES ONLY | | http://tunes.org/~nef/logs/esoteric/?C=M;O=DFor the intelligent (and not-so-intelligent) discussion of ESOTERIC PROGRAMMING LANGUAGES ONLY | | http://tunes.org/~nef/logs/esoteric/?C=M;O=D.
23:35:20 -!- Deewiant has set topic: For the intelligent (and not-so-intelligent) discussion of ESOTERIC PROGRAMMING LANGUAGES ONLY | | http://tunes.org/~nef/logs/esoteric/?C=M;O=D.
23:35:33 <th3b0m> /part of us
23:35:49 <th3b0m> it leaves the channel!
23:36:10 <zzo38> I do not know the code to use to join your channel. Use your own channel name in place of the this one and read the XChat documentation for more help.
23:36:12 <elliott> th4t's b3cause y0u are not yet 4uthentic4ted
23:36:54 <th3b0m> im authenticated now
23:36:59 <th3b0m> just got the e-mail
23:37:13 <zzo38> th3b0m: OK. Now use the CS REGISTER command to register your channel.
23:37:22 <elliott> th3b0m: authenticated with our hax0rzz!
23:37:56 <th3b0m> zzo38: how many diff channels can i have?
23:38:05 <th3b0m> elliot: how do i authenticate?
23:38:27 <elliott> th3b0m: you must disconnect and reconnect in an hour...i've started the process now
23:38:28 <zzo38> th3b0m: You have already authenticated. I do not know how many channels you are allowed to have, ask that question on #freenode
23:39:30 <th3b0m> just did
23:40:00 <th3b0m> thanks guys for ur help
23:40:14 <th3b0m> btw, how do u then join the channel when it has a password?
23:40:25 <zzo38> th3b0m: Give the password after the channel name in the JOIN command.
23:40:29 <elliott> th3b0m: it's impossible
23:42:28 <th3b0m> kk
23:54:18 -!- oerjan has joined.
←2011-01-29 2011-01-30 2011-01-31→ ↑2011 ↑all