Home liberachat/#haskell: Logs Calendar

Logs: liberachat/#haskell

←Prev  Next→
Page 1 .. 762 763 764 765 766 767 768 769 770 771 772 .. 18021
— 1,802,012 events total
2021-07-03 05:43:06 × nate1 quits (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 252 seconds)
2021-07-03 05:43:45 <edrx> and the same but with grep -i io.agda only returns the IO.agda in ~/.cabal/store/ghc-8.8.4/Agda-2.6.2-b2f8eb43cd09b8b95a6e2958c006bc2f47b9966435e6f21d09b053b958e4fc43/share/lib/prim/Agda/Builtin/IO.agda ...
2021-07-03 05:43:48 <tomsmeding> try 'find ~ -name agda-stdlib'
2021-07-03 05:43:55 <edrx> ok!
2021-07-03 05:44:08 × jess quits (~jess@libera/staff/jess) (Remote host closed the connection)
2021-07-03 05:44:19 <tomsmeding> "grep -i io.agda" is not going to help much, that searches the _content_ of files for that string :p
2021-07-03 05:44:25 <tomsmeding> how did you install agda-stdlib?
2021-07-03 05:44:36 <edrx> I didn't =(
2021-07-03 05:44:54 <tomsmeding> then you should!
2021-07-03 05:45:04 <edrx> I only have the agda-stdlib from Debian, not one in cabal... ok, trying!
2021-07-03 05:45:09 <tomsmeding> either https://github.com/agda/agda-stdlib/blob/master/notes/installation-guide.md or perhaps the debian package? not sure if that is remotely new enough
2021-07-03 05:45:25 <tomsmeding> edrx: don't think you're going to get one from cabal
2021-07-03 05:45:38 <edrx> the docs say that the Debian package is too broken
2021-07-03 05:46:00 <tomsmeding> lol
2021-07-03 05:46:07 <tomsmeding> then use the link I sent I guess
2021-07-03 05:46:38 <tomsmeding> right and that also explains how to point the main 'agda' executable to wherever you put the stdlib
2021-07-03 05:47:54 × xff0x quits (~xff0x@2001:1a81:52ae:a300:b096:1d82:d091:433d) (Ping timeout: 240 seconds)
2021-07-03 05:48:01 → slack1256 joins (~slack1256@191.125.188.158)
2021-07-03 05:49:10 → xff0x joins (~xff0x@2001:1a81:52ae:a300:6abc:acbb:6923:464a)
2021-07-03 05:55:34 → takuan joins (~takuan@178-116-218-225.access.telenet.be)
2021-07-03 05:57:18 → nate1 joins (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net)
2021-07-03 06:00:32 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 272 seconds)
2021-07-03 06:01:07 × Xnuk quits (~xnuk@45.76.202.58) (Quit: ZNC - https://znc.in)
2021-07-03 06:01:24 → Xnuk joins (~xnuk@vultr.xnu.kr)
2021-07-03 06:01:53 → chomwitt joins (~Pitsikoko@2a02:587:dc0b:0:d8f7:cdfe:4658:bec4)
2021-07-03 06:02:10 × nate1 quits (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 252 seconds)
2021-07-03 06:03:58 × dunkeln quits (~dunkeln@94.129.65.28) (Ping timeout: 268 seconds)
2021-07-03 06:03:59 <edrx> tomsmeding: I downloaded it, unpacked it, ran "cabal install", and patched ~/.agda/libraries and ~/.agda/defaults according to the instructions, but when I try to compile my test1.agda I still get the same error. Do I need a line like "open import Agda.Builtin.IO" in my ~/AGDA/test1.agda that loads a file that declares "run"?
2021-07-03 06:04:33 <tomsmeding> no 'open import IO' should be enough
2021-07-03 06:04:40 <edrx> trying!
2021-07-03 06:06:29 <tomsmeding> O.o 'agda --compile' does something exceedingly weird on my system
2021-07-03 06:07:38 × chomwitt quits (~Pitsikoko@2a02:587:dc0b:0:d8f7:cdfe:4658:bec4) (Ping timeout: 256 seconds)
2021-07-03 06:07:45 → dunkeln joins (~dunkeln@94.129.65.28)
2021-07-03 06:08:12 → wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net)
2021-07-03 06:08:24 <edrx> what?
2021-07-03 06:09:54 × myShoggoth quits (~myShoggot@75.164.51.64) (Ping timeout: 256 seconds)
2021-07-03 06:10:08 × sheepduck quits (~sheepduck@user/sheepduck) (Quit: Konversation terminated!)
2021-07-03 06:10:35 <edrx> ok, now "agda test1.agda" compiled lots of stuff in agda-stdlib...
2021-07-03 06:10:42 <edrx> but I got a new error:
2021-07-03 06:10:51 <edrx> Importing module IO using the --guardedness flag from a module which does not.
2021-07-03 06:10:51 <edrx> when scope checking the declaration
2021-07-03 06:10:51 <edrx> open import IO
2021-07-03 06:12:16 <tomsmeding> --guardedness should be the default, according to agda's option listing
2021-07-03 06:12:33 <tomsmeding> but I guess you can try adding it (i.e. agda --compile --guardedness'
2021-07-03 06:12:42 <tomsmeding> s/'/)/
2021-07-03 06:13:01 → tromp joins (~textual@dhcp-077-249-230-040.chello.nl)
2021-07-03 06:13:12 × wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 272 seconds)
2021-07-03 06:15:07 → nate1 joins (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net)
2021-07-03 06:17:18 <edrx> new error: I ran "agda --compile --guardedness test1.agda" and it gave lots of lines like "Checking Data.List.Relation.Binary.Lex.Core (/home/edrx/usrc/agda-stdlib-1.7/src/Data/List/Relation/Binary/Lex/Core.agda)."... and then it aborted with:
2021-07-03 06:17:23 <edrx> Unsolved metas at the following locations:
2021-07-03 06:17:23 <edrx> /home/edrx/AGDA/test1.agda:9,8-11
2021-07-03 06:18:26 <edrx> at line 9, columns 8-11 of test1.agda I have "run".
2021-07-03 06:20:10 × nate1 quits (~nate@108-233-125-227.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds)
2021-07-03 06:20:55 × slowButPresent quits (~slowButPr@user/slowbutpresent) (Quit: leaving)
2021-07-03 06:23:02 tomsmeding is compiling a more recent agda
2021-07-03 06:24:51 → chexum joins (~chexum@gateway/tor-sasl/chexum)
2021-07-03 06:25:33 × Erutuon quits (~Erutuon@user/erutuon) (Ping timeout: 268 seconds)
2021-07-03 06:26:54 edrx is latexing a diagram in trog mode
2021-07-03 06:29:22 <tomsmeding> edrx: I got hello world to compile!
2021-07-03 06:31:29 <tomsmeding> edrx: https://paste.tomsmeding.com/dNKEhru6
2021-07-03 06:31:33 × slack1256 quits (~slack1256@191.125.188.158) (Remote host closed the connection)
2021-07-03 06:31:46 <tomsmeding> the 'cabal build' exits with an error but is necessary to construct the package db, it seems
2021-07-03 06:31:56 <tomsmeding> relevant: https://github.com/agda/agda/issues/3619
2021-07-03 06:33:34 × jespada quits (~jespada@90.254.247.46) (Ping timeout: 268 seconds)
2021-07-03 06:33:57 <edrx> works!!! thanks!!! =)
2021-07-03 06:35:14 → jespada joins (~jespada@90.254.247.46)
2021-07-03 06:36:12 <edrx> I didn't need the package db or the Numeric.IEEE fix... but I when I copied the code for hello world from the manual it didn't have this line: "main : Main"
2021-07-03 06:36:18 <tomsmeding> also relevant: https://github.com/agda/agda/issues/4627
2021-07-03 06:36:25 <tomsmeding> apparently they're working on making this a bit smoother :)
2021-07-03 06:36:51 <edrx> thanks a lot!!!!!!!! =)
2021-07-03 06:37:18 <tomsmeding> edrx: ah I see, and then you're getting this "unresolved metas" line
2021-07-03 06:37:39 × cheater quits (~Username@user/cheater) (Ping timeout: 258 seconds)
2021-07-03 06:37:45 <tomsmeding> I know very little about agda the language (and in particular the standard library), but I guess that type signature is necessary?
2021-07-03 06:38:03 <tomsmeding> and that if the compiler would have gotten past that, you would have run into the same issue
2021-07-03 06:38:07 → cheater joins (~Username@user/cheater)
2021-07-03 06:38:17 → Gurkenglas joins (~Gurkengla@dslb-002-203-144-156.002.203.pools.vodafone-ip.de)
2021-07-03 06:38:40 tomsmeding now suddenly doesn't need the db fix either anymore?
2021-07-03 06:38:46 tomsmeding is confused but holes edrx is happy
2021-07-03 06:38:58 → mei joins (~mei@user/mei)
2021-07-03 06:39:07 <tomsmeding> s/holes/hopes/
2021-07-03 06:39:25 <edrx> seems to be. I just found that Main is defined in src/IO/Base.agda - I'll try to understand that...
2021-07-03 06:39:37 <edrx> does Agda support holes like Idris?
2021-07-03 06:39:45 → argento joins (~argent0@168-227-96-53.ptr.westnet.com.ar)
2021-07-03 06:40:26 × argento quits (~argent0@168-227-96-53.ptr.westnet.com.ar) (Client Quit)
2021-07-03 06:41:31 <edrx> anyway, don't worry about that! I need to sleep, thanks again! =)
2021-07-03 06:46:19 <tomsmeding> edrx: it should support that!
2021-07-03 06:48:14 → tomek-grzesiak joins (~tomek-grz@109.206.213.203)
2021-07-03 06:49:08 <tomsmeding> edrx: I think you're supposed to use agda from an editor with editor integration; emacs seems to be the most-supported thing, but atom, or with some configuration vim, may also work
2021-07-03 06:49:12 → neo1 joins (~neo3@cpe-292712.ip.primehome.com)
2021-07-03 06:49:15 <tomsmeding> then _ or ? or {!!} are holes
2021-07-03 06:49:55 × neo quits (~neo3@cpe-292712.ip.primehome.com) (Ping timeout: 258 seconds)
2021-07-03 06:51:18 × dunkeln quits (~dunkeln@94.129.65.28) (Ping timeout: 252 seconds)
2021-07-03 06:51:50 × favonia quits (~favonia@user/favonia) (Ping timeout: 256 seconds)
2021-07-03 06:52:15 → favonia joins (~favonia@user/favonia)
2021-07-03 06:58:53 → Lycurgus joins (~juan@cpe-45-46-140-49.buffalo.res.rr.com)
2021-07-03 06:59:26 → chomwitt joins (~Pitsikoko@2a02:587:dc0b:0:d8f7:cdfe:4658:bec4)
2021-07-03 06:59:31 × tromp quits (~textual@dhcp-077-249-230-040.chello.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2021-07-03 07:00:32 × beka__ quits (~beka@104.193.170-244.PUBLIC.monkeybrains.net) (Ping timeout: 265 seconds)
2021-07-03 07:02:51 → dunkeln_ joins (~dunkeln@94.129.65.28)
2021-07-03 07:02:56 × tomek-grzesiak quits (~tomek-grz@109.206.213.203) (Quit: Leaving)
←Prev  Next→
Page 1 .. 762 763 764 765 766 767 768 769 770 771 772 .. 18021

All times are in UTC.