00:23:13 -!- FreeFull has quit.
00:26:56 -!- sleepnap has joined.
00:28:52 -!- tromp has joined.
00:28:58 -!- sleepnap1 has joined.
00:31:14 -!- sleepnap has quit (Ping timeout: 244 seconds).
00:33:15 -!- tromp has quit (Ping timeout: 252 seconds).
00:52:25 -!- ais523 has quit (Quit: quit).
01:01:38 -!- sleepnap1 has quit (Quit: Leaving.).
02:37:32 -!- heroux has quit (Ping timeout: 245 seconds).
02:37:44 -!- heroux has joined.
03:50:08 -!- Sgeo__ has joined.
03:52:58 -!- Sgeo_ has quit (Ping timeout: 245 seconds).
05:33:23 -!- tromp has joined.
05:33:39 -!- uplime has quit (Quit: ZNC 1.7.3 - https://znc.in).
05:34:08 -!- uplime has joined.
05:37:57 -!- tromp has quit (Ping timeout: 252 seconds).
06:45:19 -!- tromp has joined.
07:01:01 <rain1> $ a=b b=a; echo $((a))
07:01:03 <rain1> bash: b: expression recursion level exceeded (error token is "b")
07:38:51 -!- xkapastel has joined.
07:58:56 -!- AnotherTest has joined.
08:12:32 -!- Phantom_Hoover has joined.
08:27:58 -!- Lord_of_Life has quit (Ping timeout: 272 seconds).
08:28:55 -!- Lord_of_Life has joined.
08:37:04 -!- Phantom_Hoover has quit (Quit: Leaving).
09:13:46 -!- onon has left ("†").
09:44:24 <Taneb> I've just realised that the idea I had for writing a text editor is, rougly speaking, Smalltalk
09:52:17 -!- cpressey has joined.
09:56:31 <cpressey> Good morning. I've been reading the R7RS. It's been making me laugh.
09:58:32 <cpressey> I don't mean to say that it is laughable; overall, I like Scheme.
09:58:40 <rain1> what funny abut it
09:59:02 <rain1> think R7RS could be better but course corrected well
09:59:59 <cpressey> Mainly, it's amusing when they leave so much wiggle room.
10:00:14 <cpressey> For example, a Scheme implementation is allowed to use symbols outside Unicode if it wants.
10:01:33 <rain1> they don't even specify stuff about filesystem paths for importing files
10:01:53 <rain1> in case someone wants an SQL database backed complaint r7rs implementation
10:01:59 <rain1> the result is you cannot portably do a multiple file project
10:04:56 <rain1> https://rain-1.github.io/scheme-srfi-1.html
10:06:47 <cpressey> rain1: Is it ironic that *none* of those look like https://srfi.schemers.org/srfi-55/srfi-55.html ?
10:07:24 <rain1> wow i didnt even realize that
10:07:43 <cpressey> (require-extension (srfi 1)) might work in one or more of those
10:07:43 <rain1> but yeah this is the mess we're in
10:07:51 <rain1> and everybody is wondering why nobody uses scheme
10:12:17 <cpressey> I still prefer it over Common Lisp and Clojure (but I'm probably not typical). I'd like it even more if mutability was forbidden. I thought there was a SRFI for this, but I went looking for it again and I couldn't find it.
10:12:47 <rain1> I would remove the call/cc and similar operators
10:12:53 <rain1> I think it's become clear that they aren't useful
10:16:00 <cpressey> Scheme (and Haskell) have a lot of features in them that are mainly to support PL research and education... I'd put call/cc in that bucket.
10:16:31 <cpressey> For learning about continuations, it's cool. Will I ever actually *use* it...? Probably not.
10:48:39 <int-e> continuations are easy
10:48:45 <int-e> delimited continuations are weird
10:49:06 <Taneb> All programming constructions are weird
10:49:08 <int-e> (bla bla shift bla bla reset bla bla)
10:49:51 <int-e> Taneb: that was an opinion, of course
10:50:05 <int-e> Or maybe a statement that I grokked the former but not the latter.
10:50:42 <Taneb> Whereas what I said was a contrarian but defensible statement made partially in jest
10:57:33 <shachaf> All continuations are delimited, though.
10:57:47 -!- xkapastel has quit (Quit: Connection closed for inactivity).
10:57:58 <cpressey> Therefore continuations are easy and weird
10:59:01 <cpressey> I have the start of a CPS concatenative language but I had to use a nonstandard definition of function composition to get it
10:59:50 -!- arseniiv has joined.
11:00:05 <shachaf> I'm mystified by this, actually:
11:00:30 <shachaf> * I feel like I understand undelimited continuations
11:00:41 <shachaf> * I feel like I don't understand delimited continuations
11:00:49 <shachaf> * All continuations are delimited
11:01:24 <shachaf> Actually, see "A theory of regulation." in https://www.bloomberg.com/opinion/articles/2017-01-24/metrics-fees-and-regulations
11:01:55 <cpressey> Thing I didn't expect after your list of bullet points about continuations: a link to Bloomberg.com
11:02:26 <shachaf> I only realized that I was quoting that article after I finished writing the bullet points.
11:03:15 <int-e> shachaf: I'm confused by the shift/reset syntax, and how it translates to the common functional (a -> r) -> r idea.
11:04:08 <int-e> Maybe I just haven't read the right paper(s) yet.
11:04:51 <shachaf> Haskell Cont continuations are delimited by runCont.
11:05:36 <int-e> As I said, I'm mainly confused by shift & reset.
11:06:08 <cpressey> I suspect "delimited" refers to something that's not actually the continuation per se -- but I don't really know.
11:06:37 <int-e> Well, whole program continuations are silly.
11:07:28 <shachaf> Oh, my pseudo-continuation thing has a delimiter, normally written {}.
11:07:34 <int-e> To carve out a context from a program you need a point where the context starts, and a hole, "delimiting" it from two sides.
11:08:26 <shachaf> When you write { ...foo`...; ... }, foo gets "{\x; ...x...; ... }" as an argument.
11:08:48 <shachaf> Rather than the entire rest of the program.
11:11:27 <shachaf> In the classic Scheme shift-reset thing, shift is a binder, right?
11:11:31 <arseniiv> int-e: shift/reset confuses me too. This or previous year I have seen something more natural but I don’t remember if it was purely about delimited continuations or something other
11:12:58 <arseniiv> hm how algebraic effects relate to continuations? At least syntactic ideas about the former are more understandable for me
11:14:20 <arseniiv> that handling case-like construct and data-like definition of an effect
11:14:25 <shachaf> Oh, I think I understand shift/reset now.
11:15:05 -!- atslash has joined.
11:15:19 <arseniiv> IMO shift takes on itself too much, and that effect syntax takes from it some control to the “reset” side
11:16:08 <arseniiv> and then suddenly it starts to resemble control constructs from imperative languages, e. g. try/catch
11:17:53 <arseniiv> oh also I had read something that made me think I understood shift/reset, but now I remember it only vaguely
11:21:20 <shachaf> int-e: OK, I now understand shift-reset and can work the examples.
11:22:38 <shachaf> I'm not sure why shift is called shift, and why it doesn't take a lambda.
11:32:09 <shachaf> The shift/reset in http://pllab.is.ocha.ac.jp/~asai/cw2011tutorial/main-e.pdf seem a bit more reasonable.
11:55:07 -!- adu has quit (Quit: adu).
12:03:47 <int-e> okay... next question... why?
12:04:03 <fungot> int-e: i hope something good came in the mail
12:04:33 <int-e> That's a better answer than I hoped for. But it's still not very satisfying.
12:05:38 <cpressey> So "delimited" means that instead of one thing called call/cc you have two things called shift and reset
12:06:21 <int-e> shachaf: there's a subtlety around the behavior of ; inside reset though...
12:06:47 <cpressey> Here's a stack. No, there's no stack now. Okay, now there's a stack again, but it's a different stack.
12:06:49 <int-e> shachaf: reset (foo; shift ...) doesn't capture the 'foo' part.
12:07:35 <int-e> shachaf: otherwise the tree walking wouldn't make sense (I think)
12:09:19 <int-e> cpressey: Yeah I guess that explains it operationally, more or less... shift = "capture the stack between here and the latest reset on the heap, and return a closure that, when invoked, puts it back on the stack".
12:13:45 <cpressey> int-e: if it explains anything operationally, it was by accident
12:14:15 <cpressey> it was more about... well, hard to say. I am prattling.
12:15:48 <int-e> Oh was I finding patterns in the noise... mistaking them for communication? I believe that's a common mistake for humans :)
12:15:56 <int-e> (So maybe I'm human? Who knew...)
12:19:43 <cpressey> I'll chalk it up to coincidence. I was perhaps trying to answer "why?"
12:20:23 <int-e> This is all so dysfuncational!
12:21:28 <cpressey> Do I really want continuations that have been made more useful by making them delimited continuations? Isn't the point kind of to make it *less* useful? To make it easier to analyze, etc.
12:21:47 <cpressey> If I wanted useful, I'd just not deal with continuations at all.
12:22:26 <int-e> I rather suspect that continuations were meant to be useful.
12:22:27 <cpressey> I guess there is some kind of control structure that delimited continuations can capture, that "regular" ones can't, but I haven't seen what it is
12:23:35 <cpressey> doesn't interest me enough to justify me hunting it down unfortunately
12:24:03 <int-e> I wonder about the history.
12:24:16 <int-e> This may have been an accident.
12:27:03 <cpressey> I dunno, I kind of stopped paying listening to academics after I heard Wadler compare monads to a solution to Descartes' mind-body problem.
12:27:06 <int-e> (Made-up history: 1. We want exception-like behavior, a bit like setjmp/longjmp, but memory-safe! Let's make something that captures the current state of the stack so we can resume at this point later. Let's name it call/cc. 2. call/cc is slow because it has to capture all of the current stack... let's add a mechanism to limit the amount of stack we safe! (reset / shift=call/cc up to last...
12:27:12 <int-e> ...reset). 3. Hmm, what can we use this new primitive for? 4. 100 papers. )
12:27:59 -!- PaniniTheDevelop has joined.
12:28:01 <cpressey> int-e: I believe continuations, the concept, started in denotational semantics.
12:28:20 <cpressey> So if it's "We want to write a function that describes exception-like behaviour" then yes
12:28:36 <int-e> cpressey: let's focus on steps 2-4 :)
12:30:25 <int-e> ("1. God gave us call/cc." - Let's pretend I wrote that instead ;) )
12:30:28 <cpressey> int-e: https://cs.indiana.edu/~dyb/pubs/monadicDC.pdf refers to a 1987 paper called "Beyond continuations" that
12:31:01 <int-e> `relcome PaniniTheDevelop
12:31:02 <HackEso> PaniniTheDevelop: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: <https://esolangs.org/>. (For the other kind of esoterica, try #esoteric on EFnet or DALnet.)
12:31:18 <int-e> PaniniTheDevelop: ask on #freenode
12:32:14 <int-e> (oh. register where?)
12:33:13 <int-e> sorry, I somehow assumed the IRC server
12:34:02 <int-e> `bf 64+"!dlroW ,olleH">:#,_@
12:37:58 <int-e> `ibin/befunge 64+"!dlroW ,olleH">:#,_@
12:38:22 <int-e> Now what was the official way to do that...
12:38:56 <int-e> the `ibin/befunge was important
12:40:25 <int-e> `! befunge 9857727254>\#+:#*9-#\_$.@
12:41:22 <HackEso> `! emulates the ! command of our former bot EgoBot. You write `! then the name of the language then a program, and it runs the program you give and returns the result. We used to use it to test out esoprograms in-channel all the time, but the set of included esolangs is fairly old now and so it's rarely used.
12:41:53 <esowiki> [[Special:Log/newusers]] create * PaniniTheDeveloper * New user account
12:42:23 <int-e> One more hoop to jump through.
12:45:50 <int-e> It will ask you to introduce yourself at some point... I don't know whether it tells you immediately after creating the account or when you attempt to edit a page though. (Maybe both, but perhaps only the latter.)
12:47:15 <int-e> Anyway, we're all sorry for those hoops but we did suffer from a lot of spam in the past (including some that figured out how to solve the befunge captcha, either automatically or perhaps by employing humans that are rewarded simply for creating an account successfully.)
12:51:36 <cpressey> If the latter, it is probably the only instance ever of people being paid to code in Befunge.
12:52:06 <cpressey> Anyway I didn't realize there was a captcha at all
12:54:37 <int-e> cpressey: I imagine the reward to be more along the lines of being allowed to download a couple of pornographic videos.
12:55:26 <int-e> or maybe a "stress-test" of the network connection of "a friend".
13:01:44 <int-e> I should stress that I don't know. I'm extrapolating from https://krebsonsecurity.com/ mostly.
13:21:38 -!- PaniniTheDevelop has quit (Remote host closed the connection).
14:09:28 <esowiki> [[Emoji]] M https://esolangs.org/w/index.php?diff=65578&oldid=65554 * Dtuser1337 * (-35) removing unnecessary newlines.
14:09:54 <esowiki> [[Emoji]] https://esolangs.org/w/index.php?diff=65579&oldid=65578 * Dtuser1337 * (+35) Undo revision 65578 by [[Special:Contributions/Dtuser1337|Dtuser1337]] ([[User talk:Dtuser1337|talk]]) Oops
14:11:46 <esowiki> [[Emoji]] M https://esolangs.org/w/index.php?diff=65580&oldid=65579 * Dtuser1337 * (+1) trying out new thing.
14:17:22 <rain1> I think delimited continuations are easier
14:17:28 <rain1> for one thing you can algebraically axiomatize them
14:17:52 <rain1> (2004) Axioms for Delimited Continuations in the CPS Hierarchy - Yukiyoshi Kameyama
14:18:49 <rain1> if you wanted to define orthogonal language constructs in terms of continuations you need multiple-prompt continuations to separate them though
14:39:47 <arseniiv> <int-e> ("1. God gave us call/cc." - Let's pretend I wrote that instead ;) ) => no, God gave us the integers, he couldn’t have given us two different things at once, it would be cheating
14:40:30 <arseniiv> if you’re right, call/cc = integers
14:42:15 <arseniiv> but what about call/pred then? I know Kronecker probably meant only nonnegative/positive integers, but it’s more fun if we’d take them all
14:42:32 <arseniiv> oh one time I was bored and tried to make Peano-like axioms for Z
14:49:35 <int-e> arseniiv: I thought he gave use more tablets full of commandments but Moses was too lazy to carry them down the mountain?
14:50:17 <int-e> should've used paper
14:50:40 <Taneb> arseniiv: hmm, 0 is in Z, succ is a bijection from Z -> Z such that succ(x) != x
14:51:48 <Taneb> Induction's the tricky one, as always
14:51:55 * int-e tries to find context
14:52:08 <int-e> ah. "I was bored and tried to make Peano-like axioms"
14:52:47 <arseniiv> I added prev and tried to make sure pred succ = succ pred = id
14:52:59 <Taneb> If K is a set such that 0 is in K and for every integer n, n being in K implies that succ(n) and succ^-1(n) is in K, then K contains every integer
14:53:28 <Taneb> arseniiv: I was trying to be sneaky and rely on pred existing due to succ being bijective
14:53:28 <arseniiv> Taneb: yeah, I wrote it in that way, though using pred instead of succ^−1
14:53:32 <int-e> Z is the monoid given by the presentation <s,p | sp = ps = 1>
14:54:28 <int-e> arseniiv: we can translate that back into peano style, surely.
14:54:54 <int-e> It just won't be nearly as nice as Peano's axioms... unfortunately.
14:55:19 <arseniiv> though all said, I like the definition of N as a free monoid on one generator :)
14:55:42 <arseniiv> then we can add multiplication more or less naturally
14:56:12 <int-e> In reality I like Z as a quotient of N x N (with (a,b) = (c,d) whenever a + d = b + c)
14:56:52 <arseniiv> yeah it’s a nice construction and works for more things, I forgot what it’s named in general
14:57:37 <int-e> Just like Q is the quotient of (Z x (Z - {0})) w.r.t (a,b) = (c,d) <--> a*d = b*c)
14:58:15 <Taneb> a + 0 = a, a + succ(b) = succ(a + b), a + succ^-1(b) = succ^-1(a + b), exercize: show that this is consistent
14:58:51 <int-e> Taneb: what do you mean by succ^-1?
14:58:57 <rain1> is ^-1 just a constructor
14:59:18 <rain1> or maybe succ^-1 is a single constructor
14:59:24 <int-e> Taneb: I'd be happier if you used `pred` and axioms for the interaction of succ and pred
15:01:00 <Taneb> int-e: I define succ to be a bijection, and succ^-1 is the inverse function of succ, which you can call pred if you like
15:02:12 <int-e> so putting that equationally, you have pred(succ(x)) = x and succ(pred(x)) = x.
15:03:07 <rain1> http://minikanren.org/workshop/2019/minikanren19-final4.pdf I like this
15:04:07 <int-e> fortuntately, the rewrite rules +(x, 0) -> x, +(x, s(y)) -> s(+(x,y)), +(x, p(y)) -> p(+(x,y)), s(p(x)) -> x, p(s(x)) -> x are terminating and confluent, and there are distinct normal forms (e.g., 0 and s(0)), so the system is consistent. (Exercise: Figure out what having distinct normal forms has to do with "consistency")
15:05:34 <rain1> what theorem is that
15:05:52 <cpressey> I am probably missing something, but, how is this not group theory
15:05:56 <rain1> I guess its some fundamental result from term rewriting theory
15:07:26 <int-e> (Solution to exercise: Since we're specifying an algebraic structure by equations alone, there's always a model that consists of a single element. So the natural analogue of "consistency" is not "has a model", but "has a non-trivial model", which means a model with more than one element.)
15:07:55 <int-e> This /is/ related to standard consitency formulated in terms of booleans: we don't want to have false = true.
15:16:27 <int-e> cpressey: "how is this not group theory" -- term rewriting is closer to universal algebra (you can have an arbitrary number of functions of arbitrary arity, and you can talk about presentations of such structures (given by equations between terms that may contain variables, like that s(p(x)) = x above) and stuff like that. And then you can ask questions like whether two terms (0 and s(0)) are...
15:16:33 <int-e> ...the same. To that end, one can try to "complete" the system, by which checking whether t = u amounts to reducing t and u to a normal form with respect to a complete (terminating and confluent) system, and then comparing those normal forms syntactically.).
15:17:55 <int-e> https://en.wikipedia.org/wiki/Knuth%E2%80%93Bendix_completion_algorithm is not the best Wikipedia article ever... but it might serve as a starting point nonetheless. Note that the seminal paper is titled "Simple Word Problems in Universal Algebras", so the universal algebra angle was there from the very beginning.
15:19:26 <int-e> Sorry, I've worked in this field for 8 years. Some things stick :P
15:20:34 <cpressey> Is it not the case that "Peano-like axioms for Z" would be roughly the same as "Axioms for (infinite, ordered) groups"
15:21:24 <int-e> abelian would've been my first instinct
15:21:52 <cpressey> But s() induces an order, I'm sure
15:22:16 <int-e> until it runs into a cycle (and cycle avoidance is the main challenge here)
15:22:25 <cpressey> I sure hope it induces an order, or I've wandered into an episode of The Twilight Zone
15:22:51 <int-e> modulo 3 you have 0 < 1 < 2 < 0 < 1 < 2 < 0 < 1 ...
15:23:06 <int-e> That's not much of an order, if you ask me.
15:23:27 <int-e> Anyway, that's what derailed *my* train of thought.
15:23:51 <int-e> And at least it's still a quasi-order.
15:24:53 <int-e> and even a... https://en.wikipedia.org/wiki/Well-quasi-ordering
15:25:19 -!- xkapastel has joined.
15:25:27 <cpressey> I think I see what you're getting at
15:30:33 * cpressey tries to think of how to extend the Peano axioms to ensure that the set is infinite
15:31:32 <Taneb> I think the peano axioms do imply the set is infinite
15:32:09 <int-e> (the axiom schema, not the proof method)
15:32:35 <Taneb> Because succ is injective and there's no natural n such that succ(n) = 0
15:32:36 <rain1> couldn't you just assume you had a finite model then add one to the biggest number
15:34:08 <cpressey> I'm completely lost then. That's okay.
15:34:46 <cpressey> I'm not sure where the modulo 3 thing came from.
15:35:29 <rain1> well if you had a finite model
15:35:36 <rain1> take the biggest element
15:35:44 <rain1> the assumption is that S(biggest) is not in that set
15:36:03 <rain1> if it was in the set, then you have S(biggest) = something so theres a loop, kind of like modular arithmetic
15:36:09 <Taneb> rain1: I don't think that that's where cpressey is lost
15:40:14 <cpressey> I don't really know anything about model theory so I have no intuitions here, but if you have axioms for infinite ordered groups, I would expect that there is no finite model that would satisfy them
15:40:47 <cpressey> On the other hand I can see how you could have a finite model satisying axioms for abelian groups, that doesn't sound wrong to me
15:41:03 <cpressey> And that's where modulo 3 could come in, I can see that
15:41:36 <int-e> cpressey: oh well I'm having a totally different wtf moment about this: https://www.gq.com/story/war-against-sneaker-bots
15:45:44 <Taneb> int-e: it's amazing the things that happen in this world
15:48:55 <int-e> or, to quote Brian Krebs, 'For readers unfamiliar with this term, “shoe botting” or “sneaker bots” refers to the use of automated bot programs and services that aid in the rapid acquisition of limited-release, highly sought-after designer shoes that can then be resold at a profit on secondary markets.'
15:49:24 <int-e> Taneb: And disturbing.
15:57:40 -!- Sgeo_ has joined.
16:00:52 -!- Sgeo__ has quit (Ping timeout: 245 seconds).
16:03:34 <cpressey> What they don't tell you is that the shoes are highly sought-after because, properly applied, they will eradicate 80% of the world's diseases
16:05:15 <int-e> . o O ( Instead of dozens of different causes, everybody will die from shoe poisoning from this point onward. )
16:06:37 -!- sebbu2 has joined.
16:08:04 <int-e> cpressey: I'm only half kidding. I have a genuine problem with applying percentages to causes of death when we're dealing with a 100% mortality rate in the long run.
16:09:12 -!- Vorpal has quit (Ping timeout: 245 seconds).
16:10:25 -!- sebbu has quit (Ping timeout: 268 seconds).
16:11:03 <Taneb> I remember seeing some headline that eating cheese reduces death rate from all causes
16:11:14 <Taneb> The obvious jokes were made
16:14:31 -!- Vorpal has joined.
16:14:31 -!- Vorpal has quit (Changing host).
16:14:31 -!- Vorpal has joined.
16:37:03 <cpressey> What they don't tell you is that the shoes are highly sought-after because they cause the wearer to become invisible and able to sneak up on dragons and slay them and take their treasure.
16:37:21 <cpressey> And the reason they don't tell you these things, is because they're not true.
16:41:58 -!- sebbu has joined.
16:45:43 -!- sebbu2 has quit (Ping timeout: 246 seconds).
16:46:07 -!- sebbu2 has joined.
16:48:48 -!- sebbu has quit (Ping timeout: 245 seconds).
16:48:53 -!- sebbu2 has changed nick to sebbu.
17:00:04 <cpressey> Hmm. Four languages called "Robin" on Github, and only one of them's mine.
17:00:12 -!- cpressey has quit (Quit: A la prochaine.).
17:21:24 -!- Phantom_Hoover has joined.
17:31:55 -!- b_jonas has joined.
17:35:05 -!- xkapastel has quit (Quit: Connection closed for inactivity).
17:35:37 <b_jonas> fungot, has SGDQ started yet?
17:35:38 <fungot> b_jonas: is it 1974? what's for supper? can i program as if it was much thanks to oerjan)). how do you duplicate the list d e k f g c h i j w p r
17:36:09 <HackEso> olist 1176: shachaf oerjan Sgeo FireFly boily nortti b_jonas
17:38:01 <b_jonas> "<shachaf> Why would ELF symbol relocations be relevant for a statically linked executable?" => the program will refer to symbols in vdso
17:54:27 <b_jonas> "<cpressey> Here's a stack. No, there's no stack now. Okay, now there's a stack again, but it's a different stack." => right, a cactus stack, because if you capture a continuation and leak it, it keeps a reference to the stack frame (and all stack frames below) even though you've exited those already
17:54:50 <moony> all hail the cactus stack
17:55:19 <moony> pointy and prickly and stabs whoever dares touch it
17:58:28 <rain1> fungot, has SGDQ started yet?
17:58:28 <fungot> rain1: i got it set up a return address) to each function, correct?)
18:04:45 <b_jonas> int-e: that may be the history, but it also happens to allow cooperative context switching between execution threads, which is sort of nice to show how powerful that primitive is
18:05:58 <b_jonas> alternately maybe it started because someone wrote a lisp an interpreter that stored the stack frames individually allocated in a linked list on the heap, and then noticed that now his interpreter is so inefficient that they can implement call/cc without making it too much worse
18:07:00 <b_jonas> `! befunge 64+"!dlroW ,olleH">:#,_@
18:07:10 <HackEso> `! emulates the ! command of our former bot EgoBot. You write `! then the name of the language then a program, and it runs the program you give and returns the result. We used to use it to test out esoprograms in-channel all the time, but the set of included esolangs is fairly old now and so it's rarely used.
18:08:34 <fungot> rain1: well i guess i could
18:08:51 <fungot> moony: so i've always tied another on top of scheme, i don't know how
18:13:17 <b_jonas> "<int-e> ... I have a genuine problem with applying percentages to causes of death when we're dealing with a 100% mortality rate in the long run." => the mortality rates are usually given in deaths per year though, so they don't add up to 100%, they add up to about 1/70 year^-1
18:24:26 <b_jonas> fungot: is the weather warm at wherever you are too? I guess you're in a server room with nice heat conditioning.
18:24:28 <fungot> b_jonas: ( map ' ( 1 2 4 8 16... 2n, the difference between what?! what good is a kaiser roll without a little
18:25:15 <b_jonas> today's the last hot day though
18:25:26 -!- Sgeo_ has quit (Ping timeout: 258 seconds).
18:26:33 <b_jonas> it will be less hot during the week
18:30:08 -!- moony has changed nick to nogoawayiciloo.
18:30:18 -!- nogoawayiciloo has changed nick to moony.
18:38:30 -!- FreeFull has joined.
18:41:23 -!- moony has quit (Quit: Bye!).
18:41:40 -!- asdfbot has quit (Ping timeout: 272 seconds).
18:42:14 -!- moony has joined.
18:44:55 -!- Sgeo has joined.
19:15:27 <shachaf> int-e: It doesn't? It seems to in the (reset (begin ...)) example on Wikipedia.
19:18:21 <shachaf> int-e: In my variant, {} is the delimiter, and { a; b; c; } means { a; { b; c; } }, but I don't think regular shift/reset does that.
19:25:46 <moony> I need to take higher math classes sooner, so i can understand some of the stuff talked about in here :P
19:31:41 <b_jonas> moony: I'm not sure it would let you understand the crazy stuff on this channel, but I do support the idea of taking math classes
19:32:14 <moony> b_jonas: fair. And I would take the classes anyways
19:32:44 <b_jonas> it's worth for things other than understanding #esoteric
19:33:03 <shachaf> Mathematical Anti Telharsic Harfatum Septomin
19:34:26 <moony> because things like set theory
19:38:17 <b_jonas> why set theory in particular?
19:40:35 <shachaf> let this = Goodstein's theorem in Do you like this?
19:51:43 -!- Vorpal has quit (Ping timeout: 245 seconds).
19:56:46 -!- Vorpal has joined.
19:56:46 -!- Vorpal has quit (Changing host).
19:56:46 -!- Vorpal has joined.
20:01:32 <shachaf> whoa, https://bitbucket.org/blog/sunsetting-mercurial-support-in-bitbucket
20:27:21 -!- Lord_of_Life_ has joined.
20:28:21 -!- Lord_of_Life has quit (Ping timeout: 244 seconds).
20:30:04 <moony> b_jonas: I see it a lot, and think it could be useful for software optimization, as well
20:30:16 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
20:32:09 <shachaf> int-e: Oh, maybe you're right. I wish I could test this.
21:02:41 -!- b_jonas has quit (Quit: leaving).
21:23:32 -!- moony has changed nick to asdfbot2.
21:28:01 -!- asdfbot2 has quit (Quit: Bye!).
21:28:23 -!- moony has joined.
21:39:06 -!- AnotherTest has quit (Ping timeout: 268 seconds).
21:50:42 -!- xkapastel has joined.
21:56:25 -!- ais523 has joined.
21:56:48 <ais523> I'm currently trying to learn the theorem prover / SAT solver Z3
21:58:16 <shachaf> Oh, I was trying to use Z3 the other day.
21:58:24 <ais523> it produces some pretty esoteric answers sometimes
21:58:45 <ais523> for example, if you ask it "find an integer x such that x * x > 3", it pretty consistently produces the answer -8
21:58:56 <ais523> which is a valid answer to the question, but not one I would have thought of
22:00:23 <ais523> `! brachylog A×↙A>3∧Aw
22:00:39 <ais523> Brachylog's answer to the same question is more expected
22:07:02 <shachaf> Hmm, when you link against a .o, does dead coffee elimination on functions you don't use typically happen?
22:07:32 <shachaf> It seems like that would put a bunch of restrictions on the .o
22:08:02 <shachaf> Or maybe this is why people use .a instead of .o files, because it can only be done on the file level?
22:08:20 <moony> for C/C++ using GCC/Clang, it only happens if you use -fLTO, which adds a lot of link-time data that can be used for dead code elimination, among other optimizations
22:08:45 <shachaf> Man. That sounds mega complicated.
22:09:10 <shachaf> I want to write my own linker for my own program but I still want to use C libraries.
22:09:14 <moony> it's compilerspecific
22:09:32 <shachaf> But .o files are a standard format.
22:09:48 <shachaf> Probably some kind of .note.gnu.whatever section
22:09:54 <shachaf> What's the situation on Windows?
22:10:08 <moony> Windows is dominated by MSVC, which is closed source
22:10:31 <shachaf> And the PE format is pretty well documented
22:12:10 <moony> i don't really use windows
22:15:48 <ais523> shachaf: by default, you get no dead code elimination with .o but do get dead code elimination with .a (in the sense that an entire file in the archive won't be used if nothing in it is referenced)
22:16:55 <ais523> the way LTO is implemented is normally a fairly good approximation to "let's just do all the actual work of the compile during the link"
22:17:12 <ais523> of course some of it is done during the compile step, but it moves a number of compile steps to happen at link-time instead
22:17:26 <ais523> this needs a very configurable linker so that you can ask it to call back into the compiler
22:20:04 <shachaf> Wow, that sounds horrible.
22:20:22 <shachaf> Why does it need to call back into the compiler?
22:22:13 <ais523> to do the rest of the optimisation
22:22:31 <shachaf> Is it things like cross-module inlining?
22:22:59 <shachaf> That sounds so complicated.
22:24:41 <ais523> it's basically cross-module everything, a typical LTO is the equivalent of just dumping your entire program (and its libraries) into one file with #include and optimising that
22:25:45 <shachaf> Then why not just do whole-program compilation?
22:26:10 <ais523> that's pretty much what's happening, I think
22:26:24 <ais523> but -fLTO is stronger than -fwhole-program because it looks in the libraries for things to optimise in too
22:26:47 <ais523> also, you do get incremental builds to some extent
22:26:59 <ais523> because there is a lot of work the compiler has to do before it even starts to optimise the program
22:27:11 <ais523> and many optimisations are done first on a single procedure before being extended to being interprocedural
22:27:14 <shachaf> The problem is that I want to write my program in a non-gcc language.
22:27:32 <shachaf> But I want to use some libraries written in C.
22:29:46 <ais523> it's probably best to not LTO against them, in that case
22:29:55 <ais523> unless your compiler and theirs have a common backend
22:30:08 <ais523> I'm not aware of any LTOers which try to parse asm, although it's an interesting idea
22:30:25 <ais523> generally speaking optimisations want a higher-level source format anyway so that they know what UB they're allowed to exploit
22:30:26 <shachaf> Isn't the basic idea of a linker that it supports linking code written in multiple languages?
22:30:34 <shachaf> That's the only reason you need a linker or object files.
22:31:03 <ais523> no, the main reason you need a linker is for updating separately compiled files so that they reference each other
22:31:12 <ais523> that's useful even within a single language
22:31:28 <ais523> many linkers do support multiple source languages, typically by only working at the asm level anyway
22:31:36 <moony> GCC and LLVM both use a intermediate language for LTO
22:31:43 <moony> LLVM uses it's IR, as expected
22:31:46 <ais523> but I was once paid to write a linker, and that linker was specific to a single language
22:32:21 <ais523> its main purpose was to generate glue code to allow different compilation units to call functions defined in each other
22:32:57 <shachaf> But splitting a program into multiple translation units is an implementation detail of a compiler.
22:33:03 <shachaf> You could just do whole program compilation.
22:34:37 <ais523> the main reason not to is because the separate translation units make incremental builds much easier to implement
22:35:04 <ais523> (obviously, implementing incremental builds with whole-program compilation isn't impossible, but building a file at a time is a really easy way to do them and it's what's normally done in practice)
22:35:17 <shachaf> I'm not sure how much incremental builds matter.
22:35:33 <ais523> …do you never work on large programs?
22:35:59 <ais523> even on something like NetHack, which isn't even large, there are at least tens of seconds difference between an incremental build and a full rebuild
22:36:16 <shachaf> I mean that I find the argument that compilers should be way faster and then incrementality doesn't matter so much pretty compelling.
22:36:34 <shachaf> Hmm, I bet NetHack would compile faster if it was in one translation unit.
22:36:55 <ais523> it would, there are a lot of headers that are recursively included in everything
22:36:57 <fizzie> We have [REDACTED] lines of code in [REDACTED], and incremental builds are pretty [REDACTED] for it.
22:37:28 <shachaf> Certainly [REDACTED] benefits from incremental builds.
22:37:51 <shachaf> But it's probably written in C++ or something.
22:38:23 <ais523> I sort-of would prefer to go the other way, I think compilers should consider spending more effort than they do a) proving the input program correct and b) optimising it
22:39:09 <shachaf> Well, a very fast debug-only build should be available.
22:40:21 <shachaf> At one point Chromium started combining its translation units into larger chunks (I think ~30 files each maybe?) to make compilation faster.
22:40:48 <shachaf> The trouble with (some) C++ code is that all the code is in headers, so each translation includes the entire program.
22:42:39 <fizzie> Heh, the Chrome build instructions start with: "Are you a Google employee? See go/building-chrome instead."
22:43:34 <fizzie> I mean, the Chromium build instructions.
22:44:28 -!- ais523 has quit (Remote host closed the connection).
22:45:41 -!- ais523 has joined.
22:45:51 <fizzie> I think they've been switching build systems every now and then. I guess it's still GN+Ninja though.
22:46:05 <fizzie> But it definitely was GYP before, and I think something else before that.
22:48:22 <shachaf> I'm trying to build NetHack now to compare build times.
22:48:44 <shachaf> But the build instructions are convoluted so I still haven't figured it out.
22:49:32 <ais523> shachaf: for NetHack 3.4.3, try this patch: https://bilious.alt.org/?452
22:49:53 <ais523> it automates all the manual steps of the build
22:50:29 <ais523> that has a different build system
22:50:40 <ais523> but it's a bit easier to use than 3.4.3's once you have an appropriate hints file
22:50:48 <shachaf> ais523: Hmm, instead of application/octet-stream you should serve your .patch fail as text/plain so it opens in browsers.
22:51:52 <shachaf> Oh, I was only looking for executable files in the hints directory, with tab completion. So I thought there was only one for Mac OS.
22:52:33 <ais523> the one for Linux mostly works apart from the directories I think
22:52:47 <ais523> oh, hmm, apparently bilious is downloading it /from/ my website
22:53:18 <ais523> text/plain is the wrong MIME type for a diff, though (and there are security reasons not to use text/plain for /anything/ online, blame Microsoft)
22:53:39 <moony> ais523: what's MS do
22:54:18 <ais523> moony: some versions of IE interpret text/plain as text/html if they think the file looks sufficiently HTMLlish
22:54:27 <ais523> this allows XSS attacks against plaintext files
22:54:48 <ais523> (last time this conversation came up, someone successfully XSS-attacked oerjan via a plaintext log file)
22:54:59 <ais523> (so it's not just a theoretical issue)
22:55:03 <ais523> log for #esoteric, that is
22:57:10 <fizzie> There were some workarounds though. Like, X-Content-Type-Options=nosniff on IE >= 8.0, which is... well, it's something.
22:57:42 <shachaf> Well, I really don't like application/octet-stream because no browser shows a preview option.
22:57:44 -!- FreeFull has quit.
22:57:51 <moony> note to self: put demo for this madness on hellomouse.net
22:57:54 <ais523> the workaround we were always told to use on Wikipedia was to serve as text/css
22:57:55 <shachaf> This is really a problem with browsers, but all browsers have this behavior.
22:58:19 <ais523> fwiw, when I followed the link it opened in my text editor, with syntax highlighting
22:58:24 <fizzie> ais523: I think that works on older versions of IE than just the header.
22:58:32 <ais523> but I suspect that's a consequence of some configuration I did in the past
22:59:01 <ais523> "on Wikipedia" here = to prevent people XSS-attacking Wikipedia itself
22:59:08 <fizzie> I'm sending "Content-Type: text/plain" + "X-Content-Type-Options: nosniff" from hack.esolangs.org/tmp/... URLs.
22:59:39 <fizzie> I guess that should probably be served from a different second-level domain than the wiki, actually.
22:59:56 <fizzie> But I don't want to pay for esolangsusercontent.com or some such.
23:01:07 <ais523> are the wiki cookies marked HTTP-only?
23:01:17 <ais523> that would probably be enough as far as mitigations go
23:01:42 <ais523> I'd test this but I'm not particularly inclined to fire up IE on the live internet
23:01:55 <ais523> especially as the version of IE that I have installed is IE6
23:02:35 <fizzie> I think at least some of them are.
23:02:46 <shachaf> Man, NetHack has all sorts of problems.
23:02:54 <fizzie> "Set-Cookie: esolang_wiki_session=[redacted]; path=/; secure; HttpOnly"
23:02:55 <shachaf> Like multiple incompatible definitions of "struct monst".
23:04:44 <ais523> that's a new one for me
23:05:04 <shachaf> Putting everything into one translation unit will show all sorts of odd things.
23:05:21 <shachaf> Some of them are sort of reasonable, like #defines for common words without #undefs.
23:05:49 <ais523> objects.h gets compiled twice, the first time uses a dummy definition for struct monst
23:07:43 <shachaf> objects.c is compiled twice? Oh no.
23:08:24 <ais523> several of the files that are compiled are generated from other compiled files at build time
23:13:26 -!- Phantom_Hoover has quit (Quit: Leaving).
23:20:51 <ais523> what's the name for the version of boolean satisfaction where you can put as many forall quantifiers as you like at the start, but don't get other quantifiers or quantifiers anywhere else?
23:21:06 <ais523> e.g. "find x, y, such that forall a, b, c, f(a,b,c,x,y) is true"
23:22:47 <shachaf> Someone told me the name of that recently but I've forgotten it.
23:28:39 <shachaf> Without -O, NetHack builds in <5 seconds on my machine.
23:28:42 <esowiki> [[Blackspace]] N https://esolangs.org/w/index.php?oldid=65581 * A * (+219) Created page with "[[Blackspace]] is an [[esoteric programming language]] completely based on the old-fashioned control characters. Currently this page is a placeholder. [[Category:2019]] Cat..."
23:28:42 -!- Sgeo has quit (Read error: Connection reset by peer).
23:29:05 -!- Sgeo has joined.
23:29:19 <esowiki> [[Husk]] M https://esolangs.org/w/index.php?diff=65582&oldid=65577 * A * (+30)
23:33:12 <shachaf> (This is unrelated to the one-translation-unit thing, which isn't working very well in this code base.)
23:33:50 <shachaf> Also a big problem is that you can only get parallelization in most compilers by breaking up your code into multiple translation units.
23:38:45 <ais523> I thought that but forgot to say it in-channel
23:47:40 -!- atslash has quit (Quit: This computer has gone to sleep).
23:49:54 <shachaf> Is -O even relevant to a program like NetHack?
23:52:04 <ais523> yes, we need to do optimisation rounds every now and then
23:52:38 <ais523> vanilla NetHack was designed for very old computers where it ran very slowly, so a lot of optimisation was needed for that and means that we can afford to be sloppy when running old parts of the code on modern computers
23:53:05 <ais523> but NetHack derivatives like NH4 take advantage of the speed of modern computers to do things like continuously saving the game (the save code is pretty slow)
23:53:31 <ais523> also, reading code compiled at -O0 hurts to look at
23:53:50 <ais523> it often doesn't even really use registers, everything gets loaded from memory for one instruction then put right back into memory
23:54:58 <moony> there can be programs that behave differently because of how unoptimized -O0 is
23:55:10 <moony> and languages like Rust kinda depend on -O1 or better to even make good code
23:55:20 <shachaf> But if you're recompiling for development (which is the case where you want incremental builds) you presumably don't care about that so much.
23:55:33 <shachaf> Yes, Rust has certainly taken that part of the C++ philosophy.
23:56:25 <moony> i.e. take Rust futures
23:56:28 <moony> if they weren't optimized
23:56:36 <moony> a single Future object could reach 100s of KBs large
23:56:39 <ais523> shachaf: I consider the generation of suboptimal asm to be a bug
23:56:56 <ais523> in either the compilier or the source code, but the source code is normally easier to fix
23:57:08 <shachaf> But generating optimal assembly is uncomputable.
23:57:10 <ais523> I'll write a piece of the program, then look at the generated asm to see if it's fast enough or if I need to do better
23:57:24 <ais523> shachaf: depends on what the program is doing
23:57:42 <ais523> in many cases you just have a finite-state machine, optimising that is very computable
23:57:50 <moony> I think part of the difficulty in generating optimal asm is, yknow, x86 itself
23:57:50 <shachaf> Something like a computer game, even NetHack, is more like a real-time system.
23:57:57 <ais523> why do you think I'm learning Z3? :-D
23:58:14 <shachaf> It's a bug if it's too slow but if you don't miss your deadlines it's fine.
23:58:25 <moony> ais523: compiler for a FSM language that generates nearly optimal ASM when
23:58:26 <ais523> shachaf: I actually really disagree with this
23:58:38 <ais523> I am upset at all the electricity that's being wasted in parts of the cycles that could be idle
23:58:53 <ais523> moony: I'm really seriously considering it atm
23:59:07 <moony> i mean, that'd be amazing for some problems
23:59:19 <shachaf> ais523: I bet more cycles are being used to display NetHack in a GUI terminal than on computing NetHack.
23:59:25 <ais523> actually, Z3 is sufficiently high level that I think you could express it in only a few hundred lines or so of Z3 + a program wrapping it
23:59:52 <ais523> whether Z3 could actually run the resulting program with any sort of efficiency would be the real question
23:59:54 <moony> ais523: good luck handling the insanity that is per-processor behavior and SSE