Re: [isabelle] Localization of code generator (and thus quickcheck)

Hi all,

> changeset:   63072:413184c7a2a2
> user:        wenzelm
> date:        Mon May 09 14:37:47 2016 +0200
> files:       src/Doc/more_antiquote.ML
> src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
> src/HOL/Tools/Predicate_Compile/predicate_compile.ML
> src/HOL/Tools/record.ML src/Pure/Isar/code.ML src/Pure/axclass.ML
> src/Tools/Code/code_preproc.ML src/Tools/Code/code_thingol.ML
> description:
> clarified context, notably for internal use of Simplifier;
> The codegen setup has quite a few uses Proof_Context.init_global left:
> that seems to be required for a hard reset of the logical context
> (fixes, sorts of type variables etc.), but it disrupts the use of
> options in the context to control other tools (notably the Simplifier).
> Is there a chance to make the code generator fully context-conformant?

indeed I am currently working in that area, to iron out some of these
issues which I have stumbled over from a different perspective also.

The main reasons why significant parts of the code generator
infrastructure are not context-conformant are not of logical nature (the
only example I am aware of is in nbe.ML) but merely technical: there is
still some ancient global-theory background cache.  Over the last years
at least the user interfaces have gained more and more proper contexts,
and this will continue hopefully soon.  Maybe the days of that cache are
also counted, lets see.


>     Makarius


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.