On Fri, 30 Nov 2012, Lawrence Paulson wrote:
Doubtless some student enjoys tinkering with video formats and could
make a five-minute video that simply answers the question, how do I get
started? What are the main interaction modes? And maybe touches on some
of the more advanced features.
I h
I don't think you need to do this personally. Doubtless some student enjoys
tinkering with video formats and could make a five-minute video that simply
answers the question, how do I get started? What are the main interaction
modes? And maybe touches on some of the more advanced features.
Larry
On Fri, 30 Nov 2012, Lawrence Paulson wrote:
I think we should still include hints on how to use PG but without the
same level of support as in the past. Obviously, if a clamour arose for
a bundled PG version, we could deal with that at the time.
Whatever happens, it needs to be clear reasona
On Fri, 30 Nov 2012, Lawrence Paulson wrote:
I imagine that some sort of short tutorial video or slideshow (analogous
to the one I made a number of years ago) might be better than any amount
of written documentation.
I've recently started experimenting with video recording, which works
quite
It actually makes sense to put every effort into making the jEdit version as
good as possible, especially for beginners. It might be worth investigating
what issues cause them the most problems; I imagine that some sort of short
tutorial video or slideshow (analogous to the one I made a number o
On Thu, 29 Nov 2012, Lawrence Paulson wrote:
Will it run without compiled files? And will it run efficiently enough?
Certainly I've always compiled my copy.
On 21 Nov 2012, at 10:35, Makarius wrote:
* A version of Proof General as Isabelle component, like
http://isabelle.in.tum.de/compo
Will it run without compiled files? And will it run efficiently enough?
Certainly I've always compiled my copy.
Larry
On 21 Nov 2012, at 10:35, Makarius wrote:
> * A version of Proof General as Isabelle component, like
>http://isabelle.in.tum.de/components/ProofGeneral-4.1.tar.gz
>(it
On Tue, 20 Nov 2012, Lawrence Paulson wrote:
I am using version 4.1. I was having problems compiling 4.2, and it
doesn't seem to run in interpreted mode. I'm not sure what is changed
between 4.1 and 4.2 anyway.
I am unsure myself, but there was quite a lot of activity on the Coq side
on the
I am using version 4.1. I was having problems compiling 4.2, and it doesn't
seem to run in interpreted mode. I'm not sure what is changed between 4.1 and
4.2 anyway.
For the Emacs client, definitely Aquamacs. The other Emacs port is terrible, in
particular because it doesn't behave at all like
Dear all,
exactly 6 months after the last release, we have to start thinking
seriously about the next one. This involves consolidation of what was
added in the past few months, or before the last release and did not get
consolidated properly (like nested contexts on my side).
As far as I ca
On 02/05/2012, at 11:11 PM, Makarius wrote:
> On Tue, 17 Apr 2012, Gerwin Klein wrote:
>
>> There is a third small thing that I will discuss separately with Florian:
>> there is a bug in the code generator setup in Isabelle2011-1 somewhere in
>> generating narrowing lemmas. It is triggered for
On Tue, 17 Apr 2012, Gerwin Klein wrote:
There is a third small thing that I will discuss separately with
Florian: there is a bug in the code generator setup in Isabelle2011-1
somewhere in generating narrowing lemmas. It is triggered for records
with more than ~530 fields where it constructs a
On 19/04/2012, at 4:26 AM, Florian Haftmann wrote:
> I think it is very important to differentiate here into more detail.
> There is not »the« code generator setup but a layered one:
> a) Registering a record, its projections and quality on the record as an
> executable program fragment
> b) Provid
On Thu, 19 Apr 2012, Gerwin Klein wrote:
Btw, it's easy to reproduce: just make a theory file based on HOL
(Main.thy) that defines a record with 600 fields. Run it in
Isabelle-2009-1 and the current version for comparison.
We also have a semi-active src/HOL/Record_Benchmark for quite some tim
On Thu, 19 Apr 2012, Gerwin Klein wrote:
What happens in b) is much more ambitious, and if this is really a
bottleneck, an option like »record_quickcheck« could do the job.
But I think before to settle here it is important to have more detailed
benchmarks about records which separates figures
On 04/18/2012 08:26 PM, Florian Haftmann wrote:
Hi all,
- I would like to add a size limit to records beyond which no code generator setup
is performed. The main reason is that on sizes> 200 fields or so, the setup
does not make any sense, but consumes very large amounts of memory (and time)
On 19/04/2012, at 4:26 AM, Florian Haftmann wrote:
> Hi all,
>
>> - I would like to add a size limit to records beyond which no code generator
>> setup is performed. The main reason is that on sizes > 200 fields or so, the
>> setup does not make any sense, but consumes very large amounts of me
Hi all,
> - I would like to add a size limit to records beyond which no code generator
> setup is performed. The main reason is that on sizes > 200 fields or so, the
> setup does not make any sense, but consumes very large amounts of memory (and
> time). Switching it off gets rid of almost all
Hi all,
> The overloading rules are quite tricky. I don't understand why the first
> instantiation requires a definition of sup_hf (including the type in the
> constant name), while the second one simply requires a definition of minus.
> Perhaps because there is an explicit type in the first in
On Wed, 18 Apr 2012, Gerwin Klein wrote:
If 3) means "configuration option" in the sense of Config.T, here is
the canonical 1-liner to make one for a package:
val split_limit = Attrib.setup_config_int @{binding linarith_split_limit} (K
9);
Yes, that's what I meant. It's easy to set up, but
On 18/04/2012, at 12:29 AM, Makarius wrote:
> On Tue, 17 Apr 2012, Gerwin Klein wrote:
>
>> - I would like to add a size limit to records beyond which no code generator
>> setup is performed. The main reason is that on sizes > 200 fields or so, the
>> setup does not make any sense, but consumes
On Tue, 17 Apr 2012, Gerwin Klein wrote:
- I would like to add a size limit to records beyond which no code
generator setup is performed. The main reason is that on sizes > 200
fields or so, the setup does not make any sense, but consumes very large
amounts of memory (and time). Switching it o
On 12/04/2012, at 7:02 PM, Makarius wrote:
> we need to get to a more concrete release schedule. Presently I would like
> to aim for late May, which means we need to start consolidating and
> converging about now.
>
> Are there any further big things in the pipeline?
There are two small thing
Am 12/04/2012 14:06, schrieb Lawrence Paulson:
> There is something I'd like to mention, not a big deal, but worth considering.
>
> I've been doing some proofs lately after a long gap, making myself a
> combination of a novice and expert. And I've got confused by things that
> would probably con
On Fri, 13 Apr 2012, Lukas Bulwahn wrote:
Since (2) is nothing specifically exciting by JUNG either -- it seems
to be based on plain Java Graphics2D stuff -- I had recommended to
abandon JUNG altogether. Did anything happen here in the meantime?
We have discussed internally in more detail how
On 04/12/2012 08:32 PM, Makarius wrote:
On Thu, 12 Apr 2012, Lukas Bulwahn wrote:
We still have the locale browser in the pipeline. Do you have
objections to integrate the tool you have reviewed two months ago?
Our private discussion yielded further source code improvements,
however the tool
On Thu, 12 Apr 2012, Lukas Bulwahn wrote:
We still have the locale browser in the pipeline. Do you have objections
to integrate the tool you have reviewed two months ago? Our private
discussion yielded further source code improvements, however the tool is
already in a fully functional state, a
There is something I'd like to mention, not a big deal, but worth considering.
I've been doing some proofs lately after a long gap, making myself a
combination of a novice and expert. And I've got confused by things that would
probably confuse true novices even more.
Here are two instantiations
On 04/12/2012 11:02 AM, Makarius wrote:
Dear all,
we need to get to a more concrete release schedule. Presently I would
like to aim for late May, which means we need to start consolidating
and converging about now.
Are there any further big things in the pipeline?
We still have the locale
Dear all,
we need to get to a more concrete release schedule. Presently I would
like to aim for late May, which means we need to start consolidating and
converging about now.
Are there any further big things in the pipeline?
This is also a good point to populate NEWS, CONTRIBUTORS, and upda
Thanks for your input, I have added some of your lemmas to List (and will write
to you about separately).
No, there is no fixed process for adding such contributions. Until it becomes a
nuisance ;-) you are welcome to post them here or send them to some active
developer.
Tobias
Am 16/03/2012 10:
Am 22.03.2012 11:42, schrieb Makarius:
> On Fri, 16 Mar 2012, Florian Haftmann wrote:
>
>> * The set story:
>> https://isabelle.in.tum.de/community/Having_%27a_set_back Not
>> everything mentioned there is an ultimate need, but we should strive
>> to pick as many fruits as we can from the set type
On Fri, 16 Mar 2012, Florian Haftmann wrote:
* The set story:
https://isabelle.in.tum.de/community/Having_%27a_set_back Not everything
mentioned there is an ultimate need, but we should strive to pick as
many fruits as we can from the set type constructor – the more likely
this will compensat
Hi *,
I am currently busy with stocktaking the results of my visit to TUM last
Wednesday, and I have updated the current state of two affairs in the wiki:
* The set story: https://isabelle.in.tum.de/community/Having_%27a_set_back
Not everything mentioned there is an ultimate need, but we should s
Something slightly related and not very important. In changeset
9ff441f295c2 of the Isabelle repo the congruence rule for the constant
"list_ex" is called list_any_cong. For consistency I suggest to rename
it to list_ex_cong.
cheers
chris
On 03/16/2012 06:47 PM, Christian Sternagel wrote:
D
Dear all,
in preparation for the next release I refactored one of our AFP entries
(Abstract-Rewriting). There was an underlying theory Util.thy (quite
big), which essentially turned out to be unused in the rest of the AFP
entry ;) (but we heavily rely on it in IsaFoR, which is not in the AFP).
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 m
> 4 months after Isabelle2011-1 we are roughly in the middle between two
> official releases. This is a good point to recollect things for the
> coming release, better than a few weeks before actual rollout (which
> will the time for testing the integrated system, not adding new features).
In app
Dear all,
4 months after Isabelle2011-1 we are roughly in the middle between two
official releases. This is a good point to recollect things for the
coming release, better than a few weeks before actual rollout (which will
the time for testing the integrated system, not adding new features).
39 matches
Mail list logo
