[Agda] how to reference to a version

Sergei Meshveliani mechvel at botik.ru
Thu Dec 8 22:03:19 CET 2016


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
>         
> 
> 




More information about the Agda mailing list