implement DESTDIR support for distros

[juhp]

Description

Prefix ${PREFIX} with ${DESTDIR} allowing installation into a staging directory for packaging Idris2.

Also take DESTDIR into account with idris2 --install etc.

Should this change go in the CHANGELOG?

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG.md (and potentially also
  CONTRIBUTORS.md).

I tested this a little on Fedora Linux.

When DESTDIR is not set, installation should behave exactly as now.

[juhp]

I would appreciate if someone could just have a glance at my simple idris code

[gallais]

Should PREFIX be computed from DESTDIR rather than prepending DESTDIR everywhere (and risking to forget it in places)?

[mattpolzin]

Should PREFIX be computed from DESTDIR

That might be more confusing than not since DESTDIR is documented as both "only applied in install steps" and "never showing up in built files" (like IdrisPaths.idr). So, for example, we would need to be careful to track where PREFIX gets used very carefully and also not redefine it prior to setting IDRIS2_PREFIX based on it.

OTOH, I think I'd be ok with either the current approach or a new variable like INSTALL_PREFIX. Would still perhaps benefit from explicit comment that such a variable is only to be used to offset installation and not to impact any build operations.

[juhp]

Right, this patch tries to do the minimal simplest thing, so that it should be obvious it does no harm.
DESTDIR support has been missing for a long time.
Perhaps further down the road it could be integrated more deeply.

[juhp]

Thank you @gallais for reviewing :yay: