lclem / agda-kernel Goto Github PK

I recently installed the kernel, together with the Jupyter notebook extensions (agda-extension). All seems well, the kernel starts as it should on a new notebook, but every time I press Sfift-Enter on a cell, all I get is "cell needs to be evaluated first...". This happens even with commands like "%autosave 300", that execute in any other kernel. I tried in vain to find a fix for this on the net.

The holes in the following fragment

module code.hole-test where

f : ∀ {A : Set} → A → A
f a = ? where
    g : ∀ {B : Set} → B → B
    g b = ?

are reported by Agda as

?0 : B
?1 : A

while the kernel expects them the other way around. Fixing this requires analysing the nesting structure of the where clauses.

@lclem let me first thank you for your work on the kernel, we're trying to use it at nextjournal to get Agda running.

Using the kernel I've encountered some issues with Tab completions:

1. Give command is always accepted if the provided expression type-checks alright, but we might want to trigger a case split instead (as meantioned in the README) like in this case:

2. suggestions from agsy involving chains of eq-reasoning are split erroneously

From logs I understand it's a matter of splitting response lines from agsy:

[IPKernelApp] ERROR | result is: Listing solution(s) 0-9
0  cong suc (+-assoc m n p)
1  begin
suc (m + n + p) ≡⟨ cong suc (+-assoc m n p) ⟩
suc (m + (n + p)) ≡⟨
sym (cong (λ _ → suc (m + (n + p))) (+-assoc m p p)) ⟩
suc (m + (n + p)) ∎
2  begin
suc (m + n + p) ≡⟨ cong suc (+-assoc m n p) ⟩
suc (m + (n + p)) ≡⟨
sym (cong (λ _ → suc (m + (n + p))) (+-assoc m p n)) ⟩
suc (m + (n + p)) ∎
3  begin
suc (m + n + p) ≡⟨ cong suc (+-assoc m n p) ⟩
suc (m + (n + p)) ≡⟨
sym (cong (λ _ → suc (m + (n + p))) (+-assoc m p m)) ⟩
suc (m + (n + p)) ∎
4  begin .....

Given it is hard to map the whole agda-mode onto just two commands (Tab and Shift+Tab) do you have suggestions on how to solve 1. (while for 2. I probably can open a pull request for a fix). Would it make sense to always prefer AGDA_CMD_MAKE_CASE command in case the expression in the hole isn't empty and the case command succeeds? (Returning both the result of give and case split might mess up cursor start/end for substitution in the client).

Do you think we could handle case split over agsy? Do you know if it's possible to pass agsy options directly into the hole? Something like {! -c m !} in the context of the first example above to trigger case split.

You can remix this nextjournal notebook to reproduce the issues above.

What versions of Agda does the kernel support? It seems that it doesn't work with the current release candidate.

when a cell takes very long to evaluate, it may be convenient to do incremental output to show the user that the kernel is doing something. cf. here.

Currently a code cell is restricted to start with a module xxx where line,
which effectively prevents the use of OPTIONS pragmas such as {-# OPTIONS --cubical #-}.