Public bug reported:
I tried using literate Agda on Ubuntu. I was able to run Agda perfectly
in Emacs. It loaded libraries without any problem. But I tried to run
agda on the command-line, it had trouble with finding libraries.
Both
`agda --html --html-highlight=code NahasTutorialModule.lagda.md`
and
`agda NahasTutorialModule.lagda.md`
generated the following error:
```
Checking NahasTutorialModule
(/mnt/mass_storage/Desktop/Home/projects/Math_DB/Tools/Agda/NahasTutorialModule.lagda.md).
/mnt/mass_storage/Desktop/Home/projects/Math_DB/Tools/Agda/NahasTutorialModule.lagda.md:701,8-51
Failed to find source of module
Relation.Binary.PropositionalEquality in any of the following
locations:
/mnt/mass_storage/Desktop/Home/projects/Math_DB/Tools/Agda/Relation/Binary/PropositionalEquality.agda
/mnt/mass_storage/Desktop/Home/projects/Math_DB/Tools/Agda/Relation/Binary/PropositionalEquality.lagda
/usr/share/libghc-agda-dev/lib/prim/Relation/Binary/PropositionalEquality.agda
/usr/share/libghc-agda-dev/lib/prim/Relation/Binary/PropositionalEquality.lagda
when scope checking the declaration
import Relation.Binary.PropositionalEquality as Eq
```
It looks like agda, when invoked on the command-line, is looking in the
wrong place for the standard libraries.
After some searching, I found that the libraries were located at:
/usr/share/agda-stdlib. I was able to get around the problem with:
`agda -i /usr/share/agda-stdlib/ --html --html-highlight=code
NahasTutorialModule.lagda.md`
Mike
I'm running Agda 2.6.0.1 on Ubuntu 20.04.3 LTS.
$ lsb_release -rd
Description: Ubuntu 20.04.3 LTS
Release: 20.04
$ apt list agda
Listing... Done
agda/focal,focal,now 2.6.0.1-1build4 all [installed]
$ apt-cache policy agda
agda:
Installed: 2.6.0.1-1build4
Candidate: 2.6.0.1-1build4
Version table:
*** 2.6.0.1-1build4 500
500 http://us.archive.ubuntu.com/ubuntu focal/universe amd64 Packages
500 http://us.archive.ubuntu.com/ubuntu focal/universe i386 Packages
100 /var/lib/dpkg/status
** Affects: agda (Ubuntu)
Importance: Undecided
Status: New
--
You received this bug notification because you are a member of Ubuntu
Bugs, which is subscribed to Ubuntu.
https://bugs.launchpad.net/bugs/1949641
Title:
command-line invocation doesn't find stdlib
To manage notifications about this bug go to:
https://bugs.launchpad.net/ubuntu/+source/agda/+bug/1949641/+subscriptions
--
ubuntu-bugs mailing list
ubuntu-bugs@lists.ubuntu.com
https://lists.ubuntu.com/mailman/listinfo/ubuntu-bugs
