Re: [isabelle-dev] Towards the next release
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 30 Nov 2012, at 15:27, Makarius makar...@sketis.net wrote: 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 well e.g. on Ubuntu 12.04 with one of the many open-source applications for that. After spending some hours on it, I tried to present the results on a web page and failed miserably. Web standards don't really exist. One might interpret the 5 in HTML5 as 5 years from now or need 5 different formats for your video. Most people seem to delegate the problem to Youtube. I am only a beginner in the film production business. So maybe some experts on it can say more. Once the technical side-conditions are worked out, one needs to have a good script to explain how to produce nice proof documents (not scripts). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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 had pointed to this before, but it still fun to watch: http://www.youtube.com/user/bauerandrej He is using a different proof assistant, but the classic Proof General 3.7.1.1. So this guy actually has an Isabelle distribution around as well. The last official version of the 3.x branch was 3.7.1, and I made this temporary lifetime extension for the Isabelle distribution in desparation when the Emacs platform was moving forward, but PG 4.x was still not to be seen to catch up. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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 http://isabelle.in.tum.de/components/ProofGeneral-4.1.tar.gz (it must be platform/emacs independent, without .elc files). ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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 http://isabelle.in.tum.de/components/ProofGeneral-4.1.tar.gz (it must be platform/emacs independent, without .elc files). As far as I remember, we've never had a bundled version of Proof General with compiled .elc files. These are non-portable across Emacs versions, so it will not work by default. Working a bit slower is better than not working at all. Once users start recompiling and rearranging things, it gets more like IKEA do-it-yourself software. (I am myself an expert of IKEA hardware assembly for the kitchen and usually enjoy it. Not for software, though.) BTW, for recompiling you need Unix make, and that is not installed by default on any of the 3 platform families: Linux, Mac OS X, Windows. Generally, it touches the question if Proof General should be bundled at all. I started that a long time ago to approximate an out-of-the-box experience for Isabelle, but never succeeded in the last consequence. Right now there are PG 3.7.1.1, 4.0, 4.1 being activly used, so which one to chose? (I would have taken the latest stable version.) Coq never had a PG bundled either, and expert users expect it like that. David Aspinall never liked the bundling of Isabelle Proof General in the first place. So is it time to stop it? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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 PG devel mailing list. I've used 4.2 recently with Isabelle, and found it a bit awkward in some details. Somehow the windows don't pop-up and disappear the way they did before, making it hard to work in the two-window mode of the ancient past that I am still using. (If I were still involved, I would have spent a few days investigating this, produce tracker items, polish the elisp code myself.) Maybe I should make an effort to get the hard-wrap for text paragraphs work smoothly in Isabelle/jEdit, so that I don't have to go back to Emacs just for that (the last thing where I still use the dinosaur). For the Emacs client, definitely Aquamacs. The other Emacs port is terrible, in particular because it doesn't behave at all like a native OS X application. What I need for the release (on-time before the start of the RC phase) is this: * A version of Proof General as Isabelle component, like http://isabelle.in.tum.de/components/ProofGeneral-4.1.tar.gz (it must be platform/emacs independent, without .elc files). * A specification which Emacs.app needs to be included in the Isabelle.app -- I will do the final montage myself. It is then up to remaining PG/Emacs users to test that in the RC phase of the release (2-3 weeks before lift-off). I am not going myself again through the agony and desparation to make all this work in all reasonable combinations that users might have (as I used to do until October 2011). And this for me is still a problem with jEdit as well. So what are the remaining problems? It is time to list them and sort them out if possible. At the Orleans Isabelle Tutorial someone had a very new Mac and was unable to copy-paste from the Output window, but that was Isabelle2012 with the Lobo browser, not the Rich_Text_Area of Isabelle/jEdit now. (I will ask him to test again before the coming release). Anything else that hinders Isabelle/jEdit use, especially on the Mac? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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 with more than ~530 fields where it constructs a lemma of the form f ty = g a b .. aa ab .. tw tx ty tz .. where the ty on the rhs is different to the ty on the left. It should be easy to fix once I manage to trace down where it is actually constructed and I haven't checked yet if it still occurs in the development version. Is this still an open issue for the release? It can wait for after the release. I don't think anyone is blocked on it. Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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). Switching it off gets rid of almost all of the mysterious memory blowup that we had and enables us to run our proofs within 4GB on Linux (32bit) and ~8GB on Darwin (64bit). Having limits like these is not ideal, but I don't see a better workaround, because the code generator setup *is* useful for small records. There is a question on how to implement the limit: 1) as an option available the user at record definition time 2) as an option/flag to the internal record definition function only 3) as a configuration option 4) as a compile time constant 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 lemma of the form f ty = g a b .. aa ab .. tw tx ty tz .. where the ty on the rhs is different to the ty on the left. It should be easy to fix once I manage to trace down where it is actually constructed and I haven't checked yet if it still occurs in the development version. 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) Provided support for all those funny quickcheck generators. I would strongly recommend not to sacrifice a) for a »optimisiation« (once I had something similar in the datatype package and it produced a lot of pain); basically, it uses theorems which are »almost there« anyway. 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 for a) and b). Commenting out ensure_random_record and ensure_exhaustive_record in function add_code coulde make a good start. Undoubtedly, Quickcheck has to produce a few large terms for each record to support them. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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 time -- it goes back to formerly passive theories by Norbert Schirmer. This is run by isatest via the special full target, which is meant to measure things that don't need to be tested otherwise. Here are some recent statistics http://isabelle.in.tum.de/devel/stats/mac-poly64-M4/HOL-Record_Benchmark.png Formally, one can imagine the record package to provide a few boolean options record_codegen, record_quickcheck etc. to control certain features in an agnostic way. One needs to make sure that such feature variants are routinely tested. One should also try hard to understand the actual issues that are worked around here. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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 instantiation and not
on the second one? In any event, if the user gets wrong, a warning would be
appropriate. And I hope that wouldn't be difficult to implement.
instantiation hf :: sup
begin
definition sup_hf :: hf \Rightarrow hf \Rightarrow hf
where sup_hf a b = ...
instantiation hf :: minus
begin
definition minus_hf where
minus A B = ...
instance proof
the rules are roughly as follows:
* Given a class parameter foo to be instantiated to a type bar, the
corresponding parameter name for defining foo on bar is foo_bar; this
can also be inspected using the print_context command inside the
instantiation block.
* Given a class parameter foo with type T[?'a], each of its appearances
at type T[('a, …, 'z) bar] is substituted by foo_bar.
Hope this helps,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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 the mysterious memory blowup that we had and enables us to run our proofs within 4GB on Linux (32bit) and ~8GB on Darwin (64bit). Having limits like these is not ideal, but I don't see a better workaround, because the code generator setup *is* useful for small records. There is a question on how to implement the limit: 1) as an option available the user at record definition time 2) as an option/flag to the internal record definition function only 3) as a configuration option 4) as a compile time constant 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 lemma of the form f ty = g a b .. aa ab .. tw tx ty tz .. where the ty on the rhs is different to the ty on the left. It should be easy to fix once I manage to trace down where it is actually constructed and I haven't checked yet if it still occurs in the development version. 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) Provided support for all those funny quickcheck generators. I would strongly recommend not to sacrifice a) for a »optimisiation« (once I had something similar in the datatype package and it produced a lot of pain); basically, it uses theorems which are »almost there« anyway. 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 for a) and b). Commenting out ensure_random_record and ensure_exhaustive_record in function add_code coulde make a good start. Also note that most of the quickcheck addons are by Lukas, not me ;-) Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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 (and time). Switching it off gets rid of almost all of the mysterious memory blowup that we had and enables us to run our proofs within 4GB on Linux (32bit) and ~8GB on Darwin (64bit). Having limits like these is not ideal, but I don't see a better workaround, because the code generator setup *is* useful for small records. There is a question on how to implement the limit: 1) as an option available the user at record definition time 2) as an option/flag to the internal record definition function only 3) as a configuration option 4) as a compile time constant 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 lemma of the form f ty = g a b .. aa ab .. tw tx ty tz .. where the ty on the rhs is different to the ty on the left. It should be easy to fix once I manage to trace down where it is actually constructed and I haven't checked yet if it still occurs in the development version. 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) Provided support for all those funny quickcheck generators. I would strongly recommend not to sacrifice a) for a »optimisiation« (once I had something similar in the datatype package and it produced a lot of pain); basically, it uses theorems which are »almost there« anyway. It's not an optimisation for us. It's the choice between using Isabelle or not. I'm happy to sacrifice a lot of features for that choice.. 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 for a) and b). Commenting out ensure_random_record and ensure_exhaustive_record in function add_code coulde make a good start. My feeling is that the problem already occurs in a), but you are right, this needs to be confirmed. I'll measure and see how things go. 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. Also note that most of the quickcheck addons are by Lukas, not me ;-) Sorry, I had just assumed that anything that looks like code generator is in your domain ;-) Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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 from the NICTA side in the pipeline (should be in by end of April): - Tom would like to add a tactic for bit-wise proofs on machine words, based on Sacha's and his work a while back. This is one is ready, I'll push it to the test board later and add it to the repository if everything works. - 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 the mysterious memory blowup that we had and enables us to run our proofs within 4GB on Linux (32bit) and ~8GB on Darwin (64bit). Having limits like these is not ideal, but I don't see a better workaround, because the code generator setup *is* useful for small records. There is a question on how to implement the limit: 1) as an option available the user at record definition time 2) as an option/flag to the internal record definition function only 3) as a configuration option 4) as a compile time constant I'm currently in favour of 4, because the limit is very specialised and will only really occur for records that are somehow automatically generated in which case the code generator setup is very unlikely to make sense. Options 1 and 3 would require adding syntax/configuration names which is not really worth it. Option 2 threads yet another obscure parameter through a rather large package. I'm open to other ideas/comments/feedback, though. 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 lemma of the form f ty = g a b .. aa ab .. tw tx ty tz .. where the ty on the rhs is different to the ty on the left. It should be easy to fix once I manage to trace down where it is actually constructed and I haven't checked yet if it still occurs in the development version. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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 large amounts of memory
(and time). Switching it off gets rid of almost all of the mysterious memory
blowup that we had and enables us to run our proofs within 4GB on Linux
(32bit) and ~8GB on Darwin (64bit). Having limits like these is not ideal,
but I don't see a better workaround, because the code generator setup *is*
useful for small records. There is a question on how to implement the limit:
1) as an option available the user at record definition time
2) as an option/flag to the internal record definition function only
3) as a configuration option
4) as a compile time constant
I'm currently in favour of 4, because the limit is very specialised and will
only really occur for records that are somehow automatically generated in
which case the code generator setup is very unlikely to make sense. Options
1 and 3 would require adding syntax/configuration names which is not really
worth it. Option 2 threads yet another obscure parameter through a rather
large package.
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 pollutes the config name
space a little more for users. Of course it also means that it can be changed
at runtime. If there is a slight preference for this, I'm happy to go that road.
Concerning performance issues in general, I've recently made a lot of
measurements. It seems indeed that the code generator is responsible for
quite a bit of it, although I did not look any further into its depths.
Instead I've made some performance tuning for the critical infrastructure for
localizing big packages with big application.
Yes, this looks very promising. After the record package/code generator find
we're now almost done updating things to Isabelle2011-1. Just in time for
Isabelle2012 ;-)
Moreover, David Matthews is right now reforming the Poly/ML runtime system,
such that we might see an improvement of an order of magnitude soon.
We'll be very keen on that one, too.
Cheers,
Gerwin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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 true novices even more. Here are two instantiations, both of which simply do overloading but justify no properties. Such instantiations always succeed, because there is nothing to prove. But I discovered that you have to be very careful to introduce overloading correctly. If it's wrong, the instantiation effectively does nothing; when that happens, a warning ought to appear. 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 instantiation and not on the second one? In any event, if the user gets wrong, a warning would be appropriate. And I hope that wouldn't be difficult to implement. instantiation hf :: sup begin definition sup_hf :: hf \Rightarrow hf \Rightarrow hf where sup_hf a b = ... instantiation hf :: minus begin definition minus_hf where minus A B = ... instance proof Probably most users of locales have experienced this situation. I don't know if it is easy to explain the rules or to improve the situation. I think that the fully qualified name f_type always works (?) and one can then try to see if the suffix can be dropped. I would be happy with that but one problem remains: if you drop the suffix, I don't know how to tell if it worked except that your instance proof fails for no clear reason if it did not work. That is my main source of confusion. Tobias Larry On 12 Apr 2012, at 10:02, 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? This is also a good point to populate NEWS, CONTRIBUTORS, and update manuals to cover new things. (I am speaking to myself here as well.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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 to continue, but have not made any progress in the implementation itself. I have also spoken to Stefan Berghofer again, and encoraged him to help porting his great graph layout tool to Scala. Conceptually, the old graph browser can still compete with newer things on the market, but with its use of AWT from Java 1.1 that is hard to explain to end-users. (It is also technically hard to integrate into contemporary Swing components.) Before Stefan starts yet another implementation, we should make sure that the different projects converge. The idea was the same as before, when we had our joint discussion on the browser projects: join the efforts of Stefan from 1996 and Markus Kaiser from 2011. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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, both of which simply do overloading but justify no properties. Such instantiations always succeed, because there is nothing to prove. But I discovered that you have to be very careful to introduce overloading correctly. If it's wrong, the instantiation effectively does nothing; when that happens, a warning ought to appear. 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 instantiation and not on the second one? In any event, if the user gets wrong, a warning would be appropriate. And I hope that wouldn't be difficult to implement. instantiation hf :: sup begin definition sup_hf :: hf \Rightarrow hf \Rightarrow hf where sup_hf a b = ... instantiation hf :: minus begin definition minus_hf where minus A B = ... instance proof Larry On 12 Apr 2012, at 10:02, 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? This is also a good point to populate NEWS, CONTRIBUTORS, and update manuals to cover new things. (I am speaking to myself here as well.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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, and the source code improvements would not change so much from a user's point of view. I remember well our discussion with Stefan Berghofer and especially Markus Kaiser who did the main work in this project. We parted at the point where everybody observed the little return that JUNG gives for all the investment that it requires. This huge framework also seems to be unmaintained since 2010, exactly at the moment when I was getting excited about it (errornously). After removing all the initial hopes what JUNG would deliver, only two potential benefits were remaining on our list: (1) Java object model for graph data structures (2) facilities for drawing and a bit of editing of graphs You had pointed out that a port of the Isabelle graph.ML to Scala would make (1) obsolete (which has its own problems due to mutability). I did that in the meantime, and made various refinements so that http://isabelle.in.tum.de/repos/isabelle/file/83294cd0e7ee/src/Pure/General/graph.scala is pretty stable and closely agrees with the ML version. I am already using graph.scala myself in the Prover IDE document model, to manage dependencies of theory buffers etc. 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? I have also spoken to Stefan Berghofer again, and encoraged him to help porting his great graph layout tool to Scala. Conceptually, the old graph browser can still compete with newer things on the market, but with its use of AWT from Java 1.1 that is hard to explain to end-users. (It is also technically hard to integrate into contemporary Swing components.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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:47, schrieb Christian Sternagel: 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). While refactoring I saw that some lemmas from Util.thy have found their way (either by moving or independently) into the main Isabelle distribution (mostly List.thy) -- but without being removed from the AFP entry. Still there are many definitions and lemmas left that are not part of the main distribution (some of which are ugly and ad hoc, but others quite useful and maybe deserving to end up in the distribution or library). After this rather long story ;) my actual question: Is there some way to propose definitions/lemmas for the main distribution/library? If not, maybe someone of the developers feels like reading through the attached theory-file and picking out whatever he/she likes? cheers chris On 02/28/2012 10:21 PM, Makarius wrote: 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). After 3.4 weeks vacation in Marokko in Jan/Feb and 2 weeks working through my mail folders like crazy, I still have issues in the pipeline that need to be reanimated. I also need to figure out which essential things of the Prover IDE can make it into the release ... Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev This body part will be downloaded on demand. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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 compensate users if they have to adjust their theories * The numeral story: https://isabelle.in.tum.de/community/Numerals It looks quite good (preliminary tests of the AFP did not reveal much problems). The fork should be done by the end of April. The further perspectives listed there are no need-to-haves for the next release. Does it mean both will reforms will be finished for the coming release? Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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: 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). While refactoring I saw that some lemmas from Util.thy have found their way (either by moving or independently) into the main Isabelle distribution (mostly List.thy) -- but without being removed from the AFP entry. Still there are many definitions and lemmas left that are not part of the main distribution (some of which are ugly and ad hoc, but others quite useful and maybe deserving to end up in the distribution or library). After this rather long story ;) my actual question: Is there some way to propose definitions/lemmas for the main distribution/library? If not, maybe someone of the developers feels like reading through the attached theory-file and picking out whatever he/she likes? cheers chris On 02/28/2012 10:21 PM, Makarius wrote: 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). After 3.4 weeks vacation in Marokko in Jan/Feb and 2 weeks working through my mail folders like crazy, I still have issues in the pipeline that need to be reanimated. I also need to figure out which essential things of the Prover IDE can make it into the release ... Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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 strive to pick as many fruits as we can from the set type constructor – the more likely this will compensate users if they have to adjust their theories * The numeral story: https://isabelle.in.tum.de/community/Numerals It looks quite good (preliminary tests of the AFP did not reveal much problems). The fork should be done by the end of April. The further perspectives listed there are no need-to-haves for the next release. I further did some doodling around with mira; after 14 staying away from there I did not encountered fundamental difficulties, but my original intent, operative configurations for distribution build and docs, did not grow very far. I will set aside this as it is by now and would appreciate if anybody would continue on this, sooner or later. After this experience I will keep mira on my screen, but when I will return to it I plan to focus on * re-learn what the current deployment at TUM is * improve the notoriously annoying settings mechanisms * minor technical improvements before doing anything end-user visible. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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 more likely to actually do it. Yours, Thomas. The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
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 approx. two weeks I plan to be in Garching and distill a working plan there, containing * still things to polish for sets (https://isabelle.in.tum.de/community/Having_%27a_set_back), to let users benefit from the new situation as much as possible * state of alternative numeral representation (https://isabelle.in.tum.de/community/Numerals) – I am still optimistic that this can make it into the next release, although a lot of things which can be improved then compared to what is now will have to wait. * various cleanups, e.g. set/pred relations, HOL-Import, code generation, enriched type (don't know how far I can get with that). Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
