| 21 Aug 2020 |
 Nick Hu | * The biggest issue with Matrix is when people (like us unfortunately) use the matrix.org homeserver, which is severely over capacity (https://t2bot.io/docs/2020-matrix-org-lag/). This causes events, e.g. push notifications and messages, to sometimes be severely delayed, although I haven't noticed this super recently | 12:25:55 |
| Nick Hu | Ideally, each university/CS department should have their own homeserver - I've been trying to set ours up in Oxford | 12:26:29 |
| Nick Hu | I feel that discourse (and forums in general) is a different medium to webchat, and we actually have a discourse instance too at discourse.agda.club | 12:27:32 |
| Nick Hu | Slack has this weird user limit and privacy issues because you have to let them host it, and I don't think it offers any tangible benefit over Matrix - it doesn't do anything particularly novel, and as far as I can tell it's just IRC made proprietary and marketed for millions of dollars | 12:30:18 |
| Nick Hu | Zulip is the same as slack except you have the "killer feature" of threads - to me, it seems like at any moment slack could implement this and then zulip will be abandoned | 12:31:25 |
| Nick Hu | In particular I'm excited for element to adopt LaTeX support (https://github.com/matrix-org/matrix-react-sdk/pull/3251), which is on the roadmap and should happen soon(TM) | 12:32:47 |
| Nick Hu | Mozilla and the French government have adopted Matrix, so hopefully that's convincing enough to show you it's not so niche! | 12:34:37 |
| Nick Hu | * Mozilla and the French government have adopted Matrix, so hopefully that's convincing enough to show you it's not so niche! (Although polish is undoubtedly desired, we'll get there..) | 12:35:03 |
 Jesper Cockx | Thanks, that's very useful information! I was currently favouring Zulip but I do like the whole concept of Matrix a lot. | 12:36:24 |
| Jesper Cockx | Mind if I share your messages on the Agda mailing list? I'm trying to push for an "official" chat channel that we can link to from the website and use during online agda meetings. | 12:38:13 |
| Nick Hu | Not at all, please feel free | 12:38:37 |
| Nick Hu | Matrix supports markdown with syntax highlighting, so you can write things like
main :: IO ()
main = undefined
| 12:39:48 |
| Nick Hu | It uses highlight.js for this, so if someone were to write a highlight.js plugin for Agda then that might be nice 😉 | 12:40:39 |
|  yotamdvir joined the room. | 12:53:07 |
|  Sr. Bonobo joined the room. | 13:04:06 |
| 14 Sep 2020 |
| Nick Hu | Hi everyone, I set up an instance of matrix in our CS department linked with SSO: https://chat.cs.ox.ac.uk - if anyone is interested, please check it out and tell me what you think | 10:39:35 |
| Jitsi widget removed by Nick Hu | 10:39:41 |
| 17 Sep 2020 |
|  @jgarte:matrix.org joined the room. | 09:56:28 |
| 18 Sep 2020 |
| @jgarte:matrix.org | complete proof noob here. Any resources any one can suggest that could help a beginner get started learning agda? | 08:24:02 |
| 15 Dec 2020 |
|  cnmne joined the room. | 01:14:07 |
| cnmne | jgart: am also noob; I've had good success with plfa: https://plfa.github.io/ | 12:08:00 |
| 3 Jan 2021 |
|  n0v4 joined the room. | 15:03:52 |
| n0v4 | having a lot of trouble trying to get Agda to install on ubuntu 20.04. i've tried installing by following the instructions to install with cabal https://agda.readthedocs.io/en/v2.6.1.1/getting-started/installation.html, as well here: https://github.com/pigworker/CS410-18, as well as with "sudo apt install agda" .
In each case i get the following error when trying to compile the 'hello world' program in the docs:
" /home/n0v4/Dropbox/git/agda/IO.agda
/home/n0v4/Dropbox/git/agda/IO.lagda
/home/n0v4/.cabal/store/ghc-8.8.3/Agda-2.6.1.2-b558f1520aa5233a08833ff00fd81875c214adbcbf9fe3c1b91673ebd02fba4e/share/lib/prim/IO.agda
/home/n0v4/.cabal/store/ghc-8.8.3/Agda-2.6.1.2-b558f1520aa5233a08833ff00fd81875c214adbcbf9fe3c1b91673ebd02fba4e/share/lib/prim/IO.lagda
when scope checking the declaration
"
although i can find two copies of this file at:
/usr/share/agda-stdlib/IO.agda
/usr/share/libghc-agda-dev/lib/prim/Agda/Builtin/IO.agda
.i have even reinstalled a fresh copy of ubuntu and tried again and it does not work. i would really appreciate any tips on how to get agda to work. thank you | 16:33:43 |
| n0v4 | sorry, the error is "Failed to find source of module IO in any of the following
locations" followed by those locations | 16:34:55 |
| n0v4 | (actually i'm on ubuntu 20.10) | 16:35:45 |
| @jgarte:matrix.org | I want to use agda with vis. What would I need to make the experience pleasant? | 23:04:57 |
| 20 Jan 2021 |
| @jgarte:matrix.org changed their display name from jgart to jgarte. | 06:16:23 |
| 21 Jan 2021 |
| @jgarte:matrix.org changed their display name from jgarte to jgart. | 20:29:09 |
| 10 Feb 2021 |
|  plumenator joined the room. | 13:22:40 |
| 16 Feb 2021 |
| plumenator | Is it okay to ask questions about the PLFA exercises here?
My particular question is not about how to solve one, but about why my solution works. I might have to ask questions about future exercises tho. I'm already finding it much harder than before to solve the exercises in Negation. | 10:03:46 |
