-
-
Notifications
You must be signed in to change notification settings - Fork 12.7k
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
Bug compiling using Agda when Unicode ⟨⟩ is in file system #172752
Comments
Does this compile on a non nix agda? |
It compiles like in this file: |
Fix: |
It worked here, but I will let it open because it is already not fixed in Agda or in something inside nixpkgs (such as mkDerivation). |
Out of interest, we already have this flag set for the cubical derivation
Perhaps it should be default for agda, would there be any downside to this? |
Opened agda/agda#5903 |
Related: agda/agda#4678 |
I agree and will prepare a pull request. This comes up when updating to Agda 2.6.3, the stdlib doesn't compile without it. |
Describe the bug
Agda can't compile files their names have Unicode ⟨⟩ on them.
Steps To Reproduce
Just run
nix build
in this file:Expected behavior
It should compile like in this file:
https://github.com/agda/cubical/blob/master/Cubical/Syntax/%E2%9F%A8%E2%9F%A9.agda
Notify maintainers
@abbradar @Ericson2314 @turion @alexarice @neosimsim @Fuuzetsu @zimbatm @AndersonTorres @roberth @TilCreator @globin
The text was updated successfully, but these errors were encountered: