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
----------------------------------------------------------------------------
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
