Phantom arguments in functions [Re: [Agda] another possible without-K problem]

[Nils Anders Danielsson]

On 2013-07-10 21:09, Dan Licata wrote:
> Also: does anyone know if there is a nice way to install and switch
> between multiple versions of Agda? How would I have 2.3.2.1 from cabal
> and the devel version installed simultaneously?

It's easy if you don't use the Emacs mode:

   cabal install Agda
   cabal install Agda-2.3.2.1 --program-suffix=-2.3.2.1

Then agda gives you the development version, and agda-2.3.2.1 gives you
version 2.3.2.1.

Switching between different versions of Agda in Emacs is a bit trickier.
Two (untested) options:

* Fiddle with paths or symlinks to make sure that agda and agda-mode
   refer to the version you are interested in, and restart Emacs.

* Replace

     (load-file (let ((coding-system-for-read 'utf-8))
                     (shell-command-to-string "agda-mode locate")))

   in .emacs with

     (load-file (let ((coding-system-for-read 'utf-8))
                     (shell-command-to-string "agda-mode-2.3.2.1 locate")))

   (say), modify agda2-program-name so that it points to the right
   executable, and restart Emacs.

-- 
/NAD