[isabelle-dev] isabelle components -a does nothing

Jasmin Blanchette jasmin.blanchette at gmail.com
Tue Sep 4 18:05:01 CEST 2012


Hi Makarius,

> 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"

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.

Jasmin




More information about the isabelle-dev mailing list