Logs: freenode/#xmonad
| 2020-12-02 19:54:53 | → | ircbrowse_tom joins (~ircbrowse@64.225.78.177) |
| 2020-12-02 19:54:53 | Server | sets mode +cnt |
| 2020-12-02 19:55:35 | <tomsmeding> | https://ircbrowse.tomsmeding.com/browse/xmonad |
| 2020-12-02 19:55:50 | <tomsmeding> | looks like znc's config pages work fine with lynx :) |
| 2020-12-02 19:56:09 | <geekosaur> | thank you |
| 2020-12-02 19:56:19 | <mc47> | thanks! |
| 2020-12-02 20:00:40 | <Solid> | awesome, thank you so much :) |
| 2020-12-02 20:03:05 | <tomsmeding> | no problem :) |
| 2020-12-02 20:03:18 | <tomsmeding> | Let me ask a question in return: the topic says "... with formally proven extensions" |
| 2020-12-02 20:03:46 | <tomsmeding> | is that an exaggeration or is the behaviour/correctness/non-crashyness? of extensions really formally proven? |
| 2020-12-02 20:04:24 | <mc47> | Some parts of the core have been formalized in Coq and formally proven |
| 2020-12-02 20:04:27 | <mc47> | https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.722.3692&rep=rep1&type=pdf |
| 2020-12-02 20:05:02 | <Solid> | I think there are some proofs for some extensions around |
| 2020-12-02 20:05:04 | <geekosaur> | and someone did do a subset of the extensions at one point |
| 2020-12-02 20:05:07 | <Solid> | but the stackset is certainly the most impressive |
| 2020-12-02 20:05:37 | <tomsmeding> | cool! |
| 2020-12-02 20:05:38 | <geekosaur> | but only a subset because some require X11 types, whereas the Coq proofs used basic types in their place |
| 2020-12-02 20:06:14 | <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 20:06:47 | <tomsmeding> | and formally verifying X11 is not something that a sane person wants to do :) |
| 2020-12-02 20:06:58 | <geekosaur> | none of this is recent, but xmonad's core in particular doesn't change often |
| 2020-12-02 20:07:26 | <tomsmeding> | oh hey that paper is written by someone from the university where I'm studying :) |
| 2020-12-02 20:07:43 | <tomsmeding> | in fact had a class from them |
| 2020-12-02 20:08:56 | <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 20:14:09 | <Solid> | hah |
| 2020-12-02 20:14:19 | <Liskni_si> | geekosaur: can you put https://ircbrowse.tomsmeding.com/browse/xmonad in the topic pls? |
| 2020-12-02 20:14:37 | <geekosaur> | not sure I have ops here but can try |
| 2020-12-02 20:14:45 | <geekosaur> | (not sure anyone has ops here any more) |
| 2020-12-02 20:15:21 | <geekosaur> | right, no ops |
| 2020-12-02 20:15:37 | <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 20:15:52 | <Liskni_si> | (might as well ask him for adding mods to /r/xmonad) |
| 2020-12-02 20:17:04 | <geekosaur> | oh, there are newer people with acess, but they keep disappearing too |
| 2020-12-02 20:17:52 | <Liskni_si> | maybe byorgey has access? |
| 2020-12-02 20:19:04 | <geekosaur> | nope |
| 2020-12-02 20:19:21 | <geekosaur> | /msg chanserv access #xmonad list |
| 2020-12-02 20:19:22 | <tomsmeding> | the current topic is set by them, however |
| 2020-12-02 20:19:38 | <geekosaur> | but I haven't seen any of them in some time |
| 2020-12-02 20:23:37 | <Liskni_si> | we can send them an e-mail :-) |
| 2020-12-02 20:23:55 | <geekosaur> | gwern's around, I'm asking for help |
| 2020-12-02 20:23:57 | → | gwern joins (~gwern@wikipedia/Gwern) |
| 2020-12-02 20:24:51 | ChanServ | sets mode +o gwern |
| 2020-12-02 20:25:35 | ChanServ | sets mode +o geekosaur |
| 2020-12-02 20:26:03 | <geekosaur> | thanks |
| 2020-12-02 20:26:48 | gwern | sets mode +o geekosaur |
| 2020-12-02 20:27:39 | <gwern> | I assume no one has any objections to geekosaur being added to ops? |
| 2020-12-02 20:27:53 | geekosaur | sets topic to "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 20:28:01 | <geekosaur> | everyone thought I already had ops |
| 2020-12-02 20:28:28 | <Liskni_si> | ^^ :-) |
| 2020-12-02 20:29:07 | geekosaur | sets mode -o geekosaur |
| 2020-12-02 20:39:23 | → | doct0rhu joins (~orctarorg@pool-72-88-158-154.nwrknj.fios.verizon.net) |
| 2020-12-02 20:52:39 | → | ChubaDuba joins (~ChubaDuba@5.167.119.188) |
| 2020-12-02 20:53:26 | → | notis joins (~notis@185.51.134.222) |
| 2020-12-02 21:27:09 | × | ChubaDuba quits (~ChubaDuba@5.167.119.188) (Quit: WeeChat 1.6) |
| 2020-12-02 21:40:36 | × | geekosaur quits (82659a09@host154-009.vpn.uakron.edu) (Remote host closed the connection) |
| 2020-12-02 22:24:22 | × | seschwar quits (~seschwar@unaffiliated/seschwar) (Disconnected by services) |
| 2020-12-02 22:24:27 | → | seschwar_ joins (~seschwar@unaffiliated/seschwar) |
| 2020-12-02 22:47:56 | × | mc47 quits (~yecinem@89.246.239.190) (Remote host closed the connection) |
| 2020-12-02 22:55:14 | → | ddellacosta joins (dd@gateway/vpn/mullvad/ddellacosta) |
| 2020-12-02 22:58:11 | SemperUbiSubUbi | is now known as Hash |
| 2020-12-02 23:34:35 | × | gazler_ quits (~gazler@2001:8b0:b165:a8d2:1553:5c63:3022:700e) (Remote host closed the connection) |
| 2020-12-02 23:34:57 | → | gazler_ joins (~gazler@2001:8b0:b165:a8d2:1553:5c63:3022:700e) |
| 2020-12-02 23:37:36 | × | seschwar_ quits (~seschwar@unaffiliated/seschwar) (Ping timeout: 240 seconds) |
| 2020-12-03 00:08:24 | × | Rockj quits (~rockj@2001:67c:550:feed::1) (Ping timeout: 240 seconds) |
| 2020-12-03 00:13:45 | × | notis quits (~notis@185.51.134.222) (Ping timeout: 240 seconds) |
| 2020-12-03 00:24:08 | → | Rockj joins (~rockj@2001:67c:550:feed::1) |
| 2020-12-03 00:24:32 | × | sagax quits (~sagax_nb@213.138.71.146) (Quit: Konversation terminated!) |
| 2020-12-03 00:36:46 | × | thc202 quits (~thc202@unaffiliated/thc202) (Ping timeout: 244 seconds) |
| 2020-12-03 00:49:07 | → | rabliatu joins (~quassel@107.158.96.163) |
| 2020-12-03 01:18:22 | × | SpiderPig quits (~matt@047-132-233-190.res.spectrum.com) (Ping timeout: 246 seconds) |
| 2020-12-03 01:24:54 | → | SpiderPig joins (~matt@047-132-233-190.res.spectrum.com) |
| 2020-12-03 02:08:49 | → | fionnan joins (~fionnan@109.255.20.201) |
| 2020-12-03 02:19:26 | → | james joins (~james@d75-159-1-216.abhsia.telus.net) |
| 2020-12-03 02:19:45 | james | is now known as Guest3622 |
| 2020-12-03 02:21:06 | → | jamik joins (~james@d75-159-1-216.abhsia.telus.net) |
| 2020-12-03 02:21:24 | × | Guest3622 quits (~james@d75-159-1-216.abhsia.telus.net) (Remote host closed the connection) |
| 2020-12-03 02:21:25 | × | jamik quits (~james@d75-159-1-216.abhsia.telus.net) (Remote host closed the connection) |
| 2020-12-03 02:21:55 | → | jamik joins (~james@d75-159-1-216.abhsia.telus.net) |
| 2020-12-03 02:25:39 | <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 02:26:42 | <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 02:48:44 | <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 02:49:34 | <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 02:50:50 | <jamik> | Ah amazing! I thought someone had probably done something along these lines, thanks fizzie :) |
| 2020-12-03 02:52:08 | <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 02:53:19 | <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 02:53:54 | <jamik> | It may not be worth the effort but I'm curious about it regardless |
| 2020-12-03 02:58:48 | <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 02:59:59 | <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 03:00:00 | <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 03:01:00 | <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 03:04:07 | <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 03:27:53 | → | Temer joins (bd7ab158@189.122.177.88) |
| 2020-12-03 03:36:05 | × | theDon quits (~td@94.134.91.130) (Ping timeout: 240 seconds) |
| 2020-12-03 03:38:20 | → | theDon joins (~td@muedsl-82-207-238-021.citykom.de) |
| 2020-12-03 03:41:09 | → | materiyolo joins (~materiyol@112.204.171.225) |
| 2020-12-03 03:51:16 | × | materiyolo quits (~materiyol@112.204.171.225) (Read error: Connection reset by peer) |
| 2020-12-03 03:58:11 | × | jamik quits (~james@d75-159-1-216.abhsia.telus.net) (Remote host closed the connection) |
| 2020-12-03 04:00:02 | × | haasn quits (~nand@mpv/developer/haasn) (Quit: ZNC 1.7.5+deb4 - https://znc.in) |
| 2020-12-03 04:01:22 | → | haasn joins (~nand@mpv/developer/haasn) |
| 2020-12-03 04:02:48 | × | novas0x2a quits (~blah@157-131-125-210.fiber.dynamic.sonic.net) (Quit: Leaving.) |
| 2020-12-03 04:03:34 | → | novas0x2a joins (~blah@157-131-125-210.fiber.dynamic.sonic.net) |
| 2020-12-03 04:50:05 | × | ddellacosta quits (dd@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 256 seconds) |
All times are in UTC.