[isabelle-dev] Method parsing, YXML and term construction.

2010-02-09 Thread Thomas Sewell
to construct the term skeleton and appeal to the type resolver. Now I know how. BTW, should I have known this already? Is there some part of the documentation that I should have read, but have overlooked? Yours, Thomas. Makarius wrote: On Mon, 8 Feb 2010, Thomas Sewell wrote: Specifically, f

[isabelle-dev] Method parsing, YXML and term construction.

2010-02-08 Thread Thomas Sewell
Hello to isabelle-dev. Suppose some ML code I wrote has terms f, x and y. I'd like to be able to produce the function application f x y with the catch that f, x and y may all have type parameters that need to be adapted to each other. Is there any convenient facility for doing this in Isabelle

[isabelle-dev] Beta/Eta normalisation and net matching.

2010-08-03 Thread Thomas Sewell
Hello Isabelle developers. I was about to have another attempt at speeding up a tactic we implemented for L4.verified using net-matching. In reading Pure/net.ML I spotted the comment Requires operands to be beta-eta-normal. In rereading the existing biresolution_from_nets_tac code, however, I

[isabelle-dev] Safe approach to hypothesis substitution

2010-08-23 Thread Thomas Sewell
As previously discussed in the thread Safe for boolean equality, the current strategy for using equality hypotheses 'x = expr', in which substitution for x is done and then the hypothesis is discarded, is unsafe. The conclusion of that discussion was that the problem was annoying but fairly

Re: [isabelle-dev] Safe approach to hypothesis substitution

2010-08-23 Thread Thomas Sewell
as returned by Logic.strip_assums_hyp, which it gets right. Yours, Thomas. From: Alexander Krauss [kra...@in.tum.de] Sent: Monday, August 23, 2010 7:35 PM To: Thomas Sewell Cc: Isabelle Developers Mailing List Subject: Re: [isabelle-dev] Safe approach

Re: [isabelle-dev] Safe approach to hypothesis substitution

2010-08-24 Thread Thomas Sewell
It's interesting that my innocent thread on hypothesis substitution has been hijacked into a discussion about context-aware coding guidelines. I'm trying to steer clear of contexts - it would seem more elegant to me if there was a purely tactical solution to this problem. To answer Andreas'

Re: [isabelle-dev] Safe approach to hypothesis substitution

2010-08-25 Thread Thomas Sewell
Let's try to answer everyone again: Alex: I think I was wrong about the cases involving algebra. There may be something interesting going on. The prenormalisation phase calls clarify_tac, then full_atomize_tac, then some other stuff. With a Free variable x assumed to be even, the resulting

Re: [isabelle-dev] Safe approach to hypothesis substitution

2010-08-25 Thread Thomas Sewell
/10 02:49, Makarius wrote: On Wed, 25 Aug 2010, Thomas Sewell wrote: Finally, the change to inspect_pair is indeed just a bugfix. I don't this check is needed for the simplifier driven version of hyp_subst anyway, so the bug shouldn't often be seen. Often it is hard to tell what

[isabelle-dev] FW: Safe approach to hypothesis substitution

2010-09-01 Thread Thomas Sewell
necessary. I may do that tomorrow. Yours, Thomas. From: Lawrence Paulson [l...@cam.ac.uk] Sent: Tuesday, August 31, 2010 8:21 PM To: Thomas Sewell Cc: Isabelle Developers Mailing List Subject: Re: [isabelle-dev] Safe approach to hypothesis substitution Thanks

[isabelle-dev] Feature request

2010-12-07 Thread Thomas Sewell
Hello Isabelle developers. I was recently reminded of one of the things on my wish-list for Isabelle: a make -k mode in which the system continues for as long as possible and reports as many errors as possible, rather than halting after the first one. I think this would be generally useful to

[isabelle-dev] I'd like to better understand some operations from Local_Theory.

2011-04-07 Thread Thomas Sewell
Hello Isabelle developers. I'm doing an experiment in which I need to programmatically construct a locale. For simplicity I used the same operations that Michael Norrish was using in the l4.verified C code parser, Local_Theory.define and Local_Theory.notes. This led to some strange behaviour.

[isabelle-dev] Probable bug in let_simp simproc

2011-08-10 Thread Thomas Sewell
I spent a bit of yesterday trying to discover why the standard simpset was taking forever to simplify a large term I happen to have. The term is folded down in such a manner that unfolding Let_def will cause it to grow extremely large, which turns out to be what is happening. Deleting the

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-11 Thread Thomas Sewell
I'm strongly in favour of an explicit set type. I've been asked for advice by a number of novice Isabelle users and given the same recommendation: go make the development type-check under the old rules. Then the simplifier will start helping you rather than fighting you. I suppose there might

