I'm working with the development version of agda, which is now incompatible with the basic standard library version 1.3.
wmacmil@w:~/.agda$ agda --version
Agda version 2.6.2-41b6b25
A basic failure.agda file,
module failure where
open import Data.String
fails:
Checking failure (/home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_files/failure.agda).
Checking Data.String (/home/wmacmil/agdaStdLib/agda-stdlib-1.3/src/Data/String.agda).
Checking Data.String.Base (/home/wmacmil/agdaStdLib/agda-stdlib-1.3/src/Data/String/Base.agda).
Checking Data.List.Extrema (/home/wmacmil/agdaStdLib/agda-stdlib-1.3/src/Data/List/Extrema.agda).
Checking Data.List.Membership.Propositional.Properties (/home/wmacmil/agdaStdLib/agda-stdlib-1.3/src/Data/List/Membership/Propositional/Properties.agda).
Checking Data.List.Membership.Setoid.Properties (/home/wmacmil/agdaStdLib/agda-stdlib-1.3/src/Data/List/Membership/Setoid/Properties.agda).
Killed
How can I run two version at once? And how can I run the experimental version of of the stdlib to avoid this? Are there any other tricks someone would suggest?
Also, will someone with >1500 reputation make agda-stdlib a tag?
As noted in the description of the standard library, you need to use the experimental
branch of the library if you are working with the master
branch of Agda. You can get it by cloning the github repository at https://github.com/agda/agda-stdlib
and doing git checkout experimental
.
To automatically switch between versions of libraries when you switch Agda versions, you can have multiple libraries
files as described in the user manual:
To be found by Agda a library file has to be listed (with its full path) in a libraries file
AGDA_DIR/libraries-VERSION, or if that doesn’t exist AGDA_DIR/libraries
where VERSION is the Agda version (for instance 2.5.1). The AGDA_DIR defaults to ~/.agda on unix-like systems and C:\Users\USERNAME\AppData\Roaming\agda or similar on Windows, and can be overridden by setting the AGDA_DIR environment variable.
Alternatively, you can have a single libraries
file and check out the right version of the library when you switch Agda versions.