[Agda] Discrepancies between emacsagda and agdachecker

Marcin Benke marcin at cs.chalmers.se
Wed Dec 8 18:05:11 CET 2004


Recent changes to emacsagda resulted ina discrepancy between agdachecker 
and emacsagda: the fformer silently succeeded even when there were 
unsolved goals left.

I have committed a quick fix: agdachecker now fails if there are goals 
left, but more work is needed on this.

A side effect is that "make check" now fails 3 class-related tests where 
emacsagda also reported unsolved  goals.
So this failures are in a sense "expected", but I would leave them as 
failures until we look more closely at the problem.

Marcin


More information about the Agda mailing list