*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] antiquotations*From*: Makarius <makarius at sketis.net>*Date*: Fri, 15 Feb 2008 11:35:50 +0100 (CET)*In-reply-to*: <47B4C7C4.4060502@rsise.anu.edu.au>*References*: <478AAC94.3030404@rsise.anu.edu.au> <478B2940.5020107@informatik.tu-muenchen.de> <478BEE3B.2000007@rsise.anu.edu.au> <478C8265.2010202@in.tum.de> <478D322C.7010001@rsise.anu.edu.au> <478DB7F0.7080604@in.tum.de> <478E6F17.9000100@rsise.anu.edu.au> <478E816D.9010606@in.tum.de> <478EF53A.9070809@rsise.anu.edu.au> <Pine.LNX.4.63.0801241542360.18967@atbroy100.informatik.tu-muenchen.de> <47ABC81B.3090608@rsise.anu.edu.au> <Pine.LNX.4.63.0802081405450.9643@atbroy100.informatik.tu-muenchen.de> <47AF877C.4050205@rsise.anu.edu.au> <47B04E56.7010901@in.tum.de> <47B381D7.7050908@inf.ed.ac.uk> <47B3A61F.5090907@rsise.anu.edu.au> <Pine.LNX.4.64.0802141321090.8150@atbroy99.informatik.tu-muenchen.de> <47B4C7C4.4060502@rsise.anu.edu.au>

On Fri, 15 Feb 2008, Jeremy Dawson wrote: > How do these critical sections work? Is it to do with the function > CRITICAL which appears in the source code? See appendix A.2 of the fragmentary Isabelle/Isar implementation manual. It explains the programming model for multithreaded Isabelle; the short and simple message is: do it purely functionally and in accord with the official concepts of context (as a plain value). In rare situations, user code may also have to synchronize things explicitly, but well-behaved programs should only do this for tiny amounts of time, i.e. refrain from any real computations / proof search inside a critical section. > The question relates to what the system does. That is to say, when I am > sitting at the terminal and type in ML {* val a = @{context} *} what is > the ML code which the system evaluates ? I want to know what ML code I > would put there which would achieve exactly the same effect. You can look at the Isar implementation to find out the details, just for curiosity. It is of course out of question to attempt to interfere with the existing infrastructure in user ML code. > > In contrast, low-level access to global references buys you dynamic > > scoping in the best case, and erratic non-determinism in the worst > > case. This is why thm"foo", thms"foo", the_context() are all bad. > > > So what functions, _in ML_, are good, for these purposes? Basically none. You can refer to the compile time context using @{context}, or get a runtime context as explicit functional argument from somewhere else. For example, a proof method is essentially a function Proof.context -> args -> tactic, and your implementation will be something like (fn ctxt => fn args => ...), so you get the context ``by induction hypothesis'' over the structure of your program. Concerning theorem lookup, ProofContext.get_thm: Proof.context -> thmref -> thm enables to retrieve named facts from a given context, but it is rarely useful within abstract code, because the name spacing rules behind this are quite delicate. Better refer to proper theorem *values* directly, either via @{thm ...} at compile time, or by using well-typed interfaces to derived context data, such as DatatypePackage.the_datatype or similar operations of whatever tool you build yourself. The general idea of strongly-typed context data is explained in section 1.1 in the Isabelle/Isar implementation manual. Makarius

**Follow-Ups**:**Re: [isabelle] antiquotations***From:*Jeremy Dawson

**References**:**Re: [isabelle] antiquotations***From:*Jeremy Dawson

**Re: [isabelle] antiquotations***From:*Makarius

**Re: [isabelle] antiquotations***From:*Jeremy Dawson

**Re: [isabelle] antiquotations***From:*Alexander Krauss

**Re: [isabelle] antiquotations***From:*Lucas Dixon

**Re: [isabelle] antiquotations***From:*Jeremy Dawson

**Re: [isabelle] antiquotations***From:*Makarius

**Re: [isabelle] antiquotations***From:*Jeremy Dawson

- Previous by Date: Re: [isabelle] antiquotations
- Next by Date: [isabelle] Cfp: 3rd Int'l Workshop on Security and Rewriting Techniques Security (SecReT 2008)
- Previous by Thread: Re: [isabelle] antiquotations
- Next by Thread: Re: [isabelle] antiquotations
- Cl-isabelle-users February 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list