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

Does not build with standard library 2.0 #11

Closed
turion opened this issue Jul 1, 2024 · 4 comments
Closed

Does not build with standard library 2.0 #11

turion opened this issue Jul 1, 2024 · 4 comments

Comments

@turion
Copy link

turion commented Jul 1, 2024

I tried to build this with standard library 2.0 and it seems it doesn't:

Checking Everything (/build/source/Everything.agda).
 Checking Generics.Prelude (/build/source/src/Generics/Prelude.agda).
/build/source/src/Generics/Prelude.agda:9,51-10,49
warning: -W[no]ModuleDoesntExport
The module Relation.Binary.PropositionalEquality doesn't export the
following:
  Extensionality
  ∀-extensionality
when scope checking the declaration
  open import Relation.Binary.PropositionalEquality public
                                                    hiding ([_]; Extensionality; ∀-extensionality)
/build/source/src/Generics/Prelude.agda:22,45-23,87
warning: -W[no]ModuleDoesntExport
The module Reflection doesn't export the following:
  return
when scope checking the declaration
  open import Reflection public
                         hiding (var; return; _>>=_; _>>_; assocˡ; assocʳ; visibility;
                                 relevance; module Arg)
/build/source/src/Generics/Prelude.agda:24,1-27
Failed to find source of module Reflection.Argument in any of the
following locations:
  /nix/store/1yxiwwy44xxxgzdmvyjizq53w9cfinkn-standard-library-2.0/src/Reflection/Argument.agda
  /nix/store/1yxiwwy44xxxgzdmvyjizq53w9cfinkn-standard-library-2.0/src/Reflection/Argument.lagda
  /build/source/src/Reflection/Argument.agda
  /build/source/src/Reflection/Argument.lagda
  /build/source/examples/Reflection/Argument.agda
  /build/source/examples/Reflection/Argument.lagda
  /build/source/Reflection/Argument.agda
  /build/source/Reflection/Argument.lagda
  /nix/store/r3cpdqcxl9hna5xwgdgd57bazvfjbivq-Agda-2.6.4.3-data/share/ghc-9.6.5/x86_64-linux-ghc-9.6.5/Agda-2.6.4.3/lib/prim/Reflection/Argument.agda
  /nix/store/r3cpdqcxl9hna5xwgdgd57bazvfjbivq-Agda-2.6.4.3-data/share/ghc-9.6.5/x86_64-linux-ghc-9.6.5/Agda-2.6.4.3/lib/prim/Reflection/Argument.lagda
when scope checking the declaration
  import Reflection.Argument

See https://github.com/NixOS/nixpkgs/pull/153757/checks?check_run_id=26884760539 and NixOS/nixpkgs#153757.

@flupe
Copy link
Owner

flupe commented Jul 1, 2024

Hello, thanks for the issue, I haven't kept in touch with stdlib changes for a while. Can you please let me know if current master builds as expected on your side?

If so, I'll update the README with versionning requirments and make a proper release with a bumped version number.

@turion
Copy link
Author

turion commented Jul 1, 2024

Yes, indeed it does build, thanks!

@turion
Copy link
Author

turion commented Jul 1, 2024

The agda version I tested with in nixpkgs is 2.6.4.3.

@flupe
Copy link
Owner

flupe commented Jul 1, 2024

Thanks for checking! Released under 1.0.1.
Let me know if you encounter any more issues.

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

No branches or pull requests

2 participants