Skip to content

Commit 603fe88

Browse files
denisecasedenisecase
committed
initial
0 parents  commit 603fe88

25 files changed

+934
-0
lines changed

‎.editorconfig‎

Lines changed: 122 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,122 @@
1+
# REQ.UNIVERSAL: All professional GitHub project repositories MUST include .editorconfig.
2+
# WHY: Establish a cross-editor baseline so diffs stay clean and formatting is consistent.
3+
# ALT: Repository may omit .editorconfig ONLY if formatting is enforced equivalently by CI and formatter tooling.
4+
# CUSTOM: Adjust indent_size defaults only if organizational standards change; keep stable across projects.
5+
# NOTE: Sections are ordered by editorial importance, not strict alphabetical order.
6+
# EditorConfig is documented at https://editorconfig.org
7+
8+
[*.{editorconfig}]
9+
root = true
10+
11+
# === Global defaults (always apply) ===
12+
13+
[*]
14+
# WHY: Normalize line endings and encoding across Windows, macOS, and Linux.
15+
end_of_line = lf
16+
charset = utf-8
17+
18+
# WHY: Newline at EOF avoids noisy diffs and tool warnings.
19+
insert_final_newline = true
20+
21+
# WHY: Remove accidental whitespace noise in diffs.
22+
trim_trailing_whitespace = true
23+
24+
# WHY: Default to 2 spaces for configs and markup; language-specific overrides follow.
25+
indent_style = space
26+
indent_size = 2
27+
28+
29+
# === Build systems (special rules) ===
30+
31+
[Makefile]
32+
# WHY: Makefiles require tabs.
33+
indent_style = tab
34+
35+
[*.mk]
36+
# WHY: Makefile includes require tabs.
37+
indent_style = tab
38+
39+
40+
# === Citation and metadata ===
41+
42+
[CITATION.cff]
43+
# WHY: Citation tooling expects stable YAML formatting.
44+
indent_size = 2
45+
indent_style = space
46+
47+
48+
# === Markup and documentation ===
49+
50+
[*.md]
51+
# WHY: Keep Markdown clean; use explicit <br> for hard line breaks.
52+
indent_size = 2
53+
trim_trailing_whitespace = true
54+
55+
[*.{tex,cls,sty}]
56+
# WHY: LaTeX convention is 2 spaces.
57+
indent_size = 2
58+
indent_style = space
59+
60+
[*.xml]
61+
# WHY: XML convention is 2 spaces.
62+
indent_size = 2
63+
indent_style = space
64+
65+
[*.{yml,yaml}]
66+
# WHY: YAML convention is 2 spaces.
67+
indent_size = 2
68+
indent_style = space
69+
70+
71+
# === Data and configuration ===
72+
73+
[*.{json,jsonc,jsonl,ndjson}]
74+
# WHY: JSON tooling typically expects 2 spaces.
75+
indent_size = 2
76+
indent_style = space
77+
78+
[*.toml]
79+
# WHY: TOML often follows 4-space indentation in many projects.
80+
indent_size = 4
81+
indent_style = space
82+
83+
84+
# === Programming languages ===
85+
86+
[*.{js,ts}]
87+
# WHY: JS/TS ecosystem commonly uses 2 spaces.
88+
indent_size = 2
89+
indent_style = space
90+
91+
[*.{py,pyi}]
92+
# WHY: Python convention is 4 spaces.
93+
indent_size = 4
94+
indent_style = space
95+
96+
[*.ps1]
97+
# WHY: PowerShell convention is 4 spaces.
98+
indent_size = 4
99+
indent_style = space
100+
101+
[*.{c,cpp,h,java,cs,go,rs}]
102+
# WHY: Many C-family and systems languages commonly use 4 spaces.
103+
indent_size = 4
104+
indent_style = space
105+
106+
[*.{sh,bash}]
107+
# WHY: Shell script convention is 2 spaces.
108+
indent_size = 2
109+
indent_style = space
110+
111+
112+
# === Proof assistants and formal languages ===
113+
114+
[*.lean]
115+
# WHY: Lean 4 convention is 2 spaces; matches Mathlib and stdlib style.
116+
indent_size = 2
117+
indent_style = space
118+
119+
[*.{v,vo}]
120+
# WHY: Coq convention is 2 spaces.
121+
indent_size = 2
122+
indent_style = space

‎.gitattributes‎

