[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