Add DESTDIR to cmake symlinks

[markrtuttle]

Add $DESTDIR to the cmake install symlinks for binaries and man pages.

The cmake build uses the GNUInstallDirs package. This implements the GNU Coding Standards for the installation of binaries, including prepending $DESTDIR to each installed target file. But $DESTDIR is not included in $CMAKE_INSTALL_BINDIR currently used for the construction of symlinks. This patch manually prepends $ENV{DESTDIR} to $CMAKE_INSTALL_BINDIR in the symlink commands.

This means, however, that DESTDIR must be defined when cmake configuration is run, it is not enough to configure and then define DESTDIR at install time. Because the $ENV{DESTDIR} used in the symlink commands is evaluated at configuration time, while cmake install inserts the $ENV{DESTDIR} at configure time for evaluation at installation time.

[codecov]

Codecov Report

Merging #5419 into develop will not change coverage.
The diff coverage is n/a.

@@           Coverage Diff            @@
##           develop    #5419   +/-   ##
========================================
  Coverage    68.20%   68.20%           
========================================
  Files         1177     1177           
  Lines        97528    97528           
========================================
  Hits         66523    66523           
  Misses       31005    31005           

Flag	Coverage Δ
#cproversmt2	42.75% <ø> (ø)
#regression	65.37% <ø> (ø)
#unit	32.25% <ø> (ø)

Flags with carried forward coverage won't be shown. Click here to find out more.

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 0c08382...56b4d28. Read the comment docs.

[hannes-steffenhagen-diffblue]

EDIT Some points raised in this comment not really accurate/relevant, see below.

DESTDIR is supposed to be passed to make as make DESTDIR=<value> according to this, and this already works by default with CMake. This works just as well with CMAKE_INSTALL_BINDIR (I’ve just tested this with a small example myself).

If you need to consider DESTDIR if it’s passed as an environment variable I’d recommend changing the places where you invoke make to include make ${DESTDIR+DESTDIR="$DESTDIR"}, which will expand to make DESTDIR="$DESTDIR" if the environment variable is set, and just make otherwise.

If you use cmake --install <your build directory> instead of invoking make directly this should actually already work as intended even if it’s set as an environment variable.

[martin-cs]

I have been pinged as a code owner but as I am not using cmake I am going to defer to @hannes-steffenhagen-diffblue on this.

[hannes-steffenhagen-diffblue]

Had a chat with Mark, I misunderstood the problem, it’s specifically about the create_symlink command here. This’ll require some thinking.

[hannes-steffenhagen-diffblue]

So aside from the whole DESTDIR issue I am learning more about symlinks as well. Didn’t know they worked with relative paths too, though that certainly is very convenient.

[hannes-steffenhagen-diffblue]

So I’ve done some investigating and I believe the only thing we really need to change here would be simply to escape the $ENV to delay variable expansion to install time, and I’d also add a slash so it doesn’t break if we ever use a base directory that’s not absolute (not the case in your examples because you use full paths, but we want to generalise this as much as possible I’d think).

Suggested change

	$ENV{DESTDIR}${CMAKE_INSTALL_FULL_MANDIR}/man1/janalyzer.1 \
	\$ENV{DESTDIR}/${CMAKE_INSTALL_FULL_MANDIR}/man1/janalyzer.1 \

Because two leading slashes has an implementation defined meaning and CMake recommends against the use of DESTDIR on Windows(primarily because windows absolute paths start with a drive letter, which doesn’t make sense in the middle of a path), I’d actually recommend something along the lines of:

install(CODE
  "set(CPROVER_INSTALL_MAN_SYMLINK_DESTINATION \"${CMAKE_INSTALL_FULL_MANDIR}\")\n\
   if(DEFINED ENV{DESTDIR} AND NOT WIN32) \n \
     string(PREPEND CPROVER_INSTALL_MAN_SYMLINK_DESTINATION \"\$ENV{DESTDIR}\") \n \
   endif() \n \
   execute_process(COMMAND ${CMAKE_COMMAND} -E create_symlink cbmc.1 \"\${CPROVER_INSTALL_MAN_SYMLINK_DESTINATION}/cbmc.1\")")

And since the logic for this is basically always going to be the same and messing around with sometimes-quoted-sometimes-not strings is super error prone, we’re better off extracting this into a function:

