[isabelle-dev] Advice for replacing @{simpset} with @{context}.
Hi all, I am in the process of updating some of our local tools to the repository version of Isabelle, in preparation for the next Isabelle release (possibly named Isabelle 2013-1?) One of the changes that has occurred since Isabelle 2013 is that simpsets have been deprecated in favour of storing simplifier rules directly in the context. In this new world order, what is the best way to manage long-term simpsets when they are not in active use? For example, imagine that I have a theorem attribute foo, which adds a rule to a set of theorems: lemma a [foo]: ... lemma b [foo]: ... lemma c [foo]: ... I also have a tactic bar which internally passes this set of theorems to the simplifier. The implementation in Isabelle 2013 is simple: have a simpset floating around in your theory data, add new theorems to it on demand, and finally use it when needed. I am not sure what the best way to port this forward is. I could store the theorems as a list in my theory data, but that would mean it would need to be converted into a discrimination net each time the tactic bar was used, which could have performance implications when the number of theorems is large. I could convert back and forth from a context each time a new rule is added as such: val new_ss = simpset_of ((put_simpset convenient ctxt old_ss) addsimps [new_thm]) but I suspect that this was not the intended solution. Any suggestions as to the best way to manage sets of rules that will eventually be fed into the simplifier? Thanks so much, David 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
Re: [isabelle-dev] New handling of int/nat
Am 11.09.2013 19:00, schrieb Florian Haftmann: Hi René, in Isabelle2012 (and 2013?), the types nat and int where (using Efficient_Nat) directly translated into SML's IntInf.int on code_export. This does not happen anymore in Isabelle-dev -- here they are now mapped to types in Arith. The new behavior yields problems when interfacing with the exported code to other SML-code (type mismatch). What is the proposed new way here? Port all definitions to use type integer instead of nat (natural also maps to something in Arith)? Or add a 'wrapper' to each definition?: there are official conversions between all those arithmetic types: int_of_integer, integer_of_int etc. These you can generate and rely on them in your interface code. So you are free to provide the interfaces either on the theory level or directly on the target language level. Thanks. I've been a bit reluctant about using the Arith.* functions in my handwritten SML-code (relying on generated stuff etc), hoping that there was something automagical. But now where you've stated that it's the way to go, I've done it like that. - René -- René Neumann Institut für Informatik (I7) Technische Universität München Boltzmannstr. 3 85748 Garching b. München Tel: +49-89-289-17232 Office: MI 03.11.055 smime.p7s Description: S/MIME Kryptografische Unterschrift ___ 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
Hi,
thanks Florian and Makarius for your help.
* Discontinued theories Code_Integer and Efficient_Nat by a more
fine-grain stack of theories Code_Target_Int, Code_Binary_Nat,
Code_Target_Nat and Code_Target_Numeral. See the tutorial on code
generation for details. INCOMPATIBILITY.
Finally, I tested the Scala code generation with my existing Scala
application. The biggest change is the Code_Target_Nat. It causes
minor changes to the code. Overall, few changes had to be made to
replace the generated Scala code of Isabelle2013 with
Isabelle_10-Sep-2013. However, there is one incompatibility I cannot
fix easily.
The generated code contains the following definition:
final case class Nata(a: BigInt) extends nat
In the old version, when printing for example the natural number 42, I
got 42. Now I get Nata(42). I don't see an easy way to fix this
without touching the generated code (except modifying my code
everywhere where a nat is printed which induces a lot of code smell).
The following change to the generated code is, as far as I can see,
the best solution:
final case class Nata(a: BigInt) extends nat {override def toString
= a.toString}
Maybe this could be added to the generated code? I know that this
simple suggestion might be very hard to implement in the code
generator but it would really really help to increase the usability of
the generated code.
Cornelius
___
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 Wed, 11 Sep 2013, C. Diekmann wrote: I just found an issue with the theories panel. The width is chosen by the longest theory name, no horizontal scrollbar is added. When there is an error at the end of my theory files with a long name, I do not get visual feedback about it. I will take another look a bit later. What is your OS platform and Swing look-and-feel? On Java/Swing this is the evil parameter that can change everything -- it determines much more than just look and feel. Makarius ___ 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 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). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Monad_Syntax
On Wed, 11 Sep 2013, Florian Haftmann wrote:
Do monadic people have a standard Unicode point to render that operator?
If yes, we could assign that to \bind and use it from STIX (or provide
a glyph in the IsabelleText font).
For LaTeX I once have been using
\newcommand{\isasymbind}{\isamath{\mathbin{\!\!\!\mkern-6.7mu=}}}
following a suggestion by Jasmin as far as I remember.
We have the latex macro already since Isabelle/a33ecf47f0a0 (haftmann
2010).
If we find some Unicode point for it, we could reduce the variance of
notation to 2 or even 1. Allocating Unicode slots is a sport of many
subcultures, e.g. people writing text in Klingon (they did not make it
into the official charts, yet).
Looking around in Deja Vu or STIX for a few minutes, I did not find
anything like \bind yet, but it might be still there hidden within
thousands of symbols.
Makarius
___
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 Thu, 12 Sep 2013, David Greenaway wrote: One of the changes that has occurred since Isabelle 2013 is that simpsets have been deprecated in favour of storing simplifier rules directly in the context. Deprecated is is not really the wording we would use in the Isabelle context. Sun/Oracle use that term for Java operations that are never changed, but Isabelle lives on continuous renovation for 25 years already. The NEWS file explains what will happen in the coming release with simpset vs. Proof.context -- the Simplifier was one of the last hold-outs of non-localized tools, so after long delays we are mostly through with it. Isabelle/jEdit has now this Documentation dockable to access documentation. Its tree view also includes NEWS to access the all-important NEWS file with the history user-relevant changes. It also has its own jEdit editor mode with Sidekick tree etc. (The NEWS file still needs some polishing before we start the actual release candidate cycle in a few weeks.) Makarius ___ 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 Thu, 12 Sep 2013, C. Diekmann wrote: x86_64 Using bulky 64bit version of Poly/ML That part does not affect Java/Swing, but you might want to avoid the bulky version. On Ubuntu the required packages are something like lib32gcc or lib32stdc++6 -- I usually install as many as are required to silence the dynamic linker. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle_12-Sep-2013
On Thu, 12 Sep 2013, Makarius wrote: People used to repository snapshots might notice a few differences to such a standalone application I should probably say that the main application entry point is the outermost executable Isabelle_12-Sep-2013, which is just a shell script on Linux, an .exe on Windows and .app bundle on Mac OS X. All of them may have different snags -- I have reworked them a lot. One needs to imagine genuine users trying to start Isabelle for the first time, not people who know already that one might open a command-line window and type isabelle jedit with the correct executable path. (Command-line is relatively rare these days.) Makarius ___ 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
What is your OS platform and Swing look-and-feel? On Java/Swing this is the evil parameter that can change everything -- it determines much more than just look and feel. Default installation Ubuntu 12.04.3 LTS x86_64 Using bulky 64bit version of Poly/ML Swing look feel: Nimbus (the default selection) ___ 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
Hi Larry, Am 12.09.2013 um 20:14 schrieb Lawrence Paulson l...@cam.ac.uk: Provers don't launch at all (according to process monitor) and no output, either in the new S/H panel or via the sledgehammer command. I'm using 9d8764624487 but I don't think the precise version matters, as I grabbed a new copy this morning and nothing's changed. Anybody else seen this? I'm using the slightly more recent 3fb81ab13ea3 (but as you pointed out, hardly anything has changed in between) and everything is OK here. Let's try to debug this systematically. 1. First, can you confirm that this total failure of Sledgehammer also occurs in the following example (which should be solved quasi instantly by several ATPs)? theory Scratch imports Main begin lemma hd [x] = x sledgehammer (hd.simps) 2. If step 1 works, please try sledgehammer [mepo] instead. 3. If step 2 works, please try sledgehammer without any options. 4. If step 3 works, try to construct a minimal self-contained example that doesn't work and send it to me. One of my suspicions is that you might have enabled MaSh and today's change to it might have broken things somehow. Another We'll definitely need to be more conservative in our changes getting closer to the release. Thanks for your help. Cheers, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Total failure of sledgehammer
Provers don't launch at all (according to process monitor) and no output, either in the new S/H panel or via the sledgehammer command. I'm using 9d8764624487 but I don't think the precise version matters, as I grabbed a new copy this morning and nothing's changed. Anybody else seen this? Larry ___ 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 all, first of all, thanks Makarius for taking care of the new release. Here are my first comments: After changing to Isabelle_10-Sep-2013, most of the theories could easily be adapted. However, 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? Here are the details of my machine: MacOS X 10.8.4, 2 x 2.8 Ghz Quad-Core Intel Xeon, 6 GB RAM I noticed a similar phenomenon on my laptop with the following setup: MacOS X 10.8.4, 2.2 Ghz Intel Core i7, 8 GB RAM Cheers, René IsaFoR: a2136da2b517 AFP: 5c7a1374860e ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Isabelle_12-Sep-2013
Here is another integration test: http://www4.in.tum.de/~wenzelm/test/Isabelle_12-Sep-2013/ I've changed the way how the main application wrappers (for Linux, Windows, Mac OS X) start up the JVM and provide classpath and options, after fighting many monsters in the Pits of Jarr (where the Java sources are hidden). The situation is so much clearer after reading the real source text, not just this javadoc bla bla. This means all Isabelle/jEdit dockables should now work, including the critial Console/Scala sub-plugin. People used to repository snapshots might notice a few differences to such a standalone application, although some of the differences could be actually remaining problems. E.g. it has an explicit identification as Isabelle_12-Sep-2013 and thus gets a fresh $ISABELLE_HOME_USER directory, which might make a difference in certain test applications, keymaps etc. Makarius ___ 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 13/09/13 04:17, Makarius wrote: The NEWS file explains what will happen in the coming release with simpset vs. Proof.context -- the Simplifier was one of the last hold-outs of non-localized tools, so after long delays we are mostly through with it. Sorry, I should have mentioned that I read the NEWS file; I understood that the simplifier now accepted a context instead of a simpset, and that addsimps operated on contexts instead of simpsets. My question was instead related to the best way to perform operations on long-lived simpsets which need to be mutated over time, now that there are no exposed APIs for manipulating them. Florian's reply was helpful in pointing out some code (the code generator) which also had this problem, and its solution to this which amounts to: (i) taking your old simpset; (ii) putting it into a dummy context; (iii) performing your addsimp/addcong/etc operation; (iv) extract the simpset out again. Cheers, David 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
Re: [isabelle-dev] Isabelle_12-Sep-2013
Hi Makarius,
Thanks for your hard work for putting this together.
Most things I tried seemed to work out of the box on my 64-bit Linux
system, including sledgehammer, nitpick, etc.
I understand this is an integration test, and not a general release
candidate, but nevertheless I will write about a few small issues
I hit while playing with it:
* While auto try, auto quickcheck and auto nitpick seemed
to work, I couldn't get auto sledgehammer to give me a response.
The lemma I tried was:
lemma length xs 0 ⟹ hd (rev xs) = last xs
which sledgehammer is easily able to solve in less than two seconds
on my machine.
* It would be nice if symbol completion worked in the new find
panel. Similarly, using the standard Isabelle font in the search box
probably makes sense.
* The new find panel doesn't report the number of matches; only
the number displayed. For example, searching True displays:
displaying 40 theorem(s)
in the panel, while find_theorems reports:
found 222 theorem(s) (40 displayed):
which is perhaps more informative.
* Key-bindings (or at least hooks for keybindings) would be helpful
for the new find panel and sledgehammer panels. isabelle-find and
isabelle-sledgehammer hooks exist, but don't place focus on the
search box nor start a sledgehammer run.
* The abbreviations described in the README panel for sub, sup
and bold do not appear to work.
* The new superscripts are confusing me. term T\^suba parses,
but T\^supa does not. I must confess I don't understand the top
NEWS entry describing what has changed.
Also, using a clean Isabelle install without local patches applied
reminded me of a number of longer standing issues:
* The default Error color and Running color colours are very
similar, making them hard to distinguish in the theories panel
(Is there an error in that theory, or is it just taking a long time
to process?). I personally modify my Running color to be
a pleasant blue.
* When opening a theory from the command line, it would be nice to
have an option to automatically open dependent theory files without
prompting. It is nice to type:
isabelle jedit -l SomeLongRunningHeap FileWithManyDeps.thy
go away for a coffee, and come back with everything ready to go.
Currently, you have to click yes after the heap has built before
Isabelle will start processing FileWithManyDeps.thy.
* The output panel has a habit of scrolling to the top each time
the current output is appended to. It would be nice to preserve the
user's position.
For example, trying to view the current progress of the command:
ML {*
map (fn x = (tracing (PolyML.makestring x);
OS.Process.sleep (seconds 0.1))) (1 upto 100)
*}
is difficult.
I am, of course, happy to submit patches for review for any (or all) of
these problems if there is any indication that such patches would be
appreciated.
Thanks again for all your hard work, and my apologies in advance if
I am raising issues that you are already aware of.
Cheers,
David
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
