Skip to content

Commit aa9b464

Browse files
hyperpolymathhyperpolymath
authored
Merge branch 'main' into wip/brouwer-phase-1-3-recursive-predicate
2 parents 077fca0 + 9312add commit aa9b464

109 files changed

Lines changed: 16676 additions & 910 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.editorconfig‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
root = true
3+
4+
[*]
5+
end_of_line = lf
6+
insert_final_newline = true
7+
charset = utf-8
8+
indent_style = space
9+
indent_size = 2
10+
trim_trailing_whitespace = true
11+
12+
[*.agda]
13+
indent_size = 2
14+
15+
[*.rs]
16+
indent_size = 4
17+
18+
[Makefile]
19+
indent_style = tab
20+
21+
[Justfile]
22+
indent_style = tab

‎.envrc‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
use flake

‎.gitattributes‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
* text=auto eol=lf
2+
*.agda text eol=lf
3+
*.adoc text eol=lf
4+
*.md text eol=lf
5+
*.yml text eol=lf
6+
*.yaml text eol=lf
7+
*.scm text eol=lf
8+
*.a2ml text eol=lf
9+
*.agdai binary

‎.github/workflows/agda.yml‎

Lines changed: 21 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,14 @@ jobs:
3030
git clone --depth 1 --branch v2.3 https://github.com/agda/agda-stdlib.git "$STDLIB_DIR"
3131
echo "stdlib_dir=$STDLIB_DIR" >> "$GITHUB_OUTPUT"
3232
33-
- name: Register standard library for Agda
33+
- name: Fetch absolute-zero library
34+
id: absz
35+
run: |
36+
ABSZ_DIR="$RUNNER_TEMP/absolute-zero"
37+
git clone --depth 1 https://github.com/hyperpolymath/absolute-zero.git "$ABSZ_DIR"
38+
echo "absz_dir=$ABSZ_DIR" >> "$GITHUB_OUTPUT"
39+
40+
- name: Register libraries for Agda
3441
run: |
3542
mkdir -p "$HOME/.agda"
3643
@@ -40,11 +47,23 @@ jobs:
4047
include: ${{ steps.stdlib.outputs.stdlib_dir }}/src
4148
EOF
4249
43-
printf '%s\n' "$STDLIB_LIB" > "$HOME/.agda/libraries"
50+
ABSZ_LIB="$RUNNER_TEMP/absolute-zero.agda-lib"
51+
cat > "$ABSZ_LIB" <<EOF
52+
name: absolute-zero
53+
include: ${{ steps.absz.outputs.absz_dir }}/proofs/agda
54+
EOF
55+
56+
printf '%s\n%s\n' "$STDLIB_LIB" "$ABSZ_LIB" > "$HOME/.agda/libraries"
4457
printf '%s\n' "standard-library" > "$HOME/.agda/defaults"
4558
4659
- name: Typecheck full suite
4760
run: agda -i proofs/agda proofs/agda/All.agda
4861

