FS#78119 - [agda-stdlib] 1.7.2-1 warnings overload

Attached to Project: Community Packages
Opened by Thorsten Wissmann (twi) - Wednesday, 05 April 2023, 07:53 GMT
Last edited by Toolybird (Toolybird) - Wednesday, 10 May 2023, 22:46 GMT
Task Type Bug Report
Category Packages
Status Closed
Assigned To Felix Yan (felixonmars)
Architecture All
Severity Low
Priority Normal
Reported Version
Due in Version Undecided
Due Date Undecided
Percent Complete 100%
Votes 2
Private No

Details

Description:
The PKGBUILD for agda-stdlib replaces the upstream file standard-library.agda-lib and by that removes the flag --warning=noUnsupportedIndexedMatch which suppresses certain warnings. When now compiling any agda file using the standard libray, the output is flooded with 3470 lines of warnings raised from the standard-library.


Additional info:
* Archlinux's standard-library.agda-lib: https://github.com/archlinux/svntogit-community/blob/packages/agda-stdlib/trunk/standard-library.agda-lib.in
* Upstream's standard-library.agda-lib: https://github.com/agda/agda-stdlib/blob/master/standard-library.agda-lib
* agda's console output when compiling any file is attached
* agda 2.6.3-2
* agda-stdlib 1.7.2-1

Steps to reproduce:
mkdir -p ~/.agda
echo 'standard-library' > ~/.agda/defaults
echo '/usr/share/agda/lib/standard-library.agda-lib' > ~/.agda/libraries
echo 'import Data.Vec' > hello.agda
agda hello.agda # output in attached file.
   agda-warnings.log (136.4 KiB)
This task depends upon

Closed by  Toolybird (Toolybird)
Wednesday, 10 May 2023, 22:46 GMT
Reason for closing:  Fixed
Additional comments about closing:  agda-stdlib 1.7.2-3
Comment by Felix Yan (felixonmars) - Tuesday, 09 May 2023, 08:45 GMT
I have synced standard-library.agda-lib with upstream and also added the flag when compiling the standard library. Unfortunately this only fixes warnings while building the agda-stdlib package, not when you using the standard library like the steps provided. I could still reproduce the same warnings with agda-stdlib 1.7.2-3.
Comment by Thorsten Wissmann (twi) - Wednesday, 10 May 2023, 09:04 GMT
Thanks for updating the package! When upgrading to 1.7.2-3, the issue is resolved for me :-)

~/git/agda> mkdir -p ~/.agda
~/git/agda> echo 'standard-library' > ~/.agda/defaults
~/git/agda>
~/git/agda> mkdir temp
~/git/agda> cd temp
~/git/agda/temp> echo 'standard-library' > ~/.agda/defaults
~/git/agda/temp> echo '/usr/share/agda/lib/standard-library.agda-lib' > ~/.agda/libraries
~/git/agda/temp> echo 'import Data.Vec' > hello.agda
~/git/agda/temp> agda hello.agda
Checking hello (/home/thorsten/git/agda/temp/hello.agda).
~/git/agda/temp> cat /usr/share/agda/lib/standard-library.agda-lib
name: standard-library-2.0
include: stdlib
flags:
--warning=noUnsupportedIndexedMatch
~/git/agda/temp> pacman -Qs agda
local/agda 2.6.3-5
A dependently typed functional programming language and proof assistant
local/agda-stdlib 1.7.2-3
Agda standard libraries
local/python-agda-pkg 0.1.51-00
A package manager for Agda
~/git/agda/temp>

Loading...