Moving from inline shell in the Makefile to separate shell scripts

[ElectreAAS]

Cleaning the Makefile, one script at a time

This PR will eventually resolve #330, at least Phase 1. The Makefile is huge and ripe with quoted shell, which leads to quoting issues, especially with empty variables. Putting everything in bash scripts means we don't need to juggle makefile syntax and bash syntax, so less error-prone. I also use Shellcheck to lint the scripts.

Design decisions

• A Makefile should make stuff, not run it. However, this would require dune integration and is going to be in the phase 2.
• No quoted shell. If we use bash scripts, let's at least put those in proper bash scripts, with file names, function names and comments.
• No "quoted make". By this I mean other places than the Makefile where variables contain make commands (like in the dockerfile currently)
• No unnecessary noise. This means @ at the start of a lot of commands, and >/dev/null at the end of others. We should still echo what we are doing so errors have context in the logs.
• Simpler usage. Running the default command should be something like make build_and_run or make; make run... Configuration should be in one easily identified place.
• Using the docker cache as much as possible. This one is to improve performance on current-bench. We should have all the build commands (hopefully not many) in the dockerfile, and make bench should just not need to build anything.

[ElectreAAS]

I am considering splitting this PR into several smaller independent PRs, as the multiple shell scripts are independent.

[ElectreAAS]

I rebased this branch on main, hence the multiple force pushes

[ElectreAAS]

Progress report: All of the complicated make commands have been replaced by shell scripts Some 2-3 lines one still remain