[Agda] Version mixup

[Philip Wadler]

Aha! I wondered how to check what path Emacs is using. Answer below. Thank you for your help! Go well, -- P


exec-path is a variable defined in ‘C source code’.
Its value is
("/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/bin" "/bin" "/usr/sbin" "/sbin" "/Applications/Aquamacs.app/Contents/MacOS/libexec" "/Applications/Aquamacs.app/Contents/MacOS/bin" "/usr/texbin" "/usr/local/texlive/2022/bin" "/usr/local/texlive/2021/bin" "/usr/local/texlive/2019/bin" "/usr/local/texlive/2008/bin")

Original value was
("/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/bin" "/bin" "/usr/sbin" "/sbin" "/usr/texbin" "/Library/TeX/texbin" "/usr/local/texlive/2022/bin" "/usr/local/texlive/2021/bin" "/usr/local/texlive/2019/bin" "/usr/local/texlive/2008/bin" "/Applications/Aquamacs.app/Contents/MacOS/libexec")


  This variable may be risky if used as a file-local variable.

Documentation:
List of directories to search programs to run in subprocesses.
Each element is a string (directory name) or nil (try default directory).

By default the last element of this list is ‘exec-directory’. The
last element is not always used, for example in shell completion
(‘shell-dynamic-complete-command’).

You can customize this variable.


.   \ 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 16:38, 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 17:20, Philip Wadler wrote:
> Thanks! I tried what you suggested, but am still getting the same
> error message.
>
>   Could not find agda-mode-2.6.2.2
>
> Listing from the call to cabal appears below, for completeness, along
> with my current $PATH.

Please also check what the value of the Emacs variable exec-path is:

   C-h v exec-path RET

--
/NAD
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/84d1a5ca/attachment.html>