[isabelle-dev] typrep?

[Amine Chaieb]

The situation is more delicate that I thought at first.


I just have some comments and more questions, no solution to the problem:

wrt to d) and e) (Users/Developers, HOL is difficult).
This theory is for now a "using" HOL, but of course I want to develop it
in a manner that it could become part of HOL.
The situation you mention in d) and e) has not to be this way and we
should not take it for granted that HOL is complex to develop etc. The
social and psychological consequences are not very nice if it becomes a
rule (my opinion).
Isabelle/HOL is remarkably more user friendly than many other system.
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 ?


If typerep is mainly used in connection with code-generation (as I
understand) isn't it an option to generate all these instances when you
call any code-generation facility? Or even in prior step e.g. called
setup-every-thing-that-has-to-do-with-code-generation?


Besides, I don't object to the idea of typerep at all, I am just
confused why the names clash? (Wasn't this the problem). In other words
is this problem unavoidable, so that one needs a hard
discussion/decision like typerep or no typerep?


Amine.


Florian Haftmann wrote:

> Hi all over there,
>
> some comments on my behalf:
>
> a) The Typerep theory if used by Imperative_HOL, but this is *not* its
> only application; it is also used for evaluation using code generation
> (value [code]) -- indeed, I added this immediately after the 2008
> release in order to gain some experience how this machinery works and
> which problem it raises.
>
> b) Beside "typerep" and "size", there are also "itself" and "eq";
> similar mechanisms are also used for datatype realizers and sledgehammer.
>
> c) I agree with Alex that the reason why only typerep so far caused one
> problem is that typerep is bootstrapped rather lately because it needs
> lists, and thus you might run into problems if you rearrange the HOL
> thygraph.
>
> d) I accept that the behaviour Amine has encountered is difficult to
> trace, but -- we should have no illusion: *developing* HOL is more
> delicate than *using* HOL anyway.  For this reason we have the
> advertised entry points Base, Plain, Main, Complex_Main which provide a
> consistent setup of packages, whereas using other HOL theories directly
> is branded as "use at your own risk" explicitly.
>
> e) Of course there still remains the burden for HOL developers to find
> an appropriate thygraph layout, but this has never been trivial, typerep
> notwithstanding.  "Bad" layouts can even give raise to mysterious
> non-functional discrepancy, e.g. the recent replacement of Univ_Poly by
> Polynomial which does not need lists anymore produced a significant
> speedup in building the HOL theories (perhaps due to a different
> sledgehammer situation).
>
> f)
>   
>> I, for one, am rather alarmed at the hurdles that Amine was forced to overcome to do a simple merge of two theories. Even before the typerep-related problems, merging Isabelle theories was already difficult enough! I think that merging theories is one of Isabelle's most serious weaknesses, and it has prevented many users from being able to borrow, share, and build upon each other's code. (Witness how little re-use of code there has been among AFP entries, in spite of the recommendation in the submission guidelines, "It is possible and encouraged to build on other archive entries in your submission.") 
>>     
>
> I see the point that failing merges are hard to trace (if not impossible
> without guidance of an expert), but so far I did not have the feeling
> that this would be the main obstacle for library developement.
>
> Regardless of this discussion, it would be interesting to hear about
> such failures in order to try to amend them.
>
> Hope this contributes to clarify the situation,
> 	Florian
>
>   
> ------------------------------------------------------------------------
>
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>