[isabelle-dev] How to activate/de-activate unifier-trace from ML-level

[Makarius]

On Mon, 3 Nov 2014, Peter Lammich wrote:

> I have a tactic that has a debug-mode. In debug-mode, it shall output 
> unification trace for certain (but not all) rule applications.
>
> How to write a tactic
>  resolve_with_tracing: thm list -> int -> tactic
>
> that behaves like resolve_tac, but outputs unification trace?

I don't know yet.  These ancient things are still somewhat entangled.

Last time in Garching, I had a brief discussion with Lars Nischinski about 
a proper local configuration options for unify_trace.  Then tools could 
change the context before invoking certain resolve operations.

It is conceptually not possible to work with global options on the 
background theory instead: a theory certificate is not a proper context.


> Not sure whether this belongs to user or devel, but the reason
> for my message is
>
> http://sourceforge.net/p/afp/code/ci/7189f7ffd73e17c2395eb552c89004f5b8e0453e/
>
> which seems to be related to tty-mode elimination that is currently
> going on in dev-version.

I merely removed some very old Unsynchronized.ref variables.  This 
elimination of ad-hoc mutable state has started in 2007 and is getting 
close to be finished.  Isabelle/ML tools must not poke around in memory 
arbitrarily.  Since people sometimes want to do it nonetheless, the 
canonical way is to make it structurally impossible by removing refs. (In 
most situtations, ill-defined behaviour of mutability is unintentional, 
though.)

You can contribute indirectly to important reforms that are in the 
pipeline for a long time by keeping your sources in a more up-to-date 
state.


 	Makarius

----------------------------------------------------------------------------
                   http://stop-ttip.org  777,443 people so far
----------------------------------------------------------------------------