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

[brando90]

Error:

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

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

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

[banacorn]

Thanks for reporting this!

[banacorn]

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]

I am also running into this issue!

[epicallan]

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