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

Add newest idris tool chain support #3

Open
weihongliang233 opened this issue Mar 2, 2024 · 0 comments
Open

Add newest idris tool chain support #3

weihongliang233 opened this issue Mar 2, 2024 · 0 comments

Comments

@weihongliang233
Copy link

Great work, but when opening the project in vscode devcontainer, the following error occured.

image

Currently, the docker image uses idirs2, while the vscode extension installed seems not support idris2 and it's an old project (last commit 7 years ago).

Is there any plan to upgrade the project to use newest idirs2 compiler and newest vscode extension?

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

1 participant