Re: [isabelle-dev] Probable bug in let_simp simproc

2011-08-12 Thread Thomas Sewell
keep deleting the simproc from my simpset and try to implement a mechanism for allowing these simplifications that's specific to my problem. Yours, Thomas. From: Makarius [makar...@sketis.net] Sent: Thursday, August 11, 2011 10:08 PM To: Thomas Sewell

[isabelle-dev] Using PolyML's memory consumption profiling on Isabelle

2011-10-13 Thread Thomas Sewell
Good day all. Just wanted to let the Isabelle developers know about the latest feature David Matthews has added to PolyML, and to let you all know how useful it is. The feature allows profiling of objects after garbage collection. When code is compiled with PolyML.compiler.allocationProfiling

[isabelle-dev] More context on Isabelle memory consumption

2011-10-17 Thread Thomas Sewell
My email about PolyML and memory usage has generated some discussion, perhaps I should give some more context. The L4.verified project has been stuck at Isabelle-2009-2 for years. Our proofs seem to be compatible with newer Isabelle versions, but we're running out of (virtual) memory. We've

Re: [isabelle-dev] Towards the next release

2012-03-04 Thread Thomas Sewell
We have a somewhat useful tool for expanding word equalities/inequalities bitwise, based on a part of some work Sascha and I did back in 2010. I've been meaning to push it up to the distribution for years, this will probably be a good time. The main reason I'm telling you this is that I'm now

Re: [isabelle-dev] record: fold_congs/unfold_congs

2012-04-17 Thread Thomas Sewell
The fold_congs theorems are not an accident. They are used as congruence rules to perform conversions such as rec (| x := rec x + 1 |) = x_update (%x. x + 1) rec. Note this removes the duplicated mention of the name rec. The name fold_congs is somewhat arbitrary, since either direction above

Re: [isabelle-dev] simplifier and subgoaler not transitive

