Re: [isabelle] OpenTheory import for Isabelle



> And 80 MB of compressed, generated files is
> unappealing as well and likely to create trouble. I am guessing that
> .art files are opentheory files. If that is the case, can't they reside
> in the opentheory repository?

Yes, they are OpenTheory files. The "isabelle-opentheory" session reads
them in (as test cases, essentially) during regular "isabelle build" or
when opening them in Isabelle/jEdit. So they need to be somewhere
Isabelle can find them. I'm assuming that downloading them on-the-fly is
not an option. In principle the OpenTheory import for Isabelle can be
built without reading any .art files, but then there's nothing testing
that it actually works.

Cheers
Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.