Re: [isabelle-dev] New HOL/Import
On Thu, Mar 29, 2012 at 8:04 PM, Makarius wrote: > Wow, I am impressed by the brevity of it. You should mention the secret > http://cl-informatik.uibk.ac.at/~cek/proofs which is a bzip stream to be > uncompressed, before it can be used with import_file in the example. That's the preprocessed proof image for importing basic hol-light. > You are no longer using any XML/YXML now. Is the format somehow related to > OpenTheory by Joe Hurd? No; the information stored is similar to the old format, but more brief and easier to parse: every line contains a next typ/term/thm to read, with arguments space separated and last uses of an object marked with a minus. It could be converted (possibly automatically) to OpenTheory; however the sharing is done at a different level so it would be hard to recover additional sharing and without it, Opentheory would be at least an order of magnitude bigger. >> - Does anyone have opinions about the HOL4 code that has been long dead? > Which HOL4 code do you mean exactly? The code currently in isabelle repository is in 3 places: Import, Import/HOL_Light and Import/HOL4 The Import/HOL_Light is functional but the proposed code replaces it. The Import/HOL4 has not been functional for a while, (I have not been able to use it even with proofs from 2004); should it still stay in the repository? Regards, Cezary ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] New HOL/Import
On Wed, 28 Mar 2012, Cezary Kaliszyk wrote: 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 You know the formalities for that: * Wiring in IsaMakefile for static part (ML etc), say with some conditional loading of actual HOL_Light proofs (that blob cannot be managed easily within the repository, so one can make a conditional test as for some other sessions, depending on settings that isatest/mira will provide.) * Canonical file headers with authors etc. * NEWS entry * CONTRIBUTORS entry replacing the old one. I am not adressing this here. It depends on who answers your initial question. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] New HOL/Import
On Wed, 28 Mar 2012, Cezary Kaliszyk wrote: - 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 Wow, I am impressed by the brevity of it. You should mention the secret http://cl-informatik.uibk.ac.at/~cek/proofs which is a bzip stream to be uncompressed, before it can be used with import_file in the example. You are no longer using any XML/YXML now. Is the format somehow related to OpenTheory by Joe Hurd? - Is anyone using the old HOL/Import? In principle you could ask on isabelle-users as well, although I would be surprised to hear about anybody using the old relic. It has sucked up maintenance resources for many years, without tangible results. - Does anyone have opinions about the HOL4 code that has been long dead? Which HOL4 code do you mean exactly? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JDK / Mira
On Thu, 29 Mar 2012, Lukas Bulwahn wrote: I restarted all mira daemons now. Lukas On 03/29/2012 09:53 AM, Florian Haftmann wrote: I guess someone must restart the mira deamons in order to run with the adjusted configurations. What I did independently the day before was to change ~isatest/.bashrc to include this global setting: export ISABELLE_JDK_HOME="$HOME/lib/jdk/jdk1.7.0_03" It means that any freshly started shell process should have a working ISABELLE_JDK_HOME local to isatest. It is a shame that we do not have proper versioning for private configuration of the isatest account, although some part of it is already in Admin/isatest in the Isabelle repository. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JDK / Mira
I restarted all mira daemons now. Lukas On 03/29/2012 09:53 AM, Florian Haftmann wrote: I guess someone must restart the mira deamons in order to run with the adjusted configurations. Florian ___ 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] JDK / Mira
I guess someone must restart the mira deamons in order to run with the adjusted configurations. 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 29/03/2012, at 4:31 PM, Tobias Nipkow wrote: > 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. As long as I don't have to do anything for each entry/exit, I'm easy. The list is controlled via the settings in the repository, so anyone in the group can add/remove people. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] JDK / Mira
I have * linked the existing OpenJDK 1.6 on macbroyXYZ to /home/isabelle/contrib_devel/jdk * and added one line to the mira default settings to set ISABELLE_JDK_HOME accordingly in order to provide and ad-hoc setup for the mira tests. I have no idea how platform-indepedent this symlink is, so this might still need improvement. Also a proper Sun JDK or maybe OpenJDK 1.7 should be provided. I don't now how far the prospective JDK-Component for Isabelle is, because it would turn this all obsolete. 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
