diff --git a/.forgejo/workflows/checks.yml b/.forgejo/workflows/checks.yml index 6033ef8..35c511c 100644 --- a/.forgejo/workflows/checks.yml +++ b/.forgejo/workflows/checks.yml @@ -15,9 +15,7 @@ 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: diff --git a/nlnet-2024-12-324/progress.md b/nlnet-2024-12-324/progress.md index 6fb94fb..e29d4ec 100644 --- a/nlnet-2024-12-324/progress.md +++ b/nlnet-2024-12-324/progress.md @@ -4,8 +4,6 @@ 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. @@ -16,7 +14,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 #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.). +- € 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.). - € 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 diff --git a/nlnet-template/progress.md b/nlnet-template/progress.md index f1e3280..829f2cd 100644 --- a/nlnet-template/progress.md +++ b/nlnet-template/progress.md @@ -4,8 +4,6 @@ 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. diff --git a/scripts/check-consistency.sh b/scripts/check-consistency.sh index b4f58f5..481a0a7 100755 --- a/scripts/check-consistency.sh +++ b/scripts/check-consistency.sh @@ -45,96 +45,6 @@ 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\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 @@ -196,15 +106,6 @@ 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)" - else - [[ "$line" = "${project_line_prefix}ID)" ]] || \ - nonfatal_error "expected: ${project_line_prefix}ID)" - fi - skip_until_item "top level grant header" [[ "$line" =~ ^"# € "([0-9]+)" "[^[:space:]] ]] || error "expected: # € " ((grant_amount = ${BASH_REMATCH[1]})) @@ -221,40 +122,20 @@ function check_progress() skip_until_item subtasks_total=0 until ((eof)); do - subtask_expected="expected: - € [Issue #]($(issue_url "")) " + subtask_expected="expected: - € [Issue #](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) " [[ "$line" =~ ^([#-]+)" € "([0-9]+)" "[^[:space:]] ]] || error "$subtask_expected" [[ "${BASH_REMATCH[1]}" =~ ^[^'#'] ]] || break - [[ "$line" =~ ^"- € "([0-9]+)" [Issue #"([0-9]+|"N")"](https://git.libre-chip.org/libre-chip/grant-tracking/issues"('/'([0-9]*|"N"))?") "([^[:space:]].*)$ ]] || \ + [[ "$line" =~ ^"- € "([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)"