←2016-02-23 2016-02-24 2016-02-25→ ↑2016 ↑all
00:00:23 <hppavilion[1]> Perhaps something stupid, like a rewriting system
00:00:35 <hppavilion[1]> I think it's pretty similar to the Post-Canonical System article
00:02:47 -!- p34k has quit.
00:06:11 <ais523> hmm, are there any good theorems that can be proved entirely using typed lambda calculus?
00:06:21 <izabera> define good :p
00:06:29 <vanila> ais523, well, propositional tautologies can be proved
00:06:31 <ais523> not completely trivial
00:06:39 <izabera> define trivial :p
00:06:55 <vanila> like (
00:07:00 <vanila> like (\x -> x) : P -> P
00:07:01 <ais523> I guess if you have a bottom type, then you can use the implies-and-bottom construction to create some interesting tautologies
00:07:12 <vanila> I am not sure if we would consider that a non trivial theorem
00:07:17 <ais523> like de morgan's law
00:07:23 <ais523> I'd consider de morgan's law nontrivial
00:07:24 <vanila> well you can't prove that
00:07:34 <vanila> since it's constructive logic..
00:07:47 <ais523> at least, unless both sides happen to be identical after implies-and-bottom expansion, which is possilble
00:07:52 <vanila> if you throw in some extra axiomns you can prove some cool stuff
00:07:57 <shachaf> ais523: The comonad entry is accurate (though I think people would usually say "opposite category"?).
00:08:19 <shachaf> `? monoids
00:08:21 <HackEgo> Monoids are just categories with single objects.
00:08:35 <shachaf> That one is accurate if phrased oddly.
00:09:38 <shachaf> `? vector space
00:09:39 <HackEgo> A vector space is just a module over a field.
00:09:42 <shachaf> `? preorder
00:09:43 <HackEgo> A preorder is just a small thin category.
00:09:56 <shachaf> `? partial order
00:09:58 <HackEgo> A partial order is just a small thin skeletal category.
00:10:44 <ais523> A monoidal category isn't just a category that has a monoid, though
00:11:06 <shachaf> `? monoidal category
00:11:07 <HackEgo> Monoidal categories are just 2-categories with a single object.
00:11:43 <shachaf> I guess that should say weak 2-category or something?
00:11:52 <shachaf> De Morgan's laws are good, but they're even better in linear logic.
00:12:06 <hppavilion[1]> OK, here's an example proof :http://pastebin.com/qeGzdNzb
00:12:21 <ais523> now I'm trying to work out how linear logic affects de morgan's laws
00:12:34 <hppavilion[1]> It conditionally rewrites strings
00:12:49 <shachaf> If you like duality and logic, linear logic is the place to be.
00:13:08 <ais523> well affine logic is sort-of what I specialize in
00:13:17 <ais523> although it's both a special case and a generalization of linear logic
00:14:24 <shachaf> ~(A&B) = ~A + ~B
00:14:33 <hppavilion[1]> I think this is pretty much just post-canonical systems
00:14:39 <shachaf> ~(A x B) = ~A # ~B
00:14:48 -!- lynn has quit (Ping timeout: 244 seconds).
00:15:01 <ais523> shachaf: ooh, a full linear logic version
00:15:05 <ais523> how do you define not, though?
00:15:10 <hppavilion[1]> But it's still cool
00:15:14 <shachaf> Isn't it built-in?
00:15:22 <hppavilion[1]> Especially that I'm managing to do math using IRC slang
00:15:30 <shachaf> Usually written as A^_|_
00:15:49 <shachaf> ~(!A) = ?(~A)
00:15:54 -!- lynn has joined.
00:15:59 <vanila> ais523, linear logic is nice
00:16:05 <shachaf> https://en.wikipedia.org/wiki/Linear_logic#Connectives.2C_duality.2C_and_polarity
00:16:23 <ais523> shachaf: you can build a huge number of things into linear logic
00:16:29 <ais523> but that doesn't necessarily mean they're useful for programming
00:16:53 <ais523> I don't think I've seen anyone seriously use ?, for example
00:16:53 <vanila> it was difficult to integrate dependent types with linear logic
00:17:04 <shachaf> You can define (~A) as (A -o _|_)
00:18:05 <ais523> hmm, now I'm going to esointerpret that as "using A exactly once, you can create an infinite loop"
00:18:52 <shachaf> And of course ((A -o _|_) -o _|_) = A
00:21:15 <ais523> hmm, ~~A is not equivalent to A in some logics
00:21:59 <shachaf> Yes, e.g. intuitionistic logic.
00:22:15 <vanila> is it true in linear logic?
00:22:20 <shachaf> Because intuitionstic (A -> B) can be encoded as (!A -o B)
00:22:51 <shachaf> So it's something like !(!A -o _|_) -o _|_
00:23:31 <shachaf> = ~(!(~(!A))) = ?(~~(!A)) = ?(!A)
00:23:33 <shachaf> What's that?
00:26:42 -!- lynn_ has joined.
00:29:16 -!- lynn has quit (Ping timeout: 244 seconds).
00:30:11 <hppavilion[1]> vanila: What do you think of the idea of a proof esossistant?
00:30:29 <vanila> lol
00:32:39 <hppavilion[1]> vanila: No, really
00:36:55 <hppavilion[1]> vanila: Its only data types are strings (constant axioms), s/// expressions (substitution axioms), and composed s/// expressions (lemmas/theorems)
00:37:19 <hppavilion[1]> http://pastebin.com/Ax2v5XSV is the example (that one is the earlier one (or an edit thereof) posted under my actual account)
00:37:37 <boily> isn't that akin to SKI?
00:37:52 <hppavilion[1]> boily: It might be, but it's closer to post-canonical systems
00:37:59 <hppavilion[1]> boily: How so?
00:38:57 <hppavilion[1]> boily: Wait, was that not directed at me?
00:42:40 <boily> yes, it was.
00:42:44 <hppavilion[1]> OK
00:42:55 <hppavilion[1]> boily: How is it like SKI then exactly?
00:43:05 <boily> I was reminded of the applicative instance of ((->) r), where <*> is S.
00:43:08 <hppavilion[1]> It can maybe be proved TC by reduction ot SKI
00:43:30 <hppavilion[1]> boily: You have completely lost me
00:45:11 <boily> composition of substitutions should be the same as composition of s///es.
00:45:15 <boily> I guess.
00:45:25 <boily> well, I highly doubt, but I still guess so.
00:45:55 <hppavilion[1]> boily: Yep, that's the idea
00:46:24 <hppavilion[1]> boily: In fact, composition of s///es is literally just applying each individual substitution
00:46:55 <hppavilion[1]> boily: In the example, the main block is a theorem (well, a proof)
00:47:15 <hppavilion[1]> (once you have a proof, you can call it to form a theorem)
00:48:11 <hppavilion[1]> boily: It's a little bit imperative ATM, but I will soon fix that
00:48:49 <hppavilion[1]> I think I am going to fix it with the @ operator, which applies a lemma/theorem or axiom until it stops changing the string
00:51:19 <hppavilion[1]> Which means that the language reduces trivially to Thue, and is thus TC
01:09:24 -!- lambda-11235 has joined.
01:13:45 <Taneb> I heard of something terrifying today
01:13:49 <Taneb> Continuous pi calculus
01:14:06 <hppavilion[1]> practical Unlambda?
01:14:38 <boily> Tanelle. why is it terrifying?
01:15:06 <Taneb> boily, possibly the way it was described to me, which I can't really do justice to
01:15:25 -!- lynn_ has quit (Ping timeout: 255 seconds).
01:24:49 <ais523> the concept does seem terrifying, also I can't figure out how it would work
01:25:17 <vanila> as opposed to the friendly and warm: everywhere discontinuous pi calculus
01:25:38 -!- bb010g has joined.
01:25:48 <\oren\> I am a genious!
01:25:53 <\oren\> http://postimg.org/image/x9uo6lgmf/
01:26:33 -!- vanila has quit (Quit: Leaving).
01:29:32 <boily> he\\oren\. happily kerbaling?
01:33:21 <Taneb> ais523, apparently it's used by some biologists???
01:38:00 <hppavilion[1]> \oren\: My god, what OS is that?
01:38:04 <hppavilion[1]> Oh wait, probably a Linux
01:38:14 <hppavilion[1]> (The windowing looks pretty bad IMNSHO)
01:38:45 <hppavilion[1]> Taneb: How, may I ask?
01:40:48 <hppavilion[1]> I did not realize biology involved math...
01:42:59 <boily> maybe Windows 2000?
01:43:09 <ais523> hppavilion[1]: there's a lot of statistics in biology
01:43:12 <Taneb> hppavilion[1], it wasn't made clear
01:43:24 <Taneb> hppavilion[1], there's a lot of statistics and informatics
01:43:42 <hppavilion[1]> ais523: Yes, I figured there WAS math (that was a joke)
01:43:42 <ais523> hppavilion[1]: those are very Windows close/maximize/minimize buttons, but maybe they've just been made to look the same as Windows
01:43:56 <ais523> is informatics maths, technically?
01:43:56 <hppavilion[1]> ais523: Yes, that's what I was thinking
01:44:04 <boily> hppavilion[1]: when I was in university submitting stuff on the supercomputer we had, many users were bio-computer-science students.
01:44:25 <hppavilion[1]> boily: I would think that that was the "computer" and not the "bio" part
01:46:50 <hppavilion[1]> boily: So does Thoof look promising?
01:46:55 <hppavilion[1]> (or anybody else)
01:47:08 <boily> it sounds good.
01:47:31 <hppavilion[1]> Yay!
01:47:52 <shachaf> Classical (A -> B) is encoded as (!A -o ?B)
01:48:09 <shachaf> So !(!A -o ?_|_) -o ?_|_ should be the same as A?
01:48:13 <shachaf> What's ?_|_ ?
02:01:15 <boily> hellochaf. a very confused bottom.
02:05:00 <hppavilion[1]> Obviously, normal regex does not let you detect matched brackets
02:05:20 <hppavilion[1]> However, I have a nagging feeling this is possible using the horribly mutated Perl-style regex
02:05:22 <hppavilion[1]> Is this so?
02:06:11 <hppavilion[1]> Perhaps using backreference?
02:07:21 <FireFly> Perl & PCRE support recursive patterns, so yes
02:07:25 <boily> PCRE isn't horrible.
02:07:39 <boily> it has its own interior beauty.
02:10:39 <hppavilion[1]> Yes!
02:10:42 <hppavilion[1]> The lexer works!
02:10:51 <hppavilion[1]> boily: Oh, it isn't?
02:11:03 <hppavilion[1]> boily: Sorry, can't keep track of what we do and do not hate
02:11:41 <hppavilion[1]> FireFly: Is it equivalent to a PDA?
02:11:52 <hppavilion[1]> Or equivalently, BNF (now known as F)?
02:12:25 <FireFly> I think it could do some non-PDA things
02:12:40 <hppavilion[1]> Oh, wow
02:12:42 <hppavilion[1]> Impressive
02:12:48 <FireFly> perhaps
02:12:56 <FireFly> also pretty bad, depends on the application
02:13:06 <FireFly> something about great power and great responsibility
02:16:05 <ais523> hppavilion[1]: "(a*)b\1b\1" is a legal Perl/PCRE regex (even POSIX if you change the syntax slightly) that can't be matched by a PDA
02:16:30 <hppavilion[1]> Interesting.
02:16:34 <ais523> OTOH, Perl/PCRE regexes are I believe sub-TC unless you embed code in different languages inside them
02:16:49 <ais523> it's either going to be LBA or some weird class
02:20:54 -!- boily has quit (Quit: THINKING CHICKEN).
02:21:24 <hppavilion[1]> ais523: The proof assistant is TC by reduction to thue, so the regexes themselves need not be TC; AFAIC, they can just be literal string matching
02:21:35 <hppavilion[1]> But I'm allowing regexes because I am a kind and merciful god
02:21:41 <ais523> hppavilion[1]: well, if you know that something's above-PDA
02:21:50 <ais523> what computational class it actually has is an interesting question
02:23:16 -!- Phantom_Hoover has quit (Read error: Connection reset by peer).
02:27:12 -!- mihow has quit (Quit: mihow).
02:55:25 <quintopia> sup ais523
02:55:49 <ais523> hi quintopia
03:01:06 <quintopia> there is a question i want to ask but i dont know how to ensure it has only interesting answers
03:01:43 <ais523> assuming you want to ask us, you could just ask us not to give the boring answers, or let us give the boring answers first to get them out of the way and then start thinking
03:02:43 <quintopia> basically i want to define halting in such a way that it encapsulates all the usual connotations of halting
03:03:56 <ais523> oh, ouch
03:03:59 <quintopia> without specifying a specific "halt state"--just the idea that there is a state, perhaps not being explicitly tracked, after which nothing matters
03:04:09 <ais523> if I was capable of making that sort of definition I'd have at least one more paper than I have at the moment, probably two
03:04:16 <ais523> this is the thing that's holding up the 2,3 Turing machine definition
03:04:32 <ais523> err, 2,3 Turing machine paper
03:04:56 <ais523> not so much the "what counts as halting" (I found a nice construction for that where we get the Turing head to fall off the end of the tape), but what counts as a legal initial condition
03:05:16 <ais523> but it's basically the same problem, to determine what sort of description is legitimate and what sort of description is so complex it can "steal the TCness" by itself
03:07:19 <quintopia> im not worried about TCness, though I am aware of what you're referring to and the controversy around it.
03:07:46 <quintopia> i'm more interested in non-TC systems that are still very powerful
03:08:19 <ais523> hmm, well if the system /is/ TC, an interesting definition of halting would be "the point at which the evolution of the system can be fully predicted by a sub-TC system"
03:09:51 <quintopia> hmm. yeah that would be easy. however, it wont do if you choose to define sub-TC as "halting is decidable"
03:10:06 <quintopia> it would be circular
03:10:09 <ais523> indeed
03:10:17 <ais523> also, not just circular, but also incorrect
03:10:54 <quintopia> yes
03:12:23 <quintopia> but yeah i want to look at the space of systems for which halting is decidable
03:12:40 <quintopia> and to do that i need to know what halting is
03:12:59 <ais523> I think this is basically the same problem as the initial condition problem
03:13:01 <hppavilion[1]> YES!
03:13:04 <hppavilion[1]> THOOF WORKS!
03:13:22 <ais523> definitely halted: a state in which nothing happens from then on (e.g. actually terminating the interpreter, an infinite loop with no changes)
03:13:35 <hppavilion[1]> Wait, not quite, probably
03:13:38 <ais523> next simplest is a loop in which everything repeats exactly
03:14:10 <ais523> next simplest is a state in which things aren't repeating exactly but the pattern is really obvious and can be generated via a very simple automaton (e.g. the 101101110111101111101111110 pattern that was discussed during the 2,3 stuff)
03:14:12 <ais523> and so on
03:16:35 <quintopia> perhaps the only acceptable universally definition is "can be modeled by a TM in which the state in question maps to an explicit halt state.
03:16:49 <quintopia> i'm allowed to go up to TMs after all, yes?
03:17:05 <ais523> you will have problems defining "modeled"
03:17:17 <quintopia> oof
03:17:28 <ais523> if you go all the way up to bisimulation, the least contentious definition, you'll notice that the TM now has to be sub-TC because it can't do anything that the lower level couldn't do
03:17:54 <quintopia> and if i dont?
03:18:20 <ais523> then you're using a more contentious definition, and I can't think of any that would work here offhand
03:18:24 <ais523> although it's possible that there is one
03:18:42 <ais523> this is basically what I did in the 2,3 proof that I submitted to the wolfram people and that won me the prize
03:19:04 <ais523> showing that the 2,3 machine was modelling a Turing machine, thus the complexity of the initial condition didn't matter because you could look at the internals to prove I wasn't cheating
03:19:18 <ais523> but the whole thing was more subjective than most mathematicians want
03:21:44 <quintopia> what's wrong with just implementing the subTC system in a UTM, but having the implementation "know" when the system has halted even if the system itself doesnt?
03:23:07 <quintopia> for systems with an I/O mechanism (even if its just a "this state is interesting" flag) this is easy
03:23:10 <ais523> because you can run an entire TC program while checking whether the system has halted or not, and use its haltingness to choose when to declare "halted", which is basically cheating but the definition has no obvious way to catch the cheating
03:24:06 <hppavilion[1]> OK, now it works
03:24:46 <hppavilion[1]> Anybody feel like proving anything in it? xD
03:25:19 <quintopia> oh i guess its pretty circular
03:25:41 <quintopia> hppavilion[1]: no idea what uou're talking about
03:25:59 <hppavilion[1]> quintopia: I made a proof assistant based on regexy Thue called Thoof
03:26:08 <hppavilion[1]> quintopia: It's more of a programming language, but it works
03:26:16 <quintopia> lul
03:26:36 <quintopia> provide a demo
03:26:46 <hppavilion[1]> quintopia: You set up the axioms (which are s/// expressions and assumed-to-exist strings, really) then apply them until you get your goal
03:26:49 <hppavilion[1]> quintopia: OK
03:26:54 <quintopia> prove that 5+5=10
03:26:59 <hppavilion[1]> quintopia: It's TC by reduction to thue using the @ operator
03:27:18 <hppavilion[1]> quintopia: It's stringier than numerical, really, but that could certainly be done if we allow binary
03:27:40 <quintopia> hppavilion[1]: just use the peano axioms
03:28:01 <hppavilion[1]> quintopia: Here's the demo: http://pastebin.com/Ax2v5XSV
03:28:23 <hppavilion[1]> quintopia: Keep in mind, this is basically Thue with regexes and more fine-grained control
03:28:45 <hppavilion[1]> quintopia: There aren't built-in strings or anything
03:29:31 <quintopia> its pretty clear from the demo
03:29:59 <hppavilion[1]> quintopia: Great. Did I do something horribly wrong in my design?
03:30:15 <hppavilion[1]> Wait, not, "there aren't built-in strings"
03:30:25 <hppavilion[1]> I mean "there are ONLY built-in strings"
03:31:11 <quintopia> define ADD as the regex that turns S<a> + <b> into <a> + S<b>
03:31:23 <quintopia> define 5 as SSSSS0
03:31:37 <quintopia> and 10 as SSSSSSSSSS0
03:31:37 <hppavilion[1]> quintopia: Yep, that was the plan
03:32:50 <hppavilion[1]> quintopia: I was planning to use the thue incrementer, though
03:34:19 -!- oerjan has joined.
03:43:15 <oerjan> boo
03:43:18 <oerjan> nope
03:44:42 <izabera> https://esolangs.org/wiki/--C-=C-C-- why is this tc?
03:46:02 <oerjan> it doesn't looked well defined enough to say.
03:46:06 <oerjan> *look
03:46:57 -!- perrier_ has joined.
03:47:35 <ais523> well C isn't turing complete without file I/O or something similar
03:47:46 <ais523> however, removing features may make it more TC by undisallowing bignums/unlimited malloc
03:47:54 <oerjan> izabera: the author of that was a bit of a troublemaker afair
03:48:04 <oerjan> so don't expect anything to make real sense.
03:48:09 <ais523> it appears to be assigning integers to voids, so presumably it doesn't follow the rules of C exactly
03:48:44 <ais523> izabera: read the Talk page, this discussion's apparently come up before
03:49:17 <izabera> ah thanks
03:49:18 -!- perrier_ has quit (Remote host closed the connection).
03:49:56 <ais523> spoilers: pretty much everyone agrees with you
03:50:34 -!- pelegreno has joined.
03:51:54 <oerjan> ehird even blocked em at one point
03:54:09 <oerjan> that was when e was trying to fill in Unicode with a bot, i think.
03:54:25 <shachaf> ais523: Do you know what ?_|_ is?
03:55:02 <quintopia> bottom?
03:55:16 <oerjan> huh that page was created by User:Elliott
03:55:22 <ais523> shachaf: with the question mark, no
03:55:40 <shachaf> Hmm, maybe I can use Chu spaces to find out.
03:55:58 <quintopia> some thing a functor to tell whether a thing is bottom?
03:56:18 <shachaf> http://chu.stanford.edu/live/ says that _|_ is [[0],[1]] and that ?_|_ is [[1],[0]]
03:56:35 <quintopia> huh
03:57:01 <oerjan> hm that may or may not be the same person as ehird, no time overlap
03:57:09 <shachaf> Are those even different?
03:57:31 -!- hppavilion[2] has joined.
03:57:31 -!- hppavilion[1] has quit (Ping timeout: 244 seconds).
03:58:02 -!- pelegreno has quit (Remote host closed the connection).
03:58:58 <shachaf> This Java applet isn't that great.
03:59:14 -!- pelegreno has joined.
04:01:19 <izabera> so uhm
04:01:26 <izabera> i have this idea for a language
04:01:37 <izabera> i like the ones that use the filesystem
04:01:45 <izabera> but none of them seems to use symlinks
04:02:02 <izabera> and they could be used as an obvious way to loop and jump
04:02:21 <ais523> I don't think the existing ones have been designed in a way that takes the medium into account
04:02:31 <ais523> symlinks for control flow are an obvious improvement
04:02:41 <izabera> good
04:02:44 <izabera> let's do this
04:03:10 <izabera> ok so a directory is the equivalent of { }
04:03:14 <izabera> symlinks are jumps
04:03:40 <izabera> what does the memory look like? a tape? a stack? random variables?
04:03:40 <ais523> well, filesystems are typically unordered
04:03:54 <ais523> thus you shouldn't be taking advantage of the order of elements inside a directory
04:04:05 <izabera> that's not a problem, you can just call the files 1 2 3 4 5
04:04:06 <ais523> my first thought here is "is it somehow possible to use the path as memory?"
04:04:18 <izabera> uhm not sure
04:04:31 <ais523> like, with symlinks, a/a/b/a/b and a/b/b could be the same file
04:04:42 <ais523> so you have infinite storage there, although probably only accessible in a PDA way
04:04:49 <ais523> and you can put ../ in a symlink
04:06:07 <ais523> I like to start by looking at the implications of the simplest thing that could possibly work
04:06:26 <izabera> what would it be?
04:06:54 <ais523> in this case, each directory can contain either a) other directories; b) symlinks elsewhere; and c) a file with a specific name (say "run.sh") which just says "cd " followed by a directory name
04:07:13 <izabera> meh no like it
04:07:15 <ais523> you just repeatedly change directory as indicated by this directory's where-to-go-next
04:07:26 <ais523> the question is, is this PDA-complete? I suspect it might be
04:07:36 <ais523> could be worth trying to compile Splinter into it
04:08:45 <izabera> reading on splinter
04:09:04 <hppavilion[2]> Ugh
04:09:07 <hppavilion[2]> getting a weird bug
04:09:09 <ais523> it's my favourite PDA
04:09:37 <hppavilion[2]> Pretty sure it's with the interpreter, not the proof, but that's always a possibility
04:09:50 <ais523> actually I'm not sure if this folder thing is a PDA, I can't see an obvious way to copy state "upwards" from lower stack elements
04:09:56 <ais523> but that doesn't mean there isn't a non-obvious one
04:09:59 -!- FreeFull has quit (Ping timeout: 240 seconds).
04:15:36 <ais523> oh, it's a PDA, but in a rather spammy way; you use a different directory name for each possible mapping of splinters to literal code blocks, which is an incredibly large number, but finite
04:15:42 <ais523> then you just make a PDA stack out of that directly
04:15:51 <ais523> so it's a PDA but not one it's interesting to program in
04:20:11 -!- hppavilion[2] has changed nick to hppavilion[1].
04:24:00 <oerjan> borelang
04:25:58 <hppavilion[1]> Ugh, now I have to figure out how to have multiple strings in one environment
04:26:05 <hppavilion[1]> Probably should've thought of this
04:26:48 <oerjan> hppavilion[1]: just braid them together hth
04:27:30 <hppavilion[1]> oerjan: Yes, good point.
04:27:35 <hppavilion[1]> 100% valid and usefu
04:27:36 <hppavilion[1]> l
04:27:58 <oerjan> of course. that's what hth means, after all.
04:28:41 <oerjan> that's actually a valid way of combining two natural numbers. just write them in the same base and interleave.
04:29:17 <ais523> oerjan: that's the easiest way to prove that Z²=Z or R²=R
04:29:51 <hppavilion[1]> oerjan: Try it with 1000000000000000000000 and 5
04:30:34 <oerjan> ais523: i don't think it works as straightforwardly for those as for N
04:31:03 <oerjan> for the first you need to consider sign, for the second you get the .9999... = 1.0000... problem
04:31:12 <ais523> oh, handling the sign bit is a little tricky, you can treat it as a separate digit
04:31:33 <oerjan> i suppose it's easy enough in binary.
04:31:38 <ais523> the 9 recurring problem is something I hadn't thought of though
04:31:49 <shachaf> The reals are a very different thing from the cantor set.
04:31:59 <ais523> shachaf: same cardinality though
04:32:24 <shachaf> Well, if you have an isomorphism there then your job is easy.
04:32:35 <shachaf> Bijection, that's what it's called.
04:33:02 <oerjan> you could apply schröder-bernstein, then you just need injections first
04:33:58 <ais523> is that the theorem that says two sets are equivalent if they inject both ways?
04:34:05 <ais523> I've known that one for ages but didn't realise it had a name
04:34:10 <oerjan> yes
04:34:32 <oerjan> it's pretty neat
04:35:14 <ais523> it's a good example of why infinity depresses and confuses me
04:35:37 <ais523> because it's the sort of thing that should be really obvious with any normal (i.e. finite) set
04:35:59 <ais523> x ≤ y, y ≤ x, you'd think that x = y
04:36:16 <ais523> and turns out it is but you need a theorem to prove it :-(
04:38:31 <shachaf> "you need a theorem to prove it" is an odd thing to say.
04:38:48 <shachaf> You need a theorem to prove anything.
04:40:40 <ais523> I mean, that it's non-obvious enough that it's a theorem, with a name
04:40:46 <ais523> *that it's called a theorem
04:40:49 <ais523> rather than people just using it
04:41:07 <ais523> I doin't think there's a name for the fact that x ≥ y && y ≥ x implies x = y on the integers
04:41:22 <ais523> it's true but if you have to use it in a proof, you just assume it's true and that the reader will find it obvious
04:41:25 <shachaf> Antisymmetry?
04:41:26 <ais523> you don't give it a name and a citation
04:41:41 <ais523> antisymmetry is the name of the property that ≥ has that makes that happen
04:41:51 <ais523> "≥ is antisymmetric" I guess is the theorem/fact
04:42:01 <ais523> but you rarely express it in those terms
04:43:03 <ais523> hmm, actually this is true for arbitrary join-semilattices; a ≥ b means "join(a, b) = b"; thus a ≥ b && b ≥ a means b = join(a, b) = a
04:43:18 <ais523> (and it's true for arbitrary meet-semilattices for the same reason, just need a different definition of ≥ in terms of meets)
04:43:39 <shachaf> Yes, a semilattice is partially ordered.
04:44:11 <shachaf> Though a semilattice-type thing for preorders would be fine too.
04:44:23 <shachaf> Joins/meets would just not be unique.
04:47:44 <ais523> hmm, this is a slightly different concept from the "partial order" I'm used to
04:47:56 <ais523> a partial order, if you compare two things you get less than, equal, or greater
04:48:04 <ais523> whereas with a semilattice, you get less than, equal, greater, or incomparable
04:48:12 <ais523> just like with a preorder
04:48:17 <shachaf> Are you thinking of a total order?
04:48:19 <ais523> the difference is that meets /are/ unique
04:48:34 <ais523> shachaf: I'm thinking of something along the lines of a < b < (c = d = e) < f
04:48:44 <ais523> whereas a total would be a < b < c < d < e <f
04:49:06 <oerjan> partial order has incomparable too
04:49:12 <ais523> and a preorder as being any cycle-free directed graph (a partial preorder can have cycles)
04:49:22 <ais523> oerjan: hmm
04:49:50 <ais523> how do you disallow things like a < b, a < c, b < d, b < e, c < d, c < e, + transitive closure, but no other < relationships?
04:50:07 <ais523> because that doesn't have unique meets
04:51:55 <oerjan> well that's a partial order
04:51:57 <shachaf> Disallow what about it?
04:52:09 <shachaf> It's a partial order which isn't a semilattice.
04:53:17 <ais523> so what's a preorder that isn't a partial order?
04:53:19 <shachaf> https://chart.googleapis.com/chart?chl=digraph+%7B+a+-%3E+b%3B+a+-%3E+c%3B+b+-%3E+d%3B+b+-%3E+e%3B+c+-%3E+d%3B+c+-%3E+e%3B+%7D&cht=gv hth
04:53:41 <oerjan> ais523: a <= b, b <= a, a != b
04:53:42 <shachaf> Er, that's not an answer to your question, it's just your poset rendered.
04:53:42 <ais523> also, is that just a web interface to dot?
04:53:48 <shachaf> Yes.
04:53:57 <shachaf> And what oerjan said.
04:54:20 <ais523> oh, so a preorder can have cycles, but requires a <= or => opinion on any two elements?
04:54:34 <oerjan> yes, no
04:54:53 <oerjan> just add an uncomparable c if you like
04:54:57 <ais523> is it actually just a directed graph?
04:55:08 <shachaf> It's reflexive and transitive.
04:55:12 <ais523> right
04:55:36 <shachaf> `? preorder
04:55:37 <HackEgo> A preorder is just a small thin category.
04:55:59 <shachaf> ("thin" means that for any pair of objects (A,B) there's at most one arrow : A -> B.)
04:56:20 <ais523> and small means that it's not sufficiently infinite to make set theory cry
04:56:40 <shachaf> Right.
04:57:06 <shachaf> In topological terms, a partial order is like a T0 space.
04:57:21 <shachaf> Any two points are distinguishable.
04:58:00 * oerjan has been going to this "italian" restaurant and now has a https://www.youtube.com/watch?v=RruDYGIx1Ak earworm
04:58:26 <prooftechnique> Ear poison
04:58:58 <prooftechnique> `? postorder
04:58:59 <HackEgo> postorder? ¯\(°​_o)/¯
04:59:01 <prooftechnique> Good
05:00:01 <oerjan> `learn Postorder is the same as Polish notation, since Post was Polish. Not to be confused with reverse Polish notation.
05:00:05 <HackEgo> Learned 'postorder': Postorder is the same as Polish notation, since Post was Polish. Not to be confused with reverse Polish notation.
05:00:23 <prooftechnique> I was expecting a big fat category
05:00:45 <oerjan> `learn Postorder is the same as Polish notation, since Post was Polish. Not to be confused with reverse Polish notation, which puts operations last.
05:00:47 <HackEgo> Learned 'postorder': Postorder is the same as Polish notation, since Post was Polish. Not to be confused with reverse Polish notation, which puts operations last.
05:01:37 <shachaf> oerjan: Reverse Polish notation is what you get when you do a postorder traversal of a tree representing an arithmetic expression.
05:02:12 <oerjan> `learn Postorder is the same as Polish notation, since Post was Polish. Not to be confused with reverse Polish notation, which is postfix.
05:02:14 <HackEgo> Learned 'postorder': Postorder is the same as Polish notation, since Post was Polish. Not to be confused with reverse Polish notation, which is postfix.
05:03:15 -!- tromp_ has joined.
05:03:49 -!- andrew has joined.
05:11:57 <oerjan> `? !
05:12:07 <HackEgo> ​/hackenv/bin/?: 5: [: closing paren expected \ !? ¯\(°​_o)/¯
05:12:14 <oerjan> ooh
05:12:25 <oerjan> `? hm!
05:12:27 <HackEgo> hm!? ¯\(°​_o)/¯
05:12:39 <oerjan> `test !
05:12:40 <HackEgo> No output.
05:12:48 <oerjan> `cat bin/?
05:12:49 <HackEgo> ​#!/bin/sh \ topic=$(echo "$1" | lowercase | sed "s/noo\+dl/nooodl/;s/ *$//") \ topic1=$(echo "$topic" | sed "s/s$//") \ cd wisdom \ if [ \( "$topic1" = "ngevd" \) -a \( -e ngevd \) ]; \ then cat /dev/urandom; \ elif [ -e "$topic" ]; \ then cat "$topic" | rnooodl; \ elif [ -e "$topic1" ]; \ then cat "$topic1" | rnooodl; \
05:13:28 <oerjan> `cat wisdom/!
05:13:29 <HackEgo> cat: wisdom/!: No such file or directory
05:13:43 -!- jaboja has joined.
05:13:53 <oerjan> `? !test
05:13:54 <HackEgo> ​!test? ¯\(°​_o)/¯
05:14:00 <oerjan> `? !
05:14:01 <HackEgo> ​/hackenv/bin/?: 5: [: closing paren expected \ !? ¯\(°​_o)/¯
05:14:08 <oerjan> weird
05:14:13 <ais523> hmm, this site I've had open for a couple of hours suddenly started playing music, presumably through an advert
05:14:16 <oerjan> `? !!
05:14:17 <HackEgo> ​!!? ¯\(°​_o)/¯
05:14:26 <ais523> so first I muted my speakers, then looked through the site's HTML for ad containers and deleted them all
05:14:52 <ais523> ugh, some of them have come back
05:15:07 <oerjan> oh is it the if test
05:15:25 <ais523> oerjan: it's clearly test misinterpreting ! as an operator rather than an operand
05:15:26 <ais523> `? -le
05:15:27 <HackEgo> ​-le? ¯\(°​_o)/¯
05:15:30 <ais523> hmm
05:15:32 <ais523> `? -gt
05:15:33 <HackEgo> ​-gt? ¯\(°​_o)/¯
05:15:47 <ais523> presumably that looks like an operand because it would be a binary operator and there's nothing before it
05:16:02 <oerjan> yeah
05:26:47 <shachaf> So in Chu(Set, 2), 1 is the singleton set, with one point and two opens.
05:27:10 <shachaf> And _|_ is the dual (the CABA corresponding to the singleton set?), with two points and one open.
05:27:53 <shachaf> "The operation ?A is the De Morgan dual of !A, defined by ?A = (!(A^_|_))^_|_. Just as !A weakens A to a poset (when K=2), ?A dually strengthens A to a distributive lattice, the dual notion to a poset."
05:27:56 -!- tromp_ has quit (Remote host closed the connection).
05:29:07 <shachaf> So ?_|_ should be the transpose of !1
05:29:30 <shachaf> "As our next linear logic connective we consider the unary operation !A. For finite Chu spaces over K = 2, !A yields the underlying partial order of A. This has the same points as A, which are taken to be ordered in such a way that a <= b just when it this is true in every column. Thus we have 001 <= 101 but not 010 <= 101.
05:29:35 <shachaf> The states of !A, still for K = 2, turn out to be definable as the closure under union and intersection of the states of A, together with the constantly 0 and constantly 1 states. An equivalent characterization of these states is that they are all those states that are consistent with the above partial order on A: any additional state would contradict some a <= b."
05:31:18 <shachaf> (open = state)
05:33:12 <shachaf> Wouldn't !1 be 1?
05:34:15 <ais523> if 1 is unit, then I'd expect it to be
05:43:01 <shachaf> But if ?_|_ = _|_, then !(!A -o ?_|_) -o ?_|_ = !(!A -o _|_) -o _|_
05:43:11 <shachaf> So it works out the same as intuitionistic logic.
05:43:29 <oerjan> oh hm
05:43:45 <shachaf> But maybe ?!A has the same behavior as A when your implications all look like !A -o ?B ?
05:44:03 <oerjan> `` sed -i '1c#!/bin/bash' bin/\?
05:44:17 <HackEgo> No output.
05:44:21 <ais523> was it previously using sh?
05:44:26 <oerjan> `cat bin/?
05:44:26 <HackEgo> ​#!/bin/bash \ topic=$(echo "$1" | lowercase | sed "s/noo\+dl/nooodl/;s/ *$//") \ topic1=$(echo "$topic" | sed "s/s$//") \ cd wisdom \ if [ \( "$topic1" = "ngevd" \) -a \( -e ngevd \) ]; \ then cat /dev/urandom; \ elif [ -e "$topic" ]; \ then cat "$topic" | rnooodl; \ elif [ -e "$topic1" ]; \ then cat "$topic1" | rnooodl; \
05:44:27 <oerjan> yes
05:44:33 <oerjan> `? !
05:44:33 <HackEgo> ​/hackenv/bin/?: line 5: [: `)' expected, found ngevd \ !? ¯\(°​_o)/¯
05:44:44 <oerjan> well not that it helped enough
05:44:48 <oerjan> `? ngevd
05:44:50 <HackEgo> ​֍UH<{ͅ`h;/|}niGf.fE6皸>pavtr^=F,``4^I&ĝ\.5ŏDs:>`oEC/ޟ2@2wO𠐒`h|0@tйli)7TDKɰ\U}"zZ$? 䜟
05:44:57 * oerjan whistles innocently
05:45:05 <oerjan> `? hmph
05:45:07 <HackEgo> His Master's Phonetic Hmph
05:46:00 <shachaf> `` hg log bin\? | grep summary:
05:46:03 <HackEgo> No output.
05:46:09 <shachaf> er
05:46:12 <shachaf> `` hg log bin/\? | grep summary:
05:46:15 <HackEgo> summary: <oerjan> ` sed -i \'1c#!/bin/bash\' bin/\\? \ summary: <tswett> revert \ summary: <oerjan> revert \ summary: <elliott> revert 1 \ summary: <shachaf> sed -i \'2s/no/noo/\' bin/\\? \ summary: <oerjan> sed -i \'2s!s/!s/no\\\\+dl/nooodl/;s/!\' bin/\'?\' \ summary: <oerjan> revert \ summary: <oerjan> sed -i \'2s!
05:46:42 <shachaf> `` hg wells
05:46:45 <HackEgo> hg: unknown command 'wells' \ Mercurial Distributed SCM \ \ basic commands: \ \ add add the specified files on the next commit \ annotate show changeset information by line for each file \ clone make a copy of an existing repository \ commit commit the specified files or all outstanding changes \ diff diff reposi
05:48:21 <oerjan> `` sed -i '5s/"/"_/g' bin/\?
05:48:23 <HackEgo> No output.
05:48:27 <oerjan> `? !
05:48:27 <shachaf> hg: what sort of time machine are you twh
05:48:28 <HackEgo> ​!? ¯\(°​_o)/¯
05:48:33 <oerjan> `? hmph
05:48:34 <HackEgo> His Master's Phonetic Hmph
05:48:54 <oerjan> i'm sure there's a proper way, but i cannot take any more manual reading.
05:49:13 <shachaf> oerjan: is that like automatic writing
05:49:19 <oerjan> MAYBE
05:49:34 <hppavilion[1]> quintopia: YES! I DID IT PROBABLY!
05:50:03 <oerjan> `le/rn !/! is a syntax used in Haskell and Prolog for solving evaluation order problems.
05:50:06 <HackEgo> Learned «!»
05:50:09 <oerjan> `? !
05:50:10 <HackEgo> ​! is a syntax used in Haskell and Prolog for solving evaluation order problems.
05:52:12 -!- tromp_ has joined.
05:52:30 <oerjan> <ais523> ugh, some of them have come back <-- perhaps you should block the offending ad site hth
05:52:48 <ais523> just found a different site altogether
05:54:44 <shachaf> `le/rn cut elimination/The cut-elimination theorem states that any Prolog program written using the cut operator ! can be rewritten without using that operator.
05:54:46 <HackEgo> Learned «cut elimination»
05:54:50 <oerjan> i mean, if there's a third party site server annoying ads, you might want to block it from everywhere.
05:54:55 <oerjan> *serving
05:55:12 <oerjan> shachaf: is that actually true
05:55:18 <shachaf> oerjan: i was about to ask you
05:55:21 <oerjan> i mean, the second part
05:55:39 <shachaf> which part is the first part
05:55:54 <oerjan> the part that says that's called the cut-elimination theorem hth
05:56:16 <oerjan> i don't the truth of that is in serious question
05:56:20 <oerjan> *+think
05:56:27 <shachaf> no, the cut elimination theorem is https://en.wikipedia.org/wiki/Cut-elimination_theorem
05:56:48 <oerjan> shachaf: um, i said i was not questioning that part hth
05:56:59 <shachaf> oh
05:57:10 <shachaf> i misread my own question
05:57:13 <oerjan> fancy
05:57:18 <shachaf> i don't think the second part is always true
05:57:21 <shachaf> but i don't really know prolog
05:57:31 <oerjan> i think ais523 might know
05:57:45 <oerjan> since he inspired my `? ! addition
05:57:51 <ais523> I think Prolog is TC without cut
05:58:00 <ais523> although it might be via bundling an interpreter
05:58:12 <ais523> and not a metacircular one, either, you'd have to go pretty much back to first principles
05:58:27 <shachaf> oerjan: if you can rephrase that wisdom entry to make it true that would improve it
05:59:14 <oerjan> shachaf: maybe it's like with the ordinary cut-elimination theorem, that it's possible but things blow up exponentially or more
06:00:51 <\oren\> trump won nevada
06:01:00 <Elronnd> why do you care
06:01:03 <Elronnd> you're in canada
06:01:06 <oerjan> `le/rn programmers knowing what they're doing/Programmers knowing what they're doing is a hypothetical race invoked to justify keeping horrendous traps in programming languages.
06:01:08 <HackEgo> Learned «programmers knowing what they're doing»
06:01:13 <\oren\> i'm having fun watching it
06:01:14 <oerjan> Elronnd: he might nuke canada hth
06:01:26 <\oren\> it's the funniest show on earth
06:01:30 <ais523> I'm following the US election too
06:01:32 <Elronnd> oerjan: true
06:01:55 <ais523> my opinion on Trump is that we basically don't have a clue what his opinions actually are, because the ones he publicly gives seem to have been designed for entertainment value more than truthfulness
06:02:05 <ais523> and that he probably wouldn't be as disastrous as he's pretending to be
06:02:15 <ais523> but it's fun to see what he'll come up with in the meantime
06:02:24 <Elronnd> yeah true
06:02:39 <Elronnd> I'm not quite sure whether or not I want him to be president just to see what happens
06:03:01 <\oren\> at this point I just want the show to go on
06:03:35 -!- jaboja has quit (Ping timeout: 244 seconds).
06:04:04 <oerjan> <shachaf> oerjan: if you can rephrase that wisdom entry to make it true that would improve it <-- [citation needed]
06:04:05 <ais523> there are various possibilities that would be even more dramatic
06:04:25 <ais523> e.g. say the democrats nominate hillary (which seems the most likely outcome at this point), republican convention is contested
06:04:31 <ais523> and while the republicans are deciding hillary gets arrested
06:04:37 -!- hppavilion[1] has quit (Ping timeout: 244 seconds).
06:05:05 <oerjan> `` sed -i 's/race/alien race/' wisdom/'programmers knowing what they're doing'
06:05:06 <HackEgo> ​/hackenv/bin/`: eval: line 4: unexpected EOF while looking for matching `'' \ /hackenv/bin/`: eval: line 5: syntax error: unexpected end of file
06:05:55 <ais523> oerjan: unescaped ' in the middle of your string
06:06:09 <Elronnd> `` sed -i 's/race/alien race/' 'wisdom/programmers knowing what they're doing'
06:06:09 <HackEgo> ​/hackenv/bin/`: eval: line 4: unexpected EOF while looking for matching `'' \ /hackenv/bin/`: eval: line 5: syntax error: unexpected end of file
06:06:16 <shachaf> `le/rn cat elimination/cat elimination is the process of replacing a one-argument `cat` command with the shell operator <
06:06:19 <HackEgo> Learned «cat elimination»
06:06:21 <ais523> you might want to "-quote it or use '\''
06:06:52 <Elronnd> `` sed -i "s/race/alien race/" "wisdom/programmers knowing what they're doing"
06:06:54 <HackEgo> No output.
06:06:59 <ais523> `le/rn cat introduction/cat introduction is the process of piping one or more extra `cat` commands into your pipeline; occasionally this is even actually useful
06:07:01 <HackEgo> Learned «cat introduction»
06:07:01 <oerjan> fancy
06:07:33 <Elronnd> when is it "actually useful"?
06:07:35 <shachaf> oerjan: is that related to http://www.purrsonals.com/ twh
06:08:28 <oerjan> ais523: i'm not really following, but i've been assuming that the only chance either trump or sanders has of becoming president is if they face each other in the final election.
06:08:45 <izabera> is there any language that has implicit looping and explicit termination?
06:08:59 <ais523> oerjan: well, the only two other people who seem likely on the republican side are cruz and rubio
06:09:14 <izabera> like, when you run out of instructions you start from the beginning of the program again, and there's an explicit instruction to exit
06:09:15 <ais523> and cruz is known to be pretty extreme in views (as opposed to trump, for whom it's hard to tell)
06:09:20 <oerjan> hm
06:09:42 <ais523> cruz versus sanders, for example, would basically be a choice between extreme right and extreme left (from a US point of view)
06:10:03 <ais523> izabera: quite a few of mine are like that, e.g. there's a C-INTERCAL command that puts it into that mode
06:10:14 <izabera> ah ok nice
06:10:18 <ais523> however normally I don't add the halt command because it isn't really required
06:10:21 <Elronnd> C-INTERCAL?
06:10:29 <Elronnd> Is that C bindings for INTERCAL?
06:10:38 <ais523> Elronnd: it's an INTERCAL compiler written in C
06:10:44 <ais523> it has C bindings, though
06:10:46 <ais523> also Befunge bindings
06:10:50 <Elronnd> ah
06:10:57 <izabera> TIL building walls to keep immigrants away is not extreme right
06:10:58 <ais523> and they work using INTERCAL control flow
06:11:26 <ais523> you don't necessarily call the C from the INTERCAL; you could instead put a COME FROM statement in the C and it'd steal control from the INTERCAL
06:11:50 <oerjan> `culprits wisdom/cat elimination
06:11:52 <ais523> izabera: Trump's opinions aren't consistently extreme right
06:11:53 <HackEgo> shachaf
06:12:03 <oerjan> `culprits wisdom/cat introduction
06:12:04 <ais523> also he isn't going to build it himself, he claims he's going to make the Mexicans build one
06:12:05 <HackEgo> ais523
06:12:34 <ais523> which is incredibly unrealistic; I'm not convinced they could afford it no matter how much pressure the US puts on them
06:12:37 <izabera> i thought purssonals.com was furry related but it's only cat relatex
06:12:40 <\oren\> well people have pointed out that Trump is more like a european right winger than a US one
06:12:57 -!- FreeFull has joined.
06:12:59 <ais523> and the US would probably get into a ton of international trouble
06:13:02 <ais523> it's like the Antiguan pirate movies
06:13:11 <izabera> like he careS
06:13:15 <oerjan> <shachaf> oerjan: is that related to http://www.purrsonals.com/ twh <-- why are you asking me
06:13:20 * izabera stares at her fingers
06:13:37 <ais523> (summary: there was some sort of trade dispute between the US and Antigua, the WTO found that Antigua was in the right and had lost money as a result, and they gave it the right to pirate X amount of US copyrighted stuff in order to get their money back)
06:14:44 <izabera> ah that's why antiguan iphones are so cheap
06:15:58 <oerjan> `` sed -i 's/$/./' wisdom/'cat introduction'
06:16:00 <HackEgo> No output.
06:18:08 <shachaf> oerjan: you made the wisdom entry hth
06:18:50 <oerjan> <izabera> i thought purssonals.com was furry related but it's only cat relatex <-- just blame freefall hth
06:20:06 <oerjan> shachaf: which one
06:20:42 <oerjan> shachaf: are you perchance confused again
06:20:48 -!- tromp_ has quit (Remote host closed the connection).
06:20:49 <izabera> i also had another idea: a language where the only means to loop is a goto instruction and it has a side effect of incrementing a memory cell
06:21:02 <oerjan> goto++
06:21:17 <izabera> :) nice name
06:21:35 <oerjan> remarkably, it doesn't seem taken either
06:21:47 <izabera> i'm copyrighting the idea
06:22:07 <ais523> I was pretty sure it was taken
06:22:24 <ais523> http://esolangs.org/wiki/GOTO%2B%2B
06:22:34 <oerjan> oh.
06:22:42 <oerjan> stupid capitalization
06:22:50 <shachaf> oerjan: "cat introduction" hth
06:22:56 * oerjan was just writing the url directly
06:23:07 <ais523> it also has its own website: http://www.gotopp.org/faq.html.en
06:23:26 <izabera> well this sounds easy to fix
06:23:40 <izabera> goto-- where jumping decrements a variable
06:23:52 <oerjan> shachaf: you're clearly confused. do you have toxoplasmosis tdnh
06:24:09 <shachaf> oerjan: oh
06:24:30 <shachaf> i'm not used to ais523 making wisdom entries
06:24:37 <ais523> nor am I
06:24:41 <izabera> make it --goto: cells wrap around at 256 and if the decremented value ends up being 0 you don't jump
06:24:44 <ais523> I have a few more but they're mostly serious ones
06:24:48 <shachaf> and your nicks are in the same length equivalence class
06:25:05 <ais523> why do people put nicks into equivalence classes?
06:26:34 <oerjan> due to the ancient order of myndzi
06:26:35 <shachaf> I didn't put them into that equivalence class, they were already in it.
06:26:48 <oerjan> who seems to have disappeared entirely from here
06:27:24 <oerjan> `? myndzi
06:27:25 <HackEgo> myndzi keeps us all on our feet.
06:27:39 <shachaf> `` hg log wisdom | grep 'summary: <ais523>' | egrep -v 'sed|revert'
06:27:41 <oerjan> `learn myndzi used to keep us all on our feet.
06:27:45 <HackEgo> summary: <ais523> le/rn cat introduction/cat introduction is the process of piping one or more extra `cat` commands into your pipeline; occasionally this is even actually useful \ summary: <ais523> learn Moths are the main ingredient of mothballs. \ summary: <ais523> le/rn al gore/al gore invented the algorithm \ summary: <ais523> e
06:27:49 <HackEgo> Learned 'myndzi': myndzi used to keep us all on our feet.
06:27:56 <ais523> you mean now, people have to draw in the arms, legs and bodies of stick figures /manually/?
06:28:01 <oerjan> yeah
06:28:13 <ais523> wait, "moths are the main ingredient of mothballs" was me?
06:28:22 <shachaf> `` hg log wisdom | grep 'summary: <ais523>' | egrep -v 'sed|revert' | tail -n+4
06:28:25 <HackEgo> summary: <ais523> echo wisdom/* | shuf | head -n 10 | xargs rm \ summary: <ais523> ls wisdom/* | shuf | head -n 10 | xargs rm \ summary: <ais523> le/rn hash 2346ad27d7568ba9896f1b7da6b5991251debdf2 \ summary: <ais523> le/rn resume/a resume is something that you use in order to end a pause in employment \ summary: <ais523> learn
06:28:29 <oerjan> ^celebrate aka mourn
06:28:29 <fungot> \o| c.c \o/ ಠ_ಠ \m/ \m/ \o_ c.c _o/ \m/ \m/ ಠ_ಠ \o/ c.c |o/
06:28:53 <shachaf> Those don't look very serious.
06:29:51 <ais523> indeed
06:30:04 <ais523> perhaps I was wrong abou them mostly being serious
06:30:20 <shachaf> Maybe you added serious quotes instead of serious wisdom entries.
06:30:22 <ais523> also, I decided to reverse that hash
06:30:33 <ais523> there are a ton of apparently unrelated sites where people are complaining that it's impossible to reverse
06:30:39 <ais523> I suspect it is the SHA-1 hash of "hash"
06:30:51 <oerjan> "suspect"
06:30:54 <ais523> yep, just verified
06:30:57 <ais523> I wasn't sure until I checked
06:31:25 <oerjan> the nice thing about hashes is that suspicion is close to knowledge
06:31:35 <ais523> " The word above "Hash" is the correct spelling for the word. It is very easy to misspell a word like Hash, therefore you can use TellSpell as a spell checker. Whenever you do not know how to spell a word just go to this site and search, we got millions of different misspellings for the words already indexed by google, so just google it it as you think it is spelled and hopefully google will help you find Tellspell again!"
06:32:15 <ais523> (this site actually outright reverses the hash in question, i.e. it contains the hash somewhere on the page and explains what it's a hash of also on the same page)
06:32:25 <shachaf> The Bitcoin network computes 2^64 SHA-256 hashes every 10-20 seconds.
06:32:54 <ais523> also this list of "common spellings" is ridiculous
06:33:00 <ais523> * "common misspellings"
06:33:39 <ais523> it includes things like 'whaswh', 'hkashk', 'hiesh', and 'as'
06:34:00 <ais523> ooh and 'thasth'
06:34:41 <ais523> also a list of anagrams which is actually a list of permutations
06:34:57 <oerjan> ais523: so you could say it makes a hash of spellings?
06:35:08 <ais523> definitely!
06:36:47 <oerjan> this reminds me how annoyed i get at dictionary/lyrics etc. sites that steal google hits for things they _don't have actual entries for_
06:37:30 <shachaf> lyrics websites are the worst
06:37:36 <oerjan> which is, i guess, why nowadays i go directly to wiktionary
06:37:36 <shachaf> why are they all bad twh
06:37:43 <ais523> nah, worst would probably be the search engines that attempt to steal google hits
06:38:03 <ais523> I can see why they do it but it's still mindboggling
06:38:14 <ais523> as in, top result on google is the same search, just in a different search engine
06:38:20 <oerjan> shachaf: i looked up one of those italian songs yesterday and it had the lyrics, but in the wrong charset so più had a russian letter at the end
06:38:31 <ais523> (mostly these are specific search engines that focus on one thing and aren't very well known)
06:38:49 <oerjan> *this site had
06:39:16 <shachaf> `le/rn post-turing machine/A post-Turing machine is a machine from the post-Turing era.
06:39:18 <HackEgo> Learned «post-turing machine»
06:40:20 <shachaf> Sgeo: you should sleep hth
06:41:21 * Sgeo throws a macro suffering from incorrect hygiene implementation at shachaf
06:41:27 <oerjan> hm you reminded me to peek at bitcoin again, it seems to have doubled in the last 6 months
06:42:17 <ais523> in value? or in volume?
06:42:27 <oerjan> value
06:43:09 * ais523 wonders if bitcoin is the most volatile widely-traded asset in the world
06:43:20 <oerjan> oh, i _used_ to go to merriam-webster for english words often, because they had a good pronunciation guide. but then they redesigned so it's hard to find the actual pronunciation key...
06:43:22 <ais523> it seems unlikely, but it also seems unlikely that something could be even more volatile
06:44:11 <shachaf> What counts as an asset?
06:45:53 <ais523> something that has value
06:46:06 <ais523> I had to qualify it with "widely-traded" so that it wouldn't end up applying to almost everything
06:46:06 -!- hppavilion[1] has joined.
06:47:01 <oerjan> oil is pretty volatile if you have a match hth
06:47:32 <shachaf> How widely-traded is Bitcoin?
06:48:06 <oerjan> oh hm it wasn't actually ais523 who reminded me of prolog cut, but prooftechnique
06:48:15 <oerjan> back to logreading
06:48:24 <shachaf> oerjan: toxoplasmosis strikes again hth
06:49:04 <oerjan> yeah. i didn't get away from the cats soon enough.
06:49:05 <shachaf> You can probably find some pretty volatile 3x leveraged ETF that's at least as widely-traded as Bitcoin?
06:49:27 <oerjan> normal people don't know what ETF means, shachaf.
06:49:29 <oerjan> google ->
06:50:03 <shachaf> oerjan: ask \oren\, he's an expert in derivatives hth
06:51:03 <oerjan> OKAY
06:51:23 -!- jaboja has joined.
06:52:35 <hppavilion[1]> Ugh
06:52:39 <hppavilion[1]> Introducing
06:52:43 <hppavilion[1]> Whoops
06:52:57 <hppavilion[1]> Introducing variables to Thoof would make it a LOT easier to use
06:53:06 <hppavilion[1]> But that would be cheating, IMHO...
07:04:21 <oerjan> `? theory
07:04:22 <HackEgo> To be theory is to be like a theorem, but inferior
07:04:32 <oerjan> `` sed -i 's/$/./' wisdom/theory
07:04:34 <HackEgo> No output.
07:04:44 * oerjan charges hppavilion[1] one period.
07:06:37 <hppavilion[1]> .
07:09:14 -!- lambda-11235 has quit (Quit: Bye).
07:20:49 -!- J_Arcane has quit (Quit: ChatZilla 0.9.92-rdmsoft [XULRunner 35.0.1/20150122214805]).
07:20:51 <hppavilion[1]> oerjan: Happy?
07:21:18 -!- J_Arcane has joined.
07:21:19 -!- tromp_ has joined.
07:22:04 <oerjan> as a potamus
07:25:29 -!- tromp_ has quit (Ping timeout: 240 seconds).
07:52:43 -!- adu has joined.
07:53:10 <hppavilion[1]> (to the dora tune: )b- b- b- b- b- bit-coin
07:53:26 <oerjan> <shachaf> So !(!A -o ?_|_) -o ?_|_ should be the same as A? <-- i don't think you need to know what ?_|_ is to see that can't be true, since ! is not injective
07:54:02 <shachaf> What do you mean?
07:54:28 <oerjan> i mean that !!A = !A, so the left side _also_ must be the same as !A
07:54:58 <shachaf> I must be missing the thing you're looking at.
07:55:04 <ais523> !_x!_yA = !_xyA
07:55:36 <shachaf> ais523: What's !_x?
07:55:42 -!- jaboja has quit (Ping timeout: 244 seconds).
07:55:51 <ais523> shachaf: it's a syntax used in various generalizations of linear logic
07:55:54 <oerjan> shachaf: !(!A -o ?_|_) -o ?_|_ is the same as !(!(!A) -o ?_|_) -o ?_|_ because !(!A) is the same as !A
07:56:00 <ais523> typically it just has to be a semiring eleemnt
07:56:19 <ais523> you can do interesting things by choosing various semirings
07:56:25 <oerjan> thus, if the left side is always equal to A, it must also be always equal to !A
07:56:42 <ais523> this is a big unifying theme of a bunch of type systems that I discovered during my thesis, then I discovered that they all failed at their design goal and for the same reason
07:56:58 <shachaf> oerjan: Oh, you mean the left side of the equality.
07:57:46 <shachaf> Maybe it's not the same as A but it's classically equivalent to it.
07:58:00 <oerjan> maybe it's true whenever A = !A
07:58:52 -!- ais523 has quit.
07:59:19 <shachaf> ais523 always leaves very suddenly.
07:59:39 <shachaf> No time to respond to the thing about !_x
07:59:56 <shachaf> I was going to say something about reconciling that with the comonoid laws.
08:00:10 <shachaf> Anyway the same argument you made works for intuitionistic logic.
08:00:22 <shachaf> But of course we expect ~~A to be different from A intuitionistically.
08:00:31 <oerjan> maybe he had a hunch it would be a good time to leave
08:01:42 <shachaf> Why does !A -o ?B correspond to classical implication?
08:01:56 <shachaf> It takes as many As as it wants, and produces as many Bs as it wants.
08:02:05 <shachaf> Including zero Bs?
08:02:13 -!- jaboja has joined.
08:02:51 <oerjan> as many as the caller wants, perhaps?
08:03:47 <oerjan> or maybe it's at _least_ one
08:03:55 <shachaf> Why would it be?
08:03:57 <oerjan> obviously, no one understands ?
08:04:09 <shachaf> If I give you ?A, that means you have to consume any number of As, doesn't it?
08:04:17 <shachaf> You don't know how many but you have to handle them all.
08:04:36 <oerjan> ah, maybe
08:04:47 <shachaf> But maybe that's not enough, in a similar way to comonoids and monoids behaving somewhat differently?
08:05:50 <shachaf> ~(!A -o ?B) = ~(~!A # ?B) = ~(?~A # ?B) = ~?~A x ~?B = !A x ~?B = !A x !~B
08:05:55 <shachaf> Is that right?
08:07:43 <hppavilion[1]> Got lists working in thoof :)
08:07:54 -!- AnotherTest has joined.
08:09:33 <adu> hppavilion[1]: hi
08:09:51 <b_jonas> What do all those ascii stuff even mean?
08:10:45 <shachaf> b_jonas: # is ⅋
08:10:46 <hppavilion[1]> hadu
08:10:56 <hppavilion[1]> adu: I'm making an esoteric proof assistant :)I
08:10:58 <hppavilion[1]> *:)
08:11:13 <adu> hppavilion[1]: how do I inspire clean refactors from my coworkers?
08:11:16 <b_jonas> shachaf: uh... ok
08:11:25 <shachaf> b_jonas: https://en.wikipedia.org/wiki/Linear_logic hth
08:11:41 <b_jonas> I've learnt very little of those non-classical logic thingies
08:11:54 <hppavilion[1]> adu: I have no clue. It's one of the great mysteries of the universe.
08:11:57 <b_jonas> oh, _that_ linear logic
08:12:00 <b_jonas> that's even worse
08:13:18 <adu> hppavilion[1]: I mean, if there are 3 things that, together will be a step closer to a clean API, 1 to fix the bug, and 2 to prevent similar bugs in the fugure, my coworkers tend to do 1 instead of all 3
08:13:45 <hppavilion[1]> adu: Have a riding crop?
08:14:09 <adu> hppavilion[1]: lol
08:14:12 <shachaf> b_jonas: linear logic is so good
08:14:16 <shachaf> if only i understood it
08:14:57 <hppavilion[1]> adu: Or perhaps, if you have 2 coworkers to spare, have one fix the bug and the other two (including you) will prevent it in the future?
08:15:01 <hppavilion[1]> So it's a team refactor?
08:15:22 <adu> hppavilion[1]: that's a better idea
08:16:07 <hppavilion[1]> adu: So I'm inventing a calculus to prove things using s/// notation
08:16:20 <adu> hppavilion[1]: isn't that already a thing?
08:16:24 <hppavilion[1]> adu: For the eso-proof assistant
08:16:27 <hppavilion[1]> adu: Probably.
08:16:36 <hppavilion[1]> adu: I think it's a calculus
08:16:42 <adu> http://mathworld.wolfram.com/SubstitutionSystem.html
08:16:56 <hppavilion[1]> adu: Mine uses regex?
08:17:11 <adu> well, then
08:17:16 <adu> that's different
08:17:26 <hppavilion[1]> adu: PCRE, no less
08:17:46 <adu> hppavilion[1]: https://en.wikipedia.org/wiki/Tag_system
08:17:59 <hppavilion[1]> adu: It made everything easier to use Regex; otherwise, I'm just making manual Thue
08:18:21 <hppavilion[1]> adu: I suppose it could be used to implement a cyclic tag system
08:18:59 <adu> hppavilion[1]: so have you discovered any unique insights? or tautologies?
08:19:05 <hppavilion[1]> A tag is written tagname :: s/begining(?<x>.*)/\g<x>output/
08:19:21 <hppavilion[1]> adu: No; I just got peano arithmetic working xD
08:19:25 <hppavilion[1]> Earlier today
08:19:33 <hppavilion[1]> And really only addition
08:19:54 <adu> I guess that's good
08:20:53 <adu> hppavilion[1]: but I wonder if my philisophy of refactoring is the antithesis of http://c2.com/cgi/wiki?YouArentGonnaNeedIt
08:21:25 <hppavilion[1]> adu: It appears it does
08:21:51 <adu> hppavilion[1]: but on the original hand, if you're already specifying something multiple times, then proper refactoring is covered by http://c2.com/cgi/wiki?DontRepeatYourself
08:22:14 * adu 's head explodes
08:22:58 -!- tromp_ has joined.
08:24:03 <adu> perhaps the only solution is earmarking
08:28:09 -!- tromp_ has quit (Ping timeout: 276 seconds).
08:28:21 <adu> hmm, I don't like wikipedia's earmark, but I do like http://www.urbandictionary.com/define.php?term=earmark
08:30:20 <adu> hppavilion[1]: can you use the same technique you used for addition to implement multiplication?
08:33:04 <hppavilion[1]> adu: Yes, probably
08:34:13 -!- ais523 has joined.
08:37:13 <hppavilion[1]> adu: In case you're curious, http://pastebin.com/Y00f06hb is the axioms for peano arithmetic (but not the theorems)
08:38:00 <adu> axioms are boring, theorems make a theory
08:38:33 <adu> and you don't go to school to learn axioms, you go to learn theory
08:38:55 <hppavilion[1]> Fixed
08:39:11 <hppavilion[1]> adu: ...
08:39:11 <hppavilion[1]> Fine
08:43:38 -!- llue has joined.
08:43:43 <hppavilion[1]> adu: There, updated
08:44:28 -!- lleu has quit (Read error: Connection reset by peer).
08:45:29 <adu> hppavilion[1]: oOo
08:48:44 <hppavilion[1]> adu: Is it acceptable for math iyo?
08:49:16 <adu> "iyo"?
08:49:41 <izabera> in your obliviousness
08:50:18 <adu> hppavilion[1]: perhaps 2 beers ago, I might have found a falicy in your argument, but now, I cannot
08:50:21 <hppavilion[1]> adu: Trust in the izabera. Izabera will never lead you astray
08:50:30 <hppavilion[1]> xD
08:50:58 <hppavilion[1]> Nobody on this channel ever lies or jokes. It is easy to tell what we're talking about- just read the messages
08:53:35 <adu> hppavilion[1]: I lie sometimes
08:53:48 <hppavilion[1]> adu: That's a quantum paradox.
08:53:49 <adu> for example, I don't drink beer, I drink hard apple cider
08:54:23 <adu> aHa!
08:55:10 <oerjan> hppavilion[1]: no, that would be "i lies sometimes" hth
08:55:36 <hppavilion[1]> oerjan: All probability is quantum in hte end
08:55:40 <hppavilion[1]> *the
08:55:49 <adu> hppavilion[1]: I think you meant "hte"
08:56:08 <hppavilion[1]> adu: Hope Tyrants Exterminate?
08:56:20 <adu> teh* I can never get my misspellings incorrect enough
08:56:23 <hppavilion[1]> Hellish Tyranosaurus Eggs?
08:56:28 <hppavilion[1]> xD
08:56:46 <oerjan> adu: you should learn from hppavilion[1]
08:57:26 <adu> oerjan: :)
08:57:50 <oerjan> `? hppavilion[1]
08:57:53 <HackEgo> hppavilion[1] se describe en las notas al pie. ¿Porqué no los dos? Nadie lo sabe.
08:57:59 <oerjan> `? hppavilion
08:58:00 <HackEgo> hppavilion? ¯\(°​_o)/¯
08:58:15 <adu> 3.14159?
08:58:50 <adu> why would you include ZWSP in there?
08:59:15 * adu is confused
08:59:19 <ais523> adu: probably as a method of breaking up botloops
08:59:36 <ais523> ^ul (> 4)S
08:59:37 <fungot> > 4
08:59:42 <ais523> > 4
08:59:53 <ais523> lambdabot: are you OK?
08:59:59 <adu> I'm glad I have a font that has tiny letters in boxes :D
09:00:00 <ais523> @messages?
09:00:02 <lambdabot> Sorry, no messages today.
09:00:06 <ais523> hmm
09:00:08 <ais523> @eval 4
09:00:17 <hppavilion[1]> `? hppavilion1
09:00:18 <HackEgo> higgledy piggledy / hp pavilion / doesn't like jokes that are / written in text; // uncontroversially, / one in a million is / roughly the chance they won't / be left perplexed
09:00:22 <ais523> I fear lambdabot's forgotten Haskell
09:00:27 <ais523> which would be a disaster if true
09:00:27 <ais523> ( 4
09:00:28 <idris-bot> 4 : Integer
09:00:42 <ais523> ^bf ,[.,]!( 4
09:00:42 <fungot> ( 4
09:00:45 <idris-bot> 4 : Integer
09:00:53 <ais523> you need some sort of botloop protection
09:01:08 <shachaf> hppavilion[1]: that's not a very good higgledy piggledy tdnh
09:01:09 <ais523> otherwise people will almost inevitably come up with a way to get the bots to keep talking to each other indefinitely
09:01:17 <shachaf> imo someone ought to improve it
09:01:21 <ais523> until someone mutes or kicks one in order to break up the loop
09:01:25 <hppavilion[1]> `culprits hppavilion1
09:01:29 <HackEgo> No output.
09:01:34 <ais523> it's kind-of a rite of passage whenever someene brings a (sufficiently powerful) new bot in here
09:01:35 <hppavilion[1]> `culprits wisdom/hppavilion1
09:01:39 <HackEgo> hppavilion1 ZomieCheney shachaf hppavilion1
09:01:54 <hppavilion[1]> shachaf: OH LOOK
09:01:59 <shachaf> at what
09:02:07 <shachaf> `` hg log wisdom/hppavilion1 | grep summary:
09:02:08 <HackEgo> summary: <hppavilion1> revert \ summary: <ZomieCheney> learn hppavilion1 is ZombieCheney \ summary: <shachaf> ` sed -i -e \'s/\\w\\+ \\w\\+ //\' -e \'s/leave them/be left/\' wisdom/hppavilion1 \ summary: <hppavilion1> learn hppavilion1 is higgledy piggledy / hp pavilion / doesn\'t like jokes that are / written in text; // uncontrove
09:02:26 <shachaf> looks like you made the file and i made a small change
09:02:27 -!- adu_ has joined.
09:02:28 <hppavilion[1]> Huh.
09:02:36 <hppavilion[1]> shachaf: I'm not the one who made that though.
09:02:38 <ais523> then one or other of the bot operators will figure out a way to prevent the loop permanently
09:02:48 <ais523> some of the bots do it by inserting invisible characters at the start of strings
09:02:52 <ais523> so that they don't hit another bot's prefix
09:03:01 <shachaf> @help eval
09:03:03 <lambdabot> eval. Do nothing (perversely)
09:03:09 <adu_> oops, about a year ago, I programmed to restart my router presicely now, oh well
09:03:22 -!- jaboja has quit (Ping timeout: 252 seconds).
09:03:23 <hppavilion[1]> @echo "walrus"
09:03:24 <lambdabot> echo; msg:IrcMessage {ircMsgServer = "freenode", ircMsgLBName = "lambdabot", ircMsgPrefix = "hppavilion[1]!~DevourerO@58-0-174-206.gci.net", ircMsgCommand = "PRIVMSG", ircMsgParams = ["#esoteric",":@echo \"walrus\""]} target:#esoteric rest:"\"walrus\""
09:03:27 <hppavilion[1]> +
09:03:34 <hppavilion[1]> Whoops
09:03:39 <ais523> shachaf: ah right
09:03:40 <hppavilion[1]> @say "walrus"
09:03:42 <lambdabot> Maybe you meant: src slap faq
09:03:42 <ais523> so why wasn't > working?
09:03:56 <hppavilion[1]> ) "walrus"
09:03:58 <shachaf> I think it's just having problems.
09:04:00 <shachaf> > 1
09:04:07 <hppavilion[1]> ( "walrus"
09:04:09 <idris-bot> "walrus" : String
09:04:09 <shachaf> The way to make a bot loop with two lambdabot instances is ?where.
09:04:09 <lambdabot> 1
09:04:14 <hppavilion[1]> ?where
09:04:15 <shachaf> ?where ?where
09:04:15 <lambdabot> @where <key>, return element associated with key
09:04:18 <lambdabot> ?where ?where
09:04:20 <hppavilion[1]> ?where "walrus"
09:04:27 <lambdabot> I know nothing about "walrus".
09:04:35 -!- adu has quit (Ping timeout: 248 seconds).
09:04:36 -!- adu_ has changed nick to adu.
09:04:38 <adu> http://unifoundry.com/unifont.html
09:04:38 <adu> ^ GNU unifont, best font for universal coverage, not so good for printers, though
09:04:38 <oerjan> <ais523> @eval 4 <-- wrong command hth
09:04:44 <ais523> oerjan: yes but I tried > first
09:04:47 <hppavilion[1]> shachaf: I was going to do hackego <-> lambdabot
09:04:50 <ais523> what else was I meant to do?
09:05:03 <hppavilion[1]> Ugh, when will lambdabot and HackEgo make up and just fuck.
09:06:07 <adu> hppavilion[1]: I agree
09:06:09 <hppavilion[1]> (Arbitrary attribution time! What are the genders of the various bots on the channel, followed by shame for the reasoning you assigned these genders (namely, sexism).)
09:06:30 <hppavilion[1]> (Notice that I put the period between two parentheses there).
09:06:35 <adu> hppavilion[1]: convergence of political structures is bad, convergence of technology is good
09:06:42 <shachaf> ais523: The comonoid laws say that comult which turns !A into !A⊗!A has to produce the "same" value twice, right?
09:07:05 <ais523> shachaf: in what, linear logic?
09:07:24 <hppavilion[1]> adu: If we let interpreters be anonymous objects like in Mascarpone, what does a "coterpreter" do?
09:07:38 <ais523> I don't think that's any more true in general, than A⊗A only working in monoids if both As are the same
09:07:52 <adu> hppavilion[1]: is that a cheese?
09:08:06 <hppavilion[1]> adu: No, it's a language.
09:08:07 <shachaf> ais523: Well, if you work out the comonoid laws in Haskell, they tell you that counit x = () and comult x = (x,x)
09:08:16 <shachaf> (Haskell or Set or that sort of category.)
09:08:16 <hppavilion[1]> adu: A damn good one at that
09:08:22 <adu> hppavilion[1]: or an intrapreter?
09:08:24 <shachaf> Is it different in the context of linear types?
09:08:33 <ais523> oh, hmm
09:08:43 <hppavilion[1]> adu: We should start designing an elaborate structure for interpretation
09:08:46 <ais523> we may have fallen into the problem that monoids exist at multiple levels of abstraction, again
09:08:54 <hppavilion[1]> Something beyond the normal "you have an interpreter and it does your program" thing
09:08:58 <adu> hppavilion[1]: can we model it after MMIX?
09:09:06 <hppavilion[1]> adu: If you like.
09:09:07 <adu> hppavilion[1]: oOo can I tell you my idea?
09:09:11 <hppavilion[1]> adu: Go on
09:09:43 <adu> so MMIX has 2 opcodes that are very similar, 0x00 (which is for the kernel), and 0xFF (which is for users)
09:09:51 <hppavilion[1]> OK
09:10:14 <adu> I was thinking just get rid of 0xFF for user code, and just use it for really exotic opcodes
09:10:52 <adu> like, replace_the_third_and_forth_elements_of_a_16_element_list()
09:11:11 <hppavilion[1]> adu: That's just unnecessary specificity
09:11:21 <hppavilion[1]> adu: I prefer esolangs that generalize too far to ones that specify to far
09:11:33 <hppavilion[1]> s/to far/too far/
09:11:38 <adu> hppavilion[1]: you know how x86 has escape codes for FMA4 and stuff, that's what 0xFF could be
09:11:39 <hppavilion[1]> For the previous exercise, fungot is clearly a fungus- beyond our typical interpretation of "gender"
09:11:39 <fungot> hppavilion[1]: anyway i gotta fix this, using do-loop construct. do, i can no longer do you have
09:12:18 <oerjan> @run 2 -- ais523
09:12:25 <oerjan> still dead
09:12:28 <lambdabot> 2
09:12:31 <oerjan> oh
09:12:35 <oerjan> just slow
09:12:51 <oerjan> ^ul (> 4)S
09:12:51 <fungot> > 4
09:12:55 <hppavilion[1]> adu: contrainterpreter?
09:12:58 <lambdabot> 4
09:13:02 <shachaf> ais523: Which level of abstraction were you thinking of?
09:13:04 <ais523> there we go
09:13:25 <ais523> shachaf: I'm not sure, I was simply going off the most common monoid (tuple formation) and trying to reverse all the arrows mentally
09:13:39 <shachaf> I'm talking about https://en.wikipedia.org/wiki/Monoid_(category_theory)
09:13:44 <hppavilion[1]> interpreter, coterpreter, intrapreter, cotrapreter, contrapreter is the basic set of types of interpreter for Cheese Theory
09:13:59 <ais523> shachaf: ah, I was going off "monoidal category"
09:14:02 <shachaf> Well, the dual of that.
09:14:12 <oerjan> lambdabot has got pretty good at prepending spaces to its messages, so isn't so useful for botlops any longer
09:14:16 <shachaf> A monoid is defined in a monoidal category. I guess those are two levels of abstraction.
09:14:21 <ais523> whereas the monoid you linked exists /inside/ a monoidal category, and uses the category's monoid in order to define itself
09:14:22 <shachaf> oerjan: except for ?where ?where hth
09:14:23 <ais523> yep
09:14:27 <hppavilion[1]> `? botlop
09:14:28 <HackEgo> botlops are the core of botsentiences. Sapience is scheduled for the next release.
09:14:32 <hppavilion[1]> I seemed to have developed an obligation to open any link talking about category theory, despite knowing I won't understand it
09:14:39 <hppavilion[1]> Wow. Didn't expect that.
09:14:44 <hppavilion[1]> `? botloop
09:14:45 <HackEgo> botloop? ¯\(°​_o)/¯
09:14:47 <oerjan> shachaf: wasn't that fixed?
09:14:52 <shachaf> Was it?
09:14:54 <shachaf> ?where ?where
09:14:54 <adu> hppavilion[1]: ok so 0x00 is TRIP, and 0xFF is TRAP, I think I had them reversed, 0xFF is system calls, 0x00 is user-space handlers
09:14:56 <ais523> hppavilion[1]: you mean you do understand it? or that it isn't about category theory?
09:14:56 <lambdabot> ?where ?where
09:15:11 <oerjan> shachaf: not as in it was changed, but as in you cannot define a new one
09:15:21 <shachaf> You mean ?where+ was changed?
09:15:31 <oerjan> hm or was it only with ?
09:15:32 <adu> hppavilion[1]: the secret to category theory is: "Follow the Arrows"
09:15:33 <hppavilion[1]> ais523: I know hat I won't understand whatever is in the link
09:15:43 <shachaf> Yes, it was only ?
09:15:46 <oerjan> ?where testing
09:15:47 <lambdabot> I know nothing about testing.
09:15:47 <ais523> hppavilion[1]: was replying to the "didn't expect that"
09:15:48 <shachaf> ?where test
09:15:51 <lambdabot> preflex: seen ion
09:15:52 <hppavilion[1]> ais523: Ah
09:15:55 <ais523> although I just realised it might be about wisdom rather than about monoids
09:16:05 <hppavilion[1]> ais523: No, I wasn't expecting there to be anything under `? botlop
09:16:07 <adu> ais523: wisdom is good
09:16:11 <hppavilion[1]> ais523: Because I thought it was a typo
09:16:12 <oerjan> ?where+ test ?where test
09:16:15 <lambdabot> Nice!
09:16:17 <hppavilion[1]> `tomfoolery walrus
09:16:18 <HackEgo> I must confess, I know not of what you are speaking.
09:16:20 <oerjan> ?where test
09:16:21 <lambdabot> ?where test
09:16:25 <oerjan> hm ok then
09:16:27 <shachaf> ?where+ test @where test
09:16:29 <lambdabot> Done.
09:16:30 <shachaf> ?where test
09:16:31 <lambdabot> @where test
09:16:35 <oerjan> silly
09:16:49 <hppavilion[1]> `tomfoolery c++
09:16:50 <HackEgo> C++ is an attempt to improve upon C. The only thing it actually improved was memory management, and it made everything else worse.
09:17:00 <hppavilion[1]> `tomfoolery rust
09:17:00 <HackEgo> I must confess, I know not of what you are speaking.
09:17:03 <oerjan> shachaf: but you can still only make messages that start with ? then?
09:17:08 <adu> hppavilion[1]: hey
09:17:13 <adu> hppavilion[1]: Rust is cool
09:17:13 <hppavilion[1]> adu: Yes?
09:17:17 <shachaf> security
09:17:17 <hppavilion[1]> adu: Yeah
09:17:24 <shachaf> https://github.com/lambdabot/lambdabot/blob/master/lambdabot-haskell-plugins/src/Lambdabot/Plugin/Haskell/Type.hs#L77
09:17:27 <hppavilion[1]> adu: And tomfoolery is for accuracy
09:17:36 <shachaf> oerjan: What do you mean?
09:17:37 <adu> hppavilion[1]: Rust is going to eradicate C++ from the world!
09:17:43 <hppavilion[1]> adu: Yeah, no.
09:17:49 <hppavilion[1]> Far too late for that
09:17:54 <adu> hppavilion[1]: I don't think Rust is ever going to displace C
09:17:57 <ais523> `` ln -s tomfoolery bin/'??'
09:17:59 <HackEgo> No output.
09:18:02 <ais523> `?? c++
09:18:03 <adu> hppavilion[1]: but mark my words, Rust is going to replace C++
09:18:03 <HackEgo> C++ is an attempt to improve upon C. The only thing it actually improved was memory management, and it made everything else worse.
09:18:18 <ais523> there, let's have a nice punctuationy tomfoolery-caller
09:18:28 <shachaf> What? That's not accurate at all.
09:18:43 <adu> hppavilion[1]: if you don't believe it too, then you underestimate the power of the borrow
09:18:45 <hppavilion[1]> ais523: Should we change `tomfoolery for randomness?
09:18:47 <shachaf> That's a flamewar attempt. You could be kicked for that sort of thing in a serious channel.
09:19:18 * adu is a disciple of the borrow
09:19:20 <hppavilion[1]> shachaf: Yeah, but we all hate C++ here LTIC
09:19:22 <ais523> hppavilion[1]: I'm happy with the setup atm (amazingly), although that doesn't necessarily mean that there isn't an even better one
09:19:33 <ais523> hppavilion[1]: we like compile-time-C++
09:19:36 <ais523> it's an esolang in its own right
09:19:43 <hppavilion[1]> ais523: Well yeah
09:19:45 <shachaf> I don't hate C++.
09:19:55 <hppavilion[1]> ais523: But C++ on its own is not good for programming, AFAIBT
09:19:57 <ais523> adu: actually, one thing that impresses me more than Rust getting borrows right, is Rust getting steals right
09:20:12 <hppavilion[1]> ais523: Is that a joke? I can't tell
09:20:15 <ais523> it's a huge pain to do those correctly in C, I end up having to write comments clarifying what works
09:20:21 <ais523> hppavilion[1]: not really
09:20:38 <ais523> if you borrow a reference the original caller has it again when you're done, and you can't do anything "transformative" to the reference
09:20:52 <ais523> just look at it, really; possibly mutate what it references, if it's a mutable borrow
09:21:00 <hppavilion[1]> ais523: So there's seriously a programming thing called a "steal", similar to a "borrow"?
09:21:01 <ais523> but you can't do things like change its address or make it a different data type
09:21:04 <hppavilion[1]> Is there a "lose"?
09:21:04 <adu> Rust gets memory right, ownership, borrows, etc.
09:21:17 <ais523> a steal is when the old owner no longer has access to the reference at all
09:21:27 <ais523> and you can do what you like with the reference you stole
09:21:36 <ais523> a good example is free(), it steals the reference to the pointer you're freeing
09:21:38 <ais523> so that it can get rid of it
09:21:48 <shachaf> Isn't that just "move"?
09:21:49 <ais523> realloc() also steals a reference, and then donates one back
09:22:00 <ais523> shachaf: with unique pointers, yes
09:22:03 -!- AnotherTest has quit (Ping timeout: 240 seconds).
09:22:07 <ais523> not sure about refcounted pointers
09:22:09 <oerjan> shachaf: you cannot get lambdabot to say something starting with another bot's prefix
09:22:22 <shachaf> ?where+ test ^where test
09:22:25 <ais523> which is the situation I normally talk about staling for
09:22:26 <shachaf> ?where test
09:22:31 <ais523> *stealing
09:22:35 <lambdabot> It is stored.
09:22:37 <lambdabot> ^where test
09:22:49 <ais523> oerjan: is this based on punctuation marks, or on a hardcoded list, or something else?
09:22:57 <shachaf> oerjan: I think it just adds a space if a line starts with "@".
09:23:26 <ais523> OTOH, fungot seems to have lambdabot on ignore
09:23:26 <fungot> ais523: there's more than 1 element?" at http://paste.lisp.org/ display/ fnord
09:23:30 <ais523> which makes a ton of sense really
09:23:37 <hppavilion[1]> ais523: Ouch, them too?
09:23:56 <ais523> fungot has all the bots in the channel on ignore
09:23:56 <fungot> ais523: lazy as in fnord? the ones i switch between them
09:24:02 <ais523> that's its own method of preventing botloops
09:24:12 <ais523> ^ignore
09:24:26 <ais523> not sure if I can do this, printing the list might be fizzie-only
09:24:59 <oerjan> <ais523> `` ln -s tomfoolery bin/'??' <-- note that symbolic links have a tendency of getting lost in accidents hth
09:25:20 <ais523> that's OK
09:25:35 <ais523> we can have fun with the resulting mess
09:25:39 * ais523 treats HackEgo somewhat like Agora
09:25:52 <ais523> although I haven't managed to scam HackEgo yet
09:26:01 <oerjan> <shachaf> What? That's not accurate at all. <-- shhh
09:28:11 <shachaf> oerjan: https://github.com/lambdabot/lambdabot/blob/master/lambdabot-core/src/Lambdabot/IRC.hs#L83-L85
09:28:40 -!- adu has quit (Quit: adu).
09:29:07 -!- ais523 has quit.
09:29:25 <izabera> i find brainfuck more readable than haskell
09:29:25 <b_jonas> or a sufficiently dumb one
09:29:36 <oerjan> shachaf: huh
09:29:50 <b_jonas> it'e even worse when the bots loop talking to each other in private message or on a channel nobody watches
09:33:44 -!- benderpc_ has joined.
09:35:17 -!- Treio has quit (Quit: Leaving).
09:35:30 -!- Treio has joined.
09:35:58 <oerjan> in that case, i'm pretty sure i can make a HackEgo - lambdabot botloop
09:36:55 <oerjan> ( putStr "hi"
09:36:56 <idris-bot> io_bind (prim_write "hi") (\__bindx => io_return ()) : IO ()
09:37:08 <shachaf> Doesn't HackEgo put a thing in front of every line of IRC?
09:37:24 * oerjan doesn't know whether idris-bot has any unquoted output mechanism
09:37:35 <oerjan> shachaf: no. not every.
09:38:27 <oerjan> ?where HackEgo
09:38:31 <lambdabot> I know nothing about hackego.
09:38:43 <oerjan> `? lambdabot
09:38:44 <HackEgo> lambdabot is a fully functional bot. just don't ask about @src.
09:39:08 <oerjan> ?where+ HackEgo `echo lambdabot
09:39:09 <lambdabot> Okay.
09:39:15 <oerjan> ?where HackEgo
09:39:17 <lambdabot> `echo lambdabot
09:39:18 <HackEgo> lambdabot
09:39:21 <oerjan> um
09:39:27 <oerjan> ?where+ HackEgo `cat lambdabot
09:39:28 <lambdabot> Done.
09:39:51 <oerjan> `mk lambdabot/lambdabot: ?where HackEgo
09:39:52 <HackEgo> usage: mk[x] file//contents
09:39:54 <oerjan> oops
09:40:00 <oerjan> `mk lambdabot//lambdabot: ?where HackEgo
09:40:02 <HackEgo> lambdabot
09:40:19 <oerjan> ?where HackEgo
09:40:21 <lambdabot> `cat lambdabot
09:40:22 <HackEgo> lambdabot: ?where HackEgo
09:40:23 <lambdabot> `cat lambdabot
09:40:24 <HackEgo> lambdabot: ?where HackEgo
09:40:25 <lambdabot> `cat lambdabot
09:40:26 <HackEgo> lambdabot: ?where HackEgo
09:40:27 <oerjan> `rm lambdabot
09:40:27 <HackEgo> rm: cannot remove `lambdabot ': No such file or directory
09:40:34 <lambdabot> `cat lambdabot
09:40:35 <HackEgo> lambdabot: ?where HackEgo
09:40:36 -!- lambdabot has left.
09:40:40 -!- lambdabot has joined.
09:40:49 <oerjan> `rm lambdabot
09:40:51 <HackEgo> No output.
09:40:58 <oerjan> oops silly me, left a space at the end
09:43:44 -!- AnotherTest has joined.
09:43:57 * oerjan briefly wonders if lambdabot left automatically
09:44:10 -!- hppavilion[1] has quit (Ping timeout: 244 seconds).
09:44:37 <oerjan> although i suspect shachaf more
09:50:33 -!- AnotherTest has quit (Ping timeout: 240 seconds).
09:51:31 -!- AnotherTest has joined.
09:56:01 -!- AnotherTest has quit (Ping timeout: 250 seconds).
10:15:56 -!- ais523 has joined.
10:18:59 <shachaf> Of course there are lots of possible comonoids, since the category of linear thingies is monoidal in at least four ways.
10:19:12 -!- jaboja has joined.
10:19:31 <shachaf> Since you make monoids with ⊗, maybe you make comonoids with ⅋, its dual.
10:20:01 <oerjan> ais523: you missed a botloop, see logs
10:20:32 <ais523> now I have to guess at which bots were involved
10:20:38 <oerjan> heh
10:20:41 <ais523> fungot, plus a relatively new bot?
10:20:42 <fungot> ais523: define-macro is not standard; this is all based on prior perception that they would have shortened operator to op if it wasn't
10:20:44 <ais523> two copies of lambdabot?
10:20:52 <oerjan> nope, nope
10:21:00 <ais523> ooh, checking logs, it was lambdabot and hackego
10:21:20 <ais523> I thought hackego would have better bot protection than that
10:21:32 <oerjan> _i_ thought lambdabot did :P
10:21:46 <oerjan> i knew about HackEgo's weakness
10:22:24 <ais523> HackEgo starts lines with a nick, but lambdabot sees that as a prefix
10:22:54 -!- tromp_ has joined.
10:23:34 <oerjan> @tell int-e you might want to improve lambdabot's message prefixing a bit, we can still make it and HackEgo botloop with ?where
10:23:36 <lambdabot> Consider it noted.
10:25:19 <oerjan> ] 1
10:25:25 <oerjan> hm
10:25:28 <oerjan> [ 1
10:25:29 <j-bot> oerjan: 1
10:26:00 <oerjan> there are so many new bots that _might_ have a botloop weakness this way
10:26:17 <oerjan> but i don't know their languages enough to tell
10:26:26 <shachaf> ^prefixes
10:26:26 <fungot> Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , blsqbot !
10:26:32 <ais523> oerjan: thutubot/lambdabot could probably do it
10:27:02 <oerjan> yeah but thutubot is broken around lambdabot anyway
10:27:06 -!- thutubot has joined.
10:27:10 <ais523> > "test"
10:27:15 <lambdabot> "test"
10:27:15 <thutubot> "test"
10:27:22 <ais523> indeed
10:27:30 <oerjan> ?where ?where
10:27:40 <lambdabot> ?where ?where
10:27:40 <thutubot> ?where ?where
10:27:43 <lambdabot> ?where ?where
10:27:44 <thutubot> ?where ?where
10:27:45 -!- tromp_ has quit (Ping timeout: 276 seconds).
10:27:45 <lambdabot> ?where ?where
10:27:46 <thutubot> ?where ?where
10:27:47 <lambdabot> ?where ?where
10:27:48 <thutubot> ?where ?where
10:27:50 <ais523> +quit
10:27:50 -!- thutubot has quit (Client Quit).
10:27:51 <lambdabot> ?where ?where
10:27:53 -!- lambdabot has left.
10:27:57 -!- lambdabot has joined.
10:28:03 <oerjan> hm again
10:28:17 <ais523> that certainly looks a lot like some sort of loop protection
10:28:21 <oerjan> i think possibly lambdabot has another botloop protection
10:28:30 <ais523> ?where ?where
10:28:30 <oerjan> it left the same way with HackEgo
10:28:31 <ais523> ?where ?where
10:28:31 <lambdabot> ?where ?where
10:28:33 <ais523> ?where ?where
10:28:33 <lambdabot> ?where ?where
10:28:34 <ais523> ?where ?where
10:28:35 <lambdabot> ?where ?where
10:28:36 <ais523> ?where ?where
10:28:38 <lambdabot> ?where ?where
10:28:39 <ais523> ?where ?where
10:28:50 <lambdabot> ?where ?where
10:28:52 <lambdabot> ?where ?where
10:28:53 <ais523> ?where ?where
10:28:54 <ais523> ?where ?where
10:28:54 -!- lambdabot has left.
10:29:00 -!- lambdabot has joined.
10:29:02 <ais523> oerjan: how about that for evidence?
10:29:02 <lambdabot> ?where ?where
10:29:13 <oerjan> pretty good
10:29:34 <fizzie> That last ?where ?where after rejoining seems a bit suboptimal for loop protection.
10:29:47 <ais523> it was behind by one at the time
10:30:08 <ais523> we might be able to get a sustained loop past the protection via writing the trigger phrase twice
10:30:31 <ais523> but I assume one copy disappears with each /cycle
10:31:16 <oerjan> i'm a bit worried there might be a second stage where lambdabot _doesn't_ rejoin
10:31:58 <ais523> ah right
10:35:27 <shachaf> @@ @where+ test @run text "a\nb"
10:35:45 <ais523> shachaf: I think I see where this is going
10:35:46 <lambdabot> Done.
10:35:48 <shachaf> @where test
10:35:50 <lambdabot> a b
10:35:55 <oerjan> FAYL
10:36:10 <ais523> which of our bots can produce multiple lines of output from one command?
10:36:21 <shachaf> lambdabot can produce multiple lines in some cases.
10:36:29 <oerjan> ( 1+"hi"
10:36:30 <idris-bot> String is not a numeric type
10:36:37 <shachaf> I'm not sure whether any of them can be user-produced.
10:36:43 <ais523> !bf ++++++++++[>+++++++>+<<-]>.<.>+.
10:36:43 <EgoBot> F
10:36:46 <oerjan> idris-bot: how uncharacterically brief of you
10:37:04 <ais523> !bf ++++++++++[>+++++++>+<<-]>>.<.>+.
10:37:05 <EgoBot> ​\ F.
10:37:16 <ais523> !bf ++++++++++[>+++++++>+<<-]>.>.<+.
10:37:16 <EgoBot> F \ G
10:37:19 <ais523> there we go
10:37:42 <oerjan> i think EgoBot and HackEgo use the same output scheme
10:37:44 <ais523> now I'm wondering if there's any way to get a genuine newline out of that
10:37:56 <ais523> oerjan: I seem to remember EgoBot printing three lines and DCCing me the rest
10:38:05 <ais523> but maybe that's changed since
10:38:10 <oerjan> hm well it does that for !show
10:38:19 <oerjan> ok then
10:38:25 <oerjan> !sh echo a; echo b
10:38:25 <EgoBot> a \ b
10:38:55 <oerjan> ( [1,2]
10:38:56 <idris-bot> Can't disambiguate since no name has a suitable type:
10:38:56 <idris-bot> Effects.Env.::, Data.HVect.::, Prelude.List.::, Data.Vect.Quantifiers.::, Prelude.Stream.::, Data.Vect.::
10:39:23 <ais523> idris-bot: that's more like it :-)
10:39:47 <oerjan> i'm not sure it has any way to produce free format output, though
10:39:56 -!- Nithogg has quit (Quit: WeeChat 0.4.1).
10:40:09 <oerjan> [ 1 2 ; 3 4
10:40:10 <j-bot> oerjan: ┌───┬───┐
10:40:10 <j-bot> oerjan: │1 2│3 4│
10:40:10 <j-bot> oerjan: └───┴───┘
10:40:28 <ais523>
10:40:39 <ais523> that has much the same effect on me as XKCD's type comic did
10:40:49 -!- Nithogg has joined.
10:41:04 <ais523> you don't expect data types to come back at you as ascii art
10:41:07 <ais523> err, cp437 art
10:41:42 <oerjan> [ (1; 2) (3; 4)
10:41:43 <j-bot> oerjan: |syntax error
10:41:43 <j-bot> oerjan: | (1;2)(3;4)
10:41:49 <oerjan> [ (1; 2); (3; 4)
10:41:49 <j-bot> oerjan: ┌─────┬─┬─┐
10:41:49 <j-bot> oerjan: │┌─┬─┐│3│4│
10:41:49 <j-bot> oerjan: ││1│2││ │ │
10:41:49 <j-bot> oerjan: │└─┴─┘│ │ │
10:41:49 <j-bot> oerjan: └─────┴─┴─┘
10:42:03 <oerjan> it doesn't seem to want to stack vertically
10:42:10 <oerjan> { 1,2 ; 3,4
10:42:15 <oerjan> [ 1,2 ; 3,4
10:42:16 <j-bot> oerjan: |domain error
10:42:16 <j-bot> oerjan: | 1 ,2;3,4
10:42:19 <oerjan> hmph
10:42:28 <oerjan> actually knowing J might help
10:42:31 <shachaf> @bf ++++++++++[>+++++++>+<<-]>.>.<+.
10:42:35 <lambdabot> F
10:42:37 <lambdabot> G
10:43:58 <oerjan> alas, that one _does_ prefix spaces religiously
10:44:10 <ais523> clearly we just need a bot that uses space as a prefix :-P
10:44:19 <oerjan> indeed
10:45:06 <shachaf> Just get a three-way loop where each bot activates the other two.
10:45:31 <ais523> exponential botloop
10:45:32 <shachaf> I guess that'd be as difficult as a command that prints two of the same line.
10:45:41 <shachaf> ?where hackego
10:45:41 <lambdabot> `cat lambdabot
10:45:43 <HackEgo> cat: lambdabot: No such file or directory
10:45:49 <oerjan> [ "hi"
10:45:49 <j-bot> oerjan: |syntax error
10:45:50 <j-bot> oerjan: | "hi"
10:45:54 <oerjan> [ 'hi'
10:45:55 <j-bot> oerjan: hi
10:46:02 <oerjan> ...that looks too easy.
10:46:04 <ais523> OK, what about this
10:46:12 <ais523> we all spam a lot of lambdabot commands for the next several years
10:46:22 <shachaf> `mkx bin/snackego//echo ':)'
10:46:24 <HackEgo> bin/snackego
10:46:27 <shachaf> `snackego
10:46:28 <HackEgo> ​:)
10:46:31 <ais523> so next time fizzie updates the markov chains, fungot has a good chance of coming up with lambdabot commands by accident
10:46:31 <fungot> ais523: i tried to make a fnord it increases by 1 at each turn.
10:46:41 <oerjan> `botsnack
10:46:42 <HackEgo> ​>:-D
10:46:45 <shachaf> But fungot won't listen to lambdabot.
10:46:45 <fungot> shachaf: what's wrong with the chicken release at http://www.call-with-current-continuation.org/ chicken.html chicken scheme
10:46:53 <oerjan> shachaf: RE: Dundant
10:46:55 <shachaf> fungot: ask boily hth
10:46:55 <fungot> shachaf: the granularity you fnord of course, but that
10:47:04 <ais523> come to think of it, this is one of the reasons that fungot refuses to answer the same person multiple times in a row, isn't it?
10:47:04 <fungot> ais523: http://citeseer.ist.psu.edu/ kelsey93tractable.html, page 5 bottom/ 6 top of a symbolics lisp machine implemented on top of
10:47:14 <ais523> because it could trigger a fungot/myndzi botloop
10:47:15 <fungot> ais523: why doesn't it add phrases from the other framework.)
10:47:24 <oerjan> idris-bot: 2
10:47:29 <oerjan> idris-bot: ( 2
10:47:29 <idris-bot> 2 : Integer
10:47:43 <oerjan> j-bot: 'hi'
10:47:44 <j-bot> oerjan: hi
10:47:46 <shachaf> ?where+ test [ '?where test'
10:47:55 <lambdabot> Nice!
10:47:57 <shachaf> ?where test
10:47:58 <lambdabot> [ '?where test'
10:48:12 <shachaf> [ '?where test'
10:48:13 <j-bot> shachaf: ?where test
10:48:20 <ais523> oerjan: I believe j-bot + lamdabot could create a botloop like this, but there's no obvious way to get it started
10:48:23 <oerjan> well that didn't work as expected
10:48:36 <oerjan> ais523: i think shachaf just made one that should have worked
10:48:39 <ais523> as they each ping the person who made the request
10:48:48 <oerjan> no, lambdabot doesn't
10:48:53 <ais523> ah right
10:48:58 <shachaf> ?where+ test j-bot: '?where test'
10:49:02 <ais523> j-bot just ignored lambdabot?
10:49:04 <lambdabot> Good to know.
10:49:05 <shachaf> ?where test
10:49:05 <lambdabot> j-bot: '?where test'
10:49:11 <ais523> I suspect it has an ignore list
10:49:20 <oerjan> looks likely
10:49:48 <shachaf> ^prefixes
10:49:49 <fungot> Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , blsqbot !
10:50:06 <shachaf> fungot doesn't know about j-bot?
10:50:07 <fungot> shachaf: depends on the context, and lambdas. also, it has no provisions for running out of memory...
10:51:56 <ais523> shachaf: ^prefixes is world-editable, I believe
10:52:01 <shachaf> ^ul `r```````````.j.-.b.o.t.:. .'.h.i.'i
10:52:01 <fungot> ...bad insn!
10:52:22 <ais523> ^define ul prefixes ^(Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , blsqbot ! , j-bot [)S
10:52:22 <ais523> ^define prefixes ul ^(Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , blsqbot ! , j-bot [)S
10:52:22 <shachaf> how does unlambda work twh
10:52:37 <shachaf> Oh, I was thinking its ignore list is based on that.
10:52:40 <shachaf> I guess not.
10:52:47 <ais523> shachaf: probably not with the command used for underload
10:52:53 <oerjan> ^prefixes
10:52:53 <fungot> Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , blsqbot !
10:53:02 <shachaf> Doesn't fungot do unlambda?
10:53:02 <fungot> shachaf: i'll do some work for who was a hardcore vegan for purely ideological reasons, and making my way through fnord right now
10:53:07 <shachaf> Am I thinking of the wrong bot?
10:53:08 <ais523> ^help
10:53:08 <fungot> ^<lang> <code>; ^def <command> <lang> <code>; ^show [command]; lang=bf/ul, code=text/str:N; ^str 0-9 get/set/add [text]; ^style [style]; ^bool
10:53:10 <oerjan> shachaf: no, it does underload
10:53:18 <ais523> egobot does unlambda
10:53:27 <ais523> !unlambda `r```````````.j.-.b.o.t.:. .'.h.i.'i
10:53:27 <EgoBot> j-bot: 'hi'
10:53:28 <j-bot> EgoBot: hi
10:53:40 <ais523> `! unlambda `r```````````.j.-.b.o.t.:. .'.h.i.'i
10:53:41 <HackEgo> j-bot: 'hi'
10:53:42 <j-bot> HackEgo: hi
10:53:54 <ais523> and HackEgo because it has all (or almost all?) EgoBot's interps
10:54:03 <shachaf> And lambdabot.
10:54:23 <ais523> @unlambda `r```````````.j.-.b.o.t.:. .'.h.i.'i
10:54:24 <lambdabot> j-bot: 'hi'
10:54:56 <oerjan> [1
10:55:02 <oerjan> ^prefixes
10:55:02 <fungot> Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , blsqbot !
10:55:29 <ais523> ^def prefixes ul ^(Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , blsqbot ! , j-bot [)S
10:55:29 <fungot> Defined.
10:55:33 <ais523> ^prefixes
10:55:33 <fungot> ...out of stack!
10:55:46 <ais523> ^def prefixes ul (Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , blsqbot ! , j-bot [)S
10:55:47 <fungot> Defined.
10:55:50 <ais523> ^prefixes
10:55:50 <fungot> Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , blsqbot ! , j-bot [
10:55:52 <ais523> there we go
10:56:18 <shachaf> What is jconn?
10:56:18 <oerjan> ais523: i believe the spacing is incorrect hth
10:56:28 <oerjan> jconn was the old j-bot
10:56:34 <ais523> I was copying the spacing towards the end
10:56:42 <ais523> also we can't delete the ) for reasons you are fully aware of
10:57:03 <ais523> also we've had 3 J bots at various times
10:57:07 <shachaf> The obvious thing to do is to make a bot with prefix ,
10:57:09 <oerjan> anyway, i think blsqbot died at one point
10:57:10 <ais523> jconn, j-bot, and evalj
10:57:13 <shachaf> Then the spacing will be justified.
10:58:08 <oerjan> the thing is, j-bot needs the space, while afair blsqbot didn't.
10:58:32 <ais523> oh, I see
10:58:40 <ais523> I didn't expect the spaces to be quoted
10:58:50 * shachaf is tempted to `le/rn lambdabot/lambdabot: ?where HackEgo
10:58:50 <ais523> err, copied literally with no visible quoting
10:59:11 <ais523> shachaf: where would the `? come from? lambdabot's data stores?
10:59:13 <oerjan> ^def prefixes ul (Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , j-bot [ .)S
10:59:13 <fungot> Defined.
10:59:20 <oerjan> ^prefixes
10:59:20 <fungot> Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , j-bot [ .
10:59:35 -!- benderpc_ has changed nick to bender|.
10:59:35 <shachaf> Well, ?where HackEgo would need to be fixed too, I guess.
10:59:46 <oerjan> ais523: it seemed a bit verbose to include actual quotes
10:59:55 <oerjan> `prefixes
10:59:56 <HackEgo> Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , blsqbot !
10:59:56 <ais523> oerjan: also ambiguous
11:00:03 <shachaf> just drop the commas hth
11:00:20 <ais523> clearly we need a bot which uses ctrl-a as a prefix
11:00:21 <oerjan> `` sed -i 's/blsq.*/j-bot [ ./' bin/prefixes
11:00:24 <HackEgo> No output.
11:00:28 <oerjan> `prefixes
11:00:28 <HackEgo> ​/hackenv/bin/prefixes: 3: /hackenv/bin/prefixes: Syntax error: Unterminated quoted string
11:00:32 <oerjan> argh
11:00:38 <oerjan> `cat bin/prefixes
11:00:38 -!- jix_ has quit (Remote host closed the connection).
11:00:39 <HackEgo> ​#!/bin/sh \ echo 'Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , j-bot [ .
11:00:44 -!- jix has joined.
11:01:10 <oerjan> `` sed -i "2s/$/'/" bin/prefixes
11:01:11 <HackEgo> No output.
11:01:14 <oerjan> `prefixes
11:01:15 <HackEgo> Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , j-bot [ .
11:01:26 <oerjan> !show prefixes
11:01:27 <EgoBot> sh echo 'Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , blsqbot !'
11:01:37 <oerjan> !delinterp prefixes
11:01:37 <EgoBot> ​Interpreter prefixes deleted.
11:02:02 <oerjan> !addinterp prefixes sh echo 'Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , j-bot [ .'
11:02:03 <fungot> oerjan: gp works quite well. so the first element
11:02:03 <EgoBot> ​Interpreter prefixes installed.
11:02:10 <oerjan> !prefixes
11:02:11 <EgoBot> Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , j-bot [ .
11:02:27 <oerjan> fizzie: please ^save twh
11:02:31 -!- jix has quit (Read error: No route to host).
11:03:10 <shachaf> `` >bin/prefixes (echo '#!/bin/sh'; echo 'tail -n+2 "$0"; exit'; echo 'Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , j-bot [ .')
11:03:11 <fungot> shachaf: i typed it into the calculator with that horrible thing in exercise 1.11 has anything to do with an esoteric language
11:03:11 <HackEgo> ​/hackenv/bin/`: eval: line 4: syntax error near unexpected token `(' \ /hackenv/bin/`: eval: line 4: `>bin/prefixes (echo '#!/bin/sh'; echo 'tail -n+2 "$0"; exit'; echo 'Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , j-bot [ .')'
11:03:46 <shachaf> `` >bin/prefixes echo $'#!/bin/sh\ntail -n+2 "$0"; exit\nBot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , j-bot [ .'
11:03:47 <fungot> shachaf: i found an analogy that lament might like... hanging out talking to you...
11:03:48 <HackEgo> No output.
11:03:52 <shachaf> `prefixes
11:03:54 <HackEgo> tail -n+2 "$0"; exit \ Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , j-bot [ .
11:04:16 <shachaf> `` sed -i 2s/2/3/ bin/prefixes
11:04:18 <HackEgo> No output.
11:04:19 <shachaf> `prefixes
11:04:20 <HackEgo> Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , j-bot [ .
11:04:24 <ais523> why not just #!/bin/tail ?
11:04:42 <shachaf> How would you make that print just the last line?
11:04:47 <shachaf> Hmm, I guess you're allowed one argument.
11:04:57 -!- jix has joined.
11:05:01 <ais523> shachaf: -n1, for example
11:05:15 <ais523> actually sometimes you get more, it depends on the OS
11:05:27 <shachaf> I'm used to #! lines not allowing any arguments, but of course they allow one, just not space separation.
11:05:35 <shachaf> HackEgo is running Linux.
11:06:02 <shachaf> `` >bin/prefixes echo $'#!/bin/tail -n1\nBot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , j-bot [ .'
11:06:02 <fungot> shachaf: ( which is rather perverse."
11:06:04 <HackEgo> No output.
11:06:06 <shachaf> `prefixes
11:06:07 <HackEgo> ​/home/hackbot/hackbot.hg/multibot_cmds/lib/limits: /hackenv/bin/prefixes: /bin/tail: bad interpreter: No such file or directory \ /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: /hackenv/bin/prefixes: Success
11:06:13 <shachaf> `` type tail
11:06:13 <HackEgo> tail is /usr/bin/tail
11:06:18 <shachaf> `` >bin/prefixes echo $'#!/usr/bin/tail -n1\nBot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , j-bot [ .'
11:06:18 <fungot> shachaf: if it had been scratched and hit a couple of days in a year. and i'd like to
11:06:20 <HackEgo> No output.
11:06:21 <shachaf> `prefixes
11:06:21 <HackEgo> Bot prefixes: fungot ^, HackEgo `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , j-bot [ .
11:06:27 <shachaf> ais523: thx tdh
11:07:14 <shachaf> `` cat bin/olist | rot13
11:07:15 <HackEgo> rpub -a "$(onfranzr "$0")${@:+ }$@: "; gnvy -a+2 "$0" | knetf; rkvg \ funpuns \ brewna \ Ftrb \ SverSyl \ obvyl \ abeggv \ o_wbanf
11:07:25 <shachaf> `cat bin/emptylist
11:07:26 <HackEgo> echo -n "$(basename "$0")${@:+ }$@: "; tail -n+2 "$0" | xargs; exit
11:07:44 <ais523> olist is actually echoing the command used to prompt it in the first place
11:08:01 <shachaf> I know, I wrote olist.
11:08:10 <shachaf> I'm not sure it's really necessary.
11:08:15 <ais523> (also, does "funpuns" ping you? and "brewna" looks something like a real nick too, even though my limited rot13-reading ability implies it's probably oerjan)
11:08:24 <shachaf> It does.
11:08:37 <shachaf> But I'm in here anyway. I was trying not to ping others.
11:08:47 <ais523> I know
11:08:54 <ais523> just something to know in the future if I use the same trick
11:09:23 <shachaf> `cat bin/culprits
11:09:26 <HackEgo> hg log --removed "$1" | grep summary: | awk '{print substr($2,2,length($2)-2)}' | sed "s/.$/\x0F&/" | xargs
11:09:32 * oerjan jnirf
11:09:36 <shachaf> Wasn't there a standalone command for that sed thing?
11:09:57 <oerjan> `cat bin/unping
11:10:07 <HackEgo> cat: bin/unping: No such file or directory
11:10:11 <oerjan> something like that
11:10:17 <shachaf> `` rgrep x0F bin
11:10:18 <HackEgo> bin/culprits:hg log --removed "$1" | grep summary: | awk '{print substr($2,2,length($2)-2)}' | sed "s/.$/\x0F&/" | xargs
11:10:24 <oerjan> `` ls bin/*ping*
11:10:26 <HackEgo> bin/noping \ bin/ping
11:10:31 <oerjan> `cat bin/noping
11:10:33 <HackEgo> print_args_or_input "$@" | sed 's/\(..\)/\1​/g'
11:10:35 <ais523> `cat bin/ping
11:10:38 <HackEgo> ​#!/bin/bash \ echo pong
11:10:42 <shachaf> `noping shachaf
11:10:44 <HackEgo> sh​ac​ha​f
11:11:02 <shachaf> `` cat bin/noping | xxd
11:11:04 <HackEgo> 0000000: 7072 696e 745f 6172 6773 5f6f 725f 696e print_args_or_in \ 0000010: 7075 7420 2224 4022 207c 2073 6564 2027 put "$@" | sed ' \ 0000020: 732f 5c28 2e2e 5c29 2f5c 31e2 808b 2f67 s/\(..\)/\1.../g \ 0000030: 270a '.
11:11:22 <ais523> `noping ais523
11:11:24 <HackEgo> ai​s5​23​
11:11:33 <ais523> `` noping ais523 | od -t x1z
11:11:35 <HackEgo> 0000000 61 69 e2 80 8b 73 35 e2 80 8b 32 33 e2 80 8b 0a >ai...s5...23....< \ 0000020
11:11:47 <oerjan> <ais523> olist is actually echoing the command used to prompt it in the first place <-- there's a template list somewhere you can just copy
11:12:37 <ais523> is `list working, btw?
11:12:39 <ais523> `list
11:12:42 <HackEgo> grep: /var/irclogs/_esoteric/201[3-9]-??-??.txt: No such file or directory
11:12:46 <ais523> apparently not
11:12:47 <shachaf> noping seems to have too much overhead.
11:12:52 <ais523> perhaps we should go back to the original implementation
11:12:54 <shachaf> `list was a scow command anyway.
11:13:00 <ais523> it was a great command
11:13:01 <shachaf> I'm glad it's gone.
11:13:24 <ais523> well, I mean, it was clearly ridiculous
11:13:27 <shachaf> People ought to be able to unsubscribe from things like that.
11:13:31 <ais523> and probably worked better if you didn't know how it worked
11:14:19 <shachaf> ais523: What was the original implementation?
11:14:29 <ais523> it mutated a text file when run, rather than grepping the logs
11:14:36 <shachaf> But how would it get your nick?
11:14:45 <ais523> it checked the logs for that, and thus was vulnerable to race conditions
11:14:49 <ais523> if you `listed just before someone else spoke
11:14:51 <shachaf> I thought that `list couldn't work without logs, but now I realize that it can.
11:14:58 <shachaf> It would mutate itself and then print its own culprits.
11:15:03 <ais523> ooh, culprits!
11:15:07 <ais523> yes, I think it can work
11:15:17 <ais523> `culprits bin/list
11:15:22 <oerjan> <shachaf> noping seems to have too much overhead. <-- i tried to put them just dense enough; even now ^v could theoretically get pinged but i figured i'd have to put the foot down somewhere
11:15:23 <HackEgo> tswett tswett oerjan elliott oerjan Phantom__Hoover elliott Sgeo Phantom_Hoover tswett elliott elliott tswett tswett elliott tswett boily boily metasepia tswett Ngevd oerjan elliott oerjan elliott Sgeo oklopol nortti elliott shachaf elliott Phantom_Hoover monqy Phantom_Hoover Phantom_Hoover shachaf Phantom_Hoove
11:15:23 <shachaf> Or mutate some text file.
11:15:28 <shachaf> It doesn't have to be itself.
11:15:33 <ais523> that is a lot of edits
11:15:52 <shachaf> oerjan: Just put one filler character before the last character.
11:15:56 <shachaf> Like culprits does.
11:16:45 <ais523> hmm, a talk here today that doesn't interest me that much but might interest #esoteric
11:16:47 <shachaf> `touch bin/list
11:16:48 <HackEgo> No output.
11:16:50 <shachaf> `culprits bin/list
11:16:53 <HackEgo> tswett tswett oerjan elliott oerjan Phantom__Hoover elliott Sgeo Phantom_Hoover tswett elliott elliott tswett tswett elliott tswett boily boily metasepia tswett Ngevd oerjan elliott oerjan elliott Sgeo oklopol nortti elliott shachaf elliott Phantom_Hoover monqy Phantom_Hoover Phantom_Hoover shachaf Phantom_Hoove
11:17:02 <shachaf> Right, of course that wouldn't affect it.
11:17:26 <ais523> it's talking about how the law of excluded middle implies the existence of a polymorphic function f : (forall a.a -> a) for which f true = false and f false = true
11:17:41 <oerjan> <shachaf> It would mutate itself and then print its own culprits. <-- NOOOOOOOOOOOOOO
11:17:48 -!- jaboja has quit (Ping timeout: 276 seconds).
11:18:05 <ais523> and that the opposite is also true (if such a function exists, then the law of excluded middle holds)
11:18:12 <ais523> oerjan: why does that annoy you that much?
11:18:48 <oerjan> ais523: it's just that i carefully managed to stay off the original `list :P
11:18:57 <oerjan> afair anyway
11:19:14 <ais523> I managed to stay off the original original `list
11:19:21 <ais523> but got retroactively placed on it when it was changed to be log-based
11:19:27 <oerjan> heh
11:19:28 <ais523> then I didn't care so much about staying off it
11:19:39 <shachaf> `cat bin/list
11:19:40 <HackEgo> ​#!/bin/sh \ grep '^..:..:..: <[^>]*> `list' /var/irclogs/_esoteric/201[3-9]-??-??.txt | sed 's/^.*<//;s/>.*//;s/_*$//' | sort -u | tr '\n' ' '
11:21:00 <b_jonas> um, but can't the parenthesis be quoted somehow? I mean, isn't the definition in unefunge, which can print anything you want?
11:21:59 <oerjan> <shachaf> oerjan: Just put one filler character before the last character. <-- the problem with that is people sometimes have characters they ignore at the end rather than the beginning, like _
11:22:15 <shachaf> oerjan: Put one at the beginning and one at the end.
11:22:18 <oerjan> or even at both ends like \oren\
11:22:34 <shachaf> `mkx bin/list//echo $(($(cat conscripts)+1)) > conscripts; culprits conscripts
11:22:37 <HackEgo> bin/list
11:22:48 <b_jonas> oh dear, is tail another of those moving executables like env which are sometimes in /bin and sometimes in /usr/bin and you can't tell which so you can't write portable hashbangs?
11:22:55 <shachaf> who wants to enlist
11:23:08 <ais523> shachaf: I'm not sure that'll work if conscripts isn't an existing file
11:23:18 <ais523> although I guess it does, you juts get a stderr message on the first conscript
11:23:22 <shachaf> It'll print an error the first time.
11:23:47 <shachaf> The advantage of this `list is that it nopings.
11:23:50 <shachaf> So I don't mind it.
11:24:16 <oerjan> b_jonas: no, it's in underload, which cannot print unbalanced ()
11:24:32 <shachaf> `mkx bin/list//date > conscripts; culprits conscripts
11:24:34 <HackEgo> bin/list
11:25:23 <shachaf> Hmm, I guess it should uniq the culprits.
11:25:51 <ais523> there are a lot of esolangs starting with l
11:26:11 <ais523> I didn't realise culprits nopinged
11:26:27 <ais523> `culprits wisdom/mothballs
11:26:29 <HackEgo> No output.
11:26:32 <ais523> hmm
11:26:34 <ais523> `culprits wisdom/mothball
11:26:37 <HackEgo> No output.
11:26:38 <shachaf> `culprits wisdom/moth
11:26:41 <HackEgo> ais523 int-e
11:26:47 <ais523> I can't even remember my own wisdom entries now
11:26:48 <oerjan> <shachaf> who wants to enlist <-- i somewhat dislike adding more permanent single files to HackEgo's top directory hth
11:26:52 <ais523> but yes, that's nopinged
11:26:58 <shachaf> oerjan: good thing no one enlisted yet
11:27:03 <shachaf> oerjan: put it somewhere else
11:27:05 <ais523> oerjan: you could delete them right after and it'd still work
11:27:38 <b_jonas> oh... underload
11:27:38 <shachaf> `` ls --color
11:27:39 <b_jonas> I see
11:27:39 <HackEgo> ​:-( \ (* \ 99 \ bdsmreclist \ [0m[01;34mbin[0m \ [01;32mcanary[0m \ cat \ close \ *) \ Complaints.mp3 \ [01;32m:-D[0m \ dog \ [01;32mecho-p[0m \ [01;34memoticons[0m \ equations \ [01;34metc[0m \ [01;34mevil[0m \ [01;34mfactor[0m \ [01;32mfoo[0m \ [01;34mgood[0m \ [01;32mgrph[0m \ [01;34mhw[0m \ [01;34mibin[0m \ ifc
11:27:40 <shachaf> whoa whoa whoa
11:27:55 <ais523> clearly we need a vt100-to-irc translator
11:27:57 <shachaf> I didn't realize until now that HackEgo did ANSI colors.
11:28:04 <ais523> ls does ANSI colors
11:28:09 <ais523> hackego doesn't
11:28:11 <ais523> thus the raw vt100 getting spouted to the channel
11:28:12 <shachaf> Right, and HackEgo translates them to IRC.
11:28:18 <shachaf> Er, maybe it doesn't.
11:28:20 <ais523> no it doesn't
11:28:27 <ais523> I see a literal esc[01;34m
11:28:28 <shachaf> irssi handles ANSI colors in IRC?
11:28:35 <ais523> irssi may just be echoing directly
11:28:43 <ais523> or it might be parsing it
11:28:58 <ais523> `printf \x1b[J
11:28:58 <HackEgo> ​[J
11:28:58 <shachaf> I'm surprised. OK.
11:29:08 <myname> bdsmreclist?
11:29:10 <ais523> if that didn't clear your screen, it's parsing color codes specifically
11:29:24 <shachaf> It didn't clear my screen.
11:29:30 <shachaf> Or maybe it did and irssi redrew, who knows.
11:29:42 <oerjan> <oerjan> or even at both ends like \oren\ <-- in fact i would be affected myself as oerjan_
11:29:42 <shachaf> But I doubt it just prints things like that into the terminal raw.
11:30:19 <shachaf> `` ls .hg/store/data/
11:30:20 <HackEgo> ​~02welcome.i \ ~0301,08yellow~03.i \ ~0303(~2a.i \ ~0305(~2a.i \ = 0 .i \ 0.i \ 113500.i \ 1.i \ 20131230-coin.jpg.d \ 20131230-coin.jpg.i \ ~2a)~03.i \ 2.i \ ~3a-_d.i \ ~3a-(.i \ 503.i \ ~7f~2a)~03.i \ 8ballreplies.i \ 98076.i \ 99.i \ a \ aaaa.i \ abc.i \ accesslog.i \ a.c.i \ a.i \ alise.i \ alphabet.i \ a.o.i \ a.out.i \ app.sh.i \ argv.py.i
11:30:26 <b_jonas> ais523: I think there's a specific workaround for ls, because ls doesn't know about terminfo or control codes, it just takes them from an env-var that's normally generated by another program that understands terminfo, or something
11:30:38 <b_jonas> however, I don't like colored ls, so I'm not sure about the details
11:31:01 <b_jonas> (the separate command is dircolors )
11:31:09 <b_jonas> hmm...
11:31:21 <ais523> `printf \x1b[5mtest
11:31:21 <HackEgo> ​[5mtest
11:31:27 <ais523> shachaf: what does that look like?
11:31:35 <b_jonas> maybe it's even possible to write a terminfo file that lets programs output IRC color codes?
11:31:43 <shachaf> Looks like the word test.
11:31:44 <b_jonas> I'm not sure how much the terminfo library would like that
11:32:02 <b_jonas> ais523: um, is that supposed to be blinking? try bold instead
11:32:03 <b_jonas> or red
11:32:06 <ais523> shachaf: OK, it's definitely parsing rather than just relaying m commands
11:32:11 <ais523> (in which case it'd be blinking)
11:32:22 <shachaf> I don't think my terminal can blink.
11:32:29 <shachaf> But anyway I was expecting it to parse.
11:32:48 <b_jonas> `tty
11:32:48 <HackEgo> ​/dev/tty1
11:33:02 <ais523> `printf \x1b[1mbold \x1b[0;2mitalic \x1b[0;4munderscore
11:33:03 <HackEgo> ​[1mbold [0;2mitalic [0;4munderscore
11:33:07 <b_jonas> `perl -wewarn "isatty=", (-T), ";"
11:33:10 <HackEgo> Use of uninitialized value $_ in -T at -e line 1. \ Use of uninitialized value in warn at -e line 1. \ isatty=; at -e line 1.
11:33:29 <ais523> I think italic's 2, maybe it's 3
11:33:31 <b_jonas> `perl -wefor$k(keys%ENV){$ENV{$k}=~/jonas/i and print "$k=$ENV{$k} "}
11:33:32 <HackEgo> No output.
11:33:37 <ais523> `printf \x1b[1mbold \x1b[0;2;3mitalic \x1b[0;4munderscore
11:33:38 <HackEgo> ​[1mbold [0;2;3mitalic [0;4munderscore
11:33:53 <b_jonas> hmm
11:34:19 <b_jonas> it would be nice if HackEgo passed the irc line that invoked it in some env-var
11:34:30 <b_jonas> so we could find out both the command and the invoker and the channel easily
11:34:33 <oerjan> `cat bin/list
11:34:33 -!- boily has joined.
11:34:33 <HackEgo> date > conscripts; culprits conscripts
11:35:01 <oerjan> `` sed -i 's!conscripts!share/conscripts!g' bin/list
11:35:03 <HackEgo> No output.
11:35:07 <ais523> `` ls share
11:35:08 <HackEgo> 8ballreplies \ autowelcome_status \ awesome \ cat \ construct_grams.pl \ delvs-master \ dict-words \ esolangs.txt \ esolangs.txt.sorted \ hello \ hello2.c \ hello.c \ lua \ maze \ maze.c \ radio.php?out=inline&shuffle=1&limit=1&filter=*MitamineLab* \ UnicodeData.txt \ units.dat \ WordData
11:35:19 <ais523> ah, there we go
11:35:41 <ais523> hmm, it'd be kind-of funny if we waited until everyone had forgotten about this and then someone went "I wonder what happened to `list?"
11:36:38 <oerjan> `? reflection
11:36:41 <HackEgo> cat.reflection.
11:36:52 <oerjan> `` ls -l wisdom/reflection
11:36:54 <HackEgo> lrwxrwxrwx 1 5000 0 18 Dec 9 04:13 wisdom/reflection -> /proc/self/cmdline
11:37:25 <shachaf> oerjan: culprits still needs to be sorted and uniqed or something
11:37:34 <shachaf> but the trouble is that it prints all the culprits on one line rather than one per line
11:38:05 <ais523> shachaf: can xargs do the reverse transformation to its usual one?
11:38:26 <shachaf> I don't think so.
11:38:31 <ais523> `` echo 'a b c d e f g' | xargs -n 1
11:38:33 <HackEgo> a \ b \ c \ d \ e \ f \ g
11:38:35 <ais523> it can
11:38:46 <shachaf> Ah, hmm.
11:39:04 <boily> hello y'all. y'ello.
11:39:12 <ais523> `` sed -i 's!$! | xargs -n 1 | sort -u | xargs' bin/list
11:39:12 <HackEgo> sed: -e expression #1, char 35: unterminated `s' command
11:39:14 <shachaf> I wanted to do that once and I ended up using a loop in bash for some reason.
11:39:16 <ais523> `` sed -i 's!$! | xargs -n 1 | sort -u | xargs!' bin/list
11:39:17 <boily> what are you guys up to? are you destroying the culprits command?
11:39:18 <HackEgo> No output.
11:39:29 <shachaf> boily: why don't you `list and find out hth
11:39:31 <oerjan> `` echo '! ! !' | xargs -n 1
11:39:32 <HackEgo> ​! \ ! \ !
11:39:34 <ais523> boily: no, we're reimplementing `list
11:39:48 <ais523> because it was broken
11:39:49 <ais523> `cat bin/list
11:39:50 <HackEgo> date > share/conscripts; culprits share/conscripts | xargs -n 1 | sort -u | xargs
11:40:06 <b_jonas> In buubot, I made the nick of the invocant and the channel (and some other similar stuff) accessible to buubot macros through the buubot command "arg"
11:40:43 <shachaf> Hmm, what if bin/list printed the culprits of conscripts into conscripts?
11:41:06 <shachaf> I guess you would need an extra run to be properly subscribed?
11:41:15 <b_jonas> wg. try /msg perlbot compose (echo chan=(arg &c) nick=(arg &n))
11:41:28 <b_jonas> s/wg./eg./
11:41:28 <ais523> I don't really see the point, it's not like we need to backup the VCS's metadata inside the directories being versioned
11:41:41 <shachaf> I just want a canonical thing to put in the file.
11:41:50 <shachaf> date is a hack
11:42:06 <b_jonas> shachaf: pid?
11:42:11 <b_jonas> no wait
11:42:18 <b_jonas> you want one that's always different?
11:42:28 <shachaf> Yes.
11:42:54 <b_jonas> ``` openssl rand -base64 32
11:42:56 <HackEgo> WARNING: can't open config file: /usr/lib/ssl/openssl.cnf \ bxd0jDsvTIaU9pHRBu2ejhGxFwt9j7ERxeZVS//Qh6A=
11:42:59 <b_jonas> uh
11:43:05 <b_jonas> ``` openssl rand -base64 32
11:43:05 <b_jonas> ``` openssl rand -base64 32
11:43:06 <HackEgo> WARNING: can't open config file: /usr/lib/ssl/openssl.cnf \ Gz4O3uQRsEW0DQGn8BMip9gAtJjvQilIqNRmZn60qrA=
11:43:06 <HackEgo> WARNING: can't open config file: /usr/lib/ssl/openssl.cnf \ mNEsg6wleDYweOS1GGI0Ym+7Go9GWFtME1Ok6d3eA5s=
11:43:27 <b_jonas> ``` od -N32 /dev/random
11:43:30 <ais523> isn't that consuming entropy?
11:43:31 <FireFly> Huh, list got replaced with a new list
11:43:34 <ais523> also what does ``` do?
11:43:41 <ais523> FireFly: old one was broken
11:43:44 <FireFly> Yeah
11:43:45 <b_jonas> ais523: ``` is the same as `` but clears the locale
11:43:55 <FireFly> Clever to implement it as culprits
11:43:56 <ais523> so it's C rather than newzealandish?
11:43:57 <HackEgo> No output.
11:44:04 <b_jonas> ais523: something like that
11:44:06 <b_jonas> `` locale
11:44:08 <b_jonas> ``` locale
11:44:12 <ais523> FireFly: it has the problem that nobody dares test whether it works
11:44:26 <FireFly> That is a problem, yes
11:44:37 <shachaf> That's what boily is for.
11:44:48 <shachaf> pushing buttons without finding out what they do first
11:44:55 <b_jonas> um
11:45:00 <boily> `list
11:45:00 <shachaf> `? list
11:45:05 <HackEgo> No output.
11:45:07 <HackEgo> list is a fun program that HackEgo has! Run it with `list and join the fun!
11:45:18 <boily> hmm... if I push it harder...
11:45:19 <boily> `list
11:45:24 <HackEgo> boily
11:45:28 <ais523> congratulations!
11:45:28 <boily> heh :D
11:46:05 <myname> wat
11:46:20 <boily> mynamello. SCIENCE!
11:46:20 -!- chicken_jonas has joined.
11:46:32 <chicken_jonas> `list
11:46:33 <myname> i see
11:46:33 <boily> chelloken_jonas.
11:46:38 <HackEgo> boily
11:46:43 <boily> uhm.
11:46:43 <ais523> @@ @where+ test @run text "`list"
11:46:46 -!- chicken_jonas has left.
11:46:50 <lambdabot> Nice!
11:46:54 <b_jonas> we have +n mode now?
11:46:56 <oerjan> it's a bit scow that it only changes for the next person
11:47:03 <ais523> boily: it's delayed by one cycle
11:47:12 <boily> oh.
11:47:14 <ais523> also I think I might be missing lambdabot perms
11:47:18 <myname> `list
11:47:22 <boily> . o O ( what's a +n? )
11:47:23 <shachaf> @run is just really slow.
11:47:23 <HackEgo> boily chicken_jonas
11:47:28 <myname> i see
11:47:29 <b_jonas> oh, you need one more cycle?
11:47:32 -!- chicken_jonas has joined.
11:47:34 <chicken_jonas> `list
11:47:34 <ais523> to get it to join the `listing
11:47:39 <chicken_jonas> `list again
11:47:39 <HackEgo> boily chicken_jonas myname
11:47:45 <oerjan> b_jonas: yeah hagb4rd discovered it was off and started using it to get around his ban
11:47:46 <HackEgo> boily chicken_jonas myname
11:47:46 <shachaf> boily: it's a pity you weren't around at 02:46
11:47:46 <chicken_jonas> `list and again
11:47:47 <shachaf> 02:46 <fungot> shachaf: what's wrong with the chicken release at http://www.call-with-current-continuation.org/ chicken.html chicken scheme │
11:47:52 <HackEgo> boily chicken_jonas myname
11:48:02 <myname> i may regret that
11:48:17 <ais523> ?where test
11:48:18 <lambdabot> `list
11:48:24 <HackEgo> boily chicken_jonas myname
11:48:30 <ais523> myname: it doesn't ping any more
11:48:40 -!- chicken_jonas has quit (Client Quit).
11:48:52 <boily> shachaf: which 02:46? UTC?
11:49:04 <shachaf> shachaf standard time
11:49:05 <myname> it is a bit more funny with ping because even if you can annoy people with it, you will get annoyed later
11:49:32 <b_jonas> wait, can we just dos it by giving enough different nicknames starting with A that they fill the line?
11:49:53 <b_jonas> or is it sorted by date of first list?
11:50:04 <myname> good point
11:50:09 <shachaf> Right now it's sorted alphabetically.
11:50:12 <oerjan> <ais523> also I think I might be missing lambdabot perms <-- no, you just loaded, you didn't shoot hth
11:50:14 <shachaf> `` culprits bin/list | xargs -n 1 | sort -u | xargs
11:50:17 <b_jonas> hmm
11:50:18 <HackEgo> ais523 Bike boily cuttlefish elliott fungot Jafet metasepia monqy Ngevd nortti oerjan oklopol Phantom__Hoover Phantom_Hoover pikhq Sgeo Sgeo_ shachaf Taneb tswett
11:50:19 <boily> shachaf: I was still asleep at that time, 14 minutes before my phone alarm.
11:50:28 <ais523> oerjan: actually what happened was that my connection was lagging
11:50:37 <b_jonas> oh, so it's sorted by new-zealand locale
11:50:54 <shachaf> ``` culprits bin/list | xargs -n 1 | sort -u | xargs
11:50:58 <HackEgo> Bike Jafet Ngevd Phantom_Hoover Phantom__Hoover Sgeo Sgeo_ Taneb ais523 boily cuttlefish elliott fungot metasepia monqy nortti oerjan oklopol pikhq shachaf tswett
11:51:11 <Taneb> It's brainfuck competition day aaaah
11:51:16 <ais523> so I didn't get a response for a while
11:51:16 <ais523> and my complaint may also have been delayed
11:51:17 -!- ais523 has quit.
11:51:25 <boily> Taneb: Tanelle. aaaaaaaaaaaaaah!
11:51:50 <shachaf> Taneb: do you want to `list hth
11:52:20 <b_jonas> `` echo A K Z a k z [ \\ ] ^ _ \` { \| } ~ 0 1 5 9 - | tr \ \\n | sort
11:52:21 <HackEgo> ​` \ ^ \ | \ _ \ - \ [ \ ] \ { \ } \ \ \ 0 \ 1 \ 5 \ 9 \ a \ A \ k \ K \ /tmp \ z \ Z
11:52:30 <b_jonas> `` echo A K Z a k z [ \\ ] ^ _ \` { \| } ~ 0 1 5 9 - | tr \ \\n | sort | tr \\n \
11:52:31 <HackEgo> ​` ^ | _ - [ ] { } \ 0 1 5 9 a A k K /tmp z Z
11:52:54 <b_jonas> `` echo A K Z a k z [ \\ ] ^ _ \` { \| } ~ 0 1 5 9 - \`m | tr \ \\n | sort | tr \\n \
11:52:55 <HackEgo> ​` ^ | _ - [ ] { } \ 0 1 5 9 a A k K `m /tmp z Z
11:53:00 <myname> wtf /tmp
11:53:11 <myname> ah
11:53:18 <b_jonas> right, ~
11:53:23 <b_jonas> `` echo A K Z a k z [ \\ ] ^ _ \` { \| } \~ 0 1 5 9 - \`m | tr \ \\n | sort | tr \\n \
11:53:24 <HackEgo> ​` ^ ~ | _ - [ ] { } \ 0 1 5 9 a A k K `m z Z
11:53:34 <Taneb> shachaf, I've listed in the past
11:53:59 <shachaf> Taneb: there's a new opportunity for enlistment
11:54:07 <b_jonas> `` echo A K Z a k z [ \\ ] ^ _ \` { \| } \~ 0 1 5 9 - \`m ^m \~m \|m _m -m \[m \]m \{m \}m \\m 0m 1m 5m 9m | tr \ \\n | sort | tr \\n \
11:54:08 <HackEgo> ​` ^ ~ | _ - [ ] { } \ 0 0m 1 1m 5 5m 9 9m a A k K `m ^m ~m |m _m -m [m ]m {m }m \m z Z
11:54:57 <b_jonas> `` echo A K Z a k z a\`a a-a am | tr \ \\n | sort | tr \\n \
11:54:58 <HackEgo> a A a`a a-a am k K z Z
11:55:01 <boily> fungot: could you `list please? we give out free fnords today! limited time offer!
11:55:02 <fungot> boily: we have an element, we're ready to call the brainfuck datastructure? tape?
11:55:26 <boily> fungot: it's Taneb who's ready to call the brainfuck.
11:55:27 <fungot> boily: datum and data are so very painful in structure
11:55:30 <b_jonas> ok, so we need nicks something like a`a`a`a probably
11:55:41 -!- boily has changed nick to a`a`a`a.
11:55:44 <a`a`a`a> `list
11:55:50 <HackEgo> boily chicken_jonas lambdabot myname
11:55:55 -!- a`a`a`a has changed nick to boily.
11:55:55 -!- a`a`a`a`jonas0 has joined.
11:56:05 <a`a`a`a`jonas0> `list me
11:56:12 <HackEgo> a`a`a`a boily chicken_jonas lambdabot myname
11:56:34 <myname> it still pings
11:56:50 -!- a`a`a`a`jonas0 has changed nick to a`a`a`a`jo1as.
11:56:55 <a`a`a`a`jo1as> `list me
11:57:02 <HackEgo> a`a`a`a a`a`a`a`jonas0 boily chicken_jonas lambdabot myname
11:57:07 <izabera> what are you doooooiiing
11:57:26 <a`a`a`a`jo1as> izabera: trying to dos
11:57:35 <shachaf> why do you gotta sabotage it
11:57:37 <a`a`a`a`jo1as> izabera: by filling up the whole irc line
11:58:10 <a`a`a`a`jo1as> izabera: I think it backfired on me though, because actually just "jonas" pings me, although I might have to refine that rule because it gives too much
11:58:20 <a`a`a`a`jo1as> false positives on some chans
11:58:46 <myname> jonas is so big, it can hold several tb od data
11:58:46 <boily> izabera: izabellora! join the conscription! be part of a Great Project!
11:58:54 <a`a`a`a`jo1as> well, only \bjonas\b actually, but still
11:58:56 <izabera> what great project?
11:59:11 -!- a`a`a`a`jo1as has changed nick to a`a`a`a`jo2as.
11:59:19 <a`a`a`a`jo2as> `list me too
11:59:25 <HackEgo> a`a`a`a a`a`a`a`jo1as a`a`a`a`jonas0 boily chicken_jonas lambdabot myname
11:59:33 -!- a`a`a`a`jo2as has changed nick to a`a`a`a`jo3as.
11:59:44 <a`a`a`a`jo3as> `list everypony
11:59:48 -!- a`a`a`a`jo3as has changed nick to a`a`a`a`jo4as.
11:59:50 <HackEgo> a`a`a`a a`a`a`a`jo1as a`a`a`a`jo2as a`a`a`a`jonas0 boily chicken_jonas lambdabot myname
11:59:56 <izabera> it's probably easier if you set up a bot...
12:00:00 <izabera> or at least quicker
12:00:05 <a`a`a`a`jo4as> `list soon the too many nick changes rule will trigger on freenode
12:00:12 <HackEgo> a`a`a`a a`a`a`a`jo1as a`a`a`a`jo2as a`a`a`a`jo3as a`a`a`a`jonas0 boily chicken_jonas lambdabot myname
12:00:42 <a`a`a`a`jo4as> izabera: freenode has a rule on how fast it allows nick changes, so I can't do it fast anyway
12:00:44 <boily> everypony: wasn't it Vermin Supreme who said that?
12:00:58 <izabera> a`a`a`a`jo4as: surely you can use multiple users?
12:01:09 <a`a`a`a`jo4as> and besides, HackEgo output lines have a short enough caps, so it's not that difficult this way either
12:01:10 * izabera teaches ddosing 101
12:01:15 <shachaf> `` sed -i 's/sort -u/awk '\''!x[$0]++'\''/' bin/list
12:01:18 <HackEgo> No output.
12:01:31 -!- a`a`a`a`jo4as has changed nick to a`a`a`a`jo5as.
12:01:40 -!- oerjan has quit (Quit: `lost).
12:01:44 <a`a`a`a`jo5as> `list
12:01:48 <HackEgo> a`a`a`a`jo4as a`a`a`a`jo3as a`a`a`a`jo2as a`a`a`a`jo1as a`a`a`a`jonas0 a`a`a`a lambdabot chicken_jonas myname boily
12:02:03 <b_jonas> wait, why are the numbers sorted backwards?
12:02:15 <izabera> `cat bin/list
12:02:15 <HackEgo> date > share/conscripts; culprits share/conscripts | xargs -n 1 | awk '!x[$0]++' | xargs
12:02:17 <FireFly> Maybe they count backwards in new zealand
12:02:23 <FireFly> it's the southern hemisphere after all
12:02:29 <shachaf> FireFly++
12:02:32 <shachaf> makes perfect sense to me
12:02:44 -!- andrew has quit (Remote host closed the connection).
12:02:54 <izabera> xargs -n 1 is a crappy way to split a line
12:03:16 <FireFly> I usually fold -1
12:03:21 <b_jonas> `` echo 0 1 2 3 a0 a1 a2 a3 a0b a1k a2t a3f | tr \ \\n | sort | tr \\n \
12:03:22 <HackEgo> 0 1 2 3 a0 a0b a1 a1k a2 a2t a3 a3f
12:03:34 <FireFly> er hm, no
12:03:40 <b_jonas> FireFly: some people use awk '{print$1}'
12:03:50 <FireFly> I guess just tr \ \\n
12:03:51 <b_jonas> oh
12:03:57 <b_jonas> maybe it's sorted by date now?
12:04:05 -!- a`a`a`a`jo5as has changed nick to a`a`a`a`jo6as.
12:04:10 <a`a`a`a`jo6as> `list
12:04:12 -!- a`a`a`a`jo6as has changed nick to a`a`a`a`jo3as.
12:04:13 <FireFly> Looks like it
12:04:14 <a`a`a`a`jo3as> `list
12:04:15 <HackEgo> a`a`a`a`jo5as a`a`a`a`jo4as a`a`a`a`jo3as a`a`a`a`jo2as a`a`a`a`jo1as a`a`a`a`jonas0 a`a`a`a lambdabot chicken_jonas myname boily
12:04:20 <HackEgo> a`a`a`a`jo6as a`a`a`a`jo5as a`a`a`a`jo4as a`a`a`a`jo3as a`a`a`a`jo2as a`a`a`a`jo1as a`a`a`a`jonas0 a`a`a`a lambdabot chicken_jonas myname boily
12:04:33 -!- a`a`a`a`jo3as has changed nick to a`a`a`a`jo8as.
12:04:35 <a`a`a`a`jo8as> `list
12:04:38 -!- a`a`a`a`jo8as has changed nick to a`a`a`a`jo7as.
12:04:43 <HackEgo> a`a`a`a`jo3as a`a`a`a`jo6as a`a`a`a`jo5as a`a`a`a`jo4as a`a`a`a`jo2as a`a`a`a`jo1as a`a`a`a`jonas0 a`a`a`a lambdabot chicken_jonas myname boily
12:04:49 <boily> never in my life was I so much pinged in such a short time... I feel dirty...
12:05:01 <myname> boily: hi
12:05:05 <a`a`a`a`jo7as> `list
12:05:12 <boily> myname: bleh :P
12:05:12 <izabera> hey boily
12:05:12 <HackEgo> a`a`a`a`jo8as a`a`a`a`jo3as a`a`a`a`jo6as a`a`a`a`jo5as a`a`a`a`jo4as a`a`a`a`jo2as a`a`a`a`jo1as a`a`a`a`jonas0 a`a`a`a lambdabot chicken_jonas myname boily
12:05:18 <boily> izabera: flblblblblbl :P
12:05:24 <izabera> to you too
12:05:24 <b_jonas> oh! it's sorted backwards by _latest_ access
12:05:29 <b_jonas> then the dosing can't work
12:05:33 <shachaf> boily: maybe you'd better `list again just to be on the safe side hth
12:05:35 <b_jonas> or at least only afterwards
12:05:44 <b_jonas> because anyone who lists will get to the front immediately
12:05:46 <boily> `list
12:05:53 <boily> shachaf: I like to live dangerously.
12:05:54 <HackEgo> a`a`a`a`jo7as a`a`a`a`jo8as a`a`a`a`jo3as a`a`a`a`jo6as a`a`a`a`jo5as a`a`a`a`jo4as a`a`a`a`jo2as a`a`a`a`jo1as a`a`a`a`jonas0 a`a`a`a lambdabot chicken_jonas myname boily
12:05:54 <shachaf> b_jonas: yes, that was the goal
12:06:41 <a`a`a`a`jo7as> well, in that case
12:06:43 <shachaf> If you wanted to deny service, you could also, y'know, `rm bin/list
12:06:47 -!- a`a`a`a`jo7as has quit (Quit: this is useless).
12:06:56 <b_jonas> shachaf: nah, you'd just revert that
12:07:09 <b_jonas> which would probably even get me on the list since I deleted it
12:07:09 <shachaf> I can always switch from conscripts to another file.
12:13:46 <b_jonas> what if that command also printed " To unsubscribe, `unlist " or something?
12:14:06 <b_jonas> ``` find -name *list*
12:14:11 <HackEgo> ​./bdsmreclist \ ./wisdom/bdsmreclist
12:14:11 <b_jonas> ``` find -name "*list*"
12:14:15 <HackEgo> ​./bin/slist \ ./bin/listen \ ./bin/dontaskdonttelllist \ ./bin/don'taskdon'ttelllist \ ./bin/erflist \ ./bin/olist \ ./bin/flist \ ./bin/makelist \ ./bin/smlist \ ./bin/mlist \ ./bin/FireFlist \ ./bin/emptylist \ ./bin/testlist \ ./bin/llist \ ./bin/list \ ./bin/pbflist \ ./bin/danddreclist \ ./share/lua/5.2/luarocks/list.lua \ ./.hg/store/dh/no
12:14:33 <b_jonas> wow
12:14:54 <b_jonas> ``` cat bin/emptylist
12:14:55 <HackEgo> echo -n "$(basename "$0")${@:+ }$@: "; tail -n+2 "$0" | xargs; exit
12:15:02 <b_jonas> `type cat
12:15:03 <HackEgo> ​/home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: type: not found
12:15:07 <b_jonas> ``` type cat
12:15:08 <HackEgo> cat is /bin/cat
12:15:28 <b_jonas> hmm
12:15:50 <b_jonas> ``` perl -pe1 bin/emptylist
12:15:51 <HackEgo> echo -n "$(basename "$0")${@:+ }$@: "; tail -n+2 "$0" | xargs; exit
12:15:53 <b_jonas> ``` perl -pe1 bin/flist
12:15:54 <HackEgo> echo -n "$(basename "$0")${@:+ }$@: "; tail -n+2 "$0" | xargs; exit
12:15:56 <b_jonas> ``` perl -pe1 bin/slist
12:15:57 <HackEgo> echo -n "$(basename "$0")${@:+ }$@: "; tail -n+2 "$0" | xargs; exit \ Taneb \ atriq \ Ngevd \ nvd \ Fiora \ Sgeo \ ThatOtherPerson \ alot
12:16:14 <shachaf> are you pinging everyone
12:16:17 <b_jonas> argh
12:16:18 <shachaf> that's kind of rude
12:16:18 <b_jonas> sorry
12:16:28 <b_jonas> shouldn't those things be rot13-encoded _inside?
12:17:12 <b_jonas> ``` perl -pe'y/(\w)(\w)/$1.$2/' bin/mlist
12:17:12 <HackEgo> echo Seeing a philosopher
12:17:17 <b_jonas> ``` perl -pe'y/(\w)(\w)/$1.$2/' bin/smlist
12:17:18 <HackEgo> echo -n "$$basename "$0".${@:+ }$@: "; tail -n+2 "$0" | xargs; exit \ shachaf \ monqy \ elliott \ mnoqy
12:17:32 <b_jonas> argh
12:17:33 <shachaf> that still pings me tdnh
12:17:35 <b_jonas> ``` perl -pe'y/(\w)(\w)/$1.$2/g' bin/smlist
12:17:36 <HackEgo> Bareword found where operator expected at -e line 1, near "y/(\w)(\w)/$1.$2/g" \ syntax error at -e line 1, near "y/(\w)(\w)/$1.$2/g \ " \ Execution of -e aborted due to compilation errors.
12:17:41 <b_jonas> ``` perl -pe's/(\w)(\w)/$1.$2/g' bin/smlist
12:17:42 <HackEgo> e.ch.o -n "$(b.as.en.am.e "$0")${@:+ }$@: "; t.ai.l -n+2 "$0" | x.ar.gs; e.xi.t \ s.ha.ch.af \ m.on.qy \ e.ll.io.tt \ m.no.qy
12:18:02 <b_jonas> wait, there's a pbflist?
12:18:08 <b_jonas> ``` perl -pe's/(\w)(\w)/$1.$2/g' bin/pbflist
12:18:08 <HackEgo> e.ch.o -n "$(b.as.en.am.e "$0")${@:+ }$@: "; t.ai.l -n+2 "$0" | x.ar.gs; e.xi.t \ s.ha.ch.af \ S.ge.o \ q.ui.nt.op.ia \ i.on
12:18:55 <Taneb> `rot13 Ngevd
12:18:56 <HackEgo> Atriq
12:19:01 <b_jonas> ``` perl -pe'$O=shift;open O;print O "b_jonas\n"' bin/pbflist
12:19:02 <HackEgo> echo -n "$(basename "$0")${@:+ }$@: "; tail -n+2 "$0" | xargs; exit \ shachaf \ Sgeo \ quintopia \ ion
12:19:17 <b_jonas> no no
12:19:19 <b_jonas> `revert
12:19:21 <HackEgo> rm: cannot remove `/home/hackbot/hackbot.hg/multibot_cmds/env/.hg/store/data/canary.orig': Is a directory \ Done.
12:19:23 <shachaf> still pinging me
12:19:42 <b_jonas> ``` perl -we'$O=shift;open O,">>",$O;print O "b_jonas\n"' bin/pbflist
12:19:44 <HackEgo> No output.
12:19:53 <b_jonas> ``` perl -pe's/(\w)(\w)/$1.$2/g' bin/pbflist
12:19:54 <HackEgo> e.ch.o -n "$(b.as.en.am.e "$0")${@:+ }$@: "; t.ai.l -n+2 "$0" | x.ar.gs; e.xi.t \ s.ha.ch.af \ S.ge.o \ q.ui.nt.op.ia \ i.on \ b._j.on.as
12:19:57 <b_jonas> there
12:20:13 <b_jonas> sorry everyone for all the pinging
12:20:43 <b_jonas> ``` perl -pe's/(\w)(\w)/$1.$2/g' bin/flist
12:20:44 <HackEgo> e.ch.o -n "$(b.as.en.am.e "$0")${@:+ }$@: "; t.ai.l -n+2 "$0" | x.ar.gs; e.xi.t
12:20:46 <b_jonas> ``` perl -pe's/(\w)(\w)/$1.$2/g' bin/llist
12:20:47 <HackEgo> e.ch.o -n "$(b.as.en.am.e "$0")${@:+ }$@: "; t.ai.l -n+2 "$0" | x.ar.gs; e.xi.t \ d.an.is.h
12:21:14 -!- J_Arcane has quit (Ping timeout: 244 seconds).
12:21:15 -!- boily has quit (Quit: TEAM CHICKEN).
12:22:32 <b_jonas> ``` perl -e-e($t="bin/wrlist")and die;use File::Copy;copy("bin/flist",$t)
12:22:33 <HackEgo> bash: -c: line 0: syntax error near unexpected token `(' \ bash: -c: line 0: `perl -e-e($t="bin/wrlist")and die;use File::Copy;copy("bin/flist",$t)'
12:22:39 <b_jonas> `perl -e-e($t="bin/wrlist")and die;use File::Copy;copy("bin/flist",$t)
12:22:41 <HackEgo> No output.
12:22:49 <b_jonas> ``` perl -pe's/(\w)(\w)/$1.$2/g' bin/wrlist
12:22:50 <HackEgo> e.ch.o -n "$(b.as.en.am.e "$0")${@:+ }$@: "; t.ai.l -n+2 "$0" | x.ar.gs; e.xi.t
12:25:09 <b_jonas> ``` find -name "*list*" | tail -n16
12:25:12 <HackEgo> ​./src/ploki/list.c \ ./src/ploki/examples/list.pk \ ./src/ploki/list.h \ ./src/ploki/list.depend \ ./bdsmreclist \ ./interps/cfunge/cfunge-src/tools/gen_fprint_list.sh \ ./interps/clc-intercal/inst/lib/perl5/x86_64-linux-gnu-thread-multi/auto/Language/INTERCAL/.packlist \ ./wisdom/herbalist \ ./wisdom/slist \ ./wisdom/kallisti \ ./wisdom/olist \
12:25:36 <b_jonas> ``` find -name "*list*" | sort
12:25:39 <HackEgo> ​./.hg/store/data/bdsmreclist..i \ ./.hg/store/data/bdsmreclist.i \ ./.hg/store/data/bin/_fire_flist.i \ ./.hg/store/data/bin/danddreclist.i \ ./.hg/store/data/bin/deletedlist.i \ ./.hg/store/data/bin/don'taskdon'ttelllist.i \ ./.hg/store/data/bin/dontaskdonttelllist.i \ ./.hg/store/data/bin/elist.i \ ./.hg/store/data/bin/emptylist.i \ ./.hg/stor
12:25:53 <b_jonas> ``` find * -name "*list*" | sort
12:25:54 <HackEgo> bdsmreclist \ bin/FireFlist \ bin/danddreclist \ bin/don'taskdon'ttelllist \ bin/dontaskdonttelllist \ bin/emptylist \ bin/erflist \ bin/flist \ bin/list \ bin/listen \ bin/llist \ bin/makelist \ bin/mlist \ bin/olist \ bin/pbflist \ bin/slist \ bin/smlist \ bin/testlist \ bin/wrlist \ interps/cfunge/cfunge-src/tools/gen_fprint_list.sh \ interps/cl
12:25:57 <b_jonas> ``` find * -name "*list*" | sort | tail -n10
12:25:58 <HackEgo> src/ploki/list.h \ wisdom/bdsmreclist \ wisdom/danddreclist \ wisdom/herbalist \ wisdom/kallisti \ wisdom/list \ wisdom/olist \ wisdom/slist \ wisdom/smlist \ wisdom/supercalifragilisticexponential growth
12:26:10 <b_jonas> ``` find * -name "*list*" | sort | tail -n-10
12:26:12 <HackEgo> src/ploki/list.h \ wisdom/bdsmreclist \ wisdom/danddreclist \ wisdom/herbalist \ wisdom/kallisti \ wisdom/list \ wisdom/olist \ wisdom/slist \ wisdom/smlist \ wisdom/supercalifragilisticexponential growth
12:26:19 <b_jonas> huh?
12:26:21 <b_jonas> ``` find * -name "*list*" | sort | tail -n+10
12:26:23 <HackEgo> bin/listen \ bin/llist \ bin/makelist \ bin/mlist \ bin/olist \ bin/pbflist \ bin/slist \ bin/smlist \ bin/testlist \ bin/wrlist \ interps/cfunge/cfunge-src/tools/gen_fprint_list.sh \ interps/clc-intercal/inst/lib/perl5/x86_64-linux-gnu-thread-multi/auto/Language/INTERCAL/.packlist \ share/lua/5.2/luarocks/list.lua \ src/ploki/examples/list.pk \ sr
12:26:25 <b_jonas> ah
12:26:33 <b_jonas> ``` find * -name "*list*" | sort | tail -n+20
12:26:35 <HackEgo> interps/cfunge/cfunge-src/tools/gen_fprint_list.sh \ interps/clc-intercal/inst/lib/perl5/x86_64-linux-gnu-thread-multi/auto/Language/INTERCAL/.packlist \ share/lua/5.2/luarocks/list.lua \ src/ploki/examples/list.pk \ src/ploki/list.c \ src/ploki/list.depend \ src/ploki/list.h \ wisdom/bdsmreclist \ wisdom/danddreclist \ wisdom/herbalist \ wisdom/ka
12:27:26 <b_jonas> ``` find * -name "*list*" | sort | tail -n+30
12:27:28 <HackEgo> wisdom/kallisti \ wisdom/list \ wisdom/olist \ wisdom/slist \ wisdom/smlist \ wisdom/supercalifragilisticexponential growth
12:29:36 <b_jonas> ``` cwd
12:29:37 <HackEgo> bash: cwd: command not found
12:29:40 <b_jonas> ``` pwd
12:29:40 <HackEgo> ​/hackenv
12:30:52 <b_jonas> ``` perl -pe1 /hackenv/bin/\`\`
12:30:53 <HackEgo> ​#!/bin/sh \ export LANG=C; exec bash -O extglob -c "$@"
12:32:02 <b_jonas> `perl -eopen$O,">","bin/listlist",755;print$O qq{#!/bin/sh\nset -e\nexport LANG=C\ncd /hackenv/bin;exec ls -dF *[lL]ist*\n};
12:32:03 <HackEgo> More than one argument to open(,':perlio') at -e line 1.
12:32:41 <b_jonas> `perl -eopen$O,">",($c="bin/listlist");print$O qq{#!/bin/sh\nset -e\nexport LANG=C\ncd /hackenv/bin;exec ls -dF *[lL]ist*\n};close$O;chmod $c,0755;
12:32:43 <HackEgo> No output.
12:32:47 <b_jonas> `listlist
12:32:47 <HackEgo> ​/home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: /hackenv/bin/listlist: Permission denied \ /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: /hackenv/bin/listlist: cannot execute: Permission denied
12:32:51 <fizzie> ^save
12:32:51 <fungot> OK.
12:33:07 <b_jonas> ``` ls -ld bin/listlist
12:33:08 <HackEgo> ​-rw-r--r-- 1 5000 0 69 Feb 24 12:32 bin/listlist
12:33:18 <fizzie> @tell oerjan ^saved htdh
12:33:18 <lambdabot> Consider it noted.
12:33:55 <b_jonas> `perl -e$c="bin/listlist";chmod 0755,$c or die"chmod:$!";
12:33:58 <HackEgo> No output.
12:34:10 <b_jonas> `listlist
12:34:11 <HackEgo> FireFlist* \ danddreclist* \ don'taskdon'ttelllist@ \ dontaskdonttelllist* \ emptylist* \ erflist* \ flist* \ list* \ listen* \ listlist* \ llist* \ makelist* \ mlist* \ olist* \ pbflist* \ slist* \ smlist* \ testlist* \ wrlist
12:34:18 <b_jonas> stupid perl, having function arguments backwards
12:35:14 <b_jonas> ``` perl -pe's/(\w)(\w)/$1.$2/g' bin/makelist
12:35:15 <HackEgo> c.p b.in/e.mp.ty.li.st b.in/"$1"
12:36:39 <b_jonas> ``` ls -d */
12:36:39 <HackEgo> bin/ \ emoticons/ \ etc/ \ evil/ \ factor/ \ good/ \ hw/ \ ibin/ \ interps/ \ le/ \ lib/ \ misle/ \ paste/ \ quines/ \ share/ \ src/ \ tmflry/ \ wisdom/
12:37:06 <b_jonas> ``` ls -d share/*/ lib/*/
12:37:07 <HackEgo> ls: cannot access lib/*/: No such file or directory \ share/WordData/ \ share/delvs-master/ \ share/lua/
12:47:33 -!- AnotherTest has joined.
12:52:10 -!- AnotherTest has quit (Ping timeout: 252 seconds).
13:16:29 -!- lynn has joined.
13:19:14 -!- lynn_ has joined.
13:20:13 -!- Nithogg has quit (Quit: WeeChat 1.4).
13:22:17 -!- Nithogg has joined.
13:22:37 -!- lynn has quit (Ping timeout: 255 seconds).
13:24:18 -!- tromp_ has joined.
13:27:09 -!- Nithogg has quit (Quit: WeeChat 1.4).
13:28:26 -!- tromp_ has quit (Ping timeout: 244 seconds).
13:42:01 <b_jonas> ``` perl -pe's/(\w)(\w)/$1.$2/g' bin/alist
13:42:02 <HackEgo> Can't open bin/alist: No such file or directory.
13:42:04 <b_jonas> ``` perl -pe's/(\w)(\w)/$1.$2/g' bin/aglist
13:42:05 <HackEgo> Can't open bin/aglist: No such file or directory.
13:42:20 <b_jonas> `makelist aglist
13:42:22 <HackEgo> No output.
13:42:25 <b_jonas> ``` perl -pe's/(\w)(\w)/$1.$2/g' bin/aglist
13:42:26 <HackEgo> e.ch.o -n "$(b.as.en.am.e "$0")${@:+ }$@: "; t.ai.l -n+2 "$0" | x.ar.gs; e.xi.t
13:42:41 <b_jonas> ``` perl -pe's/(\w)(\w)/$1.$2/g' bin/wrlist
13:42:42 <HackEgo> e.ch.o -n "$(b.as.en.am.e "$0")${@:+ }$@: "; t.ai.l -n+2 "$0" | x.ar.gs; e.xi.t
13:43:59 <b_jonas> `perl -efor $comic("ag","wr"){open$O,">>","bin/${comic}list";print$O"b_jonas\n";}
13:44:01 <HackEgo> String found where operator expected at -e line 1, near "$O"b_jonas\n"" \ (Missing operator before "b_jonas\n"?)
13:44:22 -!- tromp_ has joined.
13:44:26 <b_jonas> `perl -efor $comic("ag","wr"){open$O,">>","bin/${comic}list";print$O "b_jonas\n";}
13:44:29 <HackEgo> No output.
13:44:38 <b_jonas> ``` perl -pe's/(\w)(\w)/$1.$2/g' bin/wrlist
13:44:39 <HackEgo> e.ch.o -n "$(b.as.en.am.e "$0")${@:+ }$@: "; t.ai.l -n+2 "$0" | x.ar.gs; e.xi.t \ b._j.on.as \ b._j.on.as
13:50:06 <FireFly> `cat bin/FireFlist
13:50:07 <HackEgo> echo FireFly Eldis4
13:50:08 <b_jonas> `? giraffefolk
13:50:09 <HackEgo> giraffefolk? ¯\(°​_o)/¯
13:50:11 <b_jonas> `? merfolk
13:50:12 <FireFly> ok
13:50:13 <HackEgo> merfolk? ¯\(°​_o)/¯
13:50:20 <FireFly> `culprits bin/FireFlist
13:50:21 <b_jonas> `? siren
13:50:22 <HackEgo> nortti nortti
13:50:22 <HackEgo> siren? ¯\(°​_o)/¯
13:50:24 <b_jonas> `? sphinx
13:50:25 <HackEgo> sphinx? ¯\(°​_o)/¯
13:50:28 <b_jonas> `? asphinx
13:50:29 <HackEgo> asphinx? ¯\(°​_o)/¯
13:53:34 <int-e> @metar KSFO
13:53:46 <lambdabot> KSFO 241256Z 00000KT 10SM FEW110 SCT150 11/11 A3011 RMK AO2 SLP195 T01060106 $
13:54:16 -!- tjt263_ has joined.
13:55:16 -!- lynn__ has joined.
13:58:22 -!- lynn_ has quit (Ping timeout: 244 seconds).
13:59:25 -!- tromp_ has quit (Remote host closed the connection).
14:16:11 <b_jonas> [ 366%~132141
14:16:11 <j-bot> b_jonas: 361.041
14:22:55 -!- `^_^v has joined.
14:23:42 -!- lynn_ has joined.
14:24:14 -!- lynn__ has quit (Ping timeout: 244 seconds).
14:30:29 -!- impomatic_ has joined.
14:37:40 -!- lambdabot has quit (Ping timeout: 264 seconds).
14:43:09 -!- lambdabot has joined.
14:57:30 -!- mad has quit (Ping timeout: 276 seconds).
15:00:07 -!- tromp_ has joined.
15:04:30 -!- tromp_ has quit (Ping timeout: 244 seconds).
15:19:25 -!- jaboja has joined.
15:19:39 -!- Yurume has quit (Ping timeout: 264 seconds).
15:22:13 -!- AnotherTest has joined.
15:34:58 -!- jaboja has quit (Ping timeout: 252 seconds).
15:42:54 -!- Treio has quit (Quit: Leaving).
16:00:37 -!- lynn has joined.
16:01:55 -!- lynn_ has quit (Ping timeout: 255 seconds).
16:02:20 <Taneb> This brainfuck competition is going well
16:02:31 <Taneb> Turns out it lasts all week and this is just an intro
16:03:51 <prooftechnique> Is the competition implementing brainfuck, or using it?
16:04:30 <prooftechnique> I assume the latter, but you never know
16:04:51 -!- lambda-11235 has joined.
16:07:19 -!- jaboja has joined.
16:10:06 <Taneb> The latter
16:31:10 -!- earendel2 has joined.
16:32:05 -!- earendel has quit (Ping timeout: 250 seconds).
16:34:41 -!- shikhin has changed nick to SHIKHIN.
16:34:51 -!- SHIKHIN has changed nick to shikhin.
16:48:38 <Taneb> I'm gonna need a more efficient divmod algorithm
16:50:04 <izabera> divmod (a, b) { return 7, 0 }
16:50:31 <Taneb> izabera: that woudn't quite work for calculating the largest prime factor of 2^32-2
16:50:48 <izabera> it's correct in an infinite number of cases
16:52:17 <izabera> implement a primality test instead of trial division only
16:52:19 <izabera> 2147483647 is prime
16:55:23 <Taneb> That could work!
17:00:02 -!- tromp_ has joined.
17:02:18 -!- jaboja has quit (Ping timeout: 276 seconds).
17:02:25 -!- earendel2 has quit (Ping timeout: 252 seconds).
17:04:37 -!- tromp_ has quit (Ping timeout: 252 seconds).
17:19:53 -!- Treio has joined.
17:21:29 -!- lynn has quit (Ping timeout: 240 seconds).
17:21:45 -!- Treio has quit (Remote host closed the connection).
17:28:03 -!- AnotherTest has quit (Ping timeout: 248 seconds).
17:28:04 -!- Sprocklem has quit (Ping timeout: 248 seconds).
17:41:44 -!- Treio has joined.
17:46:41 <izabera> hey, how do i move up and down in vi without arrows?
17:46:47 <izabera> j/k :P
17:51:51 -!- lynn has joined.
18:01:24 -!- tromp_ has joined.
18:03:37 <lambda-11235> izabera: Use the mouse scrollwheel. :)
18:05:33 -!- tromp_ has quit (Ping timeout: 240 seconds).
18:08:03 <izabera> izabera | j/k :P <---- cough cough
18:08:19 <izabera> cmon it was funny
18:10:55 -!- tjt263_ has quit (Quit: part).
18:16:51 -!- Treio has quit (Quit: Leaving).
18:19:00 <Taneb> izabera, I thought it was funny
18:20:49 <izabera> :3
18:22:10 -!- hppavilion[1] has joined.
18:24:24 -!- AnotherTest has joined.
18:32:15 <prooftechnique> I wonder what the initial investment is like to become a carilloneur/euse
18:35:37 <hppavilion[1]> What other interesting branches of mathematics could a Proof Assistant be based on?
18:35:44 <hppavilion[1]> I have string rewriting down, mostly.
18:35:53 <prooftechnique> HoTT
18:36:10 <hppavilion[1]> prooftechnique: HoTT? Is that for me?
18:36:22 <prooftechnique> Yeah.
18:37:38 <hppavilion[1]> prooftechnique: OK...
18:37:51 <hppavilion[1]> prooftechnique: Anything non-type theoretical?
18:37:54 <prooftechnique> There's probably something insane you could do with stack theory, too, but I think there are probably 2 people in the world who know anything about that
18:38:42 <prooftechnique> https://en.wikipedia.org/wiki/Stack_%28mathematics%29
18:38:42 <hppavilion[1]> prooftechnique: I assume stack theory is based on the stack?
18:38:46 <quintopia> izabera: i internally chuckled
18:38:47 <hppavilion[1]> Yep
18:39:06 <hppavilion[1]> https://en.wikipedia.org/w/index.php?title=Glossary_of_stack_theory&redirect=no
18:39:25 <hppavilion[1]> prooftechnique: Is stack theory a real, studied thing?
18:40:03 <hppavilion[1]> Oh, nothing to do with a stack then?
18:40:04 <prooftechnique> I think they actually call it descent theory
18:40:31 <prooftechnique> http://arxiv.org/abs/math/0412512
18:40:41 <prooftechnique> Well, not the sort of stack computers are concerned with, no
18:41:13 <prooftechnique> Though, maybe. It's an abstruse field. There could very well be a connection :D
18:42:23 -!- AlexR42 has joined.
18:43:04 <prooftechnique> Though, note https://en.wikipedia.org/wiki/Stack_(mathematics)#Set-theoretical_problems
18:43:29 -!- carado has quit (Ping timeout: 240 seconds).
18:44:25 <prooftechnique> And Grothendieck has some texts on the subject, but I think they're mainly in French
18:45:12 <hppavilion[1]> prooftechnique: Any other ideas? Something I might find easier to understand? xD
18:45:19 -!- carado has joined.
18:46:09 <prooftechnique> I was reading about Lemuridae the other day, and superdeduction sounds neat
18:46:40 <prooftechnique> http://rho.loria.fr/lemuridae.html http://citeseerx.ist.psu.edu/viewdoc/summary?doi=
18:48:04 <hppavilion[1]> I don't understand Category Theory, so I figure it's a good idea to implement it in Python to start understanding it xD
18:49:40 <hppavilion[1]> prooftechnique: Is it even possible to implement category theory in a programming language without being a god?
18:50:24 <hppavilion[1]> prooftechnique: It seems like you'd have to do a LOT of lazy evaluation
18:51:30 <prooftechnique> Define "implement category theory". Like, be able to represent it, or be able to do things with it?
18:52:02 <prooftechnique> Because there's this, I guess: http://docs.sympy.org/latest/modules/categories.html
18:52:03 <hppavilion[1]> prooftechnique: Have something that works well enough for me to play with it and see what's going on
18:52:23 <hppavilion[1]> prooftechnique: If I implement it myself, I'll have a better feel for how it works, most likely
18:54:21 <prooftechnique> Well, what do you want to be able to do? It seem pretty straightforward to have Python objects for Objects, Morphisms, and Categories
18:54:25 <prooftechnique> *seems
18:54:47 <prooftechnique> Then you just follow the math, more or less.
18:54:59 <prooftechnique> Now, proving things is another matter, I suppose.
18:55:41 <prooftechnique> Oh, and Diagrams would be good to have, I guess
18:57:27 <hppavilion[1]> prooftechnique: Yeah, that's what I'm working on. Python objects.
18:58:48 -!- bb010g has quit (Quit: Connection closed for inactivity).
19:11:59 -!- carado has quit (Ping timeout: 250 seconds).
19:15:38 -!- hppavilion[1] has quit (Ping timeout: 244 seconds).
19:25:51 -!- carado has joined.
19:28:02 -!- hppavilion[1] has joined.
19:38:59 -!- carado has quit (Ping timeout: 240 seconds).
19:41:39 -!- Sprocklem has joined.
19:49:48 -!- carado has joined.
19:51:37 -!- Phantom_Hoover has joined.
20:08:52 -!- hppavilion[1] has quit (Ping timeout: 252 seconds).
20:10:40 -!- l0de has joined.
20:11:02 <l0de> yes hello, sorcerer l0de here
20:11:22 <l0de> I'm looking for fellow arcane practitioners to work with in the NYC area
20:11:32 <Phantom_Hoover> wrong kind of esoteric mate
20:11:50 <Phantom_Hoover> `welcome
20:11:51 <l0de> There are no wrong kinds, Phantom_Hoover, only different paths
20:12:00 <HackEgo> Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: <http://esolangs.org/>. (For the other kind of esoterica, try #esoteric on EFnet or DALnet.)
20:12:34 <Phantom_Hoover> l0de, well yes but we do ask that you focus your exploration of the arcane into designing or deploying esoteric programming languages
20:13:17 <l0de> I've always considered myself as more of a chaos-affiliated magus, Phantom_Hoover
20:13:46 <Phantom_Hoover> that's ok, we have chaotic esolangs as well
20:14:20 -!- hppavilion[1] has joined.
20:17:25 -!- bender| has quit (Ping timeout: 250 seconds).
20:24:29 -!- Sprocklem has quit (Ping timeout: 240 seconds).
20:33:05 -!- J_Arcane has joined.
20:33:55 -!- lambda-11235 has quit (Quit: Bye).
20:44:46 -!- mihow has joined.
20:45:27 -!- Sprocklem has joined.
20:56:10 -!- hppavilion[1] has quit (Ping timeout: 252 seconds).
21:12:38 -!- hppavilion[1] has joined.
21:34:40 -!- hppavilion[1] has quit (Ping timeout: 252 seconds).
21:49:26 -!- oerjan has joined.
21:50:00 <oerjan> @messages-good
21:50:00 <lambdabot> fizzie said 9h 16m 42s ago: ^saved htdh
21:51:48 <oerjan> `cat bin/list
21:51:54 <HackEgo> date > share/conscripts; culprits share/conscripts | xargs -n 1 | awk '!x[$0]++' | xargs
21:52:17 <oerjan> oh i see, that was why it was changed to awk
21:52:35 <b_jonas> `? rint
21:52:38 <HackEgo> rint? ¯\(°​_o)/¯
21:53:11 <oerjan> `cat bin/culprits
21:53:11 <HackEgo> hg log --removed "$1" | grep summary: | awk '{print substr($2,2,length($2)-2)}' | sed "s/.$/\x0F&/" | xargs
21:53:21 <oerjan> oh right
21:53:53 <oerjan> shachaf: it is good you are not using noping there, because it would mess up the removal of duplicates
21:54:12 <oerjan> i was wondering why that wasn't happening
21:56:35 <b_jonas> ``` grep -l "\bhg\b" bin/*
21:56:38 <HackEgo> bin/culprits \ bin/emmental \ bin/macro \ bin/mov \ bin/searchlog \ bin/tclkit \ bin/undo \ bin/units \ bin/url \ bin/word
21:57:48 -!- hppavilion[1] has joined.
21:58:51 <b_jonas> `perl -elocal$/;open$I,"<","bin/mov" or die;print<$I>=~s/\b(\w)(\w)/$1\x0f$2/g
21:58:52 <HackEgo> Can't modify <HANDLE> in substitution (s///) at -e line 1, at EOF \ Execution of -e aborted due to compilation errors.
21:59:03 <b_jonas> `perl -elocal$/;open$I,"<","bin/mov" or die;print<$I>=~s/\b(\w)(\w)/$1\x0f$2/gr
21:59:04 <HackEgo> ​ELF............>.....`6@.....@.......(..........@.8..@.........@.......@.@.....@.@................................8......8@.....8@............................................@.......@................... ..................a.....a...........
21:59:12 <b_jonas> whoa, binary?
21:59:15 <b_jonas> what's it do?
21:59:33 <b_jonas> `perl -elocal$/;open$I,"<","bin/searchlog" or die;print<$I>=~s/\b(\w)(\w)/$1\x0f$2/gr
21:59:35 <HackEgo> ​ELF............>.....p5@.....@.......g.........@.8..@.(.%.......@.......@.@.....@.@........................................@......@............................................@.......@.....L3.....L3....... ............P3.....P3k.....P3k.....8......XW........ ...........3.....3k.....3k...................
21:59:43 <b_jonas> `perl -elocal$/;open$I,"<","bin/undo" or die;print<$I>=~s/\b(\w)(\w)/$1\x0f$2/gr
21:59:44 <HackEgo> ​#!/bin/sh \ hg diff -c "$@" | patch -p1 -R
21:59:50 <APic> lol
21:59:55 <b_jonas> `perl -elocal$/;open$I,"<","bin/url" or die;print<$I>=~s/\b(\w)(\w)/$1\x0f$2/gr
21:59:55 <HackEgo> ​#!/usr/bin/env python \ import sys, os.path, re, urllib \ if len(sys.argv) <= 1: \ print "http://codu.org/projects/hackbot/fshg/" \ else: \ f = os.path.abspath(sys.argv[1]) \ f = re.sub(r"^/+hackenv/", "", f) \ if re.match(r"/|\.hg(?:/|$)",f): \ sys.exit("File is outside web-viewab
22:00:01 <APic> Nice Blinks
22:00:04 <APic> Here on my irssi
22:00:05 <b_jonas> `perl -elocal$/;open$I,"<","bin/word" or die;print<$I>=~s/\b(\w)(\w)/$1\x0f$2/gr
22:00:06 <HackEgo> ​#!/usr/bin/perl \ $VAR1 = { \ 'qz' => { \ 'e' => 1, \ 'k' => 1, \ 'a' => 1, \ ' ' => 9, \ 'i' => 1, \ 'o' => 2 \ }, \ 'sp' => { \ 'w' => 9, \ '
22:00:26 <shachaf> ``` rgrep -l --binary-files=without-match "\bhg\b" bin
22:00:27 <HackEgo> bin/url \ bin/undo \ bin/culprits \ bin/word
22:00:29 <APic> (Probably „Ctrl-F“)
22:00:30 <b_jonas> `perl -elocal$/;open$I,"<","bin/macro" or die;print<$I>=~s/\b(\w)(\w)/$1\x0f$2/gr
22:00:31 <HackEgo> ​ELF...........>.....`@.....@.......,.........@.8..@.'.$..................@.......@.....(.....(....... ............(.............................. ...................@......@.....h.......h....................(...............0.......`..............Qtd..................................................R
22:00:33 <shachaf> now leave the ELF files alone
22:01:00 <b_jonas> shachaf: sorry
22:01:04 <zgrep> Leave the elves alone? :P
22:01:06 <shachaf> ?
22:01:12 <zgrep> They need supervision.
22:01:42 <shachaf> That was to b_jonas.
22:01:45 <shachaf> Anyway.
22:01:45 <b_jonas> ``` objdump -f bin/mov
22:01:46 <HackEgo> ​ \ bin/mov: file format elf64-x86-64 \ architecture: i386:x86-64, flags 0x00000112: \ EXEC_P, HAS_SYMS, D_PAGED \ start address 0x0000000000403660
22:01:55 <b_jonas> ``` objdump -fh bin/mov
22:01:56 <HackEgo> ​ \ bin/mov: file format elf64-x86-64 \ architecture: i386:x86-64, flags 0x00000112: \ EXEC_P, HAS_SYMS, D_PAGED \ start address 0x0000000000403660 \ \ Sections: \ Idx Name Size VMA LMA File off Algn \ 0 .interp 0000001c 0000000000400238 0000000000400238 00000238 2**0 \
22:02:12 <b_jonas> ``` objdump -fh bin/mov | tail -n+8
22:02:13 <HackEgo> Idx Name Size VMA LMA File off Algn \ 0 .interp 0000001c 0000000000400238 0000000000400238 00000238 2**0 \ CONTENTS, ALLOC, LOAD, READONLY, DATA \ 1 .note.ABI-tag 00000020 0000000000400254 0000000000400254 00000254 2**2 \ CONTENTS, ALLOC, LOAD, READONLY
22:02:29 <b_jonas> ``` ldd bin/mov
22:02:29 <HackEgo> ​linux-vdso.so.1 => (0x0000007fbffff000) \ libselinux.so.1 => /lib/x86_64-linux-gnu/libselinux.so.1 (0x0000000040002000) \ librt.so.1 => /lib/x86_64-linux-gnu/librt.so.1 (0x0000000040222000) \ libacl.so.1 => /lib/x86_64-linux-gnu/libacl.so.1 (0x000000004042b000) \ libattr.so.1 => /lib/x86_64-linux-gnu/libattr.so.1 (0x0000000040634000) \ li
22:03:05 <b_jonas> ``` ldd bin/mov | tail -n+5
22:03:05 <HackEgo> ​libattr.so.1 => /lib/x86_64-linux-gnu/libattr.so.1 (0x0000000040634000) \ libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x0000000040839000) \ libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x0000000040bc4000) \ /lib64/ld-linux-x86-64.so.2 (0x000000552aaaa000) \ libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x0000000040dc8000)
22:03:14 -!- tromp_ has joined.
22:03:18 <b_jonas> ``` ldd bin/mov | tail -n+10
22:03:19 <HackEgo> No output.
22:03:56 <b_jonas> ``` objdump -t bin/mov
22:03:57 <HackEgo> ​ \ bin/mov: file format elf64-x86-64 \ \ SYMBOL TABLE: \ no symbols
22:04:19 <b_jonas> what the heck is this mov thing?
22:04:51 <shachaf> `mov
22:04:52 <HackEgo> mov: missing file operand \ Try `mov --help' for more information.
22:04:55 <shachaf> `mov --help
22:04:55 <HackEgo> Usage: mov [OPTION]... [-T] SOURCE DEST \ or: mov [OPTION]... SOURCE... DIRECTORY \ or: mov [OPTION]... -t DIRECTORY SOURCE... \ Rename SOURCE to DEST, or move SOURCE(s) to DIRECTORY. \ \ Mandatory arguments to long options are mandatory for short options too. \ --backup[=CONTROL] make a backup of each existing destination file \
22:05:20 <shachaf> `` ls -l bin/mov
22:05:21 <HackEgo> lrwxrwxrwx 1 5000 0 7 Dec 9 04:12 bin/mov -> /bin/mv
22:05:28 <shachaf> hth
22:05:35 <b_jonas> hmm
22:05:59 <b_jonas> yes, that halep
22:06:00 <shachaf> `` hg log --removed bin/mov | grep summary:
22:06:05 <b_jonas> strange one, but helps
22:06:13 <HackEgo> summary: <tswett> revert \ summary: <tswett> rm bin -r \ summary: <oerjan> revert \ summary: <elliott> revert 1 \ summary: <kmc> ln -s /bin/mv bin/mov
22:07:46 -!- tromp_ has quit (Ping timeout: 255 seconds).
22:08:54 -!- `^_^v has quit (Quit: This computer has gone to sleep).
22:10:05 -!- AlexR42 has quit (Quit: My Mac has gone to sleep. ZZZzzz…).
22:10:10 -!- `^_^v has joined.
22:21:25 -!- hppavilion[1] has quit (Ping timeout: 252 seconds).
22:21:46 -!- `^_^v has quit (Quit: This computer has gone to sleep).
22:21:57 -!- `^_^v has joined.
22:26:41 -!- AnotherTest has quit (Quit: ZNC - http://znc.in).
22:27:44 <oerjan> `cat bin/noping
22:27:46 <HackEgo> print_args_or_input "$@" | sed 's/\(..\)/\1​/g'
22:27:59 -!- llue has quit (Quit: That's what she said).
22:28:01 <b_jonas> wtf
22:28:08 -!- lleu has joined.
22:28:11 <oerjan> shachaf: on second thought `noping wouldn't be a problem if it's done before merging the lines
22:28:21 <b_jonas> wtfwtf
22:28:40 <oerjan> b_jonas: what is the problem cwh
22:29:51 <oerjan> shachaf: however, we really should find a noping method that works for everyone. i saw boily complaining in the logs.
22:30:05 <b_jonas> I just found out that in C++, std::allocator::difference_type is a typedef for ptrdiff_t. That totally doesn't make sense. That could be larger than the object sizes.
22:30:43 <oerjan> ok chyt
22:30:59 <oerjan> *cnhyt
22:31:05 <b_jonas> Admittedly they also couldn't just make it the signed type of the same size as size_t, because that type could be _smaller_ than the object sizes on some platforms,
22:31:08 <b_jonas> but still.
22:31:14 <b_jonas> It's weird.
22:31:32 <oerjan> hm cn seems wrong too, and there is no good way
22:31:46 <b_jonas> `? cn
22:31:47 <HackEgo> cn? ¯\(°​_o)/¯
22:32:18 <oerjan> because can always merges with a following not _somehow_, unless it has a different meaning
22:34:37 <oerjan> <FireFly> I usually fold -1 <-- hm i should remember that command
22:34:44 <oerjan> (with or without -1)
22:34:52 <b_jonas> oerjan: that is related to one of the things I hate in English: in some dialects, "can" and "can't" sounds practically the same, especially in informal speech and depending on the next word
22:35:12 <b_jonas> There's no reliable way you can distinguish them from just hearing.
22:35:27 <FireFly> I misremembered with the -1, but fold -1 is useful to sort the characters in a line
22:35:29 <oerjan> i can' see what you mean
22:35:56 <FireFly> I've used :.!fold -1|sort|uniq -c in vim to get a table of letter frequency for a line
22:36:19 <b_jonas> oerjan: and that's not even the worst case, because with "can't" that would have an "nts" consonant cluster, which most speakers can pronounce fine.
22:36:46 <b_jonas> oerjan: but if you try "can't do" or "can't tell" then the chances are slimmer
22:36:48 <shachaf> oerjan: noping shouldn't have too much overhead, because sometimes it's used on long lines.
22:37:00 <b_jonas> Of cousre, this is just one of the many ambiguities in spoken English.
22:37:11 <FireFly> `cat bin/noping
22:37:12 <HackEgo> print_args_or_input "$@" | sed 's/\(..\)/\1​/g'
22:37:18 <oerjan> shachaf: well the overhead is a smaller problem than the fact that we have no character that works for everyone
22:37:26 <FireFly> I was wondering what you were discussing nop:ing for a while, and why nops would have overhead
22:37:37 <b_jonas> Some others include "make her heart sore" against "make her heart soar", and, in some dialects, "formally" against "formerly"
22:37:52 <b_jonas> ``` cat -v bin/noping
22:37:53 <HackEgo> print_args_or_input "$@" | sed 's/\(..\)/\1M-bM-^@M-^K/g'
22:38:17 <b_jonas> why doesn't it just put a \x0f instead of some non-ascii stuff? is that not enough to noping?
22:38:57 <oerjan> shachaf: heck, if we could find a method that works for each person and which doesn't break anyone's client, we could even have an exception table.
22:39:08 <FireFly> Some clients ignore formatting for highlight purposes
22:39:16 <b_jonas> I see
22:39:43 <oerjan> `hexdump bin/noping
22:39:44 <HackEgo> 0000000 7270 6e69 5f74 7261 7367 6f5f 5f72 6e69 \ 0000010 7570 2074 2422 2240 7c20 7320 6465 2720 \ 0000020 2f73 285c 2e2e 295c 5c2f e231 8b80 672f \ 0000030 0a27 \ 0000032
22:39:53 <FireFly> `` tail -c 8 bin/noping | unidecode
22:39:54 <HackEgo> No output.
22:39:58 <FireFly> `` tail -c 8 bin/noping | xargs unidecode
22:39:59 <HackEgo> xargs: unmatched single quote; by default quotes are special to xargs unless you use the -0 option
22:40:01 <oerjan> ok what's the option to make that useful again
22:40:03 <FireFly> gr
22:40:06 <FireFly> hexdump -C
22:40:33 <oerjan> that quotes exception could be a problem in other cases
22:40:41 <FireFly> oh
22:40:50 <oerjan> not allowed in nicks though
22:41:06 <FireFly> `` unidecode "$(tail -c 8 bin/noping)" # I guess this works
22:41:08 <HackEgo> ​[U+0031 DIGIT ONE] [U+200B ZERO WIDTH SPACE] [U+002F SOLIDUS] [U+0067 LATIN SMALL LETTER G] [U+0027 APOSTROPHE]
22:41:19 <oerjan> ok it uses zero width space
22:41:28 <FireFly> the quotes thing was just xargs complaining
22:41:35 <FireFly> er oh
22:41:40 <FireFly> It was pretty explicit about that
22:41:42 <oerjan> that works for many but breaks one of shachaf's clients
22:42:34 <FireFly> Isn't the noping pattern a bit replacement-happy?
22:42:56 <FireFly> A drawback with inserting so many ZWSPs is that it means less command output gets through
22:43:06 <FireFly> since the bytes count toward the line limit
22:43:20 <shachaf> hierjan
22:43:22 <shachaf> HireFly
22:43:35 <shachaf> everyone is being hired
22:43:47 <FireFly> hire Jan
22:46:07 <b_jonas> As for the overhead of noping, you could at least change it so that it adds a character only once per nick,
22:46:45 <shachaf> ais523 is the noping expert
22:46:46 <oerjan> b_jonas: the problem is where to place it
22:47:00 <shachaf> Or really any 90 programmer.
22:47:01 <b_jonas> And for even less overhead, we could go back to that older method that adds diacritics to a character in a nick, since that typically adds only one byte, eg. øerjan, b_jónas, etc
22:47:14 <shachaf> `? noping
22:47:15 <HackEgo> noping? ¯\(°​_o)/¯
22:47:17 <oerjan> you cannot place it just before the end because of, say, oerjan_
22:47:38 <FireFly> I was thinking just after the first character
22:47:40 <oerjan> or the beginning because both i and shachaf match on a tail part
22:47:40 <b_jonas> oerjan: sure, so place in between two letters that are closest to the middle, or something
22:47:43 <shachaf> `learn noping is programming in 90
22:47:45 <HackEgo> Learned 'noping': noping is programming in 90
22:47:47 <FireFly> Oh right
22:48:16 <b_jonas> hmm
22:48:29 <b_jonas> or is "øerjan" not enough because you match on the end?
22:48:40 <oerjan> b_jonas: for shachaf shac-haf would work but not sha-chaf
22:49:05 <oerjan> b_jonas: it's not enough because i match only on rjan precisely because people sometimes use the ø
22:49:07 <b_jonas> oerjan: huh... why is the latter not enough?
22:49:27 <oerjan> b_jonas: because shachaf matches on chaf
22:49:34 <oerjan> iirc
22:49:34 <b_jonas> hmm
22:50:00 -!- hppavilion[1] has joined.
22:50:10 <oerjan> b_jonas: anyway. that particular problem can be solved with an exception list.
22:50:31 <b_jonas> something like that, yes, a list of heuristic telling what to modify how
22:50:50 <b_jonas> although you'll have to be careful to not make it lie (masquarading a nick to something else, to avoid being identified as a culprit)
22:50:52 <FireFly> Hm
22:51:03 <oerjan> hm does ais523 match on ais?
22:51:20 <FireFly> I don't suppose HackEgo would have any way to know what nicks are online?
22:51:40 <b_jonas> So what would we have to do with your nick? would oeŕjan work? or would we need Esperanto stuff like oerĵan?
22:52:01 <FireFly> Just ZWSP between r and jan I guess
22:52:11 <b_jonas> oerjan: I don't think so, and besides, he's rarely online so you can't easily misping him
22:52:23 <b_jonas> FireFly: that's two bytes more than a diacritic
22:52:28 <FireFly> True
22:52:49 <FireFly> well. is it really longer than ĵ?
22:52:56 <b_jonas> FireFly: yes, that's still only two bytes
22:53:02 <b_jonas> in utf8 that is
22:53:06 <FireFly> `` hexdump -C <<<"ĵ"
22:53:08 <HackEgo> 00000000 c4 b5 0a |...| \ 00000003
22:53:11 <FireFly> I see
22:53:20 <FireFly> `` unidecode "ĵ"
22:53:30 <FireFly> Ah, didn't realise it's that low
22:53:37 <b_jonas> FireFly: anything in \x{80}-\x{7ff} is two bytes
22:53:59 <FireFly> What language allows that kind of \x escape?
22:54:03 <oerjan> FireFly: online nicks won't work for me, since my main noping interest is being able to usefully search for my nick in the logs.
22:54:03 <shachaf> oerjan: chaf\b
22:54:04 <b_jonas> FireFly: perl
22:54:07 <FireFly> Ah
22:54:18 <FireFly> oerjan: oh. bummer.
22:56:01 * oerjan thought ais523 was online pretty frequently. just not always.
22:56:42 <FireFly> Re. \x, in my mind \u escapes are for codepoints and \x escapes for raw bytes
22:57:20 <b_jonas> oh, that reminds me
22:57:30 <b_jonas> would oerjаn ping you?
22:57:44 <b_jonas> or how about oerјan?
22:57:54 <oerjan> b_jonas: in fact it doesn't ping me in irssi even if you don't do anything.
22:57:57 <b_jonas> those are still just one byte extra
22:58:09 <b_jonas> oerjan: sure, but when you search the logs or something
22:58:11 <oerjan> somehow irssi only catches it at the beginning of the line
22:58:35 <b_jonas> um, those kinds of things depend on client-side settings of what you're listening to
22:58:43 <b_jonas> (the whole ping stuff does, obviously)
22:58:46 <oerjan> b_jonas: oh. neither lights up in search.
22:58:49 -!- hppavilion[1] has quit (Ping timeout: 252 seconds).
22:59:57 -!- boily has joined.
23:00:33 <b_jonas> ok, so what if noping printed a pair of a random seed and a HMAC-SHA256 sum computed from the seed and the nick? Then it would ping only people who check their nicks to every seeded hash on the channel?
23:01:25 <b_jonas> Mind you, that also means whoever reads the noping reply can only check for the occurance of specific nicks they guess (case-sensitive, unless the nick is normalized before the checksum), not decode the checksums.
23:01:31 <b_jonas> So it might be impractical.
23:01:38 <boily> @metar CYUL
23:01:40 <lambdabot> CYUL 242200Z 05024KT 4SM -FZRA BKN008 OVC015 M01/M02 A2975 RMK SF6SF2 PRESFR SLP077
23:01:51 <FireFly> I think this might defeat the point of noping
23:01:52 <b_jonas> Plus, it's also too long compared to the other solutions.
23:02:24 <oerjan> b_jonas: noping is supposed to be readable hth
23:02:46 <b_jonas> Ok, let's go back to the character replacement idea then
23:02:57 <oerjan> b_jonas: i would of course prefer a method that's invisible.
23:02:58 <shachaf> `? hash
23:02:59 <HackEgo> hash? ¯\(°​_o)/¯
23:03:15 <shachaf> `` hg log wisdom | grep hash | grep ais523
23:03:18 <HackEgo> summary: <ais523> le/rn hash 2346ad27d7568ba9896f1b7da6b5991251debdf2
23:03:38 <shachaf> I suspect that's a SHA-1 hash of "hash"
23:03:44 <oerjan> shachaf: is there any zero width character that is not irc formatting code that doesn't mess up your client?
23:03:54 <FireFly> Seems so
23:04:02 <shachaf> oerjan: I think zero-width space might be OK.
23:04:04 <shachaf> Or it might not.
23:04:05 <shachaf> I don't know.
23:04:14 <shachaf> You should just make a special case for me.
23:04:32 <boily> @metar CYUL
23:04:33 <lambdabot> CYUL 242200Z 05024KT 4SM -FZRA BKN008 OVC015 M01/M02 A2975 RMK SF6SF2 PRESFR SLP077
23:04:39 <FireFly> Wasn't the issue that the ZWSP rendered weirdly?
23:04:40 <oerjan> shachaf: um a special case for you won't work
23:04:44 <boily> aurgh. I want the current metar.
23:04:53 <oerjan> because your client breaks when _other_ people are nopinged.
23:05:08 -!- lambda-11235 has joined.
23:05:14 <shachaf> oerjan: true
23:06:03 <b_jonas> shachaf: does a \x0e still mess up your terminal? and does \x9b mess up your terminal if it appears in an utf-8 char
23:06:26 <shachaf> Look, I don't know.
23:06:41 -!- `^_^v has quit (Quit: This computer has gone to sleep).
23:06:46 <b_jonas> because I sort of think that if they do, it's sort of such a heavy client issue that we don't really have to work around
23:07:07 <FireFly> I was thinking ZWJ might be more semantically appropriate than ZWSP
23:07:30 <oerjan> `unicode ZERO WORD JOIN
23:07:33 <HackEgo> No output.
23:07:34 <b_jonas> shachaf: also, same question about \x05
23:07:40 <FireFly> `unicode zero width joiner
23:07:41 <HackEgo> ​‍
23:07:43 <boily> @metar CYUL
23:07:43 <lambdabot> CYUL 242300Z 05019G26KT 4SM -FZRA BKN007 OVC015 M01/M01 A2970 RMK SF6SF2 PRESFR SLP060
23:07:51 <boily> aaah! much better.
23:07:57 <FireFly> @metar ESSB
23:07:58 <lambdabot> ESSB 242250Z AUTO 23005KT 9999 NCD M02/M05 Q0999
23:07:58 <boily> wait. it's getting worse.
23:08:07 <shachaf> @metar KOAK
23:08:07 <lambdabot> KOAK 242253Z 28010KT 10SM FEW200 21/09 A3010 RMK AO2 SLP193 T02060089
23:08:28 <oerjan> `` echo -n boi; unicode zero width joiner; echo ly
23:08:29 <HackEgo> boiU+200C ZERO WIDTH NON-JOINER \ UTF-8: e2 80 8c UTF-16BE: 200c Decimal: &#8204; \ ‌ \ Category: Cf (Other, Format) \ Bidi: BN (Boundary Neutral) \ \ U+200D ZERO WIDTH JOINER \ UTF-8: e2 80 8d UTF-16BE: 200d Decimal: &#8205; \ ‍ \ Category: Cf (Other, Format) \ Bidi: BN (Boundary Neutral) \ \ ly
23:08:31 * boily mapoles a few clouds at the shachafweather
23:08:37 <oerjan> ff
23:08:38 <shachaf> @@ (@metar CYUL) (@metar KOAK) (@mtar ENVA)
23:08:39 <lambdabot> Plugin `compose' failed with: Unknown command: "mtar"
23:08:41 <b_jonas> oerjan: if shachaf really matches on "chaf", then we probably need an exception for him anyway, to make sure we modify one of those chars
23:08:43 <boily> oerjan: BWAH AH AH :D
23:08:44 <shachaf> @@ (@metar CYUL) (@metar KOAK) (@metar ENVA)
23:08:45 <lambdabot> CYUL 242300Z 05019G26KT 4SM -FZRA BKN007 OVC015 M01/M01 A2970 RMK SF6SF2 PRESFR SLP060 KOAK 242253Z 28010KT 10SM FEW200 21/09 A3010 RMK AO2 SLP193 T02060089 ENVA 242250Z 27015KT 9999 SCT006 BKN015 02/01 Q0999 RMK WIND 670FT 28016KT
23:08:49 <oerjan> `` echo -n boi; unicode 'zero width joiner'; echo ly
23:08:50 <HackEgo> boi‍ \ ly
23:09:03 <shachaf> metar soup is my favorite
23:09:06 <boily> sorry, it was just perfect.
23:09:15 <oerjan> b_jonas: i think we should _entirely_ separate the question of finding a character that works, from where to place it.
23:09:25 <oerjan> darn
23:09:33 <b_jonas> oerjan: sure
23:09:42 <FireFly> `` echo -n boi; unicode 'zero width joiner' | tr -d \\n; echo ly # third time's the charm
23:09:43 <HackEgo> boi‍ly
23:09:48 <b_jonas> oerjan: and finding a character that works is usually easy, unless the name is like very short or contains only strange chars
23:09:58 <oerjan> boily: did that ping you
23:10:09 <oerjan> shachaf: did that mess up your client
23:10:32 <shachaf> oerjan: It's hard to tell.
23:10:35 <oerjan> (what FireFly did)
23:10:43 <shachaf> It doesn't mess it up immediately and not deterministically.
23:10:48 <oerjan> shachaf: fff
23:10:56 <boily> oerjan: nope.
23:11:05 <shachaf> I think it's fine.
23:11:10 <shachaf> But I might be wrong.
23:11:20 <shachaf> `le/rn weather/?? (?metar CYUL) \ (?metar ENVA) \ (?metar ESSB) \ (?metar KOAK)
23:11:25 <HackEgo> Learned «weather»
23:11:26 <shachaf> `? weather
23:11:28 <HackEgo> ​?? (?metar CYUL) \ (?metar ENVA) \ (?metar ESSB) \ (?metar KOAK)
23:11:31 <oerjan> ok, maybe we should try that character, then.
23:11:42 <shachaf> `le/rn weather/lambdabot: ?? (?metar CYUL) \ (?metar ENVA) \ (?metar ESSB) \ (?metar KOAK)
23:11:45 <HackEgo> Learned «weather»
23:11:50 <shachaf> Oops, now my terminal is messed up.
23:11:55 <shachaf> But I don't know what caused it.
23:11:59 <shachaf> `? weather
23:12:22 <HackEgo> lambdabot: ?? (?metar CYUL) \ (?metar ENVA) \ (?metar ESSB) \ (?metar KOAK)
23:12:23 <lambdabot> CYUL 242300Z 05019G26KT 4SM -FZRA BKN007 OVC015 M01/M01 A2970 RMK SF6SF2 PRESFR SLP060 \ ENVA 242250Z 27015KT 9999 SCT006 BKN015 02/01 Q0999 RMK WIND 670FT 28016KT \ ESSB 242250Z AUTO 23005KT 9999 NCD M02/M05 Q0999 \ KOAK 242253Z 28010KT 10SM FEW200 21/09 A3010 RMK AO2 SLP193 T02060089
23:12:44 <boily> wait. you can chain Hackie and Lambdie together?
23:16:03 <b_jonas> oerjan: we can use, like, replace one of [aceinorstuy] with [асеіņоŗșțúý] and their uppercased versions, and most nicks contain one of those
23:16:11 <boily> time to go outside again and ingest lots of szechuan peppers.
23:16:25 -!- boily has quit (Quit: CONVERTER CHICKEN).
23:16:59 <oerjan> <shachaf> But I don't know what caused it. <-- i suspect it's the ZWSP HackEgo put before ?? in `? weather
23:17:10 <shachaf> Oh, maybe.
23:17:31 <oerjan> b_jonas: um, i'm thinking we can use the ZWJ that we just tested
23:17:57 <b_jonas> oerjan: maybe, but that's two bytes more per nick, and we often want to noping an entire long list of nicks
23:18:28 <oerjan> *sigh*
23:19:04 <b_jonas> although I'm not really sure how you'd noping "^v". maybe like "↑v" (which is two extra bytes, not only one).
23:19:42 <oerjan> b_jonas: ok, what about only using those chars you said that look entirely identical, and use ZWJ if there aren't enough appropriate ones?
23:19:57 <b_jonas> oerjan: I didn't say any look entirely identical
23:20:12 <oerjan> the aceio looked identical to me
23:20:15 <b_jonas> but sure, if you don't find a suitable replacement, then put in a zwsp
23:20:26 <b_jonas> oerjan: that rather depends on the font.
23:20:29 <oerjan> b_jonas: ZWJ
23:20:41 <b_jonas> oerjan: that then
23:21:37 <b_jonas> For me, only "c" looks entirely identical here, although some others look very similar. Always because they're not in my font so they're taken from a replacement font.
23:22:25 <b_jonas> There's more possible replacements of course, that set was just an idea.
23:22:32 <b_jonas> s/set/map/
23:24:50 <oerjan> so, if a nick is 5 chars or shorter, it gets only one replacement, i think, preferably not at the very end (but can't do much about length <=3 there)
23:25:22 <oerjan> if it's 6 chars or longer, it gets two.
23:25:26 <b_jonas> oerjan: preferably also not at the very beginning
23:25:35 <oerjan> er *ends
23:25:58 <oerjan> that somehow got lost in the thinking
23:26:11 <b_jonas> oerjan: and preferably not two from the end if the last but one char matches [-\\|_]
23:28:54 <oerjan> i think maybe those chars should just be stripped finally before starting to look for where to replace
23:29:29 <oerjan> any number, as long as there are at least 2 chars left
23:29:43 <b_jonas> oerjan: maybe, but make sure you get something sensible (possibly the original nick) even for very short nicks or nicks made of all underscores or stuff like that where you can't really replace anything
23:30:26 <oerjan> well i don't mean stripping as in removing from the output
23:30:31 <b_jonas> sure
23:30:43 <b_jonas> just, like, don't raise an error or something
23:31:51 <oerjan> actually, since the aceio are all alphabetical, we can assume they're part of the essence of the nick if they appear
23:32:13 <b_jonas> oerjan: and test some (actual) all consonant nicks like mt..ve, st..th, n..ht, s..ki, ^..v, t..tr, ly..nn,
23:32:44 <b_jonas> oerjan: just aceio is definitely not enough though, there's lots of nicks with none of those
23:34:57 <oerjan> mt..ve might not count, i think we can use the e
23:35:06 <b_jonas> oh
23:35:08 <b_jonas> true
23:36:42 <b_jonas> oerjan: how would you quote in..t-..e ?
23:37:08 <b_jonas> I've no idea what pings him and what doesn't
23:37:26 <oerjan> hm good point, he _might_ ping on just in..t-
23:38:01 <b_jonas> oerjan: that wouldn't be a problem, since you can replace the n or the t or the i
23:38:08 <oerjan> maybe 5 chars is too little for just one replacement if it's at the end
23:38:16 <b_jonas> oerjan: but I wonder if he pings on t..-..e alone or something
23:39:04 <oerjan> perhaps the basic rule should be, there needs to be a replacement in the first 4 chars and one in the last 4, which may overlap
23:40:41 <b_jonas> um, dunno. that could make something replaced at the very beginning and very end like oerjan| => öerjan¦
23:40:50 <oerjan> except hm
23:41:01 <oerjan> oh hm
23:41:22 -!- puckipedia has quit (Ping timeout: 255 seconds).
23:42:35 <b_jonas> you could still get in trouble with nicks that have no or almost no letters of course, but in that case you can fall back to the invisible character
23:42:46 <b_jonas> but there aren't many such nicks
23:43:29 -!- hppavilion[1] has joined.
23:43:31 <hppavilion[1]> Here's an idea I'm thinking about: A strongly-typed programming language that looks normal
23:43:40 <b_jonas> there are people using strange nicks like [-__-] and stuff
23:43:53 <oerjan> hi hppavilion[1] what part of your nick pings you
23:43:56 <hppavilion[1]> Except it has all these wacky features that make no sense, but that you can't identify from just reading the syntax
23:44:10 <hppavilion[1]> oerjan: hp, hppavilion[1], and hppavellon[1]
23:44:24 <oerjan> ARGH
23:44:28 <hppavilion[1]> oerjan: Why?
23:44:31 <oerjan> b_jonas: this is doomed :P
23:44:33 <hppavilion[1]> I can disable "hp"
23:44:43 -!- puckipedia has joined.
23:44:46 <b_jonas> hppavilion[1]: "hp" only as a separate word, or anywhere?
23:44:47 <hppavilion[1]> It was added recently because of someone who thought typing my full nick was too much work
23:44:52 <hppavilion[1]> b_jonas: Not sure
23:44:57 <hppavilion[1]> But seriously, I can just remove it
23:44:59 <hppavilion[1]> Why?
23:45:01 <b_jonas> hpc: does this ping you?
23:45:04 <hppavilion[1]> Nope
23:45:09 <b_jonas> oerjan: see!
23:45:13 <oerjan> hppavilion[1]: we're trying to invent a ping prevention scheme that doesn't escape too many chars
23:45:26 <b_jonas> oerjan: only as a separate word,
23:45:32 <b_jonas> so almost any replacement works
23:45:47 <hppavilion[1]> oerjan: Have you tried putting it in []?
23:45:48 <oerjan> ah
23:46:09 -!- lynn_ has joined.
23:46:09 <hppavilion[1]> '[oerjan] said "Hi"! at 12+2i o\' clock'
23:46:16 <hppavilion[1]> [oerjan]
23:46:17 <oerjan> hppavilion[1]: not going to work for me
23:46:21 <hppavilion[1]> oerjan: Oh :/
23:46:32 <oerjan> i search for "rjan"
23:48:01 <b_jonas> ah right, just "rjan" so that örjan or ørjan or œrjan pings you
23:48:09 <oerjan> `` (echo h; echo p; unicode 'zero width joiner'; echo a) | tr -d '\n'
23:48:14 <HackEgo> hp‍a
23:48:23 <shachaf> zero width joiner
23:48:29 <shachaf> hpa
23:48:36 <b_jonas> oerjan: huh? you'd just replace the i or the a in his name
23:48:41 <oerjan> hppavilion[1]: did that HackEgo response ping you?
23:48:45 <b_jonas> oerjan: or replace both the o and the a
23:48:49 <hppavilion[1]> hppavilion[1]: It appears it did
23:48:57 <hppavilion[1]> Whoops, oerjan
23:48:59 -!- Treio has joined.
23:48:59 -!- lynn has quit (Ping timeout: 240 seconds).
23:49:01 * hppavilion[1] is an idiot
23:49:06 <shachaf> Hmm.
23:49:11 <shachaf> Did I ping you?
23:49:15 <shachaf> I didn't realize what was going on.
23:49:32 <hppavilion[1]> shachaf: No, strangely
23:49:53 <oerjan> b_jonas: i was just testing if the ZWJ actually could mess it up if placed after the p
23:50:07 <hppavilion[1]> oerjan: What is the purpose of this ping prevention scheme?
23:50:17 <b_jonas> oerjan: yeah, makes sense
23:50:53 <hppavilion[1]> So a feature of my normal-looking crazy language (which I may integrate with another project so as to cut down on my projects) is complex fuzzy bag typing.
23:50:59 <hppavilion[1]> Because nothing could be stranger than that.
23:51:10 <b_jonas> oerjan: I'll have to figure out something to decide about matches of /\bjonas\b/ which one refers to me and which doesn't. Sadly, jonas is too common a word.
23:51:13 <oerjan> hppavilion[1]: for HackEgo commands like `culprits
23:51:41 <hppavilion[1]> oerjan: Ah
23:51:47 <b_jonas> One solution that might actually make sense is to change my screen name, since then I can choose a nick that rarely accidentally matches,
23:52:21 <b_jonas> althoguh that would of course have the dual problems that people would still use b_jonas as my name, and that people wouldn't recognize me when I speak or when others speak of me using my new nick.
23:52:45 <hppavilion[1]> b_jonas: You could just add some characters
23:52:47 <hppavilion[1]> b__jonas?
23:52:57 <b_jonas> hppavilion[1]: um no, "b_jonas" itself is unique enough
23:53:05 <b_jonas> hppavilion[1]: it's just "jonas" alone that's the problem
23:53:10 <hppavilion[1]> b_jonas: Ah
23:53:13 <hppavilion[1]> Makes sense
23:53:31 <oerjan> jonas i hvalfiskens buk
23:53:42 <hppavilion[1]> b_jonas: Configure your IRC client to only acknowledge b_jonas when the characters on either side are not acceptable nick characters?
23:53:43 <b_jonas> oerjan: huh?
23:53:49 -!- Sprocklem has quit (Ping timeout: 252 seconds).
23:54:01 <b_jonas> hppavilion[1]: no no, "b_jonas" anywhere, even with surrounding characters, almost certainly refers to me
23:54:22 <oerjan> b_jonas: just some silly archaic biblical dano-norwegian
23:54:24 <hppavilion[1]> b_jonas: Yes, but that would work
23:54:28 <b_jonas> hppavilion[1]: like I said, it's "jonas" or "Jonas" alone that are problems, without the "b_" or other similar prefixes
23:54:48 <hppavilion[1]> Oh
23:54:50 <hppavilion[1]> Wait, what?
23:54:58 <hppavilion[1]> How does that ping you then?
23:55:19 <b_jonas> oerjan: yes, the bible _is_ the reason why Jonas became a popular name, which is indirectly why it's a common word on irc, and also indirectly why I use this nick
23:55:41 <b_jonas> hppavilion[1]: it might or might not, depending on my settings, but if it doesn't ping me, that's the opposite problem, then I might lose lines that actually refer to me
23:55:47 <oerjan> to b_ or not to b_, that is the question
23:56:01 <hppavilion[1]> b_jonas: And do people ever just refer to you as "jonas"?
23:56:05 <b_jonas> oerjan: yes, I mangle the "b_" in various ways, so "Be" actually occurs
23:56:17 <b_jonas> hppavilion[1]: sure, I even have "jonas" as the nick on some websites
23:56:22 <hppavilion[1]> Oh
23:56:25 <b_jonas> hppavilion[1]: it's rare on irc, where everyone sees my nick
23:56:28 <b_jonas> but it can happen
23:56:36 <b_jonas> it's a reasonable abbreviation
23:57:49 <b_jonas> I'll probably just use some dirty heuristics, like ignoring just "jonas" on certain high-traffic channels where it occurs the most frequently (but still looking for the more specific variants like "b_jonas" of course).
23:58:11 <b_jonas> hppavilion[1]: I used "jonas" before I came up with "b_jonas" to make it unique
←2016-02-23 2016-02-24 2016-02-25→ ↑2016 ↑all