Re: [Hol-info] [isabelle] More on "References about mistakes and gaps in papers"
On 26/05/2020 11:24, Andrei Popescu wrote: > > This message's subject refers to an old thread on the Isabelle mailing > list, from July 2018. This time, I and my coauthor are the > protagonists of some "mistakes and gaps"... > > In impressive recent work, > > https://arxiv.org/abs/2002.10212 > > Johannes Åman Pohjola and Arve Gengelbach have formalized in HOL4 our > model-theoretic proof of consistency for (an abstract representation > of) Isabelle/HOL's logic (http://andreipopescu.uk/pdf/ITP2015.pdf). I have now taken the time to read the paper: great work, and great to see interactions of the various people (re)working foundations of HOL with adhoc overloading. As I understand it, the particulars of the dependency relation and its construction from the definitional theory are still to be settled. Just note that the cited paper [20] (Ondřej Kunčar, CPP 2015) slightly deviates from the actual implementation https://isabelle.sketis.net/repos/isabelle/file/Isabelle2020/src/Pure/defs.ML It would be great if the next wave of formalization could clarify this --- in a way that I know if and how I should improve the implementation as well. Makarius ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] New grammar of defining theorems?
On 03/01/2019 13:20, Chun Tian (binghe) wrote:
>
> I personally don’t like the keyword “Theorem” because I think many small
> theorems with 3 lines of tactics do not deserve the name “Theorem”. The
> correct way of using these conventions should be aligned with majority
> math books, which I believe there must be some “rules” mentioned somewhere.
Isar started with 'theorem', then added 'lemma' and 'corollary', much
later 'proposition'.
In everyday use 'lemma' quickly became the most popular one. So if there
were only one keyword, it would be 'lemma'.
Makarius
signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] New grammar of defining theorems?
On 03/01/2019 11:23, Chun Tian (binghe) wrote: > Hi Michael, > > thanks for fixing the bugs. (now I see why I can’t find its definition…) > > Going in this direction, have you considered adding also “Lemma” and > “Corollary”? Internally they're equivalent with “Theorem”, but they could > literally help writers (and readers) identifying different levels of > theorems, like those in math books. This reminds me of Isabelle/Isar. Some decades ago I introduced these variants of 'theorem' and it became a running gag of confusion and unclear corner cases, because aliases were not really identical, but distinguished internally by some tools. Recently, we even introduced 'proposition' as another variant, but it is unclear if it is more prominent than 'theorem' or less prominent than 'lemma'. Thus it depends on local conventions of particular formalization projects how to treat it, e.g. in document presentation. If I had another chance today, I would probably eliminate all funny aliases of Isar commands. Makarius signature.asc Description: OpenPGP digital signature ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] QuoteFilter with precise positions
On 28/08/18 03:00, michael.norr...@data61.csiro.au wrote: > > - there is evidently a bug in the position information when the leading > delimiter is a Unicode quote mark (the number of bytes gets counted rather > than the number of "characters"); With Unicode text it is inherently difficult to say how "characters" are counted, and thus to say what is right or wrong. Whatever you do is likely to be wrong in some sense. Many people think of Unicode characters in the sense of Java or JavaScript, which used to be UCS-2, but is now UTF-16 (with its 16 or 32 bit chars). The website https://utf8everywhere.org provides very useful links and explanations on the many confusions around Unicode, and hints to avoid most of them. For internal counting, I would prefer the raw byte address, as we have it already in our fine SML strings that are undiluted by Unicode. It allows to access large text chunks quickly without recoding back and forth. For external purposes, e.g. error messages with characters positions, it is hard to tell. It depends on the "consumers" that you have in mind: a Java front-end is likely to expect 16-bit Char addresses. Unix tools are likely to expect UTF-8 characters in the sense of codepoints. Nothing of this is smallest textual unit, if you allow official Unicode in its full complexity (but nobody has implemented that correctly anyway). Makarius -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] QuoteFilter with precise positions
Dear experts on antiquotations HOL4, I've looked through tools/Holmake/QuoteFilter, but could not read the input format -- I am used to functional parser combinators instead of lex + yacc. Is there a specification of the input syntax in the documentation? But it is also changing occasionally, so it might be better to re-use the existing implementation. Ultimately I want to turn HOL4 ML source into tokens with precise source positions, e.g. byte addresses of the original string. The idea is to continue some experiments with HOL4 inside the Isabelle Prover IDE, see also https://sketis.net/2015/hol4-workshop-at-cade-25 Makarius -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Generated machine code of Poly/ML
On 17/05/18 18:12, Mario Xerxes Castelán Castro wrote:
> The Poly/ML mailing list appears to be down at the moment.
David Matthews is the guy behind this. I have contacted him privately,
and he has now updated the webiste http://polyml.org to refer to the
changed URL of the mailing list:
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
David seems to be not subscribed here, so I am posting this on his behalf.
Makarius
--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)
On 17/01/17 15:24, Chun Tian (binghe) wrote: > Sorry, I re-checked my Isabelle environment and found that the PolyML in > Isabelle is actually built by GCC (mingw versions), so my statement > about "PolyML cannot be built in ..." was completely wrong. The rest > ideas should still hold. It is indeed built with MinGW, but that is very difficult to do. See http://isabelle.in.tum.de/repos/isabelle/raw-file/Isabelle2016-1/Admin/polyml/INSTALL-MinGW which is just a reminder for me for the precise versions need to be used. Otherwise it won't work. Maybe we can open a discussion on the Poly/ML mailing list, if this rather old version of gcc on MinGW is still needed, or if things can be updated and simplified. Concerning system structures in ML, see also: http://isabelle.in.tum.de/repos/isabelle/raw-file/Isabelle2016-1/src/Pure/ML/ml_system.ML http://isabelle.in.tum.de/repos/isabelle/raw-file/Isabelle2016-1/src/Pure/System/bash.ML Here the bash.exe is the one from Cygwin -- that is required for add-on tools of Isabelle. Makarius -- Check out the vibrant tech community on one of the world's most engaging tech sites, SlashDot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] CFP: Logical Frameworks and Meta-Languages: Theory and Practice
Logical Frameworks and Meta-Languages: Theory and Practice Thursday, 23 June 2016 Affiliated with FSCD Porto, Portugal http://dlicata.web.wesleyan.edu/events/lfmtp2016/ Logical frameworks and meta-languages form a common substrate for representing, implementing, and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design and implementation and their use in reasoning tasks ranging from the correctness of software to the properties of formal computational systems have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors, and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process. LFMTP 2016 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following: * Encoding and reasoning about the meta-theory of programming languages and related formally specified systems. * Theoretical and practical issues concerning the treatment of variable binding, especially the representation of, and reasoning about, datatypes defined from binding signatures. * Logical treatments of inductive and co-inductive definitions and associated reasoning techniques. * New theory contributions: canonical and substructural frameworks, contextual frameworks, proof-theoretic foundations supporting binders, functional programming over logical frameworks, homotopy type theory. * Applications of logical frameworks, e.g., in proof-carrying architectures such as proof-carrying authorization. * Techniques for programming with binders in functional programming languages such as Haskell, OCaml, or Agda and logic programming languages such as lambda Prolog or Alpha-Prolog. == Important Dates == Friday, April 8th: Abstract deadline Wednesday, April 13th: Submission deadline Friday, May 13th: Notification to authors Friday, May 27th: Final version due Thursday, June 23rd: Workshop date == Submission == In addition to regular papers, we also solicit "work in progress" reports, in a broad sense. Those do not need to report fully polished research results, but should be interesting for the community at large. Submitted papers should be in PDF, formatted using the ACM sigplanconf style files. The length is restricted to 10 pages for regular papers and 7 pages for "Work in Progress" papers. Accepted regular papers will be included in the proceedings, which will be published in ACM digital library in its International Proceedings series. == Program Committee == - Edwin Brady - Gilles Dowek, co-chair - Marcelo Fiore - Andrew Gacek - Olivier Hermant - Chantal Keller - Dan Licata, co-chair - Bernardo Toninho - Makarius Wenzel -- Site24x7 APM Insight: Get Deep Visibility into Application Performance APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month Monitor end-to-end web transactions and take corrective actions now Troubleshoot faster and improve end-user experience. Signup Now! http://pubads.g.doubleclick.net/gampad/clk?id=272487151=/4140 ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] HOL4 build, deps etc.
Dear HOL4 experts, I am trying to understand HOL4 build management. After some initial struggles, I have managed to make a regular build of everything via bin/build. Now I want to see which sources are used in which canonical order. The file tools/build-sequence appears to specify that abstractly, but I want to get the resulting sequences of ML files. I've looked around tools/build.sml and tools/buildutils.sml a bit, and it ultimately seems to converge towards Holmake invocations. The latter is unclear to me. Which are typical targets, e.g. for the kernel or core theories? Maybe there is even some Holmake command line option to ask for used file dependencies of such targets? Makarius -- Don't Limit Your Business. Reach for the Cloud. GigeNET's Cloud Solutions provide you with the tools and support that you need to offload your IT needs and focus on growing your business. Configured For All Businesses. Start Your Cloud Today. https://www.gigenetcloud.com/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] HOL workshop, August 2-3
On Thu, 25 Jun 2015, Ramana Kumar wrote: Everyone is welcome! A draft program can be found on the workshop website: https://www.cl.cam.ac.uk/~rk436/hol15/ Thanks for welcoming even non-HOL4 guys like myself. As can be seen on the program, I've got a rather generous slot with hacking and discussion about the following topic: Isabelle/PIDE/jEdit as integrated development environment for Standard ML After more than 7 years of development, Isabelle/PIDE/jEdit is today the standard way to interact with that particular proof assistant. In Isabelle2015 (May 2015) the TTY-based REPL and its wrapper for Proof General / Emacs have already been dismantled. This radical move might be taken as an opportunity of the HOL4 community to attract former Isabelle users who really do want to use plain TTY interaction. Or as an opportunity to discuss possibilities for HOL4 users and developers to make their own moves towards full-scale IDE support. As a very modest start, I would like to present various possibilities of Isabelle/PIDE to operate as IDE for Standard ML, which happens to be the underlying language platform of HOL4 as well. This touches various facilities of Poly/ML that David Matthews provides specifically to tool builders: run-time compiler invocation with IDE feedback, toplevel environment management, structured toplevel printing (with markup and hyperlinks), and potentially also run-time debugging of SML (still unused in Isabelle2015). Beyond that it is also possible to integrate any other languages that are related or unrelated to the prover platform, using PIDE libraries either on the ML or Scala side of that IDE framework. If anybody has specific interests, it is possible to tell me beforehand (privately or here on the list) so that I can adjust the workshop presentation accordingly. Makarius -- Monitor 25 network devices or servers for free with OpManager! OpManager is web-based network management software that monitors network devices and physical virtual servers, alerts via email sms for fault. Monitor 25 devices for free with no restriction. Download now http://ad.doubleclick.net/ddm/clk/292181274;119417398;o ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Isabelle-like advanced rule induction in HOL4?
On Thu, 12 Mar 2015, Michael Norrish wrote: I’ve made a feature request on Github (https://github.com/HOL-Theorem-Prover/HOL/issues/244), which may help remind me to implement this very nice feature. (Not that it *has* to be me that implements it…) Funny. Note that the Isabelle situation is a bit convoluted after many years of advanced induct, induction, coinduct, coinduction. A bit too many authors have worked on cumulatively better versions, but there is nobody who understands all details. Of course, it *has* to be me to clear it out one day, unless some unexpected miracle happens. Makarius-- Dive into the World of Parallel Programming The Go Parallel Website, sponsored by Intel and developed in partnership with Slashdot Media, is your hub for all things parallel software development, from weekly thought leadership blogs to news, videos, case studies, tutorials and more. Take a look and join the conversation now. http://goparallel.sourceforge.net/___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] The HOL-Omega Tutorial is now available
On Mon, 4 Mar 2013, Peter Vincent Homeier wrote: There was a bug in the previous version of the HOL-Omega system which prevented it from building with Poly/ML 5.5, the current version of Poly/ML. This has been fixed and posted to the public repository for HOL-Omega, and the current version should build correctly. If anyone has tried building HOL-Omega and been frustrated, please try again with this new version of HOL-Omega. In your changeset https://github.com/mn200/HOL/commit/9b92ae9 you say ... caused a type error with Poly/ML version 5.5. This is a difference from Poly/ML version 5.3. Does it mean you were still using old Poly/ML 5.3 until recently? For Isabelle, the advances from 5.3 to 5.4 to 5.5 made a big difference in performance. 5.5 is particularly nice, since it allows to run even big sessions in plain-old 32bit address space -- due to the online sharing of immutable data that David Matthews is doing now for all of us. How is the situation for HOL4 concerning Poly/ML performance? Makarius -- Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_d2d_feb ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] A new HOL Light tool for verification of nonlinear inequalities
On Fri, 23 Nov 2012, Alexey Solovyev wrote:
* Page 15:
move: {1}x a transforms the goal into !x1 a. a + x1 = x + 3, where
x1 is an automatically generated name.
How does that compare to SSReflect by Gonthier? It is one of the very
few points where SSReflect and Isar agree, to have generated names
never intrude the proof text implicitly. Does that actually
happen above for HOL Light, or is it just the text confusing me?
I'm not sure how this is done in SSReflect/Coq since I rarely used this
construction in my SSReflect/Coq proofs (in SSReflect/HOL Light, I'm not
using it often either). The SSReflect manual shows a similar example with a
similar outcome (see http://hal.inria.fr/inria-00258384, pages 27-28). I
agree that this is not a good way to interfere with the proof. Usually, this
construction is immediately followed by the introduction tactical = which
replaces auto-generated names with user-provided names.
OK, I see the following on page 28 of the SSReflect/Coq manual:
forall n n0 : nat, n = n0 - G.
where the name n0 is picked by the Coq display function, and assuming n
appeared only in G.
I shall probably ask Gonthier about it the next time I see him.
On the other hand, in rare situations even Isar violates its own
principles about intrusion of generated names into the proof, notably in
certain induction proofs.
Makarius
--
Monitor your physical, virtual and cloud infrastructure from a single
web console. Get in-depth insight into apps, servers, databases, vmware,
SAP, cloud infrastructure, etc. Download 30-day Free Trial.
Pricing starts from $795 for 25 servers or applications!
http://p.sf.net/sfu/zoho_dev2dev_nov
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] A new HOL Light tool for verification of nonlinear inequalities
On Fri, 23 Nov 2012, Alexey Solovyev wrote: * 'have' as subgoal: I reckon it is simular to subgoal_tac in Isabelle or its counterpart in HOL. In Isar, I made this quite different: having a first-class notion of proof context, 'have' is just a fresh local goal within it, and its result a theorem with certain assumptions, which is then re-used in the enclosing proof. This gives you more structure and scalability than just goal-modifications in the old style. 'have' is implemented via SUBGOAL_THEN in HOL Light. Your implementation of 'have' in Isar sounds interesting, but could you give examples when local theorems are better than just subgoals? After so many years of first-class notion of proof context and local facts within it, I find it hard to explain its many benefits. So here are just some aspects to get an idea. (1) Occam's razor. Traditional tactical provers encode local results by pushing more and more premises into subgoals. This is somehow indirect: SUBGOAL_TAC and relatives do some logical bookeeping to do nothing more than saying you want to use later again what you had before already. To carry around local facts, I don't need logic. I just carry them around (in ML). A more basic instance of this principle are multiple facts, e.g. groups of related things like LE_1 in arith.ml of HOL-Light from today (rev 152). let LE_1 = prove (`(!n. ~(n = 0) == 0 n) /\ (!n. ~(n = 0) == 1 = n) /\ (!n. 0 n == ~(n = 0)) /\ (!n. 0 n == 1 = n) /\ (!n. 1 = n == 0 n) /\ (!n. 1 = n == ~(n = 0))`, Here Isar makes an ML list of several thm values, not a thm with several propisitions encoded via auxiliary connectives. Getting rid of redundant conjunctions (and auxilary quantifiers) should be rather obvious. If you add management of implicit hyphotheses from the context (like Coq sections, Isabelle locales, or rather Isar proof contexts) you are coming towards genuine local facts. Just facts within a context, without funny logical decorations. In your SSReflect/HOL Light manual you were speaking about the proof context in a way that might get close to that already. An important aspect of the small-scale reflection of Gonthier's original version seems to be similar avoidance of logical inconveniences. Although he is still somehow tied to his type theory. (2) Structure. The most basic indication of a structured proof step is an indication of its relevant facts: the collection of facts that might contribute to it at most. It is given explicitly. (Tools may also have a secondary context of implicit facts declared as hints in the library). If you add more and more results from SUBGOAL_TAC to you goal state, you get more and more potentially used premises. This looses information to the user. Which 1 or 2 or 3 of 20 of them contribute to the proof? (3) Scalability. Like (2) but affecting automated proof tools. Overcrowded goal states slow down proof search, or make it loop. Isar has greatly benefitted from explicit fact indication before entering the next goal statement. So relatively heavy automated tools have become more useful after the main reform in 1999. For example, you write: from fact1 fact42 fact99 have XXX by auto instead of implicit use from the old times: from prems -- 99 things produced before have XXX by auto Another aspect of scalability: having many independent 'have' goal states in your proof allows the prover to schedule things fexibly and in parallel. It is good to be relived from the one central goal state where everything had to be fiddled through sequentially. Makarius -- Monitor your physical, virtual and cloud infrastructure from a single web console. Get in-depth insight into apps, servers, databases, vmware, SAP, cloud infrastructure, etc. Download 30-day Free Trial. Pricing starts from $795 for 25 servers or applications! http://p.sf.net/sfu/zoho_dev2dev_nov ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
On Sun, 5 Aug 2012, Konrad Slind wrote: My opinion is that Peter Homeier's HOL-Omega is the right setting to properly implement something locale-like, since it provides quantification over type variables in the logic. In plain old HOL the implementation of locales as essentially assumptions on goals is too limiting for polymorphism. In the 1.5 decades refining Isabelle locales, we have separated these two concerns: (1) management of local contexts and definitional specifications wrt. local contexts, (2) logical foundations for building actual abstract contexts. (1) is the infrastructure, consisting of quite a bit of abstract non-sense. It is now called local theory in Isabelle. It provides some interfaces for definitions in a local context, where the results are polymorphic in the sense of Hindley-Milner, but some types may remain fixed according to the context. (2) are concrete implementations of locales, type classes, type-class instantiation, unrestricted overloading etc. This could cover other concepts for modular theories using facilities of HOL-Omega, or external theory interpretation as in Isabelle/AWE from Bremen. Both (1) and (2) are difficult to implement. We are still working on various fine points concerning local syntax (via notation or abbreviation) that moves between such local contexts. Another challenge that I have boldly revisited this year is to allow nesting of locale-like contexts. What is also difficult to get right are declarations for proof tools associated with theorems produced in abstract situations, when they start moving around to other contexts. E.g. ways to manage simpset-like containers in conformance to abstract theories and their interpretations by concrete instances. Type classes have turned out an important special case for all that, because the abstraction looks concrete, via polymorphic constants with some specific type constraints. Syntax and tool declarationas are often stable wrt. type-instantiation of class constants, without further ado. Makarius -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Proof assistants for way more people
On Thu, 19 Jul 2012, Freek Wiedijk wrote: Doesn't the Isabelle kernel now have a feature that you can postpone proving a thm and still already being allowed to use it? I think Makarius put that in the kernel especially to be able to parallelize Isabelle proof checking on multi-core machines? Yes, this concept is called proof promise. See page 5 of my PLMMS 2009 paper http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf Note that at the bottom right of page 5, the two main kernel rules (promise) and (fulfill) have been simplified later: \Pi_2 is required to be empty (all pending promises already fulfilled) and the \Pi_2 a check becomes obsolete --- it would be hard to implement anyway. Moreover note that the idea to fork proofs in one context and join later in another context hinges on the \Theta_2 = \Theta_1 test of (fulfill). This works in Isabelle thanks to theory certificates that were introduced by Larry in the 1990-ies, and refined by myself over the years. HOL4 and HOL-Light lack that concept. (John Harrison keeps asking me every 10 years what is its purpose :-) Proof promises are used for parallel proof checking, but the basic concept is independent of all that: a promise acts like a polymorphic proof constant that can be replaced later on, by substituting with its definition. This is like an implicit let-redex within the conceptual proof term language -- LCF systems usually omit that structure in memory. Contrast promises with oracles, which are polymorphic contants that are postulated but never replaced (implemented). Cf. 'sorry' in Isabelle. Contrast promises also with ASSUME, which is like a non-polymorphic lambda over the proof; it also tends to get in the way of other tools, not just the pretty printer. Cf. Shallow lazy proofs at TPHOLs 2005. My general plan is to make more aggressive use for proof promises in the Isabelle/PIDE interaction model, not just to improve parallelism, but do get top-down development by default without the user having to say 'sorry' all the time. Makarius -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] How do I reinitialize HOL in the command window?
On Wed, 27 Jun 2012, Gottfried Barrow wrote: An issue being migrating off of teTeX, if you want to completely get off of Cygwin. In Cygwin setup, it shows tetex-extra at version 3.0.0-3. At http://www.tug.org/tetex/, it says: I (Thomas Esser) have decided not to make new releases of teTeX any more (May 2006). The information below might get out of date as time goes by. But I have batch files and scripts to compile highlighted sections of LaTeX with MiKTeX. To compile LaTeX through isabelle latex would complicate things, and then Cygwin teTeX being old complicates things, so I stick with what's been working for me, but someday I might want antiquotations. http://www.tug.org/texlive/ seems to support Cygwin directly by its own installer, without going through the Cygwin package management. So it might be worth trying that. I haven't done anything to change the setup for ~~/contrib/cygwin-1.7.9. Cygwin from 2012 poses some challenges to threads and sockets in Poly/ML, rendering it quite unstable for big applications. This is why I have downgraded to cygwin-1.7.9 from spring 2011. I hope to pick up this loose thread again together with David Matthews. It is one of the motivations to take Poly/ML on MinGW into account more seriously. Another would be native x86_64 support that is still unavaible for Cygwin after so many years. This might be also relevant to HOL maintainers, who want to move towards more serious support of Poly/ML and Windows. Makarius -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] How do I reinitialize HOL in the command window?
On Mon, 25 Jun 2012, Michael Norrish wrote: On 25/06/12 05:49, Makarius wrote: The bare-bones Cygwin with perl and python weights merely 100 MB, the JRE/JDK 200 MB, and avarage Isabelle logic image 150 MB. Disk space is cheap of course, so being too worried about space is perhaps not such a big deal. More worrying perhaps is the thought that users may not appreciate having new systems thrown onto their computers if doing so affects things other than their theorem-proving. My limited experience with Cygwin (independent of any theorem-proving, and a while ago now) is that it could make its presence felt, even in areas where it was not wanted. Past versions of Cygwin had this principle that there can be only one cygwin.dll installed on the system. So putting one version of it here would prevent to install another version there. Moreover, the installer would change various registry entries globally that then affect other Cygwins. With more recent Cygwin 1.7.x is has become possible to make a pre-canned Cygwin installation that does not affect anything else. In Isabelle2012 I have packaged it like that for the first time, hopefully with some success. I have also changed some defaults to make HOME the actual Windows home, not the one of that particular copy of Cygwin. This is becoming more and more alien to the Unix guy, but Windows users feel more at home with it. Makarius -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
On Wed, 30 May 2012, Josef Urban wrote: On Wed, May 30, 2012 at 8:19 AM, Bill Richter rich...@math.northwestern.edu wrote: BTW Makarius seemed to say on the Isabelle group that Mizar is exactly FOL with some automation to relieve the tedious parts of FOL. Mostly yes. It is (a bit strengthened) ZFC/FOL with small amount of second-order automation to handle things like infinite axiom/theorem schemes and Fraenkel terms (which behave quite a bit like lambda abstractions). The main difference to HOL is that weird sets (like von Neuman ordinals) are part of the ZFC universe, which is (at least by default) prevented by the strong type discipline in HOL. HOL's (type-constrained) higher-order functions map to first-order citizens of ZFC. For practical purposes, there does not seem to be much difference. An overwhelming part of both systems is first-order reasoning. It is a bit difficult to have discussions stretched over several mailing lists ... Bill has quoted me in a too restrictive sense: I did not say exactly FOL about Mizar, but characterization of Mizar by Josef is fine for me. Concerning Isabelle, I need to try again to work against the standard misconceptions by most outsiders. There are at least 3 different conceptual layers involved: * Isabelle/Pure as framework for unrestricted natural deduction (nothing said about order of the logic yet), * Isabelle/Isar as proof language on top of the framework, and * Isabelle/HOL as the main application environment, including extra tools. If you start identifying Isabelle/HOL with Isabelle, and pretending that it is basically just FOL anyway, than you won't understand Isabelle. We should probably switch back to the other mailing list to work this out further ... Makarius -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
On Sun, 13 May 2012, Ramana Kumar wrote: On Sat, May 12, 2012 at 11:54 PM, John Harrison john.harri...@cl.cam.ac.ukwrote: | Does this mean unit lists in HOL Light? :) | I'm thinking of adding a check that there are no more than 2^30-1 type | variables in the input theorem. I don't exclude either possibility yet... And what about switching to big integers? (for HOL Zero and/or HOL Light) I thought HOL Zero might be switching to SML at some point anyway? With unit list John was probably hoping to have a precise model of natural numbers in OCaml. This is not exactly the case, because datatype values can have loops in that language: let rec uuuh = () :: uuuh;; List.length uuuh;; Anyway, I think we need to find an exit strategy from this endless thread. Already in October 2009, I've tried to convince Mark that OCaml is not the right vehicle for extremely high trustability that he wants to have for HOL Zero. And back then, I did not know all these nasty tricks yet that can be learned in the coffee room of LRI, with hardcore experts like Filiatre showing off all the boundary cases and neat tricks outside the normal mathematics of ML. This is why SML never became very popular, because it spoils these games. Makarius -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
for bound variables (free ones are named as in HOL-Light). Larry used to have some code that would convert the index (unbounded integer) back and forth wrt. a singleton string (essentially an 8bit integer simulated in SML90 without char type). When David von Oheimb did his Bali formalizations in the late 1990-ies, he hit that wall with terms that had more than 255 nested abstractions. Luckily it was an exception, not a kernel flaw. Back then, I repaired Larry's code and resisted the temptation to upgrade the 8bit integer into 16bit. Instead I made an unbounded representation within the string type in the ovious way. Anyway, for LCF-style kernel design type int and string are often interchangeable to identify formal entities. We have now both side-by-side for the main formal entities: types, consts, axioms etc. all have a fully-qualified name and a unique integer id in the internal tables. For both I expect immutability and unboundedness, at least in the usual approximative sense of concrete machines running out of memory eventually. The main critical operation of the sub-kernel infrastructure is now a counter to produce fresh integers. One could probably do this with 64bit word arithmetic and explicit bounds check equally well; it means the machine will stop working at some point in the future, and needs to be restarted. Still, maybe Mark Adams will find a flaw in that reasoning and then I'll change to using unit list instead of int! For such a high-assurange project, I would recommend judicious use of immutable strings or 64 bit bounded machine integers (with explicit overflow check), depending on the situation. Makarius -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
On Sat, 5 May 2012, Mark wrote: Makarius wrote: This Obj stuff is absent in SML. Yes and I plan to port HOL Zero to SML. SML is fundamentally safer and better defined than OCaml. I think I would have used SML from the onset if I knew about these OCaml vulnerabilities. Although OCaml is nicer in other ways .. I didn't know you are still planning to switch back to SML. Anyway, what did you find nicer about OCaml? As I've said, I was a bit scared by its proximity to C in many ways, when I did my little YXML implementations in 3 days (half of the time figuring out semantic snags of OCaml string operations and library modules). Makarius wrote: Moreover, as I have explained to Mark Adams already in a similar discussion, one can seal up the toplevel interpreter loop, to isolate user scripts from any such built-in nonsense. ... A managed ML toplevel is again one of these layers that would complicate a prover implementation, but make it more reliable. These techniques have the effect of removing vulnerabilities, but at the expense of greatly complicating the implementation, perhaps introducing their own vulnerabilities. What I would really like is an ML interpreter with a toplevel that can be configured to disallow all nasty stuff (e.g. overwriting the 'thm' datatype, or overwriting its pretty printer). The latter is pretty close to what I've meant above. In Poly/ML you can define how the ML toplevel reads or writes the environment of types, values, structures etc. so you can do some sandboxing there in a few pages of ML. Makarius wrote: I've looked at holzero-0.4.1 before and just today at holzero-0.5.4. (I am still hoping to see a really convincing independent proof checker for the HOL family of systems.) In what sense is HOL Zero not a convincincly independent implementation of the HOL logic? I did not look at all details yet. The project looks generally very interesting, to get a dependable external checker for HOL eventually. For the moment my main observations are: * A bit too much extra complication to repair OCaml strings. If you forget just one immutise in a criticial spot, you have a vulnerability. Such things need to be right by default, due to the underlying programming language. * Still too many obvious attacks are simply declared as forbidden in the Bounty.txt. Here is the copy from holzero-0.5.4 for the record: - building HOL Zero from a non-standard ML session state (e.g. with parallelism) - overwriting key ML objects (e.g. the 'thm' datatype or 'get_all_axioms') - overwriting the pretty printer for key ML datatypes (e.g. 'thm' or 'list') - circumventing the ML language proper or its type system (e.g. 'Obj.magic') - circumventing, reconfiguring or interfering with the ML interpreter - exploiting bugs in the ML interpreter - changing the operating system environment in which the ML interpreter runs I reckon that Milner's LCF had less vulnerabilities. For example, ML with parallel threads should now be standard, not non-standard as declared above. It is merely a historical accident that OCaml is still sequential by default. Your code will require some additional refinements to make it thread-safe, which requires some piling up of more stuff. An alternative would be to nail down the environment to be always sequential. Makarius -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
On Thu, 3 May 2012, Freek Wiedijk wrote: This is not very much about HOL as such, so if this reply is inappropriate for the HOL list, I apologise: I am also a guest here, so we try to behave as best as we can. mutating the names of constants. I always found this mutable constants complaint silly. Many people make it, but it never struck me as significant. The question is what is the name of the game you want to play. Mutable term language is not quite LCF approach, where the static type discipline is supposed to ensure correctness-by-construction. For HOL-Light, John always keeps an eye on his sources -- static check by human inspection. The ACL2 guys also manage that by hand in their weakly typed language, by restricting the number of people who work on the code-base to two. For a huge system with many contributors you can't do that. This is where a robust LCF approach really helps. Mark Adams occasionally promotes an even more aggressive scenario for HOL Zero where he wants to admit potentially malicious users, an army of paid proof-workers who want to cheat. (I am not really following him here, we are not that far yet.) Surely in every practical programming language you can cheat in some way if you try hard enough. For instance by poking the memory, either internally through some Obj.magic like interface This Obj stuff is absent in SML. You can make nonsense with some implementations, but we reduce that danger by running with more than one, so it is essentially the intersection of the semantics. Moreover, as I have explained to Mark Adams already in a similar discussion, one can seal up the toplevel interpreter loop, to isolate user scripts from any such built-in nonsense. I think the original LCF by Milner actually did work like that, since ML was a closed interpreter within LISP. (Unfortunetely, I've only ever seen the sources of Cambridge LCF. Does anybody happen to have the older ones from Edinburgh or Standard?) A managed ML toplevel is again one of these layers that would complicate a prover implementation, but make it more reliable. We don't have that in Isabelle, because the malicous scenario is a bit artificial, but there is some runtime compiler support to allow the user to work with ML bindings in a stateless manner. or if you don't get that from your language by poking in /dev/mem? That's another game. A computing system consists of many layers. If you have full physical or logical access to critical ones, you can do whatever nonsense you want. Milner had some very important ideas in the 1970-ies how to organize the chaos, such that you get mostly real theorems out of it -- by restricting to certain layers, and some infrastructure to enforce that. What's important is that you won't cheat accidentally, by misunderstanding how things work. I've recently made my first practical steps in OCaml and was a bit scared by its proximity to C. After 20 years of SML I am probably spoilt by too clean programming language semantics. I did cheat by accident, stumbling over standard semantic traps of low-level languages. Most languages have that, but it does not mean one cannot do better. Again, these oberservations are more relevant to a project like HOL Zero than for HOL-Light. I've looked at holzero-0.4.1 before and just today at holzero-0.5.4. (I am still hoping to see a really convincing independent proof checker for the HOL family of systems.) My impression is now that he *is* piling up more and more stuff to make up for the semantic weaknesses of OCaml for his project. Makarius -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
On Thu, 3 May 2012, John Harrison wrote: Of course, the ability to understand a system down to the bottom does have real value for those whose intended use is a bit more radical and outside the normal or expected usage model. Besides, I think many people are interested in formalization precisely because they want to have a clearly understood foundation, a kind of search for certainty. So those who are naturally drawn to formalization in the first place may also appreciate being able to understand completely the logical and software engineering foundations of a system. This is a delicate and very interesting aspect. A system like HOL-Light has the advantage that the reader gets quickly an impression what the basic logic functionality is meant to be. This gives some certainty under additional assumptions, i.e. that the ML really is what it seems at first sight, and that certain bad things are not done in practice. (Say someone taking apart terms and mutating the names of constants.) When Mark Adams showed his new HOL0 system for in Cambridge in 2009, he did not know yet about these snags of OCaml. Both type int and string are somehow insecure on this platform. I've also done a tiny bit of OCaml implementation myself some weeks ago, and had to look a few days very closely what the basic operators mean, say equality on strings. Sealing up such holes makes the implementation more complex. For example, the Coq people have their own version of int and string that really mean int and string in a mathematical sense, without silent overflow or hidden mutation. Driving this further and further, adding infrastructure to address weaknesses of the implementation and other side-conditions, you get to a highly complex system like Isabelle. Here the idea is to provide a secure and fast environment to the end-user, like an operating system does, but the first impression that one could easily understand it is lost. Makarius -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
On Tue, 24 Apr 2012, Bill Richter wrote: Roger, if there's ``some cultural aversion to the use of axioms in the HOL community,'' then maybe HOL isn't the right proof-checker to use in high school geometry classes. Does anyone think there is a better proof-checker? My guess is that this is just an interface problem that HOL could easily solve, and I'm willing to work on it myself. The strict definitional approach is mainly for foundational purposes, and for good reasons. The HOL community usually quotes Bertrand Russel on that: The method of postulating what we want has many advantages; they are the same as the advantages of theft over honest toil. Introduction to Mathematical Philosophy, New York and London, 1919, p 71. This means things like inductive definitions, datatypes, recursive functions are explicitly reduced to basic principles, not axiomatized by some magic ML code. Moreover your own concepts should be defined properly, and results stated and proven explicitly. Nonetheless, this does not prevent the user from working in a local context with parameters and assumptions in a quasi-axiomatic manner. Your results would then be releative to certain premises my_pred x y z == ... in terms of the logical foundations. By organizing such assumptions in a reasonable way, your application does not have to expose this to the end-user. Don't ask me how to do that in HOL4, HOL-Light, ... though. I am merely a guest on this mailing list. Makarius -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
On Sat, 21 Apr 2012, Bill Richter wrote: Mizar has a particularly annoying feature of not allowing TABs or the symbols for implies etc which Isabelle/Isar (which I never built or understood) uses. So I wrote some emacs code .mizar-isar.el which gets around this. Now I write up my Mizar code in Isar fashion, using the forbidden symbols ⇒ ¬ ∨ ∧ ≡ ∀ ∃ ⇔ and not worrying abo I was occasionally considering to disallow TABs formally in Isabelle/Isar as well -- they just introduce too many problems for very little benefit. To start using Isabelle/Isar you should not build it, just take one of the platform-specific distribution bundles from its download page and run it. The different prover platforms all have their own cultural background. And for starting a serious project you should try to figure out which culture accomodates your own most closely. Makarius-- For Developers, A Lot Can Happen In A Second. Boundary is the first to Know...and Tell You. Monitor Your Applications in Ultra-Fine Resolution. Try it FREE! http://p.sf.net/sfu/Boundary-d2dvs2 ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Quick and easy exchange of ML values via XML/YXML
Dear HOL users, in the old LISP days, exchange of symbolic data was really trivial, using built-in read/write functions for s-expressions. Later things became more complex in ML, and especially with XML. The following tiny library in SML or OCaml makes things again mostly trivial: https://bitbucket.org/makarius/yxml/src/ YXML is pronounced Why XML. It is both the question and answer to the problem of concrete transfer syntax of seemingly trivial tree expressions. The other part is a rather obvious combinator library to represent typed ML expressions over untyped XML, in the same spirit as the ML runtime would do that for untyped bits in memory. Isabelle/ML has included both as standard library functions for quite some time already. Maybe the independent versions above help to bridge over to other provers from the HOL family. Makarius -- This SF email is sponsosred by: Try Windows Azure free for 90 days Click Here http://p.sf.net/sfu/sfd2d-msazure ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] LAST CALL FOR WORKSHOP PROPOSALS: TPHOLs 2009
LAST CALL FOR WORKSHOP PROPOSALS: TPHOLs 2009 The 22th International Conference on Theorem Proving in Higher Order Logics 17 - 20 August 2009 (main conference) 21 August 2009(workshops) in Munich, Germany ** * http://tphols.in.tum.de/ * ** TPHOLs is a series of international conferences that started in 1988 and brings together researchers working in all areas of interactive theorem proving. The main conference will be held on 17 through 20 August 2009 in Munich. There will be an extra day for associated workshops: 21 August 2009. Workshop proposals -- Workshops to be proposed here as an associated event to TPHOLs 2009 should be related to the general theme of interactive theorem proving or some of its application areas. See also the call for papers of the main conference to get an idea about the topics covered there. Both well-established workshops and newer ones are welcome. The basic format will be that of a one day event on 21 August 2009, after the main conference. Workshop proceedings can be published as a technical report of TU München, if required. Proposals or any further questions should be sent by e-mail to the TPHOLs 2009 workshop chair: Makarius Wenzel makar...@sketis.net Please include the following information in particular: * Workshop name and abbreviation * Names and affiliations of organizers * Topics covered by the workshop, possibly with some links to websites of earlier instances of the workshop. Important Dates --- Submission of proposals:15 January 2009 Notification: 31 January 2009 Workshops: 21 August 2009-- Check out the new SourceForge.net Marketplace. It is the best place to buy or sell services for just about anything Open Source. http://p.sf.net/sfu/Xq1LFB___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] polyml thread support
On Sun, 9 Nov 2008, Lu Zhao wrote: Can I use the thread support in PolyML to do this task? and how? I'd like to run a ML function, which runs a HOL proof, for a certain amount of time, say 20 seconds See also the thread Are timeouts possible in HOL (mosml or poly)? on this list (August 2008): http://sourceforge.net/mailarchive/message.php?msg_name=E1KOtVj-0008Aq-00%40mta1.cl.cam.ac.uk When working with threads in Poly/M,L I do recommend the latest version 5.2.1. Before there is a problem with GC and internal wait that can produce a deadlock (very rarely). Other examples for working with Poly/ML threads are available here: http://isabelle.in.tum.de/repos/isabelle/file/tip/src/Pure/Concurrent/ Makarius - This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100url=/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] CALL FOR WORKSHOP PROPOSALS: TPHOLs 2009
CALL FOR WORKSHOP PROPOSALS: TPHOLs 2009 The 22th International Conference on Theorem Proving in Higher Order Logics 17 - 20 August 2009 (main conference) 21 August 2009(workshops) in Munich, Germany ** * http://tphols.in.tum.de/ * ** TPHOLs is a series of international conferences that started in 1988 and brings together researchers working in all areas of interactive theorem proving. The main conference will be held on 17 through 20 August 2009 in Munich. There will be an extra day for associated workshops: 21 August 2009. Workshop proposals -- Workshops to be proposed here as an associated event to TPHOLs 2009 should be related to the general theme of interactive theorem proving or some of its application areas. See also the call for papers of the main conference to get an idea about the topics covered there. Both well-established workshops and newer ones are welcome. The basic format will be that of a one day event on 21 August 2009, after the main conference. Workshop proceedings can be published as a technical report of TU München, if required. Proposals or any further questions should be sent by e-mail to the TPHOLs 2009 workshop chair: Makarius Wenzel [EMAIL PROTECTED] Please include the following information in particular: * Workshop name and abbreviation * Names and affiliations of organizers * Topics covered by the workshop, possibly with some links to websites of earlier instances of the workshop. Important Dates --- Submission of proposals:15 January 2009 Notification: 31 January 2009 Workshops: 21 August 2009- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100url=/___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Are timeouts possible in HOL (mosml or poly)?
On Fri, 1 Aug 2008, Mike Gordon wrote: Does anyone know if it is possible to run a function (e.g. SIMP_CONV arith_ss []) for a fixed time and then fail on timeout. I vaguely remember that there was no way to do this, but want to double check. This is reasonably easy in recent versions of Poly/ML (5.1 or 5.2), thanks to support for (native) Posix threads. The basic idea is to have a watchdog interrupt the current worker after some time: structure TimeLimit = struct exception TimeOut; fun timeLimit time f x = uninterruptible (fn restore_attributes = fn () = let val worker = Thread.self (); val timeout = ref false; val watchdog = Thread.fork (fn () = (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []); (*RACE! timeout signal vs. external Interrupt*) val result = Exn.capture (restore_attributes f) x; val was_timeout = (case result of Exn.Exn Interrupt = ! timeout | _ = false); val _ = Thread.interrupt watchdog handle Thread _ = (); in if was_timeout then raise TimeOut else Exn.release result end) (); end; The interface emulates the TimeLimit structure of SML/NJ, even though that platform is no longer used seriously. See also the first part of http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2008/src/Pure/ML-Systems/multithreading_polyml.ML for the actual source, including some of our auxiliary combinators for changing thread attributes (interrruptibility etc.). Makarius - This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100url=/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] CFP - Programming Languages for Mechanized Mathematics Systems 2008
--- Jacques Carette (Co-Chair) (McMaster University, Canada) John Harrison (Intel Corporation, USA) Hugo Herbelin (INRIA, Ecole polytechnique, France) James McKinna (Radboud University Nijmegen, Netherlands) Ulf Norell (Chalmers University, Sweden) Bill Page Christophe Raffalli(Universite de Savoie, France) Josef Urban(Charles University, Czech Republic) Stephen Watt (ORCCA, University of Western Ontario, Canada) Makarius Wenzel (Co-Chair) (Technische Universitaet Muenchen, Germany) Freek Wiedijk (Radboud University Nijmegen, Netherlands) Important Dates --- * Submission deadline - 5 May 2008 * Notification of acceptance - 6 June 2008 * Final version - 7 July 2008 (approximately) * Workshop - 28-29 July 2008 - This SF.net email is sponsored by: Microsoft Defy all challenges. Microsoft(R) Visual Studio 2008. http://clk.atdmt.com/MRT/go/vse012070mrt/direct/01/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
