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