Lines changed: 117 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,117 @@
1+
# REQ.UNIVERSAL: All professional GitHub project repositories MUST include .gitattributes.
2+
# WHY: Ensure consistent line endings, diff behavior, and repository metadata
3+
# across Windows, macOS, and Linux.
4+
# ALT: Repository may omit .gitattributes ONLY if equivalent normalization is
5+
# enforced by tooling and CI (rare and fragile).
6+
# CUSTOM: Update file-type rules only when introducing new languages or artifact types.
7+
8+
# WHY: Auto-detect text files and normalize line endings to avoid cross-platform drift.
9+
* text=auto
10+
11+
12+
# === Source Code ===
13+
14+
# WHY: Python and shell scripts must use LF for CI/CD, Linux environments, and containers.
15+
*.py text eol=lf
16+
*.sh text eol=lf
17+
18+
# WHY: PowerShell convention on Windows uses CRLF.
19+
*.ps1 text eol=crlf
20+
21+
22+
# === Markup and Documentation ===
23+
24+
# WHY: Documentation and markup files use LF; standard for cross-platform tooling.
25+
*.bib text eol=lf
26+
*.cls text eol=lf
27+
*.md text eol=lf
28+
*.sty text eol=lf
29+
*.tex text eol=lf
30+
31+
32+
# === Configuration and Data (Text) ===
33+
34+
# WHY: Configuration and structured text formats use LF for stable diffs.
35+
*.json text eol=lf
36+
*.jsonc text eol=lf
37+
*.jsonl text eol=lf
38+
*.ndjson text eol=lf
39+
*.toml text eol=lf
40+
*.yaml text eol=lf
41+
*.yml text eol=lf
42+
43+
44+
# === GitHub Metadata ===
45+
46+
# WHY: Exclude documentation and tests from GitHub language statistics.
47+
docs/** linguist-documentation
48+
tests/** linguist-documentation
49+
50+
51+
# === Notebooks ===
52+
53+
# WHY: Jupyter notebooks require specialized diff and merge handling.
54+
*.ipynb diff=jupyternotebook
55+
*.ipynb merge=jupyternotebook
56+
57+
58+
# === Databases (Binary) ===
59+
60+
# WHY: Database files are binary; prevent text normalization and meaningless diffs.
61+
*.db binary
62+
*.duckdb binary
63+
*.sqlite binary
64+
*.sqlite3 binary
65+
66+
# === Columnar / Analytical Data (Binary) ===
67+
68+
# WHY: Columnar and analytical data formats are binary; diffs are not meaningful.
69+
*.arrow binary
70+
*.avro binary
71+
*.feather binary
72+
*.orc binary
73+
*.parquet binary
74+
75+
76+
# === Office, BI, PDFs, and Compressed Artifacts (Binary) ===
77+
78+
# WHY: Office documents, BI files, PDFs, and compressed artifacts are binary.
79+
*.7z binary
80+
*.bz2 binary
81+
*.docx binary
82+
*.gz binary
83+
*.pbix binary
84+
*.pbit binary
85+
*.pdf binary
86+
*.pptx binary
87+
*.rar binary
88+
*.tar binary
89+
*.tgz binary
90+
*.xls binary
91+
*.xlsm binary
92+
*.xlsx binary
93+
*.xz binary
94+
*.zip binary
95+
96+
97+
# === Proof Assistants ===
98+
99+
# WHY: Lean files must use LF for cross-platform consistency and CI.
100+
*.lean text eol=lf
101+
102+
# WHY: Lean build artifacts are binary; prevent normalization and meaningless diffs.
103+
*.olean binary
104+
*.ilean binary
105+
*.trace binary
106+
107+
# WHY: Coq source uses LF; compiled objects are binary.
108+
*.v text eol=lf
109+
*.vo binary
110+
*.vok binary
111+
*.vos binary
112+
*.glob binary
113+
114+
# === Lean Build System ===
115+
116+
# WHY: Lake build directory should be excluded but if tracked, treat as binary.
117+
.lake/** binary

‎.github/dependabot.yml‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
# WHY: Automatically updates GitHub Actions to latest versions
2+
# OBS: Runs monthly to keep actions secure and up-to-date
3+
# REQ: Keep this file to maintain security patches in workflows
4+
5+
version: 2
6+
7+
updates:
8+
- package-ecosystem: "github-actions" # WHY: Updates action versions in workflows
9+
directory: "/" # WHY: Scan all .github/workflows/*.yml files
10+
schedule:
11+
interval: "monthly" # WHY: Monthly updates balance freshness vs notification noise
12+
commit-message:
13+
prefix: "(deps)" # WHY: Conventional commit format for changelog tools

‎.github/workflows/ci.yml‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
# WHY-FILE: Minimal checks for specification repositories.
2+
# REQ: Any check that can be run locally MUST be available locally via pre-commit.
3+
# REQ: CI MUST NOT introduce arbitrary rules that are not reproducible locally.
4+
# OBS: CI does not introduce additional style rules beyond repo configuration.
5+
6+
# REQ: Verify Lean proofs compile on every push and PR.
7+
# WHY: Proofs are the deliverable; broken proofs must not merge.
8+
9+
name: Lean Action CI
10+
11+
on:
12+
push:
13+
pull_request:
14+
workflow_dispatch:
15+
16+
jobs:
17+
18+
hygiene:
19+
name: Repository checks
20+
runs-on: ubuntu-latest
21+
22+
permissions:
23+
contents: read
24+
25+
steps:
26+
- name: 1) Checkout repository code
27+
# WHY: Needed to access files for checks.
28+
uses: actions/checkout@v6
29+
30+
- name: 2) Run pre-commit (all files)
31+
# WHY: Single source of truth for locally runnable quality gates.
32+
# OBS: Fails if hooks would modify files; does not commit changes.
33+
uses: pre-commit/action@v3.0.1
34+
with:
35+
extra_args: --all-files
36+
37+
build:
38+
runs-on: ubuntu-latest
39+
40+
steps:
41+
- uses: actions/checkout@v6
42+
- uses: leanprover/lean-action@v1

‎.github/workflows/links.yml‎

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
# WHY-FILE: Automated link checking.
2+
# OBS: Behavior is configured in lychee.toml in this repository.
3+
# OBS: Runs on pull requests and monthly on schedule; manual trigger always available.
4+
5+
name: Check Links
6+
7+
on:
8+
workflow_dispatch: # WHY: Manual trigger - always available
9+
10+
pull_request: # WHY: Validates PR links before merge
11+
12+
schedule:
13+
- cron: "0 6 1 * *" # WHY: Runs monthly (1st of month)
14+
15+
concurrency:
16+
# WHY: Prevent multiple simultaneous link checks on same ref
17+
group: link-check-${{ github.ref }}
18+
cancel-in-progress: true
19+
20+
jobs:
21+
lychee:
22+
runs-on: ubuntu-latest
23+
24+
permissions:
25+
contents: read
26+
issues: write
27+
pull-requests: write
28+
29+
steps:
30+
- name: 1) Checkout repository code
31+
uses: actions/checkout@v6 # OBS: v6 current as of Dec 2025
32+
33+
- name: 2) Check links with Lychee
34+
uses: lycheeverse/lychee-action@v2
35+
with:
36+
args: >
37+
--config lychee.toml
38+
--user-agent "${{ github.repository }}/lychee"
39+
'./**/*.bib'
40+
'./**/*.md'
41+
'./**/*.html'
42+
'./**/*.tex'
43+
'./**/*.yml'
44+
'./**/*.yaml'
45+
lycheeVersion: latest # OBS: Always use latest lychee release
46+
env:
47+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
48+
49+
- name: 3) Comment on PR if links broken
50+
if: failure() && github.event_name == 'pull_request'
51+
uses: actions/github-script@v8
52+
with:
53+
script: |
54+
const runUrl = `${context.payload.repository.html_url}/actions/runs/${context.runId}`;
55+
const comment = [
56+
"## Link Check Results",
57+
"",
58+
`Some links appear broken. Check the workflow logs: ${runUrl}`,
59+
].join("\n");
60+
61+
await github.rest.issues.createComment({
62+
issue_number: context.issue.number,
63+
owner: context.repo.owner,
64+
repo: context.repo.repo,
65+
body: comment,
66+
});
67+
68+
- name: 4) Create issue for scheduled failures # WHY: Track broken links found during scheduled checks
69+
# OBS: Only creates issue if none already open with 'broken-links' label
70+
if: failure() && github.event_name == 'schedule'
71+
uses: actions/github-script@v8
72+
with:
73+
script: |
74+
const date = new Date().toISOString().split("T")[0];
75+
const title = `Link Check Failed - ${date}`;
76+
const runUrl = `${context.payload.repository.html_url}/actions/runs/${context.runId}`;
77+
const body = `Monthly link check found broken links.\n\nWorkflow logs: ${runUrl}`;
78+
79+
const existing = await github.rest.issues.listForRepo({
80+
owner: context.repo.owner,
81+
repo: context.repo.repo,
82+
labels: "broken-links",
83+
state: "open",
84+
});
85+
86+
if (existing.data.length === 0) {
87+
await github.rest.issues.create({
88+
owner: context.repo.owner,
89+
repo: context.repo.repo,
90+
title,
91+
body,
92+
labels: ["maintenance", "broken-links"],
93+
});
94+
}

‎.gitignore‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
/.lake/
2+
PRIVATE_NOTES.md

0 commit comments

Comments
 (0)