<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<div dir="ltr">Thanks!  I tried what you suggested, but am still getting the same error message.
<div><br>
</div>
<div>  <span style="color:rgb(80,0,80)">Could not find agda-mode-2.6.2.2</span></div>
<div><font color="#500050"><br>
</font></div>
<div><font color="#500050">Listing from the call to cabal appears below, for completeness, along with my current $PATH.</font></div>
<div><font color="#500050"><br>
</font></div>
<div><font color="#500050">Any help gratefully received! Go well, -- P</font></div>
<div><font color="#500050"><br>
</font></div>
<div><font color="#500050"><br>
</font></div>
<div><br>
</div>
<div>
<div>Last login: Mon Jun 27 20:55:02 on ttys000<br>
rambla$ cabal install Agda-2.6.2.2 --program-suffix=-2.6.2.2<br>
Resolving dependencies...<br>
Build profile: -w ghc-8.10.7 -O1<br>
In order, the following will be built (use -v for more details):<br>
 - STMonadTrans-0.4.6 (lib) (requires build)<br>
 - boxes-0.1.5 (lib) (requires build)<br>
 - edit-distance-0.2.2.1 (lib) (requires build)<br>
 - data-hash-0.2.0.1 (lib) (requires build)<br>
 - gitrev-1.3.1 (lib) (requires build)<br>
 - hashtables-1.3 (lib) (requires build)<br>
 - alex-3.2.7.1 (exe:alex) (requires build)<br>
 - murmur-hash-0.1.0.10 (lib) (requires build)<br>
 - parallel-3.2.2.0 (lib) (requires build)<br>
 - uri-encode-1.5.0.7 (lib) (requires build)<br>
 - regex-base-0.94.0.2 (lib) (requires build)<br>
 - aeson-2.1.0.0 (lib) (requires build)<br>
 - transformers-base-0.4.6 (lib) (requires build)<br>
 - equivalence-0.4.0.1 (lib) (requires build)<br>
 - regex-tdfa-1.3.1.2 (lib) (requires build)<br>
 - monad-control-1.0.3.1 (lib) (requires build)<br>
 - Agda-2.6.2.2 (lib:Agda, exe:agda, exe:agda-mode) (requires build)<br>
