FS#69419 - [agda] looks for stdlib in different folder then where stdlib is installed.
Attached to Project:
Community Packages
Opened by brian yeh (heynairb) - Saturday, 23 January 2021, 19:24 GMT
Last edited by Buggy McBugFace (bugbot) - Saturday, 25 November 2023, 20:02 GMT
Opened by brian yeh (heynairb) - Saturday, 23 January 2021, 19:24 GMT
Last edited by Buggy McBugFace (bugbot) - Saturday, 25 November 2023, 20:02 GMT
|
Details
Description:
agda installs agda-stdlib as dependency but during compilation looks for the stdlib in a different place from where it was installed. ``` ~/agda_foundations >>> agda --compile main.agda Checking main (/home/brian/agda_foundations/main.agda). /home/brian/agda_foundations/main.agda:3,1-15 Failed to find source of module IO in any of the following locations: /home/brian/agda_foundations/IO.agda /home/brian/agda_foundations/IO.lagda /usr/share/agda/lib/prim/IO.agda /usr/share/agda/lib/prim/IO.lagda when scope checking the declaration open import IO ``` Steps to reproduce: create a file with contents: ``` module main where open import IO main = run (putStrLn "Hello, World!") ``` run `agda --compile main.agda` See: https://github.com/archlinux/svntogit-community/blob/764c37e399eda975f137688ac1d50fdea0318a81/trunk/PKGBUILD#L41 |
This task depends upon
Closed by Buggy McBugFace (bugbot)
Saturday, 25 November 2023, 20:02 GMT
Reason for closing: Moved
Additional comments about closing: https://gitlab.archlinux.org/archlinux/p ackaging/packages/agda/issues/4
Saturday, 25 November 2023, 20:02 GMT
Reason for closing: Moved
Additional comments about closing: https://gitlab.archlinux.org/archlinux/p ackaging/packages/agda/issues/4
$ cat ~/.agda/libraries
/usr/share/agda/lib/standard-library.agda-lib