[Agda] how to reference to a version

[Ulf Norell]

I was referring to $HOME/.agda/libraries.

See here for more information:

https://agda.readthedocs.io/en/latest/tools/package-system.html

/ Ulf

On Thu, Dec 8, 2016 at 10:03 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> On Thu, 2016-12-08 at 21:43 +0100, Ulf Norell wrote:
> > You just need to put the path to the .agda-lib file in
> > your .agda/libraries file.
> > No further installation should be required.
> >
>
> I see   agda/standard-library.agda-lib
>
> but do not see  .agda/libraries
> anywhere.
>
> On the other hand, I use  $adgaStLib  in the command line
> that points to            agda/std-lib/src,
> and it seems working.
> (?)
>
> ------
> Sergei
>
>
> > On Thu, Dec 8, 2016 at 9:09 PM, Sergei Meshveliani <mechvel at botik.ru>
> > wrote:
> >         On Thu, 2016-12-08 at 22:43 +0300, Sergei Meshveliani wrote:
> >         > On Thu, 2016-12-08 at 19:30 +0100, Ulf Norell wrote:
> >         > > Each commit of Agda contains a reference to the particular
> >         commit of
> >         > > the standard library
> >         > > that it has been tested with. To find out which one you
> >         can do the
> >         > > following (after checking
> >         > >
> >         > > out the commit of Agda that you are interested in):
> >         > >
> >         > >
> >         > > $ git submodule init
> >         > > Submodule 'std-lib' (https://github.com/agda/agda-stdlib)
> >         registered
> >         > > for path 'std-lib'
> >         > > $ git submodule update
> >         > > Cloning into 'std-lib'...
> >         > > Submodule path 'std-lib': checked out
> >         > > '7220ca3ee025e9339aa8e5d11efcd069764e7977'
> >         > > $ cd std-lib
> >         > > $ git status
> >         > > HEAD detached at 7220ca3
> >         > >
> >         > >
> >         > > So the commit of the standard library that works with the
> >         Agda commit
> >         > > I tested this on is
> >         > > 7220ca3. This is probably the easiest way for your users
> >         to get a
> >         > > compatible version of
> >         > > the standard library as well, saving them the trouble of
> >         keeping track
> >         > > of two commit hashes.
> >         > >
> >         >
> >         >
> >         > I am trying to find out what is the whole installation
> >         process.
> >         >
> >         > For example, I have downloaded  agda-2.5.2-dc9ffae
> >         > by running the commands
> >         >
> >         >   > git clone https://github.com/agda/agda.git
> >         >   > cd agda
> >         >   > git checkout dc9ffae
> >         >
> >         > Then I install Agda by
> >         >
> >         >   > cabal update
> >         >   > cabal install
> >         >   > agda-mode compile
> >         >
> >         > Then I need to download the needed Standard library version.
> >         > To do this, I command
> >         >
> >         >   > cd agda
> >         >   > git submodule init
> >         >   Submodule 'std-lib' (https://github.com/agda/agda-stdlib)
> >         >   registered for path 'std-lib'
> >         >
> >         >   > git submodule update
> >         >   Cloning into std-lib...
> >         >   ...
> >         >   Submodule path 'std-lib': checked out
> >         >   '7220ca3ee025e9339aa8e5d11efcd069764e7977'
> >         >
> >         >   > cd std-lib
> >         >
> >         > Initially this directory was empty. And now is has the files
> >         of the
> >         > needed library version.
> >         > Right?
> >         >
> >         > To install the library, I command
> >         >
> >         >   > cabal install
> >
> >
> >
> >         But there is not any .cabal file.
> >         And I have an impression that
> >
> >           > git submodule update
> >
> >         has already installed the needed library.
> >
> >         ------
> >         Sergei
> >
> >         _______________________________________________
> >         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/20161208/b39b3c6f/attachment-0001.html