00:13:41 -!- rain1 has quit (Quit: WeeChat 3.0).
00:47:04 <esowiki> [[Talk:Brainlove]] M https://esolangs.org/w/index.php?diff=79685&oldid=24840 * MADH95 * (+206)
00:48:06 <esowiki> [[User:MADH95]] N https://esolangs.org/w/index.php?oldid=79686 * MADH95 * (+72) Created page with "Newish to esolangs. Dabbling in creating my own that might show up here."
00:56:16 -!- arseniiv has quit (Ping timeout: 246 seconds).
01:00:13 <esowiki> [[Conveyer]] M https://esolangs.org/w/index.php?diff=79687&oldid=77873 * PythonshellDebugwindow * (+110) Unpipe; cats; external resources
01:13:09 -!- Arcorann has joined.
01:13:11 <esowiki> [[User:Hakerh400/Proof 001]] M https://esolangs.org/w/index.php?diff=79688&oldid=79498 * Hakerh400 * (+4234) Highlighting
01:26:09 <esowiki> [[Casini]] M https://esolangs.org/w/index.php?diff=79689&oldid=77137 * PythonshellDebugwindow * (+47) /* External resources */ Cats
01:32:04 <esowiki> [[Functasy]] https://esolangs.org/w/index.php?diff=79690&oldid=71243 * Hakerh400 * (+9508) Change color scheme
01:43:36 <esowiki> [[User:Hakerh400/JavaScript: Unlimited recursion and TCO]] https://esolangs.org/w/index.php?diff=79691&oldid=79100 * Hakerh400 * (+31524) Highlighting
01:46:54 <esowiki> [[User:Hakerh400/JavaScript: Unlimited recursion and TCO]] M https://esolangs.org/w/index.php?diff=79692&oldid=79691 * Hakerh400 * (+7) /* Implementation */
02:01:21 -!- MDude has quit (Quit: Going offline, see ya! (www.adiirc.com)).
02:05:41 -!- MDude has joined.
02:35:42 -!- delta23 has joined.
04:03:37 <fizzie> That's almost an HHGttG quote.
04:04:43 <fizzie> "'The things,' said Ford Prefect quietly, 'are also people.' 'The people...' resumed Arthur, 'the... other people...'"
04:22:34 -!- FreeFull has quit.
05:13:47 -!- galactic_ has joined.
05:23:05 <Hooloovo0> anyone have a good greppable h2g2?
05:23:33 <Hooloovo0> currently trying to extract the text from one of them with gs but it doesn't seem to be working well
05:23:37 <Lykaina> 0000,t_put,$H$; 0000,t_put,$i$;
05:27:25 <Lykaina> 0000,t_put,$H$; 0000,t_put,$i$; 0000,stop_; FFFF,_eof_;
05:33:14 -!- delta23 has quit (Quit: Leaving).
06:48:44 -!- imode has joined.
07:06:42 -!- uplime has quit (Disconnected by services).
07:07:29 -!- also_uplime has joined.
07:07:46 -!- also_uplime has quit (Disconnected by services).
07:08:00 -!- also_uplime has joined.
08:13:13 -!- Sgeo has quit (Read error: Connection reset by peer).
09:26:02 -!- sprocklem has quit (Ping timeout: 260 seconds).
09:42:04 -!- rain1 has joined.
10:04:52 -!- ArthurStrong has quit (Ping timeout: 265 seconds).
10:39:04 -!- arseniiv has joined.
10:49:47 <HackEso> A device is a browser session. Please verify your device.
10:50:08 <HackEso> The password of the month is wake these token brings
10:54:58 <HackEso> Bleen is the color of the ocean and the trees.
11:26:11 -!- imode has quit (Quit: WeeChat 2.9).
11:31:28 <int-e> . o O ( Smart... my emacs renders the month in 28/12/2020 in italic... )
11:32:09 <int-e> well, slanted at least
11:32:10 <shachaf> Just another reason to use 2020-12-28
11:32:30 <int-e> shachaf: Yeah I didn't actually type it that way.
11:32:34 <Taneb> It renders that in strikethrough
11:32:47 <int-e> (I faked the date in the example.)
11:36:13 <shachaf> I like these SAT/SMT lecture slides: https://www.pm.inf.ethz.ch/education/courses/program-verification.html
11:37:08 <shachaf> Is saying SAT/SMT like saying C/C++?
11:38:38 <b_jonas> Taneb: how does it render 2020年12月28日 ?
11:40:23 <Taneb> shachaf: maybe it's like saying GNU/Linux
11:40:43 <shachaf> Oh, b_jonas's system is the best, of course.
11:41:05 <b_jonas> it's not my system. my system is
11:41:07 <HackEso> 2020-12-28 11:41:07.365 +0000 UTC December 28 Monday 2020-W53-1
11:41:17 <b_jonas> 2020-12-28 . but shachaf already said that.
11:41:39 <shachaf> Too bad typing that is tricky for me.
11:41:59 <shachaf> I have Chinese input set up, but I didn't remember the Pinyin for those characters (except the middle one).
11:42:02 <b_jonas> well yes, the zero is in an awkward position in the Hungarian layout
11:42:51 <b_jonas> shachaf: try Japanese input instead maybe
11:43:00 <shachaf> I used to have that set up.
11:43:09 <shachaf> But it seems similarly difficult.
11:43:57 <Arcorann> Either way you'd need to know the pronunciation of what you want to type
11:44:18 <Arcorann> Chinese has shape-based input methods but I don't know how to use any of them
11:44:55 <shachaf> Hmm, one of the first SMT slides says: ¬(f(i)=f(j)) ∧ i-j=0
11:45:06 <shachaf> And I'm not even sure how to show that's UNSAT!
11:45:20 <shachaf> Presumably the slides will tell me but it's annoying that I hadn't even thought about it before.
11:45:52 <shachaf> Now I'm wondering what it does.
11:45:57 <b_jonas> what's this SMT? I don't know the context
11:46:37 <shachaf> Oh, I thought you were asking if this was SMT.
11:46:45 <shachaf> SMT is Satisfiability Modulo Theories.
11:46:55 <shachaf> The problem is that this is mixing theories.
11:47:19 <shachaf> Anyway, option 1: It tries to be clever and turn "i-j=0" to "i=j" in some sort of preprocessing, and then it just has one theory.
11:47:45 <shachaf> Option 2: Something with an e-graph to represent the inequality, which somehow the other theory knows about?
11:48:25 <shachaf> I've pretty much only thought about theories in isolation before. I'm not even sure what option 3 is.
11:52:55 <shachaf> OK, the slides say, extend the API of a theory over what I already know, by having it return equalities that it can figure out. Hmm.
12:04:43 <int-e> shachaf: Well you can extract i /= j from that using the theory of uninterpreted functions and then i /= j and i - j = 0 will be a contradiction in the theory of integers/rationals/reals...
12:05:09 <int-e> IIRC this kind of transfer of equalities and disequalities is at the heart of the Nelson-Oppen theory combination method.
12:05:10 <shachaf> Oh, that's a good point, that's simpler than the direction I was thinking.
12:05:57 <shachaf> But it seems like theory combination must be quite tricky.
12:06:21 <shachaf> I guess "Nelson-Oppen theory combination method" is the thing to look up. Or I can just keep reading these slides.
12:11:55 <shachaf> Oh man, this thing is complicated.
12:12:00 <shachaf> Why are SMT solvers so much work?
12:12:16 <int-e> because they're solving a pretty difficult problem
12:12:45 * int-e believes in irreducible complexity
12:13:09 -!- Alexandra has joined.
12:14:19 <int-e> shachaf: and it gets worse because a ton of people cook up barely decidable theories that an SMT solver can support
12:14:51 <shachaf> I just wanted simple things that barely count as theories.
12:15:02 <shachaf> I mean, do you consider CryptoMiniSat's xor clauses a theory?
12:15:39 <int-e> so, linear arithmetic over reals, over rationals, over integers, non-linear arithmetic over reals (and you can try it for integers and rationals even though it's undecidable there), uninterpreted functions, arrays, ....
12:16:00 <int-e> AIUI, xor clauses are directly used for unit propagation, so not, they're not a theory in the SMT picture
12:16:30 <shachaf> They also do Gaussian elimination, I think.
12:16:48 <int-e> so it's a weird mix then
12:16:59 <shachaf> But why does "used for unit propagation" make it "not a theory", rather than "a better theory"?
12:17:31 <shachaf> If you can have your watch lists wake up theories, rather than running them every literal assignment or something, that seems better.
12:17:43 <int-e> because in the SMT picture, theories are used for analyzing conflicts and learning clauses
12:18:11 <int-e> it's really a technical distinction, not a semantic one.
12:18:16 <shachaf> Yes, and xor clauses do find conflicts and learn clauses, don't they?
12:18:52 <int-e> I forgot about the linear arithmetic
12:18:52 <shachaf> In particular (a⊕b⊕c⊕...) represents a whole bunch of or-clauses at once.
12:20:00 <Alexandra> do you mean, cryptographic compute, is isoteric compue?
12:20:17 <int-e> there's also the whole pseudo-boolean constraints mess where there's an open debate on whether they should be treated as a theory, translated to boolean clauses, or handled by a special solver that knows about weights.
12:29:09 <shachaf> I have a better idea of what E-graphs and E-matching are now.
12:29:21 <shachaf> But I'm still not really clear enough on the whole picture.
12:34:23 -!- Alexandra has left.
12:42:31 <int-e> It's a huge mess :P
12:51:46 -!- lambdabot has quit (Quit: brb).
12:51:54 -!- MDude has quit (Quit: Going offline, see ya! (www.adiirc.com)).
12:57:02 -!- lambdabot has joined.
13:34:13 -!- TheLie has joined.
13:51:22 -!- lambdabot has quit (Quit: and again...).
13:53:47 -!- lambdabot has joined.
13:57:03 -!- lambdabot has quit (Quit: oops).
13:59:16 -!- Arcorann has quit (Ping timeout: 240 seconds).
14:01:23 -!- lambdabot has joined.
14:38:52 <esowiki> [[SELECT./99 bottles]] M https://esolangs.org/w/index.php?diff=79693&oldid=46398 * PythonshellDebugwindow * (-3920) Use a pre; cat; back
14:45:40 -!- Sgeo has joined.
14:49:36 -!- TheLie has quit (Remote host closed the connection).
14:52:43 <esowiki> [[NTFJ]] M https://esolangs.org/w/index.php?diff=79694&oldid=69618 * PythonshellDebugwindow * (+12) /* Minification */ CAT
14:59:22 <esowiki> [[!@$%^&*()+]] M https://esolangs.org/w/index.php?diff=79695&oldid=78631 * PythonshellDebugwindow * (-22) /* LOLOL */ Use span clss=spoiler
14:59:27 <Sgeo> Is learncpp.com good? It does seem to go into more advanced things
14:59:47 <Sgeo> Alternatively I should force myself to figure out detours in Rust so I don't contribute to the existence of C++ code
15:00:33 <HackEso> Sgeolang used to change frequently, but eventually it rusted in place.
15:01:08 <shachaf> Both of them seem too complicated and encourage complicated code.
15:01:16 <shachaf> Rust is surely better, on the former axis.
15:02:04 <shachaf> Oh, actually, you should learn Pascal and tell me what's good about it.
15:02:39 <Sgeo> >.> I may have started doing my current project in C++ because I couldn't figure out why the sample code I was looking at wanted me to cast to (PVOID&) and I didn't figure out the C equivalent until later
15:03:59 <shachaf> That guide doesn't seem like the sort of thing I'd recommend.
15:04:28 <Sgeo> The C API for OpenXR is a bit annoying and there's an... adequate if poorly documented C++ wrapper around it. Takes care of loading in extension functions and needing to call some functions twice
15:05:46 <int-e> The beauty of C++ is that it's easy to find a likeable subset because there's so much of it in the first place.
15:06:08 <shachaf> Well, I don't know what you're doing, but presumably the API boundary isn't going to be that huge so this doesn't seem like a huge consideration.
15:06:21 <shachaf> int-e: Too bad C99 isn't one of the available subsets.
15:07:18 <int-e> I mostly reach for C++ because I like having the various namespaces.
15:07:39 <int-e> in particular the namespace associated with structs
15:08:38 <fizzie> When you say "the namespace associated with structs", I think of the (C) struct/union/enum tag namespace, which you *lose* when going to C++.
15:08:50 <shachaf> Do you mean member functions?
15:09:10 <shachaf> I guess maybe you mean struct A { struct B { } }; and so on.
15:09:36 <shachaf> Or just static member functions.
15:09:42 <int-e> Yes, member functions.
15:10:46 <Sgeo> I don't particularly want to do this repeatedly https://github.com/KhronosGroup/OpenXR-SDK-Source/blob/eedc7df3d99ca7a468d63a574629a9935716ae0b/src/tests/hello_xr/graphicsplugin_opengl.cpp#L91
15:11:01 <Sgeo> Oh hey it's C++ but without that C++ wrapper
15:11:34 <shachaf> Certainly not. I don't know what OpenXR does exactly, anyway.
15:12:15 <int-e> Sgeo: it's a khronic disease
15:12:30 <shachaf> If you just mean GetInstanceProcAddr, that looks like the sort of thing OpenGL and a bunch of things make you do.
15:13:02 <Sgeo> Yeah, that's what I meant
15:13:48 <shachaf> Well, too bad, I guess, this is what they make you do anyway.
15:16:51 <Sgeo> The C++ wrapper defines a dispatcher thing that is provided as a last argument
15:19:05 <shachaf> Well, you can do https://github.com/maluoi/StereoKit/blob/master/StereoKitC/systems/platform/openxr_extensions.h or something.
15:56:03 -!- Alexandra has joined.
15:56:10 -!- Alexandra has left.
16:44:49 <esowiki> [[Special:Log/newusers]] create * NicksterSand * New user account
16:50:53 <esowiki> [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=79696&oldid=79612 * NicksterSand * (+206) /* Introductions */
18:38:21 -!- xelxebar has quit (Remote host closed the connection).
18:39:30 -!- xelxebar has joined.
18:40:01 -!- S_Gautam has joined.
18:46:14 -!- Lord_of_Life_ has joined.
18:48:38 -!- Lord_of_Life has quit (Ping timeout: 264 seconds).
18:48:38 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
18:55:37 <rain1> any cool stuff i should check out?
19:07:13 -!- Lord_of_Life has quit (Ping timeout: 246 seconds).
19:08:25 -!- Lord_of_Life has joined.
19:19:31 <zzo38> What cool stuff do you intend to find anyways?
19:27:56 -!- Alexandra has joined.
19:28:04 -!- Alexandra has left.
19:44:21 <int-e> fungot: anything to see?
19:44:22 <fungot> int-e: imported/ loaded/ whatever.) seriously, though :). my mother thinks i should run it in a fancy closet
19:58:28 <nakilon> fungot tell us more about your mother
19:58:28 <fungot> nakilon: is it me, or do you
19:59:04 <nakilon> fungot till toda we knew only about your father
19:59:04 <fungot> nakilon: what's the lisppaste i should use? ( pen and ink or digital are the main differences that cannot be guessed.) second, sure, deformative-ii. ( ignore set! for assignments, though it's debatable how worthy they are of course, supports the egobot command set.
20:22:06 -!- adu has joined.
21:16:22 <zzo38> This is the (partial) message trace output from Free Hero Mesh showing a problem: http://sprunge.us/QsMqqi
21:19:24 -!- S_Gautam has quit (Quit: Connection closed for inactivity).
21:21:57 <zzo38> I am not sure why sending the MOVED message to the Missile at (8,16) is supposed to be deferred in Hero Mesh; it would seem to have moved (this is what "1 : MOVING : 0 : 16 494 [$Missile 7 16] : 16 494 [$Missile 7 16] : 0 8 : 0 16 : 0 0" is, it is the message sent just before the object moves), and its location seems to be the right place where it should be moved to
21:26:31 <esowiki> [[C Flat]] N https://esolangs.org/w/index.php?oldid=79697 * NicksterSand * (+3633) Created page with "'''C Flat''' (or C) is an [[esoteric programming language]] that uses music as syntax. == Language overview == A C Flat program is a series of chords and rests. These are g..."
21:26:54 <esowiki> [[Language list]] https://esolangs.org/w/index.php?diff=79698&oldid=79661 * NicksterSand * (+13) /* C */ Added C Flat
22:34:17 -!- delta23 has joined.
23:15:42 -!- Arcorann has joined.
23:21:56 -!- rain1 has quit (Quit: WeeChat 3.0).
23:43:10 -!- adu has quit (Quit: adu).
23:49:15 -!- TheLie has joined.
23:56:40 -!- deltaepsilon23 has joined.
23:59:07 -!- delta23 has quit (Ping timeout: 246 seconds).
23:59:18 -!- deltaepsilon23 has changed nick to delta23.