Your message dated Wed, 23 Oct 2024 16:04:34 +0000
with message-id <[email protected]>
and subject line Bug#1085873: fixed in agda-stdlib 2.1-2
has caused the Debian Bug report #1085873,
regarding Fail to load agda-stdlib modules from agda2-mode
to be marked as done.
This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.
(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact [email protected]
immediately.)
--
1085873: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1085873
Debian Bug Tracking System
Contact [email protected] with problems
--- Begin Message ---
Package: agda-stdlib
Version: 2.1-1
Severity: important
When using agda2-mode to verify .agda files that use agda-stdlib,
it fails to load the library modules.
Here is information on related packages:
```
% env LANGUAGE=C dpkg --no-pager -l emacs-lucid emacs-el agda
agda-bin agda-stdlib elpa-agda2-mode
Desired=Unknown/Install/Remove/Purge/Hold
| Status=Not/Inst/Conf-files/Unpacked/halF-conf/Half-inst/trig-aWait/Trig-pend
|/ Err?=(none)/Reinst-required (Status,Err: uppercase=bad)
||/ Name Version Architecture Description
+++-===============-============-============-================================================================
ii agda 2.6.4.3-1 all dependently typed
functional programming language
ii agda-bin 2.6.4.3-1 amd64 commandline interface to Agda
ii agda-stdlib 2.1-1 all standard library for Agda
ii elpa-agda2-mode 2.6.4.3-1 all dependently typed
functional programming language — emacs mode
ii emacs-el 1:29.4+1-3 all GNU Emacs LISP (.el) files
ii emacs-lucid 1:29.4+1-3 amd64 GNU Emacs editor (with
Lucid GUI support)
```
Here are the steps to reproduce the problem:
```
% cat foo.agda
open import Data.Nat
```
open foo.agda in emacs, and `C-c C-l` gives errors like below in emacs
*Error* buffer:
```
/home/hibi/src/agda/debian-bug/foo.agda:1,1-21
Failed to find source of module Data.Nat in any of the following
locations:
/home/hibi/src/agda/debian-bug/Data/Nat.agda
/home/hibi/src/agda/debian-bug/Data/Nat.lagda
/usr/share/agda-stdlib/Data/Nat.agda
/usr/share/agda-stdlib/Data/Nat.lagda
/usr/share/libghc-agda-dev/lib/prim/Data/Nat.agda
/usr/share/libghc-agda-dev/lib/prim/Data/Nat.lagda
when scope checking the declaration
open import Data.Nat
```
I have confirmed that the following patch resolves the issue:
```
--- debian/60agda-stdlib.el.old 2022-08-07 01:32:51.000000000 +0900
+++ debian/60agda-stdlib.el 2024-10-23 15:13:04.296257932 +0900
@@ -2,4 +2,4 @@
;; variable in his/her own session. But that is probably the intended behaviour
;; anyway.
-(setq agda2-program-args '("-i." "-i/usr/share/agda-stdlib"))
+(setq agda2-program-args '("-i." "-i/usr/share/agda-stdlib/src"))
```
--
Kei Hibino
[email protected]
--- End Message ---
--- Begin Message ---
Source: agda-stdlib
Source-Version: 2.1-2
Done: Ilias Tsitsimpis <[email protected]>
We believe that the bug you reported is fixed in the latest version of
agda-stdlib, which is due to be installed in the Debian FTP archive.
A summary of the changes between this version and the previous one is
attached.
Thank you for reporting the bug, which will now be closed. If you
have further comments please address them to [email protected],
and the maintainer will reopen the bug report if appropriate.
Debian distribution maintenance software
pp.
Ilias Tsitsimpis <[email protected]> (supplier of updated agda-stdlib package)
(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing [email protected])
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512
Format: 1.8
Date: Wed, 23 Oct 2024 18:28:19 +0300
Source: agda-stdlib
Architecture: source
Version: 2.1-2
Distribution: unstable
Urgency: medium
Maintainer: Debian Haskell Group
<[email protected]>
Changed-By: Ilias Tsitsimpis <[email protected]>
Closes: 1085873
Changes:
agda-stdlib (2.1-2) unstable; urgency=medium
.
* Fix import path for elpa-agda2-mode.
Thanks Kei Hibino for the patch (Closes: #1085873)
* Install build artifacts under '/usr/share/agda-stdlib/_build/'
Checksums-Sha1:
d400988f6fa9699e1b4ec3dec4c44f4c701f5718 2253 agda-stdlib_2.1-2.dsc
c641a06c2e5f7568e2def6807fdccb9b77d0bec3 5980 agda-stdlib_2.1-2.debian.tar.xz
8281529222cca493d0fbf6f61fb27f16b21a501f 9462 agda-stdlib_2.1-2_amd64.buildinfo
Checksums-Sha256:
db6b47a61250c17bf9cf31a61d5471df629a479fb1d4ad7e2711f626c948fc89 2253
agda-stdlib_2.1-2.dsc
365a9386810274e82cfd58795aa9fb87a41f718a11ed0ac5c189c804d574f2c3 5980
agda-stdlib_2.1-2.debian.tar.xz
da37d19686f93341483732d6484d8732a26fc77153e112874ec6e4afbadfb26c 9462
agda-stdlib_2.1-2_amd64.buildinfo
Files:
8b11b7211132b4b55c377ab84c45c4e7 2253 libs optional agda-stdlib_2.1-2.dsc
57b8944edb6f95b37b6e3d3ed2078e63 5980 libs optional
agda-stdlib_2.1-2.debian.tar.xz
dd6835e6ff92a0001b97d469de3764e3 9462 libs optional
agda-stdlib_2.1-2_amd64.buildinfo
-----BEGIN PGP SIGNATURE-----
iQJIBAEBCgAyFiEEJ9c8pfW11+AaUTb116hngMxkQDwFAmcZGvUUHGlsaWFzdHNp
QGRlYmlhbi5vcmcACgkQ16hngMxkQDznTA/9FofNFfEVF0itww413gkqW3Fdt3Fy
VEFwKsYU8uNq2vkKPU3yBn1gZ98/Iu+vdj5dXy5BeiS9JejSczWpOGGPQR1Z9RKf
bxKwM69Gt/rtHy6j5qGiHesizILLK5rh5+cipde5yCC92OFT4gyDaEBz4ryV8hTX
yTrNwxMp+q+0yuZ08wBkBCeFVr4Q4s2DnZoQBpmZWr3Xyd16DA4ZBNrxVvrbHWNz
GlgxP681BVi2nY8QZ8jPGZzve7tgvkKwZ9+3w6sM7DyTHwVnO0O0wJDKBenEuH++
GW2HE8UTHJ2MBroPzNi/0EejGvb+IWCr5wiW7rjJg43bXWfSwdzuvR4r4YAJ5pBM
FbVB386EIitSp4EC2b62iCRJ4Z8gAMuBO+50/nHpUDvdW5oWjDFZfxp41naC/YCD
349hxe7are0CkCmwFbrj9guiu0gM7nu29ZfN2ZRsmiTiwzcbwXlSMoW+nikit3/p
kVopibzsdIVYB1OBrozR4SWUqNYQw80QXtMhauaEQ58jw2GGurYxTgLvMru+NfHz
FGor3eBuVpPcB09lrChhwjVD2hkqejgoE/GbHmto/ui3q6OeAgiYo3HL/FICVlnX
TyKxy5L16NlmzuHLRohJeSIw/IPrAiCLG+EtXXcZLoW1FsnMQ4OcParz1KvEFvBU
i9xv30A3rGczmdw=
=xSeX
-----END PGP SIGNATURE-----
pgpEOx32exiXT.pgp
Description: PGP signature
--- End Message ---
_______________________________________________
Pkg-haskell-maintainers mailing list
[email protected]
https://alioth-lists.debian.net/cgi-bin/mailman/listinfo/pkg-haskell-maintainers