# We use this function to install symlinks to their proper places -- in
# particular, it is important we take build-time DESTDIR into account
# Usage:
#   cprover_install_symlink(
#     TARGET what-you-want-to-link-to
#     DESTINATION where-the-link-should-go)
# Note that on the CMake documentation (https://cmake.org/cmake/help/v3.18/envvar/DESTDIR.html)
# it notes that DESTDIR should not be used on windows, so we don’t take it into consideration
# if WIN32 is set.
function(cprover_install_symlink)
  cmake_parse_arguments(CPROVER_INSTALL_SYMLINK "" "TARGET;DESTINATION" "" ${ARGN})
  install(CODE
    "set(CPROVER_INSTALL_SYMLINK_DESTINATION \"${CPROVER_INSTALL_SYMLINK_DESTINATION}\") \n \
     if(DEFINED ENV{DESTDIR} AND NOT WIN32) \n \
       string(PREPEND CPROVER_INSTALL_SYMLINK_DESTINATION \"\$ENV{DESTDIR}/\") \n \
     endif() \n \
     execute_process( \
       COMMAND \"${CMAKE_COMMAND}\" \
         -E create_symlink \
         \"${CPROVER_INSTALL_SYMLINK_TARGET}\" \ 
         \"\${CPROVER_INSTALL_SYMLINK_DESTINATION}\")")
endfunction()

which for this case you’d call as

cprover_install_symlink(
  TARGET cbmc.1
  DESTINATION "${CMAKE_INSTALL_FULL_MANDIR}/man1/janalyzer.1")

Which I’d argue is easier to write and understand than what we currently have, even if the blob the function resolves to is slightly more complicated.

Unfortunately CMake currently does not have a builtin function for ergonomic path concatenation: https://gitlab.kitware.com/cmake/cmake/-/issues/19568#note_704230, but this way we should have double slashes only in the middle of paths where I don’t think they’re likely to cause problems.

If you could add this function and use it throughout the PR I think that’d address the concerns we both raised (i.e. this will now work exactly the same way as the other install commands w.r.t. DESTDIR, including taking it into consideration at build time/when passed to make instead of requiring it to be set at configure time. LMK if you have any questions/comments or otherwise need help with anything.

[hannes-steffenhagen-diffblue]

I’ve also been thinking this should probably issue a warning if the DESTDIR variable is defined on windows, as again, it won’t actually work there.

[markrtuttle]

I'll do my best to look at this today, but some comments.

I used the wrong escaping mechanism, I'll try the slash and try the macro.

I think the slash after DESTIR would be a mistake. The GNU Coding Standard says write $(DESTDIR)$(bindir)/foo and not $(DESTDIR)/$(bindir)/foo. The reason is that bindir is already a full path and DESTDIR is just intended to change the meaning of /. DESTDIR is empty by default.

GNU itself says don't use DESTDIR on Windows, leave it at its default value of empty, so I think it would be a mistake to do anything to accommodate using DESTDIR on Windows.

The macro idea is a good one.

[markrtuttle]

@hannes-steffenhagen-diffblue

I've updated the symlink commands to escape the $ to delay evaluation of $ENV{DESTDIR} from the configuration stage to the install stage. I've tested this change with both "DESTDIR=/tmp/staging ninja install" and "make DESTDIR=/tmp/staging install".

I think using $ENV{DESTDIR}/ in place of $ENV{DESTDIR} would be inconsistent with the instructions GNU gives for using DESTDIR.

I think making DESTDIR work on Windows is not worth the effort because CMake and GNU both warn against setting DESTDIR on Windows.

I think using a macro is a good idea, but the proposed macro seems rather complicated and hard to debug if anything should go wrong in the future, while the current create-symlink is still pretty easy to read.

[hannes-steffenhagen-diffblue]

@markrtuttle The goal isn’t to make DESTDIR work on Windows, it’s referenced in the function specifically to avoid accidentally using it on Windows: DESTDIR isn’t a reserved name or anything, it might be set in a users environment for reasons unrelated to this build, and we shouldn’t be reading from it if that’s the case. I’m also slightly concerned about the increasing size of mostly copy&paste code with the symlink, which is why I was suggesting the function (the function is slightly more complicated than the individual calls yes, but it would only appear once in the CMake files rather than a dozen times or so).

I’m OK with leaving off the slash here if GNU says to not include it.

I’m approving for now since the main issue is addressed, I might raise another PR for function-ifying the approach later on (which I still think we should do even if we otherwise remove the if I suggested adding) so we can separate the discussion on whether or not that’s a good idea from fixing the behaviour.

[danpoe]

Not a cmake expert, though it looks good to me. Before merging we should remove the *.bak files.

[hannes-steffenhagen-diffblue]

Oh right, hadn’t seen those. @markrtuttle Could you remove these?

[markrtuttle]

I've removed the *.bak files, and I've created an issue 5430 so we don't forget about @hannes-steffenhagen-diffblue's proposal to create the symlink macro and warn against the use of DESTDIR on Windows.

[chrisr-diffblue]

Looks good, thanks!