←2012-07-13 2012-07-14 2012-07-15→ ↑2012 ↑all
00:16:34 <ais523> hi EgoBot
00:16:34 <lambdabot> ais523: You have 1 new message. '/msg lambdabot @messages' to read it.
00:42:39 -!- ogrom has quit (Quit: Left).
00:50:43 <Sgeo> ais523, do you remember what day we proved that theorem?
00:58:02 <oerjan> THEOREMS? WHERE?
01:00:03 <Vorpal> which theorem?
01:04:58 <Sgeo> oerjan, Vorpal, the one about bounded Game of Life
01:05:52 <oerjan> OK
01:07:14 <Sgeo> That any GoL pattern with at least a 5x5 hole on a bounded GoL grid has at least one Garden of Eden predecessor
01:09:51 <oerjan> ...or is itself a GoE, presumably
01:10:02 <Vorpal> Sgeo, missed that one
01:10:22 <Vorpal> Sgeo, how did you prove it
01:10:32 <Vorpal> and that is kind of interesting
01:10:39 <oerjan> or wait was that in the arbitrary far ancestor sense...
01:10:55 <Sgeo> arbitrary far ancestor sense
01:11:18 <Vorpal> isn't there a wiki for GoL btw? Did you post this (and the proof) there?
01:11:30 <Sgeo> I don't think I posted it
01:11:35 <Vorpal> do that then
01:11:37 <Sgeo> It should be in the logs somewhere
01:11:41 * oerjan vaguely recalls it now
01:11:57 <Vorpal> recalls what=?
01:11:59 <Vorpal> s/=//
01:12:23 <oerjan> basically, because of the hole you know that its immediate descendant has at least two possible parents
01:12:43 <Vorpal> yes and?
01:12:53 <oerjan> hm wait no
01:12:59 <Vorpal> also how would you know that
01:12:59 <Sgeo> If the pattern results in a loop, then only one of those patterns is in the loop (I'm a bit shaky on that part)
01:13:28 <oerjan> right that was
01:13:36 <Sgeo> Gregor, what. https://www.google.com/search?rlz=1C1TSND_enUS401US401&sugexp=chrome,mod=10&sourceid=chrome&ie=UTF-8&q=%22Garden+of+Eden%22+site%3Acodu.org
01:14:01 <oerjan> Vorpal: if you have a 5x5 hole, you can modify the center cell without changing the child state
01:14:22 <Vorpal> oh right
01:14:41 <Sgeo> Why is codu a wikipedia mirror
01:14:55 <Vorpal> huh
01:16:20 <Sgeo> So how do I download all of Gregor's stuff
01:16:29 <Sgeo> Erm, the ... bluh
01:18:21 <Gregor> Sgeo: It has a 5-clicks-to-Jesus game.
01:18:35 <Sgeo> Ah
01:18:36 <Gregor> (Assuming it still works)
01:19:49 <Sgeo> I think I found it
01:21:59 <Sgeo> http://tunes.org/~nef//logs/esoteric/11.06.26
01:22:34 <oerjan> Sgeo: you do know about `pastelogs , right?
01:26:54 <Gregor> Sgeo: What the boink are you talking about...
01:27:33 <Sgeo> As in, I wanted to download all the logs to grep them
01:31:55 <kallisti> oh, right... so
01:32:22 <kallisti> I just got why fourier transforms work on finite non-periodic signals.
01:32:56 <kallisti> since any signal is periodic if the period is infinity. :P
01:33:39 <Sgeo> Argh I want to redo my proof
01:34:10 <kallisti> Sgeo: rsync?
01:34:48 <kallisti> try: rsync -a rsync://codu.org/logs/_esoteric esologs
01:36:56 -!- zzo38 has quit (Remote host closed the connection).
01:43:42 <Sgeo> I think I'm scared of randomness
01:43:57 <Sgeo> I just put in a seed for a Minecraft world
01:44:02 <Sgeo> Not because of shared exploration
01:44:12 <Sgeo> But just... so I could reproduce another copy of the world in theory
01:48:24 <Vorpal> Sgeo, shared exploration? You mean multiplayer
01:48:43 <Vorpal> anyway you can easily dump the seed with F3 after you generated the world
01:49:06 <Sgeo> Not what I said. I mean, ala the Reddit world
01:49:09 <Sgeo> Is what I meant
01:49:09 <Vorpal> (unless it is multiplayer, in which case you need to do a bit more)
01:49:16 <Vorpal> Sgeo, I have no idea what that is
01:49:23 <Sgeo> One seed that multiple people use and explore
01:50:00 <Vorpal> Sgeo, I find that seeds are not reliable for stuff generated after worldgen (which happens with some mods, like buildcraft, and who would play vanilla these days?)
01:57:28 <Sgeo> It's night and I don't have a solid house
01:57:34 <Sgeo> Partial walls :/
01:57:43 <Sgeo> Did make a torch at least from charcoal
01:59:30 <Sgeo> Grah it's boring waiting for hopefully nothing to happen
02:05:14 <Vorpal> Sgeo, which mods do you play with?
02:05:19 <Sgeo> None right now
02:05:24 <Vorpal> Sgeo, why?
02:05:36 <Vorpal> I mean vanilla gets boring after a month or so
02:05:49 <Sgeo> I haven't played that much vanilla really
02:06:02 <Vorpal> I wouldn't play without RP2, IC2, EE2, BC3, and a bunch of other mods
02:06:20 <Vorpal> logistics pipes is another really really good one
02:06:41 <Sgeo> As in, there was maybe one world that I tried to play survival
02:06:44 <Sgeo> Not for very long
02:06:52 <Vorpal> oh?
02:07:09 <Sgeo> Played on servers a bit
02:07:12 <Vorpal> survival is fine with me, but the combat in minecraft is so utterly boring
02:07:14 <Sgeo> And that's pretty much it
02:07:24 <Vorpal> yeah don't think I would play on a vanilla server again
02:20:34 <Sgeo> Hmm, I haven't been doing much about hunger
02:37:36 <Phantom__Hoover> If the mob spawning algorithms are still idiotic you probably want to start farming early on.
02:39:39 <Sgeo> Next goal: Make a secure path between mining site and house
02:40:00 <Phantom__Hoover> You didn't build the house on top of the mining site?
02:40:07 <Sgeo> No
02:40:22 <Phantom__Hoover> (Have I mentioned how mining should totally work, it's way better than the way Minecraft does it.)
02:40:34 <Sgeo> Can I die of hunger on Normal?
02:44:27 <Phantom__Hoover> No, but it takes you down to like half a heart.
02:44:32 <Phantom__Hoover> There is a wiki for this sort of thing.
02:45:04 <Sgeo> Wish I could both browse wiki and let time pass
02:45:07 <Sgeo> Waiting for day is boring
02:47:12 -!- Phantom__Hoover has quit (Remote host closed the connection).
03:10:31 -!- david_werecat has quit (Ping timeout: 265 seconds).
03:15:29 -!- myndzi has quit (Read error: Connection reset by peer).
03:15:40 -!- myndzi has joined.
03:58:39 -!- edwardk has joined.
04:39:19 -!- edwardk has quit (Read error: Connection reset by peer).
04:39:51 -!- edwardk has joined.
04:39:56 -!- edwardk has quit (Client Quit).
05:04:26 -!- zzo38 has joined.
05:07:58 -!- myndzi has quit (Ping timeout: 265 seconds).
05:20:41 -!- oerjan has quit (Quit: Good night).
05:27:02 -!- ogrom has joined.
05:53:00 -!- pikhq_ has joined.
05:53:24 -!- pikhq has quit (Ping timeout: 265 seconds).
06:07:45 -!- pikhq has joined.
06:07:54 -!- pikhq_ has quit (Ping timeout: 265 seconds).
06:31:08 -!- tao__ has joined.
06:31:15 <zzo38> I wrote a program to test VRC7 audio.
06:31:21 <zzo38> For NES/Famicom
06:35:42 -!- tao__ has left ("Konversation terminated!").
07:13:19 -!- myndzi has joined.
07:23:25 -!- nooga has joined.
07:40:02 -!- azaq23 has joined.
07:42:47 -!- ais523 has quit.
07:59:23 -!- zzo38 has quit (Remote host closed the connection).
08:02:58 -!- edwardk has joined.
08:05:41 -!- AnotherTest has joined.
08:07:07 -!- edwardk has quit (Ping timeout: 244 seconds).
08:10:24 -!- Vorpal has quit (Ping timeout: 276 seconds).
08:12:13 <kallisti> http://sprunge.us/fFBY?haskell in which kallisti creates yet another brainfuck compiler.
08:12:21 <kallisti> in Haskell. with the standard optimizations.
08:12:52 <pikhq> Mine's better.
08:13:10 <pikhq> :)
08:14:01 <kallisti> pikhq: IIRC you made an assembly-like intermediate language right?
08:14:11 <pikhq> No.
08:14:23 <pikhq> https://github.com/pikhq/haskell-bfc/blob/master/main.hs
08:15:00 <kallisti> what's the int for on Loop?
08:15:30 <kallisti> our parse functions are similar. yours is smaller though
08:16:10 -!- Taneb has joined.
08:16:26 <kallisti> but mine goes ahead and groups consecutive commands
08:16:34 <Taneb> Hello
08:16:47 <pikhq> Which cell it's testing on, relative to the current pointer. I fold pointer movements into the instructions as much as possible.
08:17:25 <kallisti> wait I thought the pointer could shift.
08:17:50 <kallisti> !bf +[>+]
08:17:51 <EgoBot> No output.
08:18:57 <shachaf> \o/ \o/ \o/ \o/ \o/ \o/ \o/ \o/ \o/
08:18:57 <myndzi> | | | | | | | | |
08:18:57 <myndzi> /< /'\ >\ /< >\ /| |\ /`\ /'\
08:19:05 <shachaf> thmyndzi
08:20:49 <pikhq> kallisti: Yup. That gets compiled to [Add 0 1, Loop 0 [Add 1 1, Move 1]]
08:22:01 <pikhq> kallisti: If the pointer movements at the end of a loop don't net to no movement, then the pending moves get emitted right there.
08:23:21 <kallisti> oh, so "Loop 0" just means the normal [ behavior
08:23:31 <pikhq> Yes.
08:24:12 <kallisti> I'll probably end up translating this AST into a more complex mini-language.
08:24:24 <kallisti> with things like destructive add, clear, copy, and multiply.
08:24:33 <kallisti> though I guess clear would be "set 0"
08:24:43 <pikhq> Yeah, that'll give you rather a bit more power.
08:25:29 <mroman> https://github.com/FMNSSun/HsBfC/blob/71384aad6744927f165dfffe10cb5a5aa1a965e3/hsbfc.hs <- mine ;)
08:25:52 <mroman> groups instructions but lacks support for even simple optmization like +- -> Nop
08:26:31 <kallisti> my parser could probably be simplified.
08:29:04 <mroman> http://codepad.org/H1NEsAor <- parsec
08:29:26 <kallisti> pikhq: we have a lot of similar code though.
08:29:50 <pikhq> Well, yeah. A decent chunk of it is just doing it in the most natural way in Haskell.
08:30:57 <pikhq> My code generator, admittedly, is Weird.
08:31:24 <kallisti> mine is stupid
08:31:39 <kallisti> "lololol add dynamic resize condition after each >"
08:31:54 <pikhq> BF -> State (Int, Syscalls) (IO ()) -- :)
08:40:41 -!- asiekierka has joined.
08:52:37 -!- quintopia has quit (Ping timeout: 244 seconds).
09:11:54 -!- Taneb has quit (Remote host closed the connection).
09:13:10 -!- pikhq_ has joined.
09:13:30 -!- pikhq has quit (Ping timeout: 265 seconds).
09:20:15 -!- kallisti has quit (Ping timeout: 246 seconds).
09:21:59 -!- kallisti has joined.
09:22:07 -!- kallisti has quit (Changing host).
09:22:07 -!- kallisti has joined.
09:27:52 -!- pikhq has joined.
09:27:52 -!- pikhq_ has quit (Ping timeout: 246 seconds).
09:51:19 -!- nooga has quit (Ping timeout: 255 seconds).
10:51:29 -!- asiekierka has quit (Quit: Wychodzi).
11:02:18 -!- quintopia has joined.
11:18:04 -!- pikhq_ has joined.
11:18:07 -!- pikhq has quit (Ping timeout: 240 seconds).
11:31:07 * itidus21 gets agitated while contemplating subpixels when he realizes they're not quite as simple as he anticipated
11:35:16 <itidus21> http://pastebin.com/Mz73HbVN
11:38:33 <itidus21> my biggest surprise when i mapped this out is that if i say, pixel is lit if any subpixels touched then the shape will vary between 3 and 4 pixels width
11:48:19 -!- Phantom_Hoover has joined.
11:50:04 -!- asiekierka has joined.
11:52:25 -!- yorick has quit (Read error: Connection reset by peer).
12:08:14 -!- pikhq_ has quit (Ping timeout: 246 seconds).
12:08:40 -!- pikhq has joined.
12:14:44 <itidus21> (to answer my little query) i guess the solution is to simply use subpixels to determine the top left corner to pass to a bitmap drawing op
12:26:55 -!- Taneb has joined.
12:28:51 -!- yorick has joined.
12:30:13 <Taneb> Hello
12:31:32 -!- Phantom_Hoover has quit (Remote host closed the connection).
12:33:27 -!- Phantom_Hoover has joined.
12:53:17 -!- derdon has joined.
13:34:54 -!- ogrom has changed nick to marx.
13:35:09 <nortti> hi marx
13:35:20 <marx> hi nortti
13:35:23 -!- marx has changed nick to ogrom.
13:50:55 -!- edwardk has joined.
13:53:17 -!- olsner has quit (Remote host closed the connection).
13:53:30 <nortti> ogrom: who are you and what takes you here?
13:54:06 <ogrom> sometimes i join here
13:54:12 <ogrom> i like the name of the room
13:55:01 <nortti> and then you just idle here?
13:56:11 -!- olsner has joined.
13:59:47 -!- david_werecat has joined.
14:11:11 -!- claque has joined.
14:11:17 * claque applauds.
14:11:40 <nortti> why?
14:11:58 <claque> I don't ask.
14:12:00 * claque cheers.
14:13:29 * claque laughs.
14:13:32 * claque gasps!
14:13:34 * claque cheers again!
14:13:38 -!- claque has quit (Client Quit).
14:15:22 -!- olsner has quit (Remote host closed the connection).
14:45:26 <Taneb> ...
14:45:29 <Taneb> How odd
14:58:50 <itidus21> <flubber>>+++++++++[<++++++++>-]<.>+++++++[<++++>-]<+.+++++++..+++.>>>++++++++[<++++>-]
14:58:51 <itidus21> <.>>>++++++++++[<+++++++++>-]<---.<<<<.+++.------.--------.>>+.</flubber>
14:59:32 <itidus21> Beer commercials usually show big men, manly men, doing manly things: "You've just killed a small animal. It's time for a light beer." Why not have a realistic beer commercial, with a realistic thing about beer, where someone goes, "It's five o'clock in the morning. You've just pissed on a dumpster. It's Miller time."
15:00:19 <Taneb> Because, itidus21, the people who make adverts actually know how to make adverts
15:00:39 <itidus21> The Second Amendment! It says you have the right to bear arms, or the right to arm bears, whatever the hell you want to do!
15:00:57 <Taneb> Can I have some bear arms?
15:01:23 <itidus21> There was an old, crazy dude who used to live a long time ago. His name was Lord Buckley. And he said, a long time ago, he said, "People--they're kinda like flowers, and it's been a privilege walking in your garden." My love goes with you.
15:01:46 <kmc> who is itidus21 quoting
15:02:36 <kmc> "Cambridge police: Man on Harley bites, robs man"
15:03:01 <Taneb> "Late Post 'Not That Late'"
15:06:10 <itidus21> Why do they call it rush hour when nothing moves?
15:06:43 <Taneb> It's actually a corruption of "rust hour2
15:07:22 -!- augur has quit (Ping timeout: 246 seconds).
15:10:25 -!- ogrom has quit (Quit: Left).
15:12:24 <itidus21> I feel like I'm a big human snot.
15:12:29 <nortti> ok
15:12:33 <nortti> why?
15:12:45 <itidus21> oh.. everything i just said was quotations from the same person :-s
15:13:00 <nortti> ok
15:13:44 <Taneb> Proof that no Comonad may be a MonadPlus:
15:14:19 <Taneb> Consider the function extract :: Comonad w => w a -> a; and the function mzero :: MonadPlus m => m a
15:14:38 <Taneb> And the type defined as data Void
15:14:47 <Taneb> Void has no constructors and cannot exist
15:15:32 <Taneb> If there is a type with both a comonad and monadPlus instance, extract mzero has the the type forall a. a, hence Void
15:16:09 <Taneb> As extract mzero is a Void and there are no Voids, there are no types which are both Comonads and MonadPluses
15:16:10 <Taneb> QED
15:16:29 <Taneb> (you can replace MonadPlus and mzero with Alternative and empty)
15:16:39 -!- augur_ has joined.
15:17:02 <Taneb> (this proof ignores the existence of _|_)
15:18:21 <Taneb> In short, Comonad m, MonadPlus m => Void
15:18:24 -!- augur__ has joined.
15:18:36 <kmc> itidus21 who
15:21:34 -!- calamari has joined.
15:21:43 -!- augur_ has quit (Ping timeout: 246 seconds).
16:11:12 -!- edwardk has quit (Quit: Computer has gone to sleep.).
16:13:35 -!- Taneb has quit (Quit: Leaving).
16:14:00 -!- calamari has left ("Leaving").
16:17:13 -!- DHeadshot has joined.
16:22:54 -!- copumpkin has changed nick to c0w.
16:27:24 -!- c0w has changed nick to copumpkin.
16:29:39 -!- edwardk has joined.
16:46:25 -!- augur__ has quit (Ping timeout: 246 seconds).
16:51:56 -!- zzo38 has joined.
16:56:47 -!- Vorpal has joined.
17:00:53 -!- Sgeo has quit (Read error: Connection reset by peer).
17:01:30 -!- Sgeo has joined.
17:12:30 -!- augur has joined.
17:22:18 <itidus21> robin williams :P
17:28:11 -!- edwardk has quit (Quit: Computer has gone to sleep.).
17:34:33 -!- olsner has joined.
17:47:13 <kmc> ah yeah
17:47:58 <kmc> i've only heard a little bit of his standup but i hear it's pretty good
17:48:29 <kmc> it's shockingly raunchy if you're only familiar with his roles in family movies ;P
17:53:14 -!- ogrom has joined.
17:59:15 -!- atehwa has joined.
18:14:50 -!- atehwa has quit (Remote host closed the connection).
18:19:09 -!- azaq23 has quit (Remote host closed the connection).
18:24:08 -!- ogrom has quit (Quit: Left).
18:29:05 -!- ogrom has joined.
18:32:49 -!- DHeadshot has quit (Ping timeout: 246 seconds).
18:41:27 -!- ogrom has changed nick to marx.
18:41:38 -!- marx has changed nick to ogrom.
18:41:45 <nortti> marx: is your first name karl?
18:42:34 <ogrom> hi nortti
18:42:38 <ogrom> ei ole
18:43:38 <nortti> jaa. nääkin oot suomalainen vai?
18:44:10 <olsner> yhdeksän
18:44:32 <nortti> se on numero. mitä siitä
18:44:55 -!- oerjan has joined.
18:45:21 <olsner> airo on meidän?
18:45:38 <nortti> mitä hittoa?
18:45:59 <olsner> ei siis hai
18:46:21 <nortti> jaa
18:46:31 <nortti> ogrom: you are estonian?
18:46:45 <oerjan> Eesti vabarik
18:47:23 <oerjan> *ii
18:48:26 <ogrom> nortti: virosta joo
18:49:02 -!- Taneb has joined.
18:49:04 <Taneb> Hello
18:49:05 <ogrom> m en kattonu vlill
18:49:11 <ogrom> hi Taneb
18:50:00 <olsner> google translate didn't like nääkin, but suggested näin instead
18:50:26 <oerjan> it doesn't like kattonu either
18:51:09 <olsner> I do not kattonu between
18:51:19 <nortti> nääkin=sinäkin
18:51:33 <nortti> kattonu=katsonut
18:51:56 <fizzie> Oh-so-dialectal.
18:52:31 <oerjan> <kallisti> http://sprunge.us/fFBY?haskell in which kallisti creates yet another brainfuck compiler.
18:52:46 <fizzie> Or colloquial or whatever.
18:53:05 <oerjan> kallisti: to simplify your data type, i suggest using a concept called "negative numbers"
18:53:20 <kallisti> oerjan: I can do that with Inc and Dec, however
18:53:30 <kallisti> ShiftR and ShiftL should have different code output
18:53:32 <oerjan> kallisti: um my point is you don't need both :P
18:53:34 <kallisti> which I could check for
18:53:37 <kallisti> but I'm lazy.
18:53:48 <kallisti> oerjan: yes and that is what I was saying as well
18:54:02 <kallisti> "I can do that" meaning "I can combine them into one constructor"
18:54:12 <nortti> hmm. underload compiler would be interesting project. it is even possible?
18:54:38 <oerjan> nortti: well if a _befunge_ compiler is possible...
18:54:44 <kallisti> anybody doing ICFP this year?
18:55:14 <Taneb> I only just heard about it :(
18:55:32 <oerjan> the need to keep both execution and string representations might complicate things...
18:56:36 <fizzie> oerjan: You just de-transform from the machine code back to whatever the string was likely to have been when necessary.
18:56:40 <fizzie> Sounds very practical.
18:56:55 <oerjan> fizzie: and also very optimization-breaking
18:57:51 <oerjan> i'm sure ais523 has considered it, and i think someone else may have too (elliott?)
18:58:02 <oerjan> neither of which is present
18:58:19 <nortti> hmm. writing an os with underload...
18:58:30 <oerjan> nortti: it still has no input.
18:59:04 <oerjan> nortti: you probably want ais523's underlambda instead, once he finishes it. (note: ais523 is not too good at finishing esolangs.)
18:59:13 <oerjan> (neither am i, come to think of it.)
18:59:29 <olsner> me neither
18:59:42 <Taneb> I'm... not very good either
18:59:51 <nortti> oerjan: but what about subroutine call to os that returns input?
19:00:20 <nortti> also what kind of language is underlambda?
19:00:21 <oerjan> nortti: ...it doesn't have that either, although i guess you can assume they're put on the stack
19:00:35 <ogrom> ollaan hirveit murremiehii
19:00:45 <nortti> joo. mut miks?
19:01:01 <ogrom> ihan kiusaks vaan
19:01:16 <oerjan> nortti: underlambda is a language supposedly a bit like underload, but more practical and with the stated intention of being easy to compile both to and from
19:01:30 <nortti> ok. that sounds good
19:01:49 <oerjan> i think it has a core part, which can bootstrap the rest
19:02:32 <nortti> is there a page for it?
19:02:53 <oerjan> but all this is very vague. the only other thing i remember is that it does _not_ confuse strings and program, in order to allow optimizations.
19:03:32 <oerjan> oh and it is constantly in flux whenever ais523 _does_ work on it. no page.
19:04:08 -!- AnotherTest has quit (Quit: Leaving.).
19:04:37 <oerjan> btw underload itself was a scaled down version of a monster called overload, which also has no page.
19:05:09 -!- asiekierka has quit (Remote host closed the connection).
19:05:12 <nortti> I know
19:05:31 <olsner> I didn't know
19:05:38 <nortti> does anyone know what it was like?
19:05:46 <oerjan> ais523 might vaguely recall :P
19:06:04 <oerjan> iirc it had the kitchen sink included
19:06:58 <nortti> so it was emacs of esolangs?
19:07:17 <oerjan> nortti: well maybe. funge98 already is that...
19:07:44 <oerjan> the problem with adding input to underload is that there is no similarly elegant way to output...
19:07:51 <oerjan> er
19:07:59 <oerjan> *to how output is done
19:08:06 <nortti> true
19:09:40 <oerjan> and as unlambda shows, if you _don't_ base it on some kind of numeric/binary representation you end up doing a lot of single character matches...
19:09:54 <oerjan> or you could go full regexps i guess
19:11:02 <nortti> how does underload handle input?
19:11:40 <Taneb> It doesn't, nortti
19:11:57 <nortti> *unlambda
19:13:21 <Taneb> @ reads a character, ?x pattern-matches
19:13:53 <nortti> ok
19:16:36 <nortti> maybe something like I reads a char, ? returns (~) if two topmost elements are same and () if not
19:17:32 <Taneb> I was thinking of an input extension for ZOMBIE
19:19:06 <nortti> or ? can be =
19:25:58 <oerjan> nortti: and that will _still_ be horribly inefficient for anything doing significant string lookup or parsing.
19:26:37 <oerjan> (because you have to match every possible character in sequence.)
19:28:11 <nortti> what about returning is in binary with (~) being 1 and () being 0 ?
19:28:14 -!- ogrom has quit (Quit: Left).
19:28:47 <oerjan> my unlambda-in-unlambda interpreter had to contain a full character table in order to parse ?x functions (there is no way to construct ?x from the character x read)
19:29:27 -!- edwardk has joined.
19:30:18 <oerjan> nortti: well yes. but now there is suddenly no visual correspondence between an input and something which handles it, unlike for output.
19:30:52 <nortti> fuck it. there is no input in uderload. I'll code my os in SSBPL
19:31:49 <oerjan> nortti: btw check out the rule 110 underload example for my encoding of bits as single : and ^ characters.
19:33:37 <oerjan> i thought that was fitting for a cellular automaton, and i only found two plausible ways of doing it (the other would use : and a)
19:34:42 <oerjan> (i never worked out the other one, but i see no reason why it shouldn't work)
19:41:26 <oerjan> <Taneb> (this proof ignores the existence of _|_)
19:41:43 <oerjan> i feel like doing that and still allowing Void is the part where you are cheating...
19:41:50 <Taneb> Yes
19:43:05 <oerjan> admittedly you just need one type which cannot have its value constructed from your mzero and m
19:43:16 <oerjan> *one of its values
19:43:44 <oerjan> well and w, i guess
19:44:42 <oerjan> oh and parametricity also gives you that
19:44:51 <Taneb> Parametricity?
19:45:17 <oerjan> you get easily a polymorphic function of type forall a. (Comonad w, MonadPlus m) => a
19:46:28 <oerjan> and parametricity implies that f must satisfy g . f = f for all f, which means you break if you have a type with a function that has no fixpoints
19:46:40 <oerjan> say, not :: Bool -> Bool
19:46:54 <oerjan> (f :: forall a. (Comonad w, MonadPlus m) => a)
19:48:15 <oerjan> (you need to ignore _|_ to have functions without fixpoints, of course)
19:48:54 <oerjan> @free f :: forall a. a
19:48:54 <lambdabot> g f = f
19:49:09 <oerjan> wat
19:49:33 <Taneb> @free f :: forall a. a -> a
19:49:33 <lambdabot> g . f = f . g
19:49:44 <oerjan> i wonder how lambdabot justifies not including . in the first one
19:50:06 <Taneb> Because f is not a category?
19:50:21 <oerjan> oh right
19:50:37 <oerjan> oh and the first f is const applied to the second one
19:50:50 <oerjan> er, reverse
19:51:36 <oerjan> g f = (g . const f') _ = (const f' . g) _ = f
19:52:21 <oerjan> obviously the first g f = f can only hold if g is strict
19:52:28 <oerjan> *required to be
19:54:36 <oerjan> @help free
19:54:37 <lambdabot> free <ident>. Generate theorems for free
19:54:46 <oerjan> @free undefined
19:54:48 <lambdabot> f undefined = undefined
19:56:11 <oerjan> possibly @free assumes system F types (the original system where parametricity was discovered, i think), which don't afaik include anything of type forall a. a
19:56:57 <oerjan> i guess the result is also true for ML
19:57:42 <mroman> @free bar
19:57:43 <lambdabot> Extra stuff at end of line in retrieved type "Not in scope: `bar'\n\n"
19:57:50 <mroman> @free const
19:57:52 <lambdabot> f . const x = const (f x) . g
19:58:07 <mroman> hu
19:58:30 <mroman> @free head . tail
19:58:30 <lambdabot> Extra stuff at end of line
19:58:33 <mroman> :(
19:58:39 <mroman> @free head
19:58:41 <lambdabot> f . head = head . $map f
19:59:03 <mroman> @free reverse
19:59:05 <lambdabot> $map f . reverse = reverse . $map f
19:59:32 <mroman> huh.
20:00:07 <mroman> > ($map (+3) . reverse) [1..9]
20:00:10 <lambdabot> Couldn't match expected type `([a] -> [a]) -> b'
20:00:10 <lambdabot> against inferred t...
20:00:20 <oerjan> mroman: $map is really map
20:00:21 <Taneb> I think what I was trying to get at is that extract mzero must be _|_, so either mzero is _|_, or extract can be _|_ for valid data
20:00:38 <Taneb> Neither is not stupid
20:01:00 -!- edwardk has quit (Quit: Computer has gone to sleep.).
20:01:38 <mroman> Why the $ then?
20:01:42 <mroman> It looks wrong with it.
20:01:47 <Taneb> If mzero is _|_ for one type, it must be _|_ for all types, which is useless
20:01:59 <oerjan> mroman: to distinguish it from an introduced variable, i guess
20:02:11 <oerjan> @free Just
20:02:11 <lambdabot> Pattern match failure in do expression at Plugin/Free/FreeTheorem.hs:54:20-34
20:02:14 <mroman> @free map
20:02:14 <oerjan> bah
20:02:16 <lambdabot> g . h = k . f => $map g . map h = map k . $map f
20:02:28 <mroman> @free map
20:02:30 <lambdabot> g . h = k . f => $map g . map h = map k . $map f
20:02:40 <mroman> @free Just 5
20:02:40 <lambdabot> Pattern match failure in do expression at Plugin/Free/FreeTheorem.hs:54:20-34
20:02:46 <mroman> @free Nothing
20:02:46 <lambdabot> Pattern match failure in do expression at Plugin/Free/FreeTheorem.hs:54:20-34
20:03:21 <oerjan> mroman: i think it's trying to say it doesn't know about Maybe
20:03:48 <oerjan> @free []
20:03:49 <lambdabot> Pattern match failure in do expression at Plugin/Free/FreeTheorem.hs:54:20-34
20:03:51 <oerjan> bah
20:04:17 <oerjan> @free f :: [a]
20:04:18 <lambdabot> $map g f = f
20:04:37 <oerjan> @free f :: Maybe a
20:04:37 <lambdabot> $map_Maybe g f = f
20:04:49 <oerjan> oh it's actually constructors it doesn't know about
20:08:28 <mroman> @free f :: (Int,Float)
20:08:29 <lambdabot> $map_Pair $id $id f = f
20:09:12 <mroman> id $ x = id . id $ x is always true .
20:11:10 <oerjan> Int and Float have no type variables, so only id preserves them
20:28:01 <Vorpal> hm what with the trend of pads and phones going super-high dpi these days, I wonder when the same will happen on desktop and laptop monitors
20:28:56 <Vorpal> I wouldn't mind a 150 dpi desktop or laptop monitor (306 dpi like my phone would probably mean I would need dual GPUs just to render the xfce desktop though XD)
20:29:55 <Taneb> Vorpal, that sounds like the FUTURE
20:30:06 <Vorpal> I certainly hope so
20:30:18 <Taneb> Reminds me of a couple of weeks ago
20:30:34 <fizzie> This laptop does 140dpi.
20:30:38 <fizzie> Approximately.
20:30:40 <Vorpal> Taneb, anyway, 192 dpi would be perfect, you could just 2x upscale from 96 dpi (which is pretty common on desktops)
20:30:45 <Vorpal> for bitmap graphics I mean
20:30:52 <Vorpal> fizzie, I wish I had that
20:31:03 <Taneb> One of my friends has a Macbook thingy, and I'm on Ubuntu, and he was like "Haha, can your laptop do this? Spaces are a Mac only feature"
20:31:11 <Vorpal> anyway what would 306 dpi result in on my 22" desktop monitor (16:10)
20:31:11 <Taneb> I said "How many you got?"
20:31:17 <Vorpal> too tired to do the math
20:31:18 <Taneb> He said "Sixteen"
20:31:23 <nortti> has anyone here ever built heirloom-sh or any simple shell like it staticaly?
20:31:27 <Vorpal> Taneb, spaces?
20:31:40 <Vorpal> is that like... virtual desktops?
20:31:54 <Taneb> It's Ubuntu's Workspaces feature
20:32:04 <Vorpal> Taneb, assume I do not use modern ubuntu
20:32:10 <Taneb> So I configured Ubuntu to have 1000000 workspaces
20:32:11 <Vorpal> this laptop I'm on runs 10.04
20:32:11 <Taneb> Um...
20:32:13 <Vorpal> with gnome 2
20:32:19 <Taneb> They were on that?
20:32:24 <olsner> Vorpal: Spaces on mac is like virtual desktops yes
20:32:25 <Taneb> Press ctrl-alt-right?
20:32:37 <Vorpal> Taneb, ah so the virtual desktops then
20:32:41 <Taneb> Yeah
20:32:57 <Taneb> They were pretty outstanded by my million spaces
20:33:10 <olsner> so what happened when you configured it for a million workspaces? did it work?
20:33:18 <Vorpal> I use 2 virtual desktops
20:33:23 <Vorpal> and I hardly ever actually use the feature
20:33:32 <Taneb> olsner, it worked, they overfilled the switching screen and I probably counldn't use them all
20:33:40 <Taneb> I rarely use more than 1
20:34:02 <Taneb> And I've currently set it to have 36, because that's a nice square and it's more than twice what his macbook could do
20:34:02 <fizzie> Vorpal: If I counted right, 5704x3565 would give approx. 306dpi with a 22" diagonal.
20:34:11 <Vorpal> fizzie, nice
20:34:23 <fizzie> (This one gets 144dpi or so with 1920x1080 in 15.4".)
20:34:23 <Vorpal> yeah I would need a new GPU for that to run smoothly
20:34:34 <Vorpal> nice
20:34:54 <olsner> Vorpal: really? I think you probably don't need a gpu at all for that resolution
20:35:00 <Vorpal> fizzie, actually I could view the entire photos from my camera with 1:1 zoom at that resolution
20:35:04 <Vorpal> easily
20:35:11 <Vorpal> iirc it is 37xx x something
20:35:14 <fizzie> That Retina MacBook or whatever that we already discussed has 2880x1800 in the same 15.4" form factor.
20:35:16 <Vorpal> or something like that
20:35:19 <Vorpal> olsner, what
20:35:53 <Vorpal> fizzie, what does that equate in dpi
20:36:31 <fizzie> Vorpal: 220dpi.
20:36:41 <Vorpal> fair enough
20:36:59 <Vorpal> anyway at 300 dpi I suspect you could do serif fonts with no issues
20:37:00 <Vorpal> no?
20:37:47 <olsner> I think a typical desktop resolution doesn't need any acceleration at all to work, and 5704x3565 is only like 5x more than what I have now
20:37:51 <fizzie> Given that they work on paper, presumably.
20:38:04 <Vorpal> olsner, well I meant for 3D games to run smoothly of course
20:38:53 <Vorpal> but yeah I would expect 2D acceleration would be taxed by a resolution like that still
20:38:57 <Vorpal> but maybe not
20:39:24 <fizzie> olsner: You have something like 2560x1600 now, then? Fancy.
20:39:25 <Vorpal> also 120 Hz monitors are awesome
20:41:01 <olsner> fizzie: one 1920x1200 and one 1600x1200
20:41:03 <Vorpal> hm, what about that 4096p video format thing?
20:41:44 <fizzie> Dual-link DVI bandwidth "only" goes up to 3840x2400 or so, which might be a problem for the 300dpi 22" monitor. Though I suppose the more modern things have bumped that up.
20:41:51 <Vorpal> also dammit, why doesn't the youtube player offer an option to neither downscale or upscale 720p video
20:42:05 <Vorpal> s/or/nor/
20:42:34 <fizzie> I think it did, at least down-.
20:43:04 <Vorpal> well I want to play it at 720p on screen, I'm pretty sure it downscales unless full screen, and full screen upscales
20:43:28 <fizzie> Oh, I misread that.
20:43:37 <olsner> me too, it sounded like you wanted scaling
20:43:43 <fizzie> Without the 'n' in 'neither' or something.
20:44:00 <fizzie> Yes, it doesn't have a don't-scale option, that is probably true.
20:44:20 <olsner> I think it's just ambiguous with two possible readings that mean the opposite things
20:44:29 <Vorpal> right
20:44:45 <Vorpal> and youtube-dl + vlc is more work
20:45:13 <Vorpal> hm I should get an USB OTG cable...
20:45:29 <nortti> for what?
20:45:53 <Vorpal> nortti, for connecting stuff like mice and usb memories to my phone.
20:46:22 <nortti> Vorpal: what phone do you have?
20:46:28 <Vorpal> nortti, Samsung Galaxy S3
20:46:35 <Vorpal> (I9300, the international version)
20:47:17 <Vorpal> anyway, I need a micro USB plug to USB type A socket cable
20:47:22 <Vorpal> (those exist)
20:47:41 <nortti> I know. I have used one with nokia n810
20:47:56 <Vorpal> oh okay
20:48:02 <Vorpal> I wonder where to get hold of them
20:48:04 <nortti> but why do you want to attach mouse to androind phone?
20:48:24 <Vorpal> nortti, well maybe not mouse, but what about gamepad?
20:48:37 <nortti> hmm. that sound less crazy
20:48:45 <fizzie> I've done the N900 + PS3 gamepad over bluetooth thing, it worked reasonably well.
20:48:49 <Vorpal> or keyboard for when IRC chatting
20:49:01 <Vorpal> fizzie, PS3 does communication over USB too right?
20:49:09 <Vorpal> or does it only use that for charging?
20:49:23 <fizzie> It uses USB for talking, too, if you have the wire in.
20:49:23 <nortti> some kind of folding keyboard would be nice for that kind of things
20:49:28 <Vorpal> ah
20:49:29 <fizzie> That's how I use it with the computer, mostly.
20:49:35 <fizzie> No worries about batteries, after all.
20:49:56 <Vorpal> I do want to get one... but they are kind of expensive
20:50:07 <Vorpal> and the PS2 needs a converter right?
20:50:13 <nortti> fizzie: have you tried nemo os/mer on your n900?
20:50:32 <nortti> fizzie: also should I buy one
20:51:01 <fizzie> Vorpal: Yes. I've got an old PSX no-analog gamepad with an inexpensive converter for a second pad. Not that I've ever used it for that, I don't really do "friends". (I did use it before I got the PS3 pad, though.)
20:51:42 <fizzie> nortti: Buy one what? And no, I haven't tried nemo/mer or anything especially "nonstandard". Haven't really seen the need, since it works just fine as a SSH client as is.
20:51:46 <Vorpal> well I definitely want analog controllers
20:51:52 <Vorpal> that is the only reason to get a gamepad
20:51:56 <nortti> fizzie: n900
20:52:14 <Vorpal> fizzie, N900 has plastic screen right? Not gorilla glass?
20:52:24 <Vorpal> I saw one that was like super-scratched recently
20:52:26 <fizzie> nortti: Well, I don't have recommendations like that.
20:53:03 <fizzie> Vorpal: Yes. I've got a 3 EUR plastic film on top of the screen, thought I'll just change it if it gets too scratchy.
20:53:11 <nortti> Vorpal: n900 has plastic resistive screen that from what I have used is better than any capasitive screen I have used
20:53:47 <fizzie> I like the screen, but quite a lot of people go all "it's not capacitive so it's completely useless" out of what I think are philosophical reasons.
20:54:03 <fizzie> Given winter temperatures in Finland, I like how it's glove-usable, at least.
20:54:04 <Vorpal> nortti, can't you do a resistive glass screen?
20:54:13 <nortti> Vorpal: no
20:54:26 <Vorpal> anyway I prefer something that work with gloves sure, but I even more prefer something durable
20:55:12 <nortti> fizzie: for a long time I was "it's not resistive so it's completely useless" but then I used htc wildfire and was "it's not resistive so it's mostly useless"
20:55:50 <nortti> Vorpal: I still have screen of my nokia 7710 in a very good shape
20:55:53 <fizzie> Durability is a matter of handling, I personally think. I mean, sure, if you stick it uncovered in a pocket with keys, I suppose it could get scratchy. Anyway, I think the replaceable sticker thing is a reasonable "solution". (Anyway, to each his or her own.)
20:56:13 <Vorpal> eh, during non-winter capacitive works just fine. And I guess I just have to live with using capacitive gloves. Since finding resistive screens is hard
20:56:51 <Vorpal> also can you do oleophobic plastic screens?
20:56:54 <fizzie> I use the N900 stylus quite a lot too, and I understand that's also something "people" hate to do.
20:57:06 <Vorpal> because oleophobic rocks. That is one reason I don't want copter screen protector or similar
20:57:11 <nortti> I love styluses
20:57:12 <Vorpal> because they are not oleophobic
20:57:25 <Vorpal> fizzie, it means you have to use two hands
20:57:30 <Vorpal> which is not always that easy
20:58:39 <fizzie> I don't think the N900 is that terribly well-designed from the one-hand point of view, to be honest. (E.g. just unlocking it with one hand is a bit of a pain, since the hardware lock slider thing is not easy to operate single-handedly, at least for me.)
20:59:11 <fizzie> I suppose you can do the button + slide to unlock thing, but it's not one of my habits.
20:59:14 <Vorpal> heh
20:59:19 <Vorpal> hardware lock slider
20:59:20 <Vorpal> nice
20:59:56 <fizzie> It's nice until it breaks. :p (I've heard of a two or three cases in the interwebs where the hardware slider has just started spewing hundreds of firing events to the board all the time.)
21:00:56 <Vorpal> ouch
21:01:02 <fizzie> It's a spring sort of a thing, it stays in one position and then you slide it down to unlock the screen, it goes back to the previous position by itself. But it's about in the middle of one of the narrow sides, so it's a bit hard with one hand, at least for me.
21:01:20 <Vorpal> that sounds like stupid placement indeed
21:01:39 <fizzie> The whole portrait mode is a bit of an afterthought in the N900. :p
21:02:01 <fizzie> Shows its tablet roots, the way it wants to be landscape most of the time.
21:02:37 <fizzie> They added portrait mode support in the browser, and portrait virtual keyboard, quite late in the software too.
21:03:07 <fizzie> (I mean "it had already been released for a while" late.)
21:04:08 <fizzie> At least the photo browser has always (I think?) done autorotation properly. But initially that was one of the few apps that did.
21:04:57 <fizzie> I'm not even sure if the desktop portrait mode is in the latest official Nokia version, actually.
21:06:04 <Vorpal> heh
21:06:16 <Vorpal> fizzie, so auto rotation is not an OS wide feature?
21:06:21 <nortti> no
21:06:22 <Vorpal> that is kind of crazy
21:06:28 <Vorpal> on a phone I mean
21:06:41 <Vorpal> fizzie, what about rotation in the caller software?
21:06:43 <nortti> yeah. it has tablet roots
21:06:46 <fizzie> It kind of is, now, in that the GUI libs support it.
21:07:01 <Vorpal> fizzie, isn't those just gtk?
21:07:07 <nortti> hildon
21:07:11 <fizzie> There's QT now.
21:07:18 <fizzie> It's where they were going to.
21:07:35 <fizzie> And the "Phone" app is mostly portrait, yes. One of the few exceptions.
21:07:41 <nortti> but then meego was shot down. and tjen meltemi
21:07:50 <fizzie> I don't think it goes into landscape except if you open the hardware keyboard.
21:08:54 <fizzie> Anyway, personally I think something like 70% of my use is just with the hardware keyboard (plus XTerminal + ssh) open, so it doesn't matter all that much. (And most of the rest is in the ebook reader, which has done custom rotation from the start, so you can keep it in portrait mode and read books easily, scrolling pages with the hardware +/- volume rocker which is well-positioned under thumb ...
21:09:00 <fizzie> ... when holding the device portraitly.)
21:09:14 <nortti> fizzie: have you ever used pre-fremantle maemo or maemo tablets?
21:09:52 <fizzie> Not really used-as-in-owned, though I've tried a friend's tablet (I forget which one, exactly) out.
21:10:19 <nortti> did it have hwkeyboard?
21:10:29 <nortti> *hw keyboard
21:10:32 <fizzie> Yes, I think it did.
21:10:38 <nortti> n810
21:10:45 <nortti> running maemo 4
21:10:47 <fizzie> Could be.
21:10:53 <fizzie> There was some sort of a directional pad too, I believe.
21:11:00 <nortti> I have nokia 770
21:11:25 <nortti> I got it in 2005
21:11:34 <nortti> it runs maemo 1
21:11:44 <fizzie> I also briefly fiddled some tablet prototype in some sort of a place (maybe it was at NRC when I spent one summer there?), but I've completely forgotten how that fits in the family tree.
21:12:01 <nortti> NRC?
21:12:08 <fizzie> Nokia Research Centre.
21:12:13 <fizzie> Or maybe it's Center.
21:12:18 <nortti> oh. when was it?
21:12:25 <fizzie> In 2007, I think.
21:12:39 <nortti> then it was probably n800 or n810
21:13:24 <fizzie> Very possible. It had some amount of tape holding bits of it in place, that's about all I can remember.
21:13:29 <nortti> :p
21:14:48 <fizzie> And there was another prototype device (of some Symbian phone) that they didn't have well-fitting flasher hardware receptables for, so you had to keep holding the stupid thing pressed down (so that the pins caught the flashing contacts exposed through a hole behind the battery or something) during the whole flashing process.
21:15:14 <fizzie> For the regular ones the "proper" flasher bit sort of snapped together with the phone and held it in place.
21:15:52 <fizzie> Fortunately I've completely forgotten the device code names; they were funny, but I'm sure they're officially top secret insider information.
21:16:00 <fizzie> Though I've seen some of them in the interwebs.
21:16:24 <nortti> kinda like 7700 was officialy never released
21:19:25 <Vorpal> fizzie, funny?
21:19:32 <fizzie> Well, humorous.
21:19:48 <Vorpal> which ones did you see on the interwebs then
21:19:57 <nortti> there was list of codenames published in nyt some years ago
21:19:57 <Vorpal> surely those are well known already
21:20:03 <Vorpal> nortti, got a link?
21:20:20 <nortti> Vorpal: it is a paper magazine
21:20:25 <Vorpal> oh right
21:20:35 <fizzie> I've completely forgotten. But they're not *that* funny.
21:21:01 <nortti> I had scans of it on my old hd that broke
21:21:28 <fizzie> I've heard (and Wikipedia knows this too) that N9 was called "lankku" (plank, i.e. flat piece of wood), presumably due to the shape. But I'm not sure if that was actually the internal project codename or just a regular nickname.
21:22:25 <fizzie> 2007 was like half a decade ago, after all.
21:23:40 <Vorpal> dammit I want this music but it seems to only be available on iTunes...
21:23:43 <fizzie> I did get my (personal) N-gage's system software updated to the latest version at the Nokia HQ's phone-support desk with no extra cost. (I believe normally they charge some money for doing that unless you actually are having some problems with it and thus can get it done as a warranty fix.)
21:23:52 <nortti> my father told me that n92 was called halko
21:24:04 <fizzie> That sounds very possible.
21:24:16 <Vorpal> what would that name mean?
21:24:27 <fizzie> Uh, larger piece of wood.
21:24:27 <nortti> hmm.
21:24:41 <Vorpal> heh
21:25:10 <Vorpal> fizzie, a single word for "larger piece of wood"?
21:25:12 <Vorpal> awesome
21:25:17 <fizzie> "A log (piece of wood to be burned)" according to wiktionary.
21:25:24 <Vorpal> ah
21:25:26 <Vorpal> okay
21:25:29 <Vorpal> not so super-awesome then
21:25:33 <fizzie> I'm not sure it's exactly the same as the English "log" though.
21:26:06 <fizzie> 1. (7) log -- (a segment of the trunk of a tree when stripped of branches)
21:26:32 <Vorpal> hm okay
21:26:33 <nortti> also older nokia phones are sometimes called halko-nokia
21:26:34 <fizzie> I mean, "halko" kind of has a connotation that it's small enough to be burned in a wood stove or something.
21:26:41 <Vorpal> right
21:27:06 <fizzie> Or shorter, at least.
21:27:08 <fizzie> The kind of thing that you'd take an axe to, to make firewoord, instead of a whole tree trunk.
21:27:15 <fizzie> s/woord/wood/
21:27:30 <fizzie> Or possibly the results of the chopping.
21:27:39 <FireFly> so, 'ved'
21:28:06 <Vorpal> quite
21:28:24 <fizzie> "halko s
21:28:24 <fizzie> vedträ [-t/-et,-n,-na], ved [-en,-,-], klamp [-en,-ar,-arna]
21:28:33 <fizzie> Says the MOT Finnish/Swedish dictionary.
21:28:44 <Vorpal> fizzie, MOT?
21:28:53 <Taneb> Ministry of Transport
21:28:54 <fizzie> It's this dictionary company.
21:29:01 <Vorpal> fizzie, ah
21:29:04 <Vorpal> Taneb, har
21:29:10 <fizzie> I don't know if it's short for something, except for the things it's commonly short for.
21:29:29 <fizzie> It's like QED in Finnish, too, but I doubt that's related.
21:29:49 <nortti> also television program produced by YLE
21:30:18 <nortti> YLE is short for yleisradio
21:30:23 <fizzie> Actually MOT seems to be just the brand name, and the company's called "Kielikone" (lit. "language machine").
21:30:58 <fizzie> Their home page doesn't seem to describe why it's called "MOT".
21:31:31 <fizzie> (It's a commercial thing, but accessible via the university's web-proxy, they have some sort of a volume license deal. (Many other schools and universities also do.))
21:31:51 <Vorpal> hm anyone know a good way to extract the audio of a video file (MP4) to a music file (OGG Vorbis)
21:32:00 <Vorpal> or well, any other suitable format for the music
21:32:34 <Vorpal> I guess ffmpeg can do it (is there anything it can't?) but the question is how
21:32:41 <fizzie> I've used ffmpeg's command-line tool to do that kind of things, but it doesn't exactly have the most memorable command line syntax, so it's always a moment spent fiddling with the man pages.
21:32:49 <Vorpal> ffmpeg: missing argument for option '--help'
21:32:52 <Vorpal> yay
21:32:53 <fizzie> VLC's "save/stream" advanced wizard thing can probably do it too.
21:33:27 <fizzie> (You can select a "no-transcode" option in there if you don't want it to mess with the content, assuming codecs compatible with the containers involved.)
21:33:41 <nortti> Vorpal: ffmpeg -i inputfile outputfile
21:33:48 <Vorpal> nortti, that saves the audio?
21:33:56 <nortti> yes
21:33:57 <Vorpal> what audio format does MP4 contains? Or does that vary?
21:34:01 <Vorpal> nortti, thanks
21:34:02 <fizzie> If it's an audio-only output format, it will automagically do a sensible thing.
21:34:19 <Vorpal> I think it might be more than stereo though
21:34:26 <Vorpal> 5.1 or 7.1
21:34:35 <Vorpal> not 100% sure though
21:34:40 <fizzie> It will print out information about the streams, you can see what it's doing and if it looks sensible.
21:36:41 <fizzie> I don't suppose it's a YouTube MP4, incidentally?
21:36:47 <Taneb> Is it normal to be able to whistle both while inhaling and exhaling?
21:36:56 <Vorpal> and then I need to import it into audacity or something anyway to cut out a bit of a outro bit that I don't want
21:37:11 <Vorpal> Taneb, no you a totally a freak!
21:37:26 <Taneb> Is it normal to be on fire?
21:37:28 <Vorpal> (no idea, does it sound the same or slightly different quality?)
21:37:38 <fizzie> I thought it was normal. (Though I can just produce a whistling sound, not to actually whistle anything sensible.)
21:37:49 <Taneb> Inhaling has a higher range than exhaling
21:37:50 <Vorpal> fizzie, well I think it is normal too
21:38:08 <Vorpal> huh?
21:38:19 <fizzie> (The YouTube question was because youtube-dl has that --extract-audio flag which will automagically invoke the ffmpeg command line tools to save only the audio.)
21:38:25 <Vorpal> my experience is that I get less pure tones when inhaling
21:38:36 <Taneb> I can whistle tunes with both in and out, but inhaling sounds higher pitched
21:38:39 <Vorpal> <fizzie> I don't suppose it's a YouTube MP4, incidentally? <-- yes
21:38:52 <Vorpal> I already have the files downloaded though
21:39:03 <fizzie> In that case you probably don't want to use the flag.
21:39:18 <fizzie> It's not exactly a useful flag if you want both look at things and extract the audio, too.
21:39:33 <Vorpal> fizzie, anyway I do want to cut out a bit on the end where it is a bit of a different music video (with some clickable annotation stuff)
21:40:04 <fizzie> If you're lucky, you could do that with ffmpeg without re-compression, possibly.
21:40:11 <Vorpal> how?
21:40:30 <fizzie> You'd need to give start offsets and lengths in seconds, though, so it's not quite as user-friendly as doing it in Audacity.
21:40:45 <Vorpal> might not even be whole seconds
21:41:04 <fizzie> It's something like "-ss HH:MM:SS.xxx" to do a seek at the start.
21:41:09 <Vorpal> ah
21:41:29 <fizzie> And then "-t" and a similar timestamp to specify the duration of what to extract.
21:41:40 <Vorpal> well I want 0 to whatever point
21:41:43 <Vorpal> so I guess just -t
21:41:47 <fizzie> Okay. Then it's just -t.
21:41:55 <Vorpal> anyway, I need vlc to give me exact timestamps
21:41:57 <Vorpal> how
21:42:00 <Vorpal> gnh
21:42:13 <fizzie> Heh. Well, you could extract the whole thing and then get timestamps from Audacity.
21:42:20 <Vorpal> yeah that would work
21:42:37 <Vorpal> anyway I need to get the codec in mp4 to avoid transcoding the audio
21:42:52 <Vorpal> my natural instinct is using .ogg for output but that is not going to work
21:43:15 <Vorpal> could read the youtube-dl code I guess
21:43:18 <fizzie> If it's from YouTube, I think it's always either MP3 or AAC (the latter for the "high-quality" formats), but I could be wrong there.
21:43:31 <Vorpal> fizzie, some videos are 720p some are 1080p
21:43:41 <Vorpal> have a handful of videos to do this on
21:43:56 <fizzie> I'm under the impression that all that get labeled as "HD" have AAC audio in them. But, again, could be wrong.
21:44:39 <fizzie> Anyway, if you just 'ffmpeg' it into whatever, it'll report what was in there, IIRC.
21:44:41 <Vorpal> guess I could take a look at vlc debug output, it tends to dump a lot of stuff on the terminal when running
21:44:46 <Vorpal> or that
21:44:48 <oerjan> <Taneb> Is it normal to be able to whistle both while inhaling and exhaling? <-- nope, we are both freaks
21:45:09 <fizzie> So you can just "ffmpeg -i file.mp4 test.wav" to get the Audacity timestampable version, and then "ffmpeg -i file.mp4 -t duration output.ext".
21:45:20 <Vorpal> yeah it is AAC
21:45:57 <Vorpal> yeah that should work
21:46:16 <fizzie> I don't know what AAC audio gets conventionally stored in. Though I've certainly seen files with just a ".aac" extension.
21:46:31 <Vorpal> yeah I think that is how it is usually stored
21:46:34 <fizzie> "In addition to the MP4, 3GP and other ISO base media file format-based container formats for storage, AAC audio data may be packaged in a more basic format called Audio Data Interchange Format (ADIF),[39] consisting of a single header followed by the raw AAC audio data blocks.[40] Alternatively, it may be packaged in a streaming format called Audio Data Transport Stream (ADTS), consisting of ...
21:46:40 <fizzie> ... a series of frames, each frame having a header followed by the AAC audio data.[39] Both formats are defined in MPEG-2 Part 7, but are only considered informative by MPEG-4, so an MPEG-4 decoder does not need to support either format.[39] These containers, as well as a raw AAC stream, may bear the .aac file extension."
21:46:53 <fizzie> How typically confused.
21:47:15 <Vorpal> fizzie, what is the tagging format of .aac files?
21:47:18 <Vorpal> ID3?
21:47:21 <fizzie> Heh, no idea.
21:47:36 <Vorpal> ID3 is of course a mess too, as I'm sure I mentioned recently
21:49:36 <fizzie> I'm not sure if ffmpeg is magicky enough to extract only audio if you specify a file.m4a as output. (That's a common name for a MP4 file that has only an audio stream, and I think they have some sort of a common metadata thing, though that latter part is just a hunch.)
21:50:01 <Vorpal> heh
21:51:57 <Vorpal> will try in a bit, working on getting the media files to the right computer atm
21:53:31 <Vorpal> FFmpeg version SVN-r0.5.9-4:0.5.9-0ubuntu0.10.04.1, Copyright (c) 2000-2009 Fabrice Bellard, et al. <-- hm. That guy's name sounds familiar.
21:53:39 <Vorpal> Not the qemu guy, right?
21:53:43 <nortti> yes
21:53:49 <nortti> also the tcc guy
21:53:53 <Vorpal> right
21:54:01 <fizzie> Fingers in all pies.
21:54:04 <Vorpal> quite
21:55:02 <fizzie> Based on a quick test, you will need to "ffmpeg -vn -i infile.ext outfile.m4a" if you want to have it drop the video stream but output a MP4 file. (Not that I'm explicitly advocating a MP4 audio-only container, I have no idea about player/metadata compatibilities.)
21:55:27 <fizzie> (-vn and -an are the "disable video recording" and "disable audio recording" flags of ffmpeg, respectively.)
21:56:00 <Vorpal> fizzie, well I'm pretty sure my phone can do .aac so that is what I'm aiming for
21:56:21 <Vorpal> vn = video not?
21:56:36 <Vorpal> nv sounds saner (no video)
21:57:01 <Taneb> Goodnight
21:57:02 -!- Taneb has quit (Quit: Leaving).
21:57:43 <fizzie> Probably. Or "none". There's at least different "-aX" flags that control different aspects of the audio (bitrates and such), maybe it's copying tht.
21:58:06 <fizzie> I have a feeling I've put raw .aac files on the N900 too, as ring/SMS tones, but I don't know about hanging tags in them.
21:58:19 <Vorpal> tht?
21:58:31 <fizzie> That.
21:58:36 <Vorpal> ah
21:59:31 <Vorpal> anyway I use flac on my computer for music (unless the source format was not a CD), and ogg vorbis for any flac when copying that music to my phone.
21:59:44 <Vorpal> I don't think I have any .aac before though
22:00:02 <fizzie> Having an ".aac" output extension seems to "Output #0, adts, to 'test.aac'" so it'll be an ADTS file. I suppose that must be popular, if it defaults to that.
22:01:52 <fizzie> "Is there a "standard" for tagging AAC ADTS/ADIF ? I see that mp3tag uses APEv2? -- They are usually tagged like MP3 files - ID3v1, ID3v2, APEv2, etc." (Random Google-hit.)
22:02:49 <Vorpal> hm
22:03:07 <Vorpal> fair enough, I use picard mostly for tagging
22:03:18 <Vorpal> and then mp3tag to embed cover art
22:18:06 -!- nortti_ has joined.
22:19:15 -!- copumpkin has quit (Ping timeout: 246 seconds).
22:19:47 -!- copumpkin has joined.
22:23:06 -!- pikhq has quit (Ping timeout: 246 seconds).
22:23:12 -!- pikhq_ has joined.
22:33:16 -!- stanley has quit (K-Lined).
22:33:41 <oerjan> huh
22:33:52 <oerjan> `log stanley>
22:34:27 * oerjan taps fingers
22:34:31 <HackEgo> No output.
22:34:34 <oerjan> `log stanley>
22:34:51 <HackEgo> 2010-06-04.txt:16:08:52: <jamesstanley> you specify
22:34:59 <oerjan> `log <stanley>
22:35:06 <HackEgo> 2012-07-14.txt:22:34:59: <oerjan> `log <stanley>
22:35:15 <oerjan> `pastelogs <stanley>
22:35:21 <HackEgo> http://codu.org/projects/hackbot/fshg/index.cgi/raw-file/tip/paste/paste.2404
22:35:47 <oerjan> i guess he never got around to say anything in this channel
22:37:02 -!- const has changed nick to invariable.
22:37:03 <quintopia> oh
22:38:23 <Vorpal> hrrm, my ffmpeg did not like aac? why
22:38:25 <Vorpal> fizzie, ^
22:40:21 <oerjan> and my znogf is gaffled, too
22:41:17 <Vorpal> oerjan, who was/is stenley?
22:41:28 <Vorpal> stanley*
22:41:48 <Vorpal> oerjan, and what is "and my znogf is gaffled, too" all about?
22:42:43 <Vorpal> ah the ffmpeg on the other computer worked
22:43:08 <Vorpal> actually it didn't
22:43:17 <Vorpal> it just left empty files
22:43:30 <Vorpal> dammit
22:44:31 <Vorpal> oh it can only decode aac
22:47:05 <oerjan> Vorpal: (1) some guy who just got k-lined above, after being here for more than an hour without saying anything
22:47:16 <Vorpal> ah
22:47:56 <oerjan> (2) I just got struck by how incomprehensible "hrrm, my ffmpeg did not like aac? why" would look to a non-technical person
22:48:08 <Vorpal> ah
22:48:19 <Vorpal> seems it has decoding only support for it
22:51:01 <Vorpal> aha found it
22:52:21 <fizzie> Might be split into different packages.
22:52:46 <Phantom_Hoover> <oerjan> Vorpal: (1) some guy who just got k-lined above, after being here for more than an hour without saying anything
22:53:02 <Phantom_Hoover> He was probably a refugee.
22:53:13 <Phantom_Hoover> If only he knew how IRC worked.
22:57:16 <fizzie> Funny, though, you'd think even without the libfaac dependency it could just copy the stuffs, assuming libavformat is what does the actual bundling in an ADTS file.
22:58:09 <fizzie> I do think ffmpeg does try to not re-encode if it's possible.
22:59:08 <fizzie> Might be worthwhile to explicitly "-acodec copy" though.
22:59:12 <oerjan> Phantom_Hoover: wat
22:59:39 <fizzie> (Then it will at least barf if things are not going to work out, instead of silently doing something complicated.)
23:04:56 <Vorpal> building my own ffmpeg atm
23:05:29 <Vorpal> fizzie, actually -acodec copy worked
23:05:34 <Vorpal> I think
23:06:03 <Vorpal> yeah it did
23:13:51 -!- Dovregubben has quit (Ping timeout: 246 seconds).
23:15:26 -!- Dovregubben has joined.
23:15:33 -!- derdon has quit (Remote host closed the connection).
23:16:04 <Vorpal> who is Dovregubben? And that sounds like something in Norwegian?
23:16:08 <Vorpal> oerjan, right?
23:18:38 <oerjan> Vorpal: you are _so_ late
23:19:09 <oerjan> (also, it's a troll from Ibsen's Peer Gynt, and possibly Norwegian folklore in general)
23:21:05 <oerjan> "Selv om Dovregubben bygger på norske eventyr og sagn med røtter tilbake til hedensk tid, er navnet og figuren sannsynligvis Ibsens egen konstruksjon.[trenger referanse]"
23:21:18 <oerjan> take that as you will :P
23:27:04 <Vorpal> oerjan, hm?
23:27:18 <Vorpal> oerjan, yeah so that guy, is he Norwegian?
23:27:38 <oerjan> Dovregubben: er du norsk?
23:28:20 <oerjan> the comcast address does not precisely strengthen the theory
23:28:47 <oerjan> `pastelogs dovregubben
23:28:54 <HackEgo> http://codu.org/projects/hackbot/fshg/index.cgi/raw-file/tip/paste/paste.29444
23:30:02 <oerjan> i say no: <Dovregubben> we may have declared independence on July 4, 1776, but the rest of the world didn't recognize us as independent until years later (if at all)
23:30:53 -!- nortti_ has quit (Quit: AndroIRC - Android IRC Client ( http://www.androirc.com )).
23:32:43 <Vorpal> fizzie, well, whatever format mp3tag uses to write the tags in is not working in either vlc nor on the phone
23:32:44 <Vorpal> hrrm
23:49:27 -!- DHeadshot has joined.
23:53:04 -!- pikhq_ has quit (Ping timeout: 246 seconds).
23:53:09 -!- pikhq has joined.
←2012-07-13 2012-07-14 2012-07-15→ ↑2012 ↑all