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 with .agda/defaults and .agda/libraries files used by
Agda to locate the available libraries. For more information about how Agda package
system works, please read the official documentation
here.
The most common usages of agda-pkg are the following:
Agda-pkg just run the following command:$ pip3 install agda-pkg
$ apkg install --editable .
$ apkg init
$ apkg install standard-library
A list of the available packages is shown below.
$ apkg install --github agda/agda-stdlib --version v1.3
$ apkg install --github plfa/plfa.github.io --branch dev --name plfa
The easiest way to install libraries is by using the package index.
agda-pkg uses a local database to maintain a register of all
libraries available in your system. To initialize 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 your agda files defaults
and libraries, you can set up the environment variable AGDA_DIR
before run apkg as follows:
$ 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.
Check all the options of a command or subcommand by using the flag --help.
$ apkg --help
$ apkg install --help
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.
If there is an issue with your installation or you suspect something is going wrong. You might want to see the environmental variables used by apkg.
$ apkg environment
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.
Install a library is now easy. We have multiple ways to install a package.
$ apkg install standard-library
$ 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 .
$ apkg install --github agda/agda-stdlib --version v1.1
$ 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
To install multiple libraries at once, we have two options:
$ apkg install standard-library agda-base
Use @ or == if you need a specific version, see above
examples.
Generate a requirement file using apkg freeze:
$ apkg freeze > requirements.txt
$ cat requirements.txt
standard-library==v1.1
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 will remove the library from the visible libraries for Agda.
$ apkg uninstall standard-library
$ 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
We can get the latest version of a package from the versions registered in the package-index.
$ apkg update
$ apkg update standard-library agdarsec
$ apkg freeze
standard-library==v1.1
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
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
$ apkg info cubical
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.
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
$ cat mylibrary.agda-lib
name: mylibrary -- Comment
depend: LIB1 LIB2
LIB3
LIB4
include: PATH1
PATH2
PATH3
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
A nix-shell environment that loads agda-pkg as well as agda and
agda-mode for Emacs is available. To use this, apkg can put the necessary
files in your project folder by running one of the following commands:
$ curl -L https://gist.github.com/jonaprieto/53e55263405ee48a831d700f27843931/download | tar -xvz --strip-components=1
or if you already have installed agda-pkg:
$ apkg nixos
Then, you will have the following files:
./hello-world.agda
./agda_requirements.txt
./shell.nix
./deps.nix
./emacs.nix
From where you can run the nix shell.
$ nix-shell
To launch Emacs with agda-mode enabled, run mymacs in the newly launched
shell; mymacs will also load your ~/.emacs file if it exists. If you are
using Spacemacs, you will need to edit shell.nix
to use ~/.spacemacs instead.
The files provided by the commands above are also available in this repository
(apkg/support/nix) and in a third-party example
repository to give an idea of exactly
which files need to be copied to your project.
Example:
$ cat hello-world.agda
module hello-world where
open import IO
main = run (putStrLn "Hello, World!")
Run mymacs hello-world.agda then type C-c C-x C-c in emacs to compile the loaded hello world file.
Edit any of the nix expressions as needed. In particular:
agda-pkg, edit agda_requirements.txtdeps.nix.myEmacs
references in shell.nix or add similar derivations..emacs_user_config in the repository root directory and
add any additional config, such as (setq agda2-backend "GHC") to use GHC by
default when compiling Agda files from emacs.This is a proof of concept of an Agda Package Manager. Contributions are always welcomed.
FAQs
A package manager for Agda
We found that agda-pkg demonstrated a healthy version release cadence and project activity because the last version was released less than a year ago. It has 1 open source maintainer collaborating on the project.
Did you know?
Socket for GitHub automatically highlights issues in each pull request and monitors the health of all your open source dependencies. Discover the contents of your packages and block harmful activity before you install or update your dependencies.
Security News
Research
The Socket Research Team breaks down a malicious wrapper package that uses obfuscation to harvest credentials and exfiltrate sensitive data.
Research
Security News
Attackers used a malicious npm package typosquatting a popular ESLint plugin to steal sensitive data, execute commands, and exploit developer systems.
Security News
The Ultralytics' PyPI Package was compromised four times in one weekend through GitHub Actions cache poisoning and failure to rotate previously compromised API tokens.