00:00:01 -!- shikhout has joined.
00:02:17 -!- yorick has quit (Remote host closed the connection).
00:03:05 <oerjan> gah i run out of moisturizing cream and the itching on my hands immediately drives me crazy
00:03:43 -!- shikhin has quit (Ping timeout: 272 seconds).
00:08:36 -!- Froox has quit (Quit: *bubbles away*).
00:13:07 -!- Bike has quit (Ping timeout: 240 seconds).
00:27:23 -!- Bike has joined.
00:31:52 -!- Bike has quit (Ping timeout: 245 seconds).
00:39:21 -!- boily has joined.
00:40:57 <boily> back from the dentist. my mouth is now metalless!
00:43:35 <boily> it feels incredibly weird to suddenly not have a metal wire running behind one's teeth.
00:44:20 -!- Bike has joined.
00:50:48 <boily> and I had a new set of impressions made. next week I'll get a bite splint.
00:53:34 -!- mhi^ has quit (Quit: Lost terminal).
00:55:02 <boily> . o O ( I wonder what's the MRSP of a jug of alginate )
00:58:02 <boily> heh. a quick search turns out that a pound of dental alginate runs for about 12 bucks.
01:01:03 -!- Bike has quit (Ping timeout: 264 seconds).
01:02:49 -!- Bike has joined.
01:04:03 * oerjan is not sure any of those fit boily's sentence
01:08:09 -!- metasepia has joined.
01:08:14 <metasepia> MrsP.com is a free children's entertainment website. It stars actress Kathy Kinney as Mrs. P, a redheaded Irishwoman who reads classic children's stories from her "Magic Library." The target audience for the website is kids between the ages of 3-12, and its goal is to "encourage a lifetime love of reading." It has no advertising and no subscription fees. The site is produced by Mrs P Enterprises, LLC and was created by Kinney, who played Mimi on The
01:08:29 <oerjan> clearly what you meant
01:08:32 <oerjan> now in agora: a bug that people exploit by voting, retracting their vote, then revoting in the opposite way.
01:09:04 <boily> and the exploit being?
01:11:00 <oerjan> there's a reward for having voted opposite of the outcome of a proposal
01:11:20 <oerjan> and a bug in the phrasing that was _supposed_ to exclude retractions.
01:15:53 <Sgeo> Maybe I should get back into Agora someday
01:16:30 -!- Bike has quit (Ping timeout: 255 seconds).
01:17:14 <Sgeo> oerjan: which proposal? I'm curious
01:18:11 -!- Bike has joined.
01:18:18 <Sgeo> And/or was the rule in question present June 3rd?
01:20:04 <oerjan> don't recall exactly when it was amended
01:20:31 <coppro> I'm atm writing a really good judgment
01:21:55 <Sgeo> It tricked me for a moment into thinking there wasn't a bug
01:23:11 <coppro> nobody noticed until my proposal to reenact the same text
01:26:00 <Sgeo> For some reason I was thinking I didn't touch Agora since 2008, but I got involved for a bit last year
01:28:02 <oerjan> was it during the anniversary celebration?
01:29:37 <Sgeo> Around that time but unrelated to it. Was trying an Ambassador scam
01:31:02 <Sgeo> Oh, apparently Agora XX was involved in a counterscam
01:36:54 -!- boily has quit (Quit: PAIRED CHICKEN).
01:36:57 -!- metasepia has quit (Remote host closed the connection).
02:28:03 -!- Bike has quit (Ping timeout: 264 seconds).
02:32:06 <Sgeo> Erlang/Tcl comparison time: Both Erlang and Tcl have mutable objects be not automatically GCed, while some immutable objects get GCed automatically
02:34:32 -!- Bike has joined.
02:35:07 <MDude> Wait, you can still go to ancient Greek gathering places?
02:36:06 <Sgeo> MDude's name is giving me flashbacks to that M person in B
02:36:21 <oerjan> MDude: http://agoranomic.org/
02:36:43 <MDude> People are already asking me if I'm a fat guy's sense of motivation.
02:37:19 <MDude> http://www.whompcomic.com/
02:37:48 -!- Bike_ has joined.
02:38:09 <pikhq> Sgeo: Strictly speaking, Tcl has *no* GC whatsoever.
02:38:35 <Sgeo> I thought strings were GCed?
02:38:53 <pikhq> Tcl's semantics are such that there can't be cyclic references, so for simplicity's sake it reference counts instead.
02:39:55 -!- Bike has quit (Ping timeout: 240 seconds).
02:40:01 -!- Bike_ has changed nick to Bike.
02:56:10 <Sgeo> help im arguing with someone online, i don't want to be the asshole who argues with people online
02:57:29 <Bike> I t hink that you shouldn't do that, and are a bad person for doing it.
02:58:31 <Sgeo> Actually, my reluctance to argue with people who directly contradict me may be hurting me at my job
03:05:46 -!- ^v has quit (Read error: Connection reset by peer).
03:09:14 -!- ^v has joined.
03:23:06 <shachaf> copumpkin: it was _Liking What You See: A Documentary_ by Ted Chiang
03:23:23 <shachaf> I'm not sure whether the text is online.
03:23:29 <shachaf> http://www.ibooksonline.com/88/Text/liking.html exists but has terrible formatting.
03:24:27 <oerjan> it exists but you don't like what you see
03:24:49 <MDude> Sgeo: Are you arguing online with someone you work with at your job?
03:25:10 <Sgeo> Separate arguments, but technically both are online
03:25:11 <MDude> Or do you just need to pracice argue so you're a better arguer at work?
03:25:30 <Sgeo> The work one's through email, this other one's through Reddit
03:26:40 <shachaf> i asked because i thought you were ignoring my questions about it and i didn't want to be bugging you if you weren't interested
03:26:43 <shachaf> also this is a different channel
03:26:49 <copumpkin> oh, it wasn't intentional ignoring
03:26:54 <shachaf> https://docs.google.com/viewer?url=http://glacierpeak.sno.wednet.edu/teachers/bjuhl/docs/Soph%20English/Second%20Semester/Alienation,%20Tolerance,%20Cyrano/Related%20Poems,%20Articles,%20Short%20Stories,%20Etc/Liking%20What%20You%20See%20Portrait%20Version.doc might be slightly better, if more convoluted.
03:26:59 <copumpkin> I'm barely at my computer these days
03:27:10 <copumpkin> check up on it every so often, get into a chat or two and then go elsewhere
03:27:31 <shachaf> i think kmc recommended it too
03:27:36 <shachaf> he's not in this channel anymore, though
03:31:03 <oerjan> wait is he gone completely
03:33:27 <oerjan> oh well he's on freenode somewhere
03:56:32 -!- oerjan has quit (Quit: Nite).
03:57:52 <shachaf> copumpkin: what have you been doing
03:58:47 <copumpkin> hrm, working a lot, traveling to visit gf (she matched, graduated, went to china, just moved, and I did much of that with her), hanging out with work colleagues, stuff like that
03:59:33 <copumpkin> residency match program for med students
03:59:57 <copumpkin> giant algorithm matching people to hospitals they'll spend the next few years in
04:00:35 -!- drdanmaku has quit (Ping timeout: 272 seconds).
04:02:22 -!- drdanmaku has joined.
04:05:00 -!- drdanmaku has quit (Client Quit).
04:06:48 <MDude> Out of context that sounds like it might be way to decide how to beat people up very bad.
04:41:06 -!- MDude has changed nick to MDream.
04:42:18 -!- Sorella has quit (Quit: It is tiem!).
04:53:30 -!- variable has changed nick to function.
05:15:55 -!- shikhout has quit (Ping timeout: 240 seconds).
05:32:41 -!- Aetherspawn- has joined.
05:37:58 <Bike> So, in a theorem prover thingie, what exactly is a "tactic"? I swear i've heard about such things.
05:42:38 <Bike> Could you elaborate.
05:45:27 <Bike> something a silly person like me could perhaps begin to understand.
05:46:46 <elliott> a program that tries to write a proof term for a certain subset of propositions
05:46:59 <newsham> http://www.cis.upenn.edu/~bcpierce/sf/current/toc.html provides a reasonable introduction
05:47:03 <elliott> usually in some ugly turing-complete language, no real hard guarantees
05:51:24 <Bike> i wonder if i should just try going through this damn thing, i have enough books already
05:51:45 <newsham> you start of with a statement of what you want a functions type to be, and you have some other functions which can do parts of the solution for that function, giving you a simpler type (goal) to work towards
05:51:59 <newsham> its like an interactive program solver.. you nudge it along and it does a lot of the grunt work
05:52:14 <newsham> you wont have to go very far in SF before you learn what a tactic is
05:52:31 <Bike> oh, this book.
05:52:32 <newsham> the sf/current/toc.html book
05:52:54 <Bike> well, i kind of don't want to read about booleans for the billionth time. especially since i'm probably never going to use coq. you know?
05:53:17 -!- FreeFull has quit.
05:55:25 <elliott> coq doesn't really involve all that many of those
05:55:35 <newsham> sf starts out with a few boolean examples
05:55:40 <newsham> dont worry, it goes quickly from there
05:55:46 <elliott> Bike: you may like chlipala's CPDT
05:55:52 <Bike> just glancing at the table of contents, with enumerated data types
05:55:58 <elliott> it has nicer proof style than SF
05:56:01 <elliott> http://adam.chlipala.net/cpdt/
05:56:48 <Bike> Can I just ask things here?
05:57:03 <elliott> sure, if you want. I'm too tired to answer questions though.
05:57:24 <lambdabot> Local time for elliott is Thu Jun 19 06:57:23 2014
05:57:37 <Bike> well it's super basic. like, you said tactics are in some ugly imperative language, so presumably they're outside of the coq system, not written in coq?
05:57:57 <elliott> they're in a metalanguage as part of the coq system
05:58:04 <elliott> though they can also be written in ocaml, like the built-in ones are
06:01:54 <Bike> hm this "coq reference manual" which may or may not be what you just linked might be what i want
06:03:39 <Bike> sf has this as an example: "Theorem plus_O_n : ∀n : nat, 0 + n = n. Proof. intros n. reflexivity. Qed." the intros n and reflexivity are steps to do the proof? like we start with the 0 + n thing, intros n fires, that gets you something else (probably n = n), then reflexivity fires and reduces it to true?
06:04:30 <newsham> yah, "intros" and "reflexitivity" are tactics.
06:05:08 <elliott> Bike: I was joking when I called CPDT the Coq manual.
06:05:13 <elliott> it's more like the Coq manual they forgot to write.
06:05:18 <Bike> well, i am also tired.
06:05:51 <newsham> you should try to load the SF example in proof general, and step through the proof.. for each stepp it will show you what is known in the environment and what the goal is
06:06:00 <newsham> and the tactics "intros" and "reflexivity" will update those
06:06:07 <newsham> you can single step through the proof that way interactively
06:06:29 <newsham> its a shame there is no "live coq" web site that lets you do this online
06:06:31 <Bike> well, why not (besides that i haven't installed an emacs mode in so long)
06:07:27 <Bike> blugh my distro doesn't have coq in the main repos
06:07:39 <newsham> you can prob find a livecd to boot in a virtual machine
06:08:59 <Bike> elliott: yeah, it's in the AUR. not hard to install or anything, but a bit annoying
06:09:07 <Bike> and it comes with some IDE for some reason? whatever, less work maybe
06:10:21 <newsham> oh, it looks like there are some SF youtube vids
06:10:31 <newsham> maybe they would have good walktrhoughs of some proofs
06:11:17 <Bike> i'm looking at this for weird reasons nobody here would probably like
06:12:24 <newsham> the great thing about knowledge, we dont have to approve
06:15:20 <Bike> you say that now, but watch me use coq to sink california
06:21:13 <newsham> you're working for a hedge fund?
07:02:07 -!- FireFly has quit (Excess Flood).
07:03:49 -!- Effilry has joined.
07:06:43 <b_jonas> I'm hoping for something like: 3100,182,4,10001coin 10866,3582,22002,22002coin 192,1051,25,1056coin 11652,22252,23004,22002coin 8500,,4, 3001,,,coin
07:06:57 <b_jonas> 3100,182,4,10001coin 10866,3582,22002,22002coin 192,1051,25,1056coin 11652,22252,23004,22002coin 8500,,4,coin 3001,,,coin
07:23:50 -!- esowiki has joined.
07:23:54 -!- esowiki has joined.
07:23:55 -!- esowiki has joined.
07:24:46 -!- esowiki has joined.
07:24:50 -!- esowiki has joined.
07:24:50 -!- esowiki has joined.
07:25:17 -!- esowiki has joined.
07:25:21 -!- esowiki has joined.
07:25:22 -!- esowiki has joined.
07:25:48 -!- esowiki has joined.
07:25:52 -!- esowiki has joined.
07:25:53 -!- esowiki has joined.
07:26:50 -!- esowiki has joined.
07:26:54 -!- esowiki has joined.
07:26:54 -!- esowiki has joined.
07:27:21 -!- esowiki has joined.
07:27:25 -!- esowiki has joined.
07:27:26 -!- esowiki has joined.
07:27:52 -!- esowiki has joined.
07:27:56 -!- esowiki has joined.
07:27:57 -!- esowiki has joined.
07:28:25 -!- esowiki has joined.
07:28:27 -!- glogbot has joined.
07:28:27 <?unknown?> [freenode-info] please register your nickname...don't forget to auto-identify! http://freenode.net/faq.shtml#nicksetup
07:28:30 -!- esowiki has joined.
07:28:30 -!- esowiki has joined.
07:29:05 -!- realzies has joined.
07:30:38 -!- slereah_ has joined.
08:04:52 -!- password2 has joined.
08:09:35 -!- Tritonio has joined.
08:13:45 -!- password2 has quit (Ping timeout: 244 seconds).
08:15:04 -!- contrapumpkin has joined.
08:18:59 -!- copumpkin has quit (Ping timeout: 272 seconds).
08:27:26 -!- password2 has joined.
08:31:21 -!- Patashu has joined.
08:38:01 -!- Patashu_ has joined.
08:38:01 -!- Patashu has quit (Disconnected by services).
08:39:09 -!- MindlessDrone has joined.
08:45:53 -!- Patashu has joined.
08:47:36 -!- Phantom_Hoover has joined.
08:49:24 -!- Patashu_ has quit (Ping timeout: 244 seconds).
09:04:22 -!- password2 has quit (Ping timeout: 245 seconds).
09:14:02 -!- nooodl has joined.
09:33:21 -!- nooodl has quit (Quit: Ik ga weg).
09:49:58 -!- conehead has quit (Quit: Computer has gone to sleep).
10:04:16 -!- barrucad1 has changed nick to barrucadu.
10:15:40 -!- boily has joined.
10:38:06 -!- Phantom_Hoover has quit (Ping timeout: 255 seconds).
10:38:28 -!- MoALTz has joined.
11:01:23 -!- boily has quit (Quit: PLASMA CHICKEN).
11:28:52 -!- Effilry has quit (Changing host).
11:28:52 -!- Effilry has joined.
11:29:01 -!- Effilry has changed nick to FireFly.
11:34:25 -!- HackEgo has joined.
11:34:33 <HackEgo> bizobcoin pbocoin qweverpacoin rutcrtlcoin vowelcoin jumcoin kethaxcoin twositcoin fitcoin auticonformcoin jash-01coin haniacoin tediumbraincoin hunkatorecoin omecoin thestaicoin chocoin velacoin palcoin revoycoin
11:35:02 <fizzie> fungot: Couldn't you take care of your fellow bots?
11:35:03 <fungot> fizzie: so the way it does and it reports a problem on 1 exercise... 1 exercise i really dont have a clue understand his point ( because the fnord one that chances are if you never exit? that book sucks.
11:36:22 <Melvar> ( the (3 `LTE` 5) (tactics search)
11:36:24 <idris-bot> lteSucc (lteSucc (lteSucc lteZero)) : LTE 3 5
11:37:22 <Melvar> Bike: ↑ The search tactic in Idris mostly just tries constructors, which works for simple things like this.
11:58:43 <HackEgo> timensifticcoin andcoin rubicoin eodcoin poikecoin wailcoin morascoin contcoin dobeycoin quotecoin spiuntinecoin mismcoin monecoin existcoin agrtecoin boarceacoin braincoin illgaudeliumcoin factcoin tapascoin
12:01:05 -!- Sgeo has quit (Read error: Connection reset by peer).
12:18:58 -!- oerjan has joined.
12:22:22 <b_jonas> overheared coworker in meeting room saying "it's all the same because it's Turing complete"
12:24:53 <oerjan> b_jonas: just start giving him code in befunge hth
12:24:58 -!- polytone_ has changed nick to monotone.
12:32:04 <b_jonas> is funge-98 the one with bounded memory?
12:32:13 <b_jonas> or only bounded code space?
12:35:09 -!- yorick has joined.
12:35:28 <b_jonas> right, funge-98 allows arbitrary playfield dimensions,
12:39:46 <b_jonas> I wonder if my old olvashato language counts as esoteric
12:40:06 <b_jonas> it wasn't designed to be difficult to program in, so it might not count
12:41:24 <b_jonas> let me look up the official definition
12:41:45 <b_jonas> "An esoteric programming language is a computer programming language designed to experiment with weird ideas, to be hard to program in, or as a joke, rather than for practical use." -- I could argue either way
12:46:24 <elliott> http://catseye.tc/node/The_Aesthetics_of_Esolangs is my preferred vague definition of esoteric, I think
12:46:24 <oerjan> how can a language whose name means "readable" be esoteric that's absurd
12:50:18 <oerjan> also why won't ó work on google's pages in my browser
12:51:52 <oerjan> b_jonas: i corrected to funge-98 to make it clear i meant the tc variant.
12:52:12 <oerjan> or well, less un-tc. not sure if there are still some limits.
12:52:41 <elliott> funge-98 is at least as-TC-as-C, I think
12:52:43 <b_jonas> oerjan: too late to rename
12:52:50 <elliott> and has enough holes that there's probably something TC hiding in there
12:52:56 <elliott> especially with fingerprints
12:55:09 <b_jonas> oerjan: the original purpose was to make a language in which I write ugly source code, and it's compiled to readable standard ml and readable prolog code; but I sort of ran out of time and the readable part got dropped so now the compiled code is even more ugly than the original
12:55:48 <b_jonas> I might be able to make the output a bit more readable if I fix the indenting (though that's not trivial) and throw in some peep-hole beautification rules
12:56:10 <b_jonas> (it already has some of the latter, but needs more)
12:56:16 <oerjan> `addquote <b_jonas> oerjan: the original purpose was to make a language in which I write ugly source code, and it's compiled to readable standard ml and readable prolog code; but I sort of ran out of time and
12:56:17 <HackEgo> 1207) <b_jonas> oerjan: the original purpose was to make a language in which I write ugly source code, and it's compiled to readable standard ml and readable prolog code; but I sort of ran out of time and
12:56:20 <oerjan> the readable part got dropped so now the compiled code is even
12:56:22 <oerjan> more ugly than the original
12:56:40 <oerjan> bloody irssi line merging worked half-way
12:57:12 <oerjan> `addquote <b_jonas> oerjan: the original purpose was to make a language in which I write ugly source code, and it's compiled to readable standard ml and readable prolog code; but I sort of ran out of time and the readable part got dropped so now the compiled code is even more ugly than the original
12:57:13 <HackEgo> 1207) <b_jonas> oerjan: the original purpose was to make a language in which I write ugly source code, and it's compiled to readable standard ml and readable prolog code; but I sort of ran out of time and the readable part got dropped so now the compiled code is even more ugly than the original
12:57:42 <b_jonas> stuff's already here, for ages: http://www.math.bme.hu/~ambrus/pu/olvashato/
13:00:39 <oerjan> i am pretty sure using ruby to compile something into prolog and sml is blasphemic hth
13:01:46 <oerjan> because sml is the language that's supposed to be good for implementing compilers in
13:02:28 <b_jonas> what? I thought sml is supposed to be a general-purpose language with definition available only in some expensive book
13:03:10 <oerjan> well it is general purpose, but ml was _created_ for implementing other languages in
13:03:20 <oerjan> the name stands for "meta-language"
13:04:09 <oerjan> of course ocaml and haskell are also good examples, being similar in the ways that matter.
13:04:11 <slereah_> I am trying to write over some text of console, but so far nothing works D:
13:04:27 <slereah_> Neither fflush nor printf("\b") nor ncurses
13:04:55 <oerjan> hm how much has sml been hurt in recent years by being closed-documentation
13:05:43 <b_jonas> slereah_: try printf("\b\x7f") to overpunch the character with delete so the column is skipped when the tape is read back
13:06:11 <oerjan> i suspect prolog is also good to write implementations in. erlang was originally written in it?
13:06:41 <slereah_> Nope, it just writes \x7f as the unicode character 007f
13:07:22 <b_jonas> oerjan: I did consider writing an interpreter in prolog and one in sml plus only a minimal translator that translates the syntax of the program to a data structure in the input syntax of those two languages
13:07:26 -!- Patashu has quit (Ping timeout: 240 seconds).
13:07:53 <b_jonas> (such as pushes parenthesis and throws in some commas)
13:08:02 <b_jonas> but I decide it wouldn't be simpler
13:08:32 <b_jonas> and I'd likely lose points the result because it's interpreted crap
13:09:12 <slereah_> You need to use \r instead of \n in hthe text
13:10:05 <slereah_> Except now only one line displays instead of the three
13:10:09 <oerjan> b_jonas: hm it looks lispy
13:10:38 <b_jonas> oerjan: yes, in particular it's like scheme in that the head of function calls are evaluated the same as other parts
13:11:32 <b_jonas> it's common lispy in that the head of function calls is evaluated differently than the arguments
13:12:00 <b_jonas> that's why there's a primitive function |call| just like in clisp
13:12:26 <b_jonas> but the |let| builtin has a syntax different from lisps
13:14:21 <b_jonas> it's implementable as a lisp macro, but has an unnatural syntax
13:14:51 <oerjan> and here i though b_jonas was your real name
13:23:11 -!- FreeFull has joined.
13:48:33 -!- lollo64it has quit (Ping timeout: 244 seconds).
13:52:56 -!- password2 has joined.
14:16:05 -!- Sorella has joined.
14:27:58 -!- edwardk has joined.
14:37:14 -!- edwardk has quit (Quit: Computer has gone to sleep.).
14:38:42 -!- brandonson has quit (Read error: Connection reset by peer).
14:39:18 -!- brandonson has joined.
14:39:46 -!- brandonson has quit (Read error: Connection reset by peer).
14:40:06 -!- brandonson has joined.
14:42:10 -!- edwardk has joined.
15:07:55 -!- mihow has joined.
15:14:31 -!- Aetherspawn- has quit (Quit: Connection closed for inactivity).
15:34:07 -!- edwardk has quit (Quit: Computer has gone to sleep.).
15:42:03 -!- Phantom_Hoover has joined.
15:46:43 <olsner_> elliott: I don't remember going, I remember coming back
15:48:26 -!- Tritonio has quit (Ping timeout: 240 seconds).
15:53:24 -!- edwardk has joined.
15:58:17 -!- olsner_ has changed nick to olsner.
16:01:17 -!- slereah_ has quit (Quit: Leaving).
16:02:53 -!- edwardk has quit (Ping timeout: 244 seconds).
16:11:59 -!- oerjan has quit (Quit: Yay money).
16:16:10 -!- edwardk has joined.
16:20:58 -!- drdanmaku has joined.
16:54:27 -!- Tritonio has joined.
16:56:04 -!- ^v has changed nick to gabensale2014.
17:17:46 -!- mihow has quit (Quit: mihow).
17:39:24 -!- gabensale2014 has changed nick to ^0.
17:40:05 -!- lollo64it has joined.
17:43:55 -!- MDream has quit (Ping timeout: 272 seconds).
18:08:59 -!- Tritonio has quit (*.net *.split).
18:09:01 -!- edwardk has quit (*.net *.split).
18:09:02 -!- Phantom_Hoover has quit (*.net *.split).
18:09:06 -!- FreeFull has quit (*.net *.split).
18:09:09 -!- contrapumpkin has quit (*.net *.split).
18:09:17 -!- impomatic has quit (*.net *.split).
18:09:19 -!- heroux has quit (*.net *.split).
18:09:44 -!- barrucadu has quit (*.net *.split).
18:09:53 -!- hogeyui_ has quit (*.net *.split).
18:09:55 -!- lifthrasiir has quit (*.net *.split).
18:10:04 -!- idris-bot has quit (*.net *.split).
18:10:33 -!- realzies has quit (*.net *.split).
18:10:34 -!- Gregor has quit (*.net *.split).
18:10:35 -!- monotone has quit (*.net *.split).
18:10:39 -!- augur has quit (*.net *.split).
18:10:48 -!- aloril has quit (*.net *.split).
18:10:49 -!- Slereah has quit (*.net *.split).
18:10:51 -!- HackEgo has quit (*.net *.split).
18:10:58 -!- KingOfKarlsruhe has quit (*.net *.split).
18:11:09 -!- drdanmaku has quit (*.net *.split).
18:11:45 -!- b_jonas has quit (*.net *.split).
18:11:48 -!- shachaf has quit (*.net *.split).
18:11:54 -!- tromp__ has quit (*.net *.split).
18:12:14 -!- MoALTz has quit (*.net *.split).
18:12:15 -!- MindlessDrone has quit (*.net *.split).
18:12:19 -!- Bike has quit (*.net *.split).
18:12:20 -!- sebbu has quit (*.net *.split).
18:12:21 -!- Sprocklem has quit (*.net *.split).
18:12:24 -!- constant has quit (*.net *.split).
18:12:26 -!- TodPunk has quit (*.net *.split).
18:12:32 -!- Melvar has quit (*.net *.split).
18:12:47 -!- nortti has quit (*.net *.split).
18:13:05 -!- kyhwana has quit (*.net *.split).
18:13:09 -!- Burton has quit (*.net *.split).
18:13:15 -!- Taneb has quit (*.net *.split).
18:13:25 -!- ski has quit (*.net *.split).
18:13:50 -!- douglass has quit (*.net *.split).
18:13:54 -!- jix_ has quit (*.net *.split).
18:13:59 -!- diginet has quit (*.net *.split).
18:14:12 -!- ineiros has quit (*.net *.split).
18:14:14 -!- maurer has quit (*.net *.split).
18:14:16 -!- elliott has quit (*.net *.split).
18:14:16 -!- int-e has quit (*.net *.split).
18:14:18 -!- ^0 has quit (*.net *.split).
18:14:26 -!- esowiki has joined.
18:14:30 -!- esowiki has joined.
18:14:31 -!- esowiki has joined.
18:15:13 -!- esowiki has joined.
18:15:14 -!- glogbot has joined.
18:15:17 -!- esowiki has joined.
18:15:18 -!- esowiki has joined.
18:16:25 -!- mihow has joined.
18:16:26 -!- lollo64it has joined.
18:16:26 -!- brandonson has joined.
18:16:26 -!- Sorella has joined.
18:16:26 -!- 17SAAFGOG has joined.
18:16:26 -!- atehwa has joined.
18:16:26 -!- FireFly has joined.
18:16:26 -!- tromp has joined.
18:16:26 -!- coppro has joined.
18:16:26 -!- jj2baile has joined.
18:16:26 -!- myname has joined.
18:16:26 -!- erdic has joined.
18:16:26 -!- `^_^v has joined.
18:16:26 -!- vravn has joined.
18:16:26 -!- Gracenotes has joined.
18:16:26 -!- _46bit has joined.
18:16:26 -!- vyv has joined.
18:16:26 -!- mtve has joined.
18:16:26 -!- clog has joined.
18:16:26 -!- pikhq has joined.
18:16:26 -!- Speed` has joined.
18:16:26 -!- ggherdov has joined.
18:16:26 -!- newsham has joined.
18:17:33 -!- atehwa has quit (Write error: Broken pipe).
18:17:33 -!- 17SAAFGOG has quit (Write error: Broken pipe).
18:17:34 -!- jj2baile has quit (Write error: Broken pipe).
18:32:51 -!- FireFly has quit (Excess Flood).
18:33:08 -!- `^_^v has quit (Excess Flood).
18:33:13 -!- brandonson has quit (Excess Flood).
18:33:32 -!- `^_^v has joined.
18:33:59 -!- brandonson has joined.
18:34:37 -!- FireFly has joined.
19:04:32 -!- shikhin has joined.
19:12:59 -!- ^v has joined.
19:13:53 -!- ^v has quit (Client Quit).
19:31:01 -!- conehead has joined.
19:32:42 -!- Bike has quit (Ping timeout: 245 seconds).
19:34:42 -!- Bike has joined.
19:39:15 -!- MindlessDrone has quit (Quit: MindlessDrone).
19:41:54 <HackEgo> 147) <zzo38> catseye: Please wake up. Not recorded for this timezone. The big spider is not your dream \ 230) <nddrylliog> back to legal tender, that expression really makes me daydream. Like, there'd be black-market tender. Out-of-town hug shops where people exchange tenderness you've NEVER SEEN BEFORE. \ 240) <Phantom__Hoover> Gregor, yeah, but P
19:41:59 <HackEgo> 358) <olsner> as always in sweden everything goes to a fixed pattern: thursday is queueing at systembolaget to get beer and schnaps, friday is pickled herring, schnaps and dancing the frog dance around the phallos, saturday is dedicated to being hung over
19:42:46 <HackEgo> 240) <Phantom__Hoover> Gregor, yeah, but Purdue has poultry science facilities beyond the dreams of avarice.
19:44:16 <olsner> but I did the systembolaget yesterday, 5 minutes before closing when it was empty, so I neatly evaded the queueing
19:48:02 <olsner> btw, someone just pointed out that the frog dance is likely a jab at the french, imported from english derogative use of "frog" (but frog doesn't really mean that in swedish)
19:48:13 <olsner> it's also danced to a french march
19:53:03 -!- lifthrasiir has quit (Ping timeout: 240 seconds).
19:57:44 -!- mhi^ has joined.
19:59:00 <fizzie> I like the name "systembolaget".
20:02:32 <fizzie> Can't find the etymology in the (English) 'pedia.
20:02:51 -!- Bike has quit (Ping timeout: 264 seconds).
20:03:14 <fizzie> Our counterpart is just called "Alko", which is very boring.
20:04:20 -!- Bike has joined.
20:04:30 <fizzie> The Norwegian version has a refreshingly direct name. ("Vinmonopolet".)
20:05:27 <olsner> yeah, exactly what it says, it's pretty nice
20:06:53 <fizzie> "During the 1939-40 Winter War the company [Alko, or Oy Alkoholiliike Ab as it was then called] mass-produced molotov cocktails for the Finnish military, production totalling 450,000 units" heh
20:07:36 <olsner> it seems that "system" comes from http://en.wikipedia.org/wiki/Gothenburg_Public_House_System
20:10:32 -!- lifthrasiir has joined.
20:11:07 -!- MDream has joined.
20:11:07 -!- MDream has changed nick to MDude.
20:25:16 <applybot> Meta-commands: colour context help info load* restart shutdown* state timeout* undo unicode unload* \ Isabelle commands: apply by declare defer definition done find_theorems fun function lemma oops prefer primrec quickcheck term termination thm try0 typ unfolding using value
20:30:30 -!- Frooxius has joined.
20:47:57 -!- Frooxius has quit (Read error: Connection reset by peer).
20:48:52 -!- Frooxius has joined.
21:01:16 -!- Patashu has joined.
21:08:33 -!- oerjan has joined.
21:13:12 -!- nortti has changed nick to lawspeaker.
21:13:32 -!- lawspeaker has changed nick to nortti.
21:13:54 <fizzie> fungot: Prove something.
21:13:55 <fungot> fizzie: src/ ip.h or is it
21:14:16 <fungot> mroman: damn. he got that. but still patch of green where medialab extension is supposed to
21:20:13 -!- Patashu has quit (Disconnected by services).
21:20:13 -!- Patashu_ has joined.
21:27:00 -!- Patashu_ has quit (Ping timeout: 255 seconds).
21:28:43 -!- Sprocklem has quit (Quit: leaving).
21:29:00 -!- Sprocklem has joined.
21:41:52 <applybot> Loaded theories: Main "~~/src/HOL/Library/Code_Target_Nat" "~~/src/HOL/Number_Theory/Primes" \ 0 lines in session. \ Command timeout is 20 s. \ Unicode translation disabled. \ Colour output disabled.
21:42:26 <MDude> applybot: help state
21:42:26 <applybot> state: Show the state of the current proof (if there is one).
21:43:22 <MDude> applybot: help context
21:43:22 <applybot> context [N]: Show the most recent (N) lines in this session.
21:43:42 <MDude> applybot context 10
21:43:54 <MDude> applybot: context 10
21:44:21 <MDude> applybot: help term
21:44:36 <MDude> applybot: help Isabelle
21:44:50 <fungot> MDude: in the matter... things will fnord down after this week hopefully.
21:50:03 -!- boily has joined.
21:50:58 -!- metasepia has joined.
21:52:31 -!- edwardk has quit (Quit: Computer has gone to sleep.).
22:02:46 <boily> an sudden opportunity appears! b_jonas, how would you wisdomically describe yourself?
22:04:09 <HackEgo> [wiki] [[AlphaBeta]] http://esolangs.org/w/index.php?diff=39860&oldid=34593 * 188.192.76.116 * (+257) Added Lua implementation from Michael Armbruster
22:10:25 -!- nooodl has joined.
22:28:45 -!- boily has quit (Quit: INDIAN CHICKEN).
22:28:47 -!- metasepia has quit (Remote host closed the connection).
22:39:27 -!- Phantom_Hoover has quit (Ping timeout: 255 seconds).
22:42:39 -!- Phantom_Hoover has joined.
22:55:26 -!- Sgeo has joined.
23:10:13 -!- ^v has joined.
23:10:15 <MDude> Oh, metasepia has left.
23:11:36 <HackEgo> metasepia knows the weather at your nearest airport, and also something about ducks.
23:13:52 <Taneb> `learn MDude is just a dude, with an M's courage.
23:17:47 <oerjan> are you sure he's not a million dudes
23:20:04 -!- ^v has quit (Quit: http://i.imgur.com/Akc6r.gif).
23:21:33 <MDude> That would be pretty cool.
23:22:22 <Sgeo> Who was that person in B who blatantly had no idea about anything in the rules?
23:22:57 <MDude> I don't know what B is, so if I was in it I clearly had no idea.
23:23:41 <Sgeo> I think that serves as proof that MDude was that person in B
23:24:34 <MDude> It's pretty strong evidence.
23:24:42 -!- ^v has joined.
23:33:27 -!- Phantom_Hoover has quit (Ping timeout: 264 seconds).
23:37:26 -!- shikhout has joined.
23:40:12 -!- shikhin has quit (Ping timeout: 245 seconds).
23:45:14 -!- mihow has quit (Quit: mihow).
23:55:40 <oerjan> argh i now have _four_ tabs with shtetl-optimized comment threads open that i haven't managed to finish...
23:56:38 <oerjan> (even once. i sometimes go back to old ones to check for new comments.)
23:57:30 <Sgeo> Is that F# monad tutorial that doesn't say 'monad' about monads in general or just the Error monad?
23:58:03 <oerjan> it's really a thinly disguised burrito cookbook hth
23:59:18 <Sgeo> http://www.calcentral.com/~monadrailway/Monad/Welcome.html