00:00:37 http://www.cs.nott.ac.uk/~gmh/cat5.txt 00:00:57 initial F-algebra 00:01:17 no clue about GADT though 00:02:02 I think F-algebra will work for all simple data types 00:02:35 j-invariant: lol you might want to try and make your library multiple files 00:02:46 it's gonna be like 10,000 lines when you're done 00:03:06 I don't know how X) 00:03:23 j-invariant: I think "Require Import Foo." will work if Foo.v is in . 00:03:38 it would be good to compile each bit seperately 00:04:06 j-invariant: if you ever manage to construct lists and map inside this ... I dare you to extract "map" 00:04:20 it'll be the ugliest fucntion ever 00:04:20 hmm 00:04:21 *function 00:04:24 (when extracted) 00:04:34 I might be able to contribute to Evolution of a haskell programmer... 00:04:57 j-invariant: :D 00:04:58 brilliant 00:06:32 j-invariant: I wish Coq did some ugly special-casing for nats ... they're so slow and limited 00:06:39 I know there's the binary nats somewhere, but ... 00:07:01 yeah numbers must be implemented in binary, peano is only useful for theory 00:07:25 j-invariant: still, even the binary nats aren't so hot 00:07:34 j-invariant: I'd like it if it just special-cased nat and represented it internally as a machine word / bignum 00:07:43 but still allowed you to destruct on S to decrement one, etc 00:07:45 *etc. 00:08:03 that's a funny idea 00:08:04 fact and the like would be slow, but they wouldn't use up 34238490424 jiggabytes of memory 00:08:09 j-invariant: funny how? 00:08:37 I mean where would the implemeentaiton get the idea to use binary? 00:08:49 and more generally what else could it optimize 00:08:54 j-invariant: oh, I meant just hardcoding it ;-) 00:08:57 it's ugly as hell, certainly 00:08:59 but nats are very common 00:09:15 yes numbers seem to be special in some sense 00:09:26 I've never understood that 00:09:43 what do you mean? you mean that numbers tend to be more useful/common than non-number structures? 00:10:01 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 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 natural numbers are universal in the category of discrete dynamical systems 00:12:13 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 and disregard things that aren't so numbery 00:12:20 I mean, in a very general sense 00:12:25 thus why numbers seem pretty darn common 00:12:56 elliott: I cannot come up with any counter-argument to that but I don't think it's true 00:13:13 j-invariant: when in doubt, i like to blame humans :) 00:13:21 gah some words got stuck on my head 00:13:22 j-invariant: i mean, let's put it this way 00:13:34 j-invariant: there's as much mathematics not involving numbers as there is mathematics involving numbers. 00:13:38 for some reason I keep thinking of the phrase "high performance JIT cheese" 00:13:47 j-invariant: so the /only/ factor in consideration here is, why do the mathematics /we've explored/ involve numbers a lot? 00:13:51 and i suspect the answer is: because we like numbers 00:14:23 elliott: I haven't tested performance much 8-D 00:14:32 Gregor: That is not reassuring :-\ 00:14:42 Gregor: https://codu.org/projects/trac/sps/changeset/6%3A8584c8e2c0ed/cunionfs Why did you do this, I don't like it :p 00:14:55 p.s. 00:14:58 char *dotfile; 00:14:58 sprintf(dotfile, "%s%s", curd, CUNIONFS_DOTFILE); 00:15:00 lol unallocated? 00:15:05 oh wait you allocate it later 00:17:39 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 Gregor: Your sentence does not parse. 00:18:01 "cause packages to do things they ought to be finding files at weird paths" 00:18:38 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:19:35 Gregor: I don't get it :P 00:19:37 Example? 00:20:30 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 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 e.g., process-specific /var and /home sounds "no". 00:21:44 Union of a union... you know what, this is an EXCELLENT argument for /usr. 00:22:29 -!- hagb4rd has joined. 00:22:37 That's just a specific case, it's not really solved by contracting your unions a bit :P 00:23:00 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 elliott, as expected, getting lava from spawn no longer works 00:23:18 elliott: could a brain exist which was obsessed with something other than numbers? 00:23:42 j-invariant: Sure, why not. 00:23:53 maybe it would self destruct 00:23:57 buenas 00:24:00 j-invariant: I don't see why. 00:24:11 Gregor: Maybe I'll have no /bin, /lib, /share, and put it all in a cunionfs /usr :P 00:24:23 Gregor: / = {/usr, /var, /home, /tmp, /boot} or something. 00:24:30 Gregor: / = {/usr, /var, /home, /tmp, /boot, /etc} or something. 00:24:43 That was the original intention behind SPS :P 00:24:58 Well, I had a /bin and /lib for really-core stuff (libc, coreutils) 00:25:15 (So that if for some reason your package setup was punked, you weren't completely screwed) 00:26:31 Gregor: Well, I had a /bin and /lib for really-core stuff (libc, coreutils) 00:26:35 Gregor: cal(1) is really-core? :P 00:26:57 Dude, my system won't even BOOT without cal. 00:27:32 Gregor: The nice thing is that with Kitten, you're always completely screwed. 00:27:35 So I don't have to worry about that 00:27:37 *that! 00:27:55 Gregor, did you have stuff like fsck and mount in /bin too? 00:28:08 Gregor: On a more srs note, I can't really have a cunionfs /, because I have no initramfs in Kitten :P 00:28:12 So / kinda has to be a real drive. 00:28:26 DESCRIPTION 00:28:26 switch_root moves already mounted /proc, /dev and /sys to newroot and makes newroot the new root filesystem and starts init 00:28:26 process. 00:28:26 WARNING: switch_root removes recursively all files and directories on the current root filesystem. 00:28:27 Vorpal: Yeah 00:28:28 I wonder why it has to do that. 00:28:37 BURN YOUR BRIDGES! 00:29:17 elliott, to shrink the tmpfs size to 0 iirc 00:30:02 night → 00:31:31 Gregor: Do I get extra points if my package manager is Haskell? 00:31:39 No :P 00:32:15 Gregor: WHY NOPT 00:32:16 *NOT 00:32:30 BECAUSE HASKELL KILLED MY FAMILY 00:32:39 Gregor: Mine too! 00:33:00 OMG JOIN US IN ##haskellkilledmyfamilyanonymous 00:33:07 DONE 00:33:12 YOU'RE NOT THERE 00:33:22 ALSO YOU'RE NOT ANONYMOUS 00:33:43 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 I wouldn't be surprised if GHC can't even make static executables (without some hacking) 00:37:12 Gregor: It can, I just tried. 00:37:21 Well, THERE GOES THAT THEORY. 00:37:25 elliott@dinky:~$ ghc hello.hs -static -optl="-static" -optl="-pthread" ; ls -lh a.out 00:37:25 compilation IS NOT required 00:37:26 -rwxr-xr-x 1 elliott elliott 1.7M Dec 24 00:36 a.out 00:37:37 Post-stripping: 00:37:39 -rwxr-xr-x 1 elliott elliott 1.2M Dec 24 00:37 a.out 00:37:40 NOT BAD ACTUALY 00:37:42 *ACTUALLY 00:38:28 That's actually pretty damn good ... 00:40:32 Gregor: Dammit man -- the package manager has to be functionally pure now. 00:40:39 Gregor: You've turned my OS into a bad recreation of NixOS. 00:40:50 Gregor: _|_, and that's a middle finger, not the bottom value. 00:42:09 Gregor: Um. Question. 00:42:15 Gregor: Is "nm -a" supposed to work on statically linked executables? 00:42:17 (Unstripped ones.) 00:42:35 $ file hello 00:42:35 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 OK, it did actually work then :P 00:54:03 Gregor: Wait, can you add to the unioned directories without restarting a process? 00:59:58 Gregor: :p 01:00:07 -!- FireFly has quit (Quit: swatted to death). 01:09:13 65 pages so far! 01:09:29 Gregor: y/n? 01:10:05 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:10:29 what is it? 01:11:09 j-invariant: Are you asking me? 01:12:07 j-invariant: If you are: It is TeXnicard. 01:12:23 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 (Remember the page count of 65 pages also includes the index, summary of chunks, and table of contents.) 01:12:55 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 or even init, if you want it at every levle 01:13:01 *levl 01:13:04 *leve-fucking-l 01:15:35 Gregor: or am i mistaken :P 01:15:42 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 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 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 Do you like my ideas about package managers? Do you think they are wrong for some reason(s)? 01:16:54 zzo38: "based on pipes" isn't very descriptive 01:17:21 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 Gregor: OK, so it rereads the config file all the time? 01:17:51 I was unaware that it had configuration files. 01:17:59 elliott: I haven't re-added the configuration files :P 01:18:16 Gregor: So what you're TRYING to say is: 01:18:17 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 If you want it to be visible to anyone, reboot. 01:18:28 If you want it to be visible to a user, reboot. 01:18:33 If you want it to be visible to some process or process group, reboot. 01:18:38 That is the actual state. Yes? :P 01:18:42 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 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 Gregor: fam, but nobody uses it any more 01:18:59 gamin is used, which is a daemonless impl of the api 01:19:07 Gregor: I'm not expecting, I'm just /checking/ 01:19:17 Since your previous statement implied that there were, in fact, configuration files. 01:19:26 elliott: I mean, for example: wg -MR0 ftp://example.org/packages/* | pm -tQ | ... 01:19:33 zzo38: wg? 01:19:38 elliott: You're also expecting me to remember the exact state I abandoned it in. 01:19:51 Gregor: Well, you did just say that in retrospect it was pretty awesome earlier :P 01:20:05 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:07 elliott: And it is :P 01:20:12 And pm is package manager. 01:20:34 Gregor: I'ma go for aufs, with the magical property of allowing me to remount without reooting :P 01:20:35 *rebooting 01:20:50 (Unless "mount -o remount" would work with cunionfs? Wait, FUSE, so no.) 01:21:02 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:10 zzo38: Sure. 01:21:43 Do some package managers do that? 01:22:33 Probably. 01:23:22 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 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 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:32:51 *.net *.split 01:33:05 Vorpal: not minecrafting? 01:44:21 fizzie: WHAT THE FUCK 01:45:08 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 fizzie: I WANT MY FUCKING STUFF BACK, NOTCH ;__; 01:48:29 -!- pikhq has quit (Ping timeout: 250 seconds). 01:49:26 Iiiiit's Notch Quality! 01:50:29 -!- pikhq has joined. 01:52:17 s/ch// 01:54:35 j-invariant: i need help 01:58:53 -!- hagb4rd has joined. 02:07:06 elliott: heh me too 02:07:08 whats up? 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 I am sick of trying to defin a symbolic category, it's really hard 02:07:45 p : Z 02:07:45 q : positive 02:07:45 H : (p ^ 3 <= 3 * ' q ^ 3)%Z 02:07:45 ============================ 02:07:45 exists s : Q, 02:07:46 p # q < s /\ match s with 02:07:47 | p0 # q0 => (p0 ^ 3 <= 3 * ' q0 ^ 3)%Z 02:07:49 end 02:07:51 j-invariant: must prove. 02:09:17 j-invariant: i.e. "given an underestimate of 3root(3), generate a closer underestimate" 02:14:24 j-invariant: any ideas? :/ 02:14:32 I'm trying something righ tnow 02:16:06 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 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 j-invariant: yeah and that kinda defeats the point 02:18:47 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 j-invariant: I think this "computable Dedekind cut" approach would be nice if not for the proofs :/ 02:19:18 j-invariant: really? that theorem 02:19:24 j-invariant: would mean you can't use continued fractions for computable reals... 02:20:00 I stated it wrong 02:20:33 ah 02:21:24 http://arxiv.org/pdf/1012.1709 02:22:45 The continued fraction expansion of an algebraic number of degree at least 02:22:45 three cannot be generated by a finite automaton. 02:23:55 j-invariant: that's not good is it? 02:24:05 j-invariant: I mean could Coq do it? I don't actually know what computational class Coq is 02:26:51 elliott: my guess is that constructive dedekind cuts are what intuitionists that have never seen a computer use 02:27:24 j-invariant: :D 02:28:37 j-invariant: have you ever used c-corn's constructive reals? 02:28:41 no 02:29:15 hm what does :> mean again? in a coq type 02:29:16 as opposed to : 02:29:21 in a record field declaration 02:29:48 it's something to do with pretening the record is another type 02:31:38 weird 02:31:46 j-invariant: hmm you mean like 02:31:51 Record blah := mkBlah { foo :> nat; bar : ... } 02:31:54 you could use a blah as a nat? 02:32:47 yes 02:32:56 well I don't really know I don't use that, but it's something like that 02:33:00 j-invariant: I could do algebraic structures like that! 02:33:02 TIME TO TRY IT OUT 02:33:23 leave king dedede... sorry, dede.v for now 02:33:26 I still haven't been able to define this damned symbolc category 02:33:32 j-invariant: what category is it exactly? 02:33:51 actually it's just graphs, that's a simpler way to think of it. 02:34:18 how do you disable the coq stdlib in the file again? :/ 02:34:21 oh wait i have it here somewhere 02:34:27 actually graph isn't right 02:34:34 (* 02:34:34 *** Local Variables: *** 02:34:34 *** coq-prog-args: ("-emacs-U" "-nois") *** 02:34:34 *** End: *** 02:34:34 *) 02:34:35 right? 02:35:03 The idea is: Inductive Symbolic_Maps : nat -> nat -> Type := f 3 4 | h 2 1 | k 2 1 | m 3 4. 02:35:09 er 02:35:16 that was a bad example 02:35:30 lets take Inductive Symbolic_Maps : nat -> nat -> Type := f 3 4 | h 4 1 | k 1 6 | m 3 4. 02:35:44 is 3 the type w/ three elements? 02:35:45 here 02:35:54 no just the number 3, or it could be any symbolc 02:36:07 so f : Symbolic_Maps 3 4 02:36:17 ah 02:36:50 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 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 but a functor from Symbolic -> C would prove the same identity in any other category 02:38:26 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 j-invariant: I wish Coq had like, a minimal stdlib with it 02:44:14 giving eq, exists, that kind of stuff 02:44:18 rather than having to code it myself 02:44:41 You can use mine 02:45:02 j-invariant: got a link again? 02:45:21 http://pastebin.com/BQaW0Cdb this is before I start defining category 02:45:43 thanks, I'll nab useful bits from there as I go :) 02:45:43 Decidable is spelled wrong :/ 02:45:50 j-invariant: Coq has And/Or built in doesn't it? 02:45:56 what does "# Arguments." do :P 02:45:58 no 02:46:24 mispaste, should have been Set Implicit Arguments. 02:47:35 j-invariant: I think set implicit arguments actually gets in my way 02:47:46 it's nice to have to specify what gets implicit-ified 02:49:34 Inductive or (P Q : Prop) : Prop := 02:49:34 | zig : P -> or P Q 02:49:34 | zag : Q -> or P Q. 02:49:36 i like my names more 02:53:45 heheh 02:54:29 * Sgeo assassinates Active Worlds's asinine update methods 02:58:30 Error: Unknown interpretation for notation "_ /\ _". 02:58:32 what does that mean again? 02:58:39 oh 02:58:51 there we go 03:00:17 :( my symbolic category does not work 03:00:41 :/ 03:00:48 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:01 rings because that has two operations? 03:01:09 j-invariant: because it's a combination of two structures, basically 03:01:15 j-invariant: and my structures have set fields 03:01:23 j-invariant: I might restructure them to be Prop-records parameterised on type 03:01:27 but IIRC that didn't work last time I tried 03:01:40 this really sucks, F(f o g) doesn't evaluate to Ff ' Fg, should have known that 03:01:45 Ff o Fg 03:02:10 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 but if I make composition syntactic in the symbolic category then I don't get the proofs for free.. damned either way 03:03:25 Record pseudo_ring := { 03:03:25 pr_ag :> abelian_group; 03:03:25 pr_sg :> semigroup; 03:03:25 pr_left_dist : 03:03:25 forall a b c : 03:03:28 i mean do you write pr_ag or pr_sg 03:03:31 both give you problem 03:03:32 s 03:03:40 if I could refer to the record itself somehow there, that might work 03:03:55 j-invariant: who needs proofs for free :) 03:03:58 me! 03:04:29 http://coq.pastebin.com/DzVkdQbV <- broken 03:04:45 starts at line 629 03:04:59 j-invariant: i did your proof 03:05:02 j-invariant: just add one line 03:05:03 Admitted. 03:05:05 elliott: I'll just use a syntactic compose, and write a decision theorem 03:05:52 I will not admit defeat 03:08:15 Record magma S := { 03:08:15 mg_S :> Set := S; 03:08:15 mg_op : mg_S -> mg_S -> mg_S 03:08:15 }. 03:08:15 Implicit Arguments mg_op [S m]. 03:08:16 Theorem magma_is_set : forall S (m : magma S), mg_S m = S. 03:08:18 intros; apply refl. 03:08:20 Qed. 03:08:22 now THIS might work!! 03:09:07 what's that theorem about? 03:10:06 j-invariant: just checking coercion works :P 03:10:22 ah 03:10:44 the biggest problem for me is I don't want to use Set 03:11:01 I need something like NxN/~ for some equivalence 03:11:10 I thought category theory would solve it :/ 03:11:18 well, it does - I just don't see how yet 03:13:02 j-invariant: category theory solves EVERYTHING!!!!!!! 03:13:20 it bloody well better after all this hard work :p 03:18:29 j-invariant: i got pseudorings! 03:18:54 cool 03:19:52 j-invariant: got any nice theorems about pseudorings/rngs? :p 03:19:56 i wanna see if this actually works 03:20:08 I don't even know what it is LOL 03:20:15 something weaker than ring 03:20:29 j-invariant: http://en.wikipedia.org/wiki/Pseudo-ring 03:20:43 j-invariant: abelian ring (R,+) and semigroup (R,*) where * and + distribute 03:22:22 Ring 03:22:22 Pseudoring with identity element 1 for • (monoid) 03:22:25 aha 03:22:35 so i just need it to be that my pseudo-ring's semigroup must be a monoid too 03:23:32 Record ring S := { 03:23:32 rg_S :> pseudo_ring S; 03:23:32 rg_sg_is_monoid : monoid (pr_sg rg_S) 03:23:32 }. 03:23:32 what. 03:23:34 that was stupid easy. 03:23:55 time to try Z I guess 03:24:29 try to prove 0*x = 0 in ring 03:24:51 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 even though it turns into + in higher structurse 03:24:56 *structures 03:24:59 and everyone says 1 even when it's 0 03:25:03 SO CONFUZZLING 03:26:50 S : Set 03:26:50 R : ring S 03:26:50 a : R 03:26:50 ============================ 03:26:50 mn_1 * a = mn_1 03:26:53 i think this is a problem with my scheme 03:27:00 every structure on the same set looks the same to coq 03:28:24 ============================ 03:28:24 monoid ?385 03:28:25 hnnnnnnng 03:28:37 j-invariant: are you sure coq doesn't have a tactic for "let me specify this ?385 now"? :( 03:28:43 it does 03:28:47 instantiate (1 := ...) 03:29:03 j-invariant: no, but like 03:29:05 instantiate 1. 03:29:08 and it becomes the new goal 03:29:46 j-invariant: and pushes the current goal to the end 03:30:50 j-invariant: surely it must exist, i mean it'd be so useful 03:31:11 oh I don't think that exists 03:31:16 yeah that would bereally useful though 03:37:57 I think I'm going to write eval in c using exec to call out to gcc, dlopen and dlsym... tomorrow. 03:37:57 Suck it, Lisp weenies. 03:37:58 -!- Sasha has quit (Read error: Connection reset by peer). 03:37:58 ...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 I wonder how I can avoid just reinventing Nix. 03:50:52 [[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 I did my first programming when I was eight. I'm 30 now.]] 03:51:02 Fun fact: Notch's programming skills decrease every passing day. 03:51:05 Also: 03:51:07 [[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 Possibly, yes, but how do I make a cube based female model without being extremely silly and/or slightly objectifying?]] 03:51:16 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 Hmm. Xiph is working on a new audio codec... 04:51:24 http://people.xiph.org/~xiphmont/demo/celt/download1/celt-0.10.0-32.flac This is what it sounds like at *32 kbps*. 04:53:47 wow 04:54:01 hard to beleive 04:54:24 -!- j-invariant has quit (Quit: leaving). 04:54:30 pikhq: wanna write something on my blog 04:54:48 unless you have a blog (then there would be no point!!!) 04:55:01 * pikhq haþ no blog 04:56:11 pikhq: ok, well you seem like an intelligent, fun-loving guy 04:56:20 u should """""guest post""""" 05:04:29 pikhq: r u interested? 05:06:11 Perhaps. 05:08:51 * Sgeo once tried to sudo on his school's Linux system 05:09:13 Mistook that console window for the console window for my system 05:10:37 pikhq: u should www.symbo1ics.com/blog 05:15:20 Sgeo: did it get noticed? 05:16:40 Mathnerd314, no idea 05:16:46 I sent some mail to the sysadmin about it 05:18:53 Sgeo: any relation to xkcd? 05:20:03 xkcd is the reason that I thought of it just now 05:20:56 http://25.media.tumblr.com/tumblr_lc1hqgvA8F1qzymhso1_500.gif 05:23:15 * Sgeo pukes on Quadrescence 05:23:27 STOP THAT SGEO 05:23:52 Quadrescence, you're the one who posted that disgusting link 05:25:09 http://media.damnfunnypictures.com/photos/j0xqdn9-animal-tortoise-turtle-ucumari.jpg 05:26:11 I prefer that to the comic 05:35:06 * Mathnerd314 goes back to reading llvm 05:48:47 -!- pikhq has quit (Ping timeout: 265 seconds). 05:50:32 -!- pikhq has joined. 06:10:20 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 Well, aside from being unhumanly accurately played. 06:11:37 hmm, I'm always surprised by what *isn't* synthed 06:14:03 seriously, there ought to be no real barriers to me deciding to make some music *right now* 06:15:44 except talent. 06:15:47 * oerjan ducks 06:16:21 well, yeah, I'll agree that reading documentation is always a good idea 06:16:48 oerjan: This is why only Gregor makes music here. 06:17:02 He is not a man! He is walking, typing, hat-wearing talent! 06:17:52 and simultaneously! 06:18:30 even while chewing gum! 06:18:36 there's Isle of Tune, but it's too limited: http://isleoftune.com/ 06:19:43 As such is his talent! 06:19:53 He is so talented that he is talent *with talent*! 06:21:01 but AFAICT, there's no single FLOSS "music making" program 06:31:29 Who needs a program? 06:31:35 All you need is talent! 06:31:54 With talent, you can just bit-bang out the FLAC you want! 06:32:12 (note: I in no way advocate actually bit-banging a FLAC to generate music. God no.) 06:32:47 bit-bang? 06:32:57 O... literally writing the bits? 06:33:27 Actually, what would such a thing sound like? 06:33:55 Obviously, I should do it 06:35:03 Sgeo: tristan perich writes one-bit music: music played by an arduino without a dac (and therefore using nothing but square waves) 06:37:09 pikhq: then what are you advocating? 06:38:47 Mathnerd314: this is FLOSS afaict: http://chuck.cs.princeton.edu/release/ 06:38:58 if you like live coding :P 06:39:07 Mathnerd314: I don't know, but it should be PAINFUL 06:40:03 i also once composed a piece in audacity 06:40:06 from scratch 06:40:09 that was painful 06:41:02 pikhq: life is pain. so that's satisfied. 06:41:19 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 quintopia: Doesn't it anyways? 06:42:23 pikhq: it didn't blow up until 20 tracks on my old fast memoriful computer 06:42:34 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 Ha ha! Now push the "EXPLODE" button and your television set will explode. 07:01:13 Hey, I used Audacity to record my karaoke! 07:01:19 * pikhq pushes zzo38's EXPLODE button 07:01:38 zzo38: since pikhq is not interested in writing on my blog, do you wanna 07:01:43 Sgeo: Does it work? 07:01:52 -!- Zuu has quit (Read error: Connection reset by peer). 07:01:55 Quadrescence: What do you want written on it? It depends. 07:01:55 zzo38, I have a scapegoat for my horrible singing! 07:02:03 zzo38: http://symbo1ics.com/blog/ 07:02:10 stuff about stuff 07:02:34 write whatever you want as long as it's expository in nature (and ideally about math or compsci?!?!?!) 07:03:41 (enable js) 07:04:02 i know a blog written entirely in haskell that uses no js 07:04:29 yeah damn cale 07:04:30 it contains several tech topics 07:04:31 Quadrescence: What do you want me to do, add comments? 07:04:36 * pikhq is now frightened. 07:04:39 zzo38: no, i'd give you an account 07:04:48 FFXII has an optional boss with 50 million HP. 07:04:48 zzo38: and you could write a (some) posts about whatever if you wanted 07:04:55 It can apparently take 12 hours. 07:06:12 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 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:18 zzo38: what 07:07:49 http://static.tvtropes.org/pmwiki/pub/images/yiazmat3.jpg Each one of those dots is a full health bar. 07:08:17 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:32 12 hours seems reasonable 07:08:43 can you save your progress and come back to it? 07:09:03 zzo38, did you write PhlogJournal yourself? 07:09:07 * Sgeo guesses yes 07:09:10 Sgeo: Yes, I wrote it myself. 07:09:20 * Sgeo is obviously a future psychic 07:09:22 zzo38: the point is that anyone can have an account and anyone can log in and everything is secure 07:09:52 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 Quadrescence: Then why don't you juse use ssh then? 07:10:18 Grrrrr 07:10:26 Why doesn't Chrome support gopher? 07:10:33 -!- Zuu has joined. 07:10:33 Does Opera support gopher? 07:10:45 zzo38: I want several people to have access, and since I type math, I want javascript to be enabled 07:11:20 Sgeo: Neither Chrome or Opera does. But you can use netcat: echo 'phlog*f0' | nc -q -1 zzo38computer.cjb.net 80 > PhlogJournal.php 07:11:43 that is the worst way to view a blog :( 07:12:03 Quadrescence, that's downloading the source for the engine 07:12:08 oh okay 07:12:43 what's cool about phlog? 07:13:38 quintopia: Well, look at the codes if you want to. It is very simple but does calendars, comment system, and more. 07:13:58 Without slowing down your computer with JavaScript and images and stuff like that. 07:14:56 zzo38: WHAT ABOUT LATEX RENDERING WITH NATIVE FONTS 07:15:25 that's the only thing I really use JS for 07:15:29 i'm getting a 501 on your nc command up thhere? :/ 07:15:46 Quadrescence: Then just use LaTeX to make a printout. 07:15:56 quintopia: Sorry, that is because I accidentally typed 8 instead of 7. 07:15:57 Quadrescence: that's lame. images are okay. 07:16:06 Change the 8 to 7 (they are close to each other on the keyboard) 07:16:09 And then it will work. 07:16:14 quintopia: no it's quite not lame 07:16:29 thx 07:16:31 quintopia: images assume the user has some sized screen at some resolution 07:17:01 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 Port 70/TCP? Gopher? 07:17:16 Ilari: Yes. 07:17:30 zzo38: the point of a blog is to blog, and one can use TeX to do stuff on it 07:18:13 Quadrescence: Could you write a blog program in TeX? 07:18:30 what? 07:18:35 one *could* I guess 07:18:48 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:18:48 do you mean "a tex program on the blog"? 07:19:11 quintopia: what 07:19:36 there really should be a css way to do that though :/ 07:19:50 images are just a poor option when you can do native TeX typesetting and use Real Fonts 07:19:58 mathml is bad, but jsmath is good 07:20:06 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 jsmath is slow and hangs a lot. it annoys me. 07:20:28 quintopia: it needs to render 07:20:33 Ah, lynx supports gopher... 07:20:35 quintopia: Yes it is slow on my computer too. 07:20:45 I agree it's slow, but it's not TOO slow 07:20:58 I'd rather have nice looking output :) 07:21:04 Quadrescence: I think it is too slow. 07:21:10 i agree with zzo38 07:21:13 also the hanging thing 07:21:18 for rendering TeX in real time? 07:21:23 I think that's quite fast really. 07:21:36 how about we just not render it in real time, eh? 07:21:44 zzo38: AFAIK, no need to point MX record to host itself, A/AAAA records are enough for mail delivery... 07:21:58 quintopia: because that defeats the whole purpose of it 07:22:24 that's why browsers are getting better and better JS engines 07:22:25 etc 07:22:47 we just need to petition the w3c to add tex rendering stuff to the html standards. 07:22:48 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 let the browser do it fast instead of in js slowly 07:23:07 quintopia: i agree with that 07:23:07 but having it pre-rendered 07:23:10 "zzo38computer.cjb.net. 300 IN MX 0 zzo38computer.cjb.net.". 07:23:23 quintopia: but right now it's the best we have. and mathml blows 07:23:32 :( 07:23:52 Quadrescence: i didn't know. i'll test it real quick to see what you mean 07:24:01 Ilari: Yes, I did that so that CJB service will not process the mail. 07:24:25 Quadrescence: mathml doesn't blow that bad 07:25:13 yes it does 07:25:37 it is a piece of shit, designed by a web committee, not mathematicians or typographers 07:28:38 and... how does that cause it to be bad? 07:29:06 zzo38: CJB inserts their own MX record if you don't put one? 07:29:11 Well if you've ever examined either the output or the markup, you'd understand Mathnerd314 07:30:12 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 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:12 especially with monochrome laser printers 07:31:31 Ilari: Yes I think they do. 07:31:39 print? who prints? 07:31:41 treekiller 07:31:44 I print a ton 07:31:58 here's my current To Read stack http://i.imgur.com/U2uzT.jpg 07:32:14 all of which I printed 07:33:17 okay 07:33:22 :) 07:33:29 googling your nick i find that you do a lot of math reading and tex stuff 07:33:35 yes 07:33:38 i can see where that might be an issue for you 07:34:02 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 quintopia: tex4ht is a great application, I don't deny that 07:34:30 i just like the output I have I guess :S:S:S:S 07:34:31 i also didn't realize quadrescence was a made up word...what is it supposed to mean? 07:34:40 idk it's made up 07:34:55 yes but you get to make up a def too :P 07:35:09 quad represents four facets of my mind~ 07:35:47 i have one more facet than you. i win. 07:35:52 good night 07:35:56 time cube 07:36:13 EARTH HAS 4 CORNER 07:36:13 SIMULTANEOUS 4-DAY 07:36:13 TIME CUBE 07:36:13 IN ONLY 24 HOUR ROTATION. 07:36:13 4 CORNER DAYS, CUBES 4 QUAD EARTH- No 1 Day God. 07:36:15 jsMath doesn't even support a lot of commands of TeX. And the ones it does support, is all incomplete. 07:36:22 zzo38: what? 07:36:24 no... 07:36:38 zzo38: It supports the math typesetting, and that's rather complete 07:37:56 and looks exquisite if you have STIX fonts installed (free) 07:37:56 I typed \^^47amma and it says "Unknown control sequence '\^'" 07:38:09 And it can't make \def or \the\count255 or anything like that either 07:38:13 you can 07:38:21 just in the config files 07:38:24 on demand? no 07:38:38 I don't know why you'd type \^^47 anyway 07:38:42 O, \def works. 07:38:54 But \the is broken. 07:39:04 It's for typesetting math 07:39:08 that is it 07:39:21 if you want to typeset TeX documents, use TeX 07:39:39 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 \mathchar doesn't work. 07:51:05 zzo38: what is a practical use case of \mathchar 07:51:58 \kern only partially works. 07:52:36 Quadrescence: You can look at the TeXbook for some examples. 07:52:48 I know what it is. I am asking for a practical use case for a website. 07:53:03 that LaTeX doesn't solve. 07:54:37 zzo38: SORRY, I AM TAKING OFFENSE TO YOUR INANE PROBLEMS WITH JSMATH!!! 07:56:22 I think TeX works better. If you want to make a math report, you can use TeX. 07:56:59 Also, the \hbox command in jsMath is completely broken. 07:57:01 Yes, if you want to make a math report for publication, yes 07:57:20 if you want to write a blog, absolutely not 07:58:19 Actually I think TeX can be good for math blog. You should just need ssh. 07:58:51 gross 07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 08:03:39 The broken \hbox is probably the most serious mistake in jsMath, I think. 08:12:56 zzo38: i'd agree 08:22:43 But regardless of how well jsMath works or doesn't work, it is still slow!! 08:28:58 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:09:56 hey 10:10:06 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 http://xkcd.com/838/ This... is actually close to having potential. 15:30:33 Get rid of the girl in the middle panel and just make it him wondering and it would be decent. 15:32:18 20:51:24 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:19 pikhq: Whoa. 15:32:55 pikhq: heh Tom's Diner cameo at the end 15:33:24 21:10:37 pikhq: u should www.symbo1ics.com/blog 15:33:28 oh jesus christ that is the worst blog ever 15:33:39 wasn't it on reddit recently 15:33:50 -!- cheater99 has joined. 15:34:30 22:14:03 seriously, there ought to be no real barriers to me deciding to make some music *right now* 15:34:30 22:15:44 except talent. 15:34:30 22:15:47 * oerjan ducks 15:34:30 22:16:21 well, yeah, I'll agree that reading documentation is always a good idea 15:34:34 i have no response 15:35:58 22:41:19 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 22:41:51 quintopia: Doesn't it anyways? 15:36:04 audacity is possibly the worst software ... ever 15:36:50 23:03:41 (enable js) 15:36:57 desperately trying to figure out a justification for having a blog depend on js now. 15:42:37 -!- j-invariant has joined. 15:44:14 hey elliott 15:44:17 hi 15:44:34 look at the proof on line 746 http://coq.pastebin.com/rkDjqYFH 15:44:50 then see 877 where it gets mapped to a different category 15:46:32 ok 15:46:58 j-invariant: nice 15:47:08 really exciting 15:47:08 -!- cheater99 has quit (Read error: Connection reset by peer). 15:47:20 j-invariant: this is getting close to the point where i understand nothing though :) 15:47:25 this gives a general way to prove things automatically 15:47:41 -!- Mathnerd314 has joined. 15:48:16 02:10:06 me and my friend made this in my own game -> http://64pixels.org/christmas.png 15:48:18 asiek2erka: what. 15:50:53 I'm not sure if I should start keep developing this or try and simplify it and clean it up 15:51:17 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:51:32 logical consistency prohibits it 15:52:27 j-invariant: not if you did everything coinductively! maybe :P 15:52:43 j-invariant: I'd keep going, it's "clean enough" 16:03:45 j-invariant: I am not sure how to prove that 0+x = x in a ring at all, with my model 16:04:02 0+x = x isn't an axiom? 16:04:36 [[Error: Impossible to unify "mg_op b" with "mg_op b".]] wat 16:04:44 j-invariant: not that i can tell 16:04:53 -!- cheater99 has joined. 16:04:55 oh wait 16:04:57 sure it is 16:04:57 j-invariant: yes, it is 16:05:00 j-invariant: I mean 0*x = 0 16:05:02 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 "Error: Impossible to unify "mg_op b" with "mg_op b"." ;; lol ok so my system does work 16:05:13 coq just prints it confusingly 16:05:17 oh i already said that 16:05:19 and yeah OK 16:05:25 elliott: i think i wrote a proof of 0*x = 0 on this channel once 16:07:34 0*x = (0+0)*x = 0*x+0*x --> cancel --> 0*x = 0 16:07:55 `addquote elliott: i think i wrote a proof of 0*x = 0 on this channel once 16:08:00 your crowning achievement as a mathematician 16:08:07 254) elliott: i think i wrote a proof of 0*x = 0 on this channel once 16:08:10 Mathnerd314: that needs you to prove that a = a+a means a =0 16:08:14 *a = 0 16:08:40 x=a+x -> x-x=a+x-x -> 0=a 16:09:05 Theorem foo S (R : ring S) : 16:09:05 forall a, (pr_mul (p:=R) a (mn_1 (m:=pr_ag R))) = (mn_1 (m:=pr_ag R)). 16:09:08 hard enough just to formulate it! 16:09:52 thus... why Coq / etc. are not good for proving theorems 16:12:51 Mathnerd314: thus why unjustified generalisation 16:12:52 stfu 16:12:55 S : Set 16:12:55 R : ring S 16:12:55 a : R 16:13:02 lol i just realised i structured this in a way that I can't prove a:S 16:13:10 OH WELL time to soldier on 16:14:30 is 0+a = a left identity or right? 16:14:33 similarly a+0 = a 16:15:18 Theorem bar S (R : ring S) : 16:15:19 forall a, (pr_add (p:=R) a mn_1) = a. 16:15:19 intros. 16:15:19 unfold pr_add. 16:15:19 apply mn_right_ident. 16:15:19 Qed. 16:15:21 it's a start 16:17:01 -!- cheater99 has quit (Read error: Connection reset by peer). 16:25:01 left 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). 16:59:51 elliott: rewrite rules are superior 17:00:07 Mathnerd314: for... theorem proving? 17:00:12 Mathnerd314: you have no fucking clue what you're talking about 17:00:24 really? why? 17:00:42 Mathnerd314: I am eagerly awaiting your proof of the four-colour theorem in a term rewriting language 17:00:47 until then, no. 17:01:51 -!- poiuy_qwert has joined. 17:17:20 elliott: does writing Coq in a term rewriting language count? 17:17:47 Mathnerd314: Anyone can Greenspun. The answer is no. 17:18:10 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 (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 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:06 Mathnerd314: hahahaha 17:26:11 Mathnerd314: i take it you have no idea how coq actually works 17:27:00 maybe; my conception is probably inaccurate in the details 17:27:09 j-invariant: any progress btw? 17:27:16 Mathnerd314: more than the details, I'd say ... 17:27:30 I'm tired :( 17:28:13 j-invariant: category theory solves all problems! including tiredness! 17:31:38 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:19 that would be cool 17:32:52 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 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 maybe I should just press on and define limits 17:37:49 that's what i'd do 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 elliott: here we are... Coq tactics *are* rewrite rules 17:42:24 Mathnerd314: wrong, they're programs 17:42:35 in fact IIRC they can even not halt (j-invariant?) 17:42:57 rewrite rules are programs, and can be non-terminating 17:43:42 Mathnerd314: Coq tactics *are* brainfuck programs 17:43:49 brainfuck programs are programs, and can be non-terminating 17:44:00 Mathnerd314: Coq tactics *are* rule 110 initial states 17:44:00 etc. 17:44:33 elliott: no, they're rewrite rules. they take propositions and turn them into other propositions. 17:44:43 err. not really. 17:44:47 brainfuck programs aren't that general 17:45:01 um, what? 17:45:10 send proposition on stdin, get new proposition on stdout. 17:45:56 -!- poiuy_qwert has quit (Client Quit). 17:47:40 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 firstly, those two aren't definitions. 17:48:59 secondly, I like rewrite rules perfectly well. 17:49:06 thirdly, as they aren't definitions, they prove nothing. 17:49:34 s/definitions/assumptions/ then 17:49:58 well, they also aren't interpretations. 17:50:03 so i have no idea whatsoever what you are trying to convey 17:50:54 in Coq you have a situation like x:T, y:B, z:B->T->W |- _ : W 17:51:42 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 elliott: we have different assumptions, leading to differing opinions/interpretations. so I am wondering where we start to disagree. 17:52:41 if you take contexts and programming problems you can view tactics as rewrite rules 17:52:45 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 it's useless to do so because we're not interested in the tactic language 17:54:00 it's just some tacky script language that helps you program faster, like typeclasses in haskell or macros in lisp 17:54:01 j-invariant: that makes sense. 17:55:47 -!- elliott_ has joined. 17:55:48 the way you use it is more like (an advanced version of) prolog 17:56:01 because it has pproof search and unification and such 17:56:10 a _very_ advanced version of prolog :P 17:57:39 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 what's the scoop with rewrite systems anyway 18:02:43 aren't they just another universal computer? 18:03:26 yeah, but they're a "nice" universal computer, nicer IMO than lambdas 18:03:56 why? 18:05:06 fizzie: Deewiant: The server is back up, BTW. Don't think ineiros pinged you two yesterday. 18:05:09 (Without hMod though.) 18:05:34 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 when you write down a rewrite system: You don't know if it's confluent or not do you? 18:06:00 j-invariant: as in, implement other things /nicely/ in terms of them 18:06:17 I think confluence is overrated 18:06:20 is there any use of a non-confluent rewrite system? 18:06:32 yes, for computing 18:06:54 non-deterministic computing? 18:06:57 no? 18:07:02 how is it nondeterministic? 18:07:29 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 j-invariant: because, generally you have a rule for this -- e.g. "most specific match", so it'd be the second 18:07:50 built into the language 18:09:06 but imposing that restriction makes the system confluent 18:09:56 j-invariant: then yes, you do know whether it's confluent or not: it is! 18:12:11 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 well, fast; i should say efficient 18:15:13 j-invariant: also rewriting languages are pretty "extensible" 18:15:23 i.e., you can easily add new cases to a function from "anywhere", codewis 18:15:24 e 18:15:34 j-invariant: which means you don't need typeclasses 18:15:42 say you have a few constructors for your new numeric type 18:15:44 then all you have to do is 18:15:51 add (C1 ...) (C1 ...) = ... 18:15:52 add (C1 ...) (C2 ...) = ... 18:15:53 etc. 18:16:04 and if infix + is bound to add, then it all magically works 18:17:18 thats useful 18:20:03 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 but i haven't seen that done yet 18:20:42 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 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 Mathnerd314: I just mean, you are able to write down non-confluent systems -- so how do we make use of that? 18:22:25 elliott_: that's the programming language I'm trying to write 18:22:42 Mathnerd314: message passing and multiple dispatch are not pattern matching. sorry. 18:23:14 elliott_: the messages passed are rewrite rules 18:23:21 what's the difference? :D 18:23:40 j-invariant: also term rewriting lets you do fun things like this 18:23:42 > foldl (+) 0 [a,b,c,d,e,f,g]; 18:23:42 0+a+b+c+d+e+f+g 18:23:45 :p 18:24:16 whats new ?? 18:25:43 j-invariant: well, it's just a silly example. 18:25:48 but it's still pretty neat. 18:25:54 (foldl is defined the normal way) 18:26:31 what if I made a rule 18:26:39 random = 1 ; random = 2 ; random = 3 18:26:42 then random + random ? 18:26:51 > random=1;random=2;random=3; 18:26:51 > random; 18:26:51 warning: rule never reduced: random = 2; 18:26:51 warning: rule never reduced: random = 3; 18:26:51 1 18:27:02 j-invariant: basically I'd say "random = 1; random = 2; random = 3" is an invalid program 18:27:08 since you have ambiguous rules 18:27:21 it must be very hard to recognize valid/invalid programs 18:27:35 j-invariant: not really 18:27:37 well may be 18:27:39 *maybe 18:27:44 is there an algorithm? 18:27:49 probably, but i don't know it 18:27:56 i mean it depends on your rule for specificity 18:28:00 j-invariant: it's easy not to write invalid programs though IME 18:28:04 I would never write anything like that random thing 18:28:08 j-invariant: i mean, you know in haskell 18:28:21 how many times do you write a haskell program with two "f (X ...) ... = ..." that are ambiguous? 18:28:24 I never do 18:30:14 -!- impomatic has left (?). 18:38:22 j-invariant: in my language, that would make random a type. (particularly, the type containing only 1, 2, and 3) 18:40:31 err, does that make any sense? types are more like predicates 18:41:33 my type predicates are all "reachable by running rewrite rules" 18:41:45 e.g., 18:41:45 nat 0 = true 18:41:45 nat (S n) = nat n 18:41:45 nat _ = false 18:42:25 so "nat = 0; nat = S n" would specify the type nat 18:42:36 then e.g. 18:42:37 :: if nat n then nat (fact n) else true 18:42:37 fact 0 = S 0 18:42:37 fact (S n) = S n * fact n 18:42:41 Mathnerd314: really? 18:42:47 Mathnerd314: so "S S" is a nat? 18:42:50 surely you mean "nat = S nat" 18:43:04 oh, yeah. good point. 18:43:37 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:43:40 :: n:nat -> (fact n):nat 18:43:40 fact 0 = S 0 18:43:40 fact (S n) = S n * fact n 18:43:42 would be correct 18:45:06 * Mathnerd314 just has fact nat = nat 18:45:43 that doesn't make any sense 18:45:47 fac nat = {1,2,6,24,...} 18:45:49 N! is not N 18:45:58 N being naturals 18:46:03 j-invariant: that i could understand. 18:46:35 !1+i.11 18:46:35 1 2 6 24 120 720 5040 40320 362880 3.6288e6 3.99168e7 18:46:38 j-invariant: J has that :P 18:47:25 elliott_: curses, you're right. fact nat : nat 18:47:37 i see. what does "a : b" mean? 18:47:44 presumably it reduces down to a rewrite rule of some kind. 18:49:48 it's an upper bound; it says "the set of results of rewriting 'fact nat' will produce a subset of the natural numbers" 18:50:15 = is a lower bound 18:52:29 Mathnerd314: i don't suppose you have an algorithm for typechecking this 18:53:09 not a general algorithm; with that I could solve everything. but for specific cases I do 18:54:41 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 now I'm imagining Coq going "You might have proved this! I can't tell!" 18:56:41 elliott_: you can check bounds on types easily 18:57:07 Mathnerd314: if you can't check types in general, it's not a type system 18:57:26 -!- oerjan has joined. 18:57:42 ok, it's not a type system. it's a proof system. 18:57:50 -!- Gracenotes has quit (Quit: ...). 18:58:03 Mathnerd314: a proof system that can't tell you whether your proof is valid or not? 18:58:03 useful! 18:58:36 sorry, it's the thing you prove proofs about. I don't know what you call that. 18:59:08 there are two things to consider 18:59:11 * What can you compute? 18:59:14 * What can you define? 19:00:04 a turing machine computes and defines recursive sets. ZFC computes nothing but defines a huge chunk of mathematics 19:00:13 much more than just recursive sets 19:01:45 sorry, it's the thing you prove proofs about. I don't know what you call that. 19:01:47 what? 19:01:55 j-invariant: zfc scares me 19:02:28 j-invariant: 19:02:31 oops 19:02:32 mistype 19:03:31 hmm 19:03:36 I think I am going to write a parser generator 19:03:46 no! 19:03:53 write a generator parser instead 19:04:21 also, merry christmas 19:04:51 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:06:40 oerjan: it's the 24th you bum 19:07:24 elliott_: christmas starts officially 17:00 today in norway 19:07:34 oerjan: really? that's just weird. 19:07:37 you guys are stupid and smelly. 19:07:39 -!- elliott_ has changed nick to elliott. 19:07:43 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 that's when they ring all the church bells 19:07:52 Mathnerd314: you can't prove anything if you don't have a type checker 19:08:28 wtf? 2+2=4; there's no stinking type checker 19:08:56 Mathnerd314: what/ 19:08:58 *what? 19:09:11 it's a proof system, yes? presumably one based on some kind of type theory. 19:09:15 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 therefore you need a type checker to check your proofs. 19:09:22 by your own admission you don't have a general typechecker 19:09:27 oerjan: yeah yeah, silly nord 19:10:08 * Mathnerd314 reads wikipedia more 19:10:20 elliott: it's an "abstract machine" 19:11:02 are you just reading wikipedia, picking random vaguely-related words from there, and applying them? 19:11:12 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 I have no idea how you expect to be able to write and verify proofs. 19:11:42 yes, precisely. 19:11:57 ... 19:12:03 do you know yourself? 19:12:06 no. 19:12:12 Mathnerd314: then why are you wasting my time? 19:12:29 elliott: he imght just be too tired at this point 19:12:41 j-invariant: are you sure you're not generalising from a sample of 1? :D 19:12:48 from all the arguing LOL 19:13:01 yeah I might be 19:13:58 elliott: do you want an accurate answer? 19:14:07 Mathnerd314: sure? 19:14:38 * Mathnerd314 starts preparing his 100-page thesis 19:15:23 Mathnerd314: on why you're wasting my time? 19:15:39 yes. probably won't be 100 pages though. 19:17:58 -!- j-invariant has quit (Quit: leaving). 19:27:53 elliott: http://pastebin.com/SvDE6sZr 19:28:37 "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:28:47 also i demand 100 pages 19:31:34 * Mathnerd314 writes his college essays 19:41:28 elliott: Vorpal, fizzie, elliott and others who might care: [...] 19:42:00 But right, Deewiant was left out. 19:43:11 Poor Deewiant. 19:47:50 'Tis rather lonely on there right now. 19:49:48 fizzie: Incidentally, I found your secret chest. It's empty. 19:51:07 No, it's not. 19:51:24 Or do you mean the thing under my floorboards in the house? 19:51:39 fizzie: I mean the thing with the secret entrance to the left of your fire. 19:51:47 Oh, right. 19:51:54 That's not very secret. 19:52:01 fizzie: To be fair, I am very dense. 19:52:10 elliott the black hole 19:52:19 I don't think I'll bother taking out all your floorboards, though. :p 19:52:25 There's also another chest under the floor in front of that chest, but that's currently empty also. 19:52:35 I moved stuff elsewhere. 19:52:55 Okay, back to socializing. -¥ 19:53:00 What. 19:53:04 -> 19:59:39 GOD FUCKING DAMMIT 19:59:42 NOTCH YOU BASTARD 19:59:54 HOW COME DESTROYING MY CART WHILE I'M IN IT 19:59:56 SUFFOCATES ME 20:00:01 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:18:50 elliott go play my game 20:18:53 http://64pixels.org 20:18:53 :FD 20:18:54 :D* 20:19:18 I don't run Java programs that aren't Minecraft. 20:19:33 :[ 20:21:19 Port it to Haskell. :p 20:21:30 you do it 20:22:02 -!- SimonRC has joined. 20:22:09 Gimme the source then. 20:22:31 elliott i have not obfuscated the code 20:22:34 you can easily decompile it 20:22:34 :) 20:22:38 decompiled code != source 20:22:55 it is almost equal nowadays 20:22:59 both of them are ugly in my case 20:23:46 i haven't found a decent open-source java compiler 20:24:38 *decompiler 20:24:39 not compiler 20:25:39 elliott - http://64pixels.org/christmas.png 20:25:42 this is something in my game 20:25:44 reconsider playing it 20:25:45 :D 20:25:54 asiek2erka: i saw in the looks. i also said "what.". 20:26:20 but 20:26:23 there's multiplayer! 20:26:23 *logs 20:26:24 not looks 20:26:25 fff i can't spell 20:26:47 maybe if you explain wtf http://64pixels.org/christmas.png is 20:27:04 A very ASCII Christmas 20:27:13 6 screenshots glued together 20:27:16 of this giant scene 20:28:08 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:33 uhhhhhhhhhhh 20:28:36 christmas 20:28:54 Christmas = the joys of rampant consumerism; your point? 20:29:08 that is not what it is supposed to be 20:29:49 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 i don't remember the last time i saw christmas associated with christianity in... any way at all really 20:30:02 asiek2erka: um, you do realize elliott is this channel's resident semi-militant atheist? 20:30:12 oerjan: i'm not a semi-militant atheist, and it's not about that 20:30:21 I just don't see how modern christmas is related to christianity in any way 20:30:25 -!- cheater99 has joined. 20:31:01 elliott: hey i added the semi- just to avoid your protests :D 20:31:14 I wouldn't have been confused if the bible quote even /mentioned/ jesus at all :p 20:31:46 elliott: it's what the angels said when Christ was born AFAIK 20:31:50 said or sang 20:31:57 asiek2erka: I don't think that actually happened :-P 20:32:03 oerjan: well, /r/atheism irritates me as much as anyone :P ... so at least I'm not a typical reddit atheist! 20:32:06 elliott: well christians believe it did 20:32:18 asiek2erka: I'm nitpicking at this point :P 20:32:28 also you can never be 100% sure 20:32:36 s/at this point/always/ 20:32:57 * oerjan geeses 20:33:00 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 I trust it will bring me salvation. 20:33:17 (side note: that would be a way better fake religion than FSM) 20:33:17 -!- cheater99 has joined. 20:33:33 elliott: it's your belief, go ahead 20:33:37 but i agree with the side note 20:33:37 -!- wareya has quit (Read error: Connection reset by peer). 20:33:38 TOTALLY 20:33:54 Tomorrow I will celebrate The Day of the Revelation of the Teapot. 20:34:09 how much believers does your religion have 20:34:14 we are proud to have over a billion 20:34:21 -!- wareya has joined. 20:34:25 You measure the accuracy of beliefs by how many people believe them? 20:34:29 no 20:34:32 -!- cheater99 has quit (Read error: Connection reset by peer). 20:34:39 just that so many people believe us. why 20:34:42 But, uh, me and Bertrand Russell, which is pretty damn good company if you ask me. 20:34:59 asiek2erka: Um, because Christians went crusading to convert all the evil nonbelievers quite a while back and it worked surprisingly well ...? 20:35:12 elliott: Well, I can't disagree with this argument 20:35:13 As opposed to all the Buddhist missionaries going around. 20:35:30 (Solipsist missionaries are the best though.) 20:35:42 ("I'm just saying ... I don't really exist. Only you do. Think about it.") 20:36:14 well 20:36:22 Christians took Pagan holidays for their own use to stop paganism 20:36:45 Surprisingly effective. 20:36:48 yes! 20:36:55 Do you consider that a good thing? 20:37:01 well 20:37:08 i do not accept the fact we christians used force 20:37:19 (lol spanish inquisition) 20:37:22 but we've changed since then 20:37:31 we don't do spanish inquisitions anymore, do we 20:37:49 asiek2erka: Do you really think all of Christianity is united with a single opinion? 20:38:05 not all 20:38:10 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:40 but 20:38:41 haven't we 20:38:48 What? 20:38:53 also why are you arguing with a 13-year-old 20:38:58 that's the most nonsensical thing ever 20:39:05 What. 20:39:37 indeed. asiek2erka, go to your room! 20:39:48 Is asiek2erka /asking/ me to discount his opinions based on his age? 20:40:09 wait, isn't asiek2erka polish? 20:40:09 elliott: a sure sign of immaturity if i ever saw one! 20:40:26 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 very reliable if you ask me 20:40:59 i recall recently seeing some headline about polish church attendance taking a nosedive 20:41:21 elliott no 20:41:33 i am telling you why the hell are you arguing with someone that should be less intelligent than you 20:41:35 it's like trolls 20:41:40 they take you down to their level 20:41:46 then beat you with their stupid argumentatino 20:42:10 so if you're older than someone you're smarter than them? 20:42:31 asiek2erka: um this is #esoteric. here age is not the strongest indicator of intelligence by far. 20:42:34 usually 20:42:35 oerjan: sure, but it's more the early years that matter I would expect fwiw 20:42:40 to make someone christian 20:42:41 you had more experience in life 20:42:47 if it is anywhere 20:42:48 asiek2erka: lol 20:42:56 elliott look 20:43:00 what about we just go like this 20:43:02 you believe what you want 20:43:04 i believe what i want 20:43:08 and let's live in peaced 20:43:09 peace* 20:43:12 it's been minutes since i questioned anything you said. 20:43:18 well apart from the age-intelligence correlation. which is just stupid. 20:44:16 let's go back to what we started 20:44:17 christmas 20:44:41 "The word Christmas originated as a compound meaning "Christ's Mass"." 20:45:35 http://retire-well-life.com/wp-content/uploads/2009/12/santa-claus.jpg Pictured: Jesus. 20:45:54 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:01 One of your arguments is right 20:46:07 We do not know when Jesus was really born 20:46:12 it was only a suggestion and everyone said "ok" 20:46:39 there are better estimates 20:46:44 IIRC it's something like July 20:46:58 well, if the historical jesus actually exists, which is arguable, but anyway 20:46:58 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 right ... because everything not in the new testament is false? 20:47:16 no 20:47:25 for christians the new testament is 100% true 20:47:26 while 20:47:29 the rest may not be 100% true 20:47:33 for christians the new testament is 100% true 20:47:37 yes, er, hate to break it to you, but that's not even remotely so. 20:47:37 and no 20:47:43 do not get on apocryphas 20:47:58 I don't know of a single person who follows even the new testament 100% to the letter. 20:48:09 hello 20:48:14 Vorpal: hello 20:48:19 it is true but nobody reads it because nobody cares! 20:48:23 elliott: Vorpal, fizzie, elliott and others who might care: [...] <-- he is included in others 20:48:32 most Christians, at least in Poland, declare they are christians 20:48:33 Yes, but it didn't ping him, so. :p 20:48:34 but do not do anything 20:48:39 also, happy xmas everyone 20:48:41 they just declare and... maybe pray every evening 20:48:47 and do not give a **** about anything else 20:48:54 I'm a Muslim! I demonstrate my Musliminity by doing nothing. 20:48:59 (In Sweden we celebrate the 24th.) 20:49:12 Vorpal: Yes, yet more evidence that you're uncivilised backwater vikings. 20:49:35 elliott, rather, the reverse 20:49:48 Cool; I'm a viking. 20:50:30 elliott, the other reverse 20:50:34 (everyone else is backwards) 20:50:46 elliott, but yes you probably are a viking as well 20:50:57 a backwards one maybe 20:51:09 Someone get on Minecraft, it is terribly quiet today. 20:51:12 Vorpal: you mean he's a gnikiv!? [/lamejoke] 20:51:18 asiek2erka, XD 20:51:25 -!- cheater99 has joined. 20:51:28 elliott, nah, I'm going to dig into this ioctl 20:51:39 And mine it for ore? 20:51:45 elliott, ... what? 20:51:50 XD 20:52:08 elliott, been porting the pc-speaker tune playing code from freebsd to linux. As an user space app in this case. 20:52:12 almost done 20:52:19 are you going to craft a pc speaker from an ioctl and the user space 20:52:32 elliott, I have a problem however. beep(1) is GPL. Not GPL2. GPL. 20:52:41 Vorpal: So? 20:52:49 elliott, and there are some magic constants I need from there 20:53:00 Vorpal: Those aren't copyrightable. 20:53:02 elliott, because I haven't been able to find docs on the IOCTL 20:53:06 ioctl* 20:53:21 Small magic numbers aren't copyrightable; even if they are, another program's copy of them isn't. 20:53:28 elliott, it is rather large. Over 9000 20:53:34 (over 90000 even!) 20:53:50 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 elliott, it is something like jiffies per timer interrupt of original IBM XT timer 20:54:15 don't have the computer with the code on turned on atm 20:54:17 (just got home) 20:54:17 -!- cheater99 has quit (Read error: Connection reset by peer). 20:54:46 What Painterly glass texture do you use? :p 20:54:58 elliott, the same as I told you about before 20:55:03 I forget. >_> 20:55:43 (don't you hate it when someone says "same place as usual" when you ask where something is? I certainly do) 20:56:17 TO MOUNT HOOVER! 20:56:24 elliott, it has a thin white border, it has some glints in opposite corners 20:56:31 Ah. The one I currently have then. 20:56:34 I don't like the fact that it has two glints. 20:57:25 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 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:57:59 elliott, huh 20:58:18 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:27 NOPE I DIED LOL 20:58:34 elliott, stop doing it then 20:58:55 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 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:18 I KEEP FORGETTING 20:59:48 elliott, can you forget that you dislike me? 21:00:40 Ha -- my inventory duplicated. 21:00:43 But I can't pick up any of it. 21:00:48 elliott, heh 21:00:55 Also there's a minecart on fire. 21:01:00 -!- Sgeo has joined. 21:01:00 c 21:01:01 ... 21:01:01 Except it's a booster on the *other* track. 21:01:21 elliott, dw mentioned something about something similar up north some days ago 21:01:21 No wait! 21:01:23 before beta 21:01:26 *My* cart overlapped the booster. 21:01:29 As in, exactly on top of each other. 21:01:34 My cart has somehow gone onto the other track, and caught fire. 21:01:53 Also, it is seemingly invincible. I can move though it and it won't move, and I can't destroy it. 21:01:56 NOTCH QUALITY ENGINEERING 21:02:23 elliott, the option in the painterly customiser is: "I want windows with reflections in the corners." 21:02:49 Right. 21:03:30 Things can catch fire in MC? 21:03:43 ...yes. 21:03:44 elliott, I can just dump the cookie it remembers things with I guess 21:03:55 Project: FUCK THE WORLD 21:04:01 -!- poiuy_qwert has joined. 21:04:14 elliott, http://sprunge.us/fYdb 21:04:26 If you do that, I want to see screenshots 21:04:45 Sgeo, they don't burn for long mostly 21:04:52 and a lot of stuff don't burn at all 21:05:11 elliott, I never seen minecarts burning at all. And since they are iron they shouldn't 21:05:28 asiek2erka: http://art.penny-arcade.com/photos/1135238941_tVKGy-L.jpg 21:05:29 * elliott trolling 21:05:42 Vorpal: Well, things could also pass through it. And it was invincible. 21:06:58 elliott, probably a bug then 21:07:03 elliott, does it actually boost? 21:07:08 Vorpal: As I said, it wasn't a booster. 21:07:12 elliott, oh 21:07:14 Vorpal: It was just perfectly overlapped with the booster, which still moves. 21:07:14 elliott, missed that 21:07:21 I have no idea how it teleported to where the booster is. 21:07:22 elliott, I bet it is a client bug then 21:07:29 Vorpal: This was after disconnecting and reconnecting. 21:07:38 elliott, what if you reconnect again? 21:07:42 I think I did... 21:07:46 hm 21:07:47 Anyway, everything caught fire when I fell under the track. 21:07:54 So presumably it teleported from there ... to where the booster was ... on the other track. 21:07:55 SOMEHOW 21:08:02 And became pass-through (like see-through except, you know). 21:08:04 And invincible. 21:08:05 elliott, is there any lava under the track? 21:08:21 Yes. At least I recall burning, and I think there's obsidian there. 21:08:51 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 and then be able to walk up given facilities for that 21:09:01 How much can lava spread? Can it be pumped? 21:09:20 Sgeo, which sort of lava? 21:09:22 Vorpal: Or just wait for health to disappear again :P 21:09:27 Vorpal, whichever 21:09:35 Sgeo, well, define spread. 21:09:47 Flow across the world 21:09:53 Consuming everything 21:10:01 Sgeo, 4 tiles on flat ground iirc 21:10:09 "I mean, even a racist clock is right twice a day." 21:10:10 Sgeo, it can flow over an edge and get another 4 21:10:19 elliott, what 21:10:27 elliott, in fact, what is a racist clock 21:10:35 Vorpal: --Gabe, Penny Arcade 21:10:59 -!- cheater99 has joined. 21:11:24 Are porkchops good for two uses, or is that just SMP bugs duplicating it? 21:11:45 elliott, as far as I know they 1) don't stack 2) go away in one use 21:11:45 Bugs, it seems. 21:11:55 Vorpal: It goes away, then it reappears. Picking something up replaces it in its slot. 21:12:03 But I think if you right click while the dupe is there it works. 21:12:03 elliott, so infinite pork? 21:12:07 Vorpal: No. 21:12:09 It disappears the second time. 21:12:13 Because of logic. 21:12:19 elliott, .... does it heal the second time? 21:12:24 I think so. 21:12:30 But I dunno; my health bar is full. 21:12:30 this makes no sense 21:12:35 It wasn't very reliable on the survival server. 21:12:41 So I don't really know. 21:12:48 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:09 STUCK ON A FENCE 21:13:16 The Hoover farm is terribly positioned. 21:13:21 You have to jump almost over it to get to the mines the way I do. 21:13:22 elliott, ... how? 21:13:29 Vorpal: Jumpin' onto it 21:13:32 elliott, uh. why not walk around it a bit 21:13:37 I was above it. 21:13:40 Then I jumped, and miscalculated. 21:13:44 Slam, fence. Boing boing boing. 21:13:45 elliott, you don't want to jump onto the farmland anyway 21:13:48 *Boingy boingy boingy. 21:14:26 elliott, uh did you take the long stairs. Don't they go just past? 21:14:34 Go past what? 21:15:08 elliott, go past the point of the end of the farm, such that the farm is alongside the straight stairs 21:16:11 Nope. 21:16:14 They emerge a little bit from the farm. 21:16:17 elliott, thing I don't like with painterly: every pack icon has a creeper 21:16:21 But yes, I could go straight but I'd have to turn after that. 21:16:27 Vorpal: Is there something wrong with that? :P 21:16:42 Ahhh, home sweet Hoover Heavy Industries Research Facility. 21:16:49 well, you don't see it often, but mmm... I don't like creepers 21:18:11 elliott, does mcmap work yet? 21:18:17 Vorpal: Yes. More or less. 21:18:21 It crashes "sometimes". 21:18:32 I wonder if phanty would object to me expanding the HHI research facility; it is rather small. 21:19:35 HHI? 21:19:51 Sgeo: Hoover Heavy Industries. 21:19:58 Our services include many services. All our services are secret. 21:20:07 If you wish to make use of our services, contact us with money. 21:22:43 "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:41 Sgeo: BEST DEVICE EVER 21:23:58 elliott is now a Microsoft fan. 21:24:02 wut 21:24:05 Sgeo: wat 21:24:09 http://www.landoverbaptist.org/2010/december/luciferstoychest2010.html 21:24:17 Oh man, I thought it was a real thing :( 21:24:25 oh landoverbaptist 21:25:22 "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 elliott: here's for you http://www.reddit.com/r/circlejerk/comments/eqw92/i_wish_atheist_redditors_a_very_merry_xmas/ 21:26:16 oerjan: ah, /r/circlejerk ... the more moderate version of the rest of reddit 21:26:35 * oerjan is browsing r/all 21:27:24 i guess this is a sign of advanced addiction 21:27:31 Vorpal: sec 21:27:35 Vorpal: http://www.minecraftforum.net/viewtopic.php?f=25&t=55700&start=300 21:27:45 -!- SgeoN1 has joined. 21:27:45 Vorpal: leave the map one off but turn on better grass and light is what i'd recommend :P 21:27:47 erm 21:27:50 elliott, hm 21:27:53 http://www.minecraftforum.net/viewtopic.php?f=25&t=55700 21:28:08 Vorpal: bettergrass requires betterlight, so 21:28:11 at least for now 21:28:14 Dear computer: What the fucking fucking fuck? 21:28:21 elliott, EINSUFFICIENTCOMPUTER 21:28:27 Vorpal: um i used it 21:28:30 Vorpal: it's fine 21:28:35 Vorpal: barely slows down at all 21:28:44 Vorpal: the slowdown was from me also using far and fancy which my computer can't even remotely handle /anyway/ 21:28:49 elliott, besides I like the worse light. Useful when building something to match up an overhang 21:28:53 Windows, or something claiming to be such, I guess, told me it was low on memory 21:29:01 elliott, you can see exactly where you need to go based on the shadow :P 21:29:09 Now the screen is blank 21:29:52 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 (it generally never told me first, and I blame nvidia when things went shit) 21:30:24 Ibwasnt running much 21:31:00 SgeoN1, yeah, and OOM should not cause that 21:31:02 -!- Sgeo has quit (Ping timeout: 240 seconds). 21:31:04 it never has for me 21:31:23 §simoleon! 21:31:51 Encyclopædia 21:32:16 -!- cheater99 has quit (Read error: Connection reset by peer). 21:32:44 elliott, nah, I don't want better light, it seems to make things look dark based on screenshots 21:33:28 elliott, all I want is to make 2/3rd side grass work with painterly and biome grass 21:33:44 Vorpal: it doesn't, i've used it 21:33:52 it's easy to uninstall, just rm -rf bin 21:33:57 just give it a try :p 21:34:35 -!- SimonRC has quit (Ping timeout: 265 seconds). 21:36:17 -!- SimonRC has joined. 21:39:10 Yeah, I think you either have to choose no side-grass, inconsistent side-grass or just single-color all-grass. 21:41:12 fizzie, there isn't no-side grass iirc, Even the default pack has some side grass 21:41:23 fizzie, does it work with the small setting on side grass? 21:41:39 No. 21:41:49 -!- Sgeo has joined. 21:41:49 fizzie, but it does for the default texture pack! 21:42:11 Yeah, but the thing that loads from texture packs can't biomize sidecrass, I think. Or something like that, anyway. 21:42:11 Damn farkers can be idiots. I think about half of them aren't sure if Landover Baptist is parody 21:42:18 fizzie: Or you can have biome-compliant 1/1 grass. 21:42:20 http://www.fark.com/cgi/comments.pl?IDLink=5847704 21:42:22 fizzie, is there any mode for that? 21:42:25 With Better Grass. :p 21:42:37 elliott, I don't want /complete/ side grass 21:42:45 elliott, I want the 2/3rd option in painterly 21:42:45 Vorpal: Um, that's what Better Grass does. 21:42:50 elliott, yes and I don't want that 21:43:00 Well, tough, you can't have it. 21:43:33 elliott, quite, but probably there is some other mod 21:44:10 It'll probably get officially fixed too at some point. Ot 21:44:10 Vorpal: There isn't. 21:44:19 It's there in the top-ten of getsatisfaction common-problems. 21:44:32 fizzie, true 21:45:03 asiek2erka: Your game won't even start. 21:46:05 So how goes SMP. 21:46:13 elliott yes it will 21:46:18 asiek2erka: No it won't, I just tried. 21:46:22 what are you using 21:46:23 Unless there's a special key to start. 21:46:29 Sun's JVM? OpenJDK? 21:46:33 JamVM? HotSpot? 21:46:37 IcedTea? 21:46:56 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:46:57 also browser or download 21:47:00 Browser. 21:47:05 elliott try download 21:47:09 No. 21:47:14 i haven't tested it in openjdk yet 21:47:21 i dont even know where the **** you can get openjdk for windows 21:47:44 "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 The code is basically identical. 21:48:00 So it's your code's fault; fix it. 21:48:12 i can't if i can't see what's wrong 21:48:13 >:( 21:48:19 does OpenJDK implement javax.imageio 21:48:28 and javax.swing 21:48:28 OpenJDK implements everything. 21:48:33 I see the menu, I just can't select any of the options. 21:48:37 click on the window 21:48:38 Using arrow keys, WASD, space, enter. 21:48:38 duhh 21:48:41 I did. Duhh. 21:48:43 what 21:48:48 arrows should work perfectly 21:48:54 click on the select menu a few times 21:48:55 -!- cheater99 has joined. 21:49:02 It does implement the ImageIO stuff, though there were some OpenJDK imageio bugs I had to work-around in one project. 21:49:13 Something related to filters, I forget what exactly. 21:49:28 asiek2erka, what is this game (note I only have openjdk and/or icedtea as well) 21:49:34 Vorpal it should work 21:49:36 http://64pixels.org 21:49:42 it's an ASCII infinite open world game 21:49:48 with logic circuits 21:49:51 and multiplayer 21:49:59 asiek2erka, wait, why do I get dejavu 21:50:08 asiek2erka: Add WASD keys. 21:50:19 Vorpal: BUT ZOMG, JEB VISITED!1129012012 21:50:22 MOJANG FAMOUS 21:50:25 heh 21:50:30 elliott i did 21:50:36 Well, they don't do anything. 21:50:40 C:\Documents and Settings\[username]\.64pixels\config.txt 21:50:41 asiek2erka, also ascii? 21:50:44 add a line "wsad-mode=1" 21:50:49 asiek2erka, I see graphics 21:50:50 asiek2erka: No. Make them work by default. 21:50:53 elliott no 21:50:55 Vorpal: It's DOS codepage. 21:50:59 Vorpal: So what idiots think "ASCII" is. 21:51:01 i do not like WSAD 21:51:10 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 asiek2erka, do arrow keys work then 21:51:24 Vorpal yes 21:52:03 elliott, if it is a dos code page, it seems unlikely to work under linux? 21:52:10 elliott 21:52:14 the charset is a raw dump of the CGA ROM 21:52:17 and it's stored that way 21:52:24 therefore IBM should hate me by now 21:52:28 as the CGA ROM is most likely copyrighted 21:52:30 http://64pixels.org/scr5.png "64pixels 0.0.3.1, a random creation" <-- the hell 21:52:38 elliott, doesn't that look familiar to you 21:52:41 * Sgeo falls in love with the Landover Baptist Bible Quizes 21:52:49 Vorpal: One might consider it is intentional. 21:52:57 elliott, sure, but the title! 21:52:57 That's not the player thing, anyway. 21:53:03 elliott, true. 21:53:12 Does this thing have any monsters? 21:53:17 no 21:53:21 It is intensely boring. 21:53:27 make a logic circuit 21:53:33 I can do that without being a smiley face. 21:53:39 http://www.youtube.com/watch?v=0M90Hq4u3nQ 21:53:42 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 asiek2erka, are you a developer on this? (are there any other ones?) 21:53:50 asiek2erka, and, how many people play it? 21:53:53 You know, having right-clicking instantly erase anything is perhaps not such a good idea for vandalism prevention. 21:53:57 Vorpal: JEB PLAYED IT ONCE BEST GAME EVER 21:54:04 Vorpal: yes, GreaseMonkey helps me a bit 21:54:07 also it's been on indiegames.com 21:54:10 heh 21:54:11 about 15-20 people played it so far 21:54:14 right 21:54:18 or maybe more 21:54:19 "The idiot of the channel helps me occasionally!" 21:54:41 i'm putting that into the game's protocol 21:54:42 forever 21:54:45 Wait, is the space just randomly filled? 21:54:51 elliott yes 21:54:53 naturally 21:54:57 ...so you've built like two things. 21:55:20 there are more 21:55:26 but our server admin destroyed the forum database 21:55:33 ...and that destroyed the world 21:55:36 http://64pixels.org/mods.html In what universe does this count as modding? 21:55:42 elliott, if you call GM the "idiot of the channel"... what do you call asiek2erka? 21:55:44 OMG I CONFIGURED FIREFOX TODAY -- TOTALLY MODDED 21:55:48 asiek2erka, and why the nick change 21:55:49 Vorpal: 13. 21:55:54 also stop demotivating me 21:55:56 elliott, ah 21:55:59 (it's ok, he said I could discriminate based on age!) 21:56:23 elliott, are you 14 or 15 now? I forgot 21:56:31 well i'm 14 in 2 weeks 21:56:32 Vorpal: 15. :p 21:56:36 elliott, ah. 21:56:48 elliott, still 13 emotionally sometimes. 21:56:57 Yeah, and you're so mature. 21:57:06 elliott, did I claim that? I don't think I did. 21:57:10 i think Vorpal is much nicer than you 21:57:18 I guess I'm flattered 21:57:22 I'm an asshole? Wow, I never realised. 21:57:26 yes, yes you are 21:57:31 no comments on that 21:57:33 but you were the one who said it 21:57:35 :P 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:08 Yep. 21:59:22 I took the topmost flowers and nothing happened. 21:59:29 elliott oh no 21:59:31 rebuild the heap now 21:59:36 also wait, you got the game to work? :P 21:59:43 -!- asiek2erka has changed nick to asie[afk]. 21:59:45 Umm. No, I don't think I'm going to bother to figure out how to switch blocks./ 21:59:56 "DON'T LEAVE CLOCKS RUNNING THEY WASTE BANDWIDTH" -- how on earth. 22:00:03 Does it make a network connection for every tick or something? 22:00:19 elliott, local game or multiplayer? 22:00:23 Multiplayer. 22:00:29 ah 22:00:37 elliott, now to work on the pc speaker player coder 22:00:38 code* 22:00:48 One wonders if it is not asie[afk] and GreaseMonkey merely not knowing what "bandwidth" means. 22:01:39 elliott, perhaps. 22:07:53 -!- cheater99 has joined. 22:09:02 /* 22:09:02 * Emit tone of frequency thz for given number of centisecs 22:09:02 */ 22:09:02 static void tone(unsigned int thz, unsigned int centisecs) 22:09:09 elliott, thz sounds so strange 22:09:19 make me think of THz 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 what, the program runs okay under gdb but malfunctions when ran alone 22:26:55 -!- cheater99 has joined. 22:27:18 gdb quality. 22:27:47 elliott, XD 22:27:53 elliott, valgrind reports nothing 22:27:57 Vorpal: That has happened to me before, but I figured out the problem and corrected it. 22:27:59 That's not really very "what". 22:28:03 and it still malfunctions under valgrind 22:28:15 gdb does affect uninitialized memory contents and such. 22:28:29 fizzie, but 1) valgrind reports nothing 2) it still malfunctions there 22:28:32 Though valgrind often catches that sort of stuff, admittedly. 22:28:33 i probably shouldn't wander around minecraft with nothing to do. 22:28:45 fizzie, my guess atm is that ptrace changes something about how the system call works 22:28:48 fizzie, maybe EINTR 22:28:49 or such 22:28:57 why are there little blue pixels in my painterly trees 22:29:02 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 Did you know I have played D&D game today? 22:40:14 oh I found it 22:40:27 Mrf, what's the keys to rearrange tabs in xchat again? 22:40:30 fizzie, the bug was actually that I typoed argv[1] as argv[0] 22:40:33 I accidentally moved #esoteric to the left of freenode. 22:40:33 -!- hagb4rd has joined. 22:40:39 Vorpal: Just mv the program before executing it. 22:40:44 fizzie, that plus a number of coincidences 22:40:50 elliott, quite esoteric yeah 22:41:05 yay it seems to work 22:41:39 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 elliott, sounds better on my thinkpad, where it is just a pure tone through the usual speakers 22:42:36 Vorpal: Let's build a hi-fi USB PC speaker. 22:42:41 elliott, XD 22:42:45 So you can listen to it in all its glory on a laptop. 22:42:49 A *real* one too -- as in the actual same mechanics. 22:42:56 elliott, well my desktop has that 22:43:05 Vorpal: But is it hi-fi? 22:43:10 Vorpal: Are all the components isolated? 22:43:11 elliott, I doubt it 22:43:15 elliott, however this needs root to run. 22:43:23 which makes me nervous while debugging 22:43:23 LAME 22:43:28 elliott, blame linux 22:43:32 elliott, I need to open /dev/console 22:43:37 elliott, and do some ioctls on it 22:43:47 elliott, this needs either running from a vt 22:43:50 or as root under X 22:44:02 elliott, so it won't need root if you run it from a vt 22:44:19 Heh; how weird. 22:44:45 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 Vorpal: Why on earth does that thing write to a choices file? 22:44:54 elliott, and X runs as root 22:44:59 Couldn't it just assign to a variable? 22:45:04 elliott, I have no idea 22:45:30 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 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 and well, there is no buffer 22:46:52 -!- Wamanuz3 has joined. 22:46:54 I wonder if I could transfer the IΞ type system to a term rewriting system. 22:47:45 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 (those functions: beep(freq, duration_in_ms), sleep(duration_in_ms) 22:48:11 ) 22:48:26 -!- cheater99 has quit (Read error: Connection reset by peer). 22:49:07 Vorpal: Um, did you really call it sleep()? 22:49:09 In a C program? 22:49:16 POSIX hates you. 22:49:19 elliott, no 22:49:25 elliott, I call it hw_beep and hw_sleep 22:49:31 Ah. 22:49:32 elliott, and I don't call it "duration_in_ms" either 22:49:43 Vorpal: Couldn't you just usleep(x*whatever_factor_i_forget) 22:49:59 elliott, usleep: no such thing in POSIX-2008. Besides it isn't portable C. 22:50:04 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 elliott, I use nanosleep 22:50:14 elliott, since that is what replaced usleep 22:50:16 merry xmas folks ;) 22:50:20 hagb4rd: wat./ 22:50:29 i'm always online 22:50:30 elliott, usleep was made obsolete in POSIX 2001 and removed in 2008 22:50:32 hagb4rd, same! 22:50:35 i live on the internet 22:50:42 Vorpal: no you're destroying all the synapses 22:50:48 FUN FACT i have no physical form 22:50:52 np.. it's good to have you here 22:50:53 Vorpal: no you're destroying all the synapses 22:50:53 what 22:51:06 elliott, maybe you misread: merry xmas folks ;) hagb4rd, same! 22:51:12 I actually can't leave, watch: 22:51:12 -!- elliott has left (?). 22:51:12 -!- elliott has joined. 22:51:14 DAMN 22:51:20 you cycled 22:51:35 elliott, I can't leave however (channel is sticky in bouncer, it will filter /part) 22:51:35 It is my punishment, to stay in here for eternity. Well, specifically, to stay in here for eternity with Vorpal. 22:52:18 So is anybody going to MC today? :p 22:52:22 * hagb4rd giggles 22:52:27 elliott, I was on for a bit, but pc speaker is funnier! 22:52:55 I played D&D game today. Do you think I won? 22:53:10 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 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:53:47 Vorpal: just GPL v1 it? 22:54:00 after all, GPL v1 is BSD-compatible 22:54:03 elliott, yeah but I have no clue what GPL v1 actually is. 22:54:05 so if you stole BSD cdoe that's ok 22:54:11 Vorpal: http://www.gnu.org/licenses/gpl-1.0.html 22:54:13 GNU GENERAL PUBLIC LICENSE 22:54:14 Version 1, February 1989 22:54:18 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 elliott, I clearly stated that this file was same as freebsd one with minimal changes 22:54:23 Vorpal: erm gpl v2 is from june 1991 22:54:28 hm 22:54:31 so it probably means gpl 2. 22:54:39 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 zzo38: for a program predating GPL v2, even? 22:54:58 Or if the license is included with the program, you would use that one. 22:54:58 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 Vorpal: Just say "This program is licensed under the same license as the beep tool from [wherever]." 22:55:09 (I do not believe in NIH) 22:55:18 I believe in NIH! 22:55:41 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 elliott, oh. Noodly Interspace Horror? 22:55:51 yes. 22:55:58 elliott, isn't that a codename for flying spaghetti monster? 22:56:08 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 zzo38: So code licensed under "GPL" then is definitely version 1. 22:56:28 ah wait 22:56:32 elliott: Then, OK. 22:56:32 it has a COPYING 22:56:35 which is GPL2 22:56:43 Vorpal: OK then it is whatever version the COPYING file says. 22:56:44 right 22:56:50 Vorpal: I don't consider reverse engineering to be virally, though. 22:57:02 Vorpal: Copying non-trivial code, yes. 22:57:09 Figuring out how it works and reimplementing it... naw. 22:57:19 elliott, 1193180 btw 22:57:25 Vorpal: 349783498 22:57:31 elliott, won't work. 22:57:38 elliott, it is not the right magic constant 22:57:43 3459358 22:57:48 again won't work 22:58:05 elliott, anything but the one I gave and frequency will be off 22:58:07 Vorpal: Plz make shipping go faster. 22:58:13 elliott, of the tool? 22:58:16 -!- zzo38 has quit (Remote host closed the connection). 22:58:17 No. 22:58:24 -!- Wamanuz4 has joined. 22:58:25 -!- Wamanuz3 has quit (Ping timeout: 255 seconds). 22:58:26 elliott, what do you mean then 22:58:32 OF MAH LAPTOP 22:58:48 elliott, ah, I don't have any inside connections at apple 22:58:49 can't help 22:59:09 I know Steve Jobs' zombie brother. 22:59:16 But he disowned him, so GUESS THAT WON'T HELP. 22:59:18 hm 22:59:28 if system is loaded it won't play correctly 22:59:32 Also, it's been dispatched, so it's probably not Apple's problem any more :P 22:59:34 Vorpal: What? 22:59:35 Oh. 22:59:38 Loaded in that sense. 22:59:40 elliott, no buffer 22:59:43 so... 22:59:47 elliott, maybe I should try to give it real time priority? 22:59:56 I wonder what function is used for that 23:00:09 Vorpal: Just renice yourself. 23:00:09 I think. 23:00:33 elliott, right, I was thinking real time IO priority as well 23:00:37 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 If only it worked with non-root :P 23:01:01 elliott, right, but since almost everyone use X you will end up needing root /anyway/ 23:01:12 besides it won't /fail/ without real time priority. 23:01:53 * elliott decides wood-bricks aren't nice, recustomises painterly 23:02:11 Vorpal: Have you seen that insane Painterly Christmas thing? 23:02:15 Stone becomes ice. :p 23:02:20 Sound effect dissonance! 23:02:28 elliott, yes.... 23:02:35 elliott, remember that fizzie took screenshots? 23:02:37 you were on iirc 23:02:38 I might try it. You know, just for Christmas. 23:02:41 Vorpal: Yes, I believe I didn't look. 23:02:44 ah 23:04:04 I wish the Painterly chests/benches/furnaces/doors were less ornate. 23:04:06 It's weird. 23:04:48 They're a bit overdone. 23:04:55 -!- cheater99 has joined. 23:05:21 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 elliott, hm now how to change IO priority 23:12:18 Dunno. 23:12:59 ah found it 23:13:01 love google 23:13:22 great, my man ioprio_set doesn't mention what headers 23:13:43 should report that as a bug 23:13:48 to where 23:14:50 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:05 fizzie, ... huh 23:15:25 fizzie, are you /sure/? 23:15:41 Sure about hanging or sure about that being a good idea? 23:15:57 Heh, brilliant. 23:16:02 Glibc does not provide wrapper for these system calls; call them using syscall(2). 23:16:07 that is why there is no header... 23:16:09 :D 23:16:33 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 also I doubt it will help anyway 23:17:09 Vorpal: why do you need any macros? 23:17:10 it seems block device IO specific 23:17:11 just use syscall() 23:17:17 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:17 I doubt it 23:17:20 since fizzie is infallible 23:17:31 elliott, because int ioprio_set(int which, int who, int ioprio); and for the last argument you use macros to construct it 23:17:33 says the man pae 23:17:35 page* 23:17:52 elliott, it doesn't document the raw values for it 23:17:57 Vorpal: cpp(1) 23:18:00 just that it is a bitmask and you use these macros... 23:18:03 elliott, ... 23:18:08 elliott, anyway it won't help me 23:18:26 ./include/linux/ioprio.h: IOPRIO_WHO_PROCESS = 1, 23:18:26 ./include/linux/ioprio.h: IOPRIO_WHO_PGRP, 23:18:26 ./include/linux/ioprio.h: IOPRIO_WHO_USER, 23:18:38 (Grepping *.[ch] inside the kernel.) 23:18:47 elliott 23:18:55 a clock emits 120 bytes a second per player 23:18:59 that's what we mean by bandwidth 23:19:19 120p B/s, oh noes!! 23:19:20 fizzie, yes those I have no problem with 23:19:25 -!- asie[afk] has quit. 23:19:26 Max 255 players, no? 23:19:28 fizzie, I meant IOPRIO_PRIO_VALUE 23:19:37 fizzie, IOPRIO_PRIO_CLASS and IOPRIO_PRIO_DATA too 23:19:37 So maximum 32 KiB/s. 23:19:39 HOW HORRIBLE 23:19:53 Vorpal: ./include/linux/ioprio.h:#define IOPRIO_PRIO_VALUE(class, data) (((class) << IOPRIO_CLASS_SHIFT) | data) 23:19:55 The same place? 23:20:17 fizzie, right 23:20:30 fizzie, anyway it won't really help me, since it seems to be block device specific 23:20:33 Notably they're not in my /usr/include/linux, just in the kernel source tree's include/linux subdir. 23:20:38 and all I do is ioctls on a char device 23:20:53 fizzie, great... 23:21:10 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 Just hang the system for the duration of the song. :p 23:21:51 fizzie, actually I don't dare use SCHED_FIFO, SCHED_RR looks more interesting 23:22:21 I don't think it's any easier on the system. 23:22:27 elliott, well actually I won't, since I sleep, not busy wait 23:22:32 It still will pre-empt everything with a lower static priority. 23:22:35 "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:40 fizzie, hrrm 23:22:49 Vorpal: I lie my head on my pillow and busy-wait for eight hours. 23:23:11 elliott, good night then (assuming that is how it should be read) 23:23:21 elliott, also, you are going to bed early? 23:23:25 -!- cheater99 has joined. 23:24:13 Vorpal: elliott, well actually I won't, since I sleep, not busy wait 23:24:26 "I lie" as in every night. 23:24:28 Who needs sleep. 23:24:58 -!- cheater99 has quit (Read error: Connection reset by peer). 23:25:03 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 fizzie, Finland uses the proper 24th too right? 23:27:42 Yes. Well, for the gift-giving part and so on; the 25th is still Christmas too. 23:27:49 elliott, to guarantee proper execution in the face of swap trashing I should probably memlock myself too ;P 23:28:24 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 fizzie, it is just ioctls 23:30:04 fizzie, anyway, it seems to work well with just a -20 nice and normal scheduler 23:30:39 fizzie, and your suggestion would involve rather heavy rewriting, which I don't want 23:30:55 "The ucs2 and utf8 character sets do not support supplementary characters that lie outside the BMP." ~~MySQL 23:31:07 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 fizzie, including making the playstring thingy reentrant 23:31:54 fizzie, actually it will be less like the original (freebsd speaker kernel driver) 23:31:58 which also sleeps 23:32:05 and works the same way 23:32:26 elliott, uh... what? ucs2: yeah okay, that makes sense. 23:32:27 I guess it depends on whether you want to match that or to conform to some sort of an ideal. 23:32:29 but utf8? 23:32:42 fizzie, well I want to match 23:32:42 Vorpal: MYSQL QUALITY 23:33:37 also TOS theme on pc speaker is awesome "l2b.f+.p16a.c+.p l4mne8a2mspg+e8c+f+8b2" 23:34:22 The mlock/mlockall thing could be a thing to do, of course. 23:34:58 Anyone know how to insert UTF-8 chars with a mysql query? 23:35:06 i.e. what escape sequences or functions or whatever 23:35:34 ah, seems like it's CHAR() 23:36:07 I don't think I've got my PC speaker connected. I wonder how accurate the emulations are. 23:36:46 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:38 ah found docs 23:41:48 elliott, no need for GPLv2 any more 23:41:56 will probably do *BSD then 23:42:03 Vorpal: WTFPL 23:42:14 elliott, not BSD compatible iirc 23:42:29 Vorpal: Yes it is? 23:43:02 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 DO WHAT THE FUCK YOU WANT TO PUBLIC LICENSE 23:43:22 TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION 23:43:22 0. You just DO WHAT THE FUCK YOU WANT TO. 23:43:25 It's hard to not be compatible with that. 23:43:27 elliott, it is based on BSD yeah 23:43:29 (Also FSF-certified Free!) 23:43:44 elliott, and the mix is absurd 23:43:47 Vorpal: Right, then you can't remove the draconian BSD restrictions (such as requiring attribution). 23:43:54 elliott, since the bulk of the code is the BSD code 23:43:56 Vorpal: Hey, plenty of projects include BSD-licensed code but aren't BSD themselves, and the like. :p 23:44:02 Admittedly generally not in the same file. 23:44:12 elliott, the code that is not is basically main() + some linux specific functions 23:44:27 I still feel kinda dirty planning to copyleft things. 23:44:38 elliott, actually I split it in multiple files because I thought it would be larger than it turned out to be 23:46:52 Do a pulseaudio output option if you've run out of code to write. :p 23:47:16 fizzie, ... what? Can it drive the pc speaker? 23:47:22 fizzie: --lag-more 23:47:25 fizzie: or --high-latency 23:47:41 also, pc speaker or nothing 23:47:49 No, I just mean an emulation. 23:48:14 fizzie, for non-x86? 23:48:27 Right, and for us "no speaker connected" folks. :p 23:48:28 fizzie, also, shouldn't I use jackd then instead 23:48:36 fizzie, well sucks to be you :P 23:48:47 fizzie, /If/ I write anything it will be jackd 23:49:14 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 It's not like the audio needs to be synchronized with anything. 23:49:47 libao obviously 23:49:55 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 fizzie, actually I should procedurally generate a soundfont, load it into the sound card, and then play midi 23:50:03 fizzie, actually I should procedurally generate a soundfont, load it into the sound card, and then play midi 23:50:04 MT-32. 23:50:10 Make a PC speaker soundfont for an MT-32. 23:50:14 It would be GLORIOUS. 23:50:18 elliott, I would, except I don't have one to test with 23:50:23 elliott, I only have a sb live 23:50:47 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 Vorpal: You can have mine (note: no, it cost me £200). 23:51:07 Or was it £60. 23:51:08 One of the wto. 23:51:13 *two. 23:51:23 fizzie: Awesome. 23:51:27 Not the least bit creepy how easy it is to find my dad and step-mom's names 23:51:29 fizzie: How far could you recurse it, I wonder. 23:51:29 Not at all 23:51:35 Sgeo: Indeed, Seth Gold. 23:51:39 Easy-to-find names are a sign of creepiness. 23:51:43 elliott, you have one!? 23:51:45 elliott, awesome 23:51:59 Vorpal: Yes. Also a theremin.; 23:52:01 s/;$// 23:52:11 elliott, is it a professional one 23:52:14 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 The theremin? Yes, it's a Moog. 23:52:23 elliott, or one of those with a knob for one of the things 23:52:25 elliott, wow 23:52:30 Not their high-end model (that's *lots of money*), but yes. 23:52:34 Got it off eBay. 23:52:43 It's BLACK WOOD... which isn't really stylish, but there you go. 23:52:43 elliott, practising much? 23:52:51 Vorpal: No, the theremin is nearly impossible to play. 23:53:03 elliott, I seen people play it well 23:53:03 I'm willing to sell it :P 23:53:08 elliott, it just require practise 23:53:12 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 Vorpal: It needs a surgeon's hands. 23:53:24 And that's not really something you can practice at. 23:53:49 elliott, well I have a Roland FP-4 piano. Decent (but not state of the art) 23:54:03 and I prefer to play that 23:54:08 Where'd you get the MT-32? 23:54:25 Deewiant: eBay too. 23:54:34 elliott, what sort of connector do you use for it? 23:54:35 Deewiant: You can't buy them new, and they don't really degrade, so. :p 23:54:40 Vorpal: Audio. Analogue audio. 23:54:45 Vorpal: Oh, theremin? 23:54:48 Audio. Analogue audio. 23:54:49 But MT-32 too. 23:54:52 elliott, no the MT-32 23:54:55 Right. 23:54:57 It has a MIDI input and an audio out. 23:55:03 elliott, ah 23:55:03 The fat jack-style things. 23:55:15 Deewiant: Some things in life money can't buy -- for everything else there is eBay. (Paraphrased from that MasterCard ad.) 23:55:21 elliott, is that the same as the normal circular one? 23:55:29 elliott, or is it some other one 23:55:37 elliott, for midi I mean 23:55:41 Vorpal: http://en.wikipedia.org/wiki/TRS_connector 23:55:43 Oh, the MIDI one. 23:55:46 Dunno, I'll check in a minute. 23:55:48 elliott, yes 23:55:49 I have cables for it, FWIW. 23:55:51 brb 23:55:54 elliott, and how did you get that to work with a mac 23:56:05 Vorpal: Via adapter, I think. 23:56:10 elliott, ah 23:56:11 brb 23:56:23 I have a gameport<->midi cable 23:56:28 that I can use with this sound card 23:56:33 I would certainly guess the usual DIN-5 if it's "jack-style". 23:56:53 fizzie, I think he thought I asked about the audio 23:57:02 anyway, midi over usb sucks 23:57:18 no opto-isolation 23:57:48 and also, as far as I know, less real time guarantees 23:58:37 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 (What will they think of next!) 23:59:34 fizzie, to save on connectors? 23:59:38 or what 23:59:55 Yeah, you only need one hole in the laptop or whatever. 23:59:55 -!- cheater99 has joined.