Re: [isabelle-dev] NEWS: numeral representation
> However, you have talked about making the binary representation for > "nat" the default in HOL-Main, i.e. merging Code_Nat into the Nat/Num > theories. Are you still interested in doing this? Definitely, among other related things. But I'm not very optimistic this can be done before the end of April. It is not essential that it makes its way into the next release. 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] NEWS: numeral representation
On Thu, Mar 29, 2012 at 7:50 AM, Florian Haftmann wrote: > As it is now, theory »Code_Nat« is > not announced that prominently, but this is not that critical. We should at least put an announcement in NEWS about Code_Nat. However, you have talked about making the binary representation for "nat" the default in HOL-Main, i.e. merging Code_Nat into the Nat/Num theories. Are you still interested in doing this? - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: numeral representation
Hi Brian, > You had replaced Efficient_Nat.thy with a similar theory file named > Code_Numeral_Nat.thy. I chose to rename this back to Efficient_Nat > before doing the big merge, because it meant touching about a dozen > fewer files, and avoiding breaking lots of AFP entries. I also > reverted the updates that you put in NEWS and the other documentation > related to the rename: > > http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/numerals/rev/350dd336be43 > http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/numerals/rev/df49a9297ced > http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/numerals/rev/afe641c9b5d8 > > If you still want to use the name "Code_Numeral_Nat", go ahead and put > these changes back in. I have no strong opinion about that. As it is now, theory »Code_Nat« is not announced that prominently, but this is not that critical. > Besides the Efficient_Nat/Code_Numeral_Nat naming, is there anything > else that you are still missing? No. Everything seems to be there. All the best, 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] Isatest
Am 28/03/2012 23:30, schrieb Gerwin Klein: > On 29/03/2012, at 6:11 AM, Makarius wrote: > >> On Wed, 28 Mar 2012, Florian Haftmann wrote: >> >>> Once there has been the idea that everyone having commit access to the >>> Isabelle master repository (POSIX group isabelle at nfsbroy) is also a >>> isatest subscriber. >>> >>> Maybe it would be helpful to establish this as a rule (at least of thumb). >>> Isatest mails can still be sorted out by local email filters. >>> >>> What do you think? >> >> I could imagine some reforms in the meaning of the Unix group "isabelle" and >> how it is managed, although I have a tendency to leave the status-quo >> untouched. >> >> For every administrative facility that is added, one also needs to take >> maintenance into account. > > Yes, that is the main problem I see with this (otherwise I'm all for it). If > there is an email list that automatically contains everyone with push-access, > emails could easily be sent there. I wouldn't want to have to maintain that > email list, tough. Florian suggested "a rule (of thumb)", not automation. Hence I am still in favour. It just means that whoever grants write access should try and remember to add that person to the email list. Tobias > >> Who is the main responsible for isatest anyway? According to the received >> customs it would be Gerwin, since he started the service many years ago. >> (His shell scripts still mention SunOS.) > > They do ;-) > > I still feel mildly responsible for isatest, but would be more than happy to > pass this on to somebody with more time and more close in time(zone) and and > space to where it actually runs. > > Cheers, > Gerwin > > ___ > 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] New HOL/Import
Hi all, We have been working on a modernized reimplementation of HOL/Import, for HOL Light. We think we are at a point where it could be pushed to the main Isabelle repository replacing the old one. Therefore two questions: - Is anyone using the old HOL/Import? - Does anyone have opinions about the HOL4 code that has been long dead? Most important changes in the new importer as opposed to the old one: - It is much more scalable. Regular HOL-Light can be imported in less than a minute. Importing bigger theories works as well. - Rather than generating 'thy' files it creates an Image file and documentation, see either of the below: http://cl-informatik.uibk.ac.at/~cek/import.html http://cl-informatik.uibk.ac.at/~cek/import.pdf - The code is shorter and cleaner. For those that would like to inspect the code it is at: http://cl-informatik.uibk.ac.at/~cek/import.tgz Regards, Cezary -- Cezary Kaliszyk, University of Innsbruck, http://cl-informatik.uibk.ac.at/~cek/ ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isatest
On 29/03/2012, at 6:11 AM, Makarius wrote: > On Wed, 28 Mar 2012, Florian Haftmann wrote: > >> Once there has been the idea that everyone having commit access to the >> Isabelle master repository (POSIX group isabelle at nfsbroy) is also a >> isatest subscriber. >> >> Maybe it would be helpful to establish this as a rule (at least of thumb). >> Isatest mails can still be sorted out by local email filters. >> >> What do you think? > > I could imagine some reforms in the meaning of the Unix group "isabelle" and > how it is managed, although I have a tendency to leave the status-quo > untouched. > > For every administrative facility that is added, one also needs to take > maintenance into account. Yes, that is the main problem I see with this (otherwise I'm all for it). If there is an email list that automatically contains everyone with push-access, emails could easily be sent there. I wouldn't want to have to maintain that email list, tough. > Who is the main responsible for isatest anyway? According to the received > customs it would be Gerwin, since he started the service many years ago. (His > shell scripts still mention SunOS.) They do ;-) I still feel mildly responsible for isatest, but would be more than happy to pass this on to somebody with more time and more close in time(zone) and and space to where it actually runs. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: numeral representation
On Wed, Mar 28, 2012 at 9:15 PM, Florian Haftmann wrote: > Btw. for the moment you have not transferred by additional changes > concerning Efficient_Nat etc. What are your plans for these? To wait > until the transition proper has fortified a little? Or shall I take > care for these? Hi Florian, You had replaced Efficient_Nat.thy with a similar theory file named Code_Numeral_Nat.thy. I chose to rename this back to Efficient_Nat before doing the big merge, because it meant touching about a dozen fewer files, and avoiding breaking lots of AFP entries. I also reverted the updates that you put in NEWS and the other documentation related to the rename: http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/numerals/rev/350dd336be43 http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/numerals/rev/df49a9297ced http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/numerals/rev/afe641c9b5d8 If you still want to use the name "Code_Numeral_Nat", go ahead and put these changes back in. Besides the Efficient_Nat/Code_Numeral_Nat naming, is there anything else that you are still missing? - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] pred_set_conv – unidirectional rule
Hi Stefan, when considering the prospective predicate equivalent to Id, I concluded that the corresponding pred_set_conv rule should read: lemma [pred_set_conv]: "HOL.eq = (\x y. (x, y) \ Id)" by (auto simp add: Id_def fun_eq_iff) However, for obvious reasons (LHS!), this should only be applied from right to left, not the other way round! Is there a simple way to make such unidirectional rules possible? If not, it is not desaster. All the best, 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] NEWS: numeral representation
Hi Brian, >> OK, I have disabled HOL-Proofs-Lambda for the moment (cf. 500a5d97511a). > > This is now fixed in a3a64240cd98, and I have re-enabled HOL-Proofs-Lambda. > > The problem was the code equation for function "nat" configured in > Library/Code_Integer.thy which, in conjunction with Int.nat_numeral > [code_abbrev], produced code that looped indefinitely. thanks for taking care of this. Btw. for the moment you have not transferred by additional changes concerning Efficient_Nat etc. What are your plans for these? To wait until the transition proper has fortified a little? Or shall I take care for these? 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] Isatest
On Wed, 28 Mar 2012, Florian Haftmann wrote: Once there has been the idea that everyone having commit access to the Isabelle master repository (POSIX group isabelle at nfsbroy) is also a isatest subscriber. Maybe it would be helpful to establish this as a rule (at least of thumb). Isatest mails can still be sorted out by local email filters. What do you think? I could imagine some reforms in the meaning of the Unix group "isabelle" and how it is managed, although I have a tendency to leave the status-quo untouched. For every administrative facility that is added, one also needs to take maintenance into account. Last weekend I had to spend more time to figure out why isatest did not send any mails at all, than who needs to be added to the list. Who is the main responsible for isatest anyway? According to the received customs it would be Gerwin, since he started the service many years ago. (His shell scripts still mention SunOS.) Yet a different angle on the situation is to de-centralize a few things that are not essential for the main Isabelle repository. I have already started to do a few small-scale things independently via bitbucket, which I would have done via the Isabelle repos some years ago. This does not mean that I have any concrete proposals in the pocket, let's say about using a really really good issue tracker service on some open source hosting platform -- if it exists at all. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Name for derived quotient_def theorem
>> This is explained by looking at the history: The typedef package >> introduces names with underscores, quotient_type and quotient_def >> inherit this from typedef. > > This is a misunderstanding. The names generated by »typedef« have > always been retained »as they are«, merely for the sacrosanctity of > Gordon Typedef. Quotient should use the contemporary scheme. Let me add: IMHO these are the typical things which should be repaired *before* users get used to it. 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] Name for derived quotient_def theorem
What I had in mind was something as can be found e.g. in
src/HOL/Library/Dlist.thy:
definition empty :: "'a dlist"
where
"empty = Dlist []"
definition insert :: "'a \ 'a dlist \ 'a dlist"
where
"insert x dxs = Dlist (List.insert x (list_of_dlist dxs))"
definition remove :: "'a \ 'a dlist \ 'a dlist"
where
"remove x dxs = Dlist (remove1 x (list_of_dlist dxs))"
definition map :: "('a \ 'b) \ 'a dlist
\ 'b dlist" where
"map f dxs = Dlist (remdups (List.map f (list_of_dlist dxs)))"
definition filter :: "('a \ bool) \ 'a dlist
\ 'a dlist" where
"filter P dxs = Dlist (List.filter P (list_of_dlist dxs))"
lemma list_of_dlist_empty [simp, code abstract]:
"list_of_dlist empty = []"
by (simp add: empty_def)
lemma list_of_dlist_insert [simp, code abstract]:
"list_of_dlist (insert x dxs) = List.insert x (list_of_dlist dxs)"
by (simp add: insert_def)
lemma list_of_dlist_remove [simp, code abstract]:
"list_of_dlist (remove x dxs) = remove1 x (list_of_dlist dxs)"
by (simp add: remove_def)
lemma list_of_dlist_map [simp, code abstract]:
"list_of_dlist (map f dxs) = remdups (List.map f (list_of_dlist dxs))"
by (simp add: map_def)
lemma list_of_dlist_filter [simp, code abstract]:
"list_of_dlist (filter P dxs) = List.filter P (list_of_dlist dxs)"
by (simp add: filter_def)
Here, the derived equations *are* simplification rules, in the sense
that they simplify from abstract to concrete values. This pattern
enables convient proofs of abstract equational properties by using
extensionality and then default simplicifcation. Hence the idea of
».simp«. Anyway, I do not object to ».rep«, although the disadvantage
is that the corresponding operation will seldom be named »rep«.
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] sets and code generation
Hi Jesus, > trying to import simultaneously the theory file > "HOL/Matrix/Matrix.thy" and the afp entry > http://afp.sourceforge.net/entries/Matrix.shtml into a file, it seems > that the second theory file "unloads" the first one (as Makarius > suggested in his mail): > > theory Matrix_ex > imports > "~~/src/HOL/Matrix/Matrix" > "Matrix/Matrix" > begin > > Is there an easy way out of this situation in Isabelle2011-1? Renaming > one of the theory files is an acceptable solution in this case? It is. Cf. the previous email of Makarius on the same thread. 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] Name for derived quotient_def theorem
> This is explained by looking at the history: The typedef package > introduces names with underscores, quotient_type and quotient_def > inherit this from typedef. This is a misunderstanding. The names generated by »typedef« have always been retained »as they are«, merely for the sacrosanctity of Gordon Typedef. Quotient should use the contemporary scheme. 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] Isatest
Sounds like a sensible idea to avoid test failures to go unnoticed. Tobias Am 28/03/2012 20:45, schrieb Florian Haftmann: > Hi all, > > Once there has been the idea that everyone having commit access to the > Isabelle master repository (POSIX group isabelle at nfsbroy) is also a > isatest subscriber. > > Maybe it would be helpful to establish this as a rule (at least of > thumb). Isatest mails can still be sorted out by local email filters. > > What do you think? > > Maybe in the future with mira taking over more and more realm from > isatest, one could invent a more clever mechanism, e.g. only mail > authors of critical changesets – which, by the way, should not be that > difficult to implement as it is now. > > Cheers, > Florian > > > > > 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
[isabelle-dev] Isatest
Hi all, Once there has been the idea that everyone having commit access to the Isabelle master repository (POSIX group isabelle at nfsbroy) is also a isatest subscriber. Maybe it would be helpful to establish this as a rule (at least of thumb). Isatest mails can still be sorted out by local email filters. What do you think? Maybe in the future with mira taking over more and more realm from isatest, one could invent a more clever mechanism, e.g. only mail authors of critical changesets – which, by the way, should not be that difficult to implement as it is now. 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] Name for derived quotient_def theorem
On Wed, 28 Mar 2012, Ondřej Kunčar wrote: After a long discussion during a lunch break we decided to use ".rep_eq". I will also change "_rsp" to ".rsp". What about "_def"? Should I change it to ".def" as well? "_def" seems to be a inconsistency, I guess because of historical reasons. Should new packages use ".def" instead of "_def"? I don't see a reason for ".def" -- the traditional "_def" still does its job. By convention it somehow refers to a basic definition behind the scenes, which is sometimes public, sometimes considered private. BTW, qualified bindings do work in general, but not for term entities. So a Local_Theory.define with qualified names will not exactly work as could be expected, although that is its normal hevaiour: to regard only the base name in the auxiliary context. So local term definitions of some "foo.make" and "bar.make" will cause an error. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Name for derived quotient_def theorem
After a long discussion during a lunch break we decided to use ".rep_eq". I will also change "_rsp" to ".rsp". What about "_def"? Should I change it to ".def" as well? "_def" seems to be a inconsistency, I guess because of historical reasons. Should new packages use ".def" instead of "_def"? Ondrej On 03/28/2012 09:29 AM, Tobias Nipkow wrote: Yes, "simps" should not be used for special purpose rules. Tobias Am 28/03/2012 09:22, schrieb Lukas Bulwahn: Hi Florian, Thank you for your suggestions. We will take them into account. On 03/28/2012 07:26 AM, Florian Haftmann wrote: http://isabelle.in.tum.de/reports/Isabelle/rev/861f53bd95fe#l1.53 the name given to the derived theorem is unsatisfactory. Since it is not a »code-only« theorem, it should not carry the »code« within. If it would be a »code-only« theorem, the convention is to suffix with »_code«, not »_code_eqn«. Also, for derived theorems proved by packages it is much more common to use qualification suffixes (e.g. ».simp«, ».intro«) rather than plumbing underscores (cf. module binding.ML). Btw. this also applies to the respectfulness theorem: ».rsp« would be better than »_rsp«. This is explained by looking at the history: The typedef package introduces names with underscores, quotient_type and quotient_def inherit this from typedef. Here a list of names we were thinking of while discussing: - abstract_eq - abs_equation - abs_def - code_cert - code_certificate In the end, we decided for the one you can see (although I am personally still in favor of abs_equation or similar). I think ".simp" is rather strange, because it is really not simplifying anything, but rather unfolding the definition in some special way. Lukas ___ 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] Isabelle/jEdit build
The -bf option did the trick. Earlier I tried to remove things to get it rebuild. Obviously I did not manage to remove everything. Thank you. Viorel On 3/28/12 4:56 PM, Makarius wrote: On Wed, 28 Mar 2012, Viorel Preoteasa wrote: I managed to get it working with the latest version of jedit_build. However, I could only get it using scala-2.8.2.final and not with scala-2.9.1-1. Using scala-2.9.1-1 on OS X Lion generates the error: I think I did try it with scala-2.9.1-1 on OS X Lion as well, presently back on good old Snow Leopard. When you get strange class loader errors, it can mean that there are some old jars hanging around from a different build, say in ~/.isabelle/jedit/jars or ISABELLE_HOME/lib/classes You can try "isabelle jedit -bf" to force a fresh build. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle/jEdit build
On Wed, 28 Mar 2012, Viorel Preoteasa wrote: I managed to get it working with the latest version of jedit_build. However, I could only get it using scala-2.8.2.final and not with scala-2.9.1-1. Using scala-2.9.1-1 on OS X Lion generates the error: I think I did try it with scala-2.9.1-1 on OS X Lion as well, presently back on good old Snow Leopard. When you get strange class loader errors, it can mean that there are some old jars hanging around from a different build, say in ~/.isabelle/jedit/jars or ISABELLE_HOME/lib/classes You can try "isabelle jedit -bf" to force a fresh build. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle/jEdit build
Hi, I managed to get it working with the latest version of jedit_build. However, I could only get it using scala-2.8.2.final and not with scala-2.9.1-1. Using scala-2.9.1-1 on OS X Lion generates the error: ### Building Isabelle/jEdit ... 4:18:55 PM [main] [error] PluginJAR: Error while starting plugin isabelle.jedit.Plugin 4:18:55 PM [main] [error] PluginJAR: java.lang.NoClassDefFoundError: scala/Serializable 4:18:55 PM [main] [error] PluginJAR: at java.lang.ClassLoader.defineClass1(Native Method) 4:18:55 PM [main] [error] PluginJAR: at java.lang.ClassLoader.defineClassCond(ClassLoader.java:631) 4:18:55 PM [main] [error] PluginJAR: at java.lang.ClassLoader.defineClass(ClassLoader.java:615) 4:18:55 PM [main] [error] PluginJAR: at java.lang.ClassLoader.defineClass(ClassLoader.java:465) 4:18:55 PM [main] [error] PluginJAR: at org.gjt.sp.jedit.JARClassLoader._loadClass(JARClassLoader.java:439) 4:18:55 PM [main] [error] PluginJAR: at org.gjt.sp.jedit.JARClassLoader.loadClass(JARClassLoader.java:109) 4:18:55 PM [main] [error] PluginJAR: at java.lang.ClassLoader.loadClass(ClassLoader.java:247) 4:18:55 PM [main] [error] PluginJAR: at isabelle.jedit.Plugin.(plugin.scala:385) 4:18:55 PM [main] [error] PluginJAR: at sun.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method) 4:18:55 PM [main] [error] PluginJAR: at sun.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:39) 4:18:55 PM [main] [error] PluginJAR: at sun.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:27) 4:18:55 PM [main] [error] PluginJAR: at java.lang.reflect.Constructor.newInstance(Constructor.java:513) 4:18:55 PM [main] [error] PluginJAR: at java.lang.Class.newInstance0(Class.java:355) 4:18:55 PM [main] [error] PluginJAR: at java.lang.Class.newInstance(Class.java:308) 4:18:55 PM [main] [error] PluginJAR: at org.gjt.sp.jedit.PluginJAR.activatePlugin(PluginJAR.java:735) 4:18:55 PM [main] [error] PluginJAR: at org.gjt.sp.jedit.PluginJAR.activatePluginIfNecessary(PluginJAR.java:823) 4:18:55 PM [main] [error] PluginJAR: at org.gjt.sp.jedit.jEdit.main(jEdit.java:486) 4:18:55 PM [main] [error] PluginJAR: Caused by: java.lang.ClassNotFoundException: scala.Serializable 4:18:55 PM [main] [error] PluginJAR: at java.net.URLClassLoader$1.run(URLClassLoader.java:202) 4:18:55 PM [main] [error] PluginJAR: at java.security.AccessController.doPrivileged(Native Method) 4:18:55 PM [main] [error] PluginJAR: at java.net.URLClassLoader.findClass(URLClassLoader.java:190) 4:18:55 PM [main] [error] PluginJAR: at java.lang.ClassLoader.loadClass(ClassLoader.java:306) 4:18:55 PM [main] [error] PluginJAR: at sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:301) 4:18:55 PM [main] [error] PluginJAR: at java.lang.ClassLoader.loadClass(ClassLoader.java:247) 4:18:55 PM [main] [error] PluginJAR: at org.gjt.sp.jedit.JARClassLoader.loadFromParent(JARClassLoader.java:522) 4:18:55 PM [main] [error] PluginJAR: at org.gjt.sp.jedit.JARClassLoader.loadClass(JARClassLoader.java:87) 4:18:55 PM [main] [error] PluginJAR: at java.lang.ClassLoader.loadClass(ClassLoader.java:247) 4:18:55 PM [main] [error] PluginJAR: ... 17 more 4:18:55 PM [main] [error] ErrorListDialog$ErrorEntry: /Users/viorel/Work/isabelle-dev/isabelle/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar: 4:18:55 PM [main] [error] ErrorListDialog$ErrorEntry: Cannot start: java.lang.NoClassDefFoundError: scala/Serializable 4:18:55 PM [main] [error] ErrorListDialog$ErrorEntry: Try updating to a newer version of the plugin. lemon:isabelle viorel$ bin/isabelle jedit 4:21:20 PM [main] [error] PluginJAR: Error while starting plugin isabelle.jedit.Plugin 4:21:20 PM [main] [error] PluginJAR: java.lang.NoClassDefFoundError: scala/Serializable 4:21:20 PM [main] [error] PluginJAR: at java.lang.ClassLoader.defineClass1(Native Method) 4:21:20 PM [main] [error] PluginJAR: at java.lang.ClassLoader.defineClassCond(ClassLoader.java:631) 4:21:20 PM [main] [error] PluginJAR: at java.lang.ClassLoader.defineClass(ClassLoader.java:615) 4:21:20 PM [main] [error] PluginJAR: at java.lang.ClassLoader.defineClass(ClassLoader.java:465) 4:21:20 PM [main] [error] PluginJAR: at org.gjt.sp.jedit.JARClassLoader._loadClass(JARClassLoader.java:439) 4:21:20 PM [main] [error] PluginJAR: at org.gjt.sp.jedit.JARClassLoader.loadClass(JARClassLoader.java:109) 4:21:20 PM [main] [error] PluginJAR: at java.lang.ClassLoader.loadClass(ClassLoader.java:247) 4:21:20 PM [main] [error] PluginJAR: at isabelle.jedit.Plugin.(plugin.scala:385) 4:21:20 PM [main] [error] PluginJAR: at sun.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method) 4:21:20 PM [main] [error] PluginJAR: at sun.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:39) 4:21:20 PM [main] [error] PluginJAR: at sun.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImp
[isabelle-dev] Isabelle/jEdit build
This is a summary of the current situation with instantaneous building of Isabelle/jEdit from the repository (version 300fa46fd081). * http://www4.in.tum.de/~wenzelm/test/jedit_build-20120327.tar.gz provides the auxiliary jedit_build component, which is now using jedit-4.5.1 (there is an improved treatment of > 16bit Unicode, as requested last year by myself on the jEdit tracker). The component is installed as usual, e.g. via this in ~/.isabelle/etc/settings: init_component ".../jedit_build-20120327" Where "..." is expanded to the relative or absolute location of the unpacked component. * ISABELLE_JDK_HOME needs to point to a genuine JDK installation, with the proper directory layout (the standard one of Oracle, not the one of Debian). Mac OS users can set it like this in ~/.isabelle/etc/settings: ISABELLE_JDK_HOME="$(/usr/libexec/java_home -v 1.6)" * SCALA_HOME needs to point to genuine Scala according to EPFL, not Debian. The variable can be set in regular shell startup environment or Isabelle settings. I have also tried everything with latest Mac OS X Lion -- it works for me. There is no need to change anything if it works for you already. In the coming release everything will be bundled again to work out-of-the box, including full JDK components for the usual platforms. (This investment of 100-200 MB disk space saves a lot of worries for anybody.) Adventurous beta testers are encouraged to try latest JDK 1.7.x and Scala 2.10.x release candidates. Both should also work quite well already. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Building the IsarImplementation Manual on 9fc17f9ccd6c
On Wed, 28 Mar 2012, Lukas Bulwahn wrote: I cannot build the IsarImplementation Manual on 9fc17f9ccd6c: Maybe some latest change broke the document generation. See now Isabelle/b9b2e183e94d. We still don't have fully automatic doc tests, so it has to be checked manually. Doing that I've found another drop-out: *** Unknown fact "numeral_0_eq_0" (line 28 of "~~/doc-src/TutorialI/Types/Numbers.thy") *** The error(s) above occurred in document antiquotation: "Pure.thm" (line 28 of "~~/doc-src/TutorialI/Types/Numbers.thy") *** At command "text" (line 27 of "~~/doc-src/TutorialI/Types/Numbers.thy") Brian should know what to do here. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Building the IsarImplementation Manual on 9fc17f9ccd6c
I cannot build the IsarImplementation Manual on 9fc17f9ccd6c: Maybe some latest change broke the document generation. Lukas Running HOL-Thy ... HOL-Thy FAILED (see also /home/bulwahn/.isabelle/./heaps/polyml-5.3.0_x86-linux/log/HOL-Thy) *** *** The error(s) above occurred in document antiquotation: "Base.index_ML" (line 130 of "~~/doc-src/IsarImplementation/Thy/Logic.thy") *** At command "text" (line 118 of "~~/doc-src/IsarImplementation/Thy/Logic.thy") *** Error: *** Type mismatch in type constraint. ***Value: Name_Space.declare : *** Context.generic -> *** bool -> binding -> Name_Space.T -> string * Name_Space.T ***Constraint: ***Proof.context -> ***bool -> ***Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T ***Reason: ***Can't unify Context.generic with Proof.context *** (Different type constructors) *** *** The error(s) above occurred in document antiquotation: "Base.index_ML" (line 1109 of "~~/doc-src/IsarImplementation/Thy/Prelim.thy") *** At command "text" (line 1089 of "~~/doc-src/IsarImplementation/Thy/Prelim.thy") Exception- TOPLEVEL_ERROR raised *** ML error make: *** [/home/bulwahn/.isabelle/./heaps/polyml-5.3.0_x86-linux/log/HOL-Thy.gz] Error 1 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Name for derived quotient_def theorem
Yes, "simps" should not be used for special purpose rules. Tobias Am 28/03/2012 09:22, schrieb Lukas Bulwahn: > Hi Florian, > > > Thank you for your suggestions. We will take them into account. > > On 03/28/2012 07:26 AM, Florian Haftmann wrote: >> http://isabelle.in.tum.de/reports/Isabelle/rev/861f53bd95fe#l1.53 >> the name given to the derived theorem is unsatisfactory. Since it is >> not a »code-only« theorem, it should not carry the »code« within. If it >> would be a »code-only« theorem, the convention is to suffix with >> »_code«, not »_code_eqn«. >> >> Also, for derived theorems proved by packages it is much more common to >> use qualification suffixes (e.g. ».simp«, ».intro«) rather than plumbing >> underscores (cf. module binding.ML). Btw. this also applies to the >> respectfulness theorem: ».rsp« would be better than »_rsp«. > > This is explained by looking at the history: The typedef package introduces > names with underscores, quotient_type and quotient_def inherit this from > typedef. > > Here a list of names we were thinking of while discussing: > > - abstract_eq > - abs_equation > - abs_def > - code_cert > - code_certificate > > In the end, we decided for the one you can see (although I am personally still > in favor of abs_equation or similar). > I think ".simp" is rather strange, because it is really not simplifying > anything, but rather unfolding the definition in some special way. > > > Lukas > ___ > 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] Name for derived quotient_def theorem
Hi Florian, Thank you for your suggestions. We will take them into account. On 03/28/2012 07:26 AM, Florian Haftmann wrote: http://isabelle.in.tum.de/reports/Isabelle/rev/861f53bd95fe#l1.53 the name given to the derived theorem is unsatisfactory. Since it is not a »code-only« theorem, it should not carry the »code« within. If it would be a »code-only« theorem, the convention is to suffix with »_code«, not »_code_eqn«. Also, for derived theorems proved by packages it is much more common to use qualification suffixes (e.g. ».simp«, ».intro«) rather than plumbing underscores (cf. module binding.ML). Btw. this also applies to the respectfulness theorem: ».rsp« would be better than »_rsp«. This is explained by looking at the history: The typedef package introduces names with underscores, quotient_type and quotient_def inherit this from typedef. Here a list of names we were thinking of while discussing: - abstract_eq - abs_equation - abs_def - code_cert - code_certificate In the end, we decided for the one you can see (although I am personally still in favor of abs_equation or similar). I think ".simp" is rather strange, because it is really not simplifying anything, but rather unfolding the definition in some special way. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
