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 $ a=b b=a; echo $((a)) 07:01:03 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 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 Good morning. I've been reading the R7RS. It's been making me laugh. 09:58:32 I don't mean to say that it is laughable; overall, I like Scheme. 09:58:40 what funny abut it 09:59:02 think R7RS could be better but course corrected well 09:59:59 Mainly, it's amusing when they leave so much wiggle room. 10:00:14 For example, a Scheme implementation is allowed to use symbols outside Unicode if it wants. 10:00:22 They say this explicitly. 10:01:25 oh yeah 10:01:33 they don't even specify stuff about filesystem paths for importing files 10:01:53 in case someone wants an SQL database backed complaint r7rs implementation 10:01:59 the result is you cannot portably do a multiple file project 10:04:56 https://rain-1.github.io/scheme-srfi-1.html 10:06:47 rain1: Is it ironic that *none* of those look like https://srfi.schemers.org/srfi-55/srfi-55.html ? 10:07:24 wow i didnt even realize that 10:07:28 i should add that 10:07:43 (require-extension (srfi 1)) might work in one or more of those 10:07:43 but yeah this is the mess we're in 10:07:51 and everybody is wondering why nobody uses scheme 10:12:17 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 I would remove the call/cc and similar operators 10:12:53 I think it's become clear that they aren't useful 10:16:00 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 For learning about continuations, it's cool. Will I ever actually *use* it...? Probably not. 10:48:39 continuations are easy 10:48:45 delimited continuations are weird 10:49:06 All programming constructions are weird 10:49:08 (bla bla shift bla bla reset bla bla) 10:49:51 Taneb: that was an opinion, of course 10:49:58 Yes 10:50:05 Or maybe a statement that I grokked the former but not the latter. 10:50:42 Whereas what I said was a contrarian but defensible statement made partially in jest 10:57:33 All continuations are delimited, though. 10:57:47 -!- xkapastel has quit (Quit: Connection closed for inactivity). 10:57:58 Therefore continuations are easy and weird 10:59:01 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:23 cpressey: cpresshey 10:59:50 -!- arseniiv has joined. 11:00:05 I'm mystified by this, actually: 11:00:30 * I feel like I understand undelimited continuations 11:00:41 * I feel like I don't understand delimited continuations 11:00:49 * All continuations are delimited 11:01:24 Actually, see "A theory of regulation." in https://www.bloomberg.com/opinion/articles/2017-01-24/metrics-fees-and-regulations 11:01:55 Thing I didn't expect after your list of bullet points about continuations: a link to Bloomberg.com 11:02:26 I only realized that I was quoting that article after I finished writing the bullet points. 11:03:15 shachaf: I'm confused by the shift/reset syntax, and how it translates to the common functional (a -> r) -> r idea. 11:04:08 Maybe I just haven't read the right paper(s) yet. 11:04:51 Haskell Cont continuations are delimited by runCont. 11:05:36 As I said, I'm mainly confused by shift & reset. 11:06:08 I suspect "delimited" refers to something that's not actually the continuation per se -- but I don't really know. 11:06:37 Well, whole program continuations are silly. 11:07:28 Oh, my pseudo-continuation thing has a delimiter, normally written {}. 11:07:34 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 When you write { ...foo`...; ... }, foo gets "{\x; ...x...; ... }" as an argument. 11:08:48 Rather than the entire rest of the program. 11:11:27 In the classic Scheme shift-reset thing, shift is a binder, right? 11:11:31 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 hm how algebraic effects relate to continuations? At least syntactic ideas about the former are more understandable for me 11:13:25 s/about/related to 11:14:20 that handling case-like construct and data-like definition of an effect 11:14:25 Oh, I think I understand shift/reset now. 11:15:05 -!- atslash has joined. 11:15:19 IMO shift takes on itself too much, and that effect syntax takes from it some control to the “reset” side 11:15:27 AFAIR 11:16:08 and then suddenly it starts to resemble control constructs from imperative languages, e. g. try/catch 11:17:53 oh also I had read something that made me think I understood shift/reset, but now I remember it only vaguely 11:21:20 int-e: OK, I now understand shift-reset and can work the examples. 11:21:31 It seems pretty simple. 11:22:38 I'm not sure why shift is called shift, and why it doesn't take a lambda. 11:32:09 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 okay... next question... why? 12:04:03 fungot: why? 12:04:03 int-e: i hope something good came in the mail 12:04:33 That's a better answer than I hoped for. But it's still not very satisfying. 12:05:38 So "delimited" means that instead of one thing called call/cc you have two things called shift and reset 12:06:21 shachaf: there's a subtlety around the behavior of ; inside reset though... 12:06:47 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 shachaf: reset (foo; shift ...) doesn't capture the 'foo' part. 12:07:35 shachaf: otherwise the tree walking wouldn't make sense (I think) 12:09:19 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 int-e: if it explains anything operationally, it was by accident 12:14:15 it was more about... well, hard to say. I am prattling. 12:15:48 Oh was I finding patterns in the noise... mistaking them for communication? I believe that's a common mistake for humans :) 12:15:56 (So maybe I'm human? Who knew...) 12:19:43 I'll chalk it up to coincidence. I was perhaps trying to answer "why?" 12:20:23 This is all so dysfuncational! 12:21:28 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 If I wanted useful, I'd just not deal with continuations at all. 12:22:26 I rather suspect that continuations were meant to be useful. 12:22:27 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 doesn't interest me enough to justify me hunting it down unfortunately 12:24:03 I wonder about the history. 12:24:16 This may have been an accident. 12:27:03 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 (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 ...reset). 3. Hmm, what can we use this new primitive for? 4. 100 papers. ) 12:27:21 *paying attention to 12:27:59 -!- PaniniTheDevelop has joined. 12:28:01 int-e: I believe continuations, the concept, started in denotational semantics. 12:28:10 hello! 12:28:20 So if it's "We want to write a function that describes exception-like behaviour" then yes 12:28:36 cpressey: let's focus on steps 2-4 :) 12:30:25 ("1. God gave us call/cc." - Let's pretend I wrote that instead ;) ) 12:30:28 int-e: https://cs.indiana.edu/~dyb/pubs/monadicDC.pdf refers to a 1987 paper called "Beyond continuations" that 12:30:50 help 12:30:55 PaniniTheDevelop: hi 12:31:01 `relcome PaniniTheDevelop 12:31:02 ​PaniniTheDevelop: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: . (For the other kind of esoterica, try #esoteric on EFnet or DALnet.) 12:31:10 i cant register 12:31:18 PaniniTheDevelop: ask on #freenode 12:31:53 just 12:32:03 i dont know befunge 12:32:14 (oh. register where?) 12:32:22 on the wiki 12:33:13 sorry, I somehow assumed the IRC server 12:33:51 okay... 12:34:02 `bf 64+"!dlroW ,olleH">:#,_@ 12:34:05 No output. 12:34:16 hrm 12:34:40 i think its brainfck 12:37:58 `ibin/befunge 64+"!dlroW ,olleH">:#,_@ 12:37:59 Hello, World! 12:38:22 Now what was the official way to do that... 12:38:25 9857727254>\#+:#*9-#\_$.@ 12:38:30 `help interp 12:38:31 ​`interp? ¯\(°​_o)/¯ 12:38:42 help with this 12:38:56 the `ibin/befunge was important 12:40:25 `! befunge 9857727254>\#+:#*9-#\_$.@ 12:40:26 197596799 12:41:21 `? `! 12:41:22 ​`! 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:40 thanks 12:41:53 [[Special:Log/newusers]] create * PaniniTheDeveloper * New user account 12:42:12 yaaay 12:42:23 One more hoop to jump through. 12:42:30 what 12:45:50 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 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 If the latter, it is probably the only instance ever of people being paid to code in Befunge. 12:52:06 Anyway I didn't realize there was a captcha at all 12:54:37 cpressey: I imagine the reward to be more along the lines of being allowed to download a couple of pornographic videos. 12:55:26 or maybe a "stress-test" of the network connection of "a friend". 12:57:19 oh dear 13:01:44 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 [[Emoji]] M https://esolangs.org/w/index.php?diff=65578&oldid=65554 * Dtuser1337 * (-35) removing unnecessary newlines. 14:09:54 [[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 [[Emoji]] M https://esolangs.org/w/index.php?diff=65580&oldid=65579 * Dtuser1337 * (+1) trying out new thing. 14:17:22 I think delimited continuations are easier 14:17:28 for one thing you can algebraically axiomatize them 14:17:52 (2004) Axioms for Delimited Continuations in the CPS Hierarchy - Yukiyoshi Kameyama 14:18:49 if you wanted to define orthogonal language constructs in terms of continuations you need multiple-prompt continuations to separate them though 14:39:47 ("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 if you’re right, call/cc = integers 14:40:36 call/succ 14:42:15 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 oh one time I was bored and tried to make Peano-like axioms for Z 14:42:52 it ended up too verbose 14:49:35 arseniiv: I thought he gave use more tablets full of commandments but Moses was too lazy to carry them down the mountain? 14:49:56 maybe 14:50:01 they are heavy 14:50:17 should've used paper 14:50:40 arseniiv: hmm, 0 is in Z, succ is a bijection from Z -> Z such that succ(x) != x 14:51:48 Induction's the tricky one, as always 14:51:55 * int-e tries to find context 14:52:08 ah. "I was bored and tried to make Peano-like axioms" 14:52:47 I added prev and tried to make sure pred succ = succ pred = id 14:52:59 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 arseniiv: I was trying to be sneaky and rely on pred existing due to succ being bijective 14:53:28 Taneb: yeah, I wrote it in that way, though using pred instead of succ^−1 14:53:32 Z is the monoid given by the presentation 14:53:53 (that's ) 14:54:12 int-e: that’s cheating 14:54:28 arseniiv: we can translate that back into peano style, surely. 14:54:54 It just won't be nearly as nice as Peano's axioms... unfortunately. 14:55:19 though all said, I like the definition of N as a free monoid on one generator :) 14:55:42 then we can add multiplication more or less naturally 14:56:12 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 yeah it’s a nice construction and works for more things, I forgot what it’s named in general 14:57:37 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 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 Taneb: what do you mean by succ^-1? 14:58:57 is ^-1 just a constructor 14:59:18 or maybe succ^-1 is a single constructor 14:59:24 Taneb: I'd be happier if you used `pred` and axioms for the interaction of succ and pred 15:01:00 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 so putting that equationally, you have pred(succ(x)) = x and succ(pred(x)) = x. 15:02:48 oh ok i get it 15:02:55 BTW 15:03:07 http://minikanren.org/workshop/2019/minikanren19-final4.pdf I like this 15:04:07 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 what theorem is that 15:05:52 I am probably missing something, but, how is this not group theory 15:05:56 I guess its some fundamental result from term rewriting theory 15:07:26 (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 This /is/ related to standard consitency formulated in terms of booleans: we don't want to have false = true. 15:16:27 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 ...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 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:00 OK, well, yes, ok 15:19:13 Eh bien, gut, ok, yes, ok 15:19:26 Sorry, I've worked in this field for 8 years. Some things stick :P 15:20:34 Is it not the case that "Peano-like axioms for Z" would be roughly the same as "Axioms for (infinite, ordered) groups" 15:21:16 Hmm, ordered. 15:21:24 abelian would've been my first instinct 15:21:44 abelian, right, that too 15:21:52 But s() induces an order, I'm sure 15:22:16 until it runs into a cycle (and cycle avoidance is the main challenge here) 15:22:25 I sure hope it induces an order, or I've wandered into an episode of The Twilight Zone 15:22:51 modulo 3 you have 0 < 1 < 2 < 0 < 1 < 2 < 0 < 1 ... 15:23:06 That's not much of an order, if you ask me. 15:23:26 Who ordered this? 15:23:27 Anyway, that's what derailed *my* train of thought. 15:23:51 And at least it's still a quasi-order. 15:24:53 and even a... https://en.wikipedia.org/wiki/Well-quasi-ordering 15:25:19 -!- xkapastel has joined. 15:25:27 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 I think the peano axioms do imply the set is infinite 15:31:43 by induction 15:32:09 (the axiom schema, not the proof method) 15:32:35 Because succ is injective and there's no natural n such that succ(n) = 0 15:32:36 couldn't you just assume you had a finite model then add one to the biggest number 15:34:08 I'm completely lost then. That's okay. 15:34:46 I'm not sure where the modulo 3 thing came from. 15:35:12 Me neither 15:35:29 well if you had a finite model 15:35:36 take the biggest element 15:35:44 the assumption is that S(biggest) is not in that set 15:36:03 if it was in the set, then you have S(biggest) = something so theres a loop, kind of like modular arithmetic 15:36:09 rain1: I don't think that that's where cpressey is lost 15:40:14 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:17 I could be totally wrong 15:40:47 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 And that's where modulo 3 could come in, I can see that 15:41:36 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 int-e: it's amazing the things that happen in this world 15:48:55 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 Taneb: And disturbing. 15:57:40 -!- Sgeo_ has joined. 16:00:52 -!- Sgeo__ has quit (Ping timeout: 245 seconds). 16:03:34 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 . 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 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 I remember seeing some headline that eating cheese reduces death rate from all causes 16:11:14 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 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 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 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:34:09 * moony lurks 17:35:05 -!- xkapastel has quit (Quit: Connection closed for inactivity). 17:35:37 fungot, has SGDQ started yet? 17:35:38 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:06 `olist 1176 17:36:09 olist 1176: shachaf oerjan Sgeo FireFly boily nortti b_jonas 17:38:01 " Why would ELF symbol relocations be relevant for a statically linked executable?" => the program will refer to symbols in vdso 17:54:27 " 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 all hail the cactus stack 17:55:19 pointy and prickly and stabs whoever dares touch it 17:58:28 fungot, has SGDQ started yet? 17:58:28 rain1: i got it set up a return address) to each function, correct?) 18:04:45 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 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 `! befunge 64+"!dlroW ,olleH">:#,_@ 18:07:01 Hello, World! 18:07:07 int-e: ^ the official way 18:07:09 `? `! 18:07:10 ​`! 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:33 fungot: r7rs 18:08:34 rain1: well i guess i could 18:08:51 fungot: rust 18:08:51 moony: so i've always tied another on top of scheme, i don't know how 18:10:52 heh, analyzing the axioms 18:13:17 " ... 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 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 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 today's the last hot day though 18:25:26 -!- Sgeo_ has quit (Ping timeout: 258 seconds). 18:26:33 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 int-e: It doesn't? It seems to in the (reset (begin ...)) example on Wikipedia. 19:18:21 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 I need to take higher math classes sooner, so i can understand some of the stuff talked about in here :P 19:31:41 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 b_jonas: fair. And I would take the classes anyways 19:32:19 i like math 19:32:33 right 19:32:44 it's worth for things other than understanding #esoteric 19:33:03 Mathematical Anti Telharsic Harfatum Septomin 19:34:26 it'd help a bit 19:34:26 because things like set theory 19:38:17 why set theory in particular? 19:40:35 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 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 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 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 I'm currently trying to learn the theorem prover / SAT solver Z3 21:58:16 Oh, I was trying to use Z3 the other day. 21:58:24 it produces some pretty esoteric answers sometimes 21:58:33 SMT solvers are TG 21:58:45 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 which is a valid answer to the question, but not one I would have thought of 22:00:23 `! brachylog A×↙A>3∧Aw 22:00:26 2 \ true. 22:00:39 Brachylog's answer to the same question is more expected 22:07:02 Hmm, when you link against a .o, does dead coffee elimination on functions you don't use typically happen? 22:07:08 Dead code elimination 22:07:32 It seems like that would put a bunch of restrictions on the .o 22:07:55 shachaf: depends 22:08:02 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 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 Man. That sounds mega complicated. 22:09:10 I want to write my own linker for my own program but I still want to use C libraries. 22:09:14 it's compilerspecific 22:09:17 so 22:09:20 yea.. 22:09:32 But .o files are a standard format. 22:09:48 Probably some kind of .note.gnu.whatever section 22:09:54 What's the situation on Windows? 22:09:55 yea, prolly 22:09:59 Windows? 22:10:08 Windows is dominated by MSVC, which is closed source 22:10:10 have fun 22:10:21 lld links on Windows 22:10:31 And the PE format is pretty well documented 22:12:01 i mean 22:12:07 i dunno 22:12:10 i don't really use windows 22:13:59 Neither do I. 22:15:48 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 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 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 this needs a very configurable linker so that you can ask it to call back into the compiler 22:20:04 Wow, that sounds horrible. 22:20:22 Why does it need to call back into the compiler? 22:22:13 to do the rest of the optimisation 22:22:31 Is it things like cross-module inlining? 22:22:59 That sounds so complicated. 22:24:41 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 Then why not just do whole-program compilation? 22:26:10 that's pretty much what's happening, I think 22:26:24 but -fLTO is stronger than -fwhole-program because it looks in the libraries for things to optimise in too 22:26:47 also, you do get incremental builds to some extent 22:26:59 because there is a lot of work the compiler has to do before it even starts to optimise the program 22:27:11 and many optimisations are done first on a single procedure before being extended to being interprocedural 22:27:14 The problem is that I want to write my program in a non-gcc language. 22:27:32 But I want to use some libraries written in C. 22:29:46 it's probably best to not LTO against them, in that case 22:29:55 unless your compiler and theirs have a common backend 22:30:08 I'm not aware of any LTOers which try to parse asm, although it's an interesting idea 22:30:25 generally speaking optimisations want a higher-level source format anyway so that they know what UB they're allowed to exploit 22:30:26 Isn't the basic idea of a linker that it supports linking code written in multiple languages? 22:30:34 That's the only reason you need a linker or object files. 22:31:03 no, the main reason you need a linker is for updating separately compiled files so that they reference each other 22:31:12 that's useful even within a single language 22:31:28 many linkers do support multiple source languages, typically by only working at the asm level anyway 22:31:36 GCC and LLVM both use a intermediate language for LTO 22:31:43 LLVM uses it's IR, as expected 22:31:46 but I was once paid to write a linker, and that linker was specific to a single language 22:31:48 GCC uses GIMPLE 22:32:21 its main purpose was to generate glue code to allow different compilation units to call functions defined in each other 22:32:57 But splitting a program into multiple translation units is an implementation detail of a compiler. 22:33:03 You could just do whole program compilation. 22:34:37 the main reason not to is because the separate translation units make incremental builds much easier to implement 22:35:04 (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 I'm not sure how much incremental builds matter. 22:35:33 …do you never work on large programs? 22:35:59 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 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 Hmm, I bet NetHack would compile faster if it was in one translation unit. 22:36:55 it would, there are a lot of headers that are recursively included in everything 22:36:57 We have [REDACTED] lines of code in [REDACTED], and incremental builds are pretty [REDACTED] for it. 22:37:28 Certainly [REDACTED] benefits from incremental builds. 22:37:51 But it's probably written in C++ or something. 22:38:23 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 Well, a very fast debug-only build should be available. 22:40:21 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 The trouble with (some) C++ code is that all the code is in headers, so each translation includes the entire program. 22:42:39 Heh, the Chrome build instructions start with: "Are you a Google employee? See go/building-chrome instead." 22:43:34 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 I think they've been switching build systems every now and then. I guess it's still GN+Ninja though. 22:46:05 But it definitely was GYP before, and I think something else before that. 22:48:22 I'm trying to build NetHack now to compare build times. 22:48:44 But the build instructions are convoluted so I still haven't figured it out. 22:49:32 shachaf: for NetHack 3.4.3, try this patch: https://bilious.alt.org/?452 22:49:53 it automates all the manual steps of the build 22:50:10 I'm trying 3.6.2 22:50:29 that has a different build system 22:50:40 but it's a bit easier to use than 3.4.3's once you have an appropriate hints file 22:50:48 ais523: Hmm, instead of application/octet-stream you should serve your .patch fail as text/plain so it opens in browsers. 22:51:07 that isn't my website 22:51:09 just my patch 22:51:35 Ah. 22:51:52 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 the one for Linux mostly works apart from the directories I think 22:52:47 oh, hmm, apparently bilious is downloading it /from/ my website 22:53:18 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 ais523: what's MS do 22:54:18 moony: some versions of IE interpret text/plain as text/html if they think the file looks sufficiently HTMLlish 22:54:27 this allows XSS attacks against plaintext files 22:54:29 pffffft 22:54:48 (last time this conversation came up, someone successfully XSS-attacked oerjan via a plaintext log file) 22:54:59 (so it's not just a theoretical issue) 22:55:03 log for #esoteric, that is 22:57:10 There were some workarounds though. Like, X-Content-Type-Options=nosniff on IE >= 8.0, which is... well, it's something. 22:57:42 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 note to self: put demo for this madness on hellomouse.net 22:57:54 the workaround we were always told to use on Wikipedia was to serve as text/css 22:57:55 This is really a problem with browsers, but all browsers have this behavior. 22:58:19 fwiw, when I followed the link it opened in my text editor, with syntax highlighting 22:58:24 ais523: I think that works on older versions of IE than just the header. 22:58:32 but I suspect that's a consequence of some configuration I did in the past 22:59:01 "on Wikipedia" here = to prevent people XSS-attacking Wikipedia itself 22:59:08 I'm sending "Content-Type: text/plain" + "X-Content-Type-Options: nosniff" from hack.esolangs.org/tmp/... URLs. 22:59:39 I guess that should probably be served from a different second-level domain than the wiki, actually. 22:59:56 But I don't want to pay for esolangsusercontent.com or some such. 23:01:07 are the wiki cookies marked HTTP-only? 23:01:17 that would probably be enough as far as mitigations go 23:01:42 I'd test this but I'm not particularly inclined to fire up IE on the live internet 23:01:55 especially as the version of IE that I have installed is IE6 23:02:35 I think at least some of them are. 23:02:46 Man, NetHack has all sorts of problems. 23:02:54 "Set-Cookie: esolang_wiki_session=[redacted]; path=/; secure; HttpOnly" 23:02:55 Like multiple incompatible definitions of "struct monst". 23:04:44 that's a new one for me 23:05:04 Putting everything into one translation unit will show all sorts of odd things. 23:05:21 Some of them are sort of reasonable, like #defines for common words without #undefs. 23:05:38 oh, I see 23:05:49 objects.h gets compiled twice, the first time uses a dummy definition for struct monst 23:05:53 *objects.c 23:07:43 objects.c is compiled twice? Oh no. 23:08:24 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 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 e.g. "find x, y, such that forall a, b, c, f(a,b,c,x,y) is true" 23:22:47 Someone told me the name of that recently but I've forgotten it. 23:28:39 Without -O, NetHack builds in <5 seconds on my machine. 23:28:42 [[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 [[Husk]] M https://esolangs.org/w/index.php?diff=65582&oldid=65577 * A * (+30) 23:33:12 (This is unrelated to the one-translation-unit thing, which isn't working very well in this code base.) 23:33:50 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 I thought that but forgot to say it in-channel 23:40:36 Me too. 23:47:40 -!- atslash has quit (Quit: This computer has gone to sleep). 23:49:54 Is -O even relevant to a program like NetHack? 23:52:04 yes, we need to do optimisation rounds every now and then 23:52:38 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 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 also, reading code compiled at -O0 hurts to look at 23:53:50 it often doesn't even really use registers, everything gets loaded from memory for one instruction then put right back into memory 23:54:31 yes, -O0 bad 23:54:42 also 23:54:58 there can be programs that behave differently because of how unoptimized -O0 is 23:55:10 and languages like Rust kinda depend on -O1 or better to even make good code 23:55:20 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 Yes, Rust has certainly taken that part of the C++ philosophy. 23:56:25 i.e. take Rust futures 23:56:28 if they weren't optimized 23:56:36 a single Future object could reach 100s of KBs large 23:56:39 shachaf: I consider the generation of suboptimal asm to be a bug 23:56:46 ^ 23:56:56 in either the compilier or the source code, but the source code is normally easier to fix 23:57:08 But generating optimal assembly is uncomputable. 23:57:10 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 shachaf: depends on what the program is doing 23:57:42 in many cases you just have a finite-state machine, optimising that is very computable 23:57:50 I think part of the difficulty in generating optimal asm is, yknow, x86 itself 23:57:50 Something like a computer game, even NetHack, is more like a real-time system. 23:57:57 why do you think I'm learning Z3? :-D 23:58:14 It's a bug if it's too slow but if you don't miss your deadlines it's fine. 23:58:25 ais523: compiler for a FSM language that generates nearly optimal ASM when 23:58:26 shachaf: I actually really disagree with this 23:58:38 I am upset at all the electricity that's being wasted in parts of the cycles that could be idle 23:58:53 moony: I'm really seriously considering it atm 23:59:07 i mean, that'd be amazing for some problems 23:59:19 ais523: I bet more cycles are being used to display NetHack in a GUI terminal than on computing NetHack. 23:59:25 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 whether Z3 could actually run the resulting program with any sort of efficiency would be the real question 23:59:54 ais523: good luck handling the insanity that is per-processor behavior and SSE