<div dir="ltr">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<div><br></div><div><a href="https://plfa.github.io/GettingStarted/">https://plfa.github.io/GettingStarted/</a><br></div><div><p style="margin:0px 0px 15px;padding:0px;color:rgb(17,17,17);font-family:-apple-system,system-ui,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)">Finally, we need to let Agda know where to find the standard library. For this, you can follow the instructions <a href="https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html#example-using-the-standard-library" style="color:rgb(23,86,169);text-decoration-line:none">here</a>.</p><p style="margin:0px 0px 15px;padding:0px;color:rgb(17,17,17);font-family:-apple-system,system-ui,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)">[<a href="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</a>]<br></p><p style="margin:0px 0px 15px;padding:0px;color:rgb(17,17,17);font-family:-apple-system,system-ui,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)">It is possible to set up PLFA as an Agda library as well. If you want to complete the exercises found in the <code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">courses</code> folder, or to import modules from the book, you need to do this. To do so, add the path to <code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">plfa.agda-lib</code> to <code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">~/.agda/libraries</code> and add <code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">plfa</code> to <code class="gmail-language-plaintext gmail-highlighter-rouge" style="font-size:0.85em;border:1px solid rgb(232,232,232);border-radius:3px;background-color:rgb(238,238,255);padding:1px 5px;font-family:mononoki,"DejaVu Sans Mono","Source Code Pro","Bitstream Vera Sans Mono",FreeMono,"Courier New",Monaco,Menlo,monospace,serif;white-space:pre">~/.agda/defaults</code>, both on lines of their own.</p><p style="margin:0px 0px 15px;padding:0px;color:rgb(17,17,17);font-family:-apple-system,system-ui,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;background-color:rgb(253,253,253)"><br></p><div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div></div></div></div></div></div></div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, 12 Apr 2020 at 09:42, Michel Levy <<a href="mailto:michel.levy.imag@free.fr">michel.levy.imag@free.fr</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Excuse me. I have already found a solution to my problem :<br>
<br>
1) Create the missing file "standard-library.agda-lib in the directory<br>
of the standard library<br>
<br>
2) Create the directory "my_home/.agda. In the file libraries write the<br>
path to the two files agda-lib. In the defauts file, write plfa and<br>
standard-library.<br>
<br>
Le 12/04/2020 à 14:24, Michel Levy a écrit :<br>
> I'm trying to write all the PLFA exercises.  But I have a problem<br>
> installing the pfla library.<br>
> More exactly the standard library is usable without "my home/.agda"<br>
> directory. This library doesn't have a "standard-library.agda-lib" file.<br>
> When I create a ".agda" directory with only the plfa library, I lose<br>
> access to the standard library.<br>
> This library doesn't have a "standard-library.agda-lib" file.<br>
> When I create a "my home/.agda" directory with only the plfa library, I<br>
> lose access to the standard library.<br>
> What do I have to do to get both standard and plfa libraries?<br>
><br>
> PS : my agda version is 2.5.3 installed with the Ubuntu packages.<br>
><br>
-- <br>
courriel : <a href="mailto:michel.levy.imag@free.fr" target="_blank">michel.levy.imag@free.fr</a><br>
mobile : 06 59 13 42 53<br>
web : <a href="http://michel.levy.imag.free.fr" rel="noreferrer" target="_blank">michel.levy.imag.free.fr</a><br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>