Re: [isabelle] open-inductive (was: Make all selectors measure_functions?)



On Fri, 12 Feb 2016, Makarius wrote:

On Fri, 12 Feb 2016, Richard Molitor via Cl-isabelle-users wrote:

 I originally intended to get it into the AFP, but then never pushed it
 when I got busy with applying for jobs and other things. The code is on
 github though (https://github.com/gattschardo/open-inductive) and I made
 it work with Isabelle2015 (and this week Isabelle2016-RC4).

I've already commented on an earlier version of this material, and you seem to have improved it further. It generally looks good -- above the average of various ML experiments that are already in AFP.

Your comments have been very helpful! The main thing I wanted to finish
before submitting it to the "lawnmower phase" was to finish the move to
use morphisms in all relevant places (which is only half-finished, if I
recall correctly).

Hopefully I will just sit down on a rainy weekend one day and do that,
once that is done you'll hear back from me :)

Some years ago, the AFP editors did not want to see actual ML tools there, but de-facto we have that already.

That's what I've heard from the colleagues in Karlsruhe as well, so this
was not a concern.

I cannot say anything about the application, i.e. the problem that is addressed here from a user perspective.

At least in Karlsruhe there seemed to be some use-cases for it, although
some additional hand-holding (i.e. automation) in my code would make it
considerably more user-friendly. That was labelled "future work" though,
maybe for when another bachelor/master student is looking for thesis
material -- or when I become very bored for a longer period of time.

Richard




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