<div dir="ltr"><div>A big thank you to all those who got me on a good track, including Philip, Jason and Bill!</div><div><br></div><div>I have a couple more questions, if anyone can help:<br></div><div><br></div><div>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?</div><div><br></div><div>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.</div><div><br></div><div>Vox<br></div></div>