Re: [isabelle-dev] NEWS: parameterized antiquotations @{map N}, @{fold N} etc.
I have to admit: although I distinctly remember the name pairself, I can’t imagine what I could have been thinking when I chose this name. Your suggestions make a lot more sense. Larry > On 3 Nov 2014, at 09:08, Makarius wrote: > > On Thu, 30 Oct 2014, Florian Haftmann wrote: > > Isabelle/ML has antiquotations as some kind of macro language. It can > do certain things better than the C preprocessor, although one always > needs to be careful to stay within reason. How about this? ap2 f (x, y) = (f x, f y) @{ap n} f (x1, ..., xn) = (f x1, ..., f xn) Maybe even this as well? @{ap n(k)} f (x1, ..., xn) = (x1, ..., f xk, ..., xn) That might be occasionally useful to map field 1, or 2, or 3 of a triple: @{ap 3(1)}, @{ap 3(2)}, @{ap 3(3)}. The existing combinators apfst, apsnd fit into the same scheme. >> >> Both have there uses. I am not sure whether »ap« is the right name. >> »apfst« and »apsnd« are of course old-standing items, but when something >> new enters the stage further thoughts should be spent. Must confess I >> have no better proposal at hand. Or maybe »apply«?. > > Larry, you have introduced the "pairself" name some decades ago. How do you > feel about it being called "ap2" or "apply2"? > > > Makarius > > > http://stop-ttip.org 777,356 people so far > ___ 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
Re: [isabelle-dev] Experiments in best-first-search rewriter
On Sun, 2 Nov 2014, Bohua Zhan wrote: Two examples are given at the end: the first refers to the permutation example in section 6.4 of the new Isabelle Cookbook manual, rewriting: Note that the Isabelle Cookbok is not really "new". It is useful to get started in some areas of Isabelle/ML usage, but it also contains many things that are old, or outright misleading. You need to take other information into account as well, and develop a sense of (un)reliability of certain information. The official "implementation" manual is the main starting point for using Isabelle/ML. Using Isabelle/ML is not yet an Isabelle development activity, so it can be discussed on isabelle-users -- unless you want to propose concrete changes to ongoing repository versions. Makarius http://stop-ttip.org 777,535 people so far ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: uniform document heading commands
Am Montag, den 03.11.2014, 10:30 +0100 schrieb Makarius: > On Mon, 3 Nov 2014, Timothy Bourke wrote: > > Would it also be reasonable to allow 'text' before an initial 'theory' ? > > I have asked myself that yesterday, when updating some AFP entries in that > respect. > > The canonical question: Is such a feature really needed? > > So far the standard way is to say 'theory' first, before writing longer > paragraphs of text. The concept of Isabelle document preparation is to > write in a formal context (which is required for antiquotations), but > before the theory start it is undefined. In most cases I want to write a small (informal) introduction. But then the "theory ... imports ... begin" command looks out of place in the generated document and I hide it using (*<*) (*>*). So having a way to write an abstract / or an informal introduction would be nice. - Johannes ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: uniform document heading commands
* Makarius [2014-11-03 10:30 +0100]: > On Mon, 3 Nov 2014, Timothy Bourke wrote: > > >* Makarius [2014-11-02 20:24 +0100]: > >>*** Document preparation *** > >> > >>* Document headings work uniformly via the commands 'chapter', > >>'section', 'subsection', 'subsubsection' -- in any context, even > >>before the initial 'theory' command. > > > >Very nice. Thank you. > > > >Would it also be reasonable to allow 'text' before an initial 'theory' ? > > I have asked myself that yesterday, when updating some AFP entries in that > respect. > > The canonical question: Is such a feature really needed? > > So far the standard way is to say 'theory' first, before writing longer > paragraphs of text. The concept of Isabelle document preparation is to > write in a formal context (which is required for antiquotations), but before > the theory start it is undefined. I was thinking of the case where one wants to break up a set of theories into chapters while still keeping each theory within its own section. The first theory in a new chapter could now start: chapter "Theories A-D" section "Theory A" theory A imports Main begin ... end In this case, 'text' would be useful for writing introductory paragraphs between 'chapter' and 'section'. But, maybe it is better to dedicate a theory file to new chapters : chapter "Theories A-D" theory %invisible begin text {* ... *} end %invisible And then a top-level 'text' is not needed. Does anyone else had similar experiences with structuring proof documents? Tim. signature.asc Description: Digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: uniform document heading commands
On Mon, 3 Nov 2014, Timothy Bourke wrote: * Makarius [2014-11-02 20:24 +0100]: *** Document preparation *** * Document headings work uniformly via the commands 'chapter', 'section', 'subsection', 'subsubsection' -- in any context, even before the initial 'theory' command. Very nice. Thank you. Would it also be reasonable to allow 'text' before an initial 'theory' ? I have asked myself that yesterday, when updating some AFP entries in that respect. The canonical question: Is such a feature really needed? So far the standard way is to say 'theory' first, before writing longer paragraphs of text. The concept of Isabelle document preparation is to write in a formal context (which is required for antiquotations), but before the theory start it is undefined. Makarius http://stop-ttip.org 777,460 people so far ___ 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: 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
Re: [isabelle-dev] NEWS: parameterized antiquotations @{map N}, @{fold N} etc.
On Thu, 30 Oct 2014, Florian Haftmann wrote: Isabelle/ML has antiquotations as some kind of macro language. It can do certain things better than the C preprocessor, although one always needs to be careful to stay within reason. How about this? ap2 f (x, y) = (f x, f y) @{ap n} f (x1, ..., xn) = (f x1, ..., f xn) Maybe even this as well? @{ap n(k)} f (x1, ..., xn) = (x1, ..., f xk, ..., xn) That might be occasionally useful to map field 1, or 2, or 3 of a triple: @{ap 3(1)}, @{ap 3(2)}, @{ap 3(3)}. The existing combinators apfst, apsnd fit into the same scheme. Both have there uses. I am not sure whether »ap« is the right name. »apfst« and »apsnd« are of course old-standing items, but when something new enters the stage further thoughts should be spent. Must confess I have no better proposal at hand. Or maybe »apply«?. Larry, you have introduced the "pairself" name some decades ago. How do you feel about it being called "ap2" or "apply2"? Makarius http://stop-ttip.org 777,356 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] NEWS: uniform document heading commands
* Makarius [2014-11-02 20:24 +0100]: > *** Document preparation *** > > * Document headings work uniformly via the commands 'chapter', > 'section', 'subsection', 'subsubsection' -- in any context, even > before the initial 'theory' command. Very nice. Thank you. Would it also be reasonable to allow 'text' before an initial 'theory' ? Tim. signature.asc Description: Digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev