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

[Makarius]

On Mon, 3 Nov 2014, Peter Lammich wrote:

>> 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.
>
> As you said, there seems to be no other way of achieving what I 
> required. I realized that, added a comment (*Argh!*) expressing my 
> disgust about it, but at the end had to implement the hack in order to 
> get the desired behaviour.

Poking around in global memory is not well-defined.  I don't think any 
behaviour coming from it could be called desirable.

This is what the "implementation" manual says about thread-safe 
programming:

   Multi-threaded execution has become an everyday reality in Isabelle
   since Poly/ML 5.2.1 and Isabelle2008.  Isabelle/ML provides implicit and
   explicit parallelism by default, and there is no way for user-space
   tools to ``opt out''.

Insisting in sequential TTY interaction could have been seen as an attempt 
to ``opt out'', but this is no longer possible.


> Now you just removed the desired behaviour, not having a solution how to 
> get it back ... fortunately, in this particular case, it is not 
> essential, as this thing was inside some rarely used debugging tool.

Proper debugging is generally a bit difficult.  We've had many situations 
where enabling a certain flag suddenly bombed the system.  Or situations 
where spurious debugging without a flag would cause total existence 
failure.

There are known approaches where controlled tracing output usually works, 
but it requires proper options in a proper context.  Strange hacks that 
work around the absence of proper options encumber the introduction of 
them eventually.  It is the usual bootstrap problem for reforms.

I actually did start some work in the vicinity of resolve_tac with proper 
context recently, but it will require more time to revisit really ancient 
parts of the system, not to say ancient habits.


 	Makarius

----------------------------------------------------------------------------
                    http://stop-ttip.org  787,957 people so far
----------------------------------------------------------------------------