[isabelle-dev] Remaining uses of Proof General?

[Andreas Lochbihler]

>> But I try to process such
>> theories with jEdit and only go back to XEmacs/PG when I cannot stand
>> Isabelle/jEdit any longer (which usually happens when I debug the code
>> generator setup).
>
> That's an interesting observation.  What are the particular properties
> of »debugging« here that make PG preferable?  Maybe it is just a
> question of better code generation tool support.
I usually debug the code generator setup like this:

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.

2. The generated code does not terminate.

The most frequent reason for this is some unintended interaction of rewrite rules in the 
code preprocessor. In this case, I look both at the exported code and at code_thms, 
navigate again with incremental search and compare the code equations to what I originally 
have declared with [code]. When I found problematic (set of mutually recursive) code 
equations, I then have to find [code_unfold] equations that do not work as expected.

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.

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.



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.


Andreas