←2019-06-03 2019-06-04 2019-06-05→ ↑2019 ↑all
00:06:57 -!- Sgeo_ has joined.
00:10:53 -!- Sgeo__ has quit (Ping timeout: 245 seconds).
00:11:50 -!- tromp has joined.
00:13:25 -!- tromp_ has joined.
00:15:16 <int-e> hmm, fancy: https://clang.llvm.org/docs/BlockLanguageSpec.html#block-literal-expressions
00:15:42 <int-e> (every sufficiently advanced programming language invents a closure type?)
00:16:10 <kmc> mm
00:16:17 <int-e> (I encountered this because it made its way into OpenCL)
00:16:31 -!- tromp has quit (Ping timeout: 258 seconds).
00:16:31 <shachaf> int-e: Oh, they took Objective C's block syntax. I think I've seen this before.
00:16:32 <kmc> blocks have a complictaed abi https://clang.llvm.org/docs/Block-ABI-Apple.html
00:16:43 <kmc> and are mainly meant to work with the objc / apple runtime
00:16:47 <int-e> "OpenCL C 2.0 adds support for the clang block syntax."
00:17:03 <kmc> C++ lambdas are a lot more elegant
00:17:06 <shachaf> kmc: did you know you can typedef function types in c, not just function pointer types?
00:17:11 <kmc> since they are ~zero cost~
00:17:14 <kmc> shachaf: I think so
00:17:25 <shachaf> it seems nicer
00:17:28 <int-e> . o O ( You do *not* use "C++" and "elegant" in a sentence. )
00:17:31 <shachaf> but i always saw people do it the other way
00:17:39 -!- tromp_ has quit (Ping timeout: 252 seconds).
00:17:47 <shachaf> I think lambdas are among the most reasonable of C++ features in the past decade.
00:18:11 * int-e tries to remember where he heard this "You do not use ... in a sentence." for the first time...
00:18:37 <shachaf> Though they could have been more reasonable if the language had been designed with them in mind from the beginning.
00:19:45 <kmc> the same is true of most C++11 features
00:19:48 -!- budonyc has joined.
00:19:58 <shachaf> well, a lot of them are just unreasonable
00:20:10 <shachaf> man
00:20:17 <shachaf> c++ templates are such a joke
00:20:35 <shachaf> how do they keep making them more complicated
00:20:47 <shachaf> it's the most ridiculous local maximum
00:21:44 <shachaf> c++ templates can't even be parsed
00:23:59 <int-e> kmc: I would hope that most of that ABI is avoided by inlining.
00:35:27 -!- Sgeo__ has joined.
00:38:15 -!- adu has joined.
00:39:06 -!- Sgeo_ has quit (Ping timeout: 272 seconds).
01:28:38 -!- FreeFull has quit.
01:31:59 -!- Sgeo__ has quit (Read error: Connection reset by peer).
01:32:25 -!- Sgeo__ has joined.
01:57:10 <Sgeo__> zzo38, what do you think about the London Mulligan, if you have an opinion about it?
02:09:30 -!- budonyc has quit (Quit: Leaving).
03:01:57 -!- kallisti has joined.
03:03:05 -!- kallisti has quit (Remote host closed the connection).
03:13:34 -!- Sgeo__ has quit (Read error: Connection reset by peer).
03:13:56 -!- Sgeo__ has joined.
03:25:27 -!- tromp has joined.
03:30:06 -!- tromp has quit (Ping timeout: 258 seconds).
03:55:06 -!- contrapumpkin has quit (Quit: My MacBook Pro has gone to sleep. ZZZzzz…).
04:07:28 -!- S_Gautam has joined.
04:50:00 -!- tromp has joined.
04:52:25 -!- sebbu3 has joined.
04:54:29 -!- tromp has quit (Ping timeout: 252 seconds).
04:56:00 -!- sebbu has quit (Ping timeout: 244 seconds).
05:30:07 -!- Sgeo__ has quit (Read error: Connection reset by peer).
05:32:46 -!- Sgeo has joined.
05:52:20 -!- AnotherTest has joined.
05:56:49 -!- AnotherTest has quit (Ping timeout: 252 seconds).
06:38:18 -!- tromp has joined.
06:42:39 -!- tromp has quit (Ping timeout: 252 seconds).
06:44:32 -!- adu has quit (Quit: adu).
06:47:41 -!- tromp has joined.
07:22:05 <esowiki> [[Talk:EnScript]] N https://esolangs.org/w/index.php?oldid=63049 * JonoCode9374 * (+692) Just want some clarification about the ENC command
07:22:39 <esowiki> [[Talk:EnScript]] M https://esolangs.org/w/index.php?diff=63050&oldid=63049 * JonoCode9374 * (+93) Added tag
07:33:06 <esowiki> [[Talk:EnScript]] https://esolangs.org/w/index.php?diff=63051&oldid=63050 * JonoCode9374 * (+238) /* The ENC Command */
07:42:45 <esowiki> [[Talk:EnScript]] https://esolangs.org/w/index.php?diff=63052&oldid=63051 * JonoCode9374 * (+369) /* The CHS Command */ new section
07:50:17 -!- b_jonas has joined.
07:52:05 <esowiki> [[Deadfish "self-interpreter"]] https://esolangs.org/w/index.php?diff=63053&oldid=63013 * JonoCode9374 * (+849) Added python interpreter for this esolang
07:57:00 <b_jonas> `? quotefmt
07:57:01 <HackEso> quotefmt? ¯\(°​_o)/¯
07:57:05 <b_jonas> `? quoteformat
07:57:06 <HackEso> quoteformat is: <nick> message; * nick action; two spaces between messages; all elisions marked with [...] other than irrelevant intervening messages; for messages separated by elision, one space on each side, not two.
07:57:14 <b_jonas> `quote fizzie after
07:57:14 <HackEso> 13) <fizzie after embedding some of his department research into fungot> Finally I have found some actually useful purpose for it.
07:57:31 <b_jonas> are old quotes excloded from quoteformat? or should we amend them?
08:26:45 -!- b_jonas has quit (Quit: leaving).
08:34:49 <int-e> hmm, doesn't CL_DEVICE_MAX_COMPUTE_UNITS = 10 (0xa) indicate that I should be able to subdivide the device using clCreateSubDevices ...
08:36:27 <shachaf> int-e: are you making an md5 collision
08:36:27 <shachaf> twh
08:36:50 <int-e> Ah, no.
08:37:04 <int-e> There's also this: CL_DEVICE_PARTITION_MAX_SUB_DEVICES = 1
08:37:55 <int-e> shachaf: I intend to make a partial one. 80 bits, maybe 96.
08:38:55 <shachaf> Maybe I should use OpenCL.
08:38:57 <int-e> The point is really to do *something* with OpenCL.
08:39:13 <shachaf> Or maybe OpenGL compute shaders, since I was doing some other OpenGL things?
08:40:03 <int-e> (I have a single GTX 1060. It's good for about 5GH/s, for this rainbow-like application.)
08:40:21 <shachaf> 5GHHz
08:40:45 <shachaf> I guess the right way to do this is the parallel rho algorithm?
08:41:00 <int-e> (So in addition to computing MD5, it's also taking the previous hash and constructing a message from that.)
08:41:11 <int-e> Yes.
08:42:23 <shachaf> So you need to encode the hash in a GHC identifier, I guess.
08:42:28 <shachaf> Assuming that's what you're going for.
08:43:40 <int-e> Yeah. I'm targeting the unicode range 0x20000 -- 0x27FFF, since those are all valid in ids.
08:44:25 <shachaf> > map chr [0x20000, 0x27fff]
08:44:28 <lambdabot> "\131072\163839"
08:44:32 <shachaf> > text $ map chr [0x20000, 0x27fff]
08:44:34 <lambdabot> 𠀀𧿿
08:44:44 <int-e> `unidecode 𠀀𧿿
08:44:45 <HackEso> ​[U+20000 CJK UNIFIED IDEOGRAPH-20000] [U+27FFF CJK UNIFIED IDEOGRAPH-27FFF]
08:44:48 <shachaf> Right
08:45:21 <int-e> (it's a consecutive range and covers 30% of all the valid characters for identifiers)
08:45:36 <int-e> > let 𠀀𧿿 = 42 in 𠀀𧿿
08:45:39 <lambdabot> 42
08:45:40 <shachaf> > map (generalCategory . chr) [0x20000, 0x27fff, 0x28000]
08:45:42 <lambdabot> [OtherLetter,OtherLetter,OtherLetter]
08:46:25 <int-e> it's actually complicated: http://paste.debian.net/1085969/
08:46:33 <shachaf> > unwords $ [printf "%x" x | x <- 0x28000, generalCategory (chr x) /= OtherLetter]
08:46:35 <lambdabot> error:
08:46:35 <lambdabot> • No instance for (Num [Int]) arising from the literal ‘0x28000’
08:46:35 <lambdabot> • In the expression: 0x28000
08:46:40 <shachaf> > unwords $ [printf "%x" x | x <- [0x28000..], generalCategory (chr x) /= OtherLetter]
08:46:42 <lambdabot> "2a6d7 2a6d8 2a6d9 2a6da 2a6db 2a6dc 2a6dd 2a6de 2a6df 2a6e0 2a6e1 2a6e2 2a6...
08:47:19 <shachaf> > map (generalCategory . chr) [0x2a6d7]
08:47:21 <lambdabot> [NotAssigned]
08:51:14 <shachaf> > map length . sortBy (compare `on` negate . length) . filter (\x -> generalCategory (head x) `elem` [UppercaseLetter, LowercaseLetter, TitlecaseLetter, ModifierLetter, OtherLetter, NonSpacingMark, DecimalNumber, OtherNumber]) . groupBy ((==) `on` generalCategory) $ ['\0'..]
08:51:17 <lambdabot> [42711,20941,11172,6582,4149,1143,1071,921,620,569,542,366,363,332,311,268,2...
08:51:45 <shachaf> > map (\(x:_) -> printf "%x" x :: String) . sortBy (compare `on` negate . length) . filter (\x -> generalCategory (head x) `elem` [UppercaseLetter, LowercaseLetter, TitlecaseLetter, ModifierLetter, OtherLetter, NonSpacingMark, DecimalNumber, OtherNumber]) . groupBy ((==) `on` generalCategory) $ ['\0'..]
08:51:48 <lambdabot> ["20000","4e00","ac00","3400","2a700","a016","13000","12000","1401","16800",...
08:52:09 <shachaf> netcraft confirms it
08:52:41 <int-e> > length $ filter (\x -> generalCategory (head x) `elem` [UppercaseLetter, LowercaseLetter, TitlecaseLetter, ModifierLetter, OtherLetter, NonSpacingMark, DecimalNumber, OtherNumber]) . groupBy ((==) `on` generalCategory) $ ['\0'..]
08:52:43 <lambdabot> 2087
08:52:48 <shachaf> Well, what I did isn't quite correct, for two reasons. But still.
08:53:14 <int-e> > length $ filter (\x -> generalCategory x `elem` [UppercaseLetter, LowercaseLetter, TitlecaseLetter, ModifierLetter, OtherLetter, NonSpacingMark, DecimalNumber, OtherNumber]) $ ['\0'..]
08:53:17 <lambdabot> 105253
08:53:34 <int-e> > 32768 / (105253+2)
08:53:36 <lambdabot> 0.3113201273098665
08:53:43 <int-e> that's the 30% figure
08:53:45 <shachaf> @let reasonableCodepoint x = x `elem` [UppercaseLetter, LowercaseLetter, TitlecaseLetter, ModifierLetter, OtherLetter, NonSpacingMark, DecimalNumber, OtherNumber]
08:53:47 <lambdabot> Defined.
08:54:13 <int-e> "for two reasons" was nice.
08:54:31 <shachaf> Hmm?
08:54:37 <shachaf> It might be more than two reasons, but I thought of two.
08:54:48 <int-e> I thought you meant ' and _.
08:55:14 <shachaf> Oh, no. Three reasons.
08:55:37 <shachaf> I meant that if you have OtherLetter next to UppercaseLetter or something they should count as one contiguous valid block.
08:55:54 <int-e> Oh.
08:56:01 <shachaf> And that surrogate code units and so on don't show up in ['\0'..] so it's not really contiguous.
08:56:16 <int-e> yeah the whole grouping-by-category-first is a bit weird to my mind.
08:56:19 <shachaf> Or do they?
08:56:25 <shachaf> I guess they do.
08:56:32 <shachaf> > '\xd800' `elem` ['\0'..]
08:56:35 <lambdabot> True
08:57:31 <shachaf> @undef
08:57:31 <lambdabot> Undefined.
08:57:53 <shachaf> @let reasonableCodepoint x = generalCategory x `elem` [UppercaseLetter, LowercaseLetter, TitlecaseLetter, ModifierLetter, OtherLetter, NonSpacingMark, DecimalNumber, OtherNumber]
08:57:54 <lambdabot> Defined.
08:58:07 <int-e> > (length ['\0'..], fromEnum (last ['\0'..]))
08:58:08 <shachaf> > map (\(x:_) -> printf "%x" x :: String) . sortBy (compare `on` negate . length) . filter (\(x:_) -> reasonableCodepoint x) . groupBy ((==) `on` reasonableCodepoint) $ ['\0'..]
08:58:09 <lambdabot> (1114112,1114111)
08:58:13 <lambdabot> ["20000","4e00","ac00","3400","2a700","a000","13000","12000","1401","16800",...
08:58:17 <int-e> no gaps ^^
08:58:25 <shachaf> > map length . sortBy (compare `on` negate . length) . filter (\(x:_) -> reasonableCodepoint x) . groupBy ((==) `on` reasonableCodepoint) $ ['\0'..]
08:58:30 <lambdabot> [42711,20941,11172,6582,4149,1165,1071,921,620,569,542,458,366,363,340,333,3...
08:58:45 <int-e> oh I see what you're really doing there.
08:58:46 <shachaf> I must've been thinking of Data.Text.
08:59:35 <int-e> > reverse . sort . map length . group . zipWith (-) [0..] . map fromEnum . filter reasonableCodepoint $ ['\0'..]
08:59:41 <lambdabot> [42711,20941,11172,6582,4149,1165,1071,921,620,569,542,458,366,363,340,333,3...
09:01:47 <shachaf> zipWith (-) [0..] is a bit odd
09:02:14 <shachaf> @undef
09:02:15 <lambdabot> Undefined.
09:02:32 <shachaf> @let reasonableCodepoint x = generalCategory x `elem` [UppercaseLetter, LowercaseLetter, TitlecaseLetter, ModifierLetter, OtherLetter, NonSpacingMark, DecimalNumber, OtherNumber] || x == '\'' || x == '_'
09:02:33 <lambdabot> Defined.
09:02:45 <int-e> zipWith (-) [0..] maps each consecutive range to a constant.
09:03:07 <shachaf> Right.
09:03:07 <esowiki> [[Deadfish "self-interpreter"]] https://esolangs.org/w/index.php?diff=63054&oldid=63053 * JonoCode9374 * (-4) Looks like I forgot how to use html
09:03:09 <int-e> (but makes it hard to reconstruct the original values... so the proper way would be to construct a pair instead)
09:03:37 <int-e> :t groupBy
09:03:38 <lambdabot> (a -> a -> Bool) -> [a] -> [[a]]
09:04:27 <int-e> That zipWith may be a bit too clever for its own good.
09:05:00 <shachaf> If you just want the numbers you can do something simpler.
09:05:12 -!- lifthrasiir has quit (Quit: No Ping reply in 180 seconds.).
09:05:53 <shachaf> > reverse . sort . map length . filter (id . head) . group . map reasonableCodepoint $ ['\0'..]
09:05:58 <lambdabot> [42711,20941,11172,6582,4149,1165,1071,921,620,569,542,458,366,363,340,333,3...
09:06:21 <shachaf> good luck reconstructing the original values now hth
09:06:41 -!- lifthrasiir has joined.
09:06:50 <shachaf> lifthrasiir: hifthrasiir
09:07:13 <int-e> well, same thing... keep the old values around
09:07:20 <int-e> "id ." is... fun.
09:07:43 <int-e> (did you have a "fst" there?)
09:07:44 <shachaf> gotta make sure you get the identity of the value
09:07:49 <shachaf> I had "filter id"
09:07:57 <int-e> @let papers = id
09:07:59 <lambdabot> Defined.
09:07:59 <shachaf> And then I remembered it was a list.
09:09:12 <shachaf> anyway you gotta do it on the gpu. lambdabot is too slow.
09:28:13 -!- AnotherTest has joined.
09:40:39 -!- wob_jonas has joined.
09:43:24 <wob_jonas> shachaf: I think it's technically even more complicated, because the middle dot is also valid inside identifier, plus there's a small set of extra identifier characters that are that only for legacy compatibility reasons (I don't know if Haskell follows that, but that's the unicode recommendation)
10:02:52 <lifthrasiir> shachaf: ah, hi
10:02:59 <lifthrasiir> (was afk for an hour)
10:17:57 -!- nfd has joined.
10:18:48 -!- nfd9001 has quit (Ping timeout: 252 seconds).
10:21:57 <shachaf> wob_jonas: I was following what GHC does, which int-e posted earlier.
10:22:14 <shachaf> Unicode is in no position to dictate to languages what is or isn't an identifier.
10:22:20 <wob_jonas> sure
10:22:53 <wob_jonas> it jsut gives them a reasonable default about which characters are identifier start chars and which ones are identifier continue chars, and libraries provide an implementation with that,
10:22:56 -!- Lord_of_Life has quit (Ping timeout: 248 seconds).
10:23:27 <wob_jonas> and since that sort of thing is easy to mess up, and you need it on your computer anyway for stuff like parsing xml, it's often best to use it
10:24:04 <shachaf> I would be much happier if my computer never parsed any XML.
10:24:04 <wob_jonas> of course some languages modify the rules, like allowing hyphens, allowing apostrophes, reserving some keywords or reserving some forms of identifiers for library macros, etc
10:24:40 -!- Lord_of_Life has joined.
10:24:41 <wob_jonas> shachaf: I don't like XML, but there are lots of existing data available as an XML that I want to parse because I want the contained data
10:25:08 <wob_jonas> and yes, some languages count uppercase and lowercase identifiers differently
10:25:11 <wob_jonas> including haskell and prolog
10:27:40 <int-e> what is OpenCL's excuse for not having something like http://paste.debian.net/1085993/ ;-) (or did I miss it...)
10:29:00 <shachaf> int-e: what is c's excuse for not having that
10:29:09 <wob_jonas> There's a certain kind of esolang of which I'd like to know if it exists, and if not, whether it's possible to make it. I'll probably think more about whether it's possible, but let me ask about it because someone else might already know about it.
10:29:34 <int-e> shachaf: Well, Posix has strerror at least.
10:29:44 <wob_jonas> The esolang I'd want is a sort of djinn esolang, a functional language where you never write function bodies, but only the types of functions you define, plus data type definitions.
10:29:51 <shachaf> By the way, I have a C macro I couldn't figure out how to make fake-varargs
10:30:19 <wob_jonas> The compiler then derives the body of each function, where what the body can contain is seriously constrained by langauge rules.
10:30:29 <shachaf> #define ShowEnumVal3(val, e1, e2, e3) ((val) == (e1) ? #e1 : (val) == (e2) ? #e2 : (val) == (e3) ? #e3 : "UNKNOWN")
10:30:36 <shachaf> I have one of those for every k up to 8.
10:30:50 <int-e> (I mean, ideally each of these errors should come with a human readable description...)
10:30:58 <shachaf> But the usual cpp foreach trickery doesn't work here.
10:31:02 <wob_jonas> Only I want it to be elegant too, which includes that adding new declarations can make the program invalid because of ambiguity, but mustn't make the program valid but with a different meaning;
10:31:17 <wob_jonas> and obviously I also want the language to be powerful enough to express any program.
10:31:29 <wob_jonas> Does an esolang like this already exist?
10:32:53 <shachaf> This is used as e.g. «char *name = ShowEnumVal3(e.xmapping.request, MappingModifier, MappingKeyboard, MappingPointer);»
10:33:17 <shachaf> I think what I need is a real macro system instead of string substitution.
10:34:03 <int-e> shachaf: also, annoyingly, those values are not defined in an enum, so your macro wouldn't even help
10:34:23 <shachaf> My macro doesn't rely on enums.
10:34:34 <int-e> hmm
10:34:35 <shachaf> (In fact most uses of it are for #defines.)
10:34:49 <shachaf> (Which is why the usual trick doesn't work.)
10:35:55 <int-e> Oh, so it does work... Hmm. Where did I go wrong earlier...
10:36:14 <shachaf> Can you believe that in the year 2019 people still write #define str(x) str2(x) and #define str2(x) #x ?
10:36:45 <int-e> Yes.
10:37:21 <shachaf> anyway cpp is the best
10:37:27 <shachaf> I posted my fmt macro in here, right?
10:37:45 <shachaf> Yes.
10:37:48 <int-e> How bad of an idiom is sizeof(err)/sizeof(*err) ?
10:37:51 <wob_jonas> shachaf: no of course not. we don't define such things, we include hundred megabyte large libraries to get such a macro with a long prefixed name instead.
10:37:55 <int-e> yes you did
10:38:13 <wob_jonas> because don't reinvent the wheel
10:38:33 <shachaf> I have a numof() macro that checks that the type of the argument is array rather than pointer.
10:38:39 <int-e> that wheel thing
10:38:45 <int-e> wheels have been reinvented numerous times
10:38:50 <int-e> and that's a good thing
10:38:59 <shachaf> The check only works with gcc/clang but the macro can fall back to the standard behavior.
10:39:16 <wob_jonas> shachaf: #define str BOOST_PP_STRINGIZE
10:40:01 <shachaf> tdnh
10:41:08 <wob_jonas> there's probably one smewhere in the P99 library too
10:42:50 <wob_jonas> or the G_STRINGIFY macro from glib
10:43:08 <wob_jonas> see, there's no need to define yet another one
10:43:27 -!- xvnvx has quit (Quit: ZNC 1.7.1 - https://znc.in).
10:43:33 <shachaf> The point is not the overhead of defining it.
10:44:36 -!- xvnvx has joined.
10:44:41 <wob_jonas> incidentally, do I understand it correctly that the "g" in the name of "glib" comes from "gtk" and that comes from "gimp" and that comes from "gnu"?
10:45:01 <wob_jonas> I think "gtk" originally stood for "gimp toolkit"
10:45:16 <wob_jonas> and "gimp" stands for "GNU image manipulation program"
10:45:25 <wob_jonas> but I don't really know where the "glib" name comes from
10:46:47 <shachaf> glib stands for glib library
10:46:51 <shachaf> and gtk stands for gtk toolkit
10:46:55 <shachaf> and so on
10:47:01 <shachaf> g never stands for anything
10:47:51 -!- xvnvx has quit (Excess Flood).
10:48:41 -!- Cale has quit (Ping timeout: 250 seconds).
10:49:18 -!- arseniiv has joined.
10:50:08 <esowiki> [[Talk:EnScript]] M https://esolangs.org/w/index.php?diff=63055&oldid=63052 * A * (+994) Specify
10:50:28 <esowiki> [[Talk:EnScript]] M https://esolangs.org/w/index.php?diff=63056&oldid=63055 * A * (+4) /* The ENC Command */ : Cosmetics
10:50:32 -!- xvnvx has joined.
10:55:55 <esowiki> [[Talk:EnScript]] M https://esolangs.org/w/index.php?diff=63057&oldid=63056 * A * (+479) /* The ENC Command */
10:58:20 <esowiki> [[Talk:EnScript]] M https://esolangs.org/w/index.php?diff=63058&oldid=63057 * A * (+263) /* The ENC Command */
10:59:29 <esowiki> [[Talk:EnScript]] M https://esolangs.org/w/index.php?diff=63059&oldid=63058 * A * (+62) /* The ENC Command */
10:59:58 <esowiki> [[Talk:EnScript]] M https://esolangs.org/w/index.php?diff=63060&oldid=63059 * A * (-1) /* The ENC Command */ Bad English
11:00:51 <Taneb> GPS stands for GPS positioning system
11:01:28 <shachaf> Taneb invented it.
11:01:44 -!- Cale has joined.
11:01:48 <shachaf> `` cd wisdom; echo g*
11:01:49 <HackEso> galaxy gamemanj gaspacho gaspasjo gaspatsjo gaszpacho gazpacho gazspaczo gblh gene ray gentlebeing gey ghci ghoti ghoul ginorst glados glass glogbot glumgot gnimmargorp go goat god's number golf gonad goofix google gopher gostak grace period graham's number grammar gray greater gregor grimmargorp ground water group grue guarantee guillible
11:02:21 <shachaf> y'all went overboard with the gajpako
11:02:23 <esowiki> [[Talk:EnScript]] M https://esolangs.org/w/index.php?diff=63061&oldid=63060 * A * (+334) /* The CHS Command */
11:02:25 <wob_jonas> `? gray
11:02:26 <HackEso> Gray is e common misspalling of grey.
11:02:28 <wob_jonas> `? grey
11:02:29 <HackEso> grey? ¯\(°​_o)/¯
11:02:47 -!- xvnvx has quit (Quit: ZNC 1.7.1 - https://znc.in).
11:02:50 <shachaf> `? guillible
11:02:51 <HackEso> A guillible person is someone who can be fooled with a Scheme script.
11:02:56 <esowiki> [[Talk:EnScript]] M https://esolangs.org/w/index.php?diff=63062&oldid=63061 * A * (+73) /* The CHS Command */ Add
11:02:56 -!- xvnvx has joined.
11:03:13 <shachaf> `? god's number
11:03:14 <HackEso> God's number is the maximum number of moves a Rubik's cube can require to solve. It is equal to 20. No, really. Look it up.
11:03:40 <shachaf> `dowg god's number
11:03:42 <HackEso> 8411:2016-06-08 <hppavilion[1̈]> le/rn God\'s Number/God\'s number is the maximum number of moves a Rubik\'s cube can require to solve. It is equal to 20. No, really. Look it up.
11:03:52 <wob_jonas> `? greater
11:03:53 <HackEso> A greater than sign instructs the shell to send the output of the command to a file. Not very mnemonic, but a grater is the closest thing to a file that ASCII has.
11:04:06 <wob_jonas> oh right, that one's mine too
11:04:13 <wob_jonas> gene ray is mine obviously
11:04:16 <wob_jonas> `? go
11:04:17 <HackEso> Go is a common irregular verbal game programming language invented by the Germanic Taneb tribes catching monsters in the strategic territories of East Asia.
11:04:28 <shachaf> the pen is greater than the sword
11:04:41 <wob_jonas> `? gey
11:04:42 <HackEso> I know nothing about Gey, sir.
11:04:57 <shachaf> Taneb: Do you like digital signal processing?
11:05:05 <Taneb> Not hugely, I'm afraid
11:05:14 <Taneb> Although I haven't done it much
11:05:27 <shachaf> I agree with you, analog signal processing is better.
11:05:37 <shachaf> Do you like garbage collectors?
11:05:50 <shachaf> gc stands for gc collector presumably
11:06:17 <Taneb> No, they didn't collect my landfill garbage properly the other week, they left half of it in the wheelie bin
11:07:00 <esowiki> [[Talk:EnScript]] M https://esolangs.org/w/index.php?diff=63063&oldid=63062 * A * (+144) /* The ENC Command */ Add
11:07:05 <shachaf> you do wheelies with bins?
11:07:25 <shachaf> most people use bicycles or motorcycles
11:10:06 <esowiki> [[Talk:EnScript]] M https://esolangs.org/w/index.php?diff=63064&oldid=63063 * A * (-5)
11:14:17 <wob_jonas> shachaf: except for tom7 of course
11:14:44 <esowiki> [[EnScript]] M https://esolangs.org/w/index.php?diff=63065&oldid=63048 * A * (+44) /* ENC */ That is impossible
11:19:41 <esowiki> [[Collide]] N https://esolangs.org/w/index.php?oldid=63066 * A * (+177) Created page with "[[Collide]] is an [[esoteric programming language]] that features balls inside a sandbox that maps its edges. [[Category:Languages]] [[Category:2019]] [[Category:Unimplemented]]"
11:21:58 -!- sebbu3 has changed nick to sebbu.
11:23:50 <esowiki> [[Collide]] M https://esolangs.org/w/index.php?diff=63067&oldid=63066 * A * (+435) Example program
11:31:54 <esowiki> [[Collide]] https://esolangs.org/w/index.php?diff=63068&oldid=63067 * A * (+393) /* Example source code (this is not yet documented) */
11:33:15 <esowiki> [[Collide]] M https://esolangs.org/w/index.php?diff=63069&oldid=63068 * A * (+115) /* Partial syntax */
11:33:26 <esowiki> [[Collide]] M https://esolangs.org/w/index.php?diff=63070&oldid=63069 * A * (-8) /* Partial syntax */
11:34:40 <esowiki> [[Collide]] M https://esolangs.org/w/index.php?diff=63071&oldid=63070 * A * (+305) /* Syntax */
11:35:02 <esowiki> [[Collide]] M https://esolangs.org/w/index.php?diff=63072&oldid=63071 * A * (+1) /* Example source code (this is not yet documented) */
11:36:40 <esowiki> [[Collide]] https://esolangs.org/w/index.php?diff=63073&oldid=63072 * A * (+188) /* Syntax */
11:37:33 <esowiki> [[Collide]] M https://esolangs.org/w/index.php?diff=63074&oldid=63073 * A * (+85) /* Syntax */
11:38:28 -!- copumpkin has joined.
11:41:08 <fizzie> Backfilled the logs.
12:03:23 <esowiki> [[Talk:EnScript]] https://esolangs.org/w/index.php?diff=63075&oldid=63064 * JonoCode9374 * (+220) /* The ENC Command */
12:20:14 <int-e> @let import GHC.Fingerprint
12:20:15 <lambdabot> Defined.
12:21:07 <int-e> > map fingerprintString ["T\153831\150310\131091\149266\154351\131093\131072\131072\131072","T\143618\144507\156283\135458\133470\131097\131072\131072\131072"]
12:21:10 <lambdabot> [7afb892b07b256865b1116e31478f2bf,7afb892b07b256865b11353481ce648e]
12:21:21 <int-e> shachaf: ^^ 80 bit collision
12:36:44 <int-e> Now crunching a 96 bit collision at 5GH/s. So it'll be a while, but should finish within a day.
12:36:48 <int-e> or two.
12:37:51 <wob_jonas> int-e: are you just using a dumb birthday attack, or something specific about md5?
12:39:23 <wob_jonas> dumb birthday attack, according to those numbers
12:47:59 <int-e> wob_jonas: I'm doing the dumb birthday attack indeed
12:48:19 <int-e> wob_jonas: and I know that it's (almost) impractical to scale it up to a full collision.
12:49:03 <int-e> But it's unclear how to apply the differential paths based techniques when about half of the bits of the input are fixed.
12:54:07 <wob_jonas> int-e: ok. are you using those optimized cycle-based methods that let you get away with much less than a table of 2**48 hashes?
12:54:51 <wob_jonas> I found those quite interesting, and because you don't have enough RAM for 2**48 entries, but may have enough for a smaller table, it could be faster too
12:55:11 <int-e> hmm, not really cycle based... but based on distinguished elements (the rainbow table trick)
12:55:23 <wob_jonas> yeah, that
12:55:36 <wob_jonas> not cycle based, but computing deterministic chains that you can reproduce
12:56:04 <wob_jonas> and once you find two chains intersecting, you can compute them again from an earlier stage to find the first collision,
12:56:07 <int-e> 2^48/2^30 is what I'm aiming for.
12:56:39 <wob_jonas> 2^48/2^30 what?
12:56:41 <int-e> which is probably not the best memory/time trade-off for my hardware, but who cares.
12:57:00 <wob_jonas> 2^30 entries in memory?
12:57:08 <int-e> I'm only storing hashes with the 30 lowest bits zero.
12:57:12 <wob_jonas> oh
12:57:18 <wob_jonas> yeah, that may be too strong, but whatever
12:57:43 <int-e> it fits my naive approach... I'm not actually storing those in memory but in a file, because I'm lazy.
12:57:43 <wob_jonas> that means you have to recompute a 2^30 long chain. how fast can you do that, since you don't have parallelism then?
12:58:10 <wob_jonas> storing them in a file is fine because the OS can cache the file in RAM
12:58:35 <wob_jonas> the point is not to have such a large database to have to spin the disk up for every access
12:59:59 <int-e> it'll take a couple of minutes
13:00:29 <int-e> on the CPU I get about 10MH/s sequentially.
13:00:52 <wob_jonas> seems workable
13:01:35 <int-e> (with plain C code)
13:02:34 <int-e> wob_jonas: I'm storing them in a text file... so sort | uniq works ;-)
13:07:07 <wob_jonas> ok
13:09:17 -!- Sgeo_ has joined.
13:09:59 <wob_jonas> hi Sgeo
13:10:40 <wob_jonas> int-e: so what was the context for this? why did you want haskell identifiers and md5 in particular? is it md5 because of git?
13:10:55 <wob_jonas> no wait, git uses sha-1, right?
13:12:46 -!- Sgeo has quit (Ping timeout: 272 seconds).
13:16:28 <wob_jonas> > map (\s -> map ord) ["T\153831\150310\131091\149266\154351\131093\131072\131072\131072","T\143618\144507\156283\135458\133470\131097\131072\131072\131072"]
13:16:30 <lambdabot> [<[Char] -> [Int]>,<[Char] -> [Int]>]
13:16:34 <wob_jonas> how do string escapes work?
13:16:48 <wob_jonas> > map (\s -> map ord s) ["T\153831\150310\131091\149266\154351\131093\131072\131072\131072","T\143618\144507\156283\135458\133470\131097\131072\131072\131072"]
13:16:50 <lambdabot> [[84,153831,150310,131091,149266,154351,131093,131072,131072,131072],[84,143...
13:17:17 <int-e> > "\84\%123"
13:17:19 <lambdabot> <hint>:1:6: error:
13:17:19 <lambdabot> lexical error in string/character literal at character '%'
13:17:24 <int-e> > "\84\&123"
13:17:26 <lambdabot> "T123"
13:17:31 <int-e> that was the wrong magic character.
13:17:42 <wob_jonas> no, I just wanted to decode those strings you typed
13:17:55 <int-e> > text "T\153831\150310\131091\149266\154351\131093\131072\131072\131072"
13:17:58 <lambdabot> T𥣧𤬦𠀓𤜒𥫯𠀕𠀀𠀀𠀀
13:17:58 <wob_jonas> because I didn't remember the haskell syntax
13:18:17 <wob_jonas> um, I don't much care about the particular kanji, more like the code points
13:18:28 <wob_jonas> but lambdabot's answer gave those
13:19:11 <int-e> I used printf("\"%c\\%d\\%d\\%d\\%d\\%d\\%d\\%d\\%d\\%d\"\n", to generate those strings ;-)
13:21:04 <int-e> wob_jonas: the context is GHC.
13:22:07 <int-e> A collision would break the type safety of Data.Typeable.
13:22:14 <wob_jonas> their digests don't seem to match for me, how do you encode them?
13:22:40 <int-e> as big endian 32 bit unicode points.
13:22:46 <wob_jonas> I tried utf-8, utf-16be, and utf16-le
13:22:51 <wob_jonas> ah, so utf-32be
13:23:22 <wob_jonas> so that's why you said that almost half of the bits were fixed
13:23:39 <int-e> I said about...
13:25:07 <wob_jonas> yeah, I can reproduce that, the first 10 bytes of the digest match
13:25:45 <wob_jonas> and you'd need a full 128 bit collision to break Typeable?
13:26:03 <wob_jonas> and you can use just identifiers with no prefix, not even a package name?
13:26:51 <wob_jonas> it would seem strange if it didn't use a package name
13:27:06 <Taneb> (would it also have to be two valid identifiers?)
13:27:07 <int-e> yeah the package, module, and type name are hashed separately, then combined.
13:27:14 <wob_jonas> oh
13:27:22 <int-e> fingerprintTyCon tc =
13:27:22 <int-e> fingerprintFingerprints [
13:27:22 <int-e> fingerprintString (tyConPackage tc),
13:27:22 <int-e> fingerprintString (tyConModule tc),
13:27:22 <int-e> fingerprintString (tyConName tc)
13:27:24 <int-e> ]
13:27:28 <wob_jonas> Taneb: these are valid identifiers
13:27:33 <wob_jonas> they're made of mostly kanji
13:27:37 <wob_jonas> or at least int-e said so
13:27:40 <Taneb> Ah, right
13:27:41 <wob_jonas> let me see
13:27:54 <int-e> @let data T𥣧𤬦𠀓𤜒𥫯𠀕𠀀𠀀𠀀 = T𥣧𤬦𠀓𤜒𥫯𠀕𠀀𠀀𠀀
13:27:55 <lambdabot> Defined.
13:29:47 <int-e> The "valid identifier" restriction is also the reason for that "T", because more precisely, it has to be a valid constructor name
13:30:07 <int-e> and there are no upper case kanjis, somehow :)
13:31:27 <wob_jonas> I was wondering if this is perhaps solved by the internet somehow, but apparently no sane people hash utf-32 strings
13:31:39 <wob_jonas> utf-8 strings, sure, you can find collisions with a google search
13:32:01 <wob_jonas> ah
13:32:01 <wob_jonas> https://gitlab.haskell.org/ghc/ghc/issues/7634
13:32:20 <wob_jonas> a bug ticket for ghc
13:34:59 <esowiki> [[User talk:A]] M https://esolangs.org/w/index.php?diff=63076&oldid=62864 * A * (+188) /* Write some nonsense here */ Nonsense
13:36:48 <wob_jonas> int-e: that ticket tells the hashing works differently though: it seems to think that the package name, module name, and typename are combined before they're md5-hashed
13:38:01 <int-e> it changed
13:38:36 <wob_jonas> ah
13:38:40 <int-e> I don't know when exactly, whether it was ghc-8.0 or ghc-8.2. We have ghc-8.8 now.
13:48:03 <esowiki> [[Esolang:Featured languages/Candidates]] https://esolangs.org/w/index.php?diff=63077&oldid=62865 * A * (+310) /* List of candidates */ Add a lot of info
13:50:48 <esowiki> [[User talk:A]] M https://esolangs.org/w/index.php?diff=63078&oldid=63076 * A * (+193) Add some nonsense(just for fun)
13:53:24 <esowiki> [[User talk:A]] M https://esolangs.org/w/index.php?diff=63079&oldid=63078 * A * (+15)
14:07:23 -!- Lord_of_Life has quit (Ping timeout: 248 seconds).
14:09:01 -!- Lord_of_Life has joined.
14:22:45 <esowiki> [[Bitch]] M https://esolangs.org/w/index.php?diff=63080&oldid=62948 * A * (+93) /* References */
14:52:39 <arseniiv> are ε and ℩ interdefinable? εxA = «an x such that A, if it exists (or some garbage if it doesn’t, and terms aren’t allowed to be undefined)», ℩xA = «the only x such that A (or likewise blah blah)»
14:53:46 <arseniiv> they say ∀ and ∃ are definable through any of them, though ε is in some sense more powerful; and I don’t remember about ℩
14:55:07 <arseniiv> for ε, ∃xA ≡ A[εxA / x] and ∀xA ≡ A[εx(¬A) / x]
14:57:48 <arseniiv> ℩ seems less powerful
14:58:21 <arseniiv> I’m suddenly into formal semantics of natural languages
15:02:05 <arseniiv> for example, I think the section [1] is somewhat garbage-y, and I sympathize with the text at [2], but I don’t know what level the unambiguous translation mentioned there should be, and ever at least what it should look like
15:02:06 <arseniiv> [1] https://en.wikipedia.org/wiki/De_dicto_and_de_re#Representing_de_dicto_and_de_re_in_modal_logic
15:02:06 <arseniiv> [2] https://en.wikipedia.org/wiki/Theory_of_descriptions#Saul_Kripke
15:06:21 -!- Sgeo__ has joined.
15:09:37 -!- Sgeo_ has quit (Ping timeout: 258 seconds).
15:19:57 <arseniiv> also, regarding formulas in [1], I’m not only worried they miss the point, I’m also don’t quite get what should be meant by a formula □A with free variables. So I’ve read about approaches to first-order modal logics and now I’m still unsure ∃x□A is sensible
15:20:40 <arseniiv> about [1
15:20:45 <arseniiv> oh sorry
15:25:07 <arseniiv> about [1], I’ve come to think the difference shouldn’t be forced to be expressed free of speech context and that the focus is not a different translation of the syntax per se, but a different denotation of a phrase (designator, is it?) in question. In de dicto case, it isn’t bound to something in context, and in de re case, it is but a name of a thing from the context, its identity established ear
15:26:50 <wob_jonas> fungot, are you forced to expressed free of context speech and that the focus is not a different translation of syntax per se?
15:26:51 <fungot> wob_jonas: social contract. i think he will agree with fnord of common sense reasons? no; the question is, whether for war or trade; when i bring before my view the number of men in power, he holds his crown in contempt of the opinion of the intellectual eye which gives us to contemplate the fall of wise ministers and of the purity and integrity of the empire, and who serves to carry on with vigour the work of his successor, an
15:27:17 <wob_jonas> heh
15:30:11 <arseniiv> so maybe it is just a plain restatement of what is already known about this phenomenon—maybe in not so different fashion, either—but I do think it shouldn’t match something too low-level. There IS speech context, and it IS being used to disambiguate the cases, so it makes sense this situation should be formalized using a formalization of this context, and not some clever transposition of ∃x and □ (or I just hope that entry is
15:30:11 <arseniiv> an unqualified one by someone who understands even less than me)
15:30:41 <arseniiv> wob_jonas: fungot: :D
15:30:41 <fungot> arseniiv: vii. second reading of the bill which concerns my trade. i will only observe, in reference to this sphere of legislative action, with stars on his shoulders and his fnord is embittered into acrimony, strength fnord into fnord, or brissot, or fnord conventional messenger from the clouds, to firm ground and clear light. let us imitate him. our countrymen have always, even in that fugitive span he may either do some good
15:32:13 <arseniiv> (vii, oh my)
15:35:18 <wob_jonas> https://esolangs.org/logs/2019-06-01.html#lUb "<xylochoron[m]> do you other people know enough about category theory to follow what this person's trying to do cuz i don't but it sounds interesting oh well"
15:36:28 <wob_jonas> I was wondering if I should tell xylochoron[m] that if he hangs out enough on this channel, not only will he understand the category theoretic formulation, but he'll find it natural and find the more elementary phrasings of those problems unnecessarily cumbersome, but frankly I don't understand what you guys are talking about either
15:36:30 <Taneb> I sit with a copy of Categories for the Working Mathematician on my desk. I should probably read it more
15:50:39 <arseniiv> fungot: how do you think are deontological self-actualization and ontological self-deactualization dual?
15:50:39 <fungot> arseniiv: this great work at once became fnord which everybody still knows by fnord these chiefly lay the oratorical power both of chatham and of mirabeau. there have been famous orators whose speeches we may read for the beauty of the garden, the nurture of all living things.
15:51:25 <arseniiv> agree about the garden
15:55:51 <arseniiv> re tswett[m] discussion: presentations of categories with finite limits, is it really that simple? I should look into that someday!
15:57:28 <arseniiv> though a presentation could turn out an elaborate and complex thing which is hard to understand
15:59:00 <tswett[m]> arseniiv: You can do a ton with just presentations of categories with finite limits.
15:59:09 <tswett[m]> They're... not particularly simple.
15:59:12 <arseniiv> (…as it is with group presentations, it really really is no doubt)
15:59:20 <tswett[m]> But they're much simpler than, say, Lua.
15:59:51 <tswett[m]> But they're much simpler than, say, Lua.
16:00:07 <tswett[m]> In particular, pretty much any kind of algebraic object can be defined by giving a presentation of a category with finite limits.
16:00:13 -!- wob_jonas has quit (Remote host closed the connection).
16:00:26 <arseniiv> <tswett[m]> But they're much simpler than, say, Lua. => ah, then you got me
16:00:57 <tswett[m]> Including—and this is the fun part—categories with finite limits.
16:01:42 <arseniiv> a categorical self-indertion
16:01:52 <arseniiv> self-insertion*
16:01:53 <tswett[m]> Well, I shouldn't say "pretty much any kind", but you can define monoids, groups, categories, rings...
16:02:03 <tswett[m]> Probably not fields.
16:02:05 <tswett[m]> You can *almost* define topoi.
16:02:39 <arseniiv> are fields undefinable because of 1 ≠ 0 constraint? I think I heard something in that regard maybe
16:03:37 <tswett[m]> That, and the fact that division is defined everywhere except 0.
16:03:58 <tswett[m]> Now, you can define a concept that's *almost* the concept of a topos.
16:04:24 <arseniiv> tswett[m]: hm also do these presentations come with a nice internal language or what it’s called?
16:05:07 <tswett[m]> The difference is that in the definition of a topos, the word "monomorphism" is replaced with "M-morphism", where an "M-morphism" is a morphism satisfying an undefined predicate. You can assert that all M-morphisms are monomorphisms, but you cannot assert that all monomorphisms are M-morphisms.
16:05:20 <tswett[m]> I... think so.
16:06:10 <tswett[m]> Though the internal language is missing coproducts (sum types) and the initial object (the empty type).
16:06:36 <tswett[m]> Not to mention exponentials (function types).
16:35:17 -!- LKoen has joined.
16:51:12 <int-e> > map fingerprintString ["T\132596\149647\150416\152631\158821\150114\131116\131072\131072","T\140399\149685\144161\143085\148849\152119\131204\131072\131072"] -- <-- shachaf, wob_jonas: I got quite lucky. GPU time: 4h, CPU time: 20m
16:51:15 <lambdabot> [9317f8f6f091ac50e1f49feb057f3098,9317f8f6f091ac50e1f49febea88f23a]
16:52:19 <int-e> (Expected GPU time was around 15h.)
16:58:07 -!- tromp has quit (Remote host closed the connection).
17:20:19 -!- moei has joined.
17:24:46 -!- LKoen has quit (Remote host closed the connection).
17:28:47 <esowiki> [[Talk:Pointless]] N https://esolangs.org/w/index.php?oldid=63081 * Ais523 * (+513) the pointer instructions aren't useful because the cell values are limited
17:32:18 -!- sleepnap has joined.
17:41:15 -!- unlimiter has joined.
17:53:48 <esowiki> [[Talk:Pointless]] https://esolangs.org/w/index.php?diff=63082&oldid=63081 * Int-e * (+462) translate from Smallfuck
17:58:07 -!- unlimiter has quit (Quit: WeeChat 2.4).
18:00:46 -!- LKoen has joined.
18:22:28 -!- sleepnap has quit (Ping timeout: 272 seconds).
18:30:48 -!- tromp has joined.
18:35:05 -!- tromp has quit (Ping timeout: 252 seconds).
18:44:52 -!- budonyc has joined.
19:07:36 -!- adu has joined.
19:14:15 -!- b_jonas has joined.
19:25:37 -!- sleepnap has joined.
19:33:40 -!- Phantom_Hoover has joined.
19:37:41 -!- FreeFull has joined.
19:57:37 <int-e> shachaf: the best thing is that the md5 implementation can be shared between OpenCL and C. https://github.com/int-e/opencl-playground/blob/master/md5_impl.h ...
19:59:02 <int-e> (It appears that the OpenCL compiler takes care of vectorizing that thing, which keeps the code plain and simple.)
20:00:09 <rain1> wow an md5 hash collision!
20:00:24 <int-e> rain1: only 96 bits
20:01:13 <int-e> I don't want to wait nor pay for ~2^64 md5 hashes :) 2^48 was just fine though.
20:01:48 <int-e> Especially since I got away with just 2^46 of them...
20:04:23 <int-e> So 1/4 sqrt(N)... which suffices only 3% of the time, I think...
20:04:49 <int-e> > 1 - exp(-(1/4)^2/2) -- should be close
20:04:52 <lambdabot> 3.076676552365587e-2
20:19:04 -!- tromp has joined.
20:23:38 -!- tromp has quit (Ping timeout: 258 seconds).
20:32:22 -!- sleepnap has quit (Quit: Leaving.).
20:45:43 <arseniiv> for something completely different, maybe someone remembers when I mused about a Metamath-like system (metavariables! disjointness constraints!) with solid syntax soundness base (terms with more or less simple types, basically an enriched λ-calculus where this λ core is used solely for representing substitutions, and application to user-defined term constructors is intentionally not core λ-term application), so one can then define t
20:45:43 <arseniiv> he language and the rules and the system would check if some proof is correct, including of course checking typeability of all terms
20:48:55 -!- AnotherTest has quit (Ping timeout: 252 seconds).
20:53:49 <arseniiv> then I needed an algorithm to check it there is a substitution σ such that A ≡ Bσ for given terms A, B with FV(A) ∩ FV(B) = ∅, and is there a unique smallest σ (how do they call such σ?)
20:53:49 <arseniiv> and I was sad to find I don’t know how to check it in case B ≡ CD (λ application here), as I have thought it’s sensible to think (λx. z = x)y equivalent—for this system—to y = x: and now how can I decide how many β-reductions there could be in that CD term before it would be mapped by σ to A?
20:53:49 <arseniiv> so I was stuck and left the thing alone and one day had an idea to make reductions a core inference rule for users to mention explicitly. It would not be a smooth UX, but at least I could write the thing and see if it’s any good at all. And then I forgot, and remembered only a hour ago
20:54:06 <arseniiv> maybe it would be clearer to give an example:
20:55:40 <arseniiv> Axiom: X = Y ∧ Φ[X] → Φ[Y]
20:55:40 <arseniiv> Given: x = y ∧ x = x → y = x
20:55:40 <arseniiv> ↑ this isn’t well-prepared, it should be un-β-reduced explicitly by the user to
20:55:40 <arseniiv> Given′: x = y ∧ (z.z = x)[x] → (z.z = x)[y]
20:55:40 <arseniiv> then the system could show easily that Given′ ≡ Axiom[x/X, y/Y, z.z = x/Φ] without the need to decide when exactly (x = x, x = y) ≡ (Φ[X], Φ[Y])σ and is there a unique smallest σ at all
20:59:47 <arseniiv> so maybe I’m just dumb and there is no need to test someone’s patience in writing extra things like Given’ and one could write a unifier for a general case A = (CD)σ and not fall into depths of e. g. nontermination (I hope, as all terms should be typeable, could it be enough to simplify things?..)
21:00:56 <arseniiv> oh, I forgot to make my syntax less obscure again
21:02:01 <arseniiv> in the example, X, Y, Φ, x, y, z are metavariables, =, ∧ and → are user-defined term constructors, Φ[X] is ΦX and (z.z = x) is (λz. z = x)
21:02:48 <arseniiv> very fortunately, this example doesn’t mention disjointness constraints
21:04:38 <arseniiv> they can be part of the rules and proofs, as a type of premise (other type of premises is terms, and rule conclusion can be only a term too)
21:08:57 <int-e> > let f = 85375/2^18 in 1 - exp (f^2/2)
21:08:58 <lambdabot> -5.446513701917932e-2
21:09:04 <int-e> > let f = 85375/2^18 in 1 - exp (-f^2/2)
21:09:06 <lambdabot> 5.165190873274805e-2
21:10:25 <int-e> 5% is still quite lucky :)
21:11:44 <shachaf> you really squandered your luck there hth
21:14:08 <int-e> Nah, I don't believe in luck being used up.
21:16:18 -!- tromp has joined.
21:19:17 <shachaf> your dice are pre-rolled
21:32:39 <int-e> "IntelliCode uses open source GitHub projects with 100 stars or more to generate recommendations for your code."
21:32:46 -!- Phantom_Hoover has quit (Read error: Connection reset by peer).
21:33:10 <int-e> . o O ( What could possibly go wrong... )
21:33:22 <int-e> . o O ( This may also explain why MS bought github? )
21:36:59 -!- sleepnap has joined.
21:38:08 -!- Phantom_Hoover has joined.
21:38:08 -!- Phantom_Hoover has quit (Changing host).
21:38:08 -!- Phantom_Hoover has joined.
21:41:05 <int-e> Ironically I have learned little about OpenCL... no out-of-order execution, no fancy atomic operations or shared CPU/GPU memory, no subtle memory model (yes, there is a memory model...) interactions, no pipes, no kernels spawning kernels on the OpenCL side, and no interaction with OpenGL.
21:41:52 <b_jonas> int-e: well sure, you just want to compute a lot of md5 checksums, surely that's something someone else has already coded, so you don't need to write any of the parallel code
21:41:58 <b_jonas> you only need the driver that chooses the strings etc
21:42:17 <int-e> (Instead I have a fairly long-running kernel so that the overhead of communicating with the CPU is negligible anyway. And each work item works on a couple of hundred bytes of data, all completely local.)
21:42:26 <b_jonas> I mean sure, that has to run in the gpu too
21:42:30 <b_jonas> but it's not very complicated
21:42:40 <b_jonas> int-e: exactly
21:42:44 <b_jonas> very easy to parallelize
21:42:52 <shachaf> yes, int-e, didn't you notice the thing where instead of doing any programing you just downloaded and ran someone else's program
21:42:59 -!- budonyc has quit (Quit: Leaving).
21:43:14 <int-e> b_jonas: hashcat has an md5 implementation... but it seems to be specially tuned for password cracking, which surprisingly allows a few small shortcuts.
21:43:15 <shachaf> that's the reason you didn't learn anything
21:43:58 <int-e> shachaf: condescension: 10, helpfulness: 0.
21:44:20 <shachaf> i was just making a joke about how the thing b_jonas said made no sense :'(
21:44:35 <int-e> (hashcat reports 11.5MH/s in its benchmark mode on the same GPU, so I thought my 5.something was decent.)
21:44:39 <b_jonas> while generally I think GPU programming is overhyped these days (partly because "blockchain" and "deep learning" are fashionable ways to sell anything), but this is exactly the sort of thing where GPU is useful
21:44:54 <int-e> shachaf: ah, I didn't connect it to that context.
21:45:05 <int-e> . o O ( communication 1 : int-e 0. )
21:45:17 <shachaf> since obviously you did write a program so the fact that other people have written md5 implementations is irrelevant
21:45:36 <b_jonas> um
21:46:47 <int-e> shachaf: Obviously I still had to do some basic stuff. create an OpenCL context, a command queue, a buffer, a program, a kernel... it's just that there's so much more that I didn't touch at all.
21:47:05 <shachaf> Yes.
21:48:19 <shachaf> Doing the rho thing with distinguished points is presumably a little different from trying to find preimages.
21:49:17 <int-e> hashcat exploits the fact that when enumerating passwords, only a small part of the message changes... so the first half dozen values can be precomputed and never change while iterating over the last one or two chracters.
21:49:55 <shachaf> I imagine that only saves a small amount of work?
21:50:01 <int-e> And IIRC it has a trick for stopping early too. I forgot.
21:50:23 <int-e> well saving 10 out of 64 rounds (or even 5) is still a speedup.
21:50:56 <shachaf> You can compute 10 rounds without the last one or two characters?
21:51:43 <int-e> I think it was about 4 at the beginning and 4 in the end. Let me check something
21:55:29 <int-e> There's stuff like this: If you only change the 3rd word of the message in your search, then you know the message words for the last 10 rounds. And I think you can actually invert those then.
21:56:49 <int-e> (look at this: A = B + rotl(R(B, C, D) + A + K + m[j], s) -- you know the resulting A, and B,C,D,K and m[j]. So you do rotr(A - B, s) - K - m[j] - R(B,C,D)) to find the previous A.
21:56:54 <int-e> )
21:57:16 <int-e> s/3rd/4th/
21:57:49 <int-e> And, uh, why don't we do that with the first word... then we can reverse the last 15 rounds.
21:59:38 <int-e> > maximum [(elemIndex i [0..15] + elemIndex i (reverse [0,7,14,5,12,3,10,1,8,15,6,13,4,11,2,9]), i) | i <- [0..15]]
21:59:40 <lambdabot> error:
21:59:40 <lambdabot> • Could not deduce (Num (Maybe Int)) arising from a use of ‘+’
21:59:40 <lambdabot> from the context: (Num b, Enum b, Ord b)
21:59:47 <int-e> meh
22:00:19 <int-e> > maximum [(fromJust (elemIndex i [0..15]) + fromJust (elemIndex i (reverse [0,7,14,5,12,3,10,1,8,15,6,13,4,11,2,9])), i) | i <- [0..15]]
22:00:22 <lambdabot> (27,14)
22:00:53 <int-e> > reverse $ sort [(fromJust (elemIndex i [0..15]) + fromJust (elemIndex i (reverse [0,7,14,5,12,3,10,1,8,15,6,13,4,11,2,9])), i) | i <- [0..15]]
22:00:56 <lambdabot> [(27,14),(23,12),(21,15),(21,7),(19,10),(17,13),(17,5),(15,8),(15,0),(13,11)...
22:02:46 <int-e> So for the password cracking application, it's the last 15 rounds that you can reasonably expect to skip. The better indices are a tad too large.
22:03:48 -!- sleepnap has quit (Ping timeout: 245 seconds).
22:10:32 -!- Phantom_Hoover has quit (Remote host closed the connection).
22:10:45 <int-e> and you can skip 3 more rounds if you only verify 32 bits instead of all the 128 bits.
22:12:52 <int-e> what else is there... for password cracking you tend to have a lot of message words that are known to be 0. That should also yield a minor but noticable improvement.
22:20:54 -!- tromp has quit (Remote host closed the connection).
22:21:29 -!- tromp has joined.
22:29:39 -!- sleepnap has joined.
22:30:05 -!- sleepnap has left.
22:39:15 <b_jonas> `? pencil
22:39:16 <HackEso> pencil? ¯\(°​_o)/¯
22:39:37 <int-e> A pencil is an abridged antibiotic.
22:40:15 -!- LKoen has quit (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”).
22:40:21 <int-e> (I guess it works by stabbing bacteria.)
22:40:49 <b_jonas> yeah
22:53:07 -!- arseniiv_ has joined.
22:53:47 -!- arseniiv has quit (Ping timeout: 248 seconds).
22:58:16 -!- moei has quit (Quit: Leaving...).
23:01:42 -!- arseniiv_ has changed nick to arseniiv.
23:31:07 -!- Soni has quit (Quit: http://quassel-irc.org - Chat comfortably. Anywhere.).
23:32:25 -!- Soni has joined.
23:36:48 -!- b_jonas has quit (Quit: leaving).
23:44:59 -!- arseniiv has quit (Ping timeout: 248 seconds).
23:46:26 -!- S_Gautam has quit (Quit: Connection closed for inactivity).
←2019-06-03 2019-06-04 2019-06-05→ ↑2019 ↑all