[isabelle-dev] isabelle components -a does nothing
makarius at sketis.net
Tue Sep 4 17:37:21 CEST 2012
On Tue, 4 Sep 2012, Jasmin Christian Blanchette wrote:
> Am 04.09.2012 um 13:31 schrieb Jasmin Blanchette:
>> Going to
>> 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
So you should add something like this to
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
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.)
More information about the isabelle-dev