Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Agda test-suite fails due to deprecation warnings #1098

Closed
asr opened this issue Mar 4, 2020 · 2 comments · Fixed by #1100
Closed

Agda test-suite fails due to deprecation warnings #1098

asr opened this issue Mar 4, 2020 · 2 comments · Fixed by #1100

Comments

@asr
Copy link
Member

asr commented Mar 4, 2020

I couldn't update the submodule commit in Agda to the current master of the standard library because

$ make std-lib-compiler-test
...
+out >
+out > ———— All done; warnings encountered ————————————————————————
+out >
+out > /home/asr/src/agda/agda-upstream/std-lib/src/Algebra/Properties/CommutativeMonoid.agda:30,8-35
+out > Data.Table.Properties was deprecated in v1.2.
+out > Use Data.Vec.Functional.Properties instead.
+out > when scope checking the declaration
+out >   import Data.Table.Properties as TP
+out >
+out > /home/asr/src/agda/agda-upstream/std-lib/src/Algebra/Properties/CommutativeMonoid.agda:28,13-66
+out > Data.Table.Relation.Binary.Equality was deprecated in v1.2.
+out > Use Data.Vec.Functional.Relation.Binary.Pointwise instead.
+out > when scope checking the declaration
+out >   open import Data.Table.Relation.Binary.Equality as TE using (_≗_)
+out >
+out > /home/asr/src/agda/agda-upstream/std-lib/src/Algebra/Properties/CommutativeMonoid.agda:27,13-32
+out > Data.Table was deprecated in v1.2.
+out > Use Data.Vec.Functional instead.
+out > when scope checking the declaration
+out >   open import Data.Table as Table
+out >
+out > /home/asr/src/agda/agda-upstream/std-lib/src/Algebra/Operations/CommutativeMonoid.agda:21,13-51
+out > Data.Table.Base was deprecated in v1.2.
+out > Use Data.Vec.Functional instead.
+out > when scope checking the declaration
+out >   open import Data.Table.Base as Table using (Table)

Blocking agda/agda#4324.

@asr asr changed the title Agda test-suite fails on the current master due to deprecation warnings Agda test-suite fails due to deprecation warnings Mar 4, 2020
@MatthewDaggitt MatthewDaggitt added this to the v1.3 milestone Mar 5, 2020
@MatthewDaggitt
Copy link
Contributor

@asr fixed now.

@asr
Copy link
Member Author

asr commented Mar 5, 2020

Thanks! I just updated the submodule commit.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants