idris-hackers / idris-mode

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.
GNU General Public License v3.0
267 stars 70 forks source link

Infinitely looping Idris process hard to spot in Idris mode #9

Open david-christiansen opened 11 years ago

david-christiansen commented 11 years ago

This causes the type checker to loop forever:

module Death
import Providers
%language TypeProviders

%assert_total
forever : IO (Provider Bool)
forever = forever

%provide (crap : Bool) with forever

Without looking at top, we can't really see that Idris never finished type checking.

david-christiansen commented 10 years ago

It would seem that a buffer-local timeout would solve this.

david-christiansen commented 10 years ago

This was actually somewhat ameliorated by the little "!" shown if the Idris process is busy. But a timeout would still be nice to have.