Re: [isabelle-dev] Towards the next release

2012-11-30 Thread Lawrence Paulson
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.

Re: [isabelle-dev] Towards the next release

2012-11-30 Thread Makarius
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

Re: [isabelle-dev] Towards the next release

2012-11-29 Thread Lawrence Paulson
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 makar...@sketis.net wrote: * A version of Proof General as Isabelle component, like

Re: [isabelle-dev] Towards the next release

2012-11-29 Thread Makarius
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 makar...@sketis.net wrote: * A version of Proof General as Isabelle component, like

Re: [isabelle-dev] Towards the next release

2012-11-21 Thread Makarius
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

[isabelle-dev] Towards the next release

2012-11-20 Thread Makarius
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

Re: [isabelle-dev] Towards the next release

2012-05-02 Thread Gerwin Klein
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 records

Re: [isabelle-dev] Towards the next release

2012-04-19 Thread Lukas Bulwahn
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

Re: [isabelle-dev] Towards the next release

2012-04-19 Thread Makarius
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

Re: [isabelle-dev] Towards the next release

2012-04-18 Thread Florian Haftmann
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

Re: [isabelle-dev] Towards the next release

2012-04-18 Thread Florian Haftmann
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 of

Re: [isabelle-dev] Towards the next release

2012-04-18 Thread Gerwin Klein
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 memory

Re: [isabelle-dev] Towards the next release

2012-04-17 Thread Gerwin Klein
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 things

Re: [isabelle-dev] Towards the next release

2012-04-17 Thread Makarius
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

Re: [isabelle-dev] Towards the next release

2012-04-17 Thread Gerwin Klein
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 very

Re: [isabelle-dev] Towards the next release

2012-04-15 Thread Tobias Nipkow
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 confuse

Re: [isabelle-dev] Towards the next release

2012-04-14 Thread Makarius
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

[isabelle-dev] Towards the next release

2012-04-12 Thread Makarius
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

Re: [isabelle-dev] Towards the next release

2012-04-12 Thread 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 confuse true novices even more. Here are two

Re: [isabelle-dev] Towards the next release

2012-04-12 Thread Makarius
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,

Re: [isabelle-dev] Towards the next release

2012-03-26 Thread Tobias Nipkow
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

Re: [isabelle-dev] Towards the next release

2012-03-22 Thread 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 constructor – the more likely this will

Re: [isabelle-dev] Towards the next release

2012-03-22 Thread Florian Haftmann
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

Re: [isabelle-dev] Towards the next release

2012-03-16 Thread Christian Sternagel
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:

Re: [isabelle-dev] Towards the next release

2012-03-16 Thread Florian Haftmann
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

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] Towards the next release

2012-03-03 Thread Florian Haftmann
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

[isabelle-dev] Towards the next release

2012-02-28 Thread Makarius
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).