Starting     boxes-0.1.5 (lib)<br>
Starting     STMonadTrans-0.4.6 (lib)<br>
Starting     edit-distance-0.2.2.1 (lib)<br>
Starting     data-hash-0.2.0.1 (lib)<br>
Building     STMonadTrans-0.4.6 (lib)<br>
Building     boxes-0.1.5 (lib)<br>
Building     edit-distance-0.2.2.1 (lib)<br>
Building     data-hash-0.2.0.1 (lib)<br>
Haddock      boxes-0.1.5 (lib)<br>
Haddock      data-hash-0.2.0.1 (lib)<br>
Installing   boxes-0.1.5 (lib)<br>
Completed    boxes-0.1.5 (lib)<br>
Starting     gitrev-1.3.1 (lib)<br>
Installing   data-hash-0.2.0.1 (lib)<br>
Completed    data-hash-0.2.0.1 (lib)<br>
Starting     hashtables-1.3 (lib)<br>
Building     gitrev-1.3.1 (lib)<br>
Building     hashtables-1.3 (lib)<br>
Haddock      gitrev-1.3.1 (lib)<br>
Haddock      STMonadTrans-0.4.6 (lib)<br>
Installing   gitrev-1.3.1 (lib)<br>
Haddock      edit-distance-0.2.2.1 (lib)<br>
Completed    gitrev-1.3.1 (lib)<br>
Starting     alex-3.2.7.1 (exe:alex)<br>
Installing   STMonadTrans-0.4.6 (lib)<br>
Installing   edit-distance-0.2.2.1 (lib)<br>
Completed    STMonadTrans-0.4.6 (lib)<br>
Starting     murmur-hash-0.1.0.10 (lib)<br>
Completed    edit-distance-0.2.2.1 (lib)<br>
Starting     parallel-3.2.2.0 (lib)<br>
Building     alex-3.2.7.1 (exe:alex)<br>
Building     murmur-hash-0.1.0.10 (lib)<br>
Building     parallel-3.2.2.0 (lib)<br>
Haddock      murmur-hash-0.1.0.10 (lib)<br>
Installing   murmur-hash-0.1.0.10 (lib)<br>
Completed    murmur-hash-0.1.0.10 (lib)<br>
Starting     uri-encode-1.5.0.7 (lib)<br>
Haddock      parallel-3.2.2.0 (lib)<br>
Building     uri-encode-1.5.0.7 (lib)<br>
Installing   parallel-3.2.2.0 (lib)<br>
Completed    parallel-3.2.2.0 (lib)<br>
Starting     regex-base-0.94.0.2 (lib)<br>
Haddock      uri-encode-1.5.0.7 (lib)<br>
Installing   uri-encode-1.5.0.7 (lib)<br>
Building     regex-base-0.94.0.2 (lib)<br>
Completed    uri-encode-1.5.0.7 (lib)<br>
Starting     aeson-2.1.0.0 (lib)<br>
Building     aeson-2.1.0.0 (lib)<br>
Installing   alex-3.2.7.1 (exe:alex)<br>
Completed    alex-3.2.7.1 (exe:alex)<br>
Starting     transformers-base-0.4.6 (lib)<br>
Building     transformers-base-0.4.6 (lib)<br>
Haddock      regex-base-0.94.0.2 (lib)<br>
Installing   regex-base-0.94.0.2 (lib)<br>
Haddock      transformers-base-0.4.6 (lib)<br>
Completed    regex-base-0.94.0.2 (lib)<br>
Starting     equivalence-0.4.0.1 (lib)<br>
Installing   transformers-base-0.4.6 (lib)<br>
Completed    transformers-base-0.4.6 (lib)<br>
Starting     regex-tdfa-1.3.1.2 (lib)<br>
Building     equivalence-0.4.0.1 (lib)<br>
Haddock      hashtables-1.3 (lib)<br>
Building     regex-tdfa-1.3.1.2 (lib)<br>
Installing   hashtables-1.3 (lib)<br>
Completed    hashtables-1.3 (lib)<br>
Starting     monad-control-1.0.3.1 (lib)<br>
Building     monad-control-1.0.3.1 (lib)<br>
Haddock      equivalence-0.4.0.1 (lib)<br>
Installing   equivalence-0.4.0.1 (lib)<br>
Completed    equivalence-0.4.0.1 (lib)<br>
Haddock      monad-control-1.0.3.1 (lib)<br>
Installing   monad-control-1.0.3.1 (lib)<br>
Completed    monad-control-1.0.3.1 (lib)<br>
Haddock      regex-tdfa-1.3.1.2 (lib)<br>
Installing   regex-tdfa-1.3.1.2 (lib)<br>
Completed    regex-tdfa-1.3.1.2 (lib)<br>
Haddock      aeson-2.1.0.0 (lib)<br>
Installing   aeson-2.1.0.0 (lib)<br>
Completed    aeson-2.1.0.0 (lib)<br>
Starting     Agda-2.6.2.2 (all, legacy fallback)<br>
Building     Agda-2.6.2.2 (all, legacy fallback)<br>
Haddock      Agda-2.6.2.2 (all, legacy fallback)<br>
Installing   Agda-2.6.2.2 (all, legacy fallback)<br>
Completed    Agda-2.6.2.2 (all, legacy fallback)<br>
Symlinking 'agda' to '/Users/wadler/.cabal/bin/agda-2.6.2.2'<br>
Symlinking 'agda-mode' to '/Users/wadler/.cabal/bin/agda-mode-2.6.2.2'<br>
rambla$ agda --version<br>
Agda version 2.6.2.2<br>
</div>
<div>
<div>rambla$ echo $PATH<br>
/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/<a href="http://CoqIDE_8.10.2.app/Contents/Resources/bin/">CoqIDE_8.10.2.app/Contents/Resources/bin/</a>:<br>
rambla$</div>
<div> </div>
</div>
<div><br clear="all">
<div>
<div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature">
<div dir="ltr">
<div>
<div dir="ltr">
<div dir="ltr">
<div>
<div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>
.   /\ School of Informatics, University of Edinburgh<br>
</div>
<div>.  /  \ and Senior Research Fellow, IOHK<br>
</div>
<div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div>
</div>
<div dir="ltr"><br>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
<br>
</div>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Tue, 28 Jun 2022 at 06:56, Nils Anders Danielsson <<a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a>> wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
This email was sent to you by someone outside the University.<br>
You should only click on links or attachments if you are certain that the email is genuine and the content is safe.<br>
<br>
On 2022-06-28 02:02, Philip Wadler wrote:<br>
> I've installed a new version of Agda (2.6.2.2), but emacs agda mode<br>
> keeps using an older version (2.6.1.1).<br>
<br>
Perhaps the binaries for Agda 2.6.2.2 did not end up on your PATH.<br>
<br>
> Using the "Switch to another version of Agda" option with Version<br>
> 2.6.2.2 gives the error message:<br>
>      Could not find agda-mode-2.6.2.2<br>
<br>
This command looks for "agda-mode-<version>". If you want to use this<br>
command, then you can for instance install Agda using something like<br>
"cabal install Agda-2.6.2.2 --program-suffix=-2.6.2.2" (assuming that<br>
the binaries end up on your PATH). Note that the Emacs mode by default<br>
uses "agda-mode", without a suffix, even if you used the "Switch to<br>
another version of Agda" command the last time you used Emacs.<br>
<br>
--<br>
/NAD<br>
</blockquote>
</div>
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.
</body>
</html>