<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=Windows-1252">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:DengXian;
panose-1:2 1 6 0 3 1 1 1 1 1;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:"\@DengXian";
panose-1:2 1 6 0 3 1 1 1 1 1;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
p.MsoListParagraph, li.MsoListParagraph, div.MsoListParagraph
{mso-style-priority:34;
margin-top:0in;
margin-right:0in;
margin-bottom:0in;
margin-left:.5in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
.MsoChpDefault
{mso-style-type:export-only;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
/* List Definitions */
@list l0
{mso-list-id:2012828679;
mso-list-type:hybrid;
mso-list-template-ids:-1922920076 -1 67698713 67698715 67698703 67698713 67698715 67698703 67698713 67698715;}
@list l0:level1
{mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level2
{mso-level-number-format:alpha-lower;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level3
{mso-level-number-format:roman-lower;
mso-level-tab-stop:none;
mso-level-number-position:right;
text-indent:-9.0pt;}
@list l0:level4
{mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level5
{mso-level-number-format:alpha-lower;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level6
{mso-level-number-format:roman-lower;
mso-level-tab-stop:none;
mso-level-number-position:right;
text-indent:-9.0pt;}
@list l0:level7
{mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level8
{mso-level-number-format:alpha-lower;
mso-level-tab-stop:none;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level9
{mso-level-number-format:roman-lower;
mso-level-tab-stop:none;
mso-level-number-position:right;
text-indent:-9.0pt;}
ol
{margin-bottom:0in;}
ul
{margin-bottom:0in;}
--></style>
</head>
<body lang="EN-US" link="blue" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal">Hi Phil,</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Maybe you can check what is the current version of your agda-mode?</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">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:</p>
<p class="MsoNormal"><o:p> </o:p></p>
<ol style="margin-top:0in" start="1" type="1">
<li class="MsoListParagraph" style="margin-left:0in;mso-list:l0 level1 lfo1">In Agda’s git repo, switch to the version you want to install.</li><li class="MsoListParagraph" style="margin-left:0in;mso-list:l0 level1 lfo1">Install Agda using `stack install`.</li><li class="MsoListParagraph" style="margin-left:0in;mso-list:l0 level1 lfo1">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.</li><li class="MsoListParagraph" style="margin-left:0in;mso-list:l0 level1 lfo1">Go to ~/.local/bin and copy agda to agda-VERSION and agda-mode to agda-mode-VERSION.</li><li class="MsoListParagraph" style="margin-left:0in;mso-list:l0 level1 lfo1">Then you can switch among versions in Emacs.</li><li class="MsoListParagraph" style="margin-left:0in;mso-list:l0 level1 lfo1">As a bonus, you can also setup libraries file in ~/.agda so that different Agda version looks up different libraries.</li></ol>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Thanks,<o:p></o:p></p>
<p class="MsoNormal">Jason<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<div style="mso-element:para-border-div;border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0in 0in 0in">
<p class="MsoNormal" style="border:none;padding:0in"><b>From: </b><a href="mailto:wadler@inf.ed.ac.uk">Philip Wadler</a><br>
<b>Sent: </b>Tuesday, June 28, 2022 11:21 AM<br>
<b>To: </b><a href="mailto:nad@cse.gu.se">Nils Anders Danielsson</a><br>
<b>Cc: </b><a href="mailto:agda@lists.chalmers.se">Agda mailing list</a><br>
<b>Subject: </b>Re: [Agda] Version mixup</p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<p class="MsoNormal">Thanks! I tried what you suggested, but am still getting the same error message.
<o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"> <span style="color:#500050">Could not find agda-mode-2.6.2.2</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="color:#500050">Listing from the call to cabal appears below, for completeness, along with my current $PATH.</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><span style="color:#500050">Any help gratefully received! Go well, -- P</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<div>
<p class="MsoNormal">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<o:p></o:p></p>
</div>
<div>
<div>
<p class="MsoNormal">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$<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<p class="MsoNormal"><br clear="all">
<o:p></o:p></p>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>
. /\ School of Informatics, University of Edinburgh<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">. / \ and Senior Research Fellow, IOHK<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">. <a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">
http://homepages.inf.ed.ac.uk/wadler/</a><o:p></o:p></p>
</div>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal">On Tue, 28 Jun 2022 at 06:56, Nils Anders Danielsson <<a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a>> wrote:<o:p></o:p></p>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0in 0in 0in 6.0pt;margin-left:4.8pt;margin-right:0in">
<p class="MsoNormal">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<o:p></o:p></p>
</blockquote>
</div>
<p class="MsoNormal">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.
<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>