Logs: liberachat/#haskell
| 2021-07-03 03:13:08 | × | Erutuon quits (~Erutuon@user/erutuon) (Ping timeout: 252 seconds) |
| 2021-07-03 03:15:06 | → | Erutuon joins (~Erutuon@user/erutuon) |
| 2021-07-03 03:20:13 | × | finsternis quits (~X@23.226.237.192) (Remote host closed the connection) |
| 2021-07-03 03:24:08 | → | funsafe joins (~funsafe@2601:1c1:4200:938f:32aa:eb39:2110:e2ea) |
| 2021-07-03 03:27:04 | × | boxscape_ quits (~boxscape_@p4ff0ba7a.dip0.t-ipconnect.de) (Quit: Connection closed) |
| 2021-07-03 03:31:15 | × | machinedgod quits (~machinedg@24.105.81.50) (Ping timeout: 265 seconds) |
| 2021-07-03 03:31:41 | → | pfurla_ joins (~pfurla@216.131.83.59) |
| 2021-07-03 03:34:52 | × | pfurla quits (~pfurla@ool-182ed2e2.dyn.optonline.net) (Ping timeout: 272 seconds) |
| 2021-07-03 03:42:50 | → | stevenxl joins (~stevenlei@68.235.43.109) |
| 2021-07-03 03:45:56 | → | dyeplexer joins (~dyeplexer@user/dyeplexer) |
| 2021-07-03 03:47:41 | × | stevenxl quits (~stevenlei@68.235.43.109) (Ping timeout: 265 seconds) |
| 2021-07-03 03:52:51 | → | rachel231 joins (~rachel231@c-73-142-199-151.hsd1.nh.comcast.net) |
| 2021-07-03 03:53:16 | <rachel231> | Is there a way to get the right side of an either or throw an error if it's left? |
| 2021-07-03 03:53:27 | <rachel231> | like rust's .unwrap() |
| 2021-07-03 03:54:03 | <rachel231> | or like the either version of fromJust |
| 2021-07-03 03:54:55 | <davean> | either? |
| 2021-07-03 03:55:28 | <davean> | or fromRight? |
| 2021-07-03 03:55:31 | <davean> | Depending on what you want |
| 2021-07-03 03:58:00 | <sm[m]> | rachel231: yeah: either (error.fooShow) fooDoSomething efoo |
| 2021-07-03 03:58:00 | <sm[m]> | is pretty common |
| 2021-07-03 03:59:18 | <rachel231> | oooh tysm |
| 2021-07-03 03:59:59 | × | TranquilEcho quits (~grom@user/tranquilecho) (Quit: WeeChat 2.8) |
| 2021-07-03 04:00:00 | × | jolly quits (~jolly@208.180.97.158) (Quit: Connection closed) |
| 2021-07-03 04:01:50 | × | P1RATEZ quits (piratez@user/p1ratez) (Remote host closed the connection) |
| 2021-07-03 04:04:15 | → | nate1 joins (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 04:04:56 | → | fef joins (~thedawn@user/thedawn) |
| 2021-07-03 04:07:16 | → | edrx joins (~Eduardo@2804:56c:d2e2:8b00:8d96:adf9:cdb8:eb7e) |
| 2021-07-03 04:10:12 | <dsal> | :t either (fail . show) |
| 2021-07-03 04:10:13 | <lambdabot> | (MonadFail m, Show a1) => (b -> m a2) -> Either a1 b -> m a2 |
| 2021-07-03 04:10:32 | × | haykam1 quits (~haykam@static.100.2.21.65.clients.your-server.de) (Remote host closed the connection) |
| 2021-07-03 04:10:44 | → | haykam1 joins (~haykam@static.100.2.21.65.clients.your-server.de) |
| 2021-07-03 04:11:33 | → | warnz joins (~warnz@2600:1700:77c0:5610:20b2:48fc:c4b7:f8df) |
| 2021-07-03 04:15:30 | × | warnz quits (~warnz@2600:1700:77c0:5610:20b2:48fc:c4b7:f8df) (Ping timeout: 240 seconds) |
| 2021-07-03 04:16:54 | → | AgentM joins (~agentm@pool-162-83-130-212.nycmny.fios.verizon.net) |
| 2021-07-03 04:18:05 | <edrx> | is this the right place to ask questions about cabal? I'm on a Debian box that has both agda and agda-mode from Debian - known to be broken - and an Agda that I've installed from Cabal... I even had to find a compilation bug and report it, here: https://lists.chalmers.se/pipermail/agda/2021/012689.html |
| 2021-07-03 04:19:54 | <edrx> | I am now trying to understand how cabal handle its paths. 1) is there a better way to specify the path to agda-mode than "~/.cabal/store/ghc-8.8.4/Agda-2.6.2-b2f8eb43cd09b8b95a6e2958c006bc2f47b9966435e6f21d09b053b958e4fc43/share/emacs-mode/"? |
| 2021-07-03 04:20:55 | × | rachel231 quits (~rachel231@c-73-142-199-151.hsd1.nh.comcast.net) (Quit: Connection closed) |
| 2021-07-03 04:21:44 | <edrx> | 2) when I used the Agda from Debian I had to call it like this: "agda -i. -i/usr/share/agda-stdlib test1.agda". It seems that now the path to agda-stdlib should be replaced by something that points to the agda-stdlib from cabal, that haven't even been able to locate in ~/.cabal/... |
| 2021-07-03 04:22:19 | <edrx> | any recommended pointers? I am very newbie-ish on those things - like Haskell, Cabal, and Agda... |
| 2021-07-03 04:22:53 | <edrx> | apologies for asking here, but in #agda people usually take 12 to 24 hours to answer =/ |
| 2021-07-03 04:28:05 | <sclv> | you can ‘cabal unpack agda’ to get access to its static files directly |
| 2021-07-03 04:28:17 | <sclv> | if you don’t like the weird place cabal installs em too |
| 2021-07-03 04:29:46 | → | dunkeln_ joins (~dunkeln@94.129.65.28) |
| 2021-07-03 04:32:26 | <edrx> | trying! |
| 2021-07-03 04:34:37 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-07-03 04:35:47 | × | myShoggoth quits (~myShoggot@75.164.51.64) (Ping timeout: 268 seconds) |
| 2021-07-03 04:36:01 | × | shapr quits (~user@pool-100-36-247-68.washdc.fios.verizon.net) (Ping timeout: 265 seconds) |
| 2021-07-03 04:36:12 | → | myShoggoth joins (~myShoggot@75.164.51.64) |
| 2021-07-03 04:37:40 | → | nerdypepper joins (~nerdypepp@user/nerdypepper) |
| 2021-07-03 04:43:19 | <guest61> | wait, cabal can manage agda? |
| 2021-07-03 04:43:48 | × | cheater quits (~Username@user/cheater) (Ping timeout: 258 seconds) |
| 2021-07-03 04:44:07 | <edrx> | guest61: it seems so |
| 2021-07-03 04:44:09 | → | cheater joins (~Username@user/cheater) |
| 2021-07-03 04:45:55 | <edrx> | guest61: look here: https://readthedocs.org/projects/agda/downloads/pdf/latest/#page=12 |
| 2021-07-03 04:50:34 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 04:54:40 | × | cheater quits (~Username@user/cheater) (Ping timeout: 272 seconds) |
| 2021-07-03 04:54:41 | → | cheater1__ joins (~Username@user/cheater) |
| 2021-07-03 04:54:43 | cheater1__ | is now known as cheater |
| 2021-07-03 04:55:07 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 2021-07-03 04:57:30 | × | berberman_ quits (~berberman@user/berberman) (Ping timeout: 240 seconds) |
| 2021-07-03 04:58:03 | → | berberman joins (~berberman@user/berberman) |
| 2021-07-03 05:00:23 | → | qbt joins (~edun@user/edun) |
| 2021-07-03 05:01:41 | × | AgentM quits (~agentm@pool-162-83-130-212.nycmny.fios.verizon.net) (Quit: Leaving.) |
| 2021-07-03 05:03:02 | → | favonia joins (~favonia@user/favonia) |
| 2021-07-03 05:09:06 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 258 seconds) |
| 2021-07-03 05:10:58 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 05:12:33 | × | nate1 quits (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 258 seconds) |
| 2021-07-03 05:17:28 | → | favonia joins (~favonia@user/favonia) |
| 2021-07-03 05:22:01 | <edrx> | guest61: I am trying to comple the Hello World program now... did not work, but I reported the reason here: https://github.com/agda/agda/issues/5466 |
| 2021-07-03 05:25:32 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 2021-07-03 05:29:22 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 2021-07-03 05:30:49 | <edrx> | sclv: btw, "cabal unpack agda" worked great, thanks! |
| 2021-07-03 05:30:56 | → | stevenxl joins (~stevenlei@68.235.43.109) |
| 2021-07-03 05:32:29 | × | favonia quits (~favonia@user/favonia) (Ping timeout: 256 seconds) |
| 2021-07-03 05:32:55 | → | favonia joins (~favonia@user/favonia) |
| 2021-07-03 05:33:43 | <tomsmeding> | edrx: the 3rd path of the first listing is equal to the 2nd path of the second listing? |
| 2021-07-03 05:34:01 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 265 seconds) |
| 2021-07-03 05:34:08 | <tomsmeding> | oh I misunderstood, you have the file in the first path |
| 2021-07-03 05:35:24 | × | stevenxl quits (~stevenlei@68.235.43.109) (Ping timeout: 252 seconds) |
| 2021-07-03 05:35:50 | <tomsmeding> | looks like the rest of the documentation instructs to use "open import Agda.Builtin.IO", which makes sense given the paths |
| 2021-07-03 05:36:09 | <edrx> | oh, let me try that |
| 2021-07-03 05:36:11 | <tomsmeding> | e.g. section 2.3.2 |
| 2021-07-03 05:36:34 | <tomsmeding> | not sure why 2.4.4 has the different module name; looks like a documentation bug in 2.4.4 to me |
| 2021-07-03 05:36:57 | <tomsmeding> | also only hit of "open import io" :D |
| 2021-07-03 05:37:51 | <edrx> | I got another error: |
| 2021-07-03 05:37:52 | → | nate1 joins (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-03 05:37:53 | <edrx> | Not in scope: |
| 2021-07-03 05:37:53 | <edrx> | run at /home/edrx/AGDA/test1.agda:8,8-11 |
| 2021-07-03 05:37:53 | <edrx> | when scope checking run |
| 2021-07-03 05:39:04 | <tomsmeding> | ooooh I got your problem |
| 2021-07-03 05:39:18 | × | dunkeln_ quits (~dunkeln@94.129.65.28) (Ping timeout: 256 seconds) |
| 2021-07-03 05:39:24 | <tomsmeding> | that path contains just the agda builtin base files, not the Agda Standard Library, which does have an IO module |
| 2021-07-03 05:39:33 | <tomsmeding> | and presumably also a 'run' function |
| 2021-07-03 05:40:09 | <tomsmeding> | see 2.3.2 and the note at the bottom of that section |
| 2021-07-03 05:40:15 | <edrx> | looking! |
| 2021-07-03 05:40:59 | <tomsmeding> | so you'll have to figure out not where 'agda' stores its .agda files but where 'agda-stdlib' stores its .agda files :D |
| 2021-07-03 05:41:10 | → | dunkeln joins (~dunkeln@94.129.65.28) |
| 2021-07-03 05:41:17 | → | pfurla joins (~pfurla@ool-182ed2e2.dyn.optonline.net) |
| 2021-07-03 05:42:00 | × | pfurla_ quits (~pfurla@216.131.83.59) (Ping timeout: 252 seconds) |
| 2021-07-03 05:42:47 | <edrx> | tomsmeding: I tried that... I tried "cd ~/.cabal/; find * | grep -i stdlib" but got no results... |
All times are in UTC.