[Hol-info] Dependency on absolute paths remaining the same

2018-02-04 Thread Mario Xerxes Castelán Castro
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

Re: [Hol-info] Dependency on absolute paths remaining the same

2018-02-04 Thread Mario Xerxes Castelán Castro
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

Re: [Hol-info] Dependency on absolute paths remaining the same

2018-02-04 Thread Thomas Tuerk
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

Re: [Hol-info] Dependency on absolute paths remaining the same

2018-02-04 Thread Thomas Tuerk
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.

Re: [Hol-info] Dependency on absolute paths remaining the same

2018-02-04 Thread Ramana Kumar
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

Re: [Hol-info] Dependency on absolute paths remaining the same

2018-02-04 Thread Mario Xerxes Castelán Castro
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

Re: [Hol-info] Dependency on absolute paths remaining the same

2018-02-04 Thread Mario Xerxes Castelán Castro
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

Re: [Hol-info] Dependency on absolute paths remaining the same

2018-02-04 Thread Michael.Norrish
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: