[Agda] Installing Idris without breaking Agda

[András Kovács]

Apt is a standard linux package management tool which is used commonly in
Ubuntu and Debian. It installs binaries, so if you get Agda from apt you do
not build it from source on your machine. Because you don't build, you
don't need the myriad Haskell package dependencies. However, the Agda on
apt is usually out of date, as I see it's 2.5.3, while the newest version
is 2.5.4.1.

With Idris, perhaps you need to add the directory where the Idris
executable is to PATH. It's something like "~/.cabal/bin".

Dave Martin <dave.martin at mail.com> ezt írta (időpont: 2018. okt. 29., H,
8:03):

>
> Thank you! I actually used apt to install agda:
>
> sudo apt install agda-bin
>
> ...I don't even know what apt is, just that it worked. Should it have
> avoided the issues your method would have?
>
> Also, do you know what might have happened with my present situation (I
> still am mid process, with no further messages)? Why the odd behavior from
> the shell and Emacs, whereas apparently Idris had already been successfully
> installed? And have I now broken Agda with this reinstall?
>
> *Sent:* Monday, October 29, 2018 at 2:56 AM
> *From:* "Apostolis Xekoukoulotakis" <apostolis.xekoukoulotakis at gmail.com>
> *To:* dave.martin at mail.com
> *Cc:* amindfv at gmail.com, "agda list" <agda at lists.chalmers.se>
> *Subject:* Re: [Agda] Installing Idris without breaking Agda
> The way I have installed both Idris and agda is to install agda with stack
> and idris with cabal.
> This way, the one does not interfere with the other.
>
> https://www.stackage.org/package/Agda
>
>
>
>
> On Mon, Oct 29, 2018 at 8:50 AM Dave Martin <dave.martin at mail.com> wrote:
>
>> Yet another update: Idris was here; now it's gone!
>>
>> 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
>>
>> idris: command not found
>>
>> ...In response I tried
>>
>> cabal install idris
>>
>> ...again, wherein I got
>>
>> Resolving dependencies...
>> All the requested packages are already installed:
>> idris-1.3.1
>> Use --reinstall if you want to reinstall anyway.
>>
>> ...How strange! Well I did
>>
>> cabal install idris --reinstall
>>
>> ...and received
>>
>> Resolving dependencies...
>> In order, the following will be installed:
>> idris-1.3.1 (reinstall)
>> Warning: Note that reinstalls are always dangerous. Continuing anyway...
>> Configuring idris-1.3.1...
>> Building idris-1.3.1...
>>
>> ...where things stand, apparently midprocess with no further messages, to
>> this minute. What accounts for the strange behavior? Should I be concerned?
>>
>>
>>
>>
>> ----------
>>
>> ...Update!
>>
>> The install is FINALLY complete after all these hours! I got the
>> following error messages:
>>
>> Installed idris-1.3.1
>> cabal: Error: some packages failed to install:
>> Agda-2.5.3 failed during the configure step. The exception was:
>> ExitFailure 1
>>
>> ...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.
>>
>> Is everything indeed fine? Why the error messages? What has happened
>> exactly?
>>
>> ...A huge list of apparently success indicating messages...but then a
>> couple of (apparent) error messages towards the end:
>>
>> Configuring Agda-2.5.3...
>> Failed to install Agda-2.5.3
>>
>> [...]
>>
>> Configuring Agda-2.5.3...
>> setup: The program 'alex' version >=3.1.0 && <3.2.0 || >=3.2.1 is
>> required but
>> it could not be found.
>> cabal: Leaving directory '/tmp/cabal-tmp-14275/Agda-2.5.3'
>>
>> [...]
>>
>> Building idris-1.3.1...
>>
>> ...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!
>>
>>
>> > Sent: Sunday, October 28, 2018 at 7:52 PM
>> > From: "Tom Murphy" <amindfv at gmail.com>
>> > To: "Dave Martin" <dave.martin at mail.com>
>> > Cc: agda at lists.chalmers.se
>> > Subject: Re: [Agda] Installing Idris without breaking Agda
>> >
>> > What's the result of
>> >
>> >     cabal install idris Agda uri-encode
>> >
>> > ?
>> >
>> > Tom
>> >
>> > On 10/28/18, Dave Martin <dave.martin at mail.com> wrote:
>> > > I hope this isn't too off topic, but understand that I'm almost
>> completely
>> > > "computer illiterate" and I don't know of any better place to ask it!
>> > >
>> > > I some time ago installed (Linux Mint 19) Emacs and Agda; they
>> apparently
>> > > work perfectly. But now I want to install Idris as well. I followed
>> the
>> > > official instructions (
>> > > http://docs.idris-lang.org/en/latest/tutorial/starting.html ). I
>> first
>> > > installed cabal, then did cabal update, both with no messages; then I
>> > > finally tried cabal install idris. Whereupon I get this message:
>> > >
>> > > cabal: The following packages are likely to be broken by the
>> reinstalls:
>> > > uri-encode-1.5.0.5
>> > > Agda-2.5.3
>> > > Use --force-reinstalls if you want to install anyway.
>> > >
>> > > Ah, what is going on here? I don't want to break Agda! (Taking the
>> website's
>> > > suggestion of adding to my PATH didn't help.) How do I handle this
>> puzzle?
>> > >
>> > > Also: Once I succeed, will I be able to use Idris in Emacs like I can
>> Agda?
>> > > I have used Atom and I find it unpleasant and confusing.
>> > >
>> > > Any help anyone can provide would be appreciated; again, I was sure
>> this
>> > > small community is as likely as any out there to be familiar with
>> what it
>> > > takes.
>> > > _______________________________________________
>> > > Agda mailing list
>> > > Agda at lists.chalmers.se
>> > > https://lists.chalmers.se/mailman/listinfo/agda
>> > >
>> >
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181029/dd462062/attachment.html>