[isabelle-dev] Remaining uses of Proof General?

[Andreas Lochbihler]

Thanks a lot.

Andreas

On 12/05/14 20:07, Florian Haftmann wrote:
>> 1. Violation of well-sortedness constraints: type ... not an instance of
>> ...
>>
>> declare [[show_sorts]]
>> code_thms <constant to be exported>
>>
>> Then, I use educated guessing and Emacs' incremental search to navigate
>> the code equations that have been output until I find the fault --
>> usually, it's just a missing [code] or [code del] declaration for some
>> constant that has introduced a quantifier or set comprehension.
>
>> I would really appreciate support for navigating code equations in the
>> output (e.g., Ctrl-click on a constant on the RHS of an equation takes
>> me to the code equation of that constant (in the output of code_thms).
>>
>> For this particular case, it would also be useful to get the chain of
>> propagation for the sort constraint like in GHC (arising from the use of
>> ...), but since Isabelle's code generator strengthens sort constraints
>> for intermediate functions, this would be a list (tree/graph) of
>> functions that trace the propagation.
>
> I will have to think about something like that seriously.
>
>> Here, I have two suggestions for improvements:
>>
>> a) Provide an entry to the code preprocessor such that I can trace the
>> transformation of the code equations for a given (set of) constants.
>> Currently, I only know how to trace the preprocessing of *all* code
>> equations, but I am not interested in most of this trace.
>
> I will consider this.
>
>> b) [code_abbrev] is the worst code generator attribute that I know of,
>> because there's no reverse [code_abbrev del]. Each time I have to get
>> rid of a code abbreviation, I have to figure out once again how
>> [code_abbrev] transforms the theorem before it calls [code_unfold] and
>> [code_post]. Please add the [code_abbrev del] attribute.
>
> See now http://isabelle.in.tum.de/repos/isabelle/rev/40213e24c8c4
>
>> And while I am at it, here is another point that makes my life
>> unnecessarily hard, but it's not related to jEdit vs. PG:
>>
>> 3. Problems with Code_Evaluation.term_of and friends
>>
>> The term reconstruction functions are not displayed in code_thms because
>> of the section "obfuscation" in Code_Evaluation. I do not understand why
>> this has to be obfuscated. I always have to go via export_code and read
>> the generated code to figure out what the code equation for one of these
>> overloaded constants is. And it's bad luck if export_code raises an
>> error because some of the code equations are invalid.
>
> See now http://isabelle.in.tum.de/repos/isabelle/rev/1e50fddbe1f5
>
> 	Florian
>