<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>