4962
- name: Smoke-check headline theorems
5063
run: agda -i proofs/agda proofs/agda/Smoke.agda
64+
65+
- name: Typecheck characteristic lane (Gate #2 audit modules)
66+
run: agda -i proofs/agda proofs/agda/characteristic/All.agda
67+
68+
- name: Typecheck examples lane (Gate #3 canonical examples)
69+
run: agda -i proofs/agda proofs/agda/examples/All.agda

‎.github/workflows/hypatia-scan.yml‎

Lines changed: 99 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,99 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# Hypatia Neurosymbolic CI/CD Security Scan — SELF-SCAN (dogfooding)
3+
# The standards repo that defines Hypatia scans itself with Hypatia.
4+
name: Hypatia Self-Scan
5+
6+
on:
7+
push:
8+
branches: [ main ]
9+
pull_request:
10+
branches: [ main ]
11+
schedule:
12+
- cron: '0 0 * * 0' # Weekly on Sunday
13+
workflow_dispatch:
14+
15+
permissions: read-all
16+
17+
jobs:
18+
scan:
19+
name: Hypatia Neurosymbolic Analysis (Dogfooding)
20+
runs-on: ubuntu-latest
21+
22+
steps:
23+
- name: Checkout repository
24+
uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
25+
with:
26+
fetch-depth: 0
27+
28+
- name: Setup Elixir for Hypatia scanner
29+
uses: erlef/setup-beam@fc68ffb90438ef2936bbb3251622353b3dcb2f93 # v1.24.0
30+
with:
31+
elixir-version: '1.19.4'
32+
otp-version: '28.3'
33+
34+
- name: Clone Hypatia
35+
run: |
36+
git clone --depth 1 https://github.com/hyperpolymath/hypatia.git "$HOME/hypatia"
37+
38+
- name: Build Hypatia scanner
39+
run: |
40+
cd "$HOME/hypatia"
41+
if [ ! -f hypatia-v2 ]; then
42+
cd scanner && mix deps.get && mix escript.build && mv hypatia ../hypatia-v2
43+
fi
44+
45+
- name: Run Hypatia scan
46+
id: scan
47+
run: |
48+
echo "Scanning standards repo (dogfooding)"
49+
HYPATIA_FORMAT=json "$HOME/hypatia/hypatia-cli.sh" scan . > hypatia-findings.json
50+
51+
FINDING_COUNT=$(jq '. | length' hypatia-findings.json 2>/dev/null || echo 0)
52+
CRITICAL=$(jq '[.[] | select(.severity == "critical")] | length' hypatia-findings.json 2>/dev/null || echo 0)
53+
HIGH=$(jq '[.[] | select(.severity == "high")] | length' hypatia-findings.json 2>/dev/null || echo 0)
54+
MEDIUM=$(jq '[.[] | select(.severity == "medium")] | length' hypatia-findings.json 2>/dev/null || echo 0)
55+
56+
echo "findings_count=$FINDING_COUNT" >> $GITHUB_OUTPUT
57+
echo "critical=$CRITICAL" >> $GITHUB_OUTPUT
58+
echo "high=$HIGH" >> $GITHUB_OUTPUT
59+
echo "medium=$MEDIUM" >> $GITHUB_OUTPUT
60+
61+
echo "## Hypatia Self-Scan Results (Dogfooding)" >> $GITHUB_STEP_SUMMARY
62+
echo "" >> $GITHUB_STEP_SUMMARY
63+
echo "The standards repo scans itself. Findings here are compliance" >> $GITHUB_STEP_SUMMARY
64+
echo "gaps between what we define and what we practice." >> $GITHUB_STEP_SUMMARY
65+
echo "" >> $GITHUB_STEP_SUMMARY
66+
echo "| Severity | Count |" >> $GITHUB_STEP_SUMMARY
67+
echo "|----------|-------|" >> $GITHUB_STEP_SUMMARY
68+
echo "| Critical | $CRITICAL |" >> $GITHUB_STEP_SUMMARY
69+
echo "| High | $HIGH |" >> $GITHUB_STEP_SUMMARY
70+
echo "| Medium | $MEDIUM |" >> $GITHUB_STEP_SUMMARY
71+
echo "| **Total**| $FINDING_COUNT |" >> $GITHUB_STEP_SUMMARY
72+
73+
- name: Run panic-attack assail
74+
run: |
75+
# Install panic-attack if available
76+
if command -v panic-attack >/dev/null 2>&1; then
77+
panic-attack assail . > panic-attack-findings.json 2>&1 || true
78+
echo "panic-attack scan complete"
79+
else
80+
echo "panic-attack not available in CI — install from hyperpolymath/panic-attacker"
81+
echo "[]" > panic-attack-findings.json
82+
fi
83+
84+
- name: Upload findings artifacts
85+
uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4
86+
with:
87+
name: standards-self-scan
88+
path: |
89+
hypatia-findings.json
90+
panic-attack-findings.json
91+
retention-days: 90
92+
93+
- name: Check for critical issues
94+
if: steps.scan.outputs.critical > 0
95+
run: |
96+
echo "Critical self-scan issues found in the standards repo!"
97+
echo "The repo that defines standards has compliance gaps."
98+
echo "Review hypatia-findings.json for details."
99+
# Warn but don't fail — fix forward

‎.github/workflows/mirror.yml‎

Lines changed: 145 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,145 @@
1+
# SPDX-License-Identifier: PMPL-1.0
2+
# SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell
3+
name: Mirror to Git Forges
4+
5+
on:
6+
push:
7+
branches: [main]
8+
workflow_dispatch:
9+
10+
permissions:
11+
contents: read
12+
13+
jobs:
14+
mirror-gitlab:
15+
runs-on: ubuntu-latest
16+
if: vars.GITLAB_MIRROR_ENABLED == 'true'
17+
steps:
18+
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
19+
with:
20+
fetch-depth: 0
21+
22+
- uses: webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555 # v0.10.0
23+
with:
24+
ssh-private-key: ${{ secrets.GITLAB_SSH_KEY }}
25+
26+
- name: Mirror to GitLab
27+
run: |
28+
ssh-keyscan -t ed25519 gitlab.com >> ~/.ssh/known_hosts
29+
git remote add gitlab git@gitlab.com:hyperpolymath/${{ github.event.repository.name }}.git || true
30+
git push --force gitlab main
31+
32+
mirror-bitbucket:
33+
runs-on: ubuntu-latest
34+
if: vars.BITBUCKET_MIRROR_ENABLED == 'true'
35+
steps:
36+
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
37+
with:
38+
fetch-depth: 0
39+
40+
- uses: webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555 # v0.10.0
41+
with:
42+
ssh-private-key: ${{ secrets.BITBUCKET_SSH_KEY }}
43+
44+
- name: Mirror to Bitbucket
45+
run: |
46+
ssh-keyscan -t ed25519 bitbucket.org >> ~/.ssh/known_hosts
47+
git remote add bitbucket git@bitbucket.org:hyperpolymath/${{ github.event.repository.name }}.git || true
48+
git push --force bitbucket main
49+
50+
mirror-codeberg:
51+
runs-on: ubuntu-latest
52+
if: vars.CODEBERG_MIRROR_ENABLED == 'true'
53+
steps:
54+
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
55+
with:
56+
fetch-depth: 0
57+
58+
- uses: webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555 # v0.10.0
59+
with:
60+
ssh-private-key: ${{ secrets.CODEBERG_SSH_KEY }}
61+
62+
- name: Mirror to Codeberg
63+
run: |
64+
ssh-keyscan -t ed25519 codeberg.org >> ~/.ssh/known_hosts
65+
git remote add codeberg git@codeberg.org:hyperpolymath/${{ github.event.repository.name }}.git || true
66+
git push --force codeberg main
67+
68+
mirror-sourcehut:
69+
runs-on: ubuntu-latest
70+
if: vars.SOURCEHUT_MIRROR_ENABLED == 'true'
71+
steps:
72+
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
73+
with:
74+
fetch-depth: 0
75+
76+
- uses: webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555 # v0.10.0
77+
with:
78+
ssh-private-key: ${{ secrets.SOURCEHUT_SSH_KEY }}
79+
80+
- name: Mirror to SourceHut
81+
run: |
82+
ssh-keyscan -t ed25519 git.sr.ht >> ~/.ssh/known_hosts
83+
git remote add sourcehut git@git.sr.ht:~hyperpolymath/${{ github.event.repository.name }} || true
84+
git push --force sourcehut main
85+
86+
mirror-disroot:
87+
runs-on: ubuntu-latest
88+
if: vars.DISROOT_MIRROR_ENABLED == 'true'
89+
steps:
90+
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
91+
with:
92+
fetch-depth: 0
93+
94+
- uses: webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555 # v0.10.0
95+
with:
96+
ssh-private-key: ${{ secrets.DISROOT_SSH_KEY }}
97+
98+
- name: Mirror to Disroot
99+
run: |
100+
ssh-keyscan -t ed25519 git.disroot.org >> ~/.ssh/known_hosts
101+
git remote add disroot git@git.disroot.org:hyperpolymath/${{ github.event.repository.name }}.git || true
102+
git push --force disroot main
103+
104+
mirror-gitea:
105+
runs-on: ubuntu-latest
106+
if: vars.GITEA_MIRROR_ENABLED == 'true'
107+
steps:
108+
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
109+
with:
110+
fetch-depth: 0
111+
112+
- uses: webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555 # v0.10.0
113+
with:
114+
ssh-private-key: ${{ secrets.GITEA_SSH_KEY }}
115+
116+
- name: Mirror to Gitea
117+
run: |
118+
ssh-keyscan -t ed25519 ${{ vars.GITEA_HOST }} >> ~/.ssh/known_hosts
119+
git remote add gitea git@${{ vars.GITEA_HOST }}:hyperpolymath/${{ github.event.repository.name }}.git || true
120+
git push --force gitea main
121+
122+
mirror-radicle:
123+
runs-on: ubuntu-latest
124+
if: vars.RADICLE_MIRROR_ENABLED == 'true'
125+
steps:
126+
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
127+
with:
128+
fetch-depth: 0
129+
130+
- name: Setup Rust
131+
uses: dtolnay/rust-toolchain@efa25f7f19611383d5b0ccf2d1c8914531636bf9 # stable
132+
with:
133+
toolchain: stable
134+
135+
- name: Install Radicle
136+
run: |
137+
# Install via cargo (safer than curl|sh)
138+
cargo install radicle-cli --locked
139+
echo "$HOME/.cargo/bin" >> $GITHUB_PATH
140+
141+
- name: Mirror to Radicle
142+
run: |
143+
echo "${{ secrets.RADICLE_KEY }}" > ~/.radicle/keys/radicle
144+
chmod 600 ~/.radicle/keys/radicle
145+
rad sync --announce || echo "Radicle sync attempted"

0 commit comments

Comments
 (0)