[Agda] Installing standard and plfa libraries

[Philip Wadler]

Michel, I'm glad you are attempting PLFA. Did you follow the instructions
under Getting Started regarding libraries? If they don't work, we should
fix them. Go well, -- P

https://plfa.github.io/GettingStarted/

Finally, we need to let Agda know where to find the standard library. For
this, you can follow the instructions here
<https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html#example-using-the-standard-library>
.

[
https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html#example-using-the-standard-library
]

It is possible to set up PLFA as an Agda library as well. If you want to
complete the exercises found in the courses folder, or to import modules
from the book, you need to do this. To do so, add the path to plfa.agda-lib
 to ~/.agda/libraries and add plfa to ~/.agda/defaults, both on lines of
their own.


.   \ 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 Sun, 12 Apr 2020 at 09:42, Michel Levy <michel.levy.imag at free.fr> wrote:

> Excuse me. I have already found a solution to my problem :
>
> 1) Create the missing file "standard-library.agda-lib in the directory
> of the standard library
>
> 2) Create the directory "my_home/.agda. In the file libraries write the
> path to the two files agda-lib. In the defauts file, write plfa and
> standard-library.
>
> Le 12/04/2020 à 14:24, Michel Levy a écrit :
> > I'm trying to write all the PLFA exercises.  But I have a problem
> > installing the pfla library.
> > More exactly the standard library is usable without "my home/.agda"
> > directory. This library doesn't have a "standard-library.agda-lib" file.
> > When I create a ".agda" directory with only the plfa library, I lose
> > access to the standard library.
> > This library doesn't have a "standard-library.agda-lib" file.
> > When I create a "my home/.agda" directory with only the plfa library, I
> > lose access to the standard library.
> > What do I have to do to get both standard and plfa libraries?
> >
> > PS : my agda version is 2.5.3 installed with the Ubuntu packages.
> >
> --
> courriel : michel.levy.imag at free.fr
> mobile : 06 59 13 42 53
> web : michel.levy.imag.free.fr
>
> _______________________________________________
> Agda mailing list
> 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/20200412/85140a5e/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200412/85140a5e/attachment.ksh>