What steps will reproduce the problem? 1. Define this module:

module bug where A : Set A = A -- non-terminating definition should give an error, not a loop q : A q = ? -- including this definition makes agda loop

2. run agda bug.agda

What is the expected output? What do you see instead?

An error like "bug.A does NOT pass the termination check". Instead, agda loops.

What version of the product are you using? On what operating system?

Agda 2 version 2.1.3 compiled from darcs repo 071212 or so.

Please provide any additional information below.

The emacs mode gets confused when agda does not respond. Ctrl-g gives back the cursor, but the process is still tied up in the background.

/Patrik

The emacs mode gets confused when agda does not respond. Ctrl-g gives back the cursor, but the process is still tied up in the background.

Nowadays you can restart the process by invoking agda2-restart (C-c C-x C-r).

Issue 201 has been merged into this issue.

Issue 371 has been merged into this issue.

Issue 379 has been merged into this issue.

Issue 385 has been merged into this issue.

Issue 653 has been merged into this issue.

Issue 801 has been merged into this issue.

This was fixed by Andreas in February.

Andreas has recently added another mechanism that can be used to trigger non-termination:

p : Σ ℕ λ n → n ≡ 0 proj₁ p = proj₁ p proj₂ p = refl

Mutual blocks can also be used:

mutual

Foo : Set
Foo = Foo

foo : Foo
foo = foo