/home/laney/.irssi/irclogs/Freenode/#agda.log-20180105

--- Day changed Thu Jan 04 2018
pgiarrussopie_: FWIW even the Nix fans agree Nix involves more Yak shaving04/01 00:19
pie_yeah but once it works it more or less works no?04/01 00:20
* pie_ scratches head ... thats not saying much04/01 00:20
pgiarrussoThey also use it, yeah, so it must be cool somehow04/01 00:21
pgiarrusso> 11:51 PM <pie_> there ahs to be a better way to do this than manualls installing 77 haskell packages04/01 00:21
lambdabot <hint>:1:49: error: parse error on input ‘do’04/01 00:21
pgiarrussoThat’s sure wrong04/01 00:21
pgiarrussoI haven’t compiled stuff, but i guess you just need to add a dependency on Agda’s FFI package in the cabal file for the generated code (which you might have to write yourself, dunno?)04/01 00:22
pie_yeah i ran across cabal2nix04/01 00:23
pie_didnt really manage to get it to run04/01 00:24
pie_couldnt figure out the right way to call the output :P04/01 00:24
pie_ill do this some other time04/01 00:24
pgiarrussoI hope there’s some #nix channel04/01 00:24
pie_there is04/01 00:24
pie_#nixos04/01 00:24
pie_amount of help varies but generally quite friendly04/01 00:24
pgiarrussoBut have you built haskell software? Can you write cabal files?04/01 00:25
pie_not really04/01 00:25
pie_what bothers me is that its packaged but the package seems pretty broken usability-wse04/01 00:25
pgiarrussoBecause the instructions in that page assume you have experience with that :-|04/01 00:25
pgiarrussoHonestly, few people run agda programs I think, and surely it’s not heavily documented04/01 00:26
pgiarrussoI mean, I wouldn’t know from those docs how to do it with stack04/01 00:26
pgiarrussoThat webpage says to install the FFI package in the “user” cabal database, so that your program can use it, but it doesn’t say so, pie_04/01 00:27
pgiarrussoTranslating that to stack is already not trivial, I don’t want to know about Nix :-(04/01 00:29
mudri[m]BTW, what dependency is this that's being Cabal-installed?04/01 00:31
pie_i think for whatever reason it couldnt find any of them04/01 00:32
pie_well i mean the reason is obviously that the environment didnt pull them in04/01 00:32
pgiarrussopie_: having a per-user m04/01 00:33
pgiarrusso*mutable package db is evil04/01 00:33
pgiarrussoSo Nix and Stack work hard to NOT have that04/01 00:33
pie_yeah04/01 00:33
mudri[m]I'm just trying to work out how the nixpkgs Agda package gets around it.04/01 00:34
pgiarrussoIn stack you’d need to add an extra package with a path in stack.yaml04/01 00:34
pgiarrussomudri[m]: it would not need to, likely04/01 00:34
pie_well i *am* using the nixpkgs agda package04/01 00:35
pgiarrussoBuilding agda does not need to use this infrastructure, except maybe in tests04/01 00:35
mudri[m]It does some trickery about prebuilding all the builtin modules.04/01 00:35
pie_but im guessing one needs to compile to use stuff like IO04/01 00:35
pie_and im guessing noone does normal programming with agda so that rarely happens ;P04/01 00:36
pgiarrussopie_: that’s what the webpage suggests04/01 00:36
pgiarrussoAnd yep04/01 00:36
pie_idk why there isnt a proper way to install the stdlib either04/01 00:36
pie_well, i mean its still better than nothing04/01 00:37
mudri[m]You mean, like, on a per-project basis?04/01 00:37
pie_no i mean the agda stdlib at all04/01 00:38
pie_theres some packages in the nix repo but idk what theyre actually supposed to do because installing them doesnt result in agda finding them04/01 00:38
comietekhttp://agda.readthedocs.io/en/v2.5.3/getting-started/installation.html#os-x04/01 00:39
mudri[m]Aah, you mean you have to specify the path somewhere in Agda's config.04/01 00:39
comietekfortunately, someone has written exactly what needs to be specified where04/01 00:39
mudri[m]I think it's slightly more reasonable now. Let me check...04/01 00:40
comietekadjust the stdlib path to suit nix04/01 00:40
mudri[m]Just gotta find the right simlink.04/01 00:41
pie_comietek, yes thats the way i got at least that part to work in the end04/01 00:44
mudri[m]~/.nix-profile/share/agda04/01 00:44
mudri[m]Reminds me to make an ~/.agda, though.04/01 00:44
pgiarrussopie_: I suspect what you’re seeing is why Nix users send so many PRs (they have a record number of contributors, or some such stat) :-)04/01 00:48
pgiarrusso(though now I’m basically shitposting, so I’ll stop)04/01 00:48
Saizani'd bet there's some environment variables that controls what package dbs ghc is seeing, so you could set that when compiling agda programs if you don't want to install things in the user db04/01 08:40
pgiarrussoAnd Saizan wins with GHC_PACKAGE_PATH: http://downloads.haskell.org/~ghc/latest/docs/html/users_guide/packages.html#the-ghc-package-path-environment-variable04/01 09:35
pgiarrussoBut Stack (and probably Nix?) use it, so I’m not sure it’ll work in the end04/01 09:36
pgiarrussoAt least, I’m sure that’s not supported by Stack04/01 09:36
Saizanpgiarrusso: maybe "stack exec agda -c ..." would work, otherwise you can do "GHC_PACKAGE_PATH=... agda -c .."04/01 10:47
Saizans/do/try/04/01 10:48
pgiarrussoSaizan: uh, it’s agda calling GHC and needing the packages? I thought it just generated code and you compiled it later.04/01 11:54
pgiarrussopie_: ^^04/01 11:54
Saizanpgiarrusso: yeah, iirc04/01 12:09
apostolishttps://agda.github.io/agda-stdlib/Data.Nat.Base.html#80204/01 21:19
apostolisShouldn't those constructors be defined as instance ?04/01 21:19
apostolisThere is a unique solution, thus they should.04/01 21:20
Saizanapostolis: most of the stdlib was written before instance arguments were a thing04/01 21:32
apostolisSaizan : Ok , thankfully I do not need it to be instance at the moment. But maybe I will later. I will make a pull request then to change it.04/01 21:37

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!