%global _empty_manifest_terminate_build 0 Name: python-agda-pkg Version: 0.1.51 Release: 1 Summary: A package manager for Agda License: MIT URL: https://github.com/agda/agda-pkg Source0: https://mirrors.nju.edu.cn/pypi/web/packages/46/44/0cebcb9343340ea8394f1b51d425464c094d75e510a6b3938220d5b43312/agda-pkg-0.1.51.tar.gz BuildArch: noarch Requires: python3-click Requires: python3-gitpython Requires: python3-pony Requires: python3-whoosh Requires: python3-ponywhoosh Requires: python3-natsort Requires: python3-click-log Requires: python3-requests Requires: python3-humanize Requires: python3-Jinja2 Requires: python3-distlib Requires: python3-PyYAML %description agda-base | v0.2 | https://github.com/pcapriotti/agda-base.git agda-categories | v0.1 | https://github.com/agda/agda-categories.git agda-metis | v0.2.1 | https://github.com/jonaprieto/agda-metis.git agda-prelude | df679cf | https://github.com/UlfNorell/agda-prelude.git agda-prop | v0.1.2 | https://github.com/jonaprieto/agda-prop.git agda-real | e1558b62 | https://gitlab.com/pbruin/agda-real.git agda-ring-solver | d1ed21c | https://github.com/oisdk/agda-ring-solver.git agdarsec | v0.3.0 | 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 generic | f448ab3 | https://github.com/effectfully/Generic.git hott-core | 1037d82 | https://github.com/HoTT/HoTT-Agda.git hott-theorems | 1037d82 | https://github.com/HoTT/HoTT-Agda.git HoTT-UF-Agda | 9d0f38e | https://github.com/martinescardo/HoTT-UF-Agda-Lecture-Notes.git ial | v1.5.0 | https://github.com/cedille/ial.git lightweight-prelude | b2d440a | https://github.com/L-TChen/agda-lightweight-prelude.git mini-hott | d9b4a7b | https://github.com/jonaprieto/mini-hott.git MtacAR | 5417230 | https://github.com/L-TChen/MtacAR.git plfa | stable-web-2019.09 | https://github.com/plfa/plfa.github.io.git routing-library | thesis | https://github.com/MatthewDaggitt/agda-routing.git standard-library | v1.3 | https://github.com/agda/agda-stdlib.git # Usage manual ## Initialisation of the package index 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: ```bash $ 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: ```bash $ 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`. ```bash $ apkg --help $ apkg install --help ``` ## Upgrade the package index Recall updating the index every once in a while using `upgrade`. ```bash $ 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]. ## Environmental variables 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. ```bash $ apkg environment ``` ## List all the packages available To see all the packages available run the following command: ```bash $ 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](http://github.com/agda/package-index) ``` $ apkg install standard-library ``` - from a [local directory] ```bash $ apkg install . ``` or even much simpler: ```bash $ 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. ```bash $ apkg install --editable . ``` - from a github repository ```bash $ apkg install --github agda/agda-stdlib --version v1.1 ``` - from a git repository ```bash $ apkg install http://github.com/jonaprieto/agda-prop.git ``` To specify the version of a library, we use the flag `--version` ```bash $ apkg install standard-library --version v1.0 ``` Or simpler by using `@` or `==` as it follows. ```bash $ 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: 1. Using the inline method ```bash $ apkg install standard-library agda-base ``` Use `@` or `==` if you need a specific version, see above examples. 2. Using a requirement file: Generate a requirement file using `apkg freeze`: ```bash $ 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: ```bash $ apkg install -r requirements.txt ``` Check all the options of this command with the help information: ```bash $ 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 ```bash $ apkg uninstall standard-library ``` - infering the library name from the current directory ```bash $ apkg uninstall . ``` And if we want to remove the library completely (the sources and everything), we use the flag `--remove-cache`. ```bash $ 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: ```bash $ apkg update ``` - Update a specific list of libraries. If some library is not installed, this command will installed the latest version of it. ```bash $ apkg update standard-library agdarsec ``` ## See packages installed ```bash $ 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. ```bash $ apkg freeze > requirements.txt ``` To install from this requirement file run this command. ```bash $ 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: ```bash $ 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 ```bash $ 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: ```bash $ 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 ```yaml $ 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`. ```yaml $ 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 ``` ## Using with Nix or NixOS 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: ```bash $ curl -L https://gist.github.com/jonaprieto/53e55263405ee48a831d700f27843931/download | tar -xvz --strip-components=1 ``` or if you already have installed agda-pkg: ```bash $ apkg nixos ``` Then, you will have the following files: ```bash ./hello-world.agda ./agda_requirements.txt ./shell.nix ./deps.nix ./emacs.nix ``` From where you can run the nix shell. ```bash $ 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](https://www.spacemacs.org), 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](https://github.com/bbarker/LearningAgda) to give an idea of exactly which files need to be copied to your project. **Example**: ```agda $ 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. ### Configuration Edit any of the `nix` expressions as needed. In particular: 0. To add Agda dependencies via `agda-pkg`, edit `agda_requirements.txt` 1. To add more 4Haskell or other system dependencies or other target-language dependencies, edit `deps.nix`. 2. To add or alter the editor used, change the `myEmacs` references in `shell.nix` or add similar derivations. 3. Optionally, create `.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. # About This is a proof of concept of an Agda Package Manager. Contributions are always welcomed. [the package index]: https://github.com/agda/package-index [local directory]: https://agda.readthedocs.io/en/v2.5.4/tools/package-system.html [PR]: https://github.com/agda/package-index/pull/new/master %package -n python3-agda-pkg Summary: A package manager for Agda Provides: python-agda-pkg BuildRequires: python3-devel BuildRequires: python3-setuptools BuildRequires: python3-pip %description -n python3-agda-pkg agda-base | v0.2 | https://github.com/pcapriotti/agda-base.git agda-categories | v0.1 | https://github.com/agda/agda-categories.git agda-metis | v0.2.1 | https://github.com/jonaprieto/agda-metis.git agda-prelude | df679cf | https://github.com/UlfNorell/agda-prelude.git agda-prop | v0.1.2 | https://github.com/jonaprieto/agda-prop.git agda-real | e1558b62 | https://gitlab.com/pbruin/agda-real.git agda-ring-solver | d1ed21c | https://github.com/oisdk/agda-ring-solver.git agdarsec | v0.3.0 | 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 generic | f448ab3 | https://github.com/effectfully/Generic.git hott-core | 1037d82 | https://github.com/HoTT/HoTT-Agda.git hott-theorems | 1037d82 | https://github.com/HoTT/HoTT-Agda.git HoTT-UF-Agda | 9d0f38e | https://github.com/martinescardo/HoTT-UF-Agda-Lecture-Notes.git ial | v1.5.0 | https://github.com/cedille/ial.git lightweight-prelude | b2d440a | https://github.com/L-TChen/agda-lightweight-prelude.git mini-hott | d9b4a7b | https://github.com/jonaprieto/mini-hott.git MtacAR | 5417230 | https://github.com/L-TChen/MtacAR.git plfa | stable-web-2019.09 | https://github.com/plfa/plfa.github.io.git routing-library | thesis | https://github.com/MatthewDaggitt/agda-routing.git standard-library | v1.3 | https://github.com/agda/agda-stdlib.git # Usage manual ## Initialisation of the package index 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: ```bash $ 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: ```bash $ 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`. ```bash $ apkg --help $ apkg install --help ``` ## Upgrade the package index Recall updating the index every once in a while using `upgrade`. ```bash $ 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]. ## Environmental variables 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. ```bash $ apkg environment ``` ## List all the packages available To see all the packages available run the following command: ```bash $ 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](http://github.com/agda/package-index) ``` $ apkg install standard-library ``` - from a [local directory] ```bash $ apkg install . ``` or even much simpler: ```bash $ 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. ```bash $ apkg install --editable . ``` - from a github repository ```bash $ apkg install --github agda/agda-stdlib --version v1.1 ``` - from a git repository ```bash $ apkg install http://github.com/jonaprieto/agda-prop.git ``` To specify the version of a library, we use the flag `--version` ```bash $ apkg install standard-library --version v1.0 ``` Or simpler by using `@` or `==` as it follows. ```bash $ 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: 1. Using the inline method ```bash $ apkg install standard-library agda-base ``` Use `@` or `==` if you need a specific version, see above examples. 2. Using a requirement file: Generate a requirement file using `apkg freeze`: ```bash $ 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: ```bash $ apkg install -r requirements.txt ``` Check all the options of this command with the help information: ```bash $ 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 ```bash $ apkg uninstall standard-library ``` - infering the library name from the current directory ```bash $ apkg uninstall . ``` And if we want to remove the library completely (the sources and everything), we use the flag `--remove-cache`. ```bash $ 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: ```bash $ apkg update ``` - Update a specific list of libraries. If some library is not installed, this command will installed the latest version of it. ```bash $ apkg update standard-library agdarsec ``` ## See packages installed ```bash $ 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. ```bash $ apkg freeze > requirements.txt ``` To install from this requirement file run this command. ```bash $ 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: ```bash $ 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 ```bash $ 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: ```bash $ 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 ```yaml $ 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`. ```yaml $ 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 ``` ## Using with Nix or NixOS 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: ```bash $ curl -L https://gist.github.com/jonaprieto/53e55263405ee48a831d700f27843931/download | tar -xvz --strip-components=1 ``` or if you already have installed agda-pkg: ```bash $ apkg nixos ``` Then, you will have the following files: ```bash ./hello-world.agda ./agda_requirements.txt ./shell.nix ./deps.nix ./emacs.nix ``` From where you can run the nix shell. ```bash $ 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](https://www.spacemacs.org), 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](https://github.com/bbarker/LearningAgda) to give an idea of exactly which files need to be copied to your project. **Example**: ```agda $ 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. ### Configuration Edit any of the `nix` expressions as needed. In particular: 0. To add Agda dependencies via `agda-pkg`, edit `agda_requirements.txt` 1. To add more 4Haskell or other system dependencies or other target-language dependencies, edit `deps.nix`. 2. To add or alter the editor used, change the `myEmacs` references in `shell.nix` or add similar derivations. 3. Optionally, create `.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. # About This is a proof of concept of an Agda Package Manager. Contributions are always welcomed. [the package index]: https://github.com/agda/package-index [local directory]: https://agda.readthedocs.io/en/v2.5.4/tools/package-system.html [PR]: https://github.com/agda/package-index/pull/new/master %package help Summary: Development documents and examples for agda-pkg Provides: python3-agda-pkg-doc %description help agda-base | v0.2 | https://github.com/pcapriotti/agda-base.git agda-categories | v0.1 | https://github.com/agda/agda-categories.git agda-metis | v0.2.1 | https://github.com/jonaprieto/agda-metis.git agda-prelude | df679cf | https://github.com/UlfNorell/agda-prelude.git agda-prop | v0.1.2 | https://github.com/jonaprieto/agda-prop.git agda-real | e1558b62 | https://gitlab.com/pbruin/agda-real.git agda-ring-solver | d1ed21c | https://github.com/oisdk/agda-ring-solver.git agdarsec | v0.3.0 | 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 generic | f448ab3 | https://github.com/effectfully/Generic.git hott-core | 1037d82 | https://github.com/HoTT/HoTT-Agda.git hott-theorems | 1037d82 | https://github.com/HoTT/HoTT-Agda.git HoTT-UF-Agda | 9d0f38e | https://github.com/martinescardo/HoTT-UF-Agda-Lecture-Notes.git ial | v1.5.0 | https://github.com/cedille/ial.git lightweight-prelude | b2d440a | https://github.com/L-TChen/agda-lightweight-prelude.git mini-hott | d9b4a7b | https://github.com/jonaprieto/mini-hott.git MtacAR | 5417230 | https://github.com/L-TChen/MtacAR.git plfa | stable-web-2019.09 | https://github.com/plfa/plfa.github.io.git routing-library | thesis | https://github.com/MatthewDaggitt/agda-routing.git standard-library | v1.3 | https://github.com/agda/agda-stdlib.git # Usage manual ## Initialisation of the package index 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: ```bash $ 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: ```bash $ 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`. ```bash $ apkg --help $ apkg install --help ``` ## Upgrade the package index Recall updating the index every once in a while using `upgrade`. ```bash $ 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]. ## Environmental variables 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. ```bash $ apkg environment ``` ## List all the packages available To see all the packages available run the following command: ```bash $ 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](http://github.com/agda/package-index) ``` $ apkg install standard-library ``` - from a [local directory] ```bash $ apkg install . ``` or even much simpler: ```bash $ 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. ```bash $ apkg install --editable . ``` - from a github repository ```bash $ apkg install --github agda/agda-stdlib --version v1.1 ``` - from a git repository ```bash $ apkg install http://github.com/jonaprieto/agda-prop.git ``` To specify the version of a library, we use the flag `--version` ```bash $ apkg install standard-library --version v1.0 ``` Or simpler by using `@` or `==` as it follows. ```bash $ 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: 1. Using the inline method ```bash $ apkg install standard-library agda-base ``` Use `@` or `==` if you need a specific version, see above examples. 2. Using a requirement file: Generate a requirement file using `apkg freeze`: ```bash $ 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: ```bash $ apkg install -r requirements.txt ``` Check all the options of this command with the help information: ```bash $ 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 ```bash $ apkg uninstall standard-library ``` - infering the library name from the current directory ```bash $ apkg uninstall . ``` And if we want to remove the library completely (the sources and everything), we use the flag `--remove-cache`. ```bash $ 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: ```bash $ apkg update ``` - Update a specific list of libraries. If some library is not installed, this command will installed the latest version of it. ```bash $ apkg update standard-library agdarsec ``` ## See packages installed ```bash $ 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. ```bash $ apkg freeze > requirements.txt ``` To install from this requirement file run this command. ```bash $ 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: ```bash $ 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 ```bash $ 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: ```bash $ 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 ```yaml $ 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`. ```yaml $ 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 ``` ## Using with Nix or NixOS 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: ```bash $ curl -L https://gist.github.com/jonaprieto/53e55263405ee48a831d700f27843931/download | tar -xvz --strip-components=1 ``` or if you already have installed agda-pkg: ```bash $ apkg nixos ``` Then, you will have the following files: ```bash ./hello-world.agda ./agda_requirements.txt ./shell.nix ./deps.nix ./emacs.nix ``` From where you can run the nix shell. ```bash $ 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](https://www.spacemacs.org), 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](https://github.com/bbarker/LearningAgda) to give an idea of exactly which files need to be copied to your project. **Example**: ```agda $ 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. ### Configuration Edit any of the `nix` expressions as needed. In particular: 0. To add Agda dependencies via `agda-pkg`, edit `agda_requirements.txt` 1. To add more 4Haskell or other system dependencies or other target-language dependencies, edit `deps.nix`. 2. To add or alter the editor used, change the `myEmacs` references in `shell.nix` or add similar derivations. 3. Optionally, create `.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. # About This is a proof of concept of an Agda Package Manager. Contributions are always welcomed. [the package index]: https://github.com/agda/package-index [local directory]: https://agda.readthedocs.io/en/v2.5.4/tools/package-system.html [PR]: https://github.com/agda/package-index/pull/new/master %prep %autosetup -n agda-pkg-0.1.51 %build %py3_build %install %py3_install install -d -m755 %{buildroot}/%{_pkgdocdir} if [ -d doc ]; then cp -arf doc %{buildroot}/%{_pkgdocdir}; fi if [ -d docs ]; then cp -arf docs %{buildroot}/%{_pkgdocdir}; fi if [ -d example ]; then cp -arf example %{buildroot}/%{_pkgdocdir}; fi if [ -d examples ]; then cp -arf examples %{buildroot}/%{_pkgdocdir}; fi pushd %{buildroot} if [ -d usr/lib ]; then find usr/lib -type f -printf "/%h/%f\n" >> filelist.lst fi if [ -d usr/lib64 ]; then find usr/lib64 -type f -printf "/%h/%f\n" >> filelist.lst fi if [ -d usr/bin ]; then find usr/bin -type f -printf "/%h/%f\n" >> filelist.lst fi if [ -d usr/sbin ]; then find usr/sbin -type f -printf "/%h/%f\n" >> filelist.lst fi touch doclist.lst if [ -d usr/share/man ]; then find usr/share/man -type f -printf "/%h/%f.gz\n" >> doclist.lst fi popd mv %{buildroot}/filelist.lst . mv %{buildroot}/doclist.lst . %files -n python3-agda-pkg -f filelist.lst %dir %{python3_sitelib}/* %files help -f doclist.lst %{_docdir}/* %changelog * Fri May 05 2023 Python_Bot - 0.1.51-1 - Package Spec generated