On Wed, Jan 21, 2009 at 02:44, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote: > Amine Chaieb wrote: >> Isabelle/HOL is remarkably more user friendly than many other system.
If this is indeed the case, I'm glad I picked it, rather than some other system. I found the learning curb quite steep, though I believe I am near the leveling-out part. But my opinions on how to improve that have to do with building a new user interface catering to novices, which I am working on myself, and perhaps a couple new tutorials aimed a little lower as well. :) >> All this effort of the past decades seems to have negative back effects >> in the past years: Many Developers stand before complex situations >> nobody or sometimes only one understands. Don't you think it is time to >> invest in a more developer-friendly Isabelle/HOL ? > > Not sure whether user-friendliness means less developer-friendliness. This is not generally true in my experience, though of course Isabelle could be different. My uninformed opinion in this particular instance is that the problem could be mostly solved with better error reporting first, and perhaps with a rearrangement (as you suggest) second. Adding more error reporting doesn't increase the developer's burden in the long term, although rearranging things can sometimes. It seems to me that helpful error messages are key to user-friendliness. The error in Amine's case should say first which statement in which theory instantiated each of the conflicting typerep instances, and what the derived theories are that are immediately being merged, and second give a hint as to the need to rearrange things. If the interface is helpful enough when you do something wrong, you no longer have to be an expert to avoid getting stuck at errors. > The problem is: you can instantiate every type class only once to a > particular type. There is no way to get around. Here, I am completely ignorant as to Isabelle's workings. But could you not somehow cache the first instantiation at the heap level and then check before the second to see if it's cached already? This may seem ugly, but for classes that are instantiated implicitly, maybe it's the best way. Chris Capel -- "What is it like to be a bat? What is it like to bat a bee? What is it like to be a bee being batted? What is it like to be a batted bee?" -- The Mind's I (Hofstadter, Dennet)
