[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.
Thanks,
Jason
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-2.6.2.2
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-2.6.2.2 --program-suffix=-2.6.2.2
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-0.2.2.1 (lib) (requires build)
- data-hash-0.2.0.1 (lib) (requires build)
- gitrev-1.3.1 (lib) (requires build)
- hashtables-1.3 (lib) (requires build)
- alex-3.2.7.1 (exe:alex) (requires build)
- murmur-hash-0.1.0.10 (lib) (requires build)
- parallel-3.2.2.0 (lib) (requires build)
- uri-encode-1.5.0.7 (lib) (requires build)
- regex-base-0.94.0.2 (lib) (requires build)
- aeson-2.1.0.0 (lib) (requires build)
- transformers-base-0.4.6 (lib) (requires build)
- equivalence-0.4.0.1 (lib) (requires build)
- regex-tdfa-1.3.1.2 (lib) (requires build)
- monad-control-1.0.3.1 (lib) (requires build)
- Agda-2.6.2.2 (lib:Agda, exe:agda, exe:agda-mode) (requires build)
Starting boxes-0.1.5 (lib)
Starting STMonadTrans-0.4.6 (lib)
Starting edit-distance-0.2.2.1 (lib)
Starting data-hash-0.2.0.1 (lib)
Building STMonadTrans-0.4.6 (lib)
Building boxes-0.1.5 (lib)
Building edit-distance-0.2.2.1 (lib)
Building data-hash-0.2.0.1 (lib)
Haddock boxes-0.1.5 (lib)
Haddock data-hash-0.2.0.1 (lib)
Installing boxes-0.1.5 (lib)
Completed boxes-0.1.5 (lib)
Starting gitrev-1.3.1 (lib)
Installing data-hash-0.2.0.1 (lib)
Completed data-hash-0.2.0.1 (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-0.2.2.1 (lib)
Completed gitrev-1.3.1 (lib)
Starting alex-3.2.7.1 (exe:alex)
Installing STMonadTrans-0.4.6 (lib)
Installing edit-distance-0.2.2.1 (lib)
Completed STMonadTrans-0.4.6 (lib)
Starting murmur-hash-0.1.0.10 (lib)
Completed edit-distance-0.2.2.1 (lib)
Starting parallel-3.2.2.0 (lib)
Building alex-3.2.7.1 (exe:alex)
Building murmur-hash-0.1.0.10 (lib)
Building parallel-3.2.2.0 (lib)
Haddock murmur-hash-0.1.0.10 (lib)
Installing murmur-hash-0.1.0.10 (lib)
Completed murmur-hash-0.1.0.10 (lib)
Starting uri-encode-1.5.0.7 (lib)
Haddock parallel-3.2.2.0 (lib)
Building uri-encode-1.5.0.7 (lib)
Installing parallel-3.2.2.0 (lib)
Completed parallel-3.2.2.0 (lib)
Starting regex-base-0.94.0.2 (lib)
Haddock uri-encode-1.5.0.7 (lib)
Installing uri-encode-1.5.0.7 (lib)
Building regex-base-0.94.0.2 (lib)
Completed uri-encode-1.5.0.7 (lib)
Starting aeson-2.1.0.0 (lib)
Building aeson-2.1.0.0 (lib)
Installing alex-3.2.7.1 (exe:alex)
Completed alex-3.2.7.1 (exe:alex)
Starting transformers-base-0.4.6 (lib)
Building transformers-base-0.4.6 (lib)
Haddock regex-base-0.94.0.2 (lib)
Installing regex-base-0.94.0.2 (lib)
Haddock transformers-base-0.4.6 (lib)
Completed regex-base-0.94.0.2 (lib)
Starting equivalence-0.4.0.1 (lib)
Installing transformers-base-0.4.6 (lib)
Completed transformers-base-0.4.6 (lib)
Starting regex-tdfa-1.3.1.2 (lib)
Building equivalence-0.4.0.1 (lib)
Haddock hashtables-1.3 (lib)
Building regex-tdfa-1.3.1.2 (lib)
Installing hashtables-1.3 (lib)
Completed hashtables-1.3 (lib)
Starting monad-control-1.0.3.1 (lib)
Building monad-control-1.0.3.1 (lib)
Haddock equivalence-0.4.0.1 (lib)
Installing equivalence-0.4.0.1 (lib)
Completed equivalence-0.4.0.1 (lib)
Haddock monad-control-1.0.3.1 (lib)
Installing monad-control-1.0.3.1 (lib)
Completed monad-control-1.0.3.1 (lib)
Haddock regex-tdfa-1.3.1.2 (lib)
Installing regex-tdfa-1.3.1.2 (lib)
Completed regex-tdfa-1.3.1.2 (lib)
Haddock aeson-2.1.0.0 (lib)
Installing aeson-2.1.0.0 (lib)
Completed aeson-2.1.0.0 (lib)
Starting Agda-2.6.2.2 (all, legacy fallback)
Building Agda-2.6.2.2 (all, legacy fallback)
Haddock Agda-2.6.2.2 (all, legacy fallback)
Installing Agda-2.6.2.2 (all, legacy fallback)
Completed Agda-2.6.2.2 (all, legacy fallback)
Symlinking 'agda' to '/Users/wadler/.cabal/bin/agda-2.6.2.2'
Symlinking 'agda-mode' to '/Users/wadler/.cabal/bin/agda-mode-2.6.2.2'
rambla$ agda --version
Agda version 2.6.2.2
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/>:
rambla$
. \ 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 (2.6.2.2), but emacs agda mode
> keeps using an older version (2.6.1.1).
Perhaps the binaries for Agda 2.6.2.2 did not end up on your PATH.
> Using the "Switch to another version of Agda" option with Version
> 2.6.2.2 gives the error message:
> Could not find agda-mode-2.6.2.2
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-2.6.2.2 --program-suffix=-2.6.2.2" (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.
--
/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/c61bb157/attachment-0001.html>
More information about the Agda
mailing list