add checks for forgejo issues and projects

.forgejo/workflows/checks.yml

@@ -15,7 +15,9 @@ jobs:
       - run: |
           apt-get update -qq
           apt-get install -qq \
+              curl \
               default-jre-headless \
+              jq \
               python3-venv
       - uses: https://git.libre-chip.org/mirrors/cache@v4
         with:

nlnet-2024-12-324/progress.md

@@ -4,6 +4,8 @@ See Notices.txt for copyright information
 -->
 # NLnet 2024-12-324 Grant Progress
 
+[Forgejo Project for this grant.](https://git.libre-chip.org/libre-chip/grant-tracking/projects/1)
+
 # € 50000 Libre-Chip's First CPU Architecture And Formal Proof of No Spectre bugs
 
 Modern computers suffer from a constant stream of new speculative-execution security flaws (Spectre-style bugs). To address this major category of flaws, we are working towards building a high-performance computer processor (CPU) with speculative execution and working on a mathematical proof that it doesn't suffer from any speculative-execution data leaks, thereby demonstrating that this major category of flaws can be eliminated without crippling the computer's performance.
@@ -14,7 +16,7 @@ https://en.wikipedia.org/wiki/Transient_execution_CPU_vulnerability#Timeline
 
 This is for adding the code for translating Fayalite HDL to Rocq, as well as determining how exactly we'll describe HDL in Rocq. I expect the translation code to be of comparable size to the compiler portion of the simulator (the simulator is broken into three main parts, a compiler to an IR optimized for interpretation, the interpreter itself, and the code for reading/writing simulator I/O and handling time simulation), so somewhere around 5000 LoC.
 
-- € 2000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Figure out how exactly we should represent HDL in Rocq, writing down a manually-translated version of common HDL components (e.g. how to translate a register, a memory, an add/sub/mul/div, etc.).
+- € 2000 [Issue #2](https://git.libre-chip.org/libre-chip/grant-tracking/issues/2) Figure out how exactly we should represent HDL in Rocq, writing down a manually-translated version of common HDL components (e.g. how to translate a register, a memory, an add/sub/mul/div, etc.).
 - € 4000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Write the code to do the translation in Fayalite.
 
 ## € 4000 Adding supporting code for generating FPGA bitstreams from Fayalite

nlnet-template/progress.md

@@ -4,6 +4,8 @@ See Notices.txt for copyright information
 -->
 # NLnet YYYY-MM-ID Grant Progress
 
+[Forgejo Project for this grant.](https://git.libre-chip.org/libre-chip/grant-tracking/projects/ID)
+
 # € 50000 Top-level Grant Name
 
 Top-level Grant Description.

scripts/check-consistency.sh

@@ -45,6 +45,96 @@ function check_amendment()
     python3 -m takentaal.takentaal amendment_v1_0 "$1"
 }
 
+function matches_split_prefix() {
+    local expected="$1" text="$2"
+    shift 2
+    local split_token text_prefix next_text_prefix
+    for split_token in "$@"; do
+        text_prefix="$text"
+        until [[ -z "$text_prefix" ]]; do
+            if [[ "$expected" = "$text_prefix" ]]; then
+                return 0
+            else
+                next_text_prefix="${text_prefix%"$split_token"*}"
+                if [[ "$text_prefix" = "$next_text_prefix" ]]; then
+                    break
+                else
+                    text_prefix="$next_text_prefix"
+                fi
+            fi
+        done
+    done
+    return 1
+}
+
+function issue_url() {
+    local issue_number="$1"
+    echo "https://git.libre-chip.org/libre-chip/grant-tracking/issues/$issue_number"
+}
+
+function grant_url() {
+    local nlnet_id="$1"
+    if [[ "$nlnet_id" == "YYYY-MM-ID" ]]; then
+        nlnet_id=template
+    fi
+    echo "https://git.libre-chip.org/libre-chip/grant-tracking/src/branch/master/nlnet-$nlnet_id/progress.md"
+}
+
+function check_issue()
+(
+    issue_number="$1"
+    nlnet_id="$2"
+    subtask_title="$3"
+    subtask_body="$4"
+    if [[ -z "$FORGEJO_TOKEN" ]]; then
+        return
+    fi
+    example_title="NLnet $nlnet_id $subtask_title"
+    body_prefix="Issue for tracking progress of a subtask of [NLnet grant $nlnet_id]($(grant_url "$nlnet_id")):
+$subtask_title
+$subtask_body
+"
+    body_suffix="" # TODO
+    example_body_middle=$'\n<!-- add additional content here if you like -->\n'
+    function error() {
+        # emit escape sequence for a hyperlink to the issue
+        bar="---------------------------------------------------------------------------"
+        body="$body_prefix"
+        body_middle="${example_body_middle%$'\n'}"
+        body+="${body_middle#$'\n'}"
+        body+="$body_suffix"
+        printf '\e]8;;%s\e\\Issue #%s\e]8;;\e\\: error: %s\nExample Issue:\nTitle: %s\nDescription:\n%s\n%s\n%s\n' \
+            "$(issue_url "$issue_number")" "$issue_number" "$*" \
+            "$example_title" "$bar" "$body" "$bar" >&2
+        exit 1
+    }
+    issue_json="$(curl -sS "https://git.libre-chip.org/api/v1/repos/libre-chip/grant-tracking/issues/$issue_number" \
+        -H "Accept: application/json" \
+        -H "Authorization: token $FORGEJO_TOKEN")" || error "can't retrieve issue"
+    issue_title="$(echo "$issue_json" | jq -r '.title')"
+    issue_body="$(echo "$issue_json" | jq -r '.body')"
+    [[ "$issue_title" =~ ^"NLnet $nlnet_id "(.*)$ ]] || error "title must start with \`NLnet $nlnet_id \`"
+    issue_title_tail="${BASH_REMATCH[1]}"
+    split_punct=(',' '-' ';' ':')
+    matches_split_prefix "$issue_title_tail" "$subtask_title" "${split_punct[@]}" || \
+        error "issue title must be \`NLnet $nlnet_id \` followed by the subtask title, or a prefix of the subtask title that ends right before one of:$(printf ' `%s`' "${split_punct[@]}")"
+    if [[ "$issue_body" =~ ^"$body_prefix".*"$body_suffix"$ ]]; then
+        : # all good
+    elif [[ "$issue_body" =~ ^"$body_prefix"(.*)"$example_body_middle"(.*)$ || \
+            "$issue_body" =~ ^"$body_prefix"(.*)()$ ]]; then
+        example_body_middle="${BASH_REMATCH[1]}$example_body_middle${BASH_REMATCH[2]}"
+        error "issue description is missing required suffix"
+    elif [[ "$issue_body" =~ ^(.*)"$example_body_middle"(.*)"$body_suffix"$ || \
+            "$issue_body" =~ ^(.*)()"$body_suffix"$ ]]; then
+        example_body_middle="${BASH_REMATCH[1]}$example_body_middle${BASH_REMATCH[2]}"
+        error "issue description is missing required prefix"
+    elif [[ "$issue_body" =~ ^(.*)"$example_body_middle"(.*)$ || \
+            "$issue_body" =~ ^(.*)()$ ]]; then
+        example_body_middle="${BASH_REMATCH[1]}$example_body_middle${BASH_REMATCH[2]}"
+        error "issue description is missing both the required prefix and suffix"
+    fi
+)
+
 function check_progress()
 (
     set -E
@@ -106,6 +196,15 @@ function check_progress()
         "^'# NLnet $nlnet_id Grant Progress'$" \
         "^$"
 
+    project_line_prefix='[Forgejo Project for this grant.](https://git.libre-chip.org/libre-chip/grant-tracking/projects/'
+    if [[ "$nlnet_id" != "YYYY-MM-ID" ]]; then
+        [[ "$line" =~ ^"$project_line_prefix"[0-9]+')'$ ]] || \
+            nonfatal_error "expected: $project_line_prefix<the-project's-id>)"
+    else
+        [[ "$line" = "${project_line_prefix}ID)" ]] || \
+            nonfatal_error "expected: ${project_line_prefix}ID)"
+    fi
+
     skip_until_item "top level grant header"
     [[ "$line" =~ ^"# &euro; "([0-9]+)" "[^[:space:]] ]] || error "expected: # &euro; <number> <grant name>"
     ((grant_amount = ${BASH_REMATCH[1]}))
@@ -122,20 +221,40 @@ function check_progress()
         skip_until_item
         subtasks_total=0
         until ((eof)); do
-            subtask_expected="expected: - &euro; <number> [Issue #<N>](https://git.libre-chip.org/libre-chip/grant-tracking/issues/<N>) <subtask name>"
+            subtask_expected="expected: - &euro; <number> [Issue #<N>]($(issue_url "<N>")) <subtask name>"
             [[ "$line" =~ ^([#-]+)" &euro; "([0-9]+)" "[^[:space:]] ]] || error "$subtask_expected"
             [[ "${BASH_REMATCH[1]}" =~ ^[^'#'] ]] || break
-            [[ "$line" =~ ^"- &euro; "([0-9]+)" [Issue #"([0-9]+|"N")"](https://git.libre-chip.org/libre-chip/grant-tracking/issues"('/'([0-9]*|"N"))?") "[^[:space:]] ]] || \
+            [[ "$line" =~ ^"- &euro; "([0-9]+)" [Issue #"([0-9]+|"N")"](https://git.libre-chip.org/libre-chip/grant-tracking/issues"('/'([0-9]*|"N"))?") "([^[:space:]].*)$ ]] || \
                 error "$subtask_expected"
             ((subtask_amount = ${BASH_REMATCH[1]}))
             ((subtasks_total += subtask_amount))
             issue_number="${BASH_REMATCH[2]}"
             issue_number2="${BASH_REMATCH[4]}"
+            subtask_title="${BASH_REMATCH[5]}"
             [[ "$issue_number" != "N" ]] || [[ "$nlnet_id" = "YYYY-MM-ID" ]] || nonfatal_error "issue number must be set"
             [[ ( "$issue_number" = "N" && -z "$issue_number2" ) || "$issue_number" = "$issue_number2" ]] || \
                 nonfatal_error "issue number in link name must match issue number in url"
+            ((subtask_line_index = line_index))
             next_line
             skip_until_item
+            subtask_body=""
+            subtask_body_trailing_lines=""
+            # trim leading and trailing blank lines
+            for ((i = subtask_line_index + 1; i < line_index; i++)); do
+                if [[ "${lines[i]}" =~ ^[[:space:]]*$ ]]; then
+                    subtask_body_trailing_lines+="${lines[i]}"$'\n'
+                elif [[ -z "$subtask_body" ]]; then
+                    subtask_body+="${lines[i]}"$'\n'
+                    subtask_body_trailing_lines="" # ignore any leading blank lines
+                else
+                    # add subtask_body_trailing_lines since they're lines in between non-blank lines
+                    subtask_body+="$subtask_body_trailing_lines${lines[i]}"$'\n'
+                    subtask_body_trailing_lines=""
+                fi
+            done
+            if [[ "$issue_number2" =~ ^[0-9]+$ && "$nlnet_id" != "YYYY-MM-ID" && "$FORGEJO_TOKEN" ]]; then
+                check_issue "$issue_number2" "$nlnet_id" "$subtask_title" "$subtask_body" || diag "note:" -line_index="$subtask_line_index" "issue is linked from here"
+            fi
         done
         (( subtasks_total == task_amount )) || \
             nonfatal_error -line_index="$task_line_index" "task's amount ($task_amount) doesn't match sum of subtasks' amounts ($subtasks_total)"