00:14:38 <int-e> wtf is the rationale for renewing SSL certifcates twice a day (certbot default)
00:15:25 <Frankenlime> i gave up on certbot because it was always confusing and never worked for me
00:15:43 <Frankenlime> im not normally a fan of tools made out of shellscripts but dehydrated works so great, especially with dns auth
00:16:23 <fizzie> int-e: It doesn't renew twice a day. Or it shouldn't, anyway.
00:16:38 <fizzie> int-e: It *runs* twice a day, but only renews when there's less than 30 days remaining.
00:16:52 <int-e> Oh. Hmm.
00:17:06 <int-e> Right, that makes more sense.
00:17:37 <int-e> Frankenlime: I've used acme-tiny before.
00:17:51 <Frankenlime> acme-tiny seemed nice
00:18:14 <Frankenlime> i've used acme.sh at work too and its not terrible (although only used it for web auth)
00:18:58 <int-e> Yeah I only need web auth anyway, so far.
00:19:42 <fizzie> I'm using `certbot certonly --config ... --force-renewal` to basically just use certbot as a plain client (with DNS auth), it seems to work.
00:20:23 <int-e> But this time I decided to experience the hammer that is certbot.
00:20:50 <Frankenlime> see certonly and renew (or run?) differences always confused me
00:20:59 <Frankenlime> although to be fair i do get confused easily
00:21:48 <int-e> fizzie: thanks.
00:22:03 <fizzie> AIUI, the 'certonly' part means "just do the stuff related to acquiring certificates, don't try to touch the servers that use the certificate", which is what I want out of it.
00:22:14 <fizzie> (It won't have permissions to do any other actions anyway.)
00:22:19 <int-e> I only looked at the systemd timer and jumped to conclusions.
00:22:33 -!- sftp has joined.
00:22:34 <Frankenlime> oh well, i got it all working in ansible and haven't bothered touching it since
00:39:01 -!- sftp has quit (Ping timeout: 258 seconds).
01:13:48 -!- sftp has joined.
01:53:09 <esowiki> [[Esolang:Introduce yourself]]  https://esolangs.org/w/index.php?diff=77874&oldid=77853 * Vpzom * (+72) 
01:58:37 <esowiki> [[Four]] N https://esolangs.org/w/index.php?oldid=77875 * Vpzom * (+2759) Created page with "{{infobox proglang |name=Four |paradigms=[[:Category:Functional paradigm|Functional]] |author=[[user:Vpzom|vpzom]] |majorimpl=https://git.vpzom.click/vpzom/four |files=<code>...."
02:01:11 <esowiki> [[Four]]  https://esolangs.org/w/index.php?diff=77876&oldid=77875 * Vpzom * (+30) 
02:17:33 -!- sprocklem has quit (Quit: brb).
02:29:14 -!- sprocklem has joined.
02:33:56 -!- adu has joined.
03:07:11 -!- adu has quit (Quit: adu).
03:30:36 -!- adu has joined.
05:00:39 -!- MDude has quit (Quit: Going offline, see ya! (www.adiirc.com)).
05:04:07 -!- spruit11 has quit (Ping timeout: 240 seconds).
05:45:21 -!- spruit11 has joined.
06:16:06 -!- arseniiv has joined.
06:19:47 -!- lignus has joined.
06:24:35 -!- Sgeo_ has quit (Read error: Connection reset by peer).
06:35:30 -!- wmww has quit (Quit: killed).
06:35:42 -!- tswett[m] has quit (Quit: killed).
06:35:46 -!- Discordian[m] has quit (Quit: killed).
06:44:16 -!- tswett[m] has joined.
06:52:58 -!- imode has quit (Ping timeout: 256 seconds).
07:09:25 -!- wmww has joined.
07:09:31 -!- iscordian[m] has joined.
07:15:33 -!- adu has quit (Quit: adu).
07:18:51 -!- sprocklem has quit (Ping timeout: 260 seconds).
07:23:21 -!- iscordian[m] has changed nick to Discordian[m].
07:33:02 -!- arseniiv has quit (*.net *.split).
07:33:02 -!- b_jonas has quit (*.net *.split).
07:33:02 -!- izabera has quit (*.net *.split).
07:33:02 -!- paul2520 has quit (*.net *.split).
07:33:27 -!- arseniiv has joined.
07:38:33 -!- b_jonas has joined.
07:38:33 -!- izabera has joined.
07:38:33 -!- paul2520 has joined.
08:00:00 -!- cpressey has joined.
08:00:59 -!- lignus has quit (Remote host closed the connection).
08:08:34 -!- hendursa1 has joined.
08:10:43 -!- hendursaga has quit (Ping timeout: 240 seconds).
08:11:54 <esowiki> [[User:RubenVerg]] N https://esolangs.org/w/index.php?oldid=77877 * RubenVerg * (+6) Created page with "hello!"
09:25:54 -!- ProofTechnique has quit (Ping timeout: 260 seconds).
09:28:34 -!- ProofTechnique has joined.
09:30:27 -!- t20kdc has joined.
10:07:14 -!- sftp has quit (Ping timeout: 272 seconds).
10:11:57 -!- sftp has joined.
10:19:54 <Taneb> Is there a theorem that for every positive natural, n, the Fibonacci sequence contains infinitely many integer multiples of n?
10:34:55 <cpressey> https://en.wikipedia.org/wiki/Fibonacci_number says "If the members of the Fibonacci sequence are taken mod n, the resulting sequence is periodic with period at most 6n." -- is that equivalent?
10:36:00 <cpressey> I guess it's not quite equivalent, because every 6th positive natural != every positive natural
10:36:22 <cpressey> Closest I could find on that page though
10:36:40 <int-e> Note that F_0 = 0 is divisible by n. So together with periodicity modulo n you get what you want.
10:38:14 <int-e> I have not seen that 6n claim before, interesting.
10:39:57 <cpressey> Also, simply saying "periodic" doesn't imply that F_i mod n = 0 at any time, so far as I'm aware, so, I'm not so sure
10:40:38 <int-e> Periodicity is rather obvious though; there are n^2 possible pairs of consecutive remainders in the sequence, so it's ultimately periodic. But you can also reconstruct the whole sequence from any pair (computing F_n from F_(n+1) and F_(n+2)), so it's fully periodic
10:41:10 <int-e> i=0 works.
10:44:46 <int-e> There's also the related fact that F_n | F_(nk) for all integers n, k.
10:44:54 <cpressey> Yeah OK, I see how F_0 = 0 implies it F_i mod n = 0 for some i, if it's periodic 
10:46:03 <fizzie> I'm not sure I followed that periodicity argument, why does having n^2 possible pairs of consecutive remainders mean it's ultimately periodic? 
10:47:25 <int-e> fizzie: because you can look at the sequence of pairs FF_n = (F_n, F_(n+1)) and note that there's a relation FF_(n+1) = f(FF_n), to which the standard argument applies.
10:47:54 <int-e> f((x,y)) = (y,x+y)
10:48:33 <int-e> (and f is invertible over any ring)
10:49:25 <int-e> But the 6n bound is interesting, because from that idea, you only get an n^2 bound.
10:54:38 <int-e> (the "standard element" is that by the pigeon-hole principle, *some* element must repeat, and from that point onward, all the elements must repeat because that single element determines all its successors.)
10:55:26 <int-e> (and, if f() is invertible, the predecessors as well, giving full periodicity rather than just ultimate periodicity.)
11:21:42 <int-e> Oh, that's a clever use of the Frobenius automorphism. (https://en.wikipedia.org/wiki/Pisano_period#Properties near the end of the section.)
11:27:10 <int-e> (and that is the main reason why we don't get near the naive n^2 bound)
11:30:54 <int-e> "Any prime p providing a counterexample would necessarily be a Wall-Sun-Sun prime, and such primes are also conjectured not to exist."
11:30:57 <int-e> "In number theory, a Wall–Sun–Sun prime or Fibonacci–Wieferich prime is a certain kind of prime number which is conjectured to exist, although none are known."
11:31:06 <int-e> Source: Wikipedia :-)
11:36:00 <cpressey> Which is not actually a contradiction, if there really are two different mathematicians making two different conjecturs on the existence of these things
11:36:07 <cpressey> But, it does seem a bit unlikely
11:52:40 <cpressey> In other news, I think I now see why MonadPrompt and Operational use GADTs.
11:53:07 <cpressey> :t (>>=)
11:53:09 <lambdabot> Monad m => m a -> (a -> m b) -> m b
11:56:00 <cpressey> The GADT gives you an existential type that can be used for b.  If you don't have that, you don't have anything you can use for b.
11:57:53 <cpressey> (That I can see.)
12:01:38 <cpressey> Mmmmmmaybe you could put both a and b in the ADT, like data Program instr a b = ...; I've tried it but I haven't been successful at it, and the error messages aren't very encouraging.
12:01:43 <int-e> Yeah, if you have a constructor of type a -> Foo b in your GADT, then that corresponds to a monadic operation a -> m b.
12:05:40 <int-e> There's a weird existential  data F g x = F (forall a. (g a, a -> x))  type that a GADT g into a functor F g that can be used for making a free monad.
12:06:07 <cpressey> Yeah, I'll need to check out how Free works at some point too I reckon.
12:06:13 <int-e> Which I guess is nicer in theory, but as a programmer, I find the GADT describing an interface very appealing.
12:06:16 <shachaf> Do you mean with forall outside the F?
12:06:27 -!- cpressey has quit (Quit: Lunch).
12:06:33 <int-e> shachaf: Uhm. Yes.
12:06:48 <int-e> I should've used GADT syntax :P
12:07:04 <shachaf> I think that type is pretty natural.
12:07:11 <shachaf> Uh, in the non-formal sense of the word.
12:07:35 <int-e> So, properly: data F g x = forall a. F (g a) (a -> x)
12:07:58 <shachaf> Sure. Or Coyoneda f a = exists x. (f x, x -> a)
12:08:01 <int-e> So, properly: data F g a = forall r. F (g r) (r -> a) -- hmm Cont-style naming seems better.
12:08:27 <shachaf> I tend to call the universal one r (for "return" or "result" or something) and the existential one x.
12:08:36 <shachaf> But for sure the one on the outside should be called a.
12:08:37 <int-e> But nope, I don't find it natural at all.
12:09:02 <int-e> But r is a result type here as well :P
12:09:21 <shachaf> OK, imagine you had a type for which fmap was very expensive, so you wanted to minimize fmaps.
12:09:45 <shachaf> The functor laws tell you that instead of fmap f (fmap g x), you can write fmap (f.g) x
12:09:54 <int-e> Yeah I've seen that.
12:10:03 <shachaf> OK, maybe I'm just saying obvious things here.
12:10:31 <int-e> But it's a far stretch from having seen something, and kind of understanding it, to finding it natural.
12:10:49 <shachaf> An alternative thing you can say is that this thing is the free functor on a type constructor, but I bet that wouldn't strike a chord with you.
12:11:03 <int-e> You're making it worse.
12:11:09 <shachaf> I figured.
12:11:29 <shachaf> You can also use the dual: newtype Yoneda f a = Yoneda (forall r. (a -> r) -> f r)
12:11:56 <shachaf> But I find that one less intuitive, just because CPSy things are more complicated.
12:12:07 <int-e> The way I deal with category theory is to translate it back to something more concrete.
12:12:42 <int-e> The deeper you go into category theory, the more work I have to do translating it back. At some point, I get lost. :P
12:13:00 <shachaf> Well, I'm not saying any category theory words here. Except for "free", I suppose, and "dual", and "Yoneda".
12:13:04 <shachaf> But you can just ignore those.
12:13:16 <shachaf> OK, half of what I'm saying is category theory words.
12:13:36 <int-e> So yes, say CPS instead of Yoneda transform, and I'll be a bit happier.
12:13:55 <shachaf> I'm not calling it a Yoneda transform, I just wanted a name for the type that isn't F.
12:28:28 <int-e> Yeah, I'm mixing up terms.
12:28:54 <int-e> And I'm not even unhappy about it :P
12:30:04 <shachaf> @metar koak
12:30:05 <lambdabot> KOAK 081153Z 28007KT 10SM OVC012 17/12 A2992 RMK AO2 SLP132 T01670122 10167 20161 56004
12:31:12 -!- Arcorann_ has quit (Read error: Connection reset by peer).
13:03:16 -!- cpressey has joined.
13:08:20 <cpressey> <cpressey> Mmmmmmaybe you could put both a and b in the ADT, like data Program instr a b = ...; <-- I think I actually got this to work!
13:11:15 -!- hendursa1 has quit (Quit: hendursa1).
13:11:31 -!- hendursaga has joined.
13:12:05 <cpressey> All the instructions have to "return" the same type.  The type of `singleton` becomes `instr b -> Program instr b b`
13:14:01 -!- Arcorann_ has joined.
13:17:28 <cpressey> This is exciting!  I'm not sure why, but it is.  To me.
13:18:59 -!- adu has joined.
13:20:34 <cpressey> https://gist.github.com/cpressey/2ed6aea0c8eb4fc98a5a56e574807721
13:32:02 <int-e> But now `a` is baked into the type, so this is inflexible.
13:32:47 <int-e> You're pretty close to doing this though: https://paste.debian.net/1166344/
13:33:27 * int-e shrugs
13:35:03 <int-e> But maybe you're coming from the other direction. I have not read very far into the backlog.
13:41:18 <int-e> cpressey: If you want to take the GADTs out of operational, you will probably end up with a free monad anyway. The functor is  data StackF cnt = Push cnt | Pop Int (Int -> cnt)  which can be obtained from unfolding the GADT  data StackG a where Push :: Int -> StackG () | Pop :: StackG Int  into  Coyoneda StackG a.
13:42:52 <int-e> (also using that morally, cnt ~= () -> cnt)
13:44:04 <int-e> But as a programmer, StackF isn't intuitive to me, whereas StackG reads like a signature for a DSL.
13:44:17 <int-e> I really like the GADT version much better.
13:45:35 <int-e> The problem with what you currently have is that there can only ever be a single return type, namely the `a` in Program f a b.
13:45:59 <cpressey> int-e: We have different goals.
14:04:49 -!- Sgeo has joined.
14:22:30 -!- MDude has joined.
14:37:59 <esowiki> [[User:WhyNot?]]  https://esolangs.org/w/index.php?diff=77878&oldid=77854 * WhyNot? * (+84) 
15:18:23 -!- adu has quit (Quit: adu).
15:21:19 -!- Arcorann_ has quit (Read error: Connection reset by peer).
15:40:10 -!- adu has joined.
15:48:36 <esowiki> [[Esolang:Introduce yourself]]  https://esolangs.org/w/index.php?diff=77879&oldid=77874 * Konfetti * (+134) 
15:49:01 <esowiki> [[Talk:RubE On Conveyor Belts/Interpreter]] N https://esolangs.org/w/index.php?oldid=77880 * Eiim * (+685) Added two questions
15:49:40 <esowiki> [[RubE On Conveyor Belts]] M https://esolangs.org/w/index.php?diff=77881&oldid=64380 * Eiim * (+4) noted that interpreter is C++.
15:54:08 <esowiki> [[Talk:RubE On Conveyor Belts/Interpreter]] M https://esolangs.org/w/index.php?diff=77882&oldid=77880 * Eiim * (+267) noted program.out
15:56:30 <esowiki> [[Talk:Hell69]] N https://esolangs.org/w/index.php?oldid=77883 * Konfetti * (+411) Created page with "I think the example is incorrect. 0x41 * 0x69 = 0x1AA9, while 0x41 * 0x45 (which is decimal 69) = 0x1185. I am not sure which version is intended by the creator.  The result i..."
16:00:41 -!- cpressey has quit (Quit: WeeChat 1.9.1).
16:05:58 -!- arseniiv has quit (Ping timeout: 256 seconds).
16:09:36 -!- t20kdc has quit (Remote host closed the connection).
16:09:50 -!- t20kdc has joined.
16:10:56 -!- arseniiv has joined.
16:15:33 -!- rain1 has quit (Quit: Leaving).
16:17:52 -!- rain1 has joined.
16:18:42 -!- adu has quit (Quit: adu).
16:21:29 -!- adu has joined.
16:53:15 <esowiki> [[User:Eiim]] N https://esolangs.org/w/index.php?oldid=77884 * Eiim * (+150) Created User:Eiim
17:05:15 <esowiki> [[!@$%^&*()+/Algorithms]] M https://esolangs.org/w/index.php?diff=77885&oldid=76908 * SunnyMoon * (+313) Added a well-earned snippet!
17:12:41 -!- sprocklem has joined.
17:22:35 -!- LKoen has joined.
17:32:02 -!- LKoen has quit (Remote host closed the connection).
17:53:53 -!- adu has quit (Quit: adu).
17:56:17 -!- int-e has quit (Remote host closed the connection).
18:28:05 -!- LKoen has joined.
18:35:47 -!- arseniiv has quit (Ping timeout: 240 seconds).
18:38:48 -!- int-e has joined.
18:44:43 -!- adu has joined.
18:44:53 -!- deltaepsilon23 has joined.
18:45:11 -!- deltaepsilon23 has quit (Remote host closed the connection).
18:45:45 -!- deltaepsilon23 has joined.
18:46:09 <esowiki> [[User:SunnyMoon]] M https://esolangs.org/w/index.php?diff=77886&oldid=77827 * SunnyMoon * (+350) School update.
18:46:16 -!- deltaepsilon23 has changed nick to delta23.
19:03:50 -!- arseniiv has joined.
19:57:26 -!- int-e has quit (Quit: leaving).
19:57:42 -!- int-e has joined.
20:00:36 -!- imode has joined.
20:05:25 -!- DrSoy has joined.
20:05:33 -!- DrSoy has left.
21:16:53 -!- deltaepsilon23 has joined.
21:18:09 -!- delta23 has quit (Ping timeout: 260 seconds).
21:18:19 -!- deltaepsilon23 has changed nick to delta23.
21:44:14 -!- 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:05:11 -!- adu has quit (Quit: adu).
22:19:47 -!- delta23 has quit (Ping timeout: 240 seconds).
22:25:34 -!- deltaepsilon23 has joined.
22:35:11 -!- deltaepsilon23 has changed nick to delta23.
23:03:08 -!- adu has joined.
23:03:26 -!- adu has quit (Client Quit).
23:51:39 -!- orby has joined.
23:53:18 <orby> I'm trying to construct a specific combinator in Underload, but I'm falling short. Any wizards know how to construct s' where s':(x)(y)(z) -> x(z)(y(z))?
23:53:47 <user3456> Hey look a message! (And sorry I don't know Underload)
23:53:55 <orby> Also, ais523: I've found a 3 command simple translation of Underload.
23:53:58 <orby> Hello!
23:54:00 <user3456> .
23:54:27 <user3456> Sorry accidently pressed my keypad while opening my blinds
23:54:32 <orby> all good
23:54:49 -!- arseniiv has quit (Ping timeout: 264 seconds).
23:57:45 -!- deltaepsilon23 has joined.
23:58:09 -!- delta23 has quit (Disconnected by services).
23:58:15 -!- deltaepsilon23 has changed nick to delta23.