[isabelle-dev] Remaining uses of Proof General?

[Florian Haftmann]

> 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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140512/b96db5ea/attachment.sig>