Check shell scripts during CI

[rptb1]

To help prevent introduction of shell script errors.

Run the shellcheck linter on shell scripts in the MPS as part of CI.

Also adds tool/check-shell-scripts for command-line use.

Shell script errors are not known to have caused defects in the MPS, but this was very cheap to implement as a side effect of #112

[rptb1]

We plan to use this pull request as a test for the draft public MPS Review Procedure.

Accordingly, I'm executing review entry on this pull request and branch.

Applying entry.universal and entry.impl.

• entry.universal.source-available: There isn't an issue document for this change, but I think it's clear from the pull request why it's an improvement. However, that reason is unreviewed. That's not a risk to the MPS because this is just a small CI script.
• entry.universal.rules-available: rule.generic, rule.code, rule.code.style are all available in https://github.com/Ravenbrook/mps/tree/branch/2023-01-19/review-procedure/procedure but have not exited review. That could be a risk to the MPS, but these are edits of long-standing rulesets, so it's unlikely any major problems have been introduced.

Entry passed.

This step took about 5 mins.

[rptb1]

Executing review planning.

• proc.review.plan.time: About 100 lines of code @ 10 lines/minute so about 10 mins of actual checking. The whole review will take much longer because this is a test-run and training session. We'll measure that.
• @rptb1 @thejayps @UNAA008 will review on 2023-01-30 at 11:00 UTC for about 2h. This will also be a review training session.
• We will apply at least rule.generic and rule.code.
• I will discuss and assign checking roles at proc.review.kickoff.
• Participants have already been invited.

This step took about 10 mins.

[rptb1]

Extra review objectives for proc.review.ko.improve:

1. Find good ways to use the GitHub review tools.

2. Test whether this is true:

   mps/procedure/review.rst

   Lines 425 to 429 in de6159a

   	- GitHub's review tool reveals comments made by one reviewer to every
   	other reviewer in real time, so they distract one another from
   	finding their own unique defects. Avoid entering comments using
   	GitHub until `.log`_. [Verify that this is the case and check
   	whether it can be disabled or worked around. RB 2023-01-28]

3. Estimate time-to-execute and time-to-learn.

[rptb1]

Executing review kickoff.

1. @thejayps is doing proc.review.role.check.{clarity,consistency}. @UNAA008 is doing proc.review.role.check.{source,correctness}. We're not doing proc.review.role.check.backwards, because the change is too short!

2. Review objective: test GitHub review tool. @thejayps thinks that review comments (in the context of a GitHub review) are not published until the review is complete, but "individual comments" are. This could be good because we can do individual checking and press a button (submitting the review) later to publish them all during proc.review.log. We'll test this today.

3. Start checking at 11:50 and logging at 12:10, being generous with checking time. It's a short document.

4. Extra objective: Checkers will think about how to update proc.review.check for use with GitHub review tool. What button do you press when? What do you type where? We will also be doing this for proc.review.log.

Kickoff took 45 minutes including training and some discussion of improvements to the draft procedure.

[rptb1]

proc.review.check.record:

• 1 minor issue
• 5 mins checking
• checked everything

[UNAA008]

role.check.source - checked usage of shellcheck consistent with description at
https://github.com/koalaman/shellcheck
Checked shell-script-check.yml
and tool/check-shell-scripts

No issues found in the time available.

[thejayps]

.check.record:

• 3 minor defects
• 20 mins total looking at .clarity and .consistency
• Checked all the product document

[rptb1]

Executing proc.review.log.

1. We didn't have any major issues, so we went through the minor ones as if they were major as a training exercise.
2. Brainstorm scheduled at 12:50 for 13:00.

Logging took 40 minutes.

[rptb1]

Executing review brainstorm even though we don't have any major issues. It's training!

1. For Check shell scripts during CI #117 (comment) : @thejayps suggests a checklist item perhaps, where you deliberately try to misinterpret your sentences and improve them if you can (misinterpret them).
2. For Check shell scripts during CI #117 (comment) : We don't have a ruleset for shells scripts. It could cover both this and Check shell scripts during CI #117 (comment) . @UNAA008 suggests we have rules for portability (e.g. bash dependency?)
3. For Check shell scripts during CI #117 (comment) maybe there's a general principle that might be related to https://en.wikipedia.org/wiki/Principle_of_least_astonishment when communicating with colleagues. We're not sure what can be done concretely about it.
4. [Added by @rptb1 after review.] Please see https://github.com/Ravenbrook/mps/pull/117/files#r1090895426

proc.review.brainstorm.proc:

• @UNAA008 found it hard going (but not necessarily in a bad way) because there's a lot he's not fluent with. Perhaps people that know they're going to be participating allocate some pre-review time to glancing over the whole thing. @rptb1 said (in chat) that this wasn't necessary, but perhaps it was. What he has in mind is where there's a reviewer not fluent with the source material, to participate might require homework. Maybe the leader needs to consider "homework" based on the roles they think people might be best at.

• @thejayps thinks that showing the procedure now, without prior knowledge, was efficient for him. Can this review (documented here) become a worked example?

• @rptb1 says it's not necessary for everyone to understand thoroughly what's being checked. e.g. shell script language. That just means they can't do some roles. "When I run it is it actually faster like it claims?" is an example. Maybe the procedure should reassure people on this point. That's like the opposite of homework. The leader can say "Don't worry about X I'm going to get you do Y which is useful."

Brainstorm took 35 minutes.

[rptb1]

Preliminary estimation, proc.review.phase.estimation.

• 35 mins for @rptb1 plus 140 mins for @rptb1 @thejayps @UNAA008 so that's roughly 8 person-hours.
• manpower-saved: Probably only 30 mins confusion and interpreting CI output because shell script didn't work from the wrong directory.
• BUT we have started to train everyone in review in this case. Priceless.
• We reckon there are zero major defects remaining.

[rptb1]

Executing review exit.

1. Revised change passed.

Exit took 5 minutes.

Final metrics (proc.review.exit.calc):

• hours used: 8
• hours saved: 1 (a couple of new issues were fixed in 0d071c0
• major defects remaining: 0

[rptb1]

Executing pull request merge procedure.

1. There isn't a GitHub issue, but review agreed that was OK.
2. An automated test case isn't feasible as it would mean introducing broken shell scripts to GitHub and watching for CI errors.
3. Merge isn't approved because GitHub restricts the author from approving their own review. I will override it this time.

Merge procedure took 6 minutes.

[rptb1]

• Maybe the leader needs to consider "homework" based on the roles they think people might be best at.

Fixed in f8b6c94.