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
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
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
On 24/06/13 21:20, Makarius wrote:
Last week, I actually intended to make a proper exposition about
Isabelle/ML futures in the implementation manual, but for now it
just points to ~~/src/Pure/Concurrent/future.ML with its slightly odd
Notes at the beginning. That needs to be turned into
Hi Makarius,
On 09/04/13 02:06, Makarius wrote:
Sorry, I did not mean to re-open this messy thread anytime soon, but
David Matthews had offered his help with forced breaks in Poly/ML in
privite mail. Since I did not want to waste his time as well, I've
looked through the situation in
On 05/04/13 09:32, Makarius wrote:
On Fri, 5 Apr 2013, David Greenaway wrote:
What practical things could such volunteers do that you would find
helpful?
So how about maintaining Proof General, seriously, no-nonse?
As somebody who isn't a Proof General user, nor an Emacs user, nor has
ever
Hi Makarius,
On 02/04/13 21:17, Makarius wrote:
On Tue, 2 Apr 2013, David Greenaway wrote:
I would appreciate it if an Isabelle expert could review that patch
and, if acceptable, apply it to mainline. (This can be easily done
with hg import patch-file).
before you send more patches, can
Hi Alexander,
Thanks for your helpful reply.
On 04/04/13 08:58, Alexander Krauss wrote:
Hi David,
On 04/03/2013 09:18 AM, David Greenaway wrote:
[...]
Does my 4 line patch violate the Isabelle style guidelines, or have
I missed something about the correct etiquette for submitting patches
# HG changeset patch
# User David Greenaway david.greena...@nicta.com.au
# Date 1364864695 -39600
# Node ID 27bd348e777a3ffa4a4bf5bb18faa0a8428e468f
# Parent d40aec502416a0eaa094e5aef1f317f7c4867852
Fix top-level printing of exception messages containing forced-line breaks.
Both Isabelle
Hi all,
I have noticed that in c ertain circumstances both Isabelle/jEdit and
Isabelle/ProofGeneral will render certain constructs with a large number
of spaces in them.
The problem can be seen with the following testcase:
definition test a b ≡ undefined
notation (output) test (test //
On 26/03/13 00:40, Makarius wrote:
On Mon, 25 Mar 2013, David Greenaway wrote:
[...]
The problem that this patch fixes is internal to the Isabelle sources,
and not directly related to how jEdit measures strings. As mentioned
above, Pretty uses FontMetrics.stringWidth to determine if text
.
# HG changeset patch
# User David Greenaway david.greena...@nicta.com.au
# Date 1363843205 -39600
# Node ID b1420574b7273225672a9f7e6a5b3e9c6c84b75d
# Parent e0c74b23d0a87547465aced2020de1998175662a
pretty: Ensure we are consistent in our use of space-widths versus character-widths.
The current
Hi all,
Attached is a patch series which attempts to improve the font rendering
in the Isabelle/jEdit output window. In particular, it attempts to
reduce the number of cases where text is inadvertently rendered off the
right-hand-side of the output window, requiring the user to scroll
across to
caused by this email or its attachments.
# HG changeset patch
# User David Greenaway david.greena...@nicta.com.au
# Date 1363843205 -39600
# Node ID 10e9fed2f208cbaf93fd351d260c26c82cedb931
# Parent b1420574b7273225672a9f7e6a5b3e9c6c84b75d
pretty: Use a more accurate method of measuring string lengths
privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
# HG changeset patch
# User David Greenaway david.greena...@nicta.com.au
# Date 1363843205 -39600
# Node ID e0c74b23d0a87547465aced2020de1998175662a
# Parent
On 22/03/13 02:13, Makarius wrote:
On Thu, 21 Mar 2013, David Greenaway wrote:
Attached is a patch series which attempts to improve the font rendering
in the Isabelle/jEdit output window. In particular, it attempts to
reduce the number of cases where text is inadvertently rendered off
On 08/03/13 23:46, Joachim Breitner wrote:
Sometimes, when I’m writing apply-script style proofs, I have wanted
a way to modify a proof method foo to “Try foo on the first goal. If
it solves the goal, good, if it does not solve it, fail”.
[...]
I wanted to see if I could implement such a
On 14/03/13 22:37, Makarius wrote:
Before we run again into a noisy thread that leads nowhere: the system
development process is run by the people doing the actual work. This
sounds like a trivial tautology, but is often forgotten.
What level of community involvement (i.e., external
On 10/03/13 07:03, Makarius wrote:
On Fri, 8 Mar 2013, Joachim Breitner wrote:
Sometimes, when I’m writing apply-script style proofs, I have wanted
a way to modify a proof method foo to “Try foo on the first goal. If
it solves the goal, good, if it does not solve it, fail”.
The Isar proof
On 21/01/13 23:08, Makarius wrote:
After inspecting the Isabelle source a little more, I have seen that
there is a jEdit configuration variable:
editor_tracing_messages
that allows the pause threshold to be adjusted. Setting this value to
a large number solves my first problem.
The
Hi all,
I have been locally testing out the current development snapshots of
Isabelle in anticipation of the Isabelle 2013 release. So far, most
things have been very smooth; thanks everyone for your hard work.
One minor problem I am hitting is the Tracing paused messages when
running proofs
21 matches
Mail list logo
