Re: [isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
On Tue, 26 Jun 2012, Florian Haftmann wrote: * Will the idea of platform-universal components revived? If yes, the platform-sensitive components files can be discontinued. I personally like the idea, though? You are doing this in Isabelle/f06697f776b0 with ML_PLATFORM, but this is way has been long obsolete. Many years ago, the ML system was the only platform specific thing, and its platform identifier was re-used for some time for other add on tools. Around 2009/2010 I've revised this scheme, as explained in Admin/PLATFORMS. But that is already outdated again, and I will have to revise it once more based on the experience that I've gained together with Jasmin for Isabelle2011-1 and Isabelle2012. The problem is that modern operating systems suffer from a multi-personality problem. There is not the platform that you are running on, but every framework might have its own platform: ML, JVM, the settings environment (e.g. native windows vs. cygwin), certain tools. So our classic universal component idea was already right, because it is then up to the component settings to work out the details of the platform. * How to deal with the non-free components? Once a solution is found there, components can be required strictly, not liberal. * Cleanup and maintainance of nfsbroy:/home/isabelle/contrib We now have several component directories, which is the real one? /home/isabelle/contrib#haftmann /home/isabelle/contrib_devel #haftmann /home/isabelle/public_components #krauss /home/isabelle/website-Isabelle2012/dist/contrib #wenzelm (official release) If the naming scheme for components is taken with care, we should be able to have just /home/isabelle/contrib with monotonic addition of new versions as they emerge. (Overwriting with same name only for equivalent components; otherwise by adding funny -1, -2, -3 suffixes for the different builds, only where this is really needed.) The isatest/mira jobs would project from that single store via Admin/components Official releases project via copying the distributed components. A pulished version of /home/isabelle/contrib (via http) would suppress certain things that are specified in some file as nonfree. Once we know where *the* component store is, I will put a universal JVM 1.6 there. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
* Will the idea of platform-universal components revived? If yes, the platform-sensitive components files can be discontinued. I personally like the idea, though? The problem is that modern operating systems suffer from a multi-personality problem. There is not the platform that you are running on, but every framework might have its own platform: ML, JVM, the settings environment (e.g. native windows vs. cygwin), certain tools. So our classic universal component idea was already right, because it is then up to the component settings to work out the details of the platform. OK, once the universal Java is there, this disjunctive switch can be discontinued. Fine. * Cleanup and maintainance of nfsbroy:/home/isabelle/contrib We now have several component directories, which is the real one? /home/isabelle/contrib #haftmann /home/isabelle/contrib_devel #haftmann /home/isabelle/public_components #krauss /home/isabelle/website-Isabelle2012/dist/contrib #wenzelm (official release) »/home/isabelle/contrib« is supposed to be »the« place finally, which is very likely to be a superset of »/home/isabelle/website-Isabelle/dist/contrib«. »/home/isabelle/contrib_devel« will stay until mira and isatest are migrated to use Admin/components. Not sure what the status of »/home/isabelle/public_components« is. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
On Tue, 2012-06-26 at 22:46 +0200, Florian Haftmann wrote: Tiny instructions on changesets c97656ff4154 ff.: [...] The Isabelle Wiki has a HOWTO on Working with the repository version of Isabelle (at https://isabelle.in.tum.de/community/Working_with_the_repository_version_of_Isabelle). Perhaps you could update the section on Initializing auxiliary components? Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
On Wed, 27 Jun 2012, Florian Haftmann wrote: »/home/isabelle/contrib« is supposed to be »the« place finally We need a chmod g+w here for the main directory here. For each component directory, I would say the owner with full permissions is also the maintainer. Since this is not under version control, the usual problems with Unix permissions etc. are to be anticipated. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
On 06/27/2012 02:03 PM, Makarius wrote: On Wed, 27 Jun 2012, Florian Haftmann wrote: Not sure what the status of »/home/isabelle/public_components« is. See also this thread on the same topic: http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg02157.html /home/isabelle/public_components was my (incomplete) attempt to solve the remote distribution problem, while /home/isabelle/contrib now solves the local distribution problem. Currently the difference is that public_components contains tarballs (not suitable for in-place use), whereas contrib contains directories (not suitable for download via HTTP/wget: slow, and file permissions would get lost). I think we actually need to keep the content in both formats, but one directory should be automatically generated from the other. Which one should be the master? Intuitively, I like the mindset 1 component = 1 package = 1 tarball, but regarding the directories as the master and using tarballs as a mere distribution mechanism is equally valid IMO. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
On Wed, 27 Jun 2012, Makarius wrote: Once we know where *the* component store is, I will put a universal JVM 1.6 there. See now changeset: 48162:5717466d4633 tag: tip user:wenzelm date:Wed Jun 27 17:52:07 2012 +0200 files: Admin/components description: added universal jdk-6u31 as standard component; The following is also relevant for ProofGeneral users: changeset: 48161:3fd1bccb0834 user:wenzelm date:Wed Jun 27 17:51:06 2012 +0200 files: Admin/components description: added ProofGeneral-4.1 as standard component, which allows to discontinue special choosefrom magic eventually; It means ProofGeneral-4.1 will be there by default, if Florian's way to init the components for repository versions is used. So after sufficiently many people have picked up that scheme, the old guess mode via choosefrom can be discontinued. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
On Wed, 27 Jun 2012, Alexander Krauss wrote: Currently the difference is that public_components contains tarballs (not suitable for in-place use), whereas contrib contains directories (not suitable for download via HTTP/wget: slow, and file permissions would get lost). I think we actually need to keep the content in both formats, but one directory should be automatically generated from the other. Which one should be the master? Intuitively, I like the mindset 1 component = 1 package = 1 tarball, but regarding the directories as the master and using tarballs as a mere distribution mechanism is equally valid IMO. Good question. Right now I have the master tar.gz files in my home somewhere, and then publish them as unpacked directories in /home/isabelle/contrib/. The answer also depends on the HTTP technology. E.g. on CTAN you see plain directory views by default, and then can ask to download zip etc. which might be dynamically generated on the spot, or just taken statically from somewhere in the backhand. Another example is hg, where the archived formats can be requested dynamically, somehow in Python. The open directory layout might have a slight advantage here, because we could put etc/nonfree files into each nonfree package, and the HTTP service script we observe that accordingly. A disadvantage is that file attributes in a file system are less reliably maintained than in a shelved tar.gz. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
