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
On 04.02.2018 19:03, Mario Xerxes Castelán Castro wrote:
> If I understand correctly, your overall suggestion is
>
> * Have a symbolic link S that points to either A or B, where A and B are
> HOL4 source+build trees. My Emacs init file should point to hol-mode
> within S.
>
> * If I am working, and S points to A, then update and re-build B
> (vice-versa if S points to B). Switch S to point to B when convenient
> (now the roles of A and B are swapped).
>
> Is this correct?
>
> Thanks.
>
> On 04/02/18 11:56, Thomas Tuerk wrote:
>> Hi,
>>
>> for this workflow, you don't need to change the absolute location. You
>> can just choose which of the multiple installed HOL versions to use.
>> Keep the installation in the same place and just choose which one to use
>> when. The only trouble with this is that you have to rebuild your own
>> development manually and completely to switch versions. This usually
>> happens and is advisable anyhow.
>>
>> So, I do the following:
>>
>> Have multiple HOL directories around, e.g.:
>>
>> - HOL-stable
>> - HOL-version1
>> - HOL-version2
>> - symbolic link HOL -> whichever is my default version
>>
>> I use the emacs mode and use the files from the symbolic link for the
>> emacs mode. If I want to switch the default versions (I need multiple
>> ones for different projects and sometimes work several days mainly with
>> one project), I change the symbolic link. However, in your case you have
>> to rebuild your whole own development after such a change, since
>> otherwise it remembers which HOL it was build with and uses this one
>> (which might be desirable sometimes).
>>
>> By the way, the ~30 min rebuild time are just for a fresh build on a not
>> too fast machine. Very often nothing changed in parts that appear early
>> in the build-chain, rebuilding the development version is much faster.
>> Even if it takes 30 min, I tend to schedule it for my lunch break and
>> have usually not much trouble.
>>
>> Cheers
>>
>> Thomas
>>
>>
>> On 04.02.2018 18:31, Mario Xerxes Castelán Castro wrote:
>>> On 04/02/18 11:26, Ramana Kumar wrote:
>>>> Yes, to do that you need to use --relocbuild, since any executables (heaps)
>>>> need to be rebuilt if the path changes.
>>>>
>>>> Steps:
>>>> 1. Copy your HOL directory to the new location, omitting any files that
>>>> match the patterns in tools-poly/rebuild-excludes.txt
>>>> 2. Run poly --script tools/smart-configure.sml in the new location
>>>> 3. Run bin/build --relocbuild in the new location
>>> Thanks, do I need to do this every time the absolute path changes?
>>>
>>> I try to use the development version, but since it takes around 1700 s
>>> to complete the build, I only update occasionally. I intended to
>>> schedule building an updated development version while I work with an
>>> already-built version. Once it is done building and I finish my work
>>> session, then move the new build into the place where my working build
>>> is. Is this possible without having to re-build heaps after moving?
>>>
>>> Thanks.
>>>
>>>
>>>
>>> ------------------------------------------------------------------------------
>>> 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
>>> hol-info@lists.sourceforge.net
>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>>
>> ------------------------------------------------------------------------------
>> 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
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>
>
>
> ------------------------------------------------------------------------------
> 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
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
