Arch Linux User Repository

Search Criteria

Enter search criteria

Search by

Keywords

Out of Date

Sort by

Sort order

Per page

Package Details: agda-bin-git 2.6.2.98d4eb0-1

Package Actions

Git Clone URL:	https://aur.archlinux.org/agda-bin-git.git (read-only, click to copy)
Package Base:	agda-bin-git
Description:	A dependently typed functional programming language and proof assistant: development version
Upstream URL:	http://wiki.portal.chalmers.se/agda/
Licenses:	custom
Conflicts:	agda
Provides:	agda
Submitter:	LightQuantum
Maintainer:	LightQuantum
Last Packager:	LightQuantum
Votes:	0
Popularity:	0.000000
First Submitted:	2021-05-13 08:41 (UTC)
Last Updated:	2021-05-13 08:41 (UTC)

Dependencies (2)

sed (busybox-coreutils^AUR, sed-git^AUR) (make)
tar (tar-git^AUR, busybox-coreutils^AUR) (make)

Required by (4)

agda-categories (requires agda)
agda-cubical (requires agda)
haskell-agda-language-server (requires agda)
python-agda-kernel (requires agda)

Sources (2)

Latest Comments

guygastineau commented on 2022-05-04 13:30 (UTC)

The binaries from the GitHub release are expecting files in /home/runner/.cabal/share/x86_64-linux-ghc-9.2.1/Agda-2.6.3/lib. I get the following error when trying to use agda in interactive mode a la agda -I after installation:

agda: The lib directory /home/runner/.cabal/share/x86_64-linux-ghc-9.2.1/Agda-2.6.3/lib does not exist
CallStack (from HasCallStack):
  error, called at src/full/Agda/Interaction/Library.hs:138:8 in Agda-2.6.3-inplace:Agda.Interaction.Library

I don't know if anyone else has encountered this before. The agda-mode executable also "locates" the emacs mode files under the same /home/runner hierarchy, so this definitely seems like an issue with the upstream build process' environment leaking into the executables.