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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
