| 2020-12-02 20:54:53 +0100 | ircbrowse_tom | (~ircbrowse@64.225.78.177) |
| 2020-12-02 20:54:53 +0100 | Server | +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 +0100 | gwern | (~gwern@wikipedia/Gwern) |
| 2020-12-02 21:24:51 +0100 | ChanServ | +o gwern |
| 2020-12-02 21:25:35 +0100 | ChanServ | +o geekosaur |
| 2020-12-02 21:26:03 +0100 | <geekosaur> | thanks |
| 2020-12-02 21:26:48 +0100 | gwern | +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 +0100 | geekosaur | -o geekosaur |
| 2020-12-02 21:39:23 +0100 | doct0rhu | (~orctarorg@pool-72-88-158-154.nwrknj.fios.verizon.net) |
| 2020-12-02 21:52:39 +0100 | ChubaDuba | (~ChubaDuba@5.167.119.188) |
| 2020-12-02 21:53:26 +0100 | notis | (~notis@185.51.134.222) |
| 2020-12-02 22:27:09 +0100 | ChubaDuba | (~ChubaDuba@5.167.119.188) (Quit: WeeChat 1.6) |
| 2020-12-02 22:40:36 +0100 | geekosaur | (82659a09@host154-009.vpn.uakron.edu) (Remote host closed the connection) |
| 2020-12-02 23:24:22 +0100 | seschwar | (~seschwar@unaffiliated/seschwar) (Disconnected by services) |
| 2020-12-02 23:24:27 +0100 | seschwar_ | (~seschwar@unaffiliated/seschwar) |
| 2020-12-02 23:47:56 +0100 | mc47 | (~yecinem@89.246.239.190) (Remote host closed the connection) |
| 2020-12-02 23:55:14 +0100 | ddellacosta | (dd@gateway/vpn/mullvad/ddellacosta) |
| 2020-12-02 23:58:11 +0100 | SemperUbiSubUbi | Hash |