Re: [isabelle-dev] Towards Isabelle2011 release
I get a (minor) error when running this version (MacOS 10.6, double-clicking on isa2011-test2.app icon): if I have theory file being processed, and I quit Isabelle/Aquamacs, I get a dialogue box telling me that I have active processes, and do I want to kill them. If I say yes, then I get a error window saying something like: 2011-01-25 11:42:54.894 Emacs[7555:623] ns_raise_fr 2011-01-25 11:42:58.407 Emacs[7555:623] notification 2011-01-25 11:43:01.187 Emacs[7555:623] ns_raise_fr 2011-01-25 11:43:02.788 Emacs[7555:623] notification 2011-01-25 11:43:31.366 Emacs[7555:623] notification Seems to be coming from the Isabelle application wrapper: Scenario 2: I start-up by Aquamacs directly - not via the Isabelle icon, using my emacs settings which starts PG using the load-file command, then when I quit (by command-Q). In this case, I don't get a dialogue-box telling me about the active processes; instead, I get the typical emacs mini-buffer message. When I say yes there, it quits without any strange error messages. best, lucas On 24/01/2011 15:12, Makarius wrote: Here is another test release: http://www4.in.tum.de/~wenzelm/test/isa2011-test2/ while the main Isabelle code base seems to be in good shape, there are various issues with the overall integration of external tools on the different platforms that we support officially. Some of them have been resolved. Some notable changes: * contrib/spass-3.7: make it actually work on x86-darwin (Leopard) (avoiding really weird crashes and strange error messages with Sledgehammer) * contrib/cvc3-2.2: make it actually work on darwin without Mac Ports * contrib/z3: make it actually work on x86_64-linux; still not working on Windows/Cygwin (?) unavailable on Mac OS X (!) * Cygwin: Back to old ProofGeneral-3.7.1.1 with ancient XEmacs, because PG 4.x with GNU Emacs 23 is very slow here. * ProofGeneral-4.1pre110112: deleted .elc files on Linux to improve compatibility with GNU Emacs 23.1.x instead of 23.2.1 In the Mac OS X app/dmg I have also exchanged GNU Emacs 23.2.x (no nonsense version) with Aquamacs 2.1, although it looks again like this is the choice between Scylla and Charybdis. It is also unclear when exactly PG 4.1-final will be released this week. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proof General 4.1 on Mac OS X
I've had what I consider to be success with a very similar setup... I'm using: Isabelle (isa2011-test1: January 2011, which has Proof General Version 4.1pre110112) but with Aquamacs Distribution 2.1 on MacOS 10.6 I'm loading Aquamacs from the dock, so I don't get background noise. Menus respond with usual swiftness and long arrows/unicode tokens etc look good. Setup .emacs config: (custom-set-variables '(isa-isabelle-command /Applications/isa2011-test1.app/Isabelle /bin/isabelle)) (load-file /Applications/isa2011-test1.app/Isabelle/contrib/ProofGeneral/generic/proof-site.el) Light blue background looks just right on my screen/default setup. I wasn't able to reproduce the syntax-highlighting bug. best, lucas On 23/01/2011 18:57, Clemens Ballarin wrote: I repeated my recent try of ProofGeneral on my Mac with ProofGeneral-4.1pre110118. If used with Aquamacs I observe these issues: - Menus respond slowly ( 1 second) when invoked for the first time. This is fine if Aquamacs is used without ProofGeneral. - Noise on the background shell. - Fontification fails in one situation. See attached image. - Long arrows are displayed as boxes (I probably don't have a suitable font for this.) - Light blue background of processed portion of the buffer is hard to see. Unicode symbols that are available are displayed in the right size. This is much better than with my previous setup with PG 3.7.1.1 and Carbonemacs. If the slow menus can be fixed this might be a suitable companion for Isabelle 2011. Clemens PS. I did use this configuration: - Aquamacs 2.1 distribution - ProofGeneral-4.1pre110118 - MacOS X 10.5.8 Quoting Makarius makar...@sketis.net: On Fri, 21 Jan 2011, Mamoun FILALI-AMINE wrote: a remark: previously, there was aquamacs instead of emacs? I find auqamacs more convenient than emacs. In recent Isabelle releases the default combination was Proof General 3.7.1.1 with Aquamacs based on Emacs 22. That turned out as half-decent, half-working -- after many weeks of desparate search in the Mac OS X ecosphere. In Isabelle2011 the default Proof General is going to be 4.1, which has quite different Emacs requirements, and generally quite different behaviour concerning special symbols etc. So far, I did not spend much time to try all possible combinations of Emacsen with PG 4.1. According to ProofGeneral/COMPATIBILITY, plain GNU Emacs 23.2 is recommended (aka the no nonsense version). Aquamacs 2.1 is also based on that code base, so it could in principle work as well, despite fancy additions. When I've tried the slightly older Aquamacs 2.0 some months ago, it turned out much slower than plain GNU Emacs 23 -- see also http://proofgeneral.inf.ed.ac.uk/trac/ticket/324 -- but that might be obsolete in several respects. I hope to get more concrete feedback from Mac users. So far I've mainly found out that most people are stuck with very old versions of Proof General, sometimes even in combination with ancient XEmacs. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Exception. fun oddity in Isabelle 2009-2
On 06/12/2010 15:15, Makarius wrote: On Sun, 5 Dec 2010, Lucas Dixon wrote: While playing around with a robotic horror that throw strange monsters at the function package, I came across this rather strange error... My guess is that some accidental infinite loop makes something bad happen at a low level... but I've ever seen the Exception. things before, so I'm not too sure what to do next. Moreover, (and importantly for me) when I'm calling this from ML, I'm not sure how to catch the resulting error, it seems to be skipping past my attempts to handle it. Any thoughts? In Isabelle2009-2, the failure that is printed as Exception means that some of the futures to do proofs in the background has somehow been canceled, e.g. by running out of resources. thanks! that was my suspicion. After Isabelle2009-2 such indirect interrupts are propagated to the surface more clearly. You cannot really handle such low-level system failures, though. ... at the moment I need Isabelle2009-2, too many dependencies to quickly unravel... is there an easy way to disable multi-threading/futures so that I can see what the real ML error is? a quick pointer to what to hack in the ML-Systems dir? :) At the moment I need reliability/simplicity over speed; so will probably need to do this anyway... cheers, lucas -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Exception. fun oddity in Isabelle 2009-2
Hi, While playing around with a robotic horror that throw strange monsters at the function package, I came across this rather strange error... *** start of theory *** theory fun_def_oddity imports Main begin datatype Ta = C_2 nat nat | C_1 Ta nat fun f where f (C_2 a b) c = c | f (C_1 a b) c = f a (f a (f a (f (C_1 a b) b))) (* ... after a long time... constants f :: Ta ⇒ nat ⇒ nat Exception. At command fun. *) end; *** end of theory *** Now I know this isn't a good looking function, but the error message seems somewhat odd. My guess is that some accidental infinite loop makes something bad happen at a low level... but I've ever seen the Exception. things before, so I'm not too sure what to do next. Moreover, (and importantly for me) when I'm calling this from ML, I'm not sure how to catch the resulting error, it seems to be skipping past my attempts to handle it. Any thoughts? cheers, lucas -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] copying contexts
Hello, I'm wondering what the right way to copy contexts is. I remember there was some references lingering in theories, mostly as unique identifies if I remember correctly, but it meant that copying needed to be an explicit function. Is this the right way to copy a context: Context.map_theory Context.copy_thy and so copying a proof context would be: Context.proof_map (Context.map_theory Context.copy_thy) ? The reason I want to do this is that when proof planning proves new theorems it creates some meta-data which gets stored in the context. I want to be able to make a copy the context before I modify any such data so that I can compare alternatives and do fair tests. I was previously using my own generic context, but would like to cut down code duplication. cheers, lucas -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
[isabelle-dev] Isabelle/HOL axiom ext is redundant
I was really wondering what the principle was that makes -- and ALL fail (or be inappropriately convoluted) than using the meta-level connectives: is there a small example that illustrates it? My own understanding was that the meta-level of Isabelle, and the use of it by Isar, facilitated the genericity natural deduction-style reasoning. Generic proof tools can be written that work across logics. Makarius, if I understood correctly, was saying that these meta-level logical mechanisms have a utility even when just within one logic, but I didn't understand what this would be, except perhaps distinguishing between ND syntax and other logical syntax (which is my interpretation of Michael's reply). best, lucas Lawrence Paulson wrote: This sort of discussion is analogous to suggesting that we get rid of and/or/not/implies and write all formulas using the Scheffer stroke (NAND), or that Gentzen's sequent calculus should be replaced by the much simpler Hilbert system. It can be done, but who would want to do it? Larry On 12 Nov 2009, at 20:50, Lucas Dixon wrote: this is interesting to me: I don't understand why you couldn't just use the -- and ALL of HOL to do exactly what == and !! are doing? Isn't that what SPL by Zammit did? The dependencies (in Isabelle, stored in hyps) can all be recorded outside the logic (as they are in SPL). If done correctly, like Isar, the final theorems can be re-constructed easily enough from the recorded structure of the proof text... or so it seems to me. :) -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
[isabelle-dev] Isabelle/HOL axiom ext is redundant
Makarius wrote: Isar depends a lot on Larry's rule calculus !! == and in fact makes it really shine. On the other hand, less of this is visible in the text, because native structured proof elements take over -- yet another layer on top of all that. Thus Isar is a bit like a rich language like ML, where raw lambda abstractions are relatively rare, but notbody would think of removing the lambda. Plain old HOL will have a hard time imitating Isar without Pure ND rules. One would either have to reinvent it, or rethink the whole thing from the ground up. Again: look at example of Isar calculations, to see where the rule framework of Pure comes into place. this is interesting to me: I don't understand why you couldn't just use the -- and ALL of HOL to do exactly what == and !! are doing? Isn't that what SPL by Zammit did? The dependencies (in Isabelle, stored in hyps) can all be recorded outside the logic (as they are in SPL). If done correctly, like Isar, the final theorems can be re-constructed easily enough from the recorded structure of the proof text... or so it seems to me. :) cheers, lucas -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
[isabelle-dev] counter example checking from ML
Hi, a little more progress in understanding the issue...
I've made a little test program that highlights the change in behaviour
that we noticed.
The point is to stress test counter example finding and see at what
point a false-conjecture slips past. In particular, when performing 5
iterations, this code measures the average number of times it takes to
before the false conjecture is not spotted by the test_term function.
So, the bigger the number that comes out, the better test_term is doing
(at generating examples that show the conjecture to be false).
Here's the code:
ML {*
(* how many times until this false conjecture slips past codegen *)
fun count_until_missed i =
(case Codegen.test_term @{context} @{term %a (b :: nat). a + b = a
* b} 5
of NONE = i
| SOME _ = count_until_missed (i + 1));
(* average of the function's results, preformed n times *)
fun avg f n =
let fun sumf 0 a = a
| sumf k a = sumf (k - 1) (a + f())
in (Real.fromInt (sumf n 0)) / (Real.fromInt n) end;
(* avg number of times until this false conjecture slips past codegen *)
val count_avg = avg (fn () = count_until_missed 1) 50;
*}
I don't have enough internet to download and test on 2008; but there has
been a significant difference even between Isabelle 2009 and a recent
dev snapshot (32589:9353798ce61f):
On Isabelle dev snapshot (32589:9353798ce61f)
val count_avg = 14.11 : real
On Isabelle 2009
val count_avg = 32.14 : real
(takes some time... good news: you've speeded up codegen a lot! In fact,
this difference might even be compensating for the bad behaviour in
iterations :)
The deterministic version should, I think, not terminate for this
problem and many like it. But I haven't tried it yet.
These are of course averages and change a bit, but having repeated the
experiment many times, I think those numbers are aprox right. At least
they give a rough benchmarking mechanism.
This is a case where your random sampling looks to be doing the wrong
thing - with respect to the spec I've made up in my head ;-). Since (a
= 0 b = 0 | a = 2 b = 2) = (a + b = a * b), 5 iterations is going
to have to be picking the same case at least three times; a quick hack
would be to cache the examples you've already looked at. But even better
would be for your random example chooser to automatically pick the next
unpicked example, rather than repeat known results. This is probably
more of a problem for conjectures with a small number of variables, but
would still be generally a good idea.
best,
lucas
Florian Haftmann wrote:
Hi Lucas,
indeed the whole quickcheck matter has grown into a complex story.
First, we currently (e.g. following development in the hg repository)
have a kind of fork: there is the old quickcheck, residing in
Pure/codegen.ML, and the new one in HOL/Quickcheck.thy; the most
prominent difference between both is that the new one tries to
internalize as much as possible into the logic, which allows to use type
classes and avoids tinkering too much with glueing raw ML snippet
strings together.
Concerning determinism, the old quickcheck is inherently randomized.
The new one uses an open state monad which passes a random seed around
explicitly and can thus be also used to enforce determinism. If you
want to use this, be aware of the pitfalls which arise when using
unofficial intermediate stages of development rather than official releases!
The key for understanding is in HOL/Tools/quickcheck_generators.ML,
function mk_generator_expr (export it on demand and try something like
Quickcheck_Generators.mk_generator_expr @{theory} @{term
\lambdan::nat. n ~= n^2} [...@{typ nat}]); for further background
knowledge on this machinery, refer to ?4.4 in
http://www4.in.tum.de/~haftmann/phd.shtml. Don't hesitate to ask
further questions.
Hope this helps,
Florian
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
[isabelle-dev] [isabelle] counter example checking from ML
Hi following this up a bit,
I've noticed that, for the examples I've been looking at, the
counter-example finder is now much less successful than it used to be. I
need to crank up the iterations a lot.
I was previously able to use it with an input of up to size 5, with 5
iterations on over 40,000 cases without any false conjectures slipping
through. I thought this was great, but perhaps it was a feature of the
domain I was looking at (equations over datatypes and simple recursive
functions on them).
So, I'm now wondering if there is there a way to provide a deterministic
instance generator rather than the random one currently being used (is
this what happened before?) My feeling is that the first few cases for
each variable is what I'm after.
Also, to make programatic changes to the configuration of tools, we need
to have the contextual data available, so if its OK, I'll export that
also in the signature.
best,
lucas
Florian Haftmann wrote:
Hi Lucas,
note that the convention on the Codegen.test_term interface has changed:
ML {* Codegen.test_term @{context} @{term %n. n = Suc n} 2 *}
The proposition is now given as an abstraction containing *no* free
variables.
Hope this helps
Florian
Lucas Dixon schrieb:
Hello,
I have questions about using isabelle quickcheck/code generation.
I used to quite happily use it for various things but it seems that the
input is now stricter than it used to be (in 2008) - extra dependencies
between the input term and context - and I've not yet been able to
figure it out.
(Using Isabelle 32575:bf6c78d9f94c)
I'm trying to use
Codegen.test_term : Proof.context - term - int - term list option
(is this the best ML function to be using? do tell me of a better higher
level one)
Trying to do what I used to do in ML...
ML{*
val _ = (Codegen.test_term
@{context}
@{term (b :: int) + a = b});
*}
;
Produces the error:
*** Error (line 19):
*** Value or constructor (b) has not been declared
*** Error (line 19):
*** Value or constructor (a) has not been declared
*** Error (line 19):
*** Value or constructor (b) has not been declared
*** Exception- ERROR of Static Errors raised
*** val ctxt2 = context : Context.proof
*** Exception- TOPLEVEL_ERROR raised
*** At command ML (line 11 of
/afs/inf.ed.ac.uk/user/l/ldixon/Scratch.thy).
My first guess was that all terms are now implicitly dependent on the
context they live in, so perhaps I need to add the free variables to the
context, - the types should already be there. The quick undisciplined
way, I think, is:
ML{*
val (_,ctxt2) = @{context} | Variable.add_fixes [b, a];
val _ = (Codegen.test_term ctxt2 @{term (b :: int) + a = b});
*}
;
I can do some term manipulation and properly pull out the names of the
frees from the term - but I would expect the above to work... but it
also gives the same error.
This gives rise to further questions:
- how to I inspect the context? (I remember this from the Isabelle dev
workshop, but couldn't find it in the online example theories)
- what's the right way to quickly make the context that would get from a
statement like lemma ...? i.e. the context of a term, automatically
putting in the types and frees? (my first guess was to use
Variable.focus - but that seems to ignore free vars and types)
- how can I use quickcheck (or nitpick) from the ML level? and I would
love this to be in the Isabelle cookbook (shall I write an entry, once I
find out how to use it?)
- What is the hidden implicit dependency between the term given to
Codegen.text_term, and the context?
thanks,
lucas
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
[isabelle-dev] Interrupt exception
Florian Haftmann wrote: Hi Lucas, apply (unfold Product_Type.pair_collapse[symmetric, of al]) The equation Product_Type.pair_collapse[symmetric, of al] can be unfolded forever, so the method invocation does not terminate, leading to an unspecified behaviour of the system! As a quick replacement, consider apply (subst ...) In the end it is better to write a structured Isar proof text which allows fine granular control over delicate steps. Thanks, I know this - I wrote subst :) The point was just that unfold should probably be giving an error message of some more readable sort. best, lucas -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
[isabelle-dev] Interrupt exception
Makarius wrote: On Wed, 15 Jul 2009, Lucas Dixon wrote: apply (unfold Product_Type.pair_collapse[symmetric, of al]) The equation Product_Type.pair_collapse[symmetric, of al] can be unfolded forever, so the method invocation does not terminate, leading to an unspecified behaviour of the system! The point was just that unfold should probably be giving an error message of some more readable sort. The interrupt exception is probably produced by the Poly/ML runtime system when it runs out of resources. The behaviour might have changed a bit in recent internal versions. Which one did you use? Yes, I'm sure you are right; I'm using Isabelle (1d4d0b305f16: date: Fri Jul 10 09:24:50 2009 +0200), and PolyML (svn 801, 2009-07-12) The problem came up when I was writing a tactic and I wanted to unfold all occurences within a goal but not do this recursively - I wanted any introduced occurrences to be untouched. I was simulating this within a tactic script as an experiment. But perhaps the idea of unfold all current occurrences (modulo critical pairs) would be a sensible semantics for unfold? It seems like a sensible semantics for something, call it unfold or something else :) best, lucas -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
[isabelle-dev] Isabelle NEWS as a blog ?
What do people think of having the Isabelle NEWS file as a blog? I suspect people might be better at using it (both reading and contributing) than the current NEWS file... best, lucas -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
