Re: [isabelle-dev] How to activate/de-activate unifier-trace from ML-level
Hi Makarius, On 10.02.2015 18:30, Makarius wrote: On Tue, 4 Nov 2014, Makarius wrote: 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. Here is an update on this pending thread: current Isabelle/50b60f501b05 is the main move to proper context for resolve_tac etc. After endless years of preparation to localize the majority of Isabelle tools, it turned out a releatively small change. What remains are slightly odd entry points without context: resolve0_tac/rtac, eresolve_tac/etac, dresolve_tac/dtac. We could probably remove them altogether, but there are a lot of remaining uses in the new datatype implementation, which I don't want to change myself. indeed approximately 2/3 of all usages of rtac in the Isabelle distribution + AFP are in our BNF tactics (roughly 2000 occurrences). Adding a context to each of them would make the tactics even harder to read/maintain compared to their current state. The only decent way of adding the context everywhere would be via some combinators à la THEN'': (ctxt - int - tactic) * (ctxt - int - tactic) - ctxt - int - tactic assuming that rtac has type thm - ctxt - int - tactic or reuse the polymorphism of THEN' and work with an uncurried version of rtac: thm - (ctxt, int) - tactic (and other tactics). Needless to say that I could do this only locally in the BNF package, but maybe this is a general question of how tactics should look like. Dmitriy ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] How to activate/de-activate unifier-trace from ML-level
On Tue, 4 Nov 2014, Makarius wrote: 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. Here is an update on this pending thread: current Isabelle/50b60f501b05 is the main move to proper context for resolve_tac etc. After endless years of preparation to localize the majority of Isabelle tools, it turned out a releatively small change. What remains are slightly odd entry points without context: resolve0_tac/rtac, eresolve_tac/etac, dresolve_tac/dtac. We could probably remove them altogether, but there are a lot of remaining uses in the new datatype implementation, which I don't want to change myself. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] How to activate/de-activate unifier-trace from ML-level
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
[isabelle-dev] How to activate/de-activate unifier-trace from ML-level
Hi List, 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? Best, Peter p.s. 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. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] How to activate/de-activate unifier-trace from ML-level
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. 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. -- Peter 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
