[Agda] Installing Idris without breaking Agda

Mon Oct 29 08:38:25 CET 2018

You can interrupt, I don't think there's harm in that.

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

> Oh thank you! You appear to be right! I did PATH=$PATH:~/.cabal/bin and
> then idris and got the REPL again! And I guess since I started Emacs from
> that shell session, it inherited it somehow.
>
> Should I interrupt the reinstall, which is going on as we speak? I'll do
> it ASAP if need be!
> *Sent:* Monday, October 29, 2018 at 3:16 AM
> *From:* "András Kovács" <puttamalac at gmail.com>
> *To:* dave.martin at mail.com
> *Cc:* apostolis.xekoukoulotakis at gmail.com, "Agda mailing list" <
> agda at lists.chalmers.se>
> *Subject:* Re: [Agda] Installing Idris without breaking Agda
> 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/c8395f0c/attachment.html>