[isabelle-dev] isabelle components -a does nothing

[Makarius]

On Tue, 4 Sep 2012, Tjark Weber wrote:

> On Tue, 2012-09-04 at 18:09 +0200, Makarius wrote:
>> On Tue, 4 Sep 2012, Jasmin Blanchette wrote:
>>> Yes, I found out so much as soon as the web site was up. I was following
>>> the instructions from
>>>
>>> https://isabelle.in.tum.de/community/Working_with_the_repository_version_of_Isabelle
>>>
>>> one step at a time.
>>
>> You have been luck that Tjark updated it again recently.
>
> I realize that the wiki page is bound to become outdated again in the 
> future, and so it might be preferable to simply replace it with a 
> pointer to README_REPOSITORY. On the other hand, I find the latter 
> somewhat terse at the moment: it is a great reminder if one already 
> knows what to do, but IMHO not so easy to follow otherwise. Perhaps the 
> two could be merged in a pedagogically elegant way.

I know what you mean, but the "official" documents need to follow a more 
terse style.  There is also the problem that too much text is not read 
either, because people don't have time.  And the main purpose of 
README_REPOSITORY is not to say what is the fastest way to build from the 
Isabelle repository, but how to work with it professionally.

What is coming soon is another (probably even more terse) 
Admin/components/README that reminds the consumers and producers of 
components of the main ideas: like monotonicity of the component name 
space (authentic names that are are never re-used for other versions), and 
the official places where to put and to get the SHA1-identified archives.

The latter is still not 100% clear to me either: Mira still has some 
special configuration (with old contrib_devel and funny symlinks) that 
always requires a second round of tinkering.


 	Makarius