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 compile on Windows 10 with Idris version 1.3.3 #1

Open
WilliamLightner opened this issue Jul 28, 2020 · 2 comments
Open

Does not compile on Windows 10 with Idris version 1.3.3 #1

WilliamLightner opened this issue Jul 28, 2020 · 2 comments

Comments

@WilliamLightner
Copy link

2020-07-28 16:13:10.47

idris --build idris-time.ipkg
Entering directory `.\src'
Type checking .\Data\DateTime.idr
.\Data\DateTime.idr:39:11:
|
39 | getUTCTime: IO DateTime
| ^
public export Data.DateTime.getUTCTime can't refer to private Data.DateTime.DateTime

@gdevanla
Copy link
Owner

gdevanla commented Aug 1, 2020

@WilliamLightner Thanks for reporting. It is strange you get that error for the same version of Idris I am using.

That said, this library is currently not Windows compatible since it uses C level calls which are only compatible with *nix systems right now.

@WilliamLightner
Copy link
Author

WilliamLightner commented Aug 3, 2020 via email

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