[opentheory-users] invalid theory file syntax should be detected earlier

Joe Hurd joe at gilith.com
Tue Dec 6 22:30:34 UTC 2011


Hi Ramana,

> It might be nicer to get a more informative syntax error earlier on.

I've made the syntax error more friendly:

FATAL ERROR: opentheory failed:
bad show format:
  Data.Bool"
please use one of the following forms:
  "NAMESPACE"
  "NAMESPACE" as "NAMESPACE"

This is pushed and in the latest released version of the opentheory tool.

I can't easily make it happen earlier, because the opentheory tool
processes theories "lazily", so the show information only gets
processed when it's needed.

> As an aside, is there an issue tracker for the opentheory tool?

Not right now: is there one that you would recommend?

Cheers,

Joe



More information about the opentheory-users mailing list