!tFtYbvsVJEdYRVIIrQ:matrix.org

Agda Club

26 Members
Welcome to Oxford's Agda Club | Next meeting: Wed 6th May 16:00 GMT+1 | Protips: set notifications to "Mentions only" to reduce spam; use Riot in your web browser, or download RiotX on your phone1 Servers

Load older messages


SenderMessageTime
21 Aug 2020
@nickhu:matrix.orgNick 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 recently12:25:55
@nickhu:matrix.orgNick HuIdeally, each university/CS department should have their own homeserver - I've been trying to set ours up in Oxford12:26:29
@nickhu:matrix.orgNick HuI feel that discourse (and forums in general) is a different medium to webchat, and we actually have a discourse instance too at discourse.agda.club12:27:32
@nickhu:matrix.orgNick HuSlack 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 dollars12:30:18
@nickhu:matrix.orgNick HuZulip 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 abandoned12:31:25
@nickhu:matrix.orgNick HuIn 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
@nickhu:matrix.orgNick HuMozilla 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:34:37
@nickhu:matrix.orgNick 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
@jcockx:matrix.orgJesper CockxThanks, that's very useful information! I was currently favouring Zulip but I do like the whole concept of Matrix a lot.12:36:24
@jcockx:matrix.orgJesper CockxMind 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
@nickhu:matrix.orgNick HuNot at all, please feel free12:38:37
@nickhu:matrix.orgNick Hu

Matrix supports markdown with syntax highlighting, so you can write things like

main :: IO ()
main = undefined
12:39:48
@nickhu:matrix.orgNick 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:matrix.orgyotamdvir joined the room.12:53:07
@jorge-jbs:matrix.orgJorge Blázquez Saborido joined the room.13:04:06
14 Sep 2020
@nickhu:matrix.orgNick HuHi 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 think10:39:35
Jitsi widget removed by @nickhu:matrix.orgNick Hu10:39:41
17 Sep 2020
@jgarte:matrix.orgjgart joined the room.09:56:28
18 Sep 2020
@jgarte:matrix.orgjgartcomplete 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:matrix.orgcnmne joined the room.01:14:07
@cnmne:matrix.orgcnmne jgart: am also noob; I've had good success with plfa: https://plfa.github.io/ 12:08:00
3 Jan 2021
@n0v4:matrix.orgn0v4 joined the room.15:03:52
@n0v4:matrix.orgn0v4having 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 you16:33:43
@n0v4:matrix.orgn0v4sorry, the error is "Failed to find source of module IO in any of the following locations" followed by those locations16:34:55
@n0v4:matrix.orgn0v4(actually i'm on ubuntu 20.10)16:35:45
@jgarte:matrix.orgjgart I want to use agda with vis. What would I need to make the experience pleasant? 23:04:57
20 Jan 2021
@jgarte:matrix.orgjgart changed their display name from jgart to jgarte.06:16:23
21 Jan 2021
@jgarte:matrix.orgjgart changed their display name from jgarte to jgart.20:29:09
10 Feb 2021
@plumenator:matrix.orgplumenator joined the room.13:22:40
16 Feb 2021
@plumenator:matrix.orgplumenatorIs 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

There are no newer messages yet.


Back to Room List