Logs on 2020-12-02 (freenode/#xmonad)
| 19:54:53 | → | ircbrowse_tom joins (~ircbrowse@64.225.78.177) |
| 19:54:53 | Server | sets mode +cnt |
| 19:55:35 | <tomsmeding> | https://ircbrowse.tomsmeding.com/browse/xmonad |
| 19:55:50 | <tomsmeding> | looks like znc's config pages work fine with lynx :) |
| 19:56:09 | <geekosaur> | thank you |
| 19:56:19 | <mc47> | thanks! |
| 20:00:40 | <Solid> | awesome, thank you so much :) |
| 20:03:05 | <tomsmeding> | no problem :) |
| 20:03:18 | <tomsmeding> | Let me ask a question in return: the topic says "... with formally proven extensions" |
| 20:03:46 | <tomsmeding> | is that an exaggeration or is the behaviour/correctness/non-crashyness? of extensions really formally proven? |
| 20:04:24 | <mc47> | Some parts of the core have been formalized in Coq and formally proven |
| 20:04:27 | <mc47> | https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.722.3692&rep=rep1&type=pdf |
| 20:05:02 | <Solid> | I think there are some proofs for some extensions around |
| 20:05:04 | <geekosaur> | and someone did do a subset of the extensions at one point |
| 20:05:07 | <Solid> | but the stackset is certainly the most impressive |
| 20:05:37 | <tomsmeding> | cool! |
| 20:05:38 | <geekosaur> | but only a subset because some require X11 types, whereas the Coq proofs used basic types in their place |
| 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 |
| 20:06:47 | <tomsmeding> | and formally verifying X11 is not something that a sane person wants to do :) |
| 20:06:58 | <geekosaur> | none of this is recent, but xmonad's core in particular doesn't change often |
| 20:07:26 | <tomsmeding> | oh hey that paper is written by someone from the university where I'm studying :) |
| 20:07:43 | <tomsmeding> | in fact had a class from them |
| 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 |
| 20:14:09 | <Solid> | hah |
| 20:14:19 | <Liskni_si> | geekosaur: can you put https://ircbrowse.tomsmeding.com/browse/xmonad in the topic pls? |
| 20:14:37 | <geekosaur> | not sure I have ops here but can try |
| 20:14:45 | <geekosaur> | (not sure anyone has ops here any more) |
| 20:15:21 | <geekosaur> | right, no ops |
| 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 |
| 20:15:52 | <Liskni_si> | (might as well ask him for adding mods to /r/xmonad) |
| 20:17:04 | <geekosaur> | oh, there are newer people with acess, but they keep disappearing too |
| 20:17:52 | <Liskni_si> | maybe byorgey has access? |
| 20:19:04 | <geekosaur> | nope |
| 20:19:21 | <geekosaur> | /msg chanserv access #xmonad list |
| 20:19:22 | <tomsmeding> | the current topic is set by them, however |
| 20:19:38 | <geekosaur> | but I haven't seen any of them in some time |
| 20:23:37 | <Liskni_si> | we can send them an e-mail :-) |
| 20:23:55 | <geekosaur> | gwern's around, I'm asking for help |
| 20:23:57 | → | gwern joins (~gwern@wikipedia/Gwern) |
| 20:24:51 | ChanServ | sets mode +o gwern |
| 20:25:35 | ChanServ | sets mode +o geekosaur |
| 20:26:03 | <geekosaur> | thanks |
| 20:26:48 | gwern | sets mode +o geekosaur |
| 20:27:39 | <gwern> | I assume no one has any objections to geekosaur being added to ops? |
| 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" |
| 20:28:01 | <geekosaur> | everyone thought I already had ops |
| 20:28:28 | <Liskni_si> | ^^ :-) |
| 20:29:07 | geekosaur | sets mode -o geekosaur |
| 20:39:23 | → | doct0rhu joins (~orctarorg@pool-72-88-158-154.nwrknj.fios.verizon.net) |
| 20:52:39 | → | ChubaDuba joins (~ChubaDuba@5.167.119.188) |
| 20:53:26 | → | notis joins (~notis@185.51.134.222) |
| 21:27:09 | × | ChubaDuba quits (~ChubaDuba@5.167.119.188) (Quit: WeeChat 1.6) |
| 21:40:36 | × | geekosaur quits (82659a09@host154-009.vpn.uakron.edu) (Remote host closed the connection) |
| 22:24:22 | × | seschwar quits (~seschwar@unaffiliated/seschwar) (Disconnected by services) |
| 22:24:27 | → | seschwar_ joins (~seschwar@unaffiliated/seschwar) |
| 22:47:56 | × | mc47 quits (~yecinem@89.246.239.190) (Remote host closed the connection) |
| 22:55:14 | → | ddellacosta joins (dd@gateway/vpn/mullvad/ddellacosta) |
| 22:58:11 | SemperUbiSubUbi | is now known as Hash |
| 23:34:35 | × | gazler_ quits (~gazler@2001:8b0:b165:a8d2:1553:5c63:3022:700e) (Remote host closed the connection) |
| 23:34:57 | → | gazler_ joins (~gazler@2001:8b0:b165:a8d2:1553:5c63:3022:700e) |
| 23:37:36 | × | seschwar_ quits (~seschwar@unaffiliated/seschwar) (Ping timeout: 240 seconds) |
All times are in UTC on 2020-12-02.