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 >
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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
