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

--- Day changed Sun Mar 19 2017
vorgangmorning19/03 08:02
vorgang"open import Algebra" is an error for me, so I figured I need stdlib19/03 08:03
vorgangso I cloned it from github, but "make" fails because "fix-agda-whitespace" is missing19/03 08:04
vorgangI found it in agda source, but cabal doesn't find it. tl;dr how to install fix-agda-whitespace?19/03 08:06
vorgangthis page has some info http://wiki.portal.chalmers.se/agda/pmwiki.php?n=DevelopersManual.BugFixing19/03 08:07
vorgangbut neither "make install-fix-agda-whitespace" nor "make install fix-agda-whitespace" worked19/03 08:08
comietekvorgang should take a look at https://github.com/Homebrew/homebrew-core/blob/master/Formula/agda.rb19/03 10:56
vorgangok sorry I was away, did someone answer my question about stdlib installation?19/03 12:31
mietekvorgang: what is your OS?19/03 12:35
mietekOn an unrelated note, the "…because19/03 12:35
mietekone is an implicit function type and the other is an explicit19/03 12:35
mietekfunction type…" error is killing me19/03 12:35
vorgangit's fedora linux19/03 12:35
vorgangI assume that most agda developers use debian?19/03 12:36
mietekvorgang: I don’t know. I use OS X, and I encoded my knowledge about installing Agda with the stdlib as https://github.com/Homebrew/homebrew-core/blob/master/Formula/agda.rb19/03 12:36
vorgangmietek: thank you19/03 12:37
mietekvorgang: are you familiar with Haskell/cabal?19/03 12:37
vorgangnot much...19/03 12:37
mietekRight; that’s the confusing part.19/03 12:37
mietekFirst, you should install GHC and cabal-install19/03 12:37
vorgangsorry afk again for a couple minutes now..19/03 12:38
mietek`ghc --version`, `cabal --version`19/03 12:38
vorgangmietek: ghc 7.10.3, cabal "cabal-install version 1.22.9.0, 1.22.5.0 of the Cabal library"19/03 13:18
mietekThat’s an old GHC19/03 13:18
mietekDecember 201519/03 13:18
vorgangoh, I didn't know. I think it's from fedoras package manager. I'll try and update, thanks!19/03 13:18
mietekNot saying this is necessarily a problem19/03 13:19
mietekI think it still should work19/03 13:19
vorgangwell, the top-level of my problem is that "open import Algebra" doesn't compile19/03 13:19
mietekYes, we’ll get there19/03 13:19
vorgangso I tried to install agda-stdlib from github, and that failed because of the missing whitespace thing19/03 13:20
mietekhttp://agda.readthedocs.io/en/v2.5.2/getting-started/installation.html#fedora19/03 13:21
mietekDid you do `yum install Agda`?19/03 13:21
vorgangnot sure, checking now19/03 13:21
vorganguhm no, actually I installed it from source19/03 13:23
vorgangwell, maybe I should scrub that and reinstall using yum19/03 13:23
mietekGood idea19/03 13:23
mietekI don’t know if that includes the stdlib, but it’ll be a better starting point19/03 13:24
vorgangIt seems like there's no separate yum package for stdlib19/03 13:24
mietekThere may simply not be one.19/03 13:24
vorgangor rather, there is19/03 13:24
vorgangoops19/03 13:24
vorgangok that'll probably do, then19/03 13:25
vorgangdoes anyone know how to undo the manual install from source?19/03 13:25
vorgangmaybe it's a cabal command?19/03 13:26
mietekThere’s no undo in cabal.19/03 13:26
vorganghmm, that's surprising19/03 13:27
vorgangdeleting stuff in ~/.cabal/lib is probably not recommended19/03 13:28
mietekIt depends.19/03 13:28
vorgangI could remove cabal entirely and start from scatch19/03 13:28
mietekDo you use Haskell for anything else?19/03 13:28
vorgangno19/03 13:28
mietekThen you can wipe ~/.cabal and ~/.ghc19/03 13:29
vorganggood, I'll do that and also purge with yum19/03 13:29
mietekThere may be things in e.g. /usr/local depending on how exactly did you "install from source"19/03 13:29
vorgangI think there was no sudo involved, so it probably just wrote to ~/.cabal 19/03 13:30
mietekOK19/03 13:30
vorgangthe packages are broken... "nothing provides ghc(base-4.7.0.2-cb23b5265b6e147094c0cd9ac819acb1) needed by Agda-stdlib-0.9-3.fc24.x86_64"19/03 13:36
vorgangcould be the reason why I installed agda from source, in the first place19/03 13:37
mietekThat seems to want GHC 7.8.419/03 13:37
mietekAnd that’s an ancient stdlib package19/03 13:37
mietekIgnore that package19/03 13:37
mietekWhat’s the version of the Agda package?19/03 13:38
vorgangyup that's even older than the last ghc19/03 13:38
vorganghang on..19/03 13:38
vorgang2.4.2.519/03 13:39
mietekDecember 2016; reasonably recent…19/03 13:39
vorgangyup, but someone didn't update its dependencies19/03 13:39
mietekShould work with agda-stdlib 0.1119/03 13:39
mieteker19/03 13:40
vorgangmaybe I should just install everyone from source, including ghc?19/03 13:40
mietekSorry, no, it’s December 201519/03 13:40
vorgang*everything19/03 13:40
mietekIt seems that Fedora hasn’t received much love recently19/03 13:40
vorgangyup, it's a barren place19/03 13:40
mietekInstalling GHC from source will hurt19/03 13:40
gallaisThat seems way to overkill just to install the stdlib19/03 13:41
mietekYes19/03 13:41
gallaisit's usually just a matter of downloading a tarball and decompressing it19/03 13:41
vorgangif it works I don't mind19/03 13:41
mietekI think vorgang wanted to generate the documentation files and ran into cabal 19/03 13:42
vorgangmaybe I should reinstall ghc using yum, then install everything using cabal?19/03 13:42
vorgangmietek: at this point, just compiling some type that involves Nat will be enough19/03 13:43
mietekThat should really be just `agda -i /wherever/agda-stlib/src Module.agda`19/03 13:44
mietek(assuming you mean typechecking, not compiling)19/03 13:44
mietek(which is probably what you want anyway)19/03 13:45
vorgangyes I guess so19/03 13:45
vorgangcorrect, I mean typechecking19/03 13:46
mietekSo what happens when you do that?19/03 13:46
vorganguhm, well I'd have to reinstall some things before I can answer that19/03 13:46
vorgangand I'm not quite sure how. right now, there isn't even ghc19/03 13:47
vorgangI *could* install one from 2015 using yum19/03 13:47
mietekOK, look.  GHC 7.10.3 should be fine.19/03 13:47
mietekThat cabal-install you’ve had also seemed fine.19/03 13:47
vorganggood, I'll start with that then19/03 13:47
mietekIdeally, I would say, try to avoid using `cabal` at all19/03 13:48
mietekUsing it effectively requires some experience19/03 13:49
gallaisAgda is continuously tested with ghc 7.6.3, 7.8.4, 7.10.3, 8.0.2.19/03 13:49
vorgangso should I install agda from source, then? I think that uses cabal under the hood19/03 13:49
gallaisIt is supposed to work with older versions of the compiler19/03 13:49
mietekgallais: good to know. Where can we see that? Also, what happened to the "Releases" tab on GitHub?19/03 13:49
gallaishttps://github.com/agda/agda/blob/stable-2.5/Agda.cabal#L3519/03 13:50
gallaisAlso https://travis-ci.org/agda/agda/builds19/03 13:50
vorgangOK I have ghc and cabal-install now. Should I "make" the Agda source?19/03 13:50
gallaisvorgang: where did you get the source? Unless you're a developper, there's no real reason to use a dev version from github rather than the one you get from "cabal install Agda"19/03 13:51
gallaisquite the contrary actually: using a stable version is probably easier19/03 13:51
vorgang"cabal install Agda" is running, seems fine so far19/03 13:52
mietekProbably needs `cabal install alex happy cpphs` before19/03 13:53
vorgangon a side note, I've noticed that the emacs mode doesn't seem to start a process19/03 13:54
vorgangunlike coq-mode19/03 13:54
vorgangis everything evaluated on demand?19/03 13:54
vorgangmietek: correct, it needs alex etc19/03 13:54
vorgangshouldn't the Agda cabal package list alex, happy and cpphs as dependencies, and pull them automatically?19/03 13:55
mietekvorgang: :)19/03 14:00
mietekvorgang: https://github.com/haskell/cabal/issues/22019/03 14:00
mietekvorgang: TLDR: it should, but cabal doesn’t allow it19/03 14:01
mietekThe reasons are obscure and annoying19/03 14:02
vorgangdoes cabal always compile from source?19/03 14:04
vorgangok Agda install was successful. Now the emacs mode stopped working, "Agda mode version (2.5.2) doesn't match agda version (2.4.2.5)"19/03 14:06
vorgangReasons are often annoying. Don't tell me cause it hurts! https://www.youtube.com/watch?v=TR3Vdo5etCQ19/03 14:09
mietekI think pgiarrusso made some progress towards getting Agda to build with Stack, which apparently removes much of the pain19/03 14:14
mietekI don’t know the state of that work19/03 14:14
mietekUnfortunately, I can’t explain everything that is wrong about Cabal and how to work around it, because it would take me days19/03 14:14
mietekI spent more than a year trying to build a wrapper for Cabal that worked around these issues19/03 14:15
vorgangright now, I'm done with cabal, but need to reinstall the emacs mode19/03 14:15
mietek(https://halcyon.sh)19/03 14:15
mietekBut that’s obsolete now, due to Stack19/03 14:15
vorgangok it seems like the emacs mode came with cabal, as a side-product of installing agda19/03 14:17
vorgangbut their versions are not compatible... ts19/03 14:17
vorgangmaybe I should just install a linux distro that has up-to-date packages19/03 14:22
vorgangdebian?19/03 14:22
mietekSounds overkill again; why not just wipe the emacs mode and install that again?19/03 14:23
vorgangit was installed via cabal; wipe how? and, how to reinstall without cabal19/03 14:24
mietek`which agda-mode`19/03 14:25
vorgangwell, at least "agda-mode locate" tells me it's installed via cabal, which means it was installed just now19/03 14:25
vorgang/home/vgm/.cabal/bin/agda-mode19/03 14:26
mietekWhat happens with `agda-mode compile`?19/03 14:26
vorgangthat did something, not sure what19/03 14:27
vorgangversion mismatch is still there19/03 14:27
vorgangMust leave, thanks a lot folks for all the help. I will try this again.19/03 14:30

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