Ok, I understand now. Thanks for the clarification.

On 04/02/18 12:17, Thomas Tuerk wrote:
> No, that's not at all what I suggest and I would not work this way. All
> I say is that you can keep multiple source trees around without trouble.
> Use this how you see fit. You need to know what your needs are and
> choose an appropriate workflow. All I tried to do was point out some
> options. Relocation is another one, of course.
> I do the following, which fits my needs. Yours might be quite different:
> I only keep fixed versions needed for certain external (not in HOL
> examples dir) projects and a more or less up-to-date development version
> around. I do not tend to switch the symbolic link, just when switching
> projects, but select the HOL I want to use manually for every full
> rebuild. Only if I know I will mainly use a certain HOL version mostly
> for some time, I switch the default.
> I do updates directly on the development version and never had trouble,
> since it tends to take much less than 30 min on my machine (if I don't
> build many examples). I can easily schedule this for a time slot when I
> don't need HOL (e.g. lunch-time or during a meeting) and not be
> interrupted in my work. Even if I want to update while working with HOL,
> this is usually not an issue. While HOL rebuilds, I can continue working
> interactively on some proof, I just cannot restart or load additional
> theories / libs. This is for me usually not an issue for the about 5-10
> min it takes on my machine.
> Best
> Thomas

Attachment: signature.asc
Description: OpenPGP digital signature

Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
hol-info mailing list

Reply via email to