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