Re: [isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
On Sun, 15 Jul 2012, Alexander Krauss wrote: To add a new component/version: - copy the tarball to /home/isabelle/components - in some clone of the repository, run Admin/component_repository/checksum -u - check the result with hg diff (the checksum of the new file should be added to the diff) - commit and push the result Now the following tarballs are still missing: * scala-2.9.2 * ProofGeneral-4.1 * jdk-6u31 I have now added these and some more components in Isabelle/30b9a435ee04 and Isabelle/59bc6374c121. As /home/isabelle/components is shared between various users without any specific mechanisms, we will run into the standard problems of Unix permissions over time. The directory /home/isabelle/components/TRASH already contains some old material that only the owners (presently haftmann, krauss) or root can delete. 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
Am 09.07.2012 um 22:48 schrieb Alexander Krauss: So consider this a call for official components. Currently we are missing at least the following (from Admin/components as of 92c0addc): contrib/cvc3-2.2 contrib/e-1.5 contrib/kodkodi-1.2.16 contrib/spass-3.8ds contrib/scala-2.9.2 contrib/vampire-1.0 contrib/yices-1.0.28 contrib/z3-3.2 contrib/ProofGeneral-4.1 contrib/jdk-6u31 What is an official component? Among the Nitpick/Sledgehammer/SMT components, vampire-1.0 and yices-1.0.28 are not to be redistributed (due to their license) and have never been part of an official Isabelle release. (Sascha and I do use them for evaluations, though.) For the others, please use cvc3-2.4.1 (from http://www21.in.tum.de/~blanchet/cvc3-2.4.1.tar.gz) e-1.5 kodkodi-1.2.16 spass-3.8ds z3-4.0 (from http://www21.in.tum.de/~blanchet/z3-4.0.tar.gz) Jasmin ___ 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
I have consolidated the story further: * central hook Admin/init_components does not use platform-specific component files any longer but relies on good old universal components * mira uses this hook (after the next crash of the daemon and the following implicit restart) @Gerwin: maybe you could consider adjusting isatest accordingly: * use /home/isabelle/contrib instead of /home/isabelle/contrib_devel * use Admin/init_components appropriately I personally do not dare to touch this ancient sanctuary of Elder Days. 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] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
On Thu, 5 Jul 2012, Florian Haftmann wrote: @Gerwin: maybe you could consider adjusting isatest accordingly: * use /home/isabelle/contrib instead of /home/isabelle/contrib_devel * use Admin/init_components appropriately I have also started thinking about the full inclusion of Admin/init_components into isatest, but my tendency was not to do it for now. In the past we occasionally had a situation where things depending on certain non-default or non-free components ended up in the basic Isabelle/HOL libraries, and isatest would rightly reject that. 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 Sun, 1 Jul 2012, Alexander Krauss wrote: So here is my latest low-tech proposal: * /home/isabelle/components is the components repository, where all components are stored. They are stored as tarballs. * The existing php script can be used to serve this directory via HTTP. * Non-free components are marked as such simply via file permissions, i.e., by having the world-readable flag unset. Since Apache runs under group isabelle, we might have to set the group to something else (e.g., an imagined isabelle-admin). * Integrity of this directory is ensured by a cron job which compares the output of sha1sum /home/isabelle/components/* with a file in the Admin section of the Isabelle repository. So we can easily detect accidents (and revert them, possibly with the help of the standard backups). Such a script is easy to write, and I already have some fragments lying around here. * /home/isabelle/contrib is maintained automatically by unpacking the contents of the tarballs (and setting permissions properly). * A similar script in Admin/ can download components via HTTP and link them into a clone of the Isabelle repository. I would say that 30 lines of bash will do. And additional 30 lines of a README, which goes into the same directory. This is now converging to a very reasonable scheme. I also prefer to archive official .tar.gz now, since permissions of individual files in the file-system are often mangled. (There was another incident just last week.) BTW, when there is a robust script to download .tar.gz components on demand and unpack them for the user, we could even discontinue the /home/isabelle/contrib/ thing -- /home/tmp/USER provides cheap temporary disk space for private copies of it, also for mira and isatest. Most regular users are non-local anyway, using their laptop etc. 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 Fri, 29 Jun 2012, Alexander Krauss wrote: So here is another implementation alternative for all this: - This assumes universal components. - Instead of Admin/components as a file with references, there is a hg repository (using the largefiles extension), which evolves along with Isabelle and always contains exactly the components that would now be mentioned in Admin/components. - The Isabelle repository contains a file with the hash of the matching revision in the component repository, which serves as a formal link. - Thus, to get a fully working installation for a given Isabelle revision, it is enough to update the component repository to the matching revision, which will automatically download the relevant files. This appears to be an application of largefiles + subrepositories, i.e. two features of last resort in the Mercurial terminology. Moreover, I am not sure if Mercurial 2.0+ can really be assumed to be available everywhere. My Debian stable installation still has 1.6.4. Currently, Isabelle development works just fine even with very old Mercurial. I was also aware of that problem when mentioning largefiles. It means that I would have to upgrade to Ubuntu 12.04 LTS now, but officially the LTS - LTS transition only starts with the first point release in a few weeks. IIRC, the isabelle.in.tum.de server infrastructure is also using an older Mercurial. 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
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. See http://isabelle.in.tum.de/reports/Isabelle/rev/1bee47c0c278 for the current situation. I'm still not sure how to deal with the non-free components. Have one components file and one components-optional? Btw. is the universal JDK component freely distributable? In that case I will tar it to the official store http://isabelle.in.tum.de/devel/components/ In the next iteration I want to adjust mira handle components via the existing scriptlet in Admin. 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] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
On Thu, 28 Jun 2012, Tjark Weber wrote: Directories would be more amenable to version control than tarballs, if that makes a difference. These are build artifacts, not sources, so SCM a la Mercurial is a conceptual mismatch: There is no real notion of change (just monotonic addition of new components), no diffs, no merges etc. On 06/28/2012 09:54 PM, Makarius wrote: Proper versioning (with Mercurial) would solve several problems: * canonical identification of *the* true content of component repository * Unix permissions done right in shared space * built-in ssh/http pull I looked briefly at Mercurial's largefiles extension, but I don't think it is suitable: The extension helps in situations when the repository history consumes significantly more space than the working directory due to large binaries that are part of previous revisions but not the current ones, since they were changed or removed. Since our component store grows monotonically, there is no benefit from largefiles, since the size of the tip revision basically equals the size of the whole repository. In practice, this means that a pull would be cheap, but an update would be prohibitively expensive. The above assumes that we simply try to manage the flat directory as a hg repository. Trying to capture the evolution of components (i.e., different versions) does not really make sense, since each component evolves completely independently, and it would not be clear what a given revision of the component repository would mean. All this is just the conceptual difference between a source code repository such as Mercurial and build artifact repositories such as Sonatype Nexus or Artifactory. These basically implement a monotonic file store (plus integration with certain build frameworks which is quite irrelevant for us). 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
Hi Alex, These are build artifacts, not sources, so SCM a la Mercurial is a conceptual mismatch: There is no real notion of change (just monotonic addition of new components), no diffs, no merges etc. There is a conceptual mismatch, but even forgetting about third-party components most Mercurial repositories have some files that don't really change or change monotonically. As an example, there's plenty of open-source software that has separate NEWS.xxx files for different versions xxx and one would normally just monotonically add new files. Hence, SCM users are familiar with the situation and still prefer it to having to deal with an entirely different system (at least on a small scale). I looked briefly at Mercurial's largefiles extension, but I don't think it is suitable: The extension helps in situations when the repository history consumes significantly more space than the working directory due to large binaries that are part of previous revisions but not the current ones, since they were changed or removed. Since our component store grows monotonically, The way I see it, obsolete components should be removed, so as to minimize confusion. When E-1.5 appears, we should remove E-1.4, since it's obsoleted. Just like Metis in Isabelle2012 obsoletes Metis in Isabelle2011 and there's no way to use the old Metis with the new Isabelle. And E-1.0 to E-1.3 should have been removed a long time ago. For good reasons; as an example recent repository versions of Isabelle require SPASS 3.8ds or better, even though it was released only a few months ago. there is no benefit from largefiles, since the size of the tip revision basically equals the size of the whole repository. In practice, this means that a pull would be cheap, but an update would be prohibitively expensive. I'm not sure I'm following this part about pull vs. update. Sure, the components are really big and should arguably live in a different Mercurial repository than Isabelle, but how is pull vs. update more expensive than copying files around using scp? The above assumes that we simply try to manage the flat directory as a hg repository. Trying to capture the evolution of components (i.e., different versions) does not really make sense, since each component evolves completely independently, and it would not be clear what a given revision of the component repository would mean. Yes, I agree with you here. All this is just the conceptual difference between a source code repository such as Mercurial and build artifact repositories such as Sonatype Nexus or Artifactory. These basically implement a monotonic file store (plus integration with certain build frameworks which is quite irrelevant for us). How easy are these to use? Are they worth learning in addition to Mercurial? What are the arguments in favor of a monotonic store as opposed to removing obsoleted components? Jasmin ___ 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/29/2012 12:27 AM, Jasmin Christian Blanchette wrote: Since our component store grows monotonically, The way I see it, obsolete components should be removed, so as to minimize confusion. No reason for confusion here, since Admin/components tells you what you need (and I am assuming there is a little script that will download it for you if you are not sitting on NFS). Removing obsolete (wrt. to what? The repository tip? The latest release?) versions raises the question of how to easily retrieve the matching revisions for older Isabelle versions. There must be a formal link to the matching revision in the component repository. So here is another implementation alternative for all this: - This assumes universal components. - Instead of Admin/components as a file with references, there is a hg repository (using the largefiles extension), which evolves along with Isabelle and always contains exactly the components that would now be mentioned in Admin/components. - The Isabelle repository contains a file with the hash of the matching revision in the component repository, which serves as a formal link. - Thus, to get a fully working installation for a given Isabelle revision, it is enough to update the component repository to the matching revision, which will automatically download the relevant files. This looks pretty much equivalent to the other proposed solutions, at least at this late hour. But it needs some testing with real data to get some experience with the largefile extension. Moreover, I am not sure if Mercurial 2.0+ can really be assumed to be available everywhere. My Debian stable installation still has 1.6.4. Currently, Isabelle development works just fine even with very old Mercurial. there is no benefit from largefiles, since the size of the tip revision basically equals the size of the whole repository. In practice, this means that a pull would be cheap, but an update would be prohibitively expensive. I'm not sure I'm following this part about pull vs. update. Sure, the components are really big and should arguably live in a different Mercurial repository than Isabelle, but how is pull vs. update more expensive than copying files around using scp? This was assuming that we do not remove old components. All this is just the conceptual difference between a source code repository such as Mercurial and build artifact repositories such as Sonatype Nexus or Artifactory. These basically implement a monotonic file store (plus integration with certain build frameworks which is quite irrelevant for us). How easy are these to use? Are they worth learning in addition to Mercurial? They are easy to use, since there are not many ways how we would use them: Component upload can be done via a web interface, and download is via http, following some path conventions. Not sure about installation and maintenance. They do impose some conventions and strange terminology on you though, which come from the Maven way of organizing stuff. What are the arguments in favor of a monotonic store as opposed to removing obsoleted components? Well, in the end these are different implementations of the same thing, so the question is which one is simpler to use and maintain in the end... I don't know. 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 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
Re: [isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
Tiny instructions on changesets c97656ff4154 ff.:
* include the following snippet into your ~/.isabelle/etc/settings:
source ${ISABELLE_HOME}/Admin/init_components
* obtain components from Isabelle2012, http://isabelle.in.tum.de/dist or
nfsbroy:/home/isabelle/contrib; hints which components are still missing
can be obtained by a simple isabelle call (e.g. `isabelle getenv)
* try whether it works, e.g.
isabelle jedit -bf
This is just a first start and required further thought:
* Will the idea of platform-universal components revived? If yes, the
platform-sensitive components files can be discontinued. I personally
like the idea, though?
* How to deal with the non-free components? Once a solution is found
there, components can be required strictly, not liberal.
* Use this mechnisms uniformly in mira and isatest.
* Cleanup and maintainance of nfsbroy:/home/isabelle/contrib
* Should Admin/ become a component in itself?
* …
Happy hacking,
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] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
Dear Florian,
I noticed that the following components are required (due to
Admin/components)
cvc3-2.2
e-1.5
hol-light-bundle-0.5-126
kodkodi-1.2.16
spass-3.8ds
scala-2.9.2
vampire-1.0
yices-1.0.28
z3-3.2
jedit_build-20120414
of which
e-1.5 (instead there is e-1.4)
hol-light-bundle-0.5-126
vampire-1.0
yices-1.0.28
jedit_build-20120414
are not available from http://isabelle.in.tum.de/dist (of those, at
least jedit_build should be not non-free, I guess).
cheers
chris
On 06/27/2012 05:46 AM, Florian Haftmann wrote:
Tiny instructions on changesets c97656ff4154 ff.:
* include the following snippet into your ~/.isabelle/etc/settings:
source ${ISABELLE_HOME}/Admin/init_components
* obtain components from Isabelle2012, http://isabelle.in.tum.de/dist or
nfsbroy:/home/isabelle/contrib; hints which components are still missing
can be obtained by a simple isabelle call (e.g. `isabelle getenv)
* try whether it works, e.g.
isabelle jedit -bf
This is just a first start and required further thought:
* Will the idea of platform-universal components revived? If yes, the
platform-sensitive components files can be discontinued. I personally
like the idea, though?
* How to deal with the non-free components? Once a solution is found
there, components can be required strictly, not liberal.
* Use this mechnisms uniformly in mira and isatest.
* Cleanup and maintainance of nfsbroy:/home/isabelle/contrib
* Should Admin/ become a component in itself?
* …
Happy hacking,
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] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
On 06/16/2012 02:11 PM, Jasmin Christian Blanchette wrote: a) Subdirectories for each platform /home/isabelle/contrib/ x86-linux/ x86_64-linux/ x86-cygwin/ ... Then, the universal component packages must be copied, symlinked or hardlinked. b) Different packages for different platforms, roughly as it is now... /home/isabelle/contrib/ jdk-6u31_x86_64-linux/ jdk-6u31_x86-linux/ Then we need a /Admin/contributed_components file for each platform, which lists the components relevant for that platform. I would prefer both indeed: a) architecture-sensitive organisation, but with universal components directly under contrib (as is the case now) b) separate component files for different platforms I'm a bit puzzled here. What does preferring both means exactly? And why does point (a) talk about universal components, when you wrote that the time of platform-universal components is gone? What are the precise implications for the (universal) components I'm packaging (Kodkodi, CVC3, E, SPASS, Z3)? the time is gone just means that we can no longer assume that every component is platform-universal. You can continue building universal components, and I would say this is still the preferred way wherever it can be done with reasonable effort. @Florian: so your suggestion would be that there are several components files in Admin, say Admin/contributed_components_x86-linux containing contrib/x86-linux/jdx-6u31-x86_linux contrib/e-1.5 ... Then the extra path component is redundant, and I think I would rather go without it, since the risk of confusion is high, since the invariant is easy to violate. The directories-for-platforms convention also breaks down when, say, some component is universal accross linux and macos, but needs a special case for cygwin. Where would you put this then? I now realized that having separate component files has the advantage that you can easily make a single installation can be used from different platform without changing symlinks. I think this is important enough to not consider variant a) further. So I think I now prefer a flat directory as component repository, and a component file for each platform. 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
@Florian: so your suggestion would be that there are several components files in Admin, say Admin/contributed_components_x86-linux containing contrib/x86-linux/jdx-6u31-x86_linux contrib/e-1.5 ... Then the extra path component is redundant, and I think I would rather go without it, since the risk of confusion is high, since the invariant is easy to violate. The directories-for-platforms convention also breaks down when, say, some component is universal accross linux and macos, but needs a special case for cygwin. Where would you put this then? I now realized that having separate component files has the advantage that you can easily make a single installation can be used from different platform without changing symlinks. I think this is important enough to not consider variant a) further. So I think I now prefer a flat directory as component repository, and a component file for each platform. I have also come to that conclusion, yes. As a variant, I could also think of something like Admin/etc/components.x86-linux … Admin/etc/components.whatever-platform with or without a generic Admin/etc/components Whether the component mechanism handles platform suffixes implicitly or not is yet another matter of detail. 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] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
On 05/30/2012 02:44 PM, Makarius wrote: On Wed, 30 May 2012, Lukas Bulwahn wrote: On 05/29/2012 02:01 PM, Makarius wrote: * Admin/contributed_components within the repository documents semi-formally which components may be included into a certain version. The mira experts should be able to say more about the current used of that file in the testing framework. Roaring ahead with the grand unified contrib, I guess someone has changed the Scala version on lxbroy10, because now the Scala export with Imperative-HOL fails on lxbroy10. The interesting bit of information is actually here: http://isabelle.in.tum.de/reports/Isabelle/report/78fa8d673aac4dcca02465b91815adb9#l260 env: /tmp/mira/workbench/62527-140537428690688/Isabelle/contrib/scala-2.9.2/bin/scalac: Permission denied Which was caused by the lack of group executablity for the scala/bin files, which I have changed now. Thank you for digging deeper into this. So the mira testing should be now back to a working state. Lukas ___ 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
Hi all! The following is for my own home directory at TUM: .isabelle/etc/components - /home/wenzelm/isabelle/repos/Admin/contributed_components .isabelle/contrib - /home/isabelle/contrib This achieves the effect of versioned symlinks: the repository says which directories to take from the physical file-system. This assumes that the component name-version scheme in the file-system is really authentic. In the past we have occasionally updated components without bumping the version, but it might be not that critical after all. this indeed works nice at TUM, but this requires that every developer keep up-to-date his/her components on local machines for development, and, as a prerequsite, to download them to his/her machine. This first step already is not clear, or how would you obtain a HOL-Light bundle without access to TUM NFS!? So, this is my idea: a) There is a canonical place at TUM where developers place their components. b) This should then also include jedit_build. c) This place is accessible by HTTP. d) Developers maintain Admin/contributed_components accordingly. This burdens each developer to maintain local components accordingly (even things like the HOL-Light bundle which will rarely affect common development), but having a common base of components among all developers (including mira) should be worth the effort, in times where integration is increasing in importance. This can be supported by populating Admin/ further, e.g. moving e) Admin/contributed_components ~ Admin/etc/components and then including Admin as component in your ~/.isabelle/etc/settings; the same would be done by mira. This does not even require a contrib dir in the Isabelle repository. Common favorites like if [[ -z $ISABELLE_IDENTIFIER ]] then ISABELLE_OUTPUT=$ISABELLE_HOME/heaps ISABELLE_BROWSER_INFO=$ISABELLE_HOME/browser_info fi then could go to f) Admin/etc/settings providing more pre-configuration for developers. It is good to have a description like https://isabelle.in.tum.de/community/Working_with_the_repository_version_of_Isabelle (again): g) The results of this mail thread should go there. Awaiting your response, 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] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
I first intended to do the same as for Isabelle2011-1, but then realized that Isabelle2012 had diverged further from the old universal scheme of add-on packages: more and more components are specific for one of the platform families (linux, darwin, cygwin), and would have required some extra fiddling to put them all into one place and activate uniformly. This nukes the ancient idea of ~isabelle/contrib that you would just link it into your repository at TUM, regardless on which machine you are operating, and would get the best which has been achieved for that particular platform (whether the mechanism behind this are symlinks or Admin/contributed_components does not matter). I. e. if you have both jdk-6u31_x86_64-linux jdk-6u31_x86-linux you have to include either one by default, effectively restricting yourself to x86 or x86_32. Would it be impossible to provide those twins under one roof? Or is this distinction since they are not shipped both in one download bundle (as guess, I have not checked this)? 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] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
On Wed, 30 May 2012, Florian Haftmann wrote: a) There is a canonical place at TUM where developers place their components. b) This should then also include jedit_build. c) This place is accessible by HTTP. A simple script using wget in Admin/ could further lift the burden of hand work by automatically downloading all missing components. This now sounds like a fully managed component repository for Isabelle, even in arbitrary intermediate stages between releases, but we do not even have a formal process yet for the components that are bundled with official releases. I am still used to sort it out individually with people who feel partly or fully responsible for some of the parts that make up the bundles. The result can then be looted to be used for repository versions as well, but that is a partial thing. My own repository clones are hardly ever run with more than half of the components of an official release bundle, it is just too much work to configure that. Maybe we can first try to get the mira setup formalized, and make it as plain and simple as possible. It is local at TUM and a privileged user isatest:isabelle, which simplifies many things. We should also try to get rid of implicit things in the shared file system, such as links that point to latest versions without actual version control. That was from the old contrib symlink scheme for stable releases, but the stable releases now have explicit version identifiers for the components (except for polyml -- the very last special case). 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, 30 May 2012, Florian Haftmann wrote: This can be supported by populating Admin/ further, e.g. moving When going through it for the release, my impulse was to de-populate it, or rather sort out things more explicitly. A bit too much misc admin stuff has accumulated there. When we understand better what is what, and what for, we can hopefully remove a few things from Admin and clarify a few others like e) Admin/contributed_components ~ Admin/etc/components Common favorites like if [[ -z $ISABELLE_IDENTIFIER ]] then ISABELLE_OUTPUT=$ISABELLE_HOME/heaps ISABELLE_BROWSER_INFO=$ISABELLE_HOME/browser_info fi then could go to f) Admin/etc/settings I didn't know that this is still a favourite. I've discontinued this scheme when we stopped using cvs. Settings give a lot of freedom, but that should be exercised privately. It is good to have a description like https://isabelle.in.tum.de/community/Working_with_the_repository_version_of_Isabelle (again): g) The results of this mail thread should go there. I count this as part of the administrative chaos. I welcome a genuine community effort happening there, and hope it will eventually get really started, but I am myself not participating. In particular, dependable admin stuff needs to go to some official place. Using Mediawiki as some kind of rationale store or issue tracker is a bit strange. If such things should be formalized (and mechanized) one needs to invest some time to find the proper tools for it, or one of the many existing hosting platforms for such things. 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, 30 May 2012, Florian Haftmann wrote: This nukes the ancient idea of ~isabelle/contrib that you would just link it into your repository at TUM, regardless on which machine you are operating, and would get the best which has been achieved for that particular platform (whether the mechanism behind this are symlinks or Admin/contributed_components does not matter). I. e. if you have both jdk-6u31_x86_64-linux jdk-6u31_x86-linux you have to include either one by default, effectively restricting yourself to x86 or x86_32. Would it be impossible to provide those twins under one roof? Or is this distinction since they are not shipped both in one download bundle (as guess, I have not checked this)? I realized after the Isabelle2012 release that the old contrib idea was dead. When assembling the special platform bundles, I did remember that it was done differently before, but was unsure how much of it was still relevant. As the bundled distribution gets more and more sophisticated for the end-user, the situation for non-releases gets more difficult. The gap is widening with every release. Not every component is equal in that sense, though. Especially JDK, Poly/ML, jedit_build are all somehow special. I don't see any problems providing sliding versions of jedit_build components, and ~isabelle/contrib might have an almost complete history of them already. For Poly/ML the traditional scheme is to copy manually from the last stable Isabelle release. It often needs to be changed in testing anyway. For JDK I am still experimenting. Right after the release I have started to make a more universal Linux JDK 1.7 for both x86 and x86_64, at the cost of 150 MB extra disk space. (Surprisingly many Linux users get the wrong download by default, even with our smart download button now.) JDK 1.7 for Mac OS X is still an open problem. There are reasons to believe that I can unify it with Linux before the next release. JDK 1.7 for Windows is no problem, it is its own world anyway -- which is actually a problem for the testing, but that is a completely different story. 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 Sun, 27 May 2012, Florian Haftmann wrote: for years now, there was a silent convention that ~isabelle/contrib_devel at the TUM NFS would contain references to more-or-less up-to-date add-on components for Isabelle. Is there currently anybody still doing maintainance there? Also, the local Isabelle2012 distribution in ~isabelle/Isabelle2012 is not equipped with any of the add-on components shipped with the distribution on the website, e.g. there seems to be no readily usable Haskabelle2012 beneath ~isabelle. What are users of Isabelle at the local TUM infrastructure (e.g. remote runs on the macbroyXY machines) supposed to do? Private installations? Further, how to include the add-on components? Currently I use special ~/.isabelle/etc/settings for this, but maybe there is something more direct? After all those years, I think we should agree upon (again) how we (i.e. all those using Isabelle from TUM NFS) deal with all those issues. For such central issues I don't believe in private-only solutions. Or does meanwhile everybody use the testboard? On Mon, 28 May 2012, Jasmin Christian Blanchette wrote: A first step would be that the add-on components shipped with the current distribution are also available by NFS. I'm surprised they were taken out. They used to be there for Isabelle2011-1. I first intended to do the same as for Isabelle2011-1, but then realized that Isabelle2012 had diverged further from the old universal scheme of add-on packages: more and more components are specific for one of the platform families (linux, darwin, cygwin), and would have required some extra fiddling to put them all into one place and activate uniformly. Moreover, my impression was that the role of the different contrib directories needs some rethinking anyway, which is what we are doing right now on this thread. There has always been a bit of chaos here, without grand-unified structure. It does not mean we should not try again to get one. Taking the current situation as a starting point, one could do the following: * /home/isabelle/contrib contains various add-on components cumulatively with explicit version information and without funny symlinks to other versions. * /home/isabelle/contrib_devel is discontinued, it is superseded by a cleaned version of contrib above; right now there is a symlink contrib - contrib_devel anyway. * Admin/contributed_components within the repository documents semi-formally which components may be included into a certain version. The mira experts should be able to say more about the current used of that file in the testing framework. We shall also need to make an effort to keep /home/isabelle/contrib up-to-date. There is quite some divergence wrt. Isabelle2011-1 and Isabelle2012 right now. 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
Hi Florian, Am 27.05.2012 um 20:25 schrieb Florian Haftmann: for years now, there was a silent convention that ~isabelle/contrib_devel at the TUM NFS would contain references to more-or-less up-to-date add-on components for Isabelle. Is there currently anybody still doing maintainance there? ls -l reveals that blanchet, krauss, and wenzelm have been active there lately. Or does meanwhile everybody use the testboard? That seems to be the trend, but we all need a backup for when testboard is down. A first step would be that the add-on components shipped with the current distribution are also available by NFS. I'm surprised they were taken out. They used to be there for Isabelle2011-1. Cheers, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
Hi all, for years now, there was a silent convention that ~isabelle/contrib_devel at the TUM NFS would contain references to more-or-less up-to-date add-on components for Isabelle. Is there currently anybody still doing maintainance there? Also, the local Isabelle2012 distribution in ~isabelle/Isabelle2012 is not equipped with any of the add-on components shipped with the distribution on the website, e.g. there seems to be no readily usable Haskabelle2012 beneath ~isabelle. What are users of Isabelle at the local TUM infrastructure (e.g. remote runs on the macbroyXY machines) supposed to do? Private installations? Further, how to include the add-on components? Currently I use special ~/.isabelle/etc/settings for this, but maybe there is something more direct? After all those years, I think we should agree upon (again) how we (i.e. all those using Isabelle from TUM NFS) deal with all those issues. For such central issues I don't believe in private-only solutions. Or does meanwhile everybody use the testboard? A first step would be that the add-on components shipped with the current distribution are also available by NFS. 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
