00:02:02 <j-invariant> I think F-algebra will work for all simple data types
00:02:35 <elliott> j-invariant: lol you might want to try and make your library multiple files
00:02:46 <elliott> it's gonna be like 10,000 lines when you're done
00:03:23 <elliott> j-invariant: I think "Require Import Foo." will work if Foo.v is in .
00:03:38 <j-invariant> it would be good to compile each bit seperately
00:04:06 <elliott> j-invariant: if you ever manage to construct lists and map inside this ... I dare you to extract "map"
00:04:20 <elliott> it'll be the ugliest fucntion ever
00:04:34 <j-invariant> I might be able to contribute to Evolution of a haskell programmer...
00:06:32 <elliott> j-invariant: I wish Coq did some ugly special-casing for nats ... they're so slow and limited
00:06:39 <elliott> I know there's the binary nats somewhere, but ...
00:07:01 <j-invariant> yeah numbers must be implemented in binary, peano is only useful for theory
00:07:25 <elliott> j-invariant: still, even the binary nats aren't so hot
00:07:34 <elliott> j-invariant: I'd like it if it just special-cased nat and represented it internally as a machine word / bignum
00:07:43 <elliott> but still allowed you to destruct on S to decrement one, etc
00:08:04 <elliott> fact and the like would be slow, but they wouldn't use up 34238490424 jiggabytes of memory
00:08:37 <j-invariant> I mean where would the implemeentaiton get the idea to use binary?
00:08:49 <j-invariant> and more generally what else could it optimize
00:08:54 <elliott> j-invariant: oh, I meant just hardcoding it ;-)
00:08:57 <elliott> it's ugly as hell, certainly
00:09:15 <j-invariant> yes numbers seem to be special in some sense
00:09:43 <elliott> what do you mean? you mean that numbers tend to be more useful/common than non-number structures?
00:10:01 <elliott> I think that's because we looked at the most useful algebraic structures and called them numbers, and decided the less useful ones didn't count as numbers
00:10:57 <elliott> Gregor: I think I will build it on top of cunionfs... is performance ok? i've always felt like fuse is slow but that may just be bias
00:11:22 -!- Sgeo has joined.
00:11:33 <j-invariant> natural numbers are universal in the category of discrete dynamical systems
00:12:13 <elliott> j-invariant: i think it may be due to our bias -- we think numbers are interesting, so we tend to look more into something once we see numbers appear
00:12:16 <elliott> and disregard things that aren't so numbery
00:12:20 <elliott> I mean, in a very general sense
00:12:25 <elliott> thus why numbers seem pretty darn common
00:12:56 <j-invariant> elliott: I cannot come up with any counter-argument to that but I don't think it's true
00:13:13 <elliott> j-invariant: when in doubt, i like to blame humans :)
00:13:21 <Vorpal> gah some words got stuck on my head
00:13:22 <elliott> j-invariant: i mean, let's put it this way
00:13:34 <elliott> j-invariant: there's as much mathematics not involving numbers as there is mathematics involving numbers.
00:13:38 <Vorpal> for some reason I keep thinking of the phrase "high performance JIT cheese"
00:13:47 <elliott> j-invariant: so the /only/ factor in consideration here is, why do the mathematics /we've explored/ involve numbers a lot?
00:13:51 <elliott> and i suspect the answer is: because we like numbers
00:14:23 <Gregor> elliott: I haven't tested performance much 8-D
00:14:32 <elliott> Gregor: That is not reassuring :-\
00:14:42 <elliott> Gregor: https://codu.org/projects/trac/sps/changeset/6%3A8584c8e2c0ed/cunionfs Why did you do this, I don't like it :p
00:14:58 <elliott> sprintf(dotfile, "%s%s", curd, CUNIONFS_DOTFILE);
00:15:05 <elliott> oh wait you allocate it later
00:17:39 <Gregor> elliott: I do that so that you can't cause packages to do things they ought to be finding files at weird paths which just-so-happen to have the right names.
00:17:56 <elliott> Gregor: Your sentence does not parse.
00:18:01 <elliott> "cause packages to do things they ought to be finding files at weird paths"
00:18:38 <Gregor> elliott: I do that so that you can't cause packages to do things they oughtn't to by finding files at weird paths which just-so-happen to have the right names.
00:20:30 <Gregor> You have / mounted as cunionfs, and a version of sudo that isn't smart about checking the permissions of the sudoers file (it assumes only root can write to /etc). You make your own sudoers file in /home/mrhappy/evil/etc/sudoers, then mount that over / with cunionfs.
00:21:18 <elliott> Gregor: Heh. Actually come to think of it I'll probably end up with / being an aufs of {regular filesystem, cunionfs for /bin /lib /share etc.}
00:21:28 <elliott> e.g., process-specific /var and /home sounds "no".
00:21:44 <elliott> Union of a union... you know what, this is an EXCELLENT argument for /usr.
00:22:29 -!- hagb4rd has joined.
00:22:37 <Gregor> That's just a specific case, it's not really solved by contracting your unions a bit :P
00:23:00 <Gregor> And no, I assumed you'd have something else mounted over /var, /home and /root if you don't have /home/root, those are all silly to union.
00:23:05 <Vorpal> elliott, as expected, getting lava from spawn no longer works
00:23:18 <j-invariant> elliott: could a brain exist which was obsessed with something other than numbers?
00:23:42 <elliott> j-invariant: Sure, why not.
00:24:00 <elliott> j-invariant: I don't see why.
00:24:11 <elliott> Gregor: Maybe I'll have no /bin, /lib, /share, and put it all in a cunionfs /usr :P
00:24:23 <elliott> Gregor: / = {/usr, /var, /home, /tmp, /boot} or something.
00:24:30 <elliott> Gregor: / = {/usr, /var, /home, /tmp, /boot, /etc} or something.
00:24:43 <Gregor> That was the original intention behind SPS :P
00:24:58 <Gregor> Well, I had a /bin and /lib for really-core stuff (libc, coreutils)
00:25:15 <Gregor> (So that if for some reason your package setup was punked, you weren't completely screwed)
00:26:31 <elliott> Gregor: <Gregor> Well, I had a /bin and /lib for really-core stuff (libc, coreutils)
00:26:35 <elliott> Gregor: cal(1) is really-core? :P
00:26:57 <Gregor> Dude, my system won't even BOOT without cal.
00:27:32 <elliott> Gregor: The nice thing is that with Kitten, you're always completely screwed.
00:27:35 <elliott> So I don't have to worry about that
00:27:55 <Vorpal> Gregor, did you have stuff like fsck and mount in /bin too?
00:28:08 <elliott> Gregor: On a more srs note, I can't really have a cunionfs /, because I have no initramfs in Kitten :P
00:28:12 <elliott> So / kinda has to be a real drive.
00:28:26 <elliott> switch_root moves already mounted /proc, /dev and /sys to newroot and makes newroot the new root filesystem and starts init
00:28:26 <elliott> WARNING: switch_root removes recursively all files and directories on the current root filesystem.
00:28:28 <elliott> I wonder why it has to do that.
00:29:17 <Vorpal> elliott, to shrink the tmpfs size to 0 iirc
00:31:31 <elliott> Gregor: Do I get extra points if my package manager is Haskell?
00:32:30 <Gregor> BECAUSE HASKELL KILLED MY FAMILY
00:33:00 <Gregor> OMG JOIN US IN ##haskellkilledmyfamilyanonymous
00:33:43 <elliott> Gregor: Actually, shipping Haskell with a statically linked system sounds slightly stupid, as the executable will probably be around 100 MiB :P
00:36:55 <Gregor> I wouldn't be surprised if GHC can't even make static executables (without some hacking)
00:37:12 <elliott> Gregor: It can, I just tried.
00:37:21 <Gregor> Well, THERE GOES THAT THEORY.
00:37:25 <elliott> elliott@dinky:~$ ghc hello.hs -static -optl="-static" -optl="-pthread" ; ls -lh a.out
00:37:25 <elliott> compilation IS NOT required
00:37:26 <elliott> -rwxr-xr-x 1 elliott elliott 1.7M Dec 24 00:36 a.out
00:37:39 <elliott> -rwxr-xr-x 1 elliott elliott 1.2M Dec 24 00:37 a.out
00:38:28 <elliott> That's actually pretty damn good ...
00:40:32 <elliott> Gregor: Dammit man -- the package manager has to be functionally pure now.
00:40:39 <elliott> Gregor: You've turned my OS into a bad recreation of NixOS.
00:40:50 <elliott> Gregor: _|_, and that's a middle finger, not the bottom value.
00:42:15 <elliott> Gregor: Is "nm -a" supposed to work on statically linked executables?
00:42:35 <elliott> hello: ELF 64-bit LSB executable, x86-64, version 1 (GNU/Linux), statically linked, for GNU/Linux 2.6.18, not stripped
00:42:39 <elliott> OK, it did actually work then :P
00:54:03 <elliott> Gregor: Wait, can you add to the unioned directories without restarting a process?
01:00:07 -!- FireFly has quit (Quit: swatted to death).
01:10:05 <zzo38> Guess how many pages there will be when it is done. (Remember it also will have the function to read commands from DVI, as well.) When it is done, we can see how close you are to correct answer.
01:11:09 <zzo38> j-invariant: Are you asking me?
01:12:07 <zzo38> j-invariant: If you are: It is TeXnicard.
01:12:23 <Gregor> elliott: At present, no. Adding that wouldn't be particularly major, and it's something that's in the Eternal Todo o' Abandoned Projects :P
01:12:32 <zzo38> (Remember the page count of 65 pages also includes the index, summary of chunks, and table of contents.)
01:12:55 <elliott> Gregor: that's kinda dealbreaking ... you have to restart your whole X just to see the new package you installed or whatever
01:13:00 <elliott> or even init, if you want it at every levle
01:15:35 <elliott> Gregor: or am i mistaken :P
01:15:42 <zzo38> How I think package manager should work, is, if you want to install a package, you add it to the dependency list of the "locally installed packages" package.
01:15:52 <Gregor> elliott: Adding that wouldn't be particularly major, and it's something that's in the Eternal Todo o' Abandoned Projects. Just need a way to tell the process "I want you to reevaluate my package list like so", probably by a file-write.
01:16:11 <elliott> Gregor: Right, I'm just checking that, in fact, this has the major of issue requiring an effective-reboot to isntall a package :P
01:16:42 <zzo38> Do you like my ideas about package managers? Do you think they are wrong for some reason(s)?
01:16:54 <elliott> zzo38: "based on pipes" isn't very descriptive
01:17:21 <Gregor> elliott: If you want it to be visible to everyone, it's just a matter of putting it in the global configuration file. If you want it to be visible to a user, it's a matter of putting it in their user configuration file. If you want it to be visible to some process or process group, that's more tricky.
01:17:44 <elliott> Gregor: OK, so it rereads the config file all the time?
01:17:51 <elliott> I was unaware that it had configuration files.
01:17:59 <Gregor> elliott: I haven't re-added the configuration files :P
01:18:16 <elliott> Gregor: So what you're TRYING to say is:
01:18:17 <Gregor> elliott: The way it worked in D was with that daemon (the name of which I can't remember) which informs a process when a file has changed.
01:18:23 <elliott> <Gregor> If you want it to be visible to anyone, reboot.
01:18:28 <elliott> <Gregor> If you want it to be visible to a user, reboot.
01:18:33 <elliott> <Gregor> If you want it to be visible to some process or process group, reboot.
01:18:38 <elliott> That is the actual state. Yes? :P
01:18:42 <elliott> <Gregor> elliott: The way it worked in D was with that daemon (the name of which I can't remember) which informs a process when a file has changed.
01:18:45 <Gregor> elliott: Look, you just dug up a project that I abandoned midway and you're expecting it to have features that are still on the TODO list. Fuck you.
01:18:49 <elliott> Gregor: fam, but nobody uses it any more
01:18:59 <elliott> gamin is used, which is a daemonless impl of the api
01:19:07 <elliott> Gregor: I'm not expecting, I'm just /checking/
01:19:17 <elliott> Since your previous statement implied that there were, in fact, configuration files.
01:19:26 <zzo38> elliott: I mean, for example: wg -MR0 ftp://example.org/packages/* | pm -tQ | ...
01:19:38 <Gregor> elliott: You're also expecting me to remember the exact state I abandoned it in.
01:19:51 <elliott> Gregor: Well, you did just say that in retrospect it was pretty awesome earlier :P
01:20:05 <zzo38> elliott: This is just an example of new programs I might make if I make a distro. wg is like wget except that multiple retrieval is sent to stdout as a tape archive.
01:20:12 <zzo38> And pm is package manager.
01:20:34 <elliott> Gregor: I'ma go for aufs, with the magical property of allowing me to remount without reooting :P
01:20:50 <elliott> (Unless "mount -o remount" would work with cunionfs? Wait, FUSE, so no.)
01:21:02 <zzo38> elliott: But what about the other idea, that if you want to install a package, you add it to the dependency list of the "locally installed packages" package?
01:21:43 <zzo38> Do some package managers do that?
01:23:22 <zzo38> Do any package managers work by pipes? Some new programs are not pipe but some old UNIX programs are designed with pipe operation, and I think it is good idea and new programs in UNIX should also work like that too.
01:25:11 <zzo38> I mean, probably some programs on UNIX can already work with pipes, such as: curl http://example.org/mail.tar.gz | zcat | tar -x
01:26:17 -!- Wamanuz2 has joined.
01:27:36 <zzo38> So that is how I want to make a Linux distribution, nearly all program are operated by doing pipes. Including the window manager.
01:31:33 -!- BlSlereah has joined.
01:32:28 -!- hagb4rd has quit (*.net *.split).
01:32:31 -!- augur has quit (*.net *.split).
01:32:31 -!- Wamanuz has quit (*.net *.split).
01:32:40 -!- Slereah has quit (*.net *.split).
01:32:50 -!- augur has joined.
01:45:08 <elliott> fizzie: So, I come out of the track from nailor's cabin. Floor is obsidian. I break my cart while in it as usual. Normally I go into the lava below and catch fire for like, 0.25s before going back to normal. Except this time, I *stayed in the fire, died, and lost all my possessions*.
01:45:14 <elliott> fizzie: I WANT MY FUCKING STUFF BACK, NOTCH ;__;
01:48:29 -!- pikhq has quit (Ping timeout: 250 seconds).
01:50:29 -!- pikhq has joined.
01:58:53 -!- hagb4rd has joined.
02:07:17 -!- zzo38 has quit (Quit: If God Had Intended Us To Play In Ten Tones Per Octave, Then He Would Have Given Us Ten Fingers.).
02:07:37 <j-invariant> I am sick of trying to defin a symbolic category, it's really hard
02:07:45 <elliott> H : (p ^ 3 <= 3 * ' q ^ 3)%Z
02:07:45 <elliott> ============================
02:07:47 <elliott> | p0 # q0 => (p0 ^ 3 <= 3 * ' q0 ^ 3)%Z
02:09:17 <elliott> j-invariant: i.e. "given an underestimate of 3root(3), generate a closer underestimate"
02:14:24 <elliott> j-invariant: any ideas? :/
02:16:06 <j-invariant> p/q |--> (2*p^3 + 3*q^3)/(3*q*p^2) tends toward the cube root of 3 but it never satisfies p^3 <= 3q^3
02:16:38 <j-invariant> if you look at the continued fraction you get one on either side of cuberoot(3), so you could just take all the odd ones... but that means implementing all the continued fraction stuff
02:18:21 <elliott> j-invariant: yeah and that kinda defeats the point
02:18:47 <j-invariant> you can get a recurrence from the continued fraction for quadratics, but I think there is a theorem that says a state machine can't generate the continued fraction of any higher irrationality
02:18:49 <elliott> j-invariant: I think this "computable Dedekind cut" approach would be nice if not for the proofs :/
02:19:18 <elliott> j-invariant: really? that theorem
02:19:24 <elliott> j-invariant: would mean you can't use continued fractions for computable reals...
02:22:45 <j-invariant> The continued fraction expansion of an algebraic number of degree at least
02:22:45 <j-invariant> three cannot be generated by a finite automaton.
02:23:55 <elliott> j-invariant: that's not good is it?
02:24:05 <elliott> j-invariant: I mean could Coq do it? I don't actually know what computational class Coq is
02:26:51 <j-invariant> elliott: my guess is that constructive dedekind cuts are what intuitionists that have never seen a computer use
02:28:37 <elliott> j-invariant: have you ever used c-corn's constructive reals?
02:29:15 <elliott> hm what does :> mean again? in a coq type
02:29:21 <elliott> in a record field declaration
02:29:48 <j-invariant> it's something to do with pretening the record is another type
02:31:46 <elliott> j-invariant: hmm you mean like
02:31:51 <elliott> Record blah := mkBlah { foo :> nat; bar : ... }
02:31:54 <elliott> you could use a blah as a nat?
02:32:56 <j-invariant> well I don't really know I don't use that, but it's something like that
02:33:00 <elliott> j-invariant: I could do algebraic structures like that!
02:33:23 <elliott> leave king dedede... sorry, dede.v for now
02:33:26 <j-invariant> I still haven't been able to define this damned symbolc category
02:33:32 <elliott> j-invariant: what category is it exactly?
02:33:51 <j-invariant> actually it's just graphs, that's a simpler way to think of it.
02:34:18 <elliott> how do you disable the coq stdlib in the file again? :/
02:34:21 <elliott> oh wait i have it here somewhere
02:34:34 <elliott> *** coq-prog-args: ("-emacs-U" "-nois") ***
02:35:03 <j-invariant> The idea is: Inductive Symbolic_Maps : nat -> nat -> Type := f 3 4 | h 2 1 | k 2 1 | m 3 4.
02:35:30 <j-invariant> lets take Inductive Symbolic_Maps : nat -> nat -> Type := f 3 4 | h 4 1 | k 1 6 | m 3 4.
02:35:44 <elliott> is 3 the type w/ three elements?
02:35:54 <j-invariant> no just the number 3, or it could be any symbolc
02:36:50 <j-invariant> then we need something like lists, Inductive Symbolic_Mappings : nat -> nat -> Type := nil : forall x, Symbolic_Mappings x x ; cons : forall a b c, Symbolic_Map a b -> Symbolic_Mappings b c -> Symbolic_Mappings a c.
02:37:34 <j-invariant> So the identity is nil and composition is append.. then things like (f o g) o (k o h) = (f o (g o k)) o h would be provable by reflexivity
02:37:49 <j-invariant> but a functor from Symbolic -> C would prove the same identity in any other category
02:38:26 <j-invariant> right now, to prove (f o g) o (k o h) = (f o (g o k)) o h .. it takes 300 lines of proof script
02:44:10 <elliott> j-invariant: I wish Coq had like, a minimal stdlib with it
02:44:14 <elliott> giving eq, exists, that kind of stuff
02:44:18 <elliott> rather than having to code it myself
02:45:02 <elliott> j-invariant: got a link again?
02:45:21 <j-invariant> http://pastebin.com/BQaW0Cdb this is before I start defining category
02:45:43 <elliott> thanks, I'll nab useful bits from there as I go :)
02:45:50 <elliott> j-invariant: Coq has And/Or built in doesn't it?
02:45:56 <elliott> what does "# Arguments." do :P
02:46:24 <j-invariant> mispaste, should have been Set Implicit Arguments.
02:47:35 <elliott> j-invariant: I think set implicit arguments actually gets in my way
02:47:46 <elliott> it's nice to have to specify what gets implicit-ified
02:49:34 <elliott> Inductive or (P Q : Prop) : Prop :=
02:54:29 * Sgeo assassinates Active Worlds's asinine update methods
02:58:30 <elliott> Error: Unknown interpretation for notation "_ /\ _".
02:58:32 <elliott> what does that mean again?
03:00:48 <elliott> j-invariant: i've defined up to abelian groups, now to watch the whole thing fall apart as i try and do rngs
03:01:09 <elliott> j-invariant: because it's a combination of two structures, basically
03:01:15 <elliott> j-invariant: and my structures have set fields
03:01:23 <elliott> j-invariant: I might restructure them to be Prop-records parameterised on type
03:01:27 <elliott> but IIRC that didn't work last time I tried
03:01:40 <j-invariant> this really sucks, F(f o g) doesn't evaluate to Ff ' Fg, should have known that
03:02:10 <j-invariant> they are equal, but F(f o g) evaluates to Ff o (Fg o Fidentity) -- because of the way the category is made
03:02:41 <j-invariant> but if I make composition syntactic in the symbolic category then I don't get the proofs for free.. damned either way
03:03:28 <elliott> i mean do you write pr_ag or pr_sg
03:03:40 <elliott> if I could refer to the record itself somehow there, that might work
03:03:55 <elliott> j-invariant: who needs proofs for free :)
03:04:29 <j-invariant> http://coq.pastebin.com/DzVkdQbV <- broken
03:04:59 <elliott> j-invariant: i did your proof
03:05:02 <elliott> j-invariant: just add one line
03:05:05 <j-invariant> elliott: I'll just use a syntactic compose, and write a decision theorem
03:08:15 <elliott> mg_op : mg_S -> mg_S -> mg_S
03:08:15 <elliott> Implicit Arguments mg_op [S m].
03:08:16 <elliott> Theorem magma_is_set : forall S (m : magma S), mg_S m = S.
03:10:06 <elliott> j-invariant: just checking coercion works :P
03:10:44 <j-invariant> the biggest problem for me is I don't want to use Set
03:11:01 <j-invariant> I need something like NxN/~ for some equivalence
03:11:10 <j-invariant> I thought category theory would solve it :/
03:13:02 <elliott> j-invariant: category theory solves EVERYTHING!!!!!!!
03:13:20 <j-invariant> it bloody well better after all this hard work :p
03:18:29 <elliott> j-invariant: i got pseudorings!
03:19:52 <elliott> j-invariant: got any nice theorems about pseudorings/rngs? :p
03:19:56 <elliott> i wanna see if this actually works
03:20:29 <elliott> j-invariant: http://en.wikipedia.org/wiki/Pseudo-ring
03:20:43 <elliott> j-invariant: abelian ring (R,+) and semigroup (R,*) where * and + distribute
03:22:22 <elliott> Pseudoring with identity element 1 for • (monoid)
03:22:35 <elliott> so i just need it to be that my pseudo-ring's semigroup must be a monoid too
03:23:32 <elliott> rg_sg_is_monoid : monoid (pr_sg rg_S)
03:24:51 <elliott> j-invariant: heh damn you, i have to figure out what 0 is in this case... the problem is that everyone says * at the lower levels
03:24:54 <elliott> even though it turns into + in higher structurse
03:24:59 <elliott> and everyone says 1 even when it's 0
03:26:50 <elliott> ============================
03:26:53 <elliott> i think this is a problem with my scheme
03:27:00 <elliott> every structure on the same set looks the same to coq
03:28:24 <elliott> ============================
03:28:37 <elliott> j-invariant: are you sure coq doesn't have a tactic for "let me specify this ?385 now"? :(
03:29:08 <elliott> and it becomes the new goal
03:29:46 <elliott> j-invariant: and pushes the current goal to the end
03:30:50 <elliott> j-invariant: surely it must exist, i mean it'd be so useful
03:37:57 <elliott> I think I'm going to write eval in c using exec to call out to gcc, dlopen and dlsym... tomorrow.
03:37:58 -!- Sasha has quit (Read error: Connection reset by peer).
03:37:58 <elliott> ...or just use libtcc, which looks like it can do it out of the box.
03:38:06 -!- Mathnerd314 has quit (Disconnected by services).
03:38:22 -!- Sasha has joined.
03:38:23 -!- Mathnerd314_ has joined.
03:39:00 -!- Mathnerd314_ has changed nick to Mathnerd314.
03:48:11 <elliott> I wonder how I can avoid just reinventing Nix.
03:50:52 <elliott> [[Fair enough response to the half-block question. Real question: How long did it take you to become proficient enough a coder to make Minecraft?
03:50:53 <elliott> I did my first programming when I was eight. I'm 30 now.]]
03:51:02 <elliott> Fun fact: Notch's programming skills decrease every passing day.
03:51:07 <elliott> [[Any chance of getting a female player model? Also, how about some optional skinnable clothing that can be used with your model?
03:51:07 <elliott> Possibly, yes, but how do I make a cube based female model without being extremely silly and/or slightly objectifying?]]
03:51:16 <elliott> Notch has no idea how to make a female model without giving it gigantic breasts.
04:04:21 -!- elliott has quit (Quit: Leaving).
04:50:56 <pikhq> Hmm. Xiph is working on a new audio codec...
04:51:24 <pikhq> http://people.xiph.org/~xiphmont/demo/celt/download1/celt-0.10.0-32.flac This is what it sounds like at *32 kbps*.
04:54:24 -!- j-invariant has quit (Quit: leaving).
04:54:48 <Quadrescence> unless you have a blog (then there would be no point!!!)
04:56:11 <Quadrescence> pikhq: ok, well you seem like an intelligent, fun-loving guy
05:08:51 * Sgeo once tried to sudo on his school's Linux system
05:09:13 <Sgeo> Mistook that console window for the console window for my system
05:16:40 <Sgeo> Mathnerd314, no idea
05:16:46 <Sgeo> I sent some mail to the sysadmin about it
05:20:03 <Sgeo> xkcd is the reason that I thought of it just now
05:20:56 <Quadrescence> http://25.media.tumblr.com/tumblr_lc1hqgvA8F1qzymhso1_500.gif
05:23:15 * Sgeo pukes on Quadrescence
05:23:52 <Sgeo> Quadrescence, you're the one who posted that disgusting link
05:25:09 <Quadrescence> http://media.damnfunnypictures.com/photos/j0xqdn9-animal-tortoise-turtle-ucumari.jpg
05:26:11 <Sgeo> I prefer that to the comic
05:48:47 -!- pikhq has quit (Ping timeout: 265 seconds).
05:50:32 -!- pikhq has joined.
06:10:20 <pikhq> http://www.zreomusic.com/listen All that is synthed. It sounds *far* to good to be synthed...
06:10:39 -!- oerjan has joined.
06:10:40 <pikhq> Well, aside from being unhumanly accurately played.
06:11:37 <Mathnerd314> hmm, I'm always surprised by what *isn't* synthed
06:14:03 <Mathnerd314> seriously, there ought to be no real barriers to me deciding to make some music *right now*
06:16:21 <Mathnerd314> well, yeah, I'll agree that reading documentation is always a good idea
06:16:48 <pikhq> oerjan: This is why only Gregor makes music here.
06:17:02 <pikhq> He is not a man! He is walking, typing, hat-wearing talent!
06:18:30 <oerjan> even while chewing gum!
06:18:36 <Mathnerd314> there's Isle of Tune, but it's too limited: http://isleoftune.com/
06:19:43 <pikhq> As such is his talent!
06:19:53 <pikhq> He is so talented that he is talent *with talent*!
06:21:01 <Mathnerd314> but AFAICT, there's no single FLOSS "music making" program
06:31:29 <pikhq> Who needs a program?
06:31:35 <pikhq> All you need is talent!
06:31:54 <pikhq> With talent, you can just bit-bang out the FLAC you want!
06:32:12 <pikhq> (note: I in no way advocate actually bit-banging a FLAC to generate music. God no.)
06:32:57 <Sgeo> O... literally writing the bits?
06:33:27 <Sgeo> Actually, what would such a thing sound like?
06:33:55 <Sgeo> Obviously, I should do it
06:35:03 <quintopia> Sgeo: tristan perich writes one-bit music: music played by an arduino without a dac (and therefore using nothing but square waves)
06:38:47 <quintopia> Mathnerd314: this is FLOSS afaict: http://chuck.cs.princeton.edu/release/
06:39:07 <pikhq> Mathnerd314: I don't know, but it should be PAINFUL
06:40:03 <quintopia> i also once composed a piece in audacity
06:41:19 <quintopia> word to the wise: never try to do anything involving more than a handful of tracks in audacity. it will blow up and do really freaky things
06:41:51 <pikhq> quintopia: Doesn't it anyways?
06:42:23 <quintopia> pikhq: it didn't blow up until 20 tracks on my old fast memoriful computer
06:42:34 <quintopia> on this one it can't record a single track for more than five seconds...
06:47:30 -!- zzo38 has joined.
06:53:51 -!- wareya has quit (Read error: Connection reset by peer).
06:54:16 -!- wareya has joined.
06:56:11 <zzo38> Ha ha! Now push the "EXPLODE" button and your television set will explode.
07:01:13 <Sgeo> Hey, I used Audacity to record my karaoke!
07:01:19 * pikhq pushes zzo38's EXPLODE button
07:01:38 <Quadrescence> zzo38: since pikhq is not interested in writing on my blog, do you wanna
07:01:43 <zzo38> Sgeo: Does it work?
07:01:52 -!- Zuu has quit (Read error: Connection reset by peer).
07:01:55 <zzo38> Quadrescence: What do you want written on it? It depends.
07:01:55 <Sgeo> zzo38, I have a scapegoat for my horrible singing!
07:02:34 <Quadrescence> write whatever you want as long as it's expository in nature (and ideally about math or compsci?!?!?!)
07:04:02 <quintopia> i know a blog written entirely in haskell that uses no js
07:04:31 <zzo38> Quadrescence: What do you want me to do, add comments?
07:04:36 * pikhq is now frightened.
07:04:48 <pikhq> FFXII has an optional boss with 50 million HP.
07:04:48 <Quadrescence> zzo38: and you could write a (some) posts about whatever if you wanted
07:04:55 <pikhq> It can apparently take 12 hours.
07:06:12 <zzo38> Quadrescence: No, it is very slow. I prefer PhlogJournal (in which I can just create plain text files with the correct names and everything else goes by itself).
07:06:30 <quintopia> https://faidio.visuallycreated.com:8002/blog/view.cgi?id=5 here's how you make a blog in haskell. i don't know haskell so i don't know how creative this is.
07:07:49 <pikhq> http://static.tvtropes.org/pmwiki/pub/images/yiazmat3.jpg Each one of those dots is a full health bar.
07:08:17 <zzo38> Quadrescence: I mean this gopher://zzo38computer.cjb.net:70/1phlog*a it is much faster and simpler. No account or anything needed, just a directory in your computer.
07:08:43 <quintopia> can you save your progress and come back to it?
07:09:03 <Sgeo> zzo38, did you write PhlogJournal yourself?
07:09:10 <zzo38> Sgeo: Yes, I wrote it myself.
07:09:20 * Sgeo is obviously a future psychic
07:09:22 <Quadrescence> zzo38: the point is that anyone can have an account and anyone can log in and everything is secure
07:09:52 <zzo38> Sgeo: And here is the code for it: gopher://zzo38computer.cjb.net:70/0phlog*f0 (you can use netcat to download it if you want to)
07:10:18 <zzo38> Quadrescence: Then why don't you juse use ssh then?
07:10:26 <Sgeo> Why doesn't Chrome support gopher?
07:10:33 -!- Zuu has joined.
07:10:33 <Sgeo> Does Opera support gopher?
07:10:45 <Quadrescence> zzo38: I want several people to have access, and since I type math, I want javascript to be enabled
07:11:20 <zzo38> Sgeo: Neither Chrome or Opera does. But you can use netcat: echo 'phlog*f0' | nc -q -1 zzo38computer.cjb.net 80 > PhlogJournal.php
07:12:03 <Sgeo> Quadrescence, that's downloading the source for the engine
07:13:38 <zzo38> quintopia: Well, look at the codes if you want to. It is very simple but does calendars, comment system, and more.
07:13:58 <zzo38> Without slowing down your computer with JavaScript and images and stuff like that.
07:14:56 <Quadrescence> zzo38: WHAT ABOUT LATEX RENDERING WITH NATIVE FONTS
07:15:29 <quintopia> i'm getting a 501 on your nc command up thhere? :/
07:15:46 <zzo38> Quadrescence: Then just use LaTeX to make a printout.
07:15:56 <zzo38> quintopia: Sorry, that is because I accidentally typed 8 instead of 7.
07:15:57 <quintopia> Quadrescence: that's lame. images are okay.
07:16:06 <zzo38> Change the 8 to 7 (they are close to each other on the keyboard)
07:16:09 <zzo38> And then it will work.
07:16:31 <Quadrescence> quintopia: images assume the user has some sized screen at some resolution
07:17:01 <zzo38> I prefer Plain TeX to typeset the mathematics and then can publish the DVI file if we need to make a report about mathematical things.
07:17:07 <Ilari> Port 70/TCP? Gopher?
07:17:30 <Quadrescence> zzo38: the point of a blog is to blog, and one can use TeX to do stuff on it
07:18:13 <zzo38> Quadrescence: Could you write a blog program in TeX?
07:18:48 <quintopia> Quadrescence: i think it's fair to use JS to detect screen size. it's less lame than printing text in all kinds of crazy positions to simulate tex, imo.
07:19:36 <quintopia> there really should be a css way to do that though :/
07:19:50 <Quadrescence> images are just a poor option when you can do native TeX typesetting and use Real Fonts
07:20:06 <zzo38> Quadrescence: No, I mean a blog program in TeX. Like, you might use ssh to send files and stuff, perhaps message send protocol or something for comments, and then HTTP/FTP/Gopher to download the DVI file.
07:20:17 <quintopia> jsmath is slow and hangs a lot. it annoys me.
07:20:33 <Ilari> Ah, lynx supports gopher...
07:20:35 <zzo38> quintopia: Yes it is slow on my computer too.
07:21:04 <zzo38> Quadrescence: I think it is too slow.
07:21:36 <quintopia> how about we just not render it in real time, eh?
07:21:44 <Ilari> zzo38: AFAIK, no need to point MX record to host itself, A/AAAA records are enough for mail delivery...
07:21:58 <Quadrescence> quintopia: because that defeats the whole purpose of it
07:22:24 <Quadrescence> that's why browsers are getting better and better JS engines
07:22:47 <quintopia> we just need to petition the w3c to add tex rendering stuff to the html standards.
07:22:48 <zzo38> Ilari: Are you refering to my domain name? If I don't enter the MX record, I think cjb.net services will handle it.
07:22:59 <quintopia> let the browser do it fast instead of in js slowly
07:23:10 <Ilari> "zzo38computer.cjb.net. 300 IN MX 0 zzo38computer.cjb.net.".
07:23:23 <Quadrescence> quintopia: but right now it's the best we have. and mathml blows
07:23:52 <quintopia> Quadrescence: i didn't know. i'll test it real quick to see what you mean
07:24:01 <zzo38> Ilari: Yes, I did that so that CJB service will not process the mail.
07:24:25 <Mathnerd314> Quadrescence: mathml doesn't blow that bad
07:25:37 <Quadrescence> it is a piece of shit, designed by a web committee, not mathematicians or typographers
07:29:06 <Ilari> zzo38: CJB inserts their own MX record if you don't put one?
07:29:11 <Quadrescence> Well if you've ever examined either the output or the markup, you'd understand Mathnerd314
07:30:12 <quintopia> so tex4ht renders the math stuff as a png apparently. add to that a script to switch out which image to use depending on resolution i think you'd have something looking reasonable and running fast until we get a proper standard
07:31:00 <Quadrescence> I highly favor native fonts, because they scale with the text around it, have the correct baseline, and don't look like shit when printed
07:31:31 <zzo38> Ilari: Yes I think they do.
07:31:58 <Quadrescence> here's my current To Read stack http://i.imgur.com/U2uzT.jpg
07:33:29 <quintopia> googling your nick i find that you do a lot of math reading and tex stuff
07:33:38 <quintopia> i can see where that might be an issue for you
07:34:02 <Ilari> zzo38: Ah, that explains it. If querying MX records for foo. doesn't produce any results, MTAs assume implicit 'foo. 0 IN MX 0 foo.'.
07:34:19 <Quadrescence> quintopia: tex4ht is a great application, I don't deny that
07:34:30 <Quadrescence> i just like the output I have I guess :S:S:S:S
07:34:31 <quintopia> i also didn't realize quadrescence was a made up word...what is it supposed to mean?
07:34:55 <quintopia> yes but you get to make up a def too :P
07:35:47 <quintopia> i have one more facet than you. i win.
07:36:13 <Quadrescence> 4 CORNER DAYS, CUBES 4 QUAD EARTH- No 1 Day God.
07:36:15 <zzo38> jsMath doesn't even support a lot of commands of TeX. And the ones it does support, is all incomplete.
07:36:38 <Quadrescence> zzo38: It supports the math typesetting, and that's rather complete
07:37:56 <Quadrescence> and looks exquisite if you have STIX fonts installed (free)
07:37:56 <zzo38> I typed \^^47amma and it says "Unknown control sequence '\^'"
07:38:09 <zzo38> And it can't make \def or \the\count255 or anything like that either
07:38:54 <zzo38> But \the is broken.
07:39:39 <Quadrescence> if you want to typeset math using TeX on webpages, use jsmath
07:39:51 -!- Mathnerd314 has quit (Quit: ChatZilla 0.9.86-rdmsoft [XULRunner 1.9.2.12/20101026210630]).
07:45:21 -!- Sgeo has quit (Read error: Connection reset by peer).
07:48:57 <zzo38> \mathchar doesn't work.
07:51:05 <Quadrescence> zzo38: what is a practical use case of \mathchar
07:51:58 <zzo38> \kern only partially works.
07:52:36 <zzo38> Quadrescence: You can look at the TeXbook for some examples.
07:52:48 <Quadrescence> I know what it is. I am asking for a practical use case for a website.
07:54:37 <Quadrescence> zzo38: SORRY, I AM TAKING OFFENSE TO YOUR INANE PROBLEMS WITH JSMATH!!!
07:56:22 <zzo38> I think TeX works better. If you want to make a math report, you can use TeX.
07:56:59 <zzo38> Also, the \hbox command in jsMath is completely broken.
07:57:01 <Quadrescence> Yes, if you want to make a math report for publication, yes
07:58:19 <zzo38> Actually I think TeX can be good for math blog. You should just need ssh.
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:03:39 <zzo38> The broken \hbox is probably the most serious mistake in jsMath, I think.
08:22:43 <zzo38> But regardless of how well jsMath works or doesn't work, it is still slow!!
08:28:58 <zzo38> 250 Your request for doing nothing has been completed successfully.
08:37:25 -!- zzo38 has quit (Quit: Leg before wicket.).
09:13:25 -!- MigoMipo has joined.
10:09:54 -!- asiekierka has joined.
10:10:06 <asiekierka> me and my friend made this in my own game -> http://64pixels.org/christmas.png
10:14:07 -!- cheater99 has joined.
10:19:50 -!- hagb4rd has quit (Ping timeout: 240 seconds).
10:20:16 -!- cheater99 has quit (Read error: Connection reset by peer).
10:37:03 -!- cheater99 has joined.
10:43:21 -!- cheater99 has quit (Read error: Connection reset by peer).
10:55:19 -!- Anon899 has joined.
10:55:55 -!- Anon899 has left (?).
11:00:03 -!- cheater99 has joined.
11:06:11 -!- cheater99 has quit (Read error: Connection reset by peer).
11:23:03 -!- cheater99 has joined.
11:31:45 -!- cheater99 has quit (Read error: Connection reset by peer).
11:40:13 -!- asiek2erka has joined.
11:42:48 -!- asiekierka has quit (Ping timeout: 240 seconds).
11:46:33 -!- cheater99 has joined.
11:52:33 -!- cheater99 has quit (Read error: Connection reset by peer).
12:09:05 -!- cheater99 has joined.
12:14:41 -!- cheater99 has quit (Read error: Connection reset by peer).
12:17:04 -!- FireFly has joined.
12:19:48 -!- Wamanuz2 has quit (Remote host closed the connection).
12:21:17 -!- Wamanuz2 has joined.
12:27:19 -!- impomatic has joined.
12:30:24 -!- cheater99 has joined.
12:35:36 -!- cheater99 has quit (Read error: Connection reset by peer).
12:52:08 -!- BlSlereah has changed nick to Slereah.
12:52:15 -!- cheater99 has joined.
13:22:57 -!- Wamanuz2 has quit (Remote host closed the connection).
13:23:23 -!- Wamanuz2 has joined.
13:40:51 -!- yiyus_ has quit (Ping timeout: 260 seconds).
13:45:01 -!- Wamanuz3 has joined.
13:45:01 -!- Wamanuz2 has quit (Read error: Connection reset by peer).
13:52:17 -!- yiyus has joined.
14:23:22 -!- cheater99 has quit (Read error: Connection reset by peer).
14:40:50 -!- cheater99 has joined.
15:12:44 -!- poiuy_qwert has joined.
15:16:00 -!- cheater99 has quit (Read error: Connection reset by peer).
15:27:37 -!- elliott has joined.
15:30:12 <elliott> http://xkcd.com/838/ This... is actually close to having potential.
15:30:33 <elliott> Get rid of the girl in the middle panel and just make it him wondering and it would be decent.
15:32:18 <elliott> 20:51:24 <pikhq> http://people.xiph.org/~xiphmont/demo/celt/download1/celt-0.10.0-32.flac This is what it sounds like at *32 kbps*.
15:32:55 <elliott> pikhq: heh Tom's Diner cameo at the end
15:33:24 <elliott> 21:10:37 <Quadrescence> pikhq: u should www.symbo1ics.com/blog
15:33:28 <elliott> oh jesus christ that is the worst blog ever
15:33:39 <elliott> wasn't it on reddit recently
15:33:50 -!- cheater99 has joined.
15:34:30 <elliott> 22:14:03 <Mathnerd314> seriously, there ought to be no real barriers to me deciding to make some music *right now*
15:34:30 <elliott> 22:15:44 <oerjan> except talent.
15:34:30 <elliott> 22:16:21 <Mathnerd314> well, yeah, I'll agree that reading documentation is always a good idea
15:35:58 <elliott> 22:41:19 <quintopia> word to the wise: never try to do anything involving more than a handful of tracks in audacity. it will blow up and do really freaky things
15:35:58 <elliott> 22:41:51 <pikhq> quintopia: Doesn't it anyways?
15:36:04 <elliott> audacity is possibly the worst software ... ever
15:36:50 <elliott> 23:03:41 <Quadrescence> (enable js)
15:36:57 <elliott> desperately trying to figure out a justification for having a blog depend on js now.
15:42:37 -!- j-invariant has joined.
15:44:34 <j-invariant> look at the proof on line 746 http://coq.pastebin.com/rkDjqYFH
15:44:50 <j-invariant> then see 877 where it gets mapped to a different category
15:47:08 -!- cheater99 has quit (Read error: Connection reset by peer).
15:47:20 <elliott> j-invariant: this is getting close to the point where i understand nothing though :)
15:47:25 <j-invariant> this gives a general way to prove things automatically
15:47:41 -!- Mathnerd314 has joined.
15:48:16 <elliott> 02:10:06 <asiekierka> me and my friend made this in my own game -> http://64pixels.org/christmas.png
15:50:53 <j-invariant> I'm not sure if I should start keep developing this or try and simplify it and clean it up
15:51:17 <j-invariant> it's too bad I can't bootstrap it.. because it would be a lot easier to define category theory if i already had it
15:52:27 <elliott> j-invariant: not if you did everything coinductively! maybe :P
15:52:43 <elliott> j-invariant: I'd keep going, it's "clean enough"
16:03:45 <elliott> j-invariant: I am not sure how to prove that 0+x = x in a ring at all, with my model
16:04:36 <elliott> [[Error: Impossible to unify "mg_op b" with "mg_op b".]] wat
16:04:44 <elliott> j-invariant: not that i can tell
16:04:53 -!- cheater99 has joined.
16:05:00 <elliott> j-invariant: I mean 0*x = 0
16:05:02 <j-invariant> yeah that is so stupid, Coq should check if the string representations are the same - and show implicit parameters if they are
16:05:10 <elliott> "Error: Impossible to unify "mg_op b" with "mg_op b"." ;; lol ok so my system does work
16:05:13 <elliott> coq just prints it confusingly
16:05:25 <oerjan> elliott: i think i wrote a proof of 0*x = 0 on this channel once
16:07:34 <Mathnerd314> 0*x = (0+0)*x = 0*x+0*x --> cancel --> 0*x = 0
16:07:55 <elliott> `addquote <oerjan> elliott: i think i wrote a proof of 0*x = 0 on this channel once
16:08:00 <elliott> your crowning achievement as a mathematician
16:08:07 <HackEgo> 254) <oerjan> elliott: i think i wrote a proof of 0*x = 0 on this channel once
16:08:10 <elliott> Mathnerd314: that needs you to prove that a = a+a means a =0
16:09:05 <elliott> Theorem foo S (R : ring S) :
16:09:05 <elliott> forall a, (pr_mul (p:=R) a (mn_1 (m:=pr_ag R))) = (mn_1 (m:=pr_ag R)).
16:09:08 <elliott> hard enough just to formulate it!
16:09:52 <Mathnerd314> thus... why Coq / etc. are not good for proving theorems
16:12:51 <elliott> Mathnerd314: thus why unjustified generalisation
16:13:02 <elliott> lol i just realised i structured this in a way that I can't prove a:S
16:13:10 <elliott> OH WELL time to soldier on
16:14:30 <elliott> is 0+a = a left identity or right?
16:15:18 <elliott> Theorem bar S (R : ring S) :
16:15:19 <elliott> forall a, (pr_add (p:=R) a mn_1) = a.
16:17:01 -!- cheater99 has quit (Read error: Connection reset by peer).
16:31:49 -!- oerjan has quit (Quit: Later).
16:32:18 -!- cheater99 has joined.
16:34:37 -!- cheater99 has quit (Remote host closed the connection).
16:40:15 -!- poiuy_qwert has quit (Read error: Connection reset by peer).
16:41:53 -!- poiuy_qwert has joined.
16:58:03 -!- poiuy_qwert has quit (Read error: Operation timed out).
17:00:07 <elliott> Mathnerd314: for... theorem proving?
17:00:12 <elliott> Mathnerd314: you have no fucking clue what you're talking about
17:00:42 <elliott> Mathnerd314: I am eagerly awaiting your proof of the four-colour theorem in a term rewriting language
17:01:51 -!- poiuy_qwert has joined.
17:17:20 <Mathnerd314> elliott: does writing Coq in a term rewriting language count?
17:17:47 <elliott> Mathnerd314: Anyone can Greenspun. The answer is no.
17:18:10 <elliott> Good luck: (1) Finding out how on earth you use term rewriting evaluation to "prove" something, especially without a powerful type system; (2) Formulating the proof.
17:18:27 <elliott> (3) Formulating the proof _without Coq's large array of tactics_, no less.
17:20:15 -!- poiuy_qwert has quit (Read error: Connection reset by peer).
17:21:52 -!- poiuy_qwert has joined.
17:22:19 <Mathnerd314> actually, it's pretty simple. I define equality to be two constructs, "rewrite to" and "rewrite from", and then Coq proofs are term-rewriting proofs, and Coq's tactics are then term rewriting strategies
17:26:11 <elliott> Mathnerd314: i take it you have no idea how coq actually works
17:27:00 <Mathnerd314> maybe; my conception is probably inaccurate in the details
17:27:09 <elliott> j-invariant: any progress btw?
17:27:16 <elliott> Mathnerd314: more than the details, I'd say ...
17:28:13 <elliott> j-invariant: category theory solves all problems! including tiredness!
17:31:38 <j-invariant> elliott: the big picture is that category theory just organises things and seperates concerns, you still need to construct things by hand (e.g. using inductive definitions, recursive functions, composites) - so I might try and rewrite the equation prover thing without the categorical frame so I can use it to prove the early lemmas
17:32:52 <j-invariant> right now it just interprets everything as (typed) lists, with composition as append -- I think I could also add in things like fg = id
17:33:50 <j-invariant> on the other hand its a lot of work and I don't know if it will survive being turned upside down like that
17:35:26 -!- Zuu has quit (Ping timeout: 260 seconds).
17:35:54 <j-invariant> maybe I should just press on and define limits
17:40:15 -!- poiuy_qwert has quit (Read error: Connection reset by peer).
17:41:34 -!- cheater99 has joined.
17:41:53 -!- poiuy_qwert has joined.
17:42:16 <Mathnerd314> elliott: here we are... Coq tactics *are* rewrite rules
17:42:24 <elliott> Mathnerd314: wrong, they're programs
17:42:35 <elliott> in fact IIRC they can even not halt (j-invariant?)
17:42:57 <Mathnerd314> rewrite rules are programs, and can be non-terminating
17:43:42 <elliott> Mathnerd314: Coq tactics *are* brainfuck programs
17:43:49 <elliott> brainfuck programs are programs, and can be non-terminating
17:44:00 <elliott> Mathnerd314: Coq tactics *are* rule 110 initial states
17:44:33 <Mathnerd314> elliott: no, they're rewrite rules. they take propositions and turn them into other propositions.
17:45:10 <elliott> send proposition on stdin, get new proposition on stdout.
17:45:56 -!- poiuy_qwert has quit (Client Quit).
17:47:40 <Mathnerd314> hmm, we seem to different definitions. I interpret rewrite rules as "most general thing ever invented". you seem to interpret them as "esoteric thing nobody uses"
17:48:56 <elliott> firstly, those two aren't definitions.
17:48:59 <elliott> secondly, I like rewrite rules perfectly well.
17:49:06 <elliott> thirdly, as they aren't definitions, they prove nothing.
17:49:58 <elliott> well, they also aren't interpretations.
17:50:03 <elliott> so i have no idea whatsoever what you are trying to convey
17:50:54 <j-invariant> in Coq you have a situation like x:T, y:B, z:B->T->W |- _ : W
17:51:42 <j-invariant> tactics fill in the gap. e.g. you might do apply z. then you get x:T, y:B, z:B->T->W |- z _ _ : W
17:52:12 <Mathnerd314> elliott: we have different assumptions, leading to differing opinions/interpretations. so I am wondering where we start to disagree.
17:52:41 <j-invariant> if you take contexts and programming problems you can view tactics as rewrite rules
17:52:45 <elliott> Mathnerd314: what are our differing assumptions? how are they at all relevant to the situation at hand? what do you think the situation at hand is?
17:53:25 <j-invariant> it's useless to do so because we're not interested in the tactic language
17:54:00 <j-invariant> it's just some tacky script language that helps you program faster, like typeclasses in haskell or macros in lisp
17:55:47 -!- elliott_ has joined.
17:55:48 <j-invariant> the way you use it is more like (an advanced version of) prolog
17:56:01 <j-invariant> because it has pproof search and unification and such
17:56:10 <elliott_> a _very_ advanced version of prolog :P
17:57:39 <Mathnerd314> I guess I was too busy living in meta-meta-land to notice ;-)
17:59:21 -!- elliott has quit (Ping timeout: 260 seconds).
18:02:11 <j-invariant> what's the scoop with rewrite systems anyway
18:02:43 <j-invariant> aren't they just another universal computer?
18:03:26 <Mathnerd314> yeah, but they're a "nice" universal computer, nicer IMO than lambdas
18:05:06 <elliott_> fizzie: Deewiant: The server is back up, BTW. Don't think ineiros pinged you two yesterday.
18:05:34 <elliott_> j-invariant: they are pretty nice because you can implement most other things in terms of them ... and also pattern matching on constructors comes "built in", there's no special notion of a constructor
18:05:55 <j-invariant> when you write down a rewrite system: You don't know if it's confluent or not do you?
18:06:00 <elliott_> j-invariant: as in, implement other things /nicely/ in terms of them
18:06:17 <elliott_> I think confluence is overrated
18:06:20 <j-invariant> is there any use of a non-confluent rewrite system?
18:07:29 <elliott_> j-invariant: do you mean like, given "foo x = x; foo (bar x y) = quux x y", you don't know which rule to apply for "foo (bar a b)"?
18:07:43 <elliott_> j-invariant: because, generally you have a rule for this -- e.g. "most specific match", so it'd be the second
18:09:06 <j-invariant> but imposing that restriction makes the system confluent
18:09:56 <elliott_> j-invariant: then yes, you do know whether it's confluent or not: it is!
18:12:11 <elliott_> j-invariant: you may be interested in the Q language http://q-lang.sourceforge.net/ and its successor http://code.google.com/p/pure-lang/ (which, inexplicably, is very fast; faster than Python etc.)
18:14:34 <elliott_> well, fast; i should say efficient
18:15:13 <elliott_> j-invariant: also rewriting languages are pretty "extensible"
18:15:23 <elliott_> i.e., you can easily add new cases to a function from "anywhere", codewis
18:15:34 <elliott_> j-invariant: which means you don't need typeclasses
18:15:42 <elliott_> say you have a few constructors for your new numeric type
18:16:04 <elliott_> and if infix + is bound to add, then it all magically works
18:20:03 <elliott_> j-invariant: but when doing term rewriting stuff i *do* miss lambdas a bit ... I think there could be a term rewriting language that somehow makes rules themselves first class, so you could pass around anonymous rules
18:20:06 <elliott_> but i haven't seen that done yet
18:20:42 <Mathnerd314> j-invariant: I don't think people use non-confluent systems by choice; it's just that they don't bother adding in the rules to make it confluent
18:21:14 <j-invariant> there's some new(ish) pattern languages but I haven't been able to find the books on them yet so dunno
18:22:22 <j-invariant> Mathnerd314: I just mean, you are able to write down non-confluent systems -- so how do we make use of that?
18:22:25 <Mathnerd314> elliott_: that's the programming language I'm trying to write
18:22:42 <elliott_> Mathnerd314: message passing and multiple dispatch are not pattern matching. sorry.
18:23:14 <Mathnerd314> elliott_: the messages passed are rewrite rules
18:23:40 <elliott_> j-invariant: also term rewriting lets you do fun things like this
18:23:42 <elliott_> > foldl (+) 0 [a,b,c,d,e,f,g];
18:25:43 <elliott_> j-invariant: well, it's just a silly example.
18:25:54 <elliott_> (foldl is defined the normal way)
18:26:51 <elliott_> warning: rule never reduced: random = 2;
18:26:51 <elliott_> warning: rule never reduced: random = 3;
18:27:02 <elliott_> j-invariant: basically I'd say "random = 1; random = 2; random = 3" is an invalid program
18:27:08 <elliott_> since you have ambiguous rules
18:27:21 <j-invariant> it must be very hard to recognize valid/invalid programs
18:27:56 <elliott_> i mean it depends on your rule for specificity
18:28:00 <elliott_> j-invariant: it's easy not to write invalid programs though IME
18:28:04 <elliott_> I would never write anything like that random thing
18:28:08 <elliott_> j-invariant: i mean, you know in haskell
18:28:21 <elliott_> how many times do you write a haskell program with two "f (X ...) ... = ..." that are ambiguous?
18:30:14 -!- impomatic has left (?).
18:38:22 <Mathnerd314> j-invariant: in my language, that would make random a type. (particularly, the type containing only 1, 2, and 3)
18:40:31 <elliott_> err, does that make any sense? types are more like predicates
18:41:33 <Mathnerd314> my type predicates are all "reachable by running rewrite rules"
18:42:25 <Mathnerd314> so "nat = 0; nat = S n" would specify the type nat
18:42:37 <elliott_> :: if nat n then nat (fact n) else true
18:42:47 <elliott_> Mathnerd314: so "S S" is a nat?
18:43:37 <elliott_> hmm, if we say that "x:f" = "f x" and also have -> for boolean implication (i.e. true->Q = Q, false->Q = true), then
18:46:03 <elliott_> j-invariant: that i could understand.
18:46:35 <elliott_> 1 2 6 24 120 720 5040 40320 362880 3.6288e6 3.99168e7
18:47:25 <Mathnerd314> elliott_: curses, you're right. fact nat : nat
18:47:37 <elliott_> i see. what does "a : b" mean?
18:47:44 <elliott_> presumably it reduces down to a rewrite rule of some kind.
18:49:48 <Mathnerd314> it's an upper bound; it says "the set of results of rewriting 'fact nat' will produce a subset of the natural numbers"
18:52:29 <elliott_> Mathnerd314: i don't suppose you have an algorithm for typechecking this
18:53:09 <Mathnerd314> not a general algorithm; with that I could solve everything. but for specific cases I do
18:54:41 <elliott_> j-invariant: can you explain to Mathnerd314 why a type system without a type checker is useless, I'm too lazy to
18:54:56 <elliott_> now I'm imagining Coq going "You might have proved this! I can't tell!"
18:56:41 <Mathnerd314> elliott_: you can check bounds on types easily
18:57:07 <elliott_> Mathnerd314: if you can't check types in general, it's not a type system
18:57:26 -!- oerjan has joined.
18:57:42 <Mathnerd314> ok, it's not a type system. it's a proof system.
18:57:50 -!- Gracenotes has quit (Quit: ...).
18:58:03 <elliott_> Mathnerd314: a proof system that can't tell you whether your proof is valid or not?
18:58:36 <Mathnerd314> sorry, it's the thing you prove proofs about. I don't know what you call that.
19:00:04 <j-invariant> a turing machine computes and defines recursive sets. ZFC computes nothing but defines a huge chunk of mathematics
19:01:45 <elliott_> <Mathnerd314> sorry, it's the thing you prove proofs about. I don't know what you call that.
19:03:36 <elliott_> I think I am going to write a parser generator
19:03:53 <oerjan> write a generator parser instead
19:04:51 <Mathnerd314> elliott_: it's a system, with semantics. you can "run" the statements with =, producing results, and you can "infer" the statements with :, producing bounds
19:07:24 <oerjan> elliott_: christmas starts officially 17:00 today in norway
19:07:34 <elliott_> oerjan: really? that's just weird.
19:07:37 <elliott_> you guys are stupid and smelly.
19:07:39 -!- elliott_ has changed nick to elliott.
19:07:43 <Mathnerd314> elliott_: and you can prove things about running and inference.
19:07:44 -!- elliott has quit (Changing host).
19:07:44 -!- elliott has joined.
19:07:51 <oerjan> that's when they ring all the church bells
19:07:52 <elliott> Mathnerd314: you can't prove anything if you don't have a type checker
19:08:28 <Mathnerd314> wtf? 2+2=4; there's no stinking type checker
19:09:11 <elliott> it's a proof system, yes? presumably one based on some kind of type theory.
19:09:15 <oerjan> elliott: i have this theory it may be a holdover from when days were considered to start at sunset (as the jews still do for sabbath etc.)
19:09:15 <elliott> therefore you need a type checker to check your proofs.
19:09:22 <elliott> by your own admission you don't have a general typechecker
19:09:27 <elliott> oerjan: yeah yeah, silly nord
19:11:02 <elliott> are you just reading wikipedia, picking random vaguely-related words from there, and applying them?
19:11:12 <elliott> so far I have not a single idea how your system works, what it's intended to do, or what components it has at all
19:11:21 <elliott> I have no idea how you expect to be able to write and verify proofs.
19:12:12 <elliott> Mathnerd314: then why are you wasting my time?
19:12:29 <j-invariant> elliott: he imght just be too tired at this point
19:12:41 <elliott> j-invariant: are you sure you're not generalising from a sample of 1? :D
19:15:23 <elliott> Mathnerd314: on why you're wasting my time?
19:17:58 -!- j-invariant has quit (Quit: leaving).
19:28:37 <elliott> "10. He has an inflated ego (from being good at math)" <-- I wonder what to call this, it's not a self-fulfilling prophecy ... hmm ...
19:41:28 <fizzie> elliott: <ineiros> Vorpal, fizzie, elliott and others who might care: [...]
19:42:00 <fizzie> But right, Deewiant was left out.
19:47:50 <elliott> 'Tis rather lonely on there right now.
19:49:48 <elliott> fizzie: Incidentally, I found your secret chest. It's empty.
19:51:24 <fizzie> Or do you mean the thing under my floorboards in the house?
19:51:39 <elliott> fizzie: I mean the thing with the secret entrance to the left of your fire.
19:51:54 <fizzie> That's not very secret.
19:52:01 <elliott> fizzie: To be fair, I am very dense.
19:52:10 <oerjan> elliott the black hole
19:52:19 <elliott> I don't think I'll bother taking out all your floorboards, though. :p
19:52:25 <fizzie> There's also another chest under the floor in front of that chest, but that's currently empty also.
19:52:35 <fizzie> I moved stuff elsewhere.
19:52:55 <fizzie> Okay, back to socializing. -¥
19:59:54 <elliott> HOW COME DESTROYING MY CART WHILE I'M IN IT
20:00:01 <elliott> I WANT MY POSSESSIONS BACK NOTCH
20:13:31 -!- cheater99 has quit (Read error: Connection reset by peer).
20:15:19 -!- SimonRC has quit (Ping timeout: 265 seconds).
20:19:18 <elliott> I don't run Java programs that aren't Minecraft.
20:22:02 -!- SimonRC has joined.
20:22:31 <asiek2erka> elliott i have not obfuscated the code
20:23:46 <elliott> i haven't found a decent open-source java compiler
20:25:39 <asiek2erka> elliott - http://64pixels.org/christmas.png
20:25:54 <elliott> asiek2erka: i saw in the looks. i also said "what.".
20:26:47 <elliott> maybe if you explain wtf http://64pixels.org/christmas.png is
20:28:08 <elliott> i don't get the relevance of the bible quote ... well, except that christmas used to be vaguely related to christianity after they took it from the pagans, but that seems to be a rather tenuous link
20:28:54 <elliott> Christmas = the joys of rampant consumerism; your point?
20:29:49 <elliott> asiek2erka: is it "supposed" to be anything? there's no evidence at all that jesus was born on the 25th, and in fact the historical record very clearly shows that it was picked to coincide with a pagan day
20:30:01 <elliott> i don't remember the last time i saw christmas associated with christianity in... any way at all really
20:30:02 <oerjan> asiek2erka: um, you do realize elliott is this channel's resident semi-militant atheist?
20:30:12 <elliott> oerjan: i'm not a semi-militant atheist, and it's not about that
20:30:21 <elliott> I just don't see how modern christmas is related to christianity in any way
20:30:25 -!- cheater99 has joined.
20:31:01 <oerjan> elliott: hey i added the semi- just to avoid your protests :D
20:31:14 <elliott> I wouldn't have been confused if the bible quote even /mentioned/ jesus at all :p
20:31:46 <asiek2erka> elliott: it's what the angels said when Christ was born AFAIK
20:31:57 <elliott> asiek2erka: I don't think that actually happened :-P
20:32:03 <elliott> oerjan: well, /r/atheism irritates me as much as anyone :P ... so at least I'm not a typical reddit atheist!
20:32:06 <asiek2erka> elliott: well christians believe it did
20:32:18 <elliott> asiek2erka: I'm nitpicking at this point :P
20:32:36 <oerjan> s/at this point/always/
20:33:00 <elliott> asiek2erka: Indeed -- that's why I worship the tiny china teapot orbiting around the sun in an elliptical orbit between the Earth and Mars.
20:33:02 -!- cheater99 has quit (Client Quit).
20:33:06 <elliott> I trust it will bring me salvation.
20:33:17 <elliott> (side note: that would be a way better fake religion than FSM)
20:33:17 -!- cheater99 has joined.
20:33:37 -!- wareya has quit (Read error: Connection reset by peer).
20:33:54 <elliott> Tomorrow I will celebrate The Day of the Revelation of the Teapot.
20:34:09 <asiek2erka> how much believers does your religion have
20:34:21 -!- wareya has joined.
20:34:25 <elliott> You measure the accuracy of beliefs by how many people believe them?
20:34:32 -!- cheater99 has quit (Read error: Connection reset by peer).
20:34:39 <asiek2erka> just that so many people believe us. why
20:34:42 <elliott> But, uh, me and Bertrand Russell, which is pretty damn good company if you ask me.
20:34:59 <elliott> asiek2erka: Um, because Christians went crusading to convert all the evil nonbelievers quite a while back and it worked surprisingly well ...?
20:35:12 <asiek2erka> elliott: Well, I can't disagree with this argument
20:35:13 <elliott> As opposed to all the Buddhist missionaries going around.
20:35:30 <elliott> (Solipsist missionaries are the best though.)
20:35:42 <elliott> ("I'm just saying ... I don't really exist. Only you do. Think about it.")
20:36:22 <asiek2erka> Christians took Pagan holidays for their own use to stop paganism
20:36:55 <elliott> Do you consider that a good thing?
20:37:08 <asiek2erka> i do not accept the fact we christians used force
20:37:31 <asiek2erka> we don't do spanish inquisitions anymore, do we
20:37:49 <elliott> asiek2erka: Do you really think all of Christianity is united with a single opinion?
20:38:10 <elliott> You're saying "we" like you're a group of 10 likeminded people, not a group of N billion people believing the same basic vague thing but with millions of differences beyond that.
20:38:53 <asiek2erka> also why are you arguing with a 13-year-old
20:38:58 <asiek2erka> that's the most nonsensical thing ever
20:39:37 <oerjan> indeed. asiek2erka, go to your room!
20:39:48 <elliott> Is asiek2erka /asking/ me to discount his opinions based on his age?
20:40:09 <elliott> wait, isn't asiek2erka polish?
20:40:09 <oerjan> elliott: a sure sign of immaturity if i ever saw one!
20:40:26 <elliott> i seem to recall christianity having a very strong grip on poland ... going by my source for all information about poland ... that's right ... nooga!
20:40:50 <elliott> very reliable if you ask me
20:40:59 <oerjan> i recall recently seeing some headline about polish church attendance taking a nosedive
20:41:33 <asiek2erka> i am telling you why the hell are you arguing with someone that should be less intelligent than you
20:41:46 <asiek2erka> then beat you with their stupid argumentatino
20:42:10 <elliott> so if you're older than someone you're smarter than them?
20:42:31 <oerjan> asiek2erka: um this is #esoteric. here age is not the strongest indicator of intelligence by far.
20:42:35 <elliott> oerjan: sure, but it's more the early years that matter I would expect fwiw
20:43:12 <elliott> it's been minutes since i questioned anything you said.
20:43:18 <elliott> well apart from the age-intelligence correlation. which is just stupid.
20:44:41 <asiek2erka> "The word Christmas originated as a compound meaning "Christ's Mass"."
20:45:35 <elliott> http://retire-well-life.com/wp-content/uploads/2009/12/santa-claus.jpg Pictured: Jesus.
20:45:54 <asiek2erka> However, in Chronographai, a reference work published in 221, Sextus Julius Africanus suggested that Jesus was conceived on the spring equinox, popularizing the idea that Christ was born on December 25.
20:46:07 <asiek2erka> We do not know when Jesus was really born
20:46:12 <asiek2erka> it was only a suggestion and everyone said "ok"
20:46:39 <elliott> there are better estimates
20:46:44 <elliott> IIRC it's something like July
20:46:58 <elliott> well, if the historical jesus actually exists, which is arguable, but anyway
20:46:58 <asiek2erka> he New Testament does not give a date for the birth of Jesus. <- that means any guesses cannot be 100% sure even for christians
20:47:09 <elliott> right ... because everything not in the new testament is false?
20:47:25 <asiek2erka> for christians the new testament is 100% true
20:47:33 <elliott> <asiek2erka> for christians the new testament is 100% true
20:47:37 <elliott> yes, er, hate to break it to you, but that's not even remotely so.
20:47:58 <elliott> I don't know of a single person who follows even the new testament 100% to the letter.
20:48:19 <asiek2erka> it is true but nobody reads it because nobody cares!
20:48:23 <Vorpal> <fizzie> elliott: <ineiros> Vorpal, fizzie, elliott and others who might care: [...] <-- he is included in others
20:48:32 <asiek2erka> most Christians, at least in Poland, declare they are christians
20:48:33 <elliott> Yes, but it didn't ping him, so. :p
20:48:39 <Vorpal> also, happy xmas everyone
20:48:41 <asiek2erka> they just declare and... maybe pray every evening
20:48:47 <asiek2erka> and do not give a **** about anything else
20:48:54 <elliott> I'm a Muslim! I demonstrate my Musliminity by doing nothing.
20:48:59 <Vorpal> (In Sweden we celebrate the 24th.)
20:49:12 <elliott> Vorpal: Yes, yet more evidence that you're uncivilised backwater vikings.
20:49:35 <Vorpal> elliott, rather, the reverse
20:50:30 <Vorpal> elliott, the other reverse
20:50:34 <Vorpal> (everyone else is backwards)
20:50:46 <Vorpal> elliott, but yes you probably are a viking as well
20:51:09 <elliott> Someone get on Minecraft, it is terribly quiet today.
20:51:12 <asiek2erka> Vorpal: you mean he's a gnikiv!? [/lamejoke]
20:51:25 -!- cheater99 has joined.
20:51:28 <Vorpal> elliott, nah, I'm going to dig into this ioctl
20:52:08 <Vorpal> elliott, been porting the pc-speaker tune playing code from freebsd to linux. As an user space app in this case.
20:52:19 <asiek2erka> are you going to craft a pc speaker from an ioctl and the user space
20:52:32 <Vorpal> elliott, I have a problem however. beep(1) is GPL. Not GPL2. GPL.
20:52:49 <Vorpal> elliott, and there are some magic constants I need from there
20:53:00 <elliott> Vorpal: Those aren't copyrightable.
20:53:02 <Vorpal> elliott, because I haven't been able to find docs on the IOCTL
20:53:21 <elliott> Small magic numbers aren't copyrightable; even if they are, another program's copy of them isn't.
20:53:28 <Vorpal> elliott, it is rather large. Over 9000
20:53:50 <elliott> Vorpal: Srsly -- not copyrightable. If the author of beep didn't invent those constants, there is no justification for saying its license applies.
20:54:06 <Vorpal> elliott, it is something like jiffies per timer interrupt of original IBM XT timer
20:54:15 <Vorpal> don't have the computer with the code on turned on atm
20:54:17 -!- cheater99 has quit (Read error: Connection reset by peer).
20:54:46 <elliott> What Painterly glass texture do you use? :p
20:54:58 <Vorpal> elliott, the same as I told you about before
20:55:43 <Vorpal> (don't you hate it when someone says "same place as usual" when you ask where something is? I certainly do)
20:56:24 <Vorpal> elliott, it has a thin white border, it has some glints in opposite corners
20:56:31 <elliott> Ah. The one I currently have then.
20:56:34 <elliott> I don't like the fact that it has two glints.
20:57:25 <elliott> Vorpal: I've died twice -- yesterday and today -- because of destroying the cart while I was in it pushing me into the block below and me suffocating.
20:57:50 <elliott> It didn't happen when health was off; I did sink but I didn't suffocate and I could easily jump back up. I don't know whether to blame health or the beta update. Sigh.
20:58:18 <elliott> Just happened again! Disconnected before I died though. Please, god, don't make me waste more of my diamond. Let me be back above.
20:58:34 <Vorpal> elliott, stop doing it then
20:58:55 <elliott> It's a habit; it's more efficient. It's Notch's bug, not mine. Now to run to the minecart station.
20:58:56 <Vorpal> elliott, I mean, doing it again and again just to complain isn't likely to be very constructive since notch is not here
20:59:48 <Vorpal> elliott, can you forget that you dislike me?
21:00:40 <elliott> Ha -- my inventory duplicated.
21:00:43 <elliott> But I can't pick up any of it.
21:00:55 <elliott> Also there's a minecart on fire.
21:01:00 -!- Sgeo has joined.
21:01:01 <elliott> Except it's a booster on the *other* track.
21:01:21 <Vorpal> elliott, dw mentioned something about something similar up north some days ago
21:01:26 <elliott> *My* cart overlapped the booster.
21:01:29 <elliott> As in, exactly on top of each other.
21:01:34 <elliott> My cart has somehow gone onto the other track, and caught fire.
21:01:53 <elliott> Also, it is seemingly invincible. I can move though it and it won't move, and I can't destroy it.
21:02:23 <Vorpal> elliott, the option in the painterly customiser is: "I want windows with reflections in the corners."
21:03:30 <Sgeo> Things can catch fire in MC?
21:03:44 <Vorpal> elliott, I can just dump the cookie it remembers things with I guess
21:03:55 <Sgeo> Project: FUCK THE WORLD
21:04:01 -!- poiuy_qwert has joined.
21:04:14 <Vorpal> elliott, http://sprunge.us/fYdb
21:04:26 <Sgeo> If you do that, I want to see screenshots
21:04:45 <Vorpal> Sgeo, they don't burn for long mostly
21:04:52 <Vorpal> and a lot of stuff don't burn at all
21:05:11 <Vorpal> elliott, I never seen minecarts burning at all. And since they are iron they shouldn't
21:05:28 <elliott> asiek2erka: http://art.penny-arcade.com/photos/1135238941_tVKGy-L.jpg
21:05:42 <elliott> Vorpal: Well, things could also pass through it. And it was invincible.
21:06:58 <Vorpal> elliott, probably a bug then
21:07:03 <Vorpal> elliott, does it actually boost?
21:07:08 <elliott> Vorpal: As I said, it wasn't a booster.
21:07:14 <elliott> Vorpal: It was just perfectly overlapped with the booster, which still moves.
21:07:21 <elliott> I have no idea how it teleported to where the booster is.
21:07:22 <Vorpal> elliott, I bet it is a client bug then
21:07:29 <elliott> Vorpal: This was after disconnecting and reconnecting.
21:07:38 <Vorpal> elliott, what if you reconnect again?
21:07:47 <elliott> Anyway, everything caught fire when I fell under the track.
21:07:54 <elliott> So presumably it teleported from there ... to where the booster was ... on the other track.
21:08:02 <elliott> And became pass-through (like see-through except, you know).
21:08:05 <Vorpal> elliott, is there any lava under the track?
21:08:21 <elliott> Yes. At least I recall burning, and I think there's obsidian there.
21:08:51 <Vorpal> elliott, idea: clear out a space tall enough to stand in below, then you won't suffocate I think, instead you /ought/ to fall through, and just get some fall damage
21:09:00 <Vorpal> and then be able to walk up given facilities for that
21:09:01 <Sgeo> How much can lava spread? Can it be pumped?
21:09:20 <Vorpal> Sgeo, which sort of lava?
21:09:22 <elliott> Vorpal: Or just wait for health to disappear again :P
21:09:27 <Sgeo> Vorpal, whichever
21:09:35 <Vorpal> Sgeo, well, define spread.
21:09:47 <Sgeo> Flow across the world
21:09:53 <Sgeo> Consuming everything
21:10:01 <Vorpal> Sgeo, 4 tiles on flat ground iirc
21:10:09 <elliott> "I mean, even a racist clock is right twice a day."
21:10:10 <Vorpal> Sgeo, it can flow over an edge and get another 4
21:10:27 <Vorpal> elliott, in fact, what is a racist clock
21:10:35 <elliott> Vorpal: --Gabe, Penny Arcade
21:10:59 -!- cheater99 has joined.
21:11:24 <elliott> Are porkchops good for two uses, or is that just SMP bugs duplicating it?
21:11:45 <Vorpal> elliott, as far as I know they 1) don't stack 2) go away in one use
21:11:55 <elliott> Vorpal: It goes away, then it reappears. Picking something up replaces it in its slot.
21:12:03 <elliott> But I think if you right click while the dupe is there it works.
21:12:03 <Vorpal> elliott, so infinite pork?
21:12:09 <elliott> It disappears the second time.
21:12:19 <Vorpal> elliott, .... does it heal the second time?
21:12:30 <elliott> But I dunno; my health bar is full.
21:12:35 <elliott> It wasn't very reliable on the survival server.
21:12:48 <elliott> Feel free to jump off a cliff and test it :P
21:13:03 -!- cheater99 has quit (Read error: Connection reset by peer).
21:13:16 <elliott> The Hoover farm is terribly positioned.
21:13:21 <elliott> You have to jump almost over it to get to the mines the way I do.
21:13:32 <Vorpal> elliott, uh. why not walk around it a bit
21:13:40 <elliott> Then I jumped, and miscalculated.
21:13:44 <elliott> Slam, fence. Boing boing boing.
21:13:45 <Vorpal> elliott, you don't want to jump onto the farmland anyway
21:14:26 <Vorpal> elliott, uh did you take the long stairs. Don't they go just past?
21:15:08 <Vorpal> elliott, go past the point of the end of the farm, such that the farm is alongside the straight stairs
21:16:14 <elliott> They emerge a little bit from the farm.
21:16:17 <Vorpal> elliott, thing I don't like with painterly: every pack icon has a creeper
21:16:21 <elliott> But yes, I could go straight but I'd have to turn after that.
21:16:27 <elliott> Vorpal: Is there something wrong with that? :P
21:16:42 <elliott> Ahhh, home sweet Hoover Heavy Industries Research Facility.
21:16:49 <Vorpal> well, you don't see it often, but mmm... I don't like creepers
21:18:11 <Vorpal> elliott, does mcmap work yet?
21:18:17 <elliott> Vorpal: Yes. More or less.
21:18:32 <elliott> I wonder if phanty would object to me expanding the HHI research facility; it is rather small.
21:19:51 <elliott> Sgeo: Hoover Heavy Industries.
21:19:58 <elliott> Our services include many services. All our services are secret.
21:20:07 <elliott> If you wish to make use of our services, contact us with money.
21:22:43 <Sgeo> "After experimenting with the device for nearly two days, three Baptist Pastors were hospitalized with broken hips, two 14 year old girls were accidentally impregnated, and one 10-year old boy had his testicles permanently damaged."
21:23:58 <Sgeo> elliott is now a Microsoft fan.
21:24:09 <Sgeo> http://www.landoverbaptist.org/2010/december/luciferstoychest2010.html
21:24:17 <elliott> Oh man, I thought it was a real thing :(
21:25:22 <elliott> "Discerning Christian parents will immediately recognize the "Mindflex" as a crudely designed masturbation device. Simply put, it is cheap imitation of Scientology's, E-Meter - "E" meaning, "Eeeee!" or "OUCH!" as our team of specialists can attest to after squatting down on both devices for seven days."
21:25:55 <oerjan> elliott: here's for you http://www.reddit.com/r/circlejerk/comments/eqw92/i_wish_atheist_redditors_a_very_merry_xmas/
21:26:16 <elliott> oerjan: ah, /r/circlejerk ... the more moderate version of the rest of reddit
21:27:24 <oerjan> i guess this is a sign of advanced addiction
21:27:35 <elliott> Vorpal: http://www.minecraftforum.net/viewtopic.php?f=25&t=55700&start=300
21:27:45 -!- SgeoN1 has joined.
21:27:45 <elliott> Vorpal: leave the map one off but turn on better grass and light is what i'd recommend :P
21:27:53 <elliott> http://www.minecraftforum.net/viewtopic.php?f=25&t=55700
21:28:08 <elliott> Vorpal: bettergrass requires betterlight, so
21:28:14 <SgeoN1> Dear computer: What the fucking fucking fuck?
21:28:21 <Vorpal> elliott, EINSUFFICIENTCOMPUTER
21:28:35 <elliott> Vorpal: barely slows down at all
21:28:44 <elliott> Vorpal: the slowdown was from me also using far and fancy which my computer can't even remotely handle /anyway/
21:28:49 <Vorpal> elliott, besides I like the worse light. Useful when building something to match up an overhang
21:28:53 <SgeoN1> Windows, or something claiming to be such, I guess, told me it was low on memory
21:29:01 <Vorpal> elliott, you can see exactly where you need to go based on the shadow :P
21:29:09 <SgeoN1> Now the screen is blank
21:29:52 <Vorpal> SgeoN1, I never had that happen on linux (har har)
21:29:55 -!- cheater99 has joined.
21:30:05 * SgeoN1 wonders if there's any malware that fakes that
21:30:09 <Vorpal> (it generally never told me first, and I blame nvidia when things went shit)
21:31:00 <Vorpal> SgeoN1, yeah, and OOM should not cause that
21:31:02 -!- Sgeo has quit (Ping timeout: 240 seconds).
21:32:16 -!- cheater99 has quit (Read error: Connection reset by peer).
21:32:44 <Vorpal> elliott, nah, I don't want better light, it seems to make things look dark based on screenshots
21:33:28 <Vorpal> elliott, all I want is to make 2/3rd side grass work with painterly and biome grass
21:33:44 <elliott> Vorpal: it doesn't, i've used it
21:33:52 <elliott> it's easy to uninstall, just rm -rf bin
21:34:35 -!- SimonRC has quit (Ping timeout: 265 seconds).
21:36:17 -!- SimonRC has joined.
21:39:10 <fizzie> Yeah, I think you either have to choose no side-grass, inconsistent side-grass or just single-color all-grass.
21:41:12 <Vorpal> fizzie, there isn't no-side grass iirc, Even the default pack has some side grass
21:41:23 <Vorpal> fizzie, does it work with the small setting on side grass?
21:41:49 -!- Sgeo has joined.
21:41:49 <Vorpal> fizzie, but it does for the default texture pack!
21:42:11 <fizzie> Yeah, but the thing that loads from texture packs can't biomize sidecrass, I think. Or something like that, anyway.
21:42:11 <Sgeo> Damn farkers can be idiots. I think about half of them aren't sure if Landover Baptist is parody
21:42:18 <elliott> fizzie: Or you can have biome-compliant 1/1 grass.
21:42:20 <Sgeo> http://www.fark.com/cgi/comments.pl?IDLink=5847704
21:42:22 <Vorpal> fizzie, is there any mode for that?
21:42:37 <Vorpal> elliott, I don't want /complete/ side grass
21:42:45 <Vorpal> elliott, I want the 2/3rd option in painterly
21:42:45 <elliott> Vorpal: Um, that's what Better Grass does.
21:42:50 <Vorpal> elliott, yes and I don't want that
21:43:00 <elliott> Well, tough, you can't have it.
21:43:33 <Vorpal> elliott, quite, but probably there is some other mod
21:44:10 <fizzie> It'll probably get officially fixed too at some point. Ot
21:44:19 <fizzie> It's there in the top-ten of getsatisfaction common-problems.
21:45:03 <elliott> asiek2erka: Your game won't even start.
21:46:18 <elliott> asiek2erka: No it won't, I just tried.
21:46:23 <elliott> Unless there's a special key to start.
21:46:56 <elliott> OpenJDK, and no, I'm not changing; if it doesn't work, it's a problem in your code. And Sun's JVM *is* HotSpot, and IcedTea *is* OpenJDK (well, almost; slightly different VM is the only difference.)
21:47:21 <asiek2erka> i dont even know where the **** you can get openjdk for windows
21:47:44 <elliott> "Download and install the open-source JDK 6 for Ubuntu 8.04 (or later), Fedora 9 (or later), Red Hat Enterprise Linux 5, openSUSE 11.1, Debian GNU/Linux 5.0, or OpenSolaris. If you came here looking for JDK 6 product binaries for Solaris, Linux, or Windows, which are based largely on the same code, you can download them from java.sun.com."
21:47:56 <elliott> The code is basically identical.
21:48:00 <elliott> So it's your code's fault; fix it.
21:48:28 <elliott> OpenJDK implements everything.
21:48:33 <elliott> I see the menu, I just can't select any of the options.
21:48:38 <elliott> Using arrow keys, WASD, space, enter.
21:48:55 -!- cheater99 has joined.
21:49:02 <fizzie> It does implement the ImageIO stuff, though there were some OpenJDK imageio bugs I had to work-around in one project.
21:49:13 <fizzie> Something related to filters, I forget what exactly.
21:49:28 <Vorpal> asiek2erka, what is this game (note I only have openjdk and/or icedtea as well)
21:49:42 <asiek2erka> it's an ASCII infinite open world game
21:49:59 <Vorpal> asiek2erka, wait, why do I get dejavu
21:50:08 <elliott> asiek2erka: Add WASD keys.
21:50:19 <elliott> Vorpal: BUT ZOMG, JEB VISITED!1129012012
21:50:36 <elliott> Well, they don't do anything.
21:50:40 <asiek2erka> C:\Documents and Settings\[username]\.64pixels\config.txt
21:50:41 <Vorpal> asiek2erka, also ascii?
21:50:49 <Vorpal> asiek2erka, I see graphics
21:50:50 <elliott> asiek2erka: No. Make them work by default.
21:50:55 <elliott> Vorpal: It's DOS codepage.
21:50:59 <elliott> Vorpal: So what idiots think "ASCII" is.
21:51:10 <elliott> asiek2erka: They do nothing by default, so there is no reason not to have them work.
21:51:10 -!- cheater99 has quit (Read error: Connection reset by peer).
21:51:16 <Vorpal> asiek2erka, do arrow keys work then
21:52:03 <Vorpal> elliott, if it is a dos code page, it seems unlikely to work under linux?
21:52:14 <asiek2erka> the charset is a raw dump of the CGA ROM
21:52:28 <asiek2erka> as the CGA ROM is most likely copyrighted
21:52:30 <Vorpal> http://64pixels.org/scr5.png "64pixels 0.0.3.1, a random creation" <-- the hell
21:52:38 <Vorpal> elliott, doesn't that look familiar to you
21:52:41 * Sgeo falls in love with the Landover Baptist Bible Quizes
21:52:49 <elliott> Vorpal: One might consider it is intentional.
21:52:57 <Vorpal> elliott, sure, but the title!
21:52:57 <elliott> That's not the player thing, anyway.
21:53:12 <elliott> Does this thing have any monsters?
21:53:33 <elliott> I can do that without being a smiley face.
21:53:39 <asiek2erka> http://www.youtube.com/watch?v=0M90Hq4u3nQ
21:53:42 <fizzie> Font.getStringBounds was bugged in OpenJDK, and TextLayout.getBounds() returned Y=x in Sun's runtime, Y=-x in OpenJDK. And there was some unidentifiable problem in that doing AffineTransformOp.filter() didn't work, while drawImage() with the op did. I think all these have long since been fixed, though, this was two years ago.
21:53:44 <Vorpal> asiek2erka, are you a developer on this? (are there any other ones?)
21:53:50 <Vorpal> asiek2erka, and, how many people play it?
21:53:53 <elliott> You know, having right-clicking instantly erase anything is perhaps not such a good idea for vandalism prevention.
21:53:57 <elliott> Vorpal: JEB PLAYED IT ONCE BEST GAME EVER
21:54:04 <asiek2erka> Vorpal: yes, GreaseMonkey helps me a bit
21:54:19 <elliott> "The idiot of the channel helps me occasionally!"
21:54:41 <asiek2erka> i'm putting that into the game's protocol
21:54:45 <elliott> Wait, is the space just randomly filled?
21:54:57 <elliott> ...so you've built like two things.
21:55:26 <asiek2erka> but our server admin destroyed the forum database
21:55:33 <elliott> ...and that destroyed the world
21:55:36 <elliott> http://64pixels.org/mods.html In what universe does this count as modding?
21:55:42 <Vorpal> elliott, if you call GM the "idiot of the channel"... what do you call asiek2erka?
21:55:44 <elliott> OMG I CONFIGURED FIREFOX TODAY -- TOTALLY MODDED
21:55:48 <Vorpal> asiek2erka, and why the nick change
21:55:59 <elliott> (it's ok, he said I could discriminate based on age!)
21:56:23 <Vorpal> elliott, are you 14 or 15 now? I forgot
21:56:48 <Vorpal> elliott, still 13 emotionally sometimes.
21:56:57 <elliott> Yeah, and you're so mature.
21:57:06 <Vorpal> elliott, did I claim that? I don't think I did.
21:57:22 <elliott> I'm an asshole? Wow, I never realised.
21:58:12 * elliott wonders if asiek2erka actually knows what Inland Revenue is at all.
21:59:00 * asiek2erka wonders if elliott has to be so !@#$ing picky
21:59:22 <elliott> I took the topmost flowers and nothing happened.
21:59:36 <asiek2erka> also wait, you got the game to work? :P
21:59:43 -!- asiek2erka has changed nick to asie[afk].
21:59:45 <elliott> Umm. No, I don't think I'm going to bother to figure out how to switch blocks./
21:59:56 <elliott> "DON'T LEAVE CLOCKS RUNNING THEY WASTE BANDWIDTH" -- how on earth.
22:00:03 <elliott> Does it make a network connection for every tick or something?
22:00:19 <Vorpal> elliott, local game or multiplayer?
22:00:37 <Vorpal> elliott, now to work on the pc speaker player coder
22:00:48 <elliott> One wonders if it is not asie[afk] and GreaseMonkey merely not knowing what "bandwidth" means.
22:07:53 -!- cheater99 has joined.
22:09:02 <Vorpal> * Emit tone of frequency thz for given number of centisecs
22:09:02 <Vorpal> static void tone(unsigned int thz, unsigned int centisecs)
22:09:09 <Vorpal> elliott, thz sounds so strange
22:10:01 -!- cheater99 has quit (Read error: Connection reset by peer).
22:14:20 -!- elliott has quit (Ping timeout: 272 seconds).
22:21:05 -!- elliott has joined.
22:23:02 -!- zzo38 has joined.
22:26:35 <Vorpal> what, the program runs okay under gdb but malfunctions when ran alone
22:26:55 -!- cheater99 has joined.
22:27:53 <Vorpal> elliott, valgrind reports nothing
22:27:57 <zzo38> Vorpal: That has happened to me before, but I figured out the problem and corrected it.
22:27:59 <fizzie> That's not really very "what".
22:28:03 <Vorpal> and it still malfunctions under valgrind
22:28:15 <fizzie> gdb does affect uninitialized memory contents and such.
22:28:29 <Vorpal> fizzie, but 1) valgrind reports nothing 2) it still malfunctions there
22:28:32 <fizzie> Though valgrind often catches that sort of stuff, admittedly.
22:28:33 <elliott> i probably shouldn't wander around minecraft with nothing to do.
22:28:45 <Vorpal> fizzie, my guess atm is that ptrace changes something about how the system call works
22:28:57 <elliott> why are there little blue pixels in my painterly trees
22:29:02 <Vorpal> which I /should/ handle, but who knows if that is buggy
22:29:35 -!- cheater99 has quit (Read error: Connection reset by peer).
22:36:24 <zzo38> Did you know I have played D&D game today?
22:40:27 <elliott> Mrf, what's the keys to rearrange tabs in xchat again?
22:40:30 <Vorpal> fizzie, the bug was actually that I typoed argv[1] as argv[0]
22:40:33 <elliott> I accidentally moved #esoteric to the left of freenode.
22:40:33 -!- hagb4rd has joined.
22:40:39 <elliott> Vorpal: Just mv the program before executing it.
22:40:44 <Vorpal> fizzie, that plus a number of coincidences
22:40:50 <Vorpal> elliott, quite esoteric yeah
22:41:39 <Vorpal> the strings from http://svn.freebsd.org/viewvc/base/release/8.1.0/usr.sbin/spkrtest/spkrtest.sh?revision=210188&view=markup is now playable on a linux pc speaker!
22:42:21 <Vorpal> elliott, sounds better on my thinkpad, where it is just a pure tone through the usual speakers
22:42:36 <elliott> Vorpal: Let's build a hi-fi USB PC speaker.
22:42:45 <elliott> So you can listen to it in all its glory on a laptop.
22:42:49 <elliott> A *real* one too -- as in the actual same mechanics.
22:42:56 <Vorpal> elliott, well my desktop has that
22:43:10 <elliott> Vorpal: Are all the components isolated?
22:43:15 <Vorpal> elliott, however this needs root to run.
22:43:23 <Vorpal> which makes me nervous while debugging
22:43:32 <Vorpal> elliott, I need to open /dev/console
22:43:37 <Vorpal> elliott, and do some ioctls on it
22:43:47 <Vorpal> elliott, this needs either running from a vt
22:44:02 <Vorpal> elliott, so it won't need root if you run it from a vt
22:44:45 <Vorpal> elliott, well, I guess it is because /dev/console depends on the owner of the current console. And when you are in X then X owns that vt
22:44:52 <elliott> Vorpal: Why on earth does that thing write to a choices file?
22:44:54 <Vorpal> elliott, and X runs as root
22:44:59 <elliott> Couldn't it just assign to a variable?
22:45:04 <Vorpal> elliott, I have no idea
22:45:30 <Vorpal> elliott, on freebsd it needs root too iirc, but only because the default permissions of /dev/speaker
22:46:25 -!- cheater99 has joined.
22:46:26 -!- Wamanuz3 has quit (Read error: Connection reset by peer).
22:46:33 <Vorpal> elliott, hm... also I'm not sure if I can get the exact timing of freebsd. After all, on freebsd this happens in kernel
22:46:39 <Vorpal> and well, there is no buffer
22:46:52 -!- Wamanuz3 has joined.
22:46:54 <elliott> I wonder if I could transfer the IΞ type system to a term rewriting system.
22:47:45 <Vorpal> elliott, btw I made the backend code very easy to replace for different systems. Should be just two functions to rewrite (plus maybe some POSIX-isms) to port it to windows. If anyone wants to
22:48:08 <Vorpal> (those functions: beep(freq, duration_in_ms), sleep(duration_in_ms)
22:48:26 -!- cheater99 has quit (Read error: Connection reset by peer).
22:49:07 <elliott> Vorpal: Um, did you really call it sleep()?
22:49:25 <Vorpal> elliott, I call it hw_beep and hw_sleep
22:49:32 <Vorpal> elliott, and I don't call it "duration_in_ms" either
22:49:43 <elliott> Vorpal: Couldn't you just usleep(x*whatever_factor_i_forget)
22:49:59 <Vorpal> elliott, usleep: no such thing in POSIX-2008. Besides it isn't portable C.
22:50:04 <hagb4rd> unbelievable.. just made a bet with a friend that the incredible machine of elliott is online, keepin the synapses of the rest well heated
22:50:05 <Vorpal> elliott, I use nanosleep
22:50:14 <Vorpal> elliott, since that is what replaced usleep
22:50:30 <Vorpal> elliott, usleep was made obsolete in POSIX 2001 and removed in 2008
22:50:42 <elliott> Vorpal: no you're destroying all the synapses
22:50:48 <elliott> FUN FACT i have no physical form
22:50:52 <hagb4rd> np.. it's good to have you here
22:50:53 <Vorpal> <elliott> Vorpal: no you're destroying all the synapses
22:51:06 <Vorpal> elliott, maybe you misread: <hagb4rd> merry xmas folks ;) <Vorpal> hagb4rd, same!
22:51:12 <elliott> I actually can't leave, watch:
22:51:12 -!- elliott has left (?).
22:51:12 -!- elliott has joined.
22:51:35 <Vorpal> elliott, I can't leave however (channel is sticky in bouncer, it will filter /part)
22:51:35 <elliott> It is my punishment, to stay in here for eternity. Well, specifically, to stay in here for eternity with Vorpal.
22:52:18 <elliott> So is anybody going to MC today? :p
22:52:27 <Vorpal> elliott, I was on for a bit, but pc speaker is funnier!
22:52:55 <zzo38> I played D&D game today. Do you think I won?
22:53:10 <Vorpal> elliott, I should upload this code, but I don't know the license. Seeing as I pretty much had to reverse engineer beep(1) to figure out how to do it on linux (really, the docs for how you interface with kernel drivers on linux *sucks*)
22:53:44 <Vorpal> elliott, and beep(1) is, as far as I can tell, GPL. The date is 1994 and the GPL is /not/ versioned. Nor is there "any future version" clause. This means in fact GPL1
22:54:00 <elliott> after all, GPL v1 is BSD-compatible
22:54:03 <Vorpal> elliott, yeah but I have no clue what GPL v1 actually is.
22:54:05 <elliott> so if you stole BSD cdoe that's ok
22:54:11 <elliott> Vorpal: http://www.gnu.org/licenses/gpl-1.0.html
22:54:13 <elliott> GNU GENERAL PUBLIC LICENSE
22:54:18 <fizzie> Vorpal: Win32 api has a Beep(DWORD dwFreq, DWORD dwDuration) in kernel32.dll that spoke directly to PC speaker; it was dropped in Vista/WinXP 64-bit (because MessageBeep did the whole beep-via-sound-card thing, unlike kernel32 Beep); and in Windows 7 they brought Beep() back but made it pass through to a sound card.
22:54:21 <Vorpal> elliott, I clearly stated that this file was same as freebsd one with minimal changes
22:54:23 <elliott> Vorpal: erm gpl v2 is from june 1991
22:54:31 <elliott> so it probably means gpl 2.
22:54:39 <zzo38> Vorpal: I think it says if it says "GPL" with no version number, you can use any version you want to unless the copyright holder tells you otherwise.
22:54:54 <elliott> zzo38: for a program predating GPL v2, even?
22:54:58 <zzo38> Or if the license is included with the program, you would use that one.
22:54:58 <Vorpal> elliott, basically, why should I write the parser code for that convoluted string when I just need to replace some types and calls and rewrite two functions
22:55:01 <elliott> Vorpal: Just say "This program is licensed under the same license as the beep tool from [wherever]."
22:55:09 <Vorpal> (I do not believe in NIH)
22:55:41 <zzo38> elliott: I think if it says "GPL" with no version specified, and the license text is not included anywhere with the program, you are permitted to use any version of the GPL. (I think I read somewhere that it works that way?)
22:55:43 <Vorpal> elliott, oh. Noodly Interspace Horror?
22:55:58 <Vorpal> elliott, isn't that a codename for flying spaghetti monster?
22:56:08 <elliott> zzo38: That's not true ... imagine before GPL version 2 came out. It wasn't called v1, it was just called the GPL.
22:56:16 <elliott> zzo38: So code licensed under "GPL" then is definitely version 1.
22:56:32 <zzo38> elliott: Then, OK.
22:56:43 <zzo38> Vorpal: OK then it is whatever version the COPYING file says.
22:56:50 <elliott> Vorpal: I don't consider reverse engineering to be virally, though.
22:57:02 <elliott> Vorpal: Copying non-trivial code, yes.
22:57:09 <elliott> Figuring out how it works and reimplementing it... naw.
22:57:38 <Vorpal> elliott, it is not the right magic constant
22:58:05 <Vorpal> elliott, anything but the one I gave and frequency will be off
22:58:07 <elliott> Vorpal: Plz make shipping go faster.
22:58:16 -!- zzo38 has quit (Remote host closed the connection).
22:58:24 -!- Wamanuz4 has joined.
22:58:25 -!- Wamanuz3 has quit (Ping timeout: 255 seconds).
22:58:26 <Vorpal> elliott, what do you mean then
22:58:48 <Vorpal> elliott, ah, I don't have any inside connections at apple
22:59:09 <elliott> I know Steve Jobs' zombie brother.
22:59:16 <elliott> But he disowned him, so GUESS THAT WON'T HELP.
22:59:28 <Vorpal> if system is loaded it won't play correctly
22:59:32 <elliott> Also, it's been dispatched, so it's probably not Apple's problem any more :P
22:59:47 <Vorpal> elliott, maybe I should try to give it real time priority?
22:59:56 <Vorpal> I wonder what function is used for that
23:00:09 <elliott> Vorpal: Just renice yourself.
23:00:33 <Vorpal> elliott, right, I was thinking real time IO priority as well
23:00:37 <elliott> Vorpal: If you try and get realtime priority when using the Brain Fuck Scheduler and you're not root, you get isochronous priority (which X runs at); it's sort of like just-below-realtime.
23:00:50 <elliott> If only it worked with non-root :P
23:01:01 <Vorpal> elliott, right, but since almost everyone use X you will end up needing root /anyway/
23:01:12 <Vorpal> besides it won't /fail/ without real time priority.
23:01:53 * elliott decides wood-bricks aren't nice, recustomises painterly
23:02:11 <elliott> Vorpal: Have you seen that insane Painterly Christmas thing?
23:02:35 <Vorpal> elliott, remember that fizzie took screenshots?
23:02:38 <elliott> I might try it. You know, just for Christmas.
23:02:41 <elliott> Vorpal: Yes, I believe I didn't look.
23:04:04 <elliott> I wish the Painterly chests/benches/furnaces/doors were less ornate.
23:04:48 <fizzie> They're a bit overdone.
23:04:55 -!- cheater99 has joined.
23:05:21 <elliott> Also the ice doesn't tile very well at all.
23:05:49 -!- Wamanuz4 has quit (Read error: Connection reset by peer).
23:06:10 -!- Wamanuz4 has joined.
23:06:44 -!- cheater99 has quit (Read error: Connection reset by peer).
23:08:47 -!- oerjan has quit (Quit: Good night).
23:11:26 <Vorpal> elliott, hm now how to change IO priority
23:13:22 <Vorpal> great, my man ioprio_set doesn't mention what headers
23:13:43 <Vorpal> should report that as a bug
23:14:50 <fizzie> Vorpal: Incidentally, since you're already running as root and worried about exact scheduling, why not sched_setscheduler a SCHED_FIFO >0 priority for your process? That way you'd get it to hang the whole machine when it goes wrong.
23:15:25 <Vorpal> fizzie, are you /sure/?
23:15:41 <fizzie> Sure about hanging or sure about that being a good idea?
23:16:02 <Vorpal> Glibc does not provide wrapper for these system calls; call them using syscall(2).
23:16:07 <Vorpal> that is why there is no header...
23:16:33 <Vorpal> elliott, on the other hand, there is another issue: where the heck do I get the macros mentioned in the man page
23:16:59 <Vorpal> also I doubt it will help anyway
23:17:09 <elliott> Vorpal: why do you need any macros?
23:17:10 <Vorpal> it seems block device IO specific
23:17:17 <elliott> <fizzie> Vorpal: Incidentally, since you're already running as root and worried about exact scheduling, why not sched_setscheduler a SCHED_FIFO >0 priority for your process? That way you'd get it to hang the whole machine when it goes wrong.
23:17:20 <elliott> since fizzie is infallible
23:17:31 <Vorpal> elliott, because int ioprio_set(int which, int who, int ioprio); and for the last argument you use macros to construct it
23:17:52 <Vorpal> elliott, it doesn't document the raw values for it
23:18:00 <Vorpal> just that it is a bitmask and you use these macros...
23:18:08 <Vorpal> elliott, anyway it won't help me
23:18:26 <fizzie> ./include/linux/ioprio.h: IOPRIO_WHO_PROCESS = 1,
23:18:26 <fizzie> ./include/linux/ioprio.h: IOPRIO_WHO_PGRP,
23:18:26 <fizzie> ./include/linux/ioprio.h: IOPRIO_WHO_USER,
23:18:38 <fizzie> (Grepping *.[ch] inside the kernel.)
23:18:55 <asie[afk]> a clock emits 120 bytes a second per player
23:19:20 <Vorpal> fizzie, yes those I have no problem with
23:19:25 -!- asie[afk] has quit.
23:19:28 <Vorpal> fizzie, I meant IOPRIO_PRIO_VALUE
23:19:37 <Vorpal> fizzie, IOPRIO_PRIO_CLASS and IOPRIO_PRIO_DATA too
23:19:53 <fizzie> Vorpal: ./include/linux/ioprio.h:#define IOPRIO_PRIO_VALUE(class, data) (((class) << IOPRIO_CLASS_SHIFT) | data)
23:20:30 <Vorpal> fizzie, anyway it won't really help me, since it seems to be block device specific
23:20:33 <fizzie> Notably they're not in my /usr/include/linux, just in the kernel source tree's include/linux subdir.
23:20:38 <Vorpal> and all I do is ioctls on a char device
23:21:10 <fizzie> Setting the scheduler would help you in the "won't let other processes get in the way" sense, but I'm not really recommending that.
23:21:32 <elliott> Just hang the system for the duration of the song. :p
23:21:51 <Vorpal> fizzie, actually I don't dare use SCHED_FIFO, SCHED_RR looks more interesting
23:22:21 <fizzie> I don't think it's any easier on the system.
23:22:27 <Vorpal> elliott, well actually I won't, since I sleep, not busy wait
23:22:32 <fizzie> It still will pre-empt everything with a lower static priority.
23:22:35 <fizzie> "Since a nonblocking infinite loop in a process scheduled under SCHED_FIFO or SCHED_RR will block all processes with lower priority forever, a software developer should always keep available on the console a shell scheduled under a higher static priority than the tested application. This will allow an emergency kill of tested real-time applications that do not block or terminate as expected."
23:22:49 <elliott> Vorpal: I lie my head on my pillow and busy-wait for eight hours.
23:23:11 <Vorpal> elliott, good night then (assuming that is how it should be read)
23:23:21 <Vorpal> elliott, also, you are going to bed early?
23:23:25 -!- cheater99 has joined.
23:24:13 <elliott> Vorpal: <Vorpal> elliott, well actually I won't, since I sleep, not busy wait
23:24:26 <elliott> "I lie" as in every night.
23:24:58 -!- cheater99 has quit (Read error: Connection reset by peer).
23:25:03 <elliott> Vorpal: I'm probably going to bed semi-early in the interest of seeing /some/ sort of light on Christmas, though. :p
23:26:27 <Vorpal> fizzie, Finland uses the proper 24th too right?
23:27:42 <fizzie> Yes. Well, for the gift-giving part and so on; the 25th is still Christmas too.
23:27:49 <Vorpal> elliott, to guarantee proper execution in the face of swap trashing I should probably memlock myself too ;P
23:28:24 <fizzie> Instead of sleep-based wait-times (which of course ignore the time you spend thinking before you invoke sleep), you might run a fixed-interval timer with a resolution small enough that you can perform all your song-related actions at the times when that fires. (Disclaimer: I don't really know how the pc-speaker IO works, and whether that's a blocking sort of thing or not.)
23:29:41 <Vorpal> fizzie, it is just ioctls
23:30:04 <Vorpal> fizzie, anyway, it seems to work well with just a -20 nice and normal scheduler
23:30:39 <Vorpal> fizzie, and your suggestion would involve rather heavy rewriting, which I don't want
23:30:55 <elliott> "The ucs2 and utf8 character sets do not support supplementary characters that lie outside the BMP." ~~MySQL
23:31:07 <fizzie> Right. Well, you could pre-build a list of actions that you do on each timer-tick, it should (theoretically speaking, anyway) be a bit more accurate than "do a thing, then sleep", which will add the "do a thing" time to all sleep values.
23:31:13 <Vorpal> fizzie, including making the playstring thingy reentrant
23:31:54 <Vorpal> fizzie, actually it will be less like the original (freebsd speaker kernel driver)
23:32:05 <Vorpal> and works the same way
23:32:26 <Vorpal> elliott, uh... what? ucs2: yeah okay, that makes sense.
23:32:27 <fizzie> I guess it depends on whether you want to match that or to conform to some sort of an ideal.
23:32:42 <Vorpal> fizzie, well I want to match
23:33:37 <Vorpal> also TOS theme on pc speaker is awesome "l2b.f+.p16a.c+.p l4mn<b.>e8a2mspg+e8c+f+8b2"
23:34:22 <fizzie> The mlock/mlockall thing could be a thing to do, of course.
23:34:58 <elliott> Anyone know how to insert UTF-8 chars with a mysql query?
23:35:06 <elliott> i.e. what escape sequences or functions or whatever
23:35:34 <elliott> ah, seems like it's CHAR()
23:36:07 <fizzie> I don't think I've got my PC speaker connected. I wonder how accurate the emulations are.
23:36:46 <fizzie> Dosbox has a 360-line PC speaker emulation code; it looks a bit simplistic compared to something like resid-fp. (Admittedly the PC speaker itself is rather simplistic compared to SID, too.)
23:39:36 -!- poiuy_qwert has quit (Quit: This computer has gone to sleep).
23:41:25 -!- cheater99 has joined.
23:41:48 <Vorpal> elliott, no need for GPLv2 any more
23:41:56 <Vorpal> will probably do *BSD then
23:42:14 <Vorpal> elliott, not BSD compatible iirc
23:43:02 <elliott> Vorpal: If you mean "but I based it on BSD code", you can still license your parts as WTFPL. Admittedly that's silly. But no, WTFPL is 100% BSD-compatible.
23:43:03 -!- cheater99 has quit (Read error: Connection reset by peer).
23:43:21 <elliott> DO WHAT THE FUCK YOU WANT TO PUBLIC LICENSE
23:43:22 <elliott> TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
23:43:22 <elliott> 0. You just DO WHAT THE FUCK YOU WANT TO.
23:43:25 <elliott> It's hard to not be compatible with that.
23:43:27 <Vorpal> elliott, it is based on BSD yeah
23:43:29 <elliott> (Also FSF-certified Free!)
23:43:44 <Vorpal> elliott, and the mix is absurd
23:43:47 <elliott> Vorpal: Right, then you can't remove the draconian BSD restrictions (such as requiring attribution).
23:43:54 <Vorpal> elliott, since the bulk of the code is the BSD code
23:43:56 <elliott> Vorpal: Hey, plenty of projects include BSD-licensed code but aren't BSD themselves, and the like. :p
23:44:02 <elliott> Admittedly generally not in the same file.
23:44:12 <Vorpal> elliott, the code that is not is basically main() + some linux specific functions
23:44:27 <elliott> I still feel kinda dirty planning to copyleft things.
23:44:38 <Vorpal> elliott, actually I split it in multiple files because I thought it would be larger than it turned out to be
23:46:52 <fizzie> Do a pulseaudio output option if you've run out of code to write. :p
23:47:16 <Vorpal> fizzie, ... what? Can it drive the pc speaker?
23:47:41 <Vorpal> also, pc speaker or nothing
23:47:49 <fizzie> No, I just mean an emulation.
23:48:27 <fizzie> Right, and for us "no speaker connected" folks. :p
23:48:28 <Vorpal> fizzie, also, shouldn't I use jackd then instead
23:48:36 <Vorpal> fizzie, well sucks to be you :P
23:48:47 <Vorpal> fizzie, /If/ I write anything it will be jackd
23:49:14 <fizzie> I don't think it really matters, since you would just be producing a PCM audio signal; anything that can play that back would be just fine, timing-wise.
23:49:23 <fizzie> It's not like the audio needs to be synchronized with anything.
23:49:55 <fizzie> If you want to be a PC speaker purist, conduct a case study of a hundred PC speakers, then try to get as close to the same sound as possible.
23:49:57 <Vorpal> fizzie, actually I should procedurally generate a soundfont, load it into the sound card, and then play midi
23:50:03 <elliott> <Vorpal> fizzie, actually I should procedurally generate a soundfont, load it into the sound card, and then play midi
23:50:10 <elliott> Make a PC speaker soundfont for an MT-32.
23:50:18 <Vorpal> elliott, I would, except I don't have one to test with
23:50:23 <Vorpal> elliott, I only have a sb live
23:50:47 <fizzie> Doesn't ALSA have some sort of a PC speaker generic-PCM output driver? You could then run your emulated audio out via that. (It would probably sound quite horrible.)
23:51:02 <elliott> Vorpal: You can have mine (note: no, it cost me £200).
23:51:27 <Sgeo> Not the least bit creepy how easy it is to find my dad and step-mom's names
23:51:29 <elliott> fizzie: How far could you recurse it, I wonder.
23:51:39 <elliott> Easy-to-find names are a sign of creepiness.
23:51:43 <Vorpal> elliott, you have one!?
23:51:59 <elliott> Vorpal: Yes. Also a theremin.;
23:52:11 <Vorpal> elliott, is it a professional one
23:52:14 <elliott> Vorpal: Hooking up the MT-32 to an iMac didn't really work so well, though; I got it working, sort of.
23:52:21 <elliott> The theremin? Yes, it's a Moog.
23:52:23 <Vorpal> elliott, or one of those with a knob for one of the things
23:52:30 <elliott> Not their high-end model (that's *lots of money*), but yes.
23:52:43 <elliott> It's BLACK WOOD... which isn't really stylish, but there you go.
23:52:43 <Vorpal> elliott, practising much?
23:52:51 <elliott> Vorpal: No, the theremin is nearly impossible to play.
23:53:03 <Vorpal> elliott, I seen people play it well
23:53:08 <Vorpal> elliott, it just require practise
23:53:12 <fizzie> elliott: You could pull out that ALSA's bit that converts the PCM signal into PC speaker programming, then use the emulation to turn that into a PCM signal, and then just iterate until it converges. (Well, except that it might well not converge or converge to something really boring; but at least a large number of time.)
23:53:15 <elliott> Vorpal: It needs a surgeon's hands.
23:53:24 <elliott> And that's not really something you can practice at.
23:53:49 <Vorpal> elliott, well I have a Roland FP-4 piano. Decent (but not state of the art)
23:54:03 <Vorpal> and I prefer to play that
23:54:34 <Vorpal> elliott, what sort of connector do you use for it?
23:54:35 <elliott> Deewiant: You can't buy them new, and they don't really degrade, so. :p
23:54:40 <elliott> Vorpal: Audio. Analogue audio.
23:54:57 <elliott> It has a MIDI input and an audio out.
23:55:03 <elliott> The fat jack-style things.
23:55:15 <fizzie> Deewiant: Some things in life money can't buy -- for everything else there is eBay. (Paraphrased from that MasterCard ad.)
23:55:21 <Vorpal> elliott, is that the same as the normal circular one?
23:55:29 <Vorpal> elliott, or is it some other one
23:55:37 <Vorpal> elliott, for midi I mean
23:55:41 <elliott> Vorpal: http://en.wikipedia.org/wiki/TRS_connector
23:55:46 <elliott> Dunno, I'll check in a minute.
23:55:49 <elliott> I have cables for it, FWIW.
23:55:54 <Vorpal> elliott, and how did you get that to work with a mac
23:56:05 <elliott> Vorpal: Via adapter, I think.
23:56:23 <Vorpal> I have a gameport<->midi cable
23:56:28 <Vorpal> that I can use with this sound card
23:56:33 <fizzie> I would certainly guess the usual DIN-5 if it's "jack-style".
23:56:53 <Vorpal> fizzie, I think he thought I asked about the audio
23:57:02 <Vorpal> anyway, midi over usb sucks
23:57:48 <Vorpal> and also, as far as I know, less real time guarantees
23:58:37 <fizzie> What I think is funny is those hybrid "3.5mm analog stereo / optical S/PDIF" connectors. It's just like a regular stereo plug except there's basically a LED deep inside there.
23:59:20 <fizzie> (What will they think of next!)
23:59:34 <Vorpal> fizzie, to save on connectors?
23:59:55 <fizzie> Yeah, you only need one hole in the laptop or whatever.
23:59:55 -!- cheater99 has joined.