[Agda] hints on switching between Agda versions

[Martin Escardo]

On 17/11/16 20:09, Andrew Pitts wrote:
> Following up my own question, I did a bit of RTFM-style research and
> found that one can use cabal to install into a sandbox. Combining this
> with Jesper's suggerstion I did:
>
> git clone https://github.com/agda/agda.git
> cd agda
> cabal update
> cabal sandbox init

I got up to here. Then with this ...

> cabal install --program-suffix=-2.6.0

... I get

void-0.7.1 (via: Agda-2.6.0) (new package)
Agda-2.6.0 (new package)
cabal: The following packages are likely to be broken by the reinstalls:
regex-posix-0.95.2
regex-compat-0.95.1
Use --force-reinstalls if you want to install anyway.

What exactly will this break, I wonder.

Martin




> This creates some binaries in .cabal-sandbox/bin whose names end with
> -2.6.0 (in particular agda-2.6.0 and agda-mode-2.6.0) that can then be
> linked to wherever your main agda binaries reside. Switching version
> within emacs is then just a matter of typing 2.6.0 RET after selecting
> the "Switch to another version of Agda" item in the Agda menu (after
> the switch that menu item acquires a key binding (^C^X^S) that it does
> not have before -- which is somewhat weird).
>
> Andy
>
> On 17 November 2016 at 14:55, Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk> wrote:
>> Hi Jesper.
>>
>> On 17 November 2016 at 11:34, Jesper Cockx <Jesper at sikanda.be> wrote:
>>> This is what I noticed:
>>>
>>> If you run 'cabal install' with the option '--program-suffix=-xxx', then
>>> Agda will be installed under the name agda-xxx. You can then switch Agda versions using the emacs command by entering the name of the binary.
>>
>> Thanks for that tip, which sounds good. I currently have Agda-2.5.1.1
>> installed and I want to install the development version (that's
>> 2.6.0-something, I guess). So following instructions at
>> <http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Download> and
>> then at <https://github.com/agda/agda/blob/master/README.md#installing-agda>
>> I have typed the following at a command prompt:
>>
>> git clone https://github.com/agda/agda.git
>> cd agda
>> cabal update
>>
>>
>> and then using your tip
>>
>> cabal install --program-suffix=-2.6.0
>>
>>
>> and cabal says
>>
>> Resolving dependencies...
>> In order, the following would be installed:
>> fail-4.9.0.0 (via: Agda-2.6.0) (new package)
>> gitrev-1.2.0 (via: Agda-2.6.0) (new package)
>> ieee754-0.7.9 (via: Agda-2.6.0) (new package)
>> murmur-hash-0.1.0.9 (via: Agda-2.6.0) (new package)
>> regex-tdfa-1.2.2 (via: Agda-2.6.0) (new package)
>> transformers-compat-0.5.1.4 (via: Agda-2.6.0 tagged-0.8.5
>> equivalence-0.3.1) (new version)
>> equivalence-0.3.1 (via: Agda-2.6.0) (reinstall) (changes:
>> transformers-compat-0.4.0.4 -> 0.5.1.4)
>> tagged-0.8.5 (via: semigroups-0.18.2) (new package)
>> semigroups-0.18.2 -bytestring-builder (via: Agda-2.6.0) (new package)
>> Agda-2.6.0 (new version)
>> cabal: The following packages are likely to be broken by the reinstalls:
>> Agda-2.5.1.1
>> Agda-2.5.1
>> Agda-2.4.2.5
>> Use --force-reinstalls if you want to install anyway.
>>
>> and I'm not sure I really want to run
>>
>> cabal install --program-suffix=-2.6.0 --force-reinstalls
>>
>>
>> in case cabal is right and my Agda-2.5.1.1 gets screwed up.
>>
>> Am I just being too faint hearted?
>>
>> Andy
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe