search

banacorn / agda-mode-vscode

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

No backend called 'GHC' (installed backends: GHCNoMain, QuickLaTeX) #99

Open brando90 opened 2 years ago

brando90 commented 2 years ago

Error:

No backend called 'GHC' (installed backends: GHCNoMain, QuickLaTeX)

but I see that's the default in my setting:

Screen Shot 2022-04-14 at 1 57 12 PM

crossposted: https://stackoverflow.com/questions/71876445/how-does-one-use-ghc-in-agda-with-vscode

banacorn commented 2 years ago

Thanks for reporting this!

banacorn commented 2 years ago

If we use GHC as backend in the settings, agda-mode would emit GHCNoMain https://github.com/banacorn/agda-mode-vscode/blob/f06bde4ddbc03291915bc345dfd0ad23ed5af054/src/Config.res#L173-L177

But somehow, GHCNoMain would get converted back to GHC in Agda for some "backwards compatibility" reason https://github.com/agda/agda/blob/467a4b9f9a6808ea5aaf3411a55c7bdcaf714d7d/src/full/Agda/Interaction/InteractionTop.hs#L512

Could this be an Agda's issue?

vezwork commented 2 years ago

I am also running into this issue!

epicallan commented 1 year ago

I just ran into this issue, you need to sync the GHC backend setting for issue resolution.

Screen Shot 2023-01-11 at 2 43 58 PM