[Agda] Getting started: couple more questions

[Vox Veritatis]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200210/a4286e84/attachment.html>