Re: [isabelle-dev] Monad_Syntax
On 09/11/2013 05:04 PM, Makarius wrote: On Tue, 20 Aug 2013, Christian Sternagel wrote: any opinions on making the type of monadic bind more general (see the attached patch)? This thread seems to be still open. I now pushed the rebased change as eeff8139b3d8. Do monadic people have a standard Unicode point to render that operator? I would expect that most monadic people don't care very much about Unicode and are happy with latex and ascii... Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Total failure of sledgehammer
Am 13.09.2013 um 09:34 schrieb Lawrence Paulson l...@cam.ac.uk: None of them work. Can you reproduce it in Proof General? As an additional test, you could try playing with options like debug and see if the output says anything interesting. Just to make sure it's not MaSh-related somehow, I would also recommend you comment out MASH=yes in your settings file and see if this has any impact. Another useful data point would be to know if you can run the HOL-Metis_Examples session. The file Proxies.thy contains some Sledgehammer regression tests that rely on SPASS. Otherwise I'm running out of ideas. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle_10-Sep-2013
On 12/09/2013 19:25, Makarius wrote: On Thu, 12 Sep 2013, René Thiemann wrote: I noticed that on my machines I often get an Insufficient memory error. Building Check-DPP ... poly(59646,0xacc9fa28) malloc: *** mmap(size=134217728) failed (error code=12) *** error: can't allocate region *** set a breakpoint in malloc_error_break to debug Fail Insufficient memory: /Users/rene/.isabelle/Isabelle_10-Sep-2013/heaps/polyml-5.5.0_x86-darwin/Check-DPP Check-DPP FAILED To be more precise, when using ML_OPTIONS=--minheap 1000 I did not get the error under Isabelle2013, but under Isabelle_10-Sep-2013, it often fails with setting. Fortunately, using ML_OPTIONS=--minheap 3000 mostly works, but it is still annoying, since with this setting, I cannot start two Isabelle sessions in parallel. Does someone else notice increased memory consumption / crashes? There is definitely some continous bloat factor with every new release, although David Matthews was usually ahead of most big applications in recent years. In fact he is about to release Poly/ML 5.5.1 pretty soon, so a quick test with some repository version of Poly/ML might help (e.g. SVN 1843). I would suggest trying with the --stackspace option e.g. ML_OPTIONS='--stackspace 500' The Fail exception with Insufficient space arises in a number of places such as when trying to fork a thread. This requires memory outside the ML heap. The stackspace option keeps some space free from the ML heap for these purposes. I would guess that this is when running the X86/32 version rather than X86/64. Is that correct? David ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle_10-Sep-2013
Dear David, There is definitely some continous bloat factor with every new release, although David Matthews was usually ahead of most big applications in recent years. In fact he is about to release Poly/ML 5.5.1 pretty soon, so a quick test with some repository version of Poly/ML might help (e.g. SVN 1843). I would suggest trying with the --stackspace option e.g. ML_OPTIONS='--stackspace 500' The Fail exception with Insufficient space arises in a number of places such as when trying to fork a thread. This requires memory outside the ML heap. The stackspace option keeps some space free from the ML heap for these purposes. I tried it, but the setting was not high enough: then even earlier sessions crash with a new 'Run out of store - interrupting threads' error message. This also happens if I set stackspace to 1500, but it succeeded with 5000. However, then still afterwards I get the usual poly(6820,0xb09a5000) malloc: *** mmap(size=16777216) failed (error code=12) *** error: can't allocate region error as before, if I use minheap=1000, or drop the minheap parameter. I would guess that this is when running the X86/32 version rather than X86/64. Yes, I use the 32-bit mode. I will later run some tests when using the 64-bit mode. Here is my current setup: ISABELLE_BUILD_OPTIONS= ML_PLATFORM=x86-darwin ML_HOME=/Users/rene/.isabelle/contrib/polyml-5.5.0-3/x86-darwin ML_SYSTEM=polyml-5.5.0 ML_OPTIONS=--minheap 1000 --stackspace 5000 Best regards, René ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle_10-Sep-2013
On 13/09/2013 11:08, René Thiemann wrote: I would suggest trying with the --stackspace option e.g. ML_OPTIONS='--stackspace 500' The Fail exception with Insufficient space arises in a number of places such as when trying to fork a thread. This requires memory outside the ML heap. The stackspace option keeps some space free from the ML heap for these purposes. I tried it, but the setting was not high enough: then even earlier sessions crash with a new 'Run out of store - interrupting threads' error message. This also happens if I set stackspace to 1500, but it succeeded with 5000. However, then still afterwards I get the usual poly(6820,0xb09a5000) malloc: *** mmap(size=16777216) failed (error code=12) *** error: can't allocate region error as before, if I use minheap=1000, or drop the minheap parameter. I would guess that this is when running the X86/32 version rather than X86/64. Yes, I use the 32-bit mode. I will later run some tests when using the 64-bit mode. Here is my current setup: ISABELLE_BUILD_OPTIONS= ML_PLATFORM=x86-darwin ML_HOME=/Users/rene/.isabelle/contrib/polyml-5.5.0-3/x86-darwin ML_SYSTEM=polyml-5.5.0 ML_OPTIONS=--minheap 1000 --stackspace 5000 You definitely don't want a value as large as 5000. I think the exception may be occurring with PolyML.shareCommonData. This needs memory outside the heap to hold some tables. If there is a lot of live data in the heap these tables can be large and if the heap is taking up most or all of the available virtual memory, a particular problem in 32-bit mode, you may get the above message and exception. Is that possible in this case? It is safe to handle the exception and continue; it's just that the sharing process will not be complete so that the heap will be bigger than it might otherwise be. Regards, David ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle_10-Sep-2013
Dear David, I would guess that this is when running the X86/32 version rather than X86/64. Yes, I use the 32-bit mode. I will later run some tests when using the 64-bit mode. Here is my current setup: ISABELLE_BUILD_OPTIONS= ML_PLATFORM=x86-darwin ML_HOME=/Users/rene/.isabelle/contrib/polyml-5.5.0-3/x86-darwin ML_SYSTEM=polyml-5.5.0 ML_OPTIONS=--minheap 1000 --stackspace 5000 You definitely don't want a value as large as 5000. I think the exception may be occurring with PolyML.shareCommonData. This needs memory outside the heap to hold some tables. If there is a lot of live data in the heap these tables can be large and if the heap is taking up most or all of the available virtual memory, a particular problem in 32-bit mode, you may get the above message and exception. Is that possible in this case? Most of the time, it indeed appears after the theories have been processed, and the heap-file is being generated. (e.g., I never get the error with isabelle build Check-DPP, only if I build the heapfile with isabelle build -b Check-DPP) Moreover, I now tested a bit the 64-bit version of poly, and there the error does not occur, even without specifying ML_OPTIONS. For me, this looks like the most sensible solution. It is safe to handle the exception and continue; it's just that the sharing process will not be complete so that the heap will be bigger than it might otherwise be. I see. Thanks for your helpful comments, René ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Advice for replacing @{simpset} with @{context}.
The relevant text from NEWS is this: * Simplifier tactics and tools use proper Proof.context instead of historic type simpset. Old-style declarations like addsimps, addsimprocs etc. operate directly on Proof.context. Raw type simpset retains its use as snapshot of the main Simplifier context, using simpset_of and put_simpset on Proof.context. INCOMPATIBILITY -- port old tools by making them depend on (ctxt : Proof.context) instead of (ss : simpset), then turn (simpset_of ctxt) into ctxt. So the only way to replace a HOL_basic_ss addsimps ... somewhere deep inside my code (in my actual case, inside a conversion) is to thread through the proof context everywhere? ... a quite tedious change. -- Peter ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Advice for replacing @{simpset} with @{context}.
On Fri, 13 Sep 2013, Peter Lammich wrote: The relevant text from NEWS is this: * Simplifier tactics and tools use proper Proof.context instead of historic type simpset. Old-style declarations like addsimps, addsimprocs etc. operate directly on Proof.context. Raw type simpset retains its use as snapshot of the main Simplifier context, using simpset_of and put_simpset on Proof.context. INCOMPATIBILITY -- port old tools by making them depend on (ctxt : Proof.context) instead of (ss : simpset), then turn (simpset_of ctxt) into ctxt. So the only way to replace a HOL_basic_ss addsimps ... somewhere deep inside my code (in my actual case, inside a conversion) is to thread through the proof context everywhere? ... a quite tedious change. Is this hypothetical, or do you still have tools without a proper context? It should be trivial to pass through some ctxt: Proof.context nonetheless, i.e. do the localization in that elementary sense. Unless there is something really strange here ... Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] trace_unify_fail
Hi, I just spent some time discovering where trace_unify_fail went (there now exists an attribute unify_trace_failure). As the introduction of this flag had a NEWS entry, wouldn't this change also merit a NEWS entry (in particular, as it is not documented in the reference manual)? Even if it is crude to use (due to it being a global-only option), it is an important debugging tool, in particular with large goals as you get in program verification. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Orphaned theory src/HOL/Library/Sum_of_Squares_Remote
This theory brands itself as »Examples with remote CSDP« and contains nothing beyond some sos invocations. It should be moved to HOL/ex. Any objections? Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle_10-Sep-2013 (fwd)
Another copy without the attachment, which did not get past the mailing list server. Makarius -- Forwarded message -- Date: Fri, 13 Sep 2013 20:48:54 +0200 (CEST) From: Makarius makar...@sketis.net To: David Matthews d...@prolingua.co.uk Cc: René Thiemann rene.thiem...@uibk.ac.at, isabelle-...@in.tum.de Subject: Re: [isabelle-dev] Isabelle_10-Sep-2013 On Fri, 13 Sep 2013, David Matthews wrote: I think the exception may be occurring with PolyML.shareCommonData. This needs memory outside the heap to hold some tables. If there is a lot of live data in the heap these tables can be large and if the heap is taking up most or all of the available virtual memory, a particular problem in 32-bit mode, you may get the above message and exception. Is that possible in this case? It is safe to handle the exception and continue; it's just that the sharing process will not be complete so that the heap will be bigger than it might otherwise be. I've made my own tests with the following setup: Poly/ML SVN 1848 IsaFoR a44e26d6605e Isabelle a49ce8d72a44 AFP 4e87a0fc2528 ML_PLATFORM=x86-darwin ML_HOME=/Volumes/Macintosh_HD/Users/makarius/lib/polyml/polyml-svn/x86-darwin ML_SYSTEM=polyml-5.5.1 ML_OPTIONS=--minheap 500 --gcthreads 4 --debug=sharing This produces the following information about the sharing phase of GC (attached file). Moreover, I have instrumented the C++ sources of polyml to figure out which of the 5 places of Insufficient memory are relevant here: it is the one in polyml/libpolyml/sharedata.cpp (line 882): raise_exception_string(taskData, EXC_Fail, Insufficient memory); If you say that we can just absorb an exception Fail Insufficient memory in ML, we can do that on the Isabelle/ML side as a workaround. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
Repair it or burn it? Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Total failure of sledgehammer
That fixed it. Larry On 13 Sep 2013, at 10:15, Jasmin Blanchette jasmin.blanche...@gmail.com wrote: Just to make sure it's not MaSh-related somehow, I would also recommend you comment out MASH=yes in your settings file and see if this has any impact. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jdk-7u40
On 14/09/2013, at 6:50 AM, Makarius makar...@sketis.net wrote: For example, they say that Apple Retina displays are now fully supported. Can people who are so lucky to have one test that, and say if it works, or if it requires further Java properties? The isabelle jedit tool allows to pass JVM options as argument to its -J option. Looks very nice out of the box. Retina fonts are working. Never seen Isabelle symbols that sharp ;-) Cheers, Gerwin The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
