FS#64600 - [agda] fixing agda-stdlib

Attached to Project: Community Packages
Opened by poscat0x04 (Poscat) - Thursday, 21 November 2019, 13:12 GMT
Last edited by Buggy McBugFace (bugbot) - Saturday, 25 November 2023, 20:01 GMT
Task Type Bug Report
Category Packages
Status Closed
Assigned To Felix Yan (felixonmars)
Architecture All
Severity Medium
Priority Normal
Reported Version
Due in Version Undecided
Due Date Undecided
Percent Complete 100%
Votes 2
Private No

Details

Description:

right now agda cannot correctly find the standard library (https://bugs.archlinux.org/task/61904?project=5&string=agda and https://bugs.archlinux.org/task/56637?project=5&string=agda)

after fix:

PKGBUILD for agda-stdlib : https://cfp.vim-cn.com/cbf5c
PKGBUILD for agda : https://cfp.vim-cn.com/cbf5d

`libraries` and `defaults` should be placed with agda-stdlib's PKGBUILD whereas `Library.patch` should be placed with agda's PKGBUILD

`Library.patch` changes the default AGDA_DIR to `/usr/share/agda`

`libraries` and `defaults` registers the standard library

Additional info:
* package version(s)
* config and/or log files etc.
* link to upstream bug report, if any

Steps to reproduce:
This task depends upon

Closed by  Buggy McBugFace (bugbot)
Saturday, 25 November 2023, 20:01 GMT
Reason for closing:  Moved
Additional comments about closing:  https://gitlab.archlinux.org/archlinux/p ackaging/packages/agda/issues/2
Comment by poscat0x04 (Poscat) - Thursday, 21 November 2019, 13:27 GMT Comment by Felix Yan (felixonmars) - Friday, 31 July 2020, 07:25 GMT
Thanks for the report. It looks like Library.patch will ignore $HOME/.agda and use only /usr/share/agda, that seems like a breaking change to anyone reading official docs etc.

I still think it should be left to the user to decide whether he needs agda-stdlib to be configured globally or perhaps only on a project level.

For a global configuration, one can always use:

$ cat .agda/libraries
/usr/share/agda/lib/standard-library.agda-lib
$ cat .agda/defaults
standard-library
Comment by diego (diofanto33) - Monday, 15 May 2023, 09:34 GMT
Hi, I recently ran sudo pacman -S agda agda-stdlib and it seems to have installed correctly. Additionally, in ~/.agda/libraries I have /usr/share/agda/lib/standard-library.agda-lib. However, when I try to compile a simple "Hello World" program with agda --compile HelloWorld.agda, I encounter the following error:

Checking HelloWorld (/home/shine/agda-pr/HelloWorld.agda).
/home/shine/agda-pr/HelloWorld.agda:3,1-15
Failed to find source of module IO in any of the following
locations:
/home/shine/agda-pr/IO.agda
/home/shine/agda-pr/IO.lagda
/usr/share/agda/lib/prim/IO.agda
/usr/share/agda/lib/prim/IO.lagda
when scope checking the declaration
open import IO

Could you please help me with this issue?
Comment by Buggy McBugFace (bugbot) - Tuesday, 08 August 2023, 19:11 GMT
This is an automated comment as this bug is open for more then 2 years. Please reply if you still experience this bug otherwise this issue will be closed after 1 month.

Loading...