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
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
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
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
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'
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
/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
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
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
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.
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
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
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
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
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
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
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
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
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
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
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 =
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.
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
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
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
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
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
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 #
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
.
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
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
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
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,
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
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
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
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;
"Unable to increase stack" is one of the various messages that tells you that
PolyML has run out of resources. It doesn't really tell you what the problem is
though. It might be an actual problem or a temporary problem caused by a
machine being overloaded.
Cheers,
Thomas.
On 2019-03-12
38 matches
Mail list logo
