Community Packages

Please read this before reporting a bug:
http://wiki.archlinux.org/index.php/Reporting_Bug_Guidelines

Do NOT report bugs when a package is just outdated, or it is in the AUR. Use the 'flag out of date' link on the package page, or the Mailing List.

REPEAT: Do NOT report bugs for outdated packages!
Tasklist

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 Andreas Radke (AndyRTR) - Wednesday, 21 April 2021, 14:13 GMT
Task Type Bug Report
Category Packages
Status Assigned
Assigned To Felix Yan (felixonmars)
Architecture All
Severity Low
Priority Normal
Reported Version
Due in Version Undecided
Due Date Undecided
Percent Complete 0%
Votes 0
Private No

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

Loading...