Email Gateway (Aug 22 2022 at 12:38): Email Gateway (Aug 22 2022 at 12:38):From: Richard Molitor via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
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
Last updated: Nov 21 2024 at 12:39 UTC