[Agda] Getting started: couple more questions

[Andreas Abel]

Welcome, Vox!

 > 1) When pressing C-c-x-c, Emacs asks for "Backend".

Unless you want to compile your code (e.g. to Haskell via GHC), you are 
probably better off with

   C-c C-l

which just "loads" your Agda file, i.e., type-checks it and allows 
interactive edition.

To set a default backed, do

   M-x customize-group RET agda2

and there set the "Agda2 Backend" variable.  Then "Apply and Save" this 
customization buffer.

On 2020-02-10 23:14, Vox Veritatis wrote:
> A big thank you to all those who got me on a good track, including 
> Philip, Jason and Bill!
> 
> I have a couple more questions, if anyone can help:
> 
> 1) When pressing C-c-x-c, Emacs asks for "Backend". Are there several 
> options to this? For hello-world I typed "GHC" and it appears to work, 
> but what if no output is produced? Also, is there a way to set the 
> "Backend" so that one doesn't need to type it all the time?
> 
> And 2) Being familiar with Jupyter, I also installed the agda_kernel for 
> Jupyter and the agda-extension. Everything seemed fine (the kernel is 
> loaded) until I typed an example from the agda_kernel page in one cell. 
> When pressing "Shift-Enter" all I get is "the cell has to be evaluated 
> first...". Never saw this before. This happens even if the cell contains 
> a "magic" command, like "%autosave 300" - which works in any other 
> Jupyter notebook, irrespective of the kernel.
> 
> Vox
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>