Re: [isabelle] OpenTheory import for Isabelle



On 22/02/18 19:33, Gerwin.Klein at data61.csiro.au wrote:
> 
>> On 22 Feb 2018, at 03:04, Lars Hupel <hupel at in.tum.de> wrote:
>>
>>> 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.
> 
> I agree with Tobias in that don’t think the importer is a good match for the AFP. 
> 
> How about putting the importer and/or a minimal set of .art files into the distribution? Downloading might work for the distribution, in the sense that this minimal set of .art files could be a component.

In the Isabelle distribution the quality standards are even higher than
for AFP.

I would welcome a proper version of the OpenTheory importer for
Isabelle, but it needs to be done properly, as usual.


	Makarius





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