00:00:00 -!- hppavilion[2] has joined.
00:01:04 -!- FreeFull has quit.
00:03:39 -!- hppavilion[1] has quit (Ping timeout: 265 seconds).
00:04:59 -!- arseniiv has quit (Ping timeout: 276 seconds).
01:35:56 -!- atslash has joined.
01:49:57 -!- oerjan has joined.
01:58:55 -!- hppavilion[2] has quit (Remote host closed the connection).
02:09:02 <esowiki> [[HackEso]] M https://esolangs.org/w/index.php?diff=67458&oldid=67391 * Oerjan * (-7) /* The wisdom and quote databases */ Wrong directory
02:27:43 <esowiki> [[Hello world program in esoteric languages]] https://esolangs.org/w/index.php?diff=67459&oldid=67446 * Oerjan * (-1) Remind myself that you've inexplicably failed to mess up the order since my last check. Also fix language name.
02:28:17 <oerjan> (which was back in January)
02:29:32 <oerjan> first time i've checked out Recent Changes in ages
03:00:45 -!- oerjan has set topic: IOCCC source code escaped | Welcome to the international center for esoteric programming library design, development, and deployment! | https://esolangs.org | logs: https://esolangs.org/logs/ http://codu.org/logs/_esoteric/ http://tunes.org/~nef/logs/esoteric/?C=M;O=D https://github.com/KrzysztofSzewczyk/esologs/.
03:05:09 <esowiki> [[HackEso]] M https://esolangs.org/w/index.php?diff=67460&oldid=67458 * Fizzie * (+0) /* The wisdom and quote databases */ I think this was probably intended as formatting.
03:06:58 <fizzie> I think I'll add an "Implementation details" section just for the curious, though not now.
03:09:57 -!- tromp has joined.
03:14:19 -!- tromp has quit (Ping timeout: 252 seconds).
03:30:03 -!- imode has joined.
04:01:34 <esowiki> [[H]] M https://esolangs.org/w/index.php?diff=67461&oldid=67454 * A * (-2) /* Implementations */ Add the new instruction
04:03:50 <esowiki> [[Talk:H]] M https://esolangs.org/w/index.php?diff=67462&oldid=67455 * A * (+316) /* HWorld is a powerful language */
04:05:25 <esowiki> [[Bin-8]] M https://esolangs.org/w/index.php?diff=67463&oldid=67438 * A * (+41) XD means eXtremely Destructible.
04:06:32 <esowiki> [[Talk:H]] M https://esolangs.org/w/index.php?diff=67464&oldid=67462 * A * (-226) /* Q & A */ Not on-topic for this talk page
05:01:00 -!- Lord_of_Life_ has joined.
05:01:21 -!- Lord_of_Life has quit (Ping timeout: 246 seconds).
05:02:22 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
05:50:24 -!- moony has changed nick to noomy.
06:43:48 -!- hakatashi1 has quit (Remote host closed the connection).
06:47:00 -!- hppavilion[1] has joined.
06:57:14 -!- hakatashi has joined.
06:58:09 -!- hakatashi has quit (Remote host closed the connection).
07:13:20 -!- imode has quit (Ping timeout: 276 seconds).
07:19:16 -!- hakatashi has joined.
07:19:17 -!- hakatashi has quit (Read error: Connection reset by peer).
07:45:59 -!- tromp has joined.
07:48:01 -!- hakatashi has joined.
08:34:28 -!- oerjan has quit (Quit: Nite).
08:46:08 -!- hppavilion[1] has quit (Ping timeout: 245 seconds).
08:57:57 -!- b_jonas has quit (Quit: Lost terminal).
10:41:35 -!- wib_jonas has joined.
10:44:27 <wib_jonas> question about string literals. you know how there are languages like postscript where the open and close delimiter for a string literal is different, and you can put those delimiters inside the string unescaped if they are balanced. perl also allows this.
10:46:34 <wib_jonas> And you know how there are languages like Pascal and SQL where if you double the string delimiter inside a string, it escapes to a single delimiter.
10:48:30 <wib_jonas> What I'd like to know is if there's a language where the open and close delimiters for string literals are different, but they don't nest, instead the open delimiter is not special inside the string, and you can start a string literal with the close delimiter instead of the open delimiter, in which case that starting close delimiter is part of the
10:48:31 <wib_jonas> string contents, which effectively means that you can escape a close delimiter inside a literal by doubling it.
10:49:10 <wib_jonas> I'm planning to make string literals work this way in Consumer Society, but this part of the tokenization is basically independent of the rest of the language.
10:50:11 <wib_jonas> The drawback of this syntax that I propose is that you can't really parse source files read backwards.
11:12:34 <esowiki> [[HackEso]] https://esolangs.org/w/index.php?diff=67465&oldid=67460 * Fizzie * (+266) /* Command */ Split the difference: equal time for `` and ```.
11:16:19 <wib_jonas> oh yeah, I put ** instead of ''' for bold. I should just use <i>...</i> and <b>...</b>, those work alike on MediaWiki and SE.
11:18:05 <fizzie> Also, nuls are replaced by a '.' instead of truncating the message. But I'm going to fix the \r bug before updating that bit. (Sometime later, should get to work now.)
11:18:41 <fizzie> `` echo -e 'foo\0bar\x01baz'
11:23:08 <fizzie> Well, that's just weird.
11:23:36 <wib_jonas> `` echo -e 'foo\0bar\x01baz' | od -tx1
11:23:37 <HackEso> 0000000 66 6f 6f 00 62 61 72 01 62 61 7a 0a \ 0000014
11:24:40 <wib_jonas> `` echo -e 'foo\0bar\x01baz' | od -tx1
11:24:41 <HackEso> 0000000 66 6f 6f 00 62 61 72 01 62 61 7a 0a \ 0000014
11:24:43 <fizzie> Oh, right, obviously echo won't work with a raw \0 in the argument.
11:24:45 <wib_jonas> `` echo $'foo\x00bar\x01baz' | od -tx1
11:24:46 <HackEso> 0000000 66 6f 6f 0a \ 0000004
11:25:08 <wib_jonas> `python3 -cprint("foo\x00bar\rqux")
11:25:19 <wib_jonas> `python3 -cprint("foo\x00bar\x02qux")
11:25:27 <fizzie> Well, that makes more sense. I was getting a little confused.
11:25:29 <wib_jonas> `python3 -cprint("foo\x00bar\x07qux")
11:26:01 <fizzie> \0, \1 and \n are (or at least should be right now) the only specially treated characters.
11:26:17 <wib_jonas> why is \x01 treated specially? oh right, CTCP
11:26:32 <wib_jonas> but \r is treated specially by the IRC server, so you should probably treat it specially too
11:26:48 <wib_jonas> `python3 -cprint("foo\rPRIVMSG #esoteric :hello")
11:27:29 <wib_jonas> `python3 -cprint("\rPRIVMSG #esoteric :hello")
11:27:54 <fizzie> Yes, although I think it's only by luck, I'm still not 100% sure why it's not that stupid in general.
11:28:35 <fizzie> Not sure yet whether I'll replace '\r' with '.' too (under the assumption that you'll want to know when you have them), treat any one of "\n", "\r", "\r\n" and possibly "\n\r" as a single newline, or collapse any sequence of '\n' and '\r' to a single " \ " (which would make the output more compact, but you couldn't see empty lines).
11:29:10 <wib_jonas> fizzie: I'm not sure how the server actually interprets \r and \n . maybe it truncates the line between \r and \n like I think some versions of TeX do
11:29:41 <fizzie> `` echo -e 'foo\0bar\x01baz\rzuul'
11:29:51 <fizzie> Hot-patched it into . for now.
11:30:00 <wib_jonas> the irc standard says that the line delimiter is \r\n and you can't have \r or \n elsewhere, and the server keeps this when sending lines to you, but when you send, it's easier to use \n as the line delimiter because all servers accept it.
11:31:16 <fizzie> That one's still broken.
11:32:05 <fizzie> There were some leftovers in the repo of some DCC magic, I think from EgoBot times when you could still do \x01 and had network connectivity.
11:33:13 <fizzie> Wonder how much DCC is used in these days of CGNAT and whatnot.
11:35:08 <fizzie> Linux's nf_conntrack_irc module has code to help DCC through, but I assume that's not very commonplace.
11:51:25 -!- arseniiv has joined.
13:03:11 <esowiki> [[Language list]] https://esolangs.org/w/index.php?diff=67466&oldid=67390 * PythonshellDebugwindow * (+10) /* E */
13:04:14 <esowiki> [[Language list]] https://esolangs.org/w/index.php?diff=67467&oldid=67466 * PythonshellDebugwindow * (+26) /* T */
13:06:03 -!- tromp has quit (Remote host closed the connection).
13:19:43 -!- tromp has joined.
13:40:32 <esowiki> [[The Temporary Stack]] https://esolangs.org/w/index.php?diff=67468&oldid=67457 * PythonshellDebugwindow * (+6) /* Examples */
13:56:53 <wib_jonas> In some of these languages that try to have english-like syntax, it sometimes bothers me when they put terms in inconsistent orders because of that. I know three examples: (1) in python, the `for` stmt has the variable that you assign in front of the expression, but the `with` and `except` stmt has them after the expression.
13:57:30 <wib_jonas> (2) also in python, when you get or delete a key from a dictionary, the dictionary expression comes first and the key expression after, but if you test for existence of a key, then the key expression comes first.
14:00:06 <myname> what do you mean by the variable that you assign in front of the expression? like [x for y in z]?
14:01:19 <myname> i would call y the assigned variable here which in fact is after for and not before
14:01:22 <wib_jonas> myname: I'm talking about statements or statement clauses. `for variable in expression:`, `except expression as variable:`, `with expression as variable:`
14:01:59 <wib_jonas> but in a display too, it's `[... for variable in expression]` just like in a for stmt
14:02:11 <wib_jonas> (3) SQL, and this one is the worst because the delimiter is always ` AS `: in a `SELECT` stmt where you list expressions to extract as result columns, the expression comes first and the name of the new column next, similarly in the `FROM` clause the table expression come first and the name of that table next, BUT
14:04:20 <wib_jonas> in a common table expression introduced by `WITH`, the new table name comes first and the table definition expression after it, and in a `CREATE TABLE` statement for generated columns, the column name comes first and the expression generating it after.
14:05:03 <wib_jonas> At least python uses `in` when the assigned variable comes first and `as` when the assigned variable goes after; in SQL all four of these use the `AS` separator
14:05:51 <wib_jonas> Luckily I'm writing python now, not SQL, so I'm only partly confused.
14:06:05 <myname> i agree to a degree on python. it doesn't bother me because the english-like syntax makes it easy to write it wothout thinking about it. I couldn't come up with a keyword that would make "for expression $keyword variable" work
14:06:41 <wib_jonas> `for` is the one you should keep, because assignment expressions have the newly assigned name on the left too
14:07:01 <wib_jonas> even in Python, you write `variable = expression` to assign to a variable
14:07:05 <myname> what do you propose for with and except then?
14:07:43 <wib_jonas> I guess they could use `with variable in expression` or `with variable = expression` too
14:08:58 <wib_jonas> yes, I know it's not a plain assignment, because the variable can get whatever the __enter__ method returns
14:09:27 <myname> and it would be confusing in except
14:09:30 <wib_jonas> so make it `with variable in expression:` then
14:09:50 <myname> because in that case you would have mathematical equality instead of definition
14:10:19 <myname> i would find "with variable in expression" confusing
14:10:55 <myname> and it would be ambiguous
14:11:00 <wib_jonas> well, it's probably best to leave it alone now
14:11:08 <wib_jonas> right, beacuse there's an `in` operator
14:11:15 <wib_jonas> you're right. not that syntax then
14:13:07 <wib_jonas> perhaps `with variable is expression:` and `except variable is expression:` if it were a new language,
14:13:26 <wib_jonas> but it's probably not worth to modify python syntax for this now that everyone knows the existing syntax
14:14:15 <wib_jonas> yes, `is` is not a keyword right now, it would be a keyword instead of `as` in this hypothetical alternate universe
14:14:52 -!- imode has joined.
14:16:14 <wib_jonas> I don't like Haskell syntax, but Haskell do notation uses `<-` for this, which would be a bad idea in python
14:16:57 <myname> "expect variable is expression" sounds more like assert(variable == expression) to me
14:17:43 <wib_jonas> myname: it's `except`, not `expect`.
14:18:05 <wib_jonas> myname: I'm confusing myself with those too words too, but https://docs.python.org/3/reference/compound_stmts.html#the-try-statement says it's `except`, as in the start of `exception`
14:18:20 <wib_jonas> but `expect` would make sense for that keyword too, beacuse you use it when you expect an exception
14:18:43 <wib_jonas> you use it when the exception is not exceptional, but an expected normal condition from the side where you're viewing the code
14:19:25 <wib_jonas> `throw` and `catch` is less confusing :-)
14:19:44 <wib_jonas> yes, HackEso, I see fizzie modified your "command not found" message
14:20:10 -!- kingoffrance has quit (Read error: Connection reset by peer).
14:20:14 -!- x_ has joined.
14:20:34 <wib_jonas> fizzie: could you change the error message to two IRC lines, "'$command' is not recognized as an internal or external command," then "operable program or batch file." :-)
14:21:44 <wib_jonas> `str 1s++++++++[->++++++++<]>+.+.+.
14:21:48 <wib_jonas> =str 1s++++++++[->++++++++<]>+.+.+.
14:21:57 <bfbot> ok, defined 'msg1'
14:22:03 <bfbot> Error: Name can contain only lowercase letters and digits.
14:24:01 <bfbot> No such command. Try =help.
14:24:13 <esowiki> [[123]] M https://esolangs.org/w/index.php?diff=67469&oldid=32365 * 3snoW * (+1514) /* Examples */
14:25:21 <j-bot> HackEso, pong: 'hello'?
14:25:38 <wib_jonas> yeah, but you can do that without this change too I think
14:25:42 <j-bot> HackEso, pong: 'hello'
14:26:40 <wib_jonas> because HackEso doesn't put a space before the message if it starts with a letter -- I find that weird, a starting letter is how you address people without a shortcut
14:32:21 <fizzie> Yes, the rule that output matching ^[A-Za-z0-9_] doesn't get the space is a little arbitrary, especially with bots that accept "botname: " or "botname, " style commands around.
14:35:55 <wib_jonas> so fungоt and lambdabot seem to ignore HackEso completely, and it looks like I can't trigger bfbot for anything but an "Unknown command" error message because it seems to want a space after the command name
14:36:22 <wib_jonas> so I probably can't use this new error message to make botloops, but that's partly by accident
14:36:26 <HackEso> Bot prefixes: fungot ^, HackEso `, EgoBot !, lambdabot @ or ?, thutubot +, metasepia ~, idris-bot ( , jconn ) , j-bot [ , bfbot =.
14:36:36 <myname> doesn't it just put a zero-width space at the beginning of its output?
14:36:43 <wib_jonas> yeah, EgoBot and metasepia and thutubot aren't here
14:37:12 <wib_jonas> `echo =it puts a zero-width space before the input for cases like this
14:37:13 <HackEso> =it puts a zero-width space before the input for cases like this
14:37:32 <wib_jonas> `=but_not_for_the_new_error_message
14:37:33 <HackEso> =but_not_for_the_new_error_message?
14:39:44 <wib_jonas> HackEso puts something before the error message too
14:41:48 <esowiki> [[User:OsmineYT]] https://esolangs.org/w/index.php?diff=67470&oldid=67436 * OsmineYT * (+30)
14:43:46 <esowiki> [[USERA]] N https://esolangs.org/w/index.php?oldid=67471 * OsmineYT * (+129) Created page with "{{wrongtitle|title=User:A}} USERA, or User-A is simple language maded by [[User:OsmineYT|OsmineYT]] and dedicated to [[User:A]]."
14:44:02 <esowiki> [[USERA]] https://esolangs.org/w/index.php?diff=67472&oldid=67471 * OsmineYT * (+0)
14:45:01 <esowiki> [[USERA]] https://esolangs.org/w/index.php?diff=67473&oldid=67472 * OsmineYT * (+69)
14:45:25 <esowiki> [[USERA]] https://esolangs.org/w/index.php?diff=67474&oldid=67473 * OsmineYT * (+0)
14:56:51 -!- imode has quit (Ping timeout: 265 seconds).
14:57:36 <fizzie> Yes, it should be any output whatsoever.
14:58:45 -!- kspalaiologos has joined.
14:59:46 -!- kspalaiologos has quit (Read error: Connection reset by peer).
15:00:13 -!- Frater_EST has joined.
15:03:11 <esowiki> [[USERA]] https://esolangs.org/w/index.php?diff=67475&oldid=67474 * OsmineYT * (+243)
15:03:42 -!- kspalaiologos has joined.
15:10:52 -!- imode has joined.
15:12:28 <esowiki> [[Talk:USERA]] N https://esolangs.org/w/index.php?oldid=67476 * OsmineYT * (+10) Created page with "Discussion"
15:14:11 <esowiki> [[Talk:Bin-8]] N https://esolangs.org/w/index.php?oldid=67477 * OsmineYT * (+44) Created page with "Only not maded discussion for [[Timed]] yet."
15:16:40 <esowiki> [[Talk:H]] https://esolangs.org/w/index.php?diff=67478&oldid=67464 * OsmineYT * (+155)
15:20:33 <wib_jonas> kspalaiologos: search the internet for "mirc color codes"
15:20:58 <wib_jonas> ``` echo $'thing \x0204,06colored'
15:21:06 <wib_jonas> ``` echo $'thing \x0304,06colored'
15:21:19 <wib_jonas> ^ that, a control-C followed by foregroun and background color
15:21:45 <wib_jonas> some clients deliberately ignore colors, mind you, because they're mostly used by spammers
15:21:51 <HackEso> 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.)
15:22:20 <fizzie> Oh, it wasn't actually the combination of `rainbow and `words.
15:22:39 <myname> i didn't know it was a control-c
15:22:44 <kspalaiologos> `rainbow even more stuff to see how will the program behave when the text is longer than a single rainbow
15:22:45 <HackEso> even more stuff to see how will the program behave when the text is longer than a single rainbow
15:23:04 <fizzie> There's only that many colors available.
15:23:06 <fizzie> `` words 16 | rainwords # then
15:23:08 <HackEso> conaritt bca posite cutocyste occavel tograt scani gräbe dation majococh screta watry furp man oblike chiocken
15:23:14 <kspalaiologos> btw, I wrote a graphics library for brainfuck yesterday
15:23:25 <kspalaiologos> I've sent a video somewhere here yesterday probably
15:23:38 <wib_jonas> and it takes at most two digits, optionally followed by a comma and then at most two digits again, and you may need all the digits and commas depending on the following text, though you can cheat by adding a double control-B as a separator
15:23:56 <fizzie> I think the actual keyboard shortcut is ^k in mIRC, actually? But it's the byte 0x03 it uses to introduce a color code.
15:24:15 <fizzie> ^k for kolor, obviously.
15:24:46 <wib_jonas> `perl -eprintf"\x03%02d%02d ",$_,$_ for 0..99; print "."
15:24:46 <HackEso> 00 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73
15:25:04 <wib_jonas> `perl -eprintf"\x03,%02d%02d ",$_,$_ for 0..99; print "."
15:25:05 <HackEso> ,0000 ,0101 ,0202 ,0303 ,0404 ,0505 ,0606 ,0707 ,0808 ,0909 ,1010 ,1111 ,1212 ,1313 ,1414 ,1515 ,1616 ,1717 ,1818 ,1919 ,2020 ,2121 ,2222 ,2323 ,2424 ,2525 ,2626 ,2727 ,2828 ,2929 ,3030 ,3131 ,3232 ,3333 ,3434 ,3535 ,3636 ,3737 ,3838 ,3939 ,4040 ,4141 ,4242 ,4343 ,4444 ,4545 ,4646 ,4747 ,4848 ,4949 ,5050 ,5151 ,5252 ,5353 ,5454 ,5555 ,5656 ,5757 ,5858 ,5959 ,6060 ,6161 ,6262 ,6
15:25:24 <wib_jonas> `perl -eprintf"\x030,%02d%02d ",$_,$_ for 0..99; print "."
15:25:25 <HackEso> 00 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
15:25:31 <kspalaiologos> i used the video to demonstrate something was bricked with the WSL output
15:25:36 <arseniiv> my client shows all the formatting and colors but I’m lazy to investigate how does one input them in it
15:25:52 <kspalaiologos> the program I made was just printing out "1986" (can you guess what date is it?)
15:26:05 <imode> kspalaiologos: couldn't I just do that with a bf -> text generator?
15:26:34 <kspalaiologos> to make a 3d spinning cube it would take you obscene amount of time and code
15:26:46 <imode> why not dump it directly to the output.
15:27:14 <myname> are there color codes for "default"?
15:27:27 <wib_jonas> myname: I think 0 and 1 are the default
15:27:54 <myname> weird, 00,01text is slightly brighter than my default
15:28:23 <myname> i usually have a grey font color on black ground, 00,01 will print white on black ground here
15:29:12 -!- FraterEST has joined.
15:29:38 <fizzie> 99 is "default" in some clients, 0/1 I think are white and black.
15:29:48 <fizzie> Although it's really up to how your client decides to interpret it.
15:30:31 <fizzie> Colors 0 through 15 are the "old standard" ones, so they're what ^rainbow and friends use. Colors 16 .. 99 are "new standard" ones, with a little less support.
15:30:42 <kspalaiologos> everything looking uniformly is hard to comprehend
15:30:54 <wib_jonas> https://modern.ircdocs.horse/formatting.html lists more format codes than I've ever heard of
15:30:58 <myname> from what i can tell about mirc, i wouldn't be surprised if they never had the idea to make something like a default code because everybody has to use the software like they do
15:31:11 <wib_jonas> apparently someone invented codes for "Monospace" and "Strikethrough"
15:31:34 <wib_jonas> also that page says "99 - Default Foreground/Background - Not universally supported."
15:31:38 <imode> my client doesn't show all of that.
15:31:44 <imode> only 00 through 15.
15:31:56 -!- Frater_EST has quit (Ping timeout: 240 seconds).
15:32:43 <fizzie> irssi does all 99, but (at least in this terminal) only actually uses the standard 16 terminal colors, so e.g. 27, 28 and 29 are all the same dark red.
15:33:17 <fizzie> And of course there's no real orange, so 7 is brown.
15:36:04 <wib_jonas> ``` echo $'normal \x02bold\x02 normal \x1Ditalic\x1D normal \x1Funderlined\x1F normal \x1Estrikethrough\x1E normal \x11monospace\x11 normal \x16reverse\x16 normal'
15:36:07 <HackEso> normal bold normal italic normal underlined normal strikethrough normal monospace normal reverse normal
15:36:29 -!- imode has quit (Ping timeout: 265 seconds).
15:55:55 <fizzie> I can see bold, underlined and reversed here.
15:56:30 <fizzie> And esolangs.org/logs supports bold, italic, underlined and strikethrough.
15:57:09 <fizzie> Well, maybe you an always-monospace client "supports" monospace by default, kind of.
15:59:11 -!- GeekDude has quit (Ping timeout: 276 seconds).
16:02:30 <FireFly> somehow one of those control codes managed to mess up weechat's UI's colour a bit; impressive
16:08:25 <fizzie> Some clients also support [1mregular[0m ANSI codes [33mand colors[0m.
16:13:17 -!- GeekDude has joined.
16:34:43 <fizzie> No, there are graphical clients that specifically do support them, IIRC.
16:35:07 <fizzie> And from what I recall, irssi supports them pretty explicitly as well, parsing them to some internal format and then reconstructing for display.
16:35:22 <fizzie> They definitely don't just leave \e unfiltered.
16:54:19 -!- imode has joined.
17:00:50 -!- imode has quit (Ping timeout: 268 seconds).
17:03:02 -!- Lord_of_Life_ has joined.
17:03:55 -!- Lord_of_Life has quit (Ping timeout: 268 seconds).
17:04:24 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
17:28:44 <esowiki> [[HackEso]] https://esolangs.org/w/index.php?diff=67479&oldid=67465 * Fizzie * (+3104) Document implementation details.
17:44:45 -!- wib_jonas has quit (Quit: Connection closed).
17:54:05 -!- laerlingsap has joined.
18:10:14 -!- FraterEST has quit (Remote host closed the connection).
18:30:37 -!- FreeFull has joined.
18:47:24 -!- laerlingsap has quit (Read error: Connection reset by peer).
18:51:14 -!- laerling_ has joined.
19:08:41 -!- b_jonas has joined.
19:11:25 -!- LKoen has joined.
19:12:17 -!- x_ has changed nick to kingoffrance.
19:32:51 -!- laerling_ has quit (Read error: Connection reset by peer).
20:00:52 <HackEso> olist 1188: shachaf oerjan Sgeo FireFly boily nortti b_jonas
20:39:20 <b_jonas> shachaf: the kicker is in the next strip, which is the last one in the book
20:39:24 <b_jonas> and may take more than one page
20:40:59 <b_jonas> but there's been a kicker at the last strip of all five main OotS books so far
20:41:11 <b_jonas> and the Giant says that the next strip is the last strip of this book
20:43:11 <b_jonas> http://www.giantitp.com/forums/showsinglepost.php?p=24280225
20:44:43 <shachaf> I believe you but I guess I'll click the link anyway.
20:45:01 <shachaf> whoa, 1189 will be posted on Monday.
20:45:29 <b_jonas> it also says "the final strip will be posted Monday", which I thought at first was against the forum rules, but apparently it's not, the rule is worded that "Inappropriate topics. Missed/Late Comics: Threads speculating on when a comic will be posted or why it may be late will be locked; this does not apply to official threads started by site staff providing notification of a late comic."
20:46:07 <int-e> "Monday" is not all that specific anyway ;-)
20:46:37 <b_jonas> yeah. no week or timezone specified.
20:46:43 <shachaf> An official announcement isn't very speculative, anyway.
20:47:10 <int-e> it might be (sorry, weak pun)
20:47:10 <b_jonas> yeah, I thought the rule just said that you aren't allowed to discuss the schedule of online comic strips on that forum
20:48:28 <int-e> rules are made to be broken
20:49:01 <int-e> the trick is not to get punished ;)
20:50:17 <int-e> and ethics dictate that you only break rules when it doesn't hurt other people
20:55:09 -!- kspalaiologos has quit (Quit: Leaving).
21:06:06 <shachaf> Is the "only" thing that SMT does over SAT is additional propagation rules?
21:10:52 <int-e> Isn't propagation optional? I mean, the minimum functionality is just detecting conflicts...
21:11:35 <int-e> ...typically, when you have a conflict you also produce an unsatisfiable core for it because that's a propositional clause that can be learned.
21:14:01 <shachaf> Hmm, I guess thoe aren't the same.
21:14:25 <shachaf> I think of "propagation" as deducing the consequences of the current assignment, in SAT, which might lead to an empty clause. But maybe the SMT situation is more nuanced.
21:15:44 <int-e> Well, in the picture I have, the propagation is unit propagation from DPLL, handling the propositional part of a formula.
21:15:51 <int-e> so SMT doesn't add anything there.
21:16:24 <int-e> (Well, not necessarily. I'm sure that it /could/ add things there.)
21:17:30 <shachaf> The thing I was thinking based on some vague verbal descriptions was that SMT effectively gives you implications between statements in your theory.
21:17:48 <shachaf> So it can tell you that x > 5 implies x > 7, and I guess also falsifies x < 5.
21:18:16 <int-e> But I really know fairly little. Basically I've read the DPLL(T) paper, and learned some basics (linear algebra, equality reasoning, some ideas of theory combination)
21:18:33 <shachaf> Whereas with unit propagation P only truthifies P and falsifies ¬P and nothing else?
21:18:49 <shachaf> I should probably read that paper rather than blabbering on IRC.
21:20:30 <int-e> AFAIUI, if the solver ever asserts x > 5 and !x > 7 at the same time, that will be detected, and you'll get x > 5 /\ !x > 7 as an unsatisfiable core, so you can then learn the negation, which is that x > 5 implies x > 7.
21:21:12 <int-e> But! That paper is just the start of SMT research. I'm sure there's a lot more happening in modern solvers.
21:21:17 <shachaf> Hmm, maybe that's how it works.
21:21:38 <shachaf> Should I read all these papers or make a reasonable CDCL solver first?
21:21:48 <shachaf> Probably there's no actual point in writing a SAT solver.
21:22:05 <shachaf> i,i because qbf solvers are where it's at
21:22:42 <int-e> AFAIK, QBF solvers also have a CDCL core though.
21:26:06 <shachaf> Quantifier boolean formula? I just met 'er!
21:26:14 <shachaf> I guess it's "quantified".
22:04:21 -!- sftp has quit (Excess Flood).
22:04:37 -!- sftp has joined.
23:06:20 -!- b_jonas has quit (Ping timeout: 246 seconds).
23:13:12 -!- b_jonas has joined.
23:25:05 -!- arseniiv has quit (Ping timeout: 276 seconds).
23:40:56 -!- tromp has quit (Remote host closed the connection).
23:53:00 -!- b_jonas has quit (Read error: Connection reset by peer).
23:53:35 -!- b_jonas has joined.