In fact,
bin/build cleanForReloc
will purge a directory tree of the files in rebuild-excludes.txt, so it might
be easier to copy a tree and then “clean” it.
This workflow should be documented before the next release.
Best wishes,
Michael
From: Ramana Kumar
Date: Monday, 5 February 2018 at
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 nee
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. Relocatio
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
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
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.tx
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
Hello.
Is it possible to use HOL4 in such a way that it continues working
despite moving the directory to a different absolute path? The option
“--relocbuild” of “bin/build” seems to be related. Is it documented
anywhere? (I did not find anything in the manual)
Thanks.
signature.asc
Descripti