<html><head></head><body><div style="font-family: Verdana;font-size: 12.0px;"><div>
<div>Thank you! But I have communicated poorly; I never had an Agda installation failure! I did that a long time ago and it went off without a hitch; it was even easy for someone like me!</div>
<div> </div>
<div>What I am asking here (because I don't know of any better place to ask something so esoteric) is about installing Idris so it doesn't disrupt Agda. I got some warning messages that it would, then I was given a way around them which I took. But, as the story over the course of this thread relates, I apparently managed to get a working install of Idris (complete with REPL and Emacs functionality) up and running, and briefly and superficially tested Agda once again to see if it was broken.</div>
<div> </div>
<div>All seemed well until I restarted my computer, whereupon the current odd behavior appeared: Apparently Idris is still installed, but the command line does not recognize the "idris" command and Emacs does not recognize an "idris" program to load the buffer. And I forced a reinstall of Idris, and wonder if I really may have broken Agda this time. In any case I am in the middle of that same interminable wait, which I experienced at the first Idris installation!</div>
<div>
<div style="margin: 10.0px 5.0px 5.0px 10.0px;padding: 10.0px 0 10.0px 10.0px;border-left: 2.0px solid rgb(195,217,229);">
<div style="margin: 0 0 10.0px 0;"><b>Sent:</b> Monday, October 29, 2018 at 2:57 AM<br/>
<b>From:</b> "Kovács András" <kovacsandras@inf.elte.hu><br/>
<b>To:</b> "dave.martin@mail.com" <dave.martin@mail.com><br/>
<b>Cc:</b> "amindfv@gmail.com" <amindfv@gmail.com>, "Agda mailing list" <agda@lists.chalmers.se><br/>
<b>Subject:</b> Re: [Agda] Installing Idris without breaking Agda</div>
<div>
<div>Hi,
<div> </div>
<div>I do not recommend installing either Agda or Idris with cabal (if you just want to use them), instead install <a href="https://docs.haskellstack.org/en/stable/README/" target="_blank">stack</a>, then do "stack install Agda" and "stack install Idris", and add "~/.local/bin" to PATH.</div>
<div> </div>
<div>As to the Agda installation failure, I think you need to install alex and happy first, and you can also do this with "stack install alex" and "stack install happy".</div>
</div>
<div class="gmail_quote">
<div>Dave Martin <<a href="mailto:dave.martin@mail.com" onclick="parent.window.location.href='mailto:dave.martin@mail.com'; return false;" target="_blank">dave.martin@mail.com</a>> ezt írta (időpont: 2018. okt. 29., H, 7:50):</div>
<blockquote class="gmail_quote" style="margin: 0 0 0 0.8ex;border-left: 1.0px rgb(204,204,204) solid;padding-left: 1.0ex;">Yet another update: Idris was here; now it's gone!<br/>
<br/>
I had apparent success installing Idris in this manner. (I even managed to get Emacs idris-mode up and working, which seems like a minor miracle given my abilities.) But after restarting my computer, it seems Idris is gone! No REPL; Emacs idris-mode highlights text as you type but cannot find Idris to load the buffers. Typing "idris" in the command line gets you<br/>
<br/>
idris: command not found<br/>
<br/>
...In response I tried<br/>
<br/>
cabal install idris<br/>
<br/>
...again, wherein I got<br/>
<br/>
Resolving dependencies...<br/>
All the requested packages are already installed:<br/>
idris-1.3.1<br/>
Use --reinstall if you want to reinstall anyway.<br/>
<br/>
...How strange! Well I did<br/>
<br/>
cabal install idris --reinstall<br/>
<br/>
...and received<br/>
<br/>
Resolving dependencies...<br/>
In order, the following will be installed:<br/>
idris-1.3.1 (reinstall)<br/>
Warning: Note that reinstalls are always dangerous. Continuing anyway...<br/>
Configuring idris-1.3.1...<br/>
Building idris-1.3.1...<br/>
<br/>
...where things stand, apparently midprocess with no further messages, to this minute. What accounts for the strange behavior? Should I be concerned?<br/>
<br/>
<br/>
<br/>
<br/>
----------<br/>
<br/>
...Update!<br/>
<br/>
The install is FINALLY complete after all these hours! I got the following error messages:<br/>
<br/>
Installed idris-1.3.1<br/>
cabal: Error: some packages failed to install:<br/>
Agda-2.5.3 failed during the configure step. The exception was:<br/>
ExitFailure 1<br/>
<br/>
...That is indeed the version of Agda I'd had; but I've tried opening and loading an .agda file into Emacs and so far (haven't tried other commands yet) all seems well. Also called up the Idris REPL and everything seems in order there too.<br/>
<br/>
Is everything indeed fine? Why the error messages? What has happened exactly?<br/>
<br/>
...A huge list of apparently success indicating messages...but then a couple of (apparent) error messages towards the end:<br/>
<br/>
Configuring Agda-2.5.3...<br/>
Failed to install Agda-2.5.3<br/>
<br/>
[...]<br/>
<br/>
Configuring Agda-2.5.3...<br/>
setup: The program 'alex' version >=3.1.0 && <3.2.0 || >=3.2.1 is required but<br/>
it could not be found.<br/>
cabal: Leaving directory '/tmp/cabal-tmp-14275/Agda-2.5.3'<br/>
<br/>
[...]<br/>
<br/>
Building idris-1.3.1...<br/>
<br/>
...where it has been stuck for probably half an hour now. Did the fact that I still had Agda open during this process have something to do with it? It hadn't been obvious to me that I should close it; I just thought the "Agda" in the command you sent me was a flag to avoid Agda or something, not a reinstallation as I now think it may have been. What should I do now? I'm starting to think that this is not normal! Idris shouldn't take this long to install!<br/>
<br/>
<br/>
> Sent: Sunday, October 28, 2018 at 7:52 PM<br/>
> From: "Tom Murphy" <<a href="mailto:amindfv@gmail.com" onclick="parent.window.location.href='mailto:amindfv@gmail.com'; return false;" target="_blank">amindfv@gmail.com</a>><br/>
> To: "Dave Martin" <<a href="mailto:dave.martin@mail.com" onclick="parent.window.location.href='mailto:dave.martin@mail.com'; return false;" target="_blank">dave.martin@mail.com</a>><br/>
> Cc: <a href="mailto:agda@lists.chalmers.se" onclick="parent.window.location.href='mailto:agda@lists.chalmers.se'; return false;" target="_blank">agda@lists.chalmers.se</a><br/>
> Subject: Re: [Agda] Installing Idris without breaking Agda<br/>
><br/>
> What's the result of<br/>
><br/>
> cabal install idris Agda uri-encode<br/>
><br/>
> ?<br/>
><br/>
> Tom<br/>
><br/>
> On 10/28/18, Dave Martin <<a href="mailto:dave.martin@mail.com" onclick="parent.window.location.href='mailto:dave.martin@mail.com'; return false;" target="_blank">dave.martin@mail.com</a>> wrote:<br/>
> > I hope this isn't too off topic, but understand that I'm almost completely<br/>
> > "computer illiterate" and I don't know of any better place to ask it!<br/>
> ><br/>
> > I some time ago installed (Linux Mint 19) Emacs and Agda; they apparently<br/>
> > work perfectly. But now I want to install Idris as well. I followed the<br/>
> > official instructions (<br/>
> > <a href="http://docs.idris-lang.org/en/latest/tutorial/starting.html" target="_blank"> http://docs.idris-lang.org/en/latest/tutorial/starting.html</a> ). I first<br/>
> > installed cabal, then did cabal update, both with no messages; then I<br/>
> > finally tried cabal install idris. Whereupon I get this message:<br/>
> ><br/>
> > cabal: The following packages are likely to be broken by the reinstalls:<br/>
> > uri-encode-1.5.0.5<br/>
> > Agda-2.5.3<br/>
> > Use --force-reinstalls if you want to install anyway.<br/>
> ><br/>
> > Ah, what is going on here? I don't want to break Agda! (Taking the website's<br/>
> > suggestion of adding to my PATH didn't help.) How do I handle this puzzle?<br/>
> ><br/>
> > Also: Once I succeed, will I be able to use Idris in Emacs like I can Agda?<br/>
> > I have used Atom and I find it unpleasant and confusing.<br/>
> ><br/>
> > Any help anyone can provide would be appreciated; again, I was sure this<br/>
> > small community is as likely as any out there to be familiar with what it<br/>
> > takes.<br/>
> > _______________________________________________<br/>
> > Agda mailing list<br/>
> > <a href="mailto:Agda@lists.chalmers.se" onclick="parent.window.location.href='mailto:Agda@lists.chalmers.se'; return false;" target="_blank">Agda@lists.chalmers.se</a><br/>
> > <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank"> https://lists.chalmers.se/mailman/listinfo/agda</a><br/>
> ><br/>
><br/>
_______________________________________________<br/>
Agda mailing list<br/>
<a href="mailto:Agda@lists.chalmers.se" onclick="parent.window.location.href='mailto:Agda@lists.chalmers.se'; return false;" target="_blank">Agda@lists.chalmers.se</a><br/>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a></blockquote>
</div>
</div>
</div>
</div>
</div></div></body></html>