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.
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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,
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
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
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:
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
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
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
23 matches
Mail list logo
