Re: [isabelle-dev] Standard component setup (Re: NEWS)
On 01/05/2012 10:22 AM, Makarius wrote: I think one could publish ~isabelle/contrib_devel via HTTP, although it would require some clean up and tuning, say to expand symlinks. Another question is how to export the actual directory structure, without maintaining explicit index.html and tar.gz versions of everything. I had a look at this. There does not seem to be an apache extension that would let us publish a directory structure as a downloadable tarball. Also, the admins won't let us use the Apache autoindex facility, but they gave me a PHP script that does the same thing. So a low-tech suggestion with only minor overhead would be: * Components live in /home/isabelle/public_components as tarballs. The directory is regarded as append-only, possibly with infrequent garbage collection, which moves outdated packages to some archive location. The packages should be files, not symlinks (to make the directory more self-contained) I'll volunteer to provide the initial content based on contrib_devel and other sources, if people agree with the general idea. * The directory is accessible, cf. http://isabelle.in.tum.de/devel/components As the path indicates, this is mainly for developers. There could be a script in Admin/ that helps to bootstrap the local clone from this source. The more general question behind this is about an official Isabelle component repository, like major projects have it (Eclipse, Netbeans etc. even jEdit). But this needs substantial extra efforts to maintain. The above gives us a poor man's repository with several advantages over the current state - single place to look for stuff - uniform usage (download, untar, init_component, that's it.) Jasmin wrote: Could we instead provide a little script (or Isabelle tool) that turns a tarball/zip downloaded from upstream into a packaged Isabelle component? In the case of Yices and Vampire, the gain would be minimal: Without [...] Ok... let's forget about non-free stuff for now... Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Standard component setup (Re: NEWS)
On Sun, 8 Jan 2012, Alexander Krauss wrote: On 01/05/2012 12:19 PM, Jasmin Christian Blanchette wrote: We are not allowed to distribute Yices. When publishing the components, please exclude Yices. ... and Vampire. Could we instead provide a little script (or Isabelle tool) that turns a tarball/zip downloaded from upstream into a packaged Isabelle component? This would possibly lower the entry barrier for using these systems, and should be fine with the licenses. It can also save a little packaging work in the future. I've occasionally spent some thoughts on Z3 as well. MSR did not mind other distribution channels, but the user has to indicate his non-commercial status explicit, doing some awkward editing of the compinent settings. This could be somehow facilitated by allowing explicit interactive setup for components, say as Scala/JVM module that posts a dialog and asks the user to tick a license agreement before the settings are patched accordingly. Once that this concept is supported, one could easily include an adhoc download as well, say for retrieving Vampire from its official website. Anyway, there are so many other things that could be done to simplify deployment. I am not sure how much priority to apply to this painful non-free stuff right now. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Standard component setup (Re: NEWS)
Hi all, here my thoughts on the discussion: a) release candidates – the announcements of release candidates indeed could be a device for early feedback. The question is how to incite users to take them more seriously. b) development snapshots – I would prefer to get rid of them, providing clues how to make use of a repository revision instead. Taking Admin/contributed_components more seriously is a first step. Indeed, I have invented this in order to make mira run. So, a successful mira run tells that the tested revision can go along well with the components mentioned there. Maybe we should suggest for developers to include this list into ~/.isabelle/etc/settings similarly as mira does? This would require to provide a http download for the »current« components. Depends also on how »up to date« we want to require developers to be concerning components. c) non-free components – no idea at the moment d) add-ons not being formal components – at the moment ghc. I always considered re-packing or wrapping this as overkill. Any further thoughts on 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] Standard component setup (Re: NEWS)
Quoting Alexander Krauss kra...@in.tum.de: However, some components do not come with the release (vampire, yices, jedit_build). Should we simply have a directory at TUM which is served via http and where developers can get components? Maybe simply serve /home/isabelle/contrib_devel for that (For jedit_build this should be unproblematic, but I am not sure about the licensing situation for the other stuff.) We are not allowed to distribute Yices. When publishing the components, please exclude Yices. Cheers, Sascha ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
