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
Opened by poscat0x04 (Poscat) - Thursday, 21 November 2019, 13:12 GMT
Last edited by Buggy McBugFace (bugbot) - Saturday, 25 November 2023, 20:01 GMT
|
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
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
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
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?