[isabelle-dev] isabelle components -a does nothing

[Makarius]

On Tue, 4 Sep 2012, Jasmin Christian Blanchette wrote:

> Am 04.09.2012 um 13:31 schrieb Jasmin Blanchette:
>
>> Going to
>>
>>    http://isabelle.in.tum.de/components/
>>
>> prints
>>
>>    Not Found
>>
>>    The requested URL /components/ was not found on this server.
>
> OK, the web site seems to be up now. Forget my email.

There is still something missing, as far as I can tell from your 
"components -l" printout before.

You need to init components from the Admin/components/* space explicitly 
to claim them, and the let "components -a" resolve them.  The general 
attitude is to provide various parts of the relevant information in the 
repository, but not force it on anybody by default (which would break many 
historic settings).

So you should add something like this to 
$ISABELLE_HOME_USERS/etc/settings:

       init_components "$HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"
       init_components "$HOME/.isabelle/contrib" "$ISABELLE_HOME/Admin/components/optional"

Then you can also remove most of your tum/official setup, and instead make 
sure that Admin/components/main reflects what you update there as 
component maintainer.


Pretty soon, I would like to make another refinement to the 
Admin/components vs. Admin/component_repository material, to have an 
Admin/components/README in the right place to explain the situation again 
for producers and consumers of components.

Hopefully we will then converge to a uniform understanding of these 
things, that subsumes all earlier attempts in that direction.  (I have 
already discontinued my own private component setup some weeks ago, 
because the new setup works already better than that.)


 	Makarius