[Agda] Load libraries based on version?

[Jason -Zhong Sheng- Hu]

Hi all,

thx Guillaume, I found it in the doc:

https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html#installing-libraries

I will try if it works.

Arjen, you are right. it's very good for projects, and submodule can make everything consistent. I should probably do it. but it would also be useful for a global configuration when the goal is to quickly try things out.

Thanks,
Jason Hu
https://hustmphrrr.github.io/
________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of a.j.rouvoet <a.j.rouvoet at gmail.com>
Sent: May 20, 2019 5:39 AM
To: agda at lists.chalmers.se
Subject: Re: [Agda] Load libraries based on version?

Alternatively you can checkout the libraries you need in your project in a `lib/` directory and use the project local `.agda-lib` file to
include the paths by default on the project's agda path:

name: example
include:
  ./src/
  ./lib/stdlib.agda/src/
  ./lib/cubical.agda/

This works really well and has the additional benefit to be self contained.

Arjen

On 5/19/19 8:39 PM, Jesper Cockx wrote:
This is currently not possible as far as I'm aware. You could try to just have different .agda folders and switch between them when you switch agda versions.

-- Jesper

On Sun, May 19, 2019 at 8:34 PM Jason -Zhong Sheng- Hu <fdhzs2010 at hotmail.com<mailto:fdhzs2010 at hotmail.com>> wrote:
Hi all,

since Agda and libraries aren't really in the most stable state, I figured it might be useful to use multiple versions of Agda for different things. My question is, is there a way to load libraries based on Agda's version? I am currently managing libraries using ~/.agda folder. It would be nice if somehow there are configuration files that can tell what version to load what.

Thanks,
Jason Hu
https://hustmphrrr.github.io/
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda



_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190520/cc0ed667/attachment.html>