Re: [isabelle] OpenTheory import for Isabelle



> 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.

Right. Today I've been doing some digging into the implementation and I
think it should be possible to clean it up with modest effort to make it
ready for inclusion.
> Making sure that the larger collection of .art files works could be handled separately. It sounds like there is a bunch of interested parties (we are one of them), and we (Data61) can possibly provide a regression test infrastructure (need to check). If there are a few groups who are willing to maintain the collection and keep it up to date, that approach might work. 

Sure, that would work, I guess. But keep in mind that the distinction
between what should be tested and what shouldn't is pretty much
arbitrary. My starting point was the repository by Brian et.al. For
example, Maksym Bortin has put some .art files about ARM machine code in
there. (Is there a good reason why we don't try to import the entirety
of the OpenTheory database? In some sense, that database serves a
similar purpose as the AFP. There are 54 packages as of this writing.)

Cheers
Lars




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