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