[Agda] Version mixup

Jason Hu fdhzs2010 at hotmail.com
Tue Jun 28 17:48:53 CEST 2022

Hi Phil,

Maybe you can check what is the current version of your agda-mode?

Just to provide another perspective, I have done the following and I have multiple versions of Agda running. So far I have experienced no problem with different Agda versions:

  1.  In Agda’s git repo, switch to the version you want to install.
  2.  Install Agda using `stack install`.
  3.  Stack will put all Agda binaries in ~/.local/bin. Remember to add this path to $PATH if it’s not already there. Also remember to add it to Emacs’ path.
  4.  Go to ~/.local/bin and copy agda to agda-VERSION and agda-mode to agda-mode-VERSION.
  5.  Then you can switch among versions in Emacs.
  6.  As a bonus, you can also setup libraries file in ~/.agda so that different Agda version looks up different libraries.


From: Philip Wadler<mailto:wadler at inf.ed.ac.uk>
Sent: Tuesday, June 28, 2022 11:21 AM
To: Nils Anders Danielsson<mailto:nad at cse.gu.se>
Cc: Agda mailing list<mailto:agda at lists.chalmers.se>
Subject: Re: [Agda] Version mixup

Thanks!  I tried what you suggested, but am still getting the same error message.

  Could not find agda-mode-

Listing from the call to cabal appears below, for completeness, along with my current $PATH.

Any help gratefully received! Go well, -- P

Last login: Mon Jun 27 20:55:02 on ttys000
rambla$ cabal install Agda- --program-suffix=-
Resolving dependencies...
Build profile: -w ghc-8.10.7 -O1
In order, the following will be built (use -v for more details):
 - STMonadTrans-0.4.6 (lib) (requires build)
 - boxes-0.1.5 (lib) (requires build)
 - edit-distance- (lib) (requires build)
 - data-hash- (lib) (requires build)
 - gitrev-1.3.1 (lib) (requires build)
 - hashtables-1.3 (lib) (requires build)
 - alex- (exe:alex) (requires build)
 - murmur-hash- (lib) (requires build)
 - parallel- (lib) (requires build)
 - uri-encode- (lib) (requires build)
 - regex-base- (lib) (requires build)
 - aeson- (lib) (requires build)
 - transformers-base-0.4.6 (lib) (requires build)
 - equivalence- (lib) (requires build)
 - regex-tdfa- (lib) (requires build)
 - monad-control- (lib) (requires build)
 - Agda- (lib:Agda, exe:agda, exe:agda-mode) (requires build)
