Hi all! > The following is for my own home directory at TUM: > > .isabelle/etc/components -> > /home/wenzelm/isabelle/repos/Admin/contributed_components > .isabelle/contrib -> /home/isabelle/contrib > > This achieves the effect of versioned symlinks: the repository says > which directories to take from the physical file-system. This assumes > that the component name-version scheme in the file-system is really > authentic. In the past we have occasionally updated components without > bumping the version, but it might be not that critical after all.
this indeed works nice at TUM, but this requires that every developer
keep up-to-date his/her components on local machines for development,
and, as a prerequsite, to download them to his/her machine. This first
step already is not clear, or how would you obtain a HOL-Light bundle
without access to TUM NFS!?
So, this is my idea:
a) There is a canonical place at TUM where developers place their
components.
b) This should then also include jedit_build.
c) This place is accessible by HTTP.
d) Developers maintain Admin/contributed_components accordingly.
This burdens each developer to maintain local components accordingly
(even things like the HOL-Light bundle which will rarely affect common
development), but having a common base of components among all
developers (including mira) should be worth the effort, in times where
integration is increasing in importance.
This can be supported by populating Admin/ further, e.g. moving
e) Admin/contributed_components ~> Admin/etc/components
and then including Admin as component in your ~/.isabelle/etc/settings;
the same would be done by mira.
This does not even require a contrib dir in the Isabelle repository.
Common favorites like
if [[ -z "$ISABELLE_IDENTIFIER" ]]
then
ISABELLE_OUTPUT="$ISABELLE_HOME/heaps"
ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info"
fi
then could go to
f) Admin/etc/settings
providing more pre-configuration for developers.
It is good to have a description like
https://isabelle.in.tum.de/community/Working_with_the_repository_version_of_Isabelle
(again):
g) The results of this mail thread should go there.
Awaiting your response,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
