banacorn / agda-mode-vscode

agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
165 stars 37 forks source link

Download Agda binary if not exists in the path #170

Open L-TChen opened 8 months ago

L-TChen commented 8 months ago

Agda's CI/CD currently builds binaries for every commit on the master branch and produces the artefact https://github.com/agda/agda/blob/master/.github/workflows/deploy.yml

The extension can exploit the CI/CD to download artefact if agda is not found in the path.

banacorn commented 7 months ago

Where can I find binaries for official releases (non-nightly builds)?

L-TChen commented 7 months ago

We haven't released these binaries officially. Maybe the requested feature could be added as an "experiment feature". Then, once I sort out https://github.com/agda/agda/issues/6384, we could make the feature official?

banacorn commented 7 months ago

Sounds good, we can start with the nightly binaries first!