A package manager for Agda
Project description
agda-pkg
Agda-Pkg is a tool to manage Agda libraries with extra features like
installing libraries from different kind of sources. This tool does
not modify Agda
at all, it just manages systematically the directory
.agda
and the files: .agda/defaults
and .agda/libraries
used by
Agda to locate libraries. For more information about how Agda package
system works, please read the official documentation
here.
We have indexed in
agda/package-index some agda
libraries available on Github. We can install them with agda-pkg install LibraryName
.
$ apkg list
Library name Latest version URL
-----------------------------------------------------------------------------------------------------
agda-categories 026658c https://github.com/agda/agda-categories.git
agda-metis v0.2.1 https://github.com/jonaprieto/agda-metis.git
agda-prelude 64b0eb2 https://github.com/UlfNorell/agda-prelude.git
agda-prop v0.1.2 https://github.com/jonaprieto/agda-prop.git
agda-ring-solver d1ed21c https://github.com/oisdk/agda-ring-solver.git
agdarsec v0.1.1 https://github.com/gallais/agdarsec.git
alga-theory 0fdb96c https://github.com/algebraic-graphs/agda.git
ataca a9a7c06 https://github.com/jespercockx/ataca.git
cat v1.6.0 https://github.com/fredefox/cat.git
cubical v0.1 https://github.com/agda/cubical.git
FiniteSets c8c2600 https://github.com/L-TChen/FiniteSets.git
fotc apia-1.0.2 https://github.com/asr/fotc.git
hott-core 1037d82 https://github.com/HoTT/HoTT-Agda.git
hott-theorems 1037d82 https://github.com/HoTT/HoTT-Agda.git
HoTT-UF-Agda 3bdfe5c https://github.com/martinescardo/HoTT-UF-Agda-Lecture-Notes.git
lightweight-prelude b2d440a https://github.com/L-TChen/agda-lightweight-prelude.git
MtacAR mtac1 https://github.com/L-TChen/MtacAR.git
plfa 1dfd02f https://github.com/plfa/plfa.github.io.git
routing-library thesis https://github.com/MatthewDaggitt/agda-routing.git
standard-library v1.0.1 https://github.com/agda/agda-stdlib.git
Table of contents
- Quick Start
- Usage
- Creating a library with Agda-Pkg
- About
Quick Start
To install agda-pkg
, you must have installed Python 3.6+
or a latter version
on your machine. In addition, the python package manager pip 18.0+
.
We have tested agda-pkg
with Agda v2.5.4+
.
Installing using pip
:
$ pip install agda-pkg
Now, we can run the package manager using the command agda-pkg
or even
shorter just apkg
.
Usage
Initialisation of the package index
The easiest way to get some libraries is by using the package index.
We will use this index to download and to install the libraries. In
addition, agda-pkg
uses a local database to maintain a register of
all libraries available in your system. To initialise the index and
the database please run the following command:
$ apkg init
Indexing libraries from https://github.com/agda/package-index.git
Note.
To use a different location for the files defaults
and libraries
for Agda,
you can set up the environment variable AGDA_DIR
as fallows.
$ export AGDA_DIR=$HOME/.agda
Other way is to create a directory .agda
in your directory and run
agda-pkg
from that directory. agda-pkg
will prioritize the .agda
directory in the current directory.
Help command
Check all the options of a command or subcommand by using the flag --help
.
$ apkg --help
$ apkg install --help
Upgrade the package index
Recall updating the index every once in a while using upgrade
.
$ apkg upgrade
Updating Agda-Pkg from https://github.com/agda/package-index.git
If you want to index your library go to the package index and make PR.
List all the packages available
To see all the packages available run the following command:
$ apkg list
This command also has the flag --full
to display a version of the
this list with more details.
Installation of packages
Install a library is now easy. We have multiple ways to install a package.
- from the package-index
$ apkg install standard-library
- from a local directory
$ apkg install .
or even much simpler:
$ apkg install
Installing a library creates a copy for agda in the directory assigned
by agda-pkg. If you want your current directory to be taken into
account for any changes use the --editable
option. as shown below.
$ apkg install --editable .
- from a github repository
$ apkg install --github agda/agda-stdlib --version v0.16
- from a git repository
$ apkg install http://github.com/jonaprieto/agda-prop.git
To specify the version of a library, we use the flag --version
$ apkg install standard-library --version v1.0
Or simpler by using @
or ==
as it follows.
$ apkg install standard-library@v1.0
$ apkg install standard-library==v1.0
Multiple packages at once
To install multiple libraries at once, we have two options:
- Using the inline method
$ apkg install standard-library agda-prop agda-metis
Use @
or ==
if you need a specific version, see above
examples.
- Using a requirement file:
Generate a requirement file using apkg freeze
:
$ apkg freeze > requirements.txt
$ cat requirements.txt
standard-library==v0.16
Now, use the flag -r
to install all the listed libraries
in this file:
$ apkg install -r requirements.txt
Check all the options of this command with the help information:
$ apkg install --help
Uninstalling a package
Uninstalling a package will remove the library from the visible libraries for Agda.
- using the name of the library
$ apkg uninstall standard-library
- infering the library name from the current directory
$ apkg uninstall .
And if we want to remove the library completely (the sources and
everything), we use the flag --remove-cache
.
$ apkg uninstall standard-library --remove-cache
Update a package to latest version
We can get the latest version of a package from the versions registered in the package-index.
- Update all the installed libraries:
$ apkg update
- Update a specific list of libraries. If some library is not installed, this command will installed the latest version of it.
$ apkg update standard-library agdarsec
See packages installed
$ apkg freeze
standard-library==v0.16
This command is useful to keep in a file the versions used for your project to install them later.
$ apkg freeze > requirements.txt
To install from this requirement file run this command.
$ apkg install < requirements.txt
Approximate search of packages
We make a search (approximate) by using keywords and title of the packages from the index. To perform such a search, see the following example:
$ apkg search metis
1 result in 0.0012656739999998834seg
cubical
url: https://github.com/agda/cubical.git
installed: False
Get all the information of a package
$ apkg info cubical
Creating a library for Agda-Pkg
In this section, we describe how to build a library.
To build a project using agda-pkg
, we just run the following command:
$ apkg create
Some questions are going to be prompted in order to create the necessary files for Agda and for Agda-Pkg.
The output is a folder like the following showed below.
Directory structure of an agda library
A common Agda library has the following structure:
$ tree -L 1 mylibrary/
mylibrary/
├── LICENSE
├── README.md
├── mylibrary.agda-lib
├── mylibrary.agda-pkg
├── src
└── test
2 directories, 3 files
.agda-lib library file
$ cat mylibrary.agda-lib
name: mylibrary -- Comment
depend: LIB1 LIB2
LIB3
LIB4
include: PATH1
PATH2
PATH3
.agda-pkg library file
This file only works for agda-pkg
. The idea of
this file is to provide more information about the
package, pretty similar to the cabal files in Haskell.
This file has priority over its version .agda-lib
.
$ cat mylibrary.agda-pkg
name: mylibrary
version: v0.0.1
author:
- AuthorName1
- AuthorName2
category: cat1, cat2, cat3
homepage: http://github.com/user/mylibrary
license: MIT
license-file: LICENSE.md
source-repository: http://github.com/user/mylibrary.git
tested-with: 2.6.0
description: Put here a description.
include:
- PATH1
- PATH2
- PATH3
depend:
- LIB1
- LIB2
- LIB3
- LIB4
About
This is a proof of concept of an Agda Package Manager. Any contribution or feedback to improve this work is very welcomed.
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Hashes for agda_pkg-0.1.44-py2.py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 7e409a466c42f6739f5ce4ff61edb6f875ce184478b1e08763fc34a4404c3bea |
|
MD5 | a4ef97b874182bc1379209e7aa89298e |
|
BLAKE2b-256 | 2f5194fd1d94b55f11eab7ef427e4c5faeadce25174c131b13e942018e98504f |