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