2012-05-22 Thread Thomas Sewell
Question: it looks to me like (atom v # (x, y)) = (atom v # x atom v # y) It also looks like what you're trying to do is allow the system to reason with the above equality without actually giving it that equality. It looks like you've provided the equality in one direction as a rewrite rule

Re: [isabelle-dev] simplifier trace (and jedit)

2012-05-22 Thread Thomas Sewell
The _2 v.s. (2) thing is just silly. It's in find_theorems output too. It's just the way theorems get their names - probably one of these decisions made years ago and not compatible with Makarius' decisions about how to fetch theorems in Isar. Adding context information to every reduction

Re: [isabelle-dev] Problem with let-simproc

2013-02-06 Thread Thomas Sewell
I'd forgotten I'd ever reported this to you. My problems with let_simproc run a little deeper anyway, and I've moved to a different approach in the meanwhile. Sorry if I've left you labouring on my behalf. Yours, Thomas. On 07/02/13 02:38, Johannes Hölzl wrote: Am Mittwoch, den

Re: [isabelle-dev] Fix top-level printing of exception messages containing forced-line breaks

2013-04-05 Thread Thomas Sewell
2013, Thomas Sewell wrote: David's investigation explains a problem we had a few years ago where some custom tactics of mine were killing my colleagues' ProofGeneral sessions when they encountered errors. The workaround at the time was to remove all potentially useful debugging information (terms

Re: [isabelle-dev] Alternative thoughts about certifying and reading input parameters to Isabelle command functions

2013-04-28 Thread Thomas Sewell
Hey Florian. Just my two cents, but does uncurrying buy you anything here? The function doing the actual work, do_foo in your example, has not been given a name and type before. So you're free to have it accept a tuple: fun do_foo (x_1, x_2, ... x_n) = ... And now val foo_cmd =

[isabelle-dev] Can I request an improvement to the error for Duplicate session

2013-12-22 Thread Thomas Sewell
Hey Isabelle devs. I've just spent a few minutes helping a teammate who was getting Duplicate session errors out of isabelle build/jedit. To reproduce this error, take a version of isabelle at, say, ~tsewell/work/isabelle, and attempt isabelle jedit -d . -d ~tsewell/work/isabelle.

Re: [isabelle-dev] Safe approach to hypothesis substitution mark II

2014-01-15 Thread Thomas Sewell
the confusion, Thomas. On 16/01/14 02:00, Makarius wrote: On Tue, 14 Jan 2014, Thomas Sewell wrote: This is also a patch against Isabelle2013-1. Is that just a typo, or are you still using that failed release? The current one is Isabelle2013-2, and it does not introduce any incompatibilities over

Re: [isabelle-dev] Default simprules for division in fields

2014-04-06 Thread Thomas Sewell
This makes me realise that I may have been misunderstanding field_simps. I've been using it as a replacement after ring_simps disappeared a while ago. It always struck me as odd, since I'm nearly always in a word type, which is a ring but not a field. Is it just a coincidence that field_simps

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-28 Thread Thomas Sewell
Back to the actual technical questions. What are the main performance bottle-necks here? Printing of intermediate goal states? Or applying intermediate steps repeatedly? I suspect that the problem is not that the printing or the intermediate calculations are taking too long. It's that

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-04 Thread Thomas Sewell
On 03/05/14 00:05, Makarius wrote: On Tue, 29 Apr 2014, Thomas Sewell wrote: I tried an adjustment a while ago in which I had the goal state print incrementally. Even if some of the subgoals took a while to print, you'd see the line with goal (12 subgoals) immediately, and then the subgoals

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-08 Thread Thomas Sewell
Thanks Makarius. A few of us at NICTA have ported this change to our various versions of Isabelle and begun playing with it. It seems to improve the situation sometimes, though we haven't yet got a feel for when in particular it helps. In fact, we haven't really understood what the change

Re: [isabelle-dev] Notes on datatype_new list

2014-05-26 Thread Thomas Sewell
I have no particular stake in this issue, but I would think there was an option (c) which is to do the *opposite* of what Jasmin said about bringing the additional constant names etc as close as possible to wherever they fit: datatype_new 'a list = Nil ([]) | Cons 'a 'a list (infixr #

Re: [isabelle-dev] Towards the Isabelle2014 release

2014-06-03 Thread Thomas Sewell
I had hoped to have the change I was making to hypothesis-substitution ready for the coming release. I've got it working for all of HOL and the library, and begun looking at the AFP and at the l4.verified proofs. The HOL+library changes were easy enough, but the l4.verified changes are

Re: [isabelle-dev] Towards the Isabelle2014 release

2014-06-04 Thread Thomas Sewell
. Backward compatibility will be necessary for users, even if not for us. Larry On 4 Jun 2014, at 06:27, Thomas Sewell thomas.sew...@nicta.com.au wrote: I had hoped to have the change I was making to hypothesis-substitution ready for the coming release. I've got it working for all of HOL

[isabelle-dev] Has anyone ever run out of memory trying to *start* to build the AFP?

2014-06-05 Thread Thomas Sewell
While fixing theories in the AFP, I arrived in a strange situation where isabelle build -D thys would no longer find and check the remaining unbuilt theories. Instead, I got a java OutOfMemory exception on the java heap. This is before anything starts building - I take it java has run out of

Re: [isabelle-dev] Towards the Isabelle2014 release

2014-06-30 Thread Thomas Sewell
The changeset has landed in the sense that I sent Gerwin a bundle containing: changeset: 6bf63b1f41f0 tag: tip user:Thomas Sewell thomas.sew...@nicta.com.au date:Wed Jun 11 14:24:23 2014 +1000 summary: Hypsubst preserves equality hypotheses He probably pushed

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-08 Thread Thomas Sewell
I've had a quick scan over the NICTA repositories. It doesn't look like there are any live original uses of recdef. There are recdefs in a copy of Simpl-AFP, and in some backups of historical papers. Short summary, NICTA doesn't have any stakes in recdef. Cheers, Thomas. On 08/06/15 06:13,

Re: [isabelle-dev] next release

2016-01-14 Thread Thomas Sewell
I have two items of interest for the coming release. There is some interest here at Data61 (NICTA that was) in having a localised record package in Isabelle-2016. I've done the initial implementation and got the parts of the package I understand working within locales etc, but something goes

Re: [isabelle-dev] next release

2016-01-17 Thread Thomas Sewell
OK, I'll respond to these points in-line. A discussion without sources to look at is difficult. OK, I attach my working version. Colleagues of mine were told off recently for producing patches without the relevant authority, so these days I begin these discussions in abstract. Feel free to

Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH

2018-11-30 Thread Thomas Sewell
I'd just like to confirm that other users have seen this issue. Colleagues of mine have tried to pre-build heaps on a build server and share them with other users. It could have saved CPU-hours, and in some cases, hours of humans waiting around, but it never worked. My understanding is that

Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH

2018-12-04 Thread Thomas Sewell
everything can be set up so that the right Path.smart_implode events happen, and perhaps whether it's easy to set up a check that this happens. Cheers, Thomas. From: Makarius Sent: Friday, November 30, 2018 10:18:12 PM To: Thomas Sewell; Jonathon Fernyhough;