00:07:31 -!- TodPunk has quit (Quit: This is me, signing off. Probably rebooting or something.).
00:16:42 -!- Sgeo has joined.
00:25:17 -!- tromp has joined.
00:28:53 -!- Slereah_ has joined.
00:32:00 -!- Slereah__ has quit (Ping timeout: 264 seconds).
00:32:45 -!- Sprocklem has joined.
00:43:09 -!- yorick has quit (Remote host closed the connection).
01:25:22 -!- Phantom_Hoover has quit (Quit: Leaving).
01:47:20 <zzo38> Is it possible to display white pixels in CGA mode when palette 0 low intensity with background color 0 and border color 0 is selected?
02:09:49 -!- vravn has quit (Excess Flood).
02:10:53 -!- vravn has joined.
02:26:56 -!- Sorella has quit (Quit: It is tiem!).
02:32:44 -!- Slereah_ has quit (Remote host closed the connection).
02:32:59 -!- Slereah_ has joined.
02:37:26 <zzo38> Is "Big Man Computer" OK?
03:02:59 -!- Slereah_ has quit (Remote host closed the connection).
03:03:19 -!- Slereah_ has joined.
03:25:01 -!- Bicyclidine has joined.
03:39:28 <Sgeo> Sadly, not every function of several arguments can be flipped
03:40:39 <lambdabot> <hint>:1:1: parse error on input `:'
03:43:18 <Sgeo> The type of the second argument depends on the value of the first argument
03:43:43 <Sgeo> I think you can't have the dependencies go backwards
03:44:58 <Sgeo> Apparently the type of flip indicates this
03:45:28 <Sgeo> (That it only takes non-dependent functions)
03:46:53 <Bicyclidine> why have the dependency unidirectional? the Int "hello" makes just as little sense as (flip the) "hello" Int
03:46:57 <lambdabot> <hint>:1:1: parse error on input `:'
03:47:11 <Bicyclidine> lol does the underlining mean the dependent type thing
03:47:30 <Sgeo> I thinnk underlining means implicit but the implcit argument not shown?
03:47:39 <Sgeo> lowercase unbound is implicit argument
03:48:23 <Sgeo> Not sure how it displays when the implicit argument is shown
03:48:49 <Sgeo> > {n : Nat} -> a -> Vect n a -> Vect (S n) a
03:48:50 <lambdabot> <hint>:1:1: parse error on input `{'
03:49:10 <Sgeo> > :t {n : Nat} -> a -> Vect n a -> Vect (S n) a
03:49:11 <lambdabot> <hint>:1:1: parse error on input `:'
03:49:30 <Sgeo> > :t with Vect (::)
03:49:31 <lambdabot> <hint>:1:1: parse error on input `:'
03:57:17 -!- nisstyre has joined.
04:17:43 <Melvar> Sgeo: You can only have implicits in top-level types.
04:18:48 <Melvar> > :t \a => (n : Nat) -> a -> Vect n a -> Vect (S n) a
04:18:48 <idris-ircslave> \a => (n : Nat) -> a -> (Vect n a) -> Vect (S n) a : Type -> Type
04:18:49 <lambdabot> <hint>:1:1: parse error on input `:'
04:19:02 <lambdabot> <hint>:1:1: parse error on input `:'
04:20:04 <Sgeo> Do explicit implicit arguments get underlined?
04:20:53 <Bicyclidine> i'm going to pretend you didn't construct that phrase
04:20:55 <Melvar> Sgeo: you can :set showimplicits in the REPL, but the bot will not allow that command. The REPL will then display all implicit bindings, and they will still be underlined.
04:45:58 <quintopia> is there a windows rsync client thing
04:58:54 -!- Slereah__ has joined.
05:00:37 -!- Slereah_ has quit (Ping timeout: 265 seconds).
05:02:02 -!- vravn has quit (Excess Flood).
05:02:25 -!- vravn has joined.
05:04:00 -!- nooodl has quit (Ping timeout: 265 seconds).
05:24:19 -!- Slereah_ has joined.
05:24:58 -!- Slereah__ has quit (Ping timeout: 240 seconds).
05:32:04 -!- ski has quit (Quit: Lost terminal).
05:33:24 -!- tromp has quit (Remote host closed the connection).
05:47:01 -!- Sprocklem has quit (Ping timeout: 244 seconds).
05:58:11 -!- shikhin has joined.
06:08:47 -!- Slereah__ has joined.
06:10:29 -!- Slereah_ has quit (Ping timeout: 252 seconds).
06:18:01 -!- Vorpal has quit (Ping timeout: 240 seconds).
06:19:34 -!- Vorpal has joined.
06:29:51 -!- vravn has quit (Excess Flood).
06:29:59 -!- vravn has joined.
06:34:16 <zzo38> For matching a sequence of instructions, do you think this way is OK? http://sprunge.us/adVO
06:34:32 <zzo38> Please tell me anything that you think might be wrong with it.
06:37:18 -!- Bicyclidine has quit (Ping timeout: 245 seconds).
06:39:32 -!- TodPunk has joined.
06:40:37 -!- tromp has joined.
06:40:50 -!- ski has joined.
06:44:46 -!- Slereah__ has quit (Read error: Connection reset by peer).
06:45:05 -!- Slereah_ has joined.
06:45:30 -!- tromp has quit (Ping timeout: 265 seconds).
06:58:45 -!- ais523 has joined.
07:14:39 -!- oklopol has joined.
07:14:58 -!- Slereah_ has quit (Ping timeout: 240 seconds).
07:17:03 -!- shikhout has joined.
07:20:00 -!- shikhin has quit (Ping timeout: 255 seconds).
07:20:01 -!- shikhout has changed nick to shikhin.
07:43:24 -!- HackEgo has joined.
08:01:59 -!- Tod-Autojoined has joined.
08:11:02 -!- TodPunk has quit (*.net *.split).
08:11:08 -!- Sgeo has quit (*.net *.split).
08:11:10 -!- atehwa has quit (*.net *.split).
08:11:10 -!- sebbu has quit (*.net *.split).
08:11:10 -!- zzo38 has quit (*.net *.split).
08:11:12 -!- quintopia has quit (*.net *.split).
08:11:13 -!- augur has quit (*.net *.split).
08:11:13 -!- myname has quit (*.net *.split).
08:11:13 -!- jix has quit (*.net *.split).
08:33:37 -!- prooftechnique has quit (Quit: leaving).
08:47:54 -!- conehead has quit (Quit: Computer has gone to sleep.).
08:49:10 -!- shikhout has joined.
08:50:54 -!- shikhin has quit (Ping timeout: 255 seconds).
08:50:56 -!- shikhout has changed nick to shikhin.
09:00:58 -!- jix has joined.
09:00:58 -!- myname has joined.
09:00:58 -!- augur has joined.
09:00:58 -!- quintopia has joined.
09:00:58 -!- zzo38 has joined.
09:00:58 -!- sebbu has joined.
09:00:58 -!- atehwa has joined.
09:00:58 -!- Sgeo has joined.
09:07:00 -!- MoALTz has joined.
09:07:45 -!- oerjan has joined.
09:10:19 <oerjan> that was weird, irssi cycled through every freenode server i have listed + irc.freenode.net, but couldn't connect.
09:10:56 <oerjan> then i did /connect freenode manually, and it immediately reached the normal one.
09:13:51 <oerjan> wait no it got thrown off again, but it happened before i joined the channel so i didn't notice before checking the status window
09:15:55 <oerjan> nope it's even weirder, i'm on two servers, but oerjan_ didn't join this channel.
09:17:01 <oerjan> i didn't know you could connect twice to the same network in a single irssi session.
09:17:10 <oerjan> not that i've ever tried before.
09:17:46 <oerjan> presumably my manual connection got added to the usual one, which resumed cycling through the hosts after a while.
09:18:20 <olsner> if you have several users on the same network, I think the only way to do that is to connect once per user, so it makes sense if it's supported
09:18:30 <olsner> but maybe you consider yourself the same as oerjan_
09:20:14 <oerjan> well he does look eerily similar to me
09:23:03 <oerjan> `learn oerjan_ is oerjan and ørjan's chimæric clone. he shows up on irc when the network is having trouble.
09:35:25 <fizzie> Eerily similar, except for the tail.
09:36:19 <fizzie> I'm imagining something like http://goo.gl/RizR8e
10:10:24 -!- jconn has quit (Ping timeout: 264 seconds).
10:13:14 -!- jconn has joined.
10:14:12 <fizzie> It has a thing called "label tracks" where you can put point or region labels denoting things on the audio track.
10:14:32 <fizzie> And then it can export this label track in a simple text format; we've used that for a project-thing.
10:15:19 <fizzie> Turns out the time stamps in the text format have '.' or ',' as the decimal separator depending on the current locale.
10:15:53 <fizzie> It's not like it's a problem, it's just so silly.
10:17:45 <ais523> I remember SMBX uses the current locale for floats in NPC description files, meaning that levels suddenly stop working if you give them to someone French
10:18:01 <olsner> it will be a problem if someone uses a different locale... we had some silly software with the same issue and ended up making separate config files for polish computers
10:18:33 <ais523> languages really need to distinguish between functions that output for serialization, and functions that output for human consumption
10:19:27 <olsner> (or more generally, one config for .-locales and one for ,-locales, but iirc it was one specific office that had the "wrong" locale most often)
10:20:55 <ais523> comp.lang.c have been debating this recently, wrt thousands separators
10:22:00 <fizzie> I just had to make my script to parse those label tracks we got (from non-technical users) to accept either; there seems to never be a thousands separator in these.
10:22:53 <fizzie> I'm not sure if the Linux Audacity follows the system locale; mine generates dots but this is en_US; the files we got from a (presumably set to Finnish) Windows system had commas.
10:26:33 <fizzie> There's something peculiar about this (elderly, female) speaker that just makes this forced-alignment system work real badly.
11:14:27 -!- boily has joined.
11:32:02 <boily> `? something-that-isn't-in-hackego's-wisdom
11:32:03 <HackEgo> something-that-isn't-in-hackego's-wisdom? ¯\(°_o)/¯
11:32:23 <boily> I knew it! it's the same face as in this week's what if from xkcd!
11:39:27 <ais523> except that XKCD characters don't have eyes (or noses, or mouths)
11:39:45 <ais523> at least, I guess that's a mouth not a nose, but I'm not sure
11:40:05 <ais523> ``echo It is now. > "wisdom/something-that-isn't-in-hackego's-wisdom"
11:40:06 <HackEgo> /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: `echo: not found
11:40:09 <ais523> `` echo It is now. > "wisdom/something-that-isn't-in-hackego's-wisdom"
11:40:32 <fizzie> ais523: The string "¯\(°_o)/¯" is literally there in the title attribute of an image in what-if.
11:40:57 <fizzie> (How come that got legs and boily didn't?)
11:40:58 <ais523> I didn't realise what-if had alt text too
11:41:07 <ais523> fizzie: myndzi added an ignore for hackego
11:41:22 <ais523> the "not there" face was added specifically to trigger it
11:41:44 <ais523> and so myndzi added anti-botloop protection, as is customary
11:41:59 * boily pokes his own legs, just to be sure of their existence
11:43:57 <ais523> hmm, it's pretty much impossible for me to be sure you have legs: you could claim you have them, but you could be lying; if you send a photo it could be of someone else; if you meet me in person, it could be someone else pretending to be boily
11:45:46 <ais523> come to think of it, I don't even know you're actually one peron
11:46:00 <ais523> there could be a team of people, all taking turns to pretend to be boily
11:46:48 <fizzie> Many people here could well be collectives.
11:47:08 <fizzie> fungot: Are you a single bot, or a collection of bots talking to some kind of a IRC multiplexer?
11:47:08 <fungot> fizzie: lol, the pilot is safe) got by far the biggest selling game of the games where kickass im glad they are doing this song!
11:47:40 <ais523> if you did replace fungot by a multiplexer, it would be hard for us to tell
11:47:41 <fungot> ais523: it is you think its funny when the pilot had it configured for landing
11:47:54 <fungot> Available: agora alice c64 ct darwin discworld enron europarl ff7 fisher fungot homestuck ic irc iwcs jargon lovecraft nethack pa qwantz sms speeches ss wp youtube*
11:48:08 <ais523> hmm, I guess one of fungot's youtube videos must have been about a plane
11:48:53 <boily> so fungot loves the three airplane parts that compose him.
11:49:11 <boily> fungot: which one? you remember you have two girlfriends, don't you?
11:49:11 <fungot> boily: you racist son of a fool was look up the time it would be so hard).
11:49:35 <boily> fungot: eille! I'm perfectly fine with polyamorous relationships!
11:49:35 <fungot> boily: um, yes, i laughed my ass off at 100 ft, the actual song xd!!
11:49:57 <boily> fungot: 100 ft isn't that high for an airplany being like you...
11:49:57 <fungot> boily: y a quand meme eu 3 mort sur les 130 apssagers.
11:50:31 * boily slinks away from fizzie's murderous bot.
11:51:15 <boily> (translation for the lazy: “there still were three deaths in the 130 passengers.”)
11:51:19 -!- jhj has joined.
11:51:33 <fizzie> One of them was a plane crash video, yes.
11:52:10 <ais523> I think we need more videos, really
11:52:22 <ais523> in order to get reasonable (or sufficiently unreasonable) output
11:52:24 <fungot> Selected style: nethack (NetHack 3.4.3 data.base, rumors.tru, rumors.fal)
11:52:36 <ais523> let's see if fungot's more varied with this
11:52:36 <fungot> ais523: ptah: known under various names in different parts of ireland: cluricaune in cork, lurican in kerry, lurikeen in kildare and lurigadaun in tipperary. although they were sure of.
11:52:49 <ais523> I guess that's mostly literal
11:53:01 <ais523> fungot: something else?
11:53:02 <fungot> ais523: amber*: " i am aware, yes." " you wouldn't like it much anyway," answered pelias cryptically. " my dear!" said the old melnibonean empire. these large groups are able to look like nothing more than a nymph knows how old this mighty wizard is even more powerful of all nations, by barry cox)
11:53:17 <ais523> yeah, this is too literal :-(
11:53:28 <ais523> might work better with only one word of context, or one and a half
11:53:49 <fizzie> I believe the YouTube style included comments from a total of perhaps 7 videos.
11:54:20 <ais523> not exactly a large corpus
11:54:23 <fizzie> And yes, the NetHack dataset also makes fungot copy a lot verbatim.
11:54:23 <fungot> fizzie: archon: archons are the predominant inhabitants of the spider lay dead beside him.
11:54:36 <fizzie> Though I didn't know archons live in spiders.
11:54:44 <fungot> Selected style: alice (Books by Lewis Carroll)
11:54:54 <oerjan> `echo The string "¯\(°_o)/¯" is
11:55:20 <oerjan> The string "¯\(°_o)/¯" is
11:55:22 <ais523> I guess myndzi's got a general ignore on all the bots
11:55:35 <ais523> good point, why did it not trigger on the /request/
11:55:51 <oerjan> the thing is, iirc myndzi _doesn't_ have an ignore on HackEgo.
11:55:55 -!- trn has quit (Ping timeout: 265 seconds).
11:56:14 -!- ggherdov has quit (Ping timeout: 265 seconds).
11:56:16 <ais523> maybe he has throttling?
11:56:26 * boily therapeutically, restoratively maintenancically mapoles myndzi
11:56:26 <fizzie> The "alice" style includes http://sprunge.us/JOVK
11:56:31 <ais523> fungot: opinions on this matter?
11:56:31 <fungot> ais523: " i'm strolling your way," said the hatter. he came in with a teacup in one hand and a large fan in the other compartment. if the universe of things be divided with regard to the class of " new cakes", we may call it stuff, if you must know, we used to be taught in the nursery," i echoed. " the fairy-king is fnord, fnord low, that alice quite started.
11:56:39 <oerjan> no, the answer to why he didn't answer HackEgo is more devious
11:56:52 -!- clog has quit (Ping timeout: 265 seconds).
11:56:57 <ais523> oerjan: do you know it? or have you jut concluded it's devious?
11:56:58 <oerjan> (except that myndzi's script is obviously not working _now_)
11:57:05 <ais523> that looks like he was close to pinging out
11:57:07 <oerjan> well i made it, so i know :P
11:57:18 <oerjan> `echo The string "¯\(°_o)/¯" is
11:57:23 <ais523> he hasn't answered fungot either, though
11:57:24 <fungot> ais523: 4. no m' are y', and some are not-x. the lion were coming. and he shortened it up?" said bruno. " and he lets uggug take away all my fnord! and proud am i to do with you.
11:57:48 <oerjan> as you see, he responded to HackEgo there
11:58:09 <ais523> ^ul (¯\(°_o)/¯ padding)S
11:58:20 <ais523> OK, I think that explains it pretty well
11:58:38 <HackEgo> to fnordly test? ¯\(°_o)/¯
11:58:39 <fizzie> else echo "$1? ¯\(°<U+200B>_o)/¯"; exit 1;
11:59:24 <ais523> hmm, need to be careful who I copy-paste
12:00:30 <fizzie> oerjan: Thor, perhaps?
12:01:11 -!- boily has quit (Quit: INK CARTRIDGE CHICKEN).
12:07:25 <oerjan> fizzie: more like Loki
12:09:45 <oerjan> they've been doing this bloody building work since mid November.
12:09:48 -!- shikhout has joined.
12:10:24 -!- ggherdov has joined.
12:11:51 <oerjan> although i'm not sure it's still the same team as then, i cannot see them outside now.
12:12:03 -!- shikhin has quit (Ping timeout: 255 seconds).
12:12:17 <oerjan> so maybe the sound is coming from inside the house.
12:12:50 -!- shikhout has quit (Read error: No route to host).
12:12:59 <fizzie> The KILLER may already be IN THE HOUSE.
12:13:40 -!- shikhin has joined.
12:18:41 -!- clog has joined.
12:24:11 -!- MindlessDrone has joined.
12:34:57 -!- shikhin has quit (Read error: Connection reset by peer).
12:35:57 -!- nooodl^ has joined.
12:42:00 -!- shikhin has joined.
13:05:27 -!- realzies has quit (Quit: realzies).
13:11:25 -!- Guest63910 has joined.
13:18:59 -!- nooodl^ has quit (Ping timeout: 240 seconds).
13:27:33 -!- yorick has joined.
13:30:44 -!- Guest63910 has changed nick to realzies.
13:30:50 -!- realzies has quit (Changing host).
13:30:50 -!- realzies has joined.
13:35:02 -!- Bike has quit (Ping timeout: 252 seconds).
13:39:29 -!- oerjan has quit (Quit: leaving).
13:57:54 -!- monotone has quit (Quit: Rebooting server).
13:58:14 -!- Sgeo has quit (Read error: Connection reset by peer).
14:00:31 -!- Sorella has joined.
14:02:04 -!- monotone has joined.
14:24:36 -!- Phantom_Hoover has joined.
14:30:25 -!- FreeFull has joined.
14:41:13 -!- nooodl has joined.
14:41:33 -!- siruf has joined.
14:49:08 <Phantom_Hoover> MEANWHILE IN /R/BITCOIN: http://www.reddit.com/r/Bitcoin/comments/1zm1v5/today_i_logged_onto_my_computer_and_found_none_of/
14:51:12 <Phantom_Hoover> oh holy shit this one's even better: http://www.reddit.com/r/Bitcoin/comments/1zlhh5/until_recently_my_only_serious_experience_with/
14:52:17 -!- MoALTz has quit (Quit: bbl).
14:54:08 -!- siruf has quit (Changing host).
14:54:08 -!- siruf has joined.
14:58:45 -!- siruf has changed nick to siruf_.
14:59:04 -!- siruf_ has changed nick to siruf.
15:02:01 -!- siruf has quit (Quit: leaving).
15:02:37 -!- siruf has joined.
15:02:45 -!- siruf has quit (Changing host).
15:02:45 -!- siruf has joined.
15:21:26 <tromp_> is this #bitcoin-gossip now :-?
15:21:33 -!- HackEgo has quit (Ping timeout: 244 seconds).
15:32:15 -!- Sprocklem has joined.
15:34:59 -!- realzies has quit (Quit: realzies).
15:40:59 -!- Bike has joined.
15:41:20 <Phantom_Hoover> tromp_, no it's just that making fun of bitcoiners is great fun
15:42:24 <tromp_> does owning 0.00004971 BTC make me a bitcoiner:-?
15:42:59 -!- Guest91338 has joined.
15:47:04 -!- HackEgo has joined.
15:51:48 -!- HackEgo has quit (Ping timeout: 264 seconds).
16:10:47 -!- password2 has joined.
16:20:12 -!- password2 has quit (Ping timeout: 265 seconds).
16:22:59 -!- HackEgo has joined.
16:26:15 -!- password2 has joined.
16:32:45 -!- nisstyre has quit (Quit: WeeChat 0.4.3).
16:35:09 <elliott> many people with lots of bitcoins make fun of bitcoiners, too
16:38:31 <ais523> I was surprised at learning how many bitcoins were stored in bitcoin bank-equivalents to be stolen, in the first place
16:39:26 <ais523> like, the reason people store their money in banks is for a chance at interest (admittedly not so high nowadays), and (in the UK) for ISA limits
16:40:11 <elliott> and because a bank is safer than storing it in your house.
16:40:26 <elliott> also because piles of gold take up a lot of space
16:40:32 <elliott> (here I assume that you support the gold standard if you want to do this)
16:41:31 <ais523> I'm not sure if either of the last two theories apply to bitcoins
16:41:51 <elliott> well, the blockchain takes up a very annoying amount of disk space and it takes a long time to download
16:42:19 <ais523> but you don't need the blockchain to make transactions
16:42:20 <elliott> and there might be a lot of crappy services that host bitcoin wallets, but personal computers are rarely very secure at all...
16:42:32 <ais523> you need it to verify how much money a given person has
16:42:55 <elliott> I just mean it's not as "simple" as downloading bitcoin-qt or whatever
16:43:01 <elliott> but admittedly there are all the alternative clients now.
16:43:14 <elliott> anyway, how many people have computers that even have disk encryption?
16:49:40 -!- spiette has joined.
16:56:04 -!- Guest91338 has changed nick to realzies.
16:57:38 -!- Slereah_ has joined.
17:00:39 -!- Slereah__ has joined.
17:01:44 -!- Slereah__ has quit (Read error: Connection reset by peer).
17:02:00 -!- Slereah__ has joined.
17:02:32 <Vorpal> fizzie, nice "macroSD"
17:03:06 <Vorpal> fizzie, wish you could get larger depth of field in it though. :/
17:03:37 -!- Slereah_ has quit (Ping timeout: 240 seconds).
17:04:38 -!- Sprocklem has quit (Ping timeout: 252 seconds).
17:06:57 -!- Slereah__ has quit (Ping timeout: 244 seconds).
17:07:04 -!- Sprocklem has joined.
17:38:36 -!- password2 has quit (Ping timeout: 264 seconds).
17:47:20 -!- Slereahphone has joined.
17:56:13 -!- password2 has joined.
18:08:28 -!- password2 has quit (Ping timeout: 252 seconds).
18:09:59 -!- shikhout has joined.
18:12:50 -!- shikhin has quit (Ping timeout: 264 seconds).
18:12:51 -!- shikhout has changed nick to shikhin.
18:15:15 -!- Phantom_Hoover has quit (Ping timeout: 265 seconds).
18:21:01 <fizzie> Vorpal: I could do focus stacking with enfuse, I guess.
18:24:57 <fizzie> Also managed to finally write up what I found when I reverse-engineered the firmware in my VDSL2 modem back in Dec 2011, which was probably really useful to do *now*, given that I'm pretty sure they've discontinued the model already.
18:28:04 <Vorpal> fizzie, found anything interesting?
18:30:03 -!- Phantom_Hoover has joined.
18:30:03 <fizzie> Depends on the definition. I did find the hardcoded user:pass pairs for its telnet interface, which was what I was after.
18:31:33 -!- newsham_ has changed nick to newsham.
18:37:22 -!- Phantom_Hoover has quit (Ping timeout: 244 seconds).
18:39:48 -!- Sprocklem has quit (Ping timeout: 264 seconds).
19:04:34 -!- oerjan has joined.
19:08:56 <Taneb> shachaf, someone asked me what a complete lattice was and I panicked until I suddenly remembered the training you gave me
19:10:28 <Taneb> At the very least you told me what a complete lattice was
19:11:32 <shachaf> one that has all small limits, obviously
19:12:31 <ais523> isn't the definition of a lattice that it has all infima and suprema?
19:12:36 <oerjan> wait, just small ones?
19:13:03 <oerjan> also that you only need either infima or suprema, they're equivalent conditions
19:14:15 <ais523> oerjan: huh? a semilattice has one but not the other
19:14:32 <oerjan> well it has to be a lattice to start with
19:14:53 <ais523> oh gah, there are four different mathematical objects called lattices
19:15:21 <oerjan> is there's more than one that's a kind of partial order?
19:15:48 <oerjan> a lattice has infs and sups of pairs, and thus all finite ones.
19:15:49 <ais523> oerjan: ah right, so the definition of an ordinary lattice can take the infimum or supremum of two objects, a complete lattice can consistently take it of more than two
19:16:13 -!- conehead has joined.
19:16:21 <oerjan> well finite follows from two.
19:17:01 -!- MoALTz has joined.
19:17:27 <ais523> oerjan: ah right, meet and join have to be associative and commutative
19:17:40 <ais523> I'm crazy enough that I was considering a lattice-like structure where they weren't
19:18:31 <ais523> oh, incidentally, esolangs meet "proper" research: writing up my PhD thesis, my major goal right now (in fact, one of the major results) is to do with Anarchy's type system, in the absence of recursion
19:18:52 <oerjan> well it follows automatically if they're meet and join defined from actual partial orders.
19:19:41 <oerjan> so did you prove it TC
19:20:22 * oerjan guesses it wouldn't be, but couldn't resist joking
19:21:30 <ais523> oerjan: actually one major result is that it isn't, in the absence of recursion
19:21:42 <ais523> /really/ major, in that it can trivially be used to prove typed lambda calculus sub-TC
19:21:51 <ais523> which is an existing result, but one that it's nice to be able to easily replicate
19:23:30 -!- Sprocklem has joined.
19:23:55 <oerjan> well that analogy is why i guessed it wouldn't be TC
19:25:09 <oerjan> like with any of simple types/hindley-milner/system F, you need explicit recursion to make it TC
19:26:53 <oerjan> and many even stronger type systems are terminating without recursion afaiu
19:30:39 <ais523> Anarchy the language does have recursion, though, which probably makes it undecidable to compile
19:30:59 <ais523> I may put restrictions on it to make the type system decidable, especially as its purpose as a language doesn't need TCness and would benefit from totality
19:31:05 -!- itsy has joined.
19:39:16 <oerjan> hm the buggy behavior of IE's tab grouping just got weirder
19:39:54 <oerjan> i now have a purple tab between two dark blue ones, all of which started out as the same group
19:40:39 <oerjan> normally, when i drag a tab in between two in the same group, it gets joined to them.
19:41:30 <oerjan> but presumably somehow it thinks both that it already is in their group and doesn't need to be joined, and that it isn't and therefore gets a different color.
19:43:07 <zzo38> Can you tell me if my program is OK?
19:43:07 <oerjan> managed to fix it by removing another one of them from the group, then reinserting it, then permuting wildly until all got the same color again.
19:45:43 <oerjan> hm as i close all but one tab of the group, a bug remains: the tab doesn't lose its color like normal.
19:46:28 <oerjan> might wonder wtf they did to get this behavior. i have a hunch about broken linked lists.
19:48:24 <ais523> I'd find it hard to believe that Microsoft don't have a standardised internal library for list linking
19:49:02 <HackEgo> [U+0059 LATIN CAPITAL LETTER Y] [U+0070 LATIN SMALL LETTER P] [U+006E LATIN SMALL LETTER N] [U+0079 LATIN SMALL LETTER Y] [U+0070 LATIN SMALL LETTER P] [U+006E LATIN SMALL LETTER N]
19:49:44 <oerjan> hm i guess they weren't as cyrillic as they seemed in recent changes
19:50:38 <ais523> that isn't particularly pronounceable in cyrillic either, is it?
19:51:04 <oerjan> urpurp isn't so bad...
19:51:36 <ais523> oh, cyrillic n is pronounced "p"? didn't know that one
19:51:45 <ais523> I guess "urnurn" isn't bad either
19:53:00 <oerjan> also, cyrillic "italic" is weird.
19:53:34 <oerjan> enough so that i get annoyed when something cyrillic gets accidentally italicized, because i cannot transcribe it
19:55:58 <oerjan> which happens in google translate if i try to write something russian with latin letters - it'll guess what cyrillic letters i mean, but it shows them italicized so it's not obvious to me if it's guessed correctly.
19:56:09 <oerjan> not that i do this often, anyway
19:59:58 <oerjan> actually tried to test it now and it switches randomly between suggestions in cyrillic, italic cyrillic and latin
20:07:47 <zzo38> If making a instruction set with some general purpose registers, if you have a [R++] and [--R] addressing mode, if some of these "general purpose" registers also includes the program counter and stack pointer then you don't need a immediate addressing mode, and you don't need more modes for stack either.
20:18:20 -!- MindlessDrone has quit (Quit: MindlessDrone).
20:20:41 <Vorpal> Huh, just found out Chrome OS uses portage from Gentoo for package management. Probably old news to everybody else.
20:27:51 <fizzie> Can you install Chrome OS on anywhere, or is it just for Chromebooks and such?
20:28:12 <fizzie> Oh, there's a similar Chrome OS / Chromium OS thing going on? I guess that makes sense.
20:29:22 <fizzie> (Just for the terminology, maybe they should set up a separate company called Googlium to do all things related to the open-source efforts.)
20:29:25 <ion> http://www.chord.co.uk/blog/new-chord-ethernet-cables/
20:30:52 <fizzie> Wow, a directional Ethernet cable.
20:47:43 -!- tertu has joined.
20:52:01 -!- Sprocklem has quit (Ping timeout: 240 seconds).
20:53:30 -!- Sprocklem has joined.
20:56:39 -!- ais523 has quit.
21:00:49 -!- itsy has quit (Ping timeout: 240 seconds).
21:08:43 -!- itsy has joined.
21:11:13 <zzo38> Can you tell me if my pattern matching instructions program looks like OK to you? http://sprunge.us/adVO Or if, you thikn I did something wrong?
21:16:01 -!- quintopia has quit (Ping timeout: 240 seconds).
21:24:15 -!- quintopia has joined.
21:30:22 -!- Bike has quit (Ping timeout: 252 seconds).
21:46:01 <Taneb> Do we have a dicebot
21:46:47 <Taneb> lambdabot, thank you lambdabot
21:47:14 <int-e> wait, that has a contextual match?
21:48:03 <int-e> I'm surprised that I have not seen this trigger accidentally.
21:48:27 <zzo38> You could also use the dice function built-in to FurryScript.
21:48:36 <zzo38> Which may be somewhat more sophisticated.
21:48:53 <int-e> 3d1 + 3d2 + 3d3 + 3d4
21:48:53 <lambdabot> int-e: (1+1+1) + (2+1+1) + (1+2+2) + (2+3+4) => 21
21:49:36 <zzo38> Documentation is at: http://esolangs.org/wiki/User:Zzo38/FurryScript#Dice
21:52:45 <zzo38> I don't think it is installed on HackEgo, but if it has PHP then you can.
21:54:19 <zzo38> (Or else to rewrite it in C and make it go faster)
21:58:40 <zzo38> It doesn't seem to have PHP, or even SQLite.
22:02:05 <zzo38> You should install SQL on there
22:02:32 <HackEgo> Usage: java [-options] class [args...] \ (to execute a class) \ or java [-options] -jar jarfile [args...] \ (to execute a jar file) \ where options include: \ -d32 use a 32-bit data model if available \ -d64 use a 64-bit data model if available \ -server to select the "server" VM \ -jamvm to select
22:02:44 <int-e> ok. it has that. I agree then :P
22:02:53 <zzo38> O, so they do have Java
22:04:10 <zzo38> But they should install other things too such as SQLite
22:04:44 <zzo38> And PHP (which isn't actually very good, but since there are some program written in PHP, you should install it so that you can use programs which are written in PHP).
22:04:48 -!- Bike has joined.
22:05:00 -!- jconn has quit (Ping timeout: 264 seconds).
22:08:36 -!- tertu has quit (Ping timeout: 264 seconds).
22:21:36 -!- Sprocklem has quit (Ping timeout: 244 seconds).
22:32:19 -!- iamcal___ has quit (Read error: Connection reset by peer).
22:32:37 -!- iamcal___ has joined.
22:46:44 -!- oerjan has quit (Quit: leaving).
22:55:42 -!- Slereahphone has quit (Quit: Colloquy for iPhone - http://colloquy.mobi).
22:58:42 <itsy> https://twitter.com/john_metcalf/status/441346697038270464 :-)
23:07:09 <HackEgo> ` \ ^.^ \ ̊ \ ? \ ¿ \ @ \ ؟ \ ＷＥＬＣＯＭＥ \ \ \ aaaaaaaaa \ addquote \ addwep \ allquotes \ anonlog \ as86 \ aseen \ bienvenido \ botsnack \ bseen \ buttsnack \ calc \ CaT \ catcat \ cats \ cdecl \ c++decl \ chroot \ coins \ complain \ complaints \ danddreclist \ define \ delquote \ delvs \ dis86 \ e \ echo \ echo \ ello \
23:07:16 <lambdabot> unexpected end of input: expecting number, "d" or "("
23:11:24 <zzo38> You should tell Gregor to install PHP and SQLite.
23:11:56 <HackEgo> ＷＥＬＣＯＭＥ ＴＯ ＴＨＥ ＩＮＴＥＲＮＡＴＩＯＮＡＬ ＨＵＢ ＦＯＲ ＥＳＯＴＥＲＩＣ ＰＲＯＧＲＡＭＭＩＮＧ ＬＡＮＧＵＡＧＥ ＤＥＳＩＧＮ ＡＮＤ ＤＥＰＬＯＹＭＥＮＴ！ ＦＯＲ ＭＯＲＥ ＩＮＦＯＲＭＡＴＩＯＮ， ＣＨＥ
23:14:10 -!- MoALTz has quit (Quit: Leaving).
23:19:45 -!- prooftechnique has joined.
23:42:32 -!- Phantom_Hoover has joined.
23:46:53 -!- nooodl has quit (Quit: Ik ga weg).
23:53:05 -!- prooftechnique has quit (Quit: Changing server).