Configure time virtualenv setup

This is the followup MR promised in !219 (merged) that implements setup of a virtualenv at configure time, if the user has explicitly granted permission to do so. Naturally, this one builds upon !219 (merged), so it might be a bit hard to spot the changes.

marked as a Work In Progress

added 1 commit

• 5bfc1a2b - Also install packages into the configure time virtualenv

Compare with previous version

added 2 commits

• ff4b8e59 - Add a helper to enforce the presence of configure-time virtualenv form downstream modules
• 8582443a - Write a wrapper script to allow execution of scripts installed into the dune-env

Compare with previous version

added 1 commit

• 3e9709c5 - Rename virtualenv python-env -> dune-env

Compare with previous version

added 1 commit

• 7a589fc7 - Update documentation of the virtualenv module

Compare with previous version

added 7 commits

• 168ee316 - Simplify installation of python packages
• 4c118e74 - Initial implementation of configure-time virtualenv setup
• c9bab66d - Also install packages into the configure time virtualenv
• 4331a0b2 - Add a helper to enforce the presence of configure-time virtualenv form downstream modules
• 578eea80 - Write a wrapper script to allow execution of scripts installed into the dune-env
• 57bc7ccc - Rename virtualenv python-env -> dune-env
• dd3a7724 - Update documentation of the virtualenv module

Compare with previous version

added 8 commits

• d9138f7c - [doc] Add more documentation / correct after proof-reading
• da7069b8 - Initial implementation of configure-time virtualenv setup
• 67c7d154 - Also install packages into the configure time virtualenv
• fdb97f55 - Add a helper to enforce the presence of configure-time virtualenv form downstream modules
• 727cea79 - Write a wrapper script to allow execution of scripts installed into the dune-env
• 27f81616 - Rename virtualenv python-env -> dune-env
• 712ebef1 - Update documentation of the virtualenv module
• 91c9f1b1 - [doc] Some proofreading on documenation

Compare with previous version

unmarked as a Work In Progress

Is hardcoding a shebang line here common practice? I would've expected either /bin/bash or the portable version /usr/bin/env bash instead.

BASH is here substituted with the bash found by find_package(UnixCommands). I considered that clean, I have no idea of what is considered common practice, though.

#!/bin/sh should work when . is used instead of source. At least I understand the comment about using the "original Bourne shell" in the documentation for activate as it not needing bash specifically.

Please also use "$@" (with quotes) so arguments with whitespace are correctly forwarded.

Thanks Ansgar. If you have a strong suggestion for the shebang, I will happily follow that.

added 1 commit

• 7f503237 - [bugfix] Quote $@ to preserve whitespace in arguments

Compare with previous version

This is available for about a month now, I will merge at the end of the week if nobody objects.

mentioned in merge request !219 (merged)

merged

mentioned in commit 418a0e35

mentioned in commit 9d0debba