Note: This channel on freenode is currently not being logged anymore. The logs are reproduced here for posterity.

2020-12-02 20:54:53 +0100ircbrowse_tom(~ircbrowse@64.225.78.177)
2020-12-02 20:54:53 +0100Server+cnt
2020-12-02 20:55:35 +0100 <tomsmeding> https://ircbrowse.tomsmeding.com/browse/xmonad
2020-12-02 20:55:50 +0100 <tomsmeding> looks like znc's config pages work fine with lynx :)
2020-12-02 20:56:09 +0100 <geekosaur> thank you
2020-12-02 20:56:19 +0100 <mc47> thanks!
2020-12-02 21:00:40 +0100 <Solid> awesome, thank you so much :)
2020-12-02 21:03:05 +0100 <tomsmeding> no problem :)
2020-12-02 21:03:18 +0100 <tomsmeding> Let me ask a question in return: the topic says "... with formally proven extensions"
2020-12-02 21:03:46 +0100 <tomsmeding> is that an exaggeration or is the behaviour/correctness/non-crashyness? of extensions really formally proven?
2020-12-02 21:04:24 +0100 <mc47> Some parts of the core have been formalized in Coq and formally proven
2020-12-02 21:04:27 +0100 <mc47> https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.722.3692&rep=rep1&type=pdf
2020-12-02 21:05:02 +0100 <Solid> I think there are some proofs for some extensions around
2020-12-02 21:05:04 +0100 <geekosaur> and someone did do a subset of the extensions at one point
2020-12-02 21:05:07 +0100 <Solid> but the stackset is certainly the most impressive
2020-12-02 21:05:37 +0100 <tomsmeding> cool!
2020-12-02 21:05:38 +0100 <geekosaur> but only a subset because some require X11 types, whereas the Coq proofs used basic types in their place
2020-12-02 21:06:14 +0100 <geekosaur> there's a reason e.g. StackSet has 5 type parameters, it's specifically to support this by letting the X11 types be swapped for things modelable in Coq
2020-12-02 21:06:47 +0100 <tomsmeding> and formally verifying X11 is not something that a sane person wants to do :)
2020-12-02 21:06:58 +0100 <geekosaur> none of this is recent, but xmonad's core in particular doesn't change often
2020-12-02 21:07:26 +0100 <tomsmeding> oh hey that paper is written by someone from the university where I'm studying :)
2020-12-02 21:07:43 +0100 <tomsmeding> in fact had a class from them
2020-12-02 21:08:56 +0100 <mc47> When I mentioned "XMonad have been forrmalized in Coq" in the presentation, the supervisors looked at me funny because they're maintaining/working with Isabelle/HOL
2020-12-02 21:14:09 +0100 <Solid> hah
2020-12-02 21:14:19 +0100 <Liskni_si> geekosaur: can you put https://ircbrowse.tomsmeding.com/browse/xmonad in the topic pls?
2020-12-02 21:14:37 +0100 <geekosaur> not sure I have ops here but can try
2020-12-02 21:14:45 +0100 <geekosaur> (not sure anyone has ops here any more)
2020-12-02 21:15:21 +0100 <geekosaur> right, no ops
2020-12-02 21:15:37 +0100 <Liskni_si> well dons is active on Twitter and last time I asked him about xmonad, he replied quickly that he's still a user so he'd probably be able to transfer access
2020-12-02 21:15:52 +0100 <Liskni_si> (might as well ask him for adding mods to /r/xmonad)
2020-12-02 21:17:04 +0100 <geekosaur> oh, there are newer people with acess, but they keep disappearing too
2020-12-02 21:17:52 +0100 <Liskni_si> maybe byorgey has access?
2020-12-02 21:19:04 +0100 <geekosaur> nope
2020-12-02 21:19:21 +0100 <geekosaur> /msg chanserv access #xmonad list
2020-12-02 21:19:22 +0100 <tomsmeding> the current topic is set by them, however
2020-12-02 21:19:38 +0100 <geekosaur> but I haven't seen any of them in some time
2020-12-02 21:23:37 +0100 <Liskni_si> we can send them an e-mail :-)
2020-12-02 21:23:55 +0100 <geekosaur> gwern's around, I'm asking for help
2020-12-02 21:23:57 +0100gwern(~gwern@wikipedia/Gwern)
2020-12-02 21:24:51 +0100ChanServ+o gwern
2020-12-02 21:25:35 +0100ChanServ+o geekosaur
2020-12-02 21:26:03 +0100 <geekosaur> thanks
2020-12-02 21:26:48 +0100gwern+o geekosaur
2020-12-02 21:27:39 +0100 <gwern> I assume no one has any objections to geekosaur being added to ops?
2020-12-02 21:27:53 +0100 Want to help? http://bit.ly/2nYjqpQ | xmonad: the tiling window manager with formally proven extensions | http://xmonad.org | http://xmonad.org/faq | cheatsheet: http://bit.ly/gz1R4 | https://ircbrowse.tomsmeding.com/browse/xmonad
2020-12-02 21:28:01 +0100 <geekosaur> everyone thought I already had ops
2020-12-02 21:28:28 +0100 <Liskni_si> ^^ :-)
2020-12-02 21:29:07 +0100geekosaur-o geekosaur
2020-12-02 21:39:23 +0100doct0rhu(~orctarorg@pool-72-88-158-154.nwrknj.fios.verizon.net)
2020-12-02 21:52:39 +0100ChubaDuba(~ChubaDuba@5.167.119.188)
2020-12-02 21:53:26 +0100notis(~notis@185.51.134.222)
2020-12-02 22:27:09 +0100ChubaDuba(~ChubaDuba@5.167.119.188) (Quit: WeeChat 1.6)
2020-12-02 22:40:36 +0100geekosaur(82659a09@host154-009.vpn.uakron.edu) (Remote host closed the connection)
2020-12-02 23:24:22 +0100seschwar(~seschwar@unaffiliated/seschwar) (Disconnected by services)
2020-12-02 23:24:27 +0100seschwar_(~seschwar@unaffiliated/seschwar)
2020-12-02 23:47:56 +0100mc47(~yecinem@89.246.239.190) (Remote host closed the connection)
2020-12-02 23:55:14 +0100ddellacosta(dd@gateway/vpn/mullvad/ddellacosta)
2020-12-02 23:58:11 +0100SemperUbiSubUbiHash
2020-12-03 00:34:35 +0100gazler_(~gazler@2001:8b0:b165:a8d2:1553:5c63:3022:700e) (Remote host closed the connection)
2020-12-03 00:34:57 +0100gazler_(~gazler@2001:8b0:b165:a8d2:1553:5c63:3022:700e)
2020-12-03 00:37:36 +0100seschwar_(~seschwar@unaffiliated/seschwar) (Ping timeout: 240 seconds)
2020-12-03 01:08:24 +0100Rockj(~rockj@2001:67c:550:feed::1) (Ping timeout: 240 seconds)
2020-12-03 01:13:45 +0100notis(~notis@185.51.134.222) (Ping timeout: 240 seconds)
2020-12-03 01:24:08 +0100Rockj(~rockj@2001:67c:550:feed::1)
2020-12-03 01:24:32 +0100sagax(~sagax_nb@213.138.71.146) (Quit: Konversation terminated!)
2020-12-03 01:36:46 +0100thc202(~thc202@unaffiliated/thc202) (Ping timeout: 244 seconds)
2020-12-03 01:49:07 +0100rabliatu(~quassel@107.158.96.163)
2020-12-03 02:18:22 +0100SpiderPig(~matt@047-132-233-190.res.spectrum.com) (Ping timeout: 246 seconds)
2020-12-03 02:24:54 +0100SpiderPig(~matt@047-132-233-190.res.spectrum.com)
2020-12-03 03:08:49 +0100fionnan(~fionnan@109.255.20.201)
2020-12-03 03:19:26 +0100james(~james@d75-159-1-216.abhsia.telus.net)
2020-12-03 03:19:45 +0100jamesGuest3622
2020-12-03 03:21:06 +0100jamik(~james@d75-159-1-216.abhsia.telus.net)
2020-12-03 03:21:24 +0100Guest3622(~james@d75-159-1-216.abhsia.telus.net) (Remote host closed the connection)
2020-12-03 03:21:25 +0100jamik(~james@d75-159-1-216.abhsia.telus.net) (Remote host closed the connection)
2020-12-03 03:21:55 +0100jamik(~james@d75-159-1-216.abhsia.telus.net)
2020-12-03 03:25:39 +0100 <jamik> Hey guys I'd love to switch to xmonad but I want to keep my keybindings separate (via a hotkey daemon such as sxhkd). I'm wondering if anybody does this with xmonad and if they have run into any troubles
2020-12-03 03:26:42 +0100 <jamik> I'd also like some basic IPC to control xmonad from other processes. I haven't looked into it enough to know if that's an easy thing to do yet
2020-12-03 03:48:44 +0100 <fizzie> There's https://hackage.haskell.org/package/xmonad-contrib-0.16/docs/XMonad-Hooks-ServerMode.html for that kind of thing -- runs by sending X client events.
2020-12-03 03:49:34 +0100 <fizzie> (And https://hackage.haskell.org/package/xmonad-contrib-0.16/docs/XMonad-Hooks-EwmhDesktops.html allows for some forms of control in terms of desktop switching and window movement, through tools that manipulate the standard EWMH hints.)
2020-12-03 03:50:50 +0100 <jamik> Ah amazing! I thought someone had probably done something along these lines, thanks fizzie :)
2020-12-03 03:52:08 +0100 <fizzie> As for not having XMonad be responsible for keybindings, can't really comment on that, other than I'd expect it to work insofar as XMonad only grabs those keys you configure it to grab. But most of the xmonad-contrib ecosystem will probably expect you to invoke it via XMonad keybindings (when it's the sort of thing that needs keybindings in the first place).
2020-12-03 03:53:19 +0100 <jamik> Yeah I'm looking at these links to see if I can offload bindings to be interpretted by a servermode hook
2020-12-03 03:53:54 +0100 <jamik> It may not be worth the effort but I'm curious about it regardless
2020-12-03 03:58:48 +0100 <fizzie> In the end, the ServerMode event hook ends up running an arbitrary `X ()`, just like a keybinding would, so I think it's likely to mostly work. Where I guess you might run into some issues are "interactive" features like XMonad.Actions.GridSelect. Though that does its own temporary keyboard/pointer grab, so maybe even that would work; and maybe you don't care about that anyway.
2020-12-03 03:59:59 +0100 <jamik> Luckily my usage is very minimal so I won't have to worry about too many fancy features or contrib packages
2020-12-03 04:00:00 +0100 <fizzie> Just feels generally a little odd thing to do on first glance. But it's a free, uh... program. (Wanted to say something more punny like "it's a free monad", but that sounds a bit too much like it could be a real thing.)
2020-12-03 04:01:00 +0100 <fizzie> (Apparently a free monad is just "a free object relative to a forgetful functor whose domain is a category of monads", according to the internet.)
2020-12-03 04:04:07 +0100 <jamik> Yeah it is odd haha. And it's not really portable even if I keep the separation of bindings because the WM-related bindings would still have to invoke a xmonad servermode hook rather than a general operation
2020-12-03 04:27:53 +0100Temer(bd7ab158@189.122.177.88)
2020-12-03 04:36:05 +0100theDon(~td@94.134.91.130) (Ping timeout: 240 seconds)
2020-12-03 04:38:20 +0100theDon(~td@muedsl-82-207-238-021.citykom.de)
2020-12-03 04:41:09 +0100materiyolo(~materiyol@112.204.171.225)
2020-12-03 04:51:16 +0100materiyolo(~materiyol@112.204.171.225) (Read error: Connection reset by peer)
2020-12-03 04:58:11 +0100jamik(~james@d75-159-1-216.abhsia.telus.net) (Remote host closed the connection)
2020-12-03 05:00:02 +0100haasn(~nand@mpv/developer/haasn) (Quit: ZNC 1.7.5+deb4 - https://znc.in)
2020-12-03 05:01:22 +0100haasn(~nand@mpv/developer/haasn)
2020-12-03 05:02:48 +0100novas0x2a(~blah@157-131-125-210.fiber.dynamic.sonic.net) (Quit: Leaving.)
2020-12-03 05:03:34 +0100novas0x2a(~blah@157-131-125-210.fiber.dynamic.sonic.net)
2020-12-03 05:50:05 +0100ddellacosta(dd@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 256 seconds)