Starting     boxes-0.1.5 (lib)
Starting     STMonadTrans-0.4.6 (lib)
Starting     edit-distance- (lib)
Starting     data-hash- (lib)
Building     STMonadTrans-0.4.6 (lib)
Building     boxes-0.1.5 (lib)
Building     edit-distance- (lib)
Building     data-hash- (lib)
Haddock      boxes-0.1.5 (lib)
Haddock      data-hash- (lib)
Installing   boxes-0.1.5 (lib)
Completed    boxes-0.1.5 (lib)
Starting     gitrev-1.3.1 (lib)
Installing   data-hash- (lib)
Completed    data-hash- (lib)
Starting     hashtables-1.3 (lib)
Building     gitrev-1.3.1 (lib)
Building     hashtables-1.3 (lib)
Haddock      gitrev-1.3.1 (lib)
Haddock      STMonadTrans-0.4.6 (lib)
Installing   gitrev-1.3.1 (lib)
Haddock      edit-distance- (lib)
Completed    gitrev-1.3.1 (lib)
Starting     alex- (exe:alex)
Installing   STMonadTrans-0.4.6 (lib)
Installing   edit-distance- (lib)
Completed    STMonadTrans-0.4.6 (lib)
Starting     murmur-hash- (lib)
Completed    edit-distance- (lib)
Starting     parallel- (lib)
Building     alex- (exe:alex)
Building     murmur-hash- (lib)
Building     parallel- (lib)
Haddock      murmur-hash- (lib)
Installing   murmur-hash- (lib)
Completed    murmur-hash- (lib)
Starting     uri-encode- (lib)
Haddock      parallel- (lib)
Building     uri-encode- (lib)
Installing   parallel- (lib)
Completed    parallel- (lib)
Starting     regex-base- (lib)
Haddock      uri-encode- (lib)
Installing   uri-encode- (lib)
Building     regex-base- (lib)
Completed    uri-encode- (lib)
Starting     aeson- (lib)
Building     aeson- (lib)
Installing   alex- (exe:alex)
Completed    alex- (exe:alex)
Starting     transformers-base-0.4.6 (lib)
Building     transformers-base-0.4.6 (lib)
Haddock      regex-base- (lib)
Installing   regex-base- (lib)
Haddock      transformers-base-0.4.6 (lib)
Completed    regex-base- (lib)
Starting     equivalence- (lib)
Installing   transformers-base-0.4.6 (lib)
Completed    transformers-base-0.4.6 (lib)
Starting     regex-tdfa- (lib)
Building     equivalence- (lib)
Haddock      hashtables-1.3 (lib)
Building     regex-tdfa- (lib)
Installing   hashtables-1.3 (lib)
Completed    hashtables-1.3 (lib)
Starting     monad-control- (lib)
Building     monad-control- (lib)
Haddock      equivalence- (lib)
Installing   equivalence- (lib)
Completed    equivalence- (lib)
Haddock      monad-control- (lib)
Installing   monad-control- (lib)
Completed    monad-control- (lib)
Haddock      regex-tdfa- (lib)
Installing   regex-tdfa- (lib)
Completed    regex-tdfa- (lib)
Haddock      aeson- (lib)
Installing   aeson- (lib)
Completed    aeson- (lib)
Starting     Agda- (all, legacy fallback)
Building     Agda- (all, legacy fallback)
Haddock      Agda- (all, legacy fallback)
Installing   Agda- (all, legacy fallback)
Completed    Agda- (all, legacy fallback)
Symlinking 'agda' to '/Users/wadler/.cabal/bin/agda-'
Symlinking 'agda-mode' to '/Users/wadler/.cabal/bin/agda-mode-'
rambla$ agda --version
Agda version
rambla$ echo $PATH
/Users/wadler/.rbenv/shims:/Users/wadler/.cabal/bin:/Users/wadler/.ghcup/bin:/usr/local/opt/ruby/bin:/usr/local/lib/ruby/gems/3.0.0/bin:/Users/wadler/.local/bin:/Users/wadler/.ghcup/env:/usr/texbin:/opt/local/bin:/opt/local/sbin:/usr/local/go/bin/:/Users/wadler/.elan/bin:/usr/local/bin:/usr/bin:/bin:/usr/sbin:/sbin:/Library/TeX/texbin:/usr/local/go/bin:/usr/local/MacGPG2/bin:/Library/Apple/usr/bin:/usr/local/pgsql/bin:/Applications/PLT Scheme v4.1.3/bin:/Users/wadler/Library/Haskell/ghc-7.6.3/lib/lhs2tex-1.18.1/bin:/Applications/sbt/bin/:/Users/wadler/Library/Haskell/ghc-8.2.2/lib/happy-1.19.8/bin:/Users/wadler/Library/Haskell/ghc-8.2.2/lib/alex-3.2.3/bin:/Applications/CoqIDE_8.10.2.app/Contents/Resources/bin/<http://CoqIDE_8.10.2.app/Contents/Resources/bin/>:

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

On Tue, 28 Jun 2022 at 06:56, Nils Anders Danielsson <nad at cse.gu.se<mailto:nad at cse.gu.se>> wrote:
This email was sent to you by someone outside the University.
You should only click on links or attachments if you are certain that the email is genuine and the content is safe.

On 2022-06-28 02:02, Philip Wadler wrote:
> I've installed a new version of Agda (, but emacs agda mode
> keeps using an older version (

Perhaps the binaries for Agda did not end up on your PATH.

> Using the "Switch to another version of Agda" option with Version
> gives the error message:
>      Could not find agda-mode-

This command looks for "agda-mode-<version>". If you want to use this
command, then you can for instance install Agda using something like
"cabal install Agda- --program-suffix=-" (assuming that
the binaries end up on your PATH). Note that the Emacs mode by default
uses "agda-mode", without a suffix, even if you used the "Switch to
another version of Agda" command the last time you used Emacs.

The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220628/c61bb157/attachment-0001.html>

More information about the Agda mailing list