Skip to content

Commit a78c2f7

Browse files
brunoborgesCopilot
andcommitted
Add proof files spec and first example
Introduce proof/ directory for compilable .java files that verify every pattern's modern code actually compiles. Includes: - specs/proof-spec.md with conventions and instructions - proof/language/TypeInferenceWithVar.java as the first example Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
1 parent c24f08a commit a78c2f7

File tree

2 files changed

+124
-0
lines changed

2 files changed

+124
-0
lines changed
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
import java.util.*;
2+
3+
/// Proof: type-inference-with-var
4+
/// Source: content/language/type-inference-with-var.yaml
5+
void main() {
6+
var map = new HashMap<String, List<Integer>>();
7+
for (var entry : map.entrySet()) {
8+
// clean and readable
9+
}
10+
}

specs/proof-spec.md

Lines changed: 114 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,114 @@
1+
# Proof Files Specification
2+
3+
## Overview
4+
5+
The `proof/` directory contains one `.java` file per pattern slug. Each file
6+
wraps the pattern's **modern code** in a compilable program, proving that every
7+
code snippet shown on the site actually compiles with the advertised JDK version.
8+
9+
Only the **modern code** is proven — the old code is what we're moving away from.
10+
11+
---
12+
13+
## Directory Layout
14+
15+
```
16+
proof/
17+
language/
18+
TypeInferenceWithVar.java
19+
RecordsForDataClasses.java
20+
SealedClasses.java
21+
...
22+
collections/
23+
ImmutableListCreation.java
24+
...
25+
strings/
26+
streams/
27+
concurrency/
28+
io/
29+
errors/
30+
datetime/
31+
security/
32+
tooling/
33+
enterprise/
34+
```
35+
36+
The folder structure mirrors `content/` — one subfolder per category.
37+
38+
---
39+
40+
## File Conventions
41+
42+
### Naming
43+
44+
- **Folder**: matches the category name (e.g., `language/`, `collections/`)
45+
- **File**: PascalCase version of the slug (e.g., `type-inference-with-var``TypeInferenceWithVar.java`)
46+
47+
### Structure
48+
49+
Each proof file follows this structure:
50+
51+
```java
52+
import java.util.*; // whatever imports the snippet needs
53+
54+
/// Proof: {slug}
55+
/// Source: content/{category}/{slug}.yaml
56+
void main() {
57+
// modern code from the pattern, adapted to compile
58+
}
59+
```
60+
61+
Key rules:
62+
63+
1. **Use implicit class and `void main()`** — Java 25 supports running single-file
64+
programs without an explicit class declaration
65+
2. **Add necessary imports** — the snippet JSON/YAML doesn't include imports;
66+
add whatever is needed for compilation
67+
3. **Add minimal scaffolding** — if the snippet references variables or types not
68+
defined in the code, add stub declarations so it compiles
69+
4. **Keep it minimal** — the goal is compilation proof, not a full test suite
70+
5. **Include the `/// Proof:` and `/// Source:` comments** — links the proof file
71+
back to the content source
72+
73+
### What to avoid
74+
75+
- Don't add runtime assertions or test logic
76+
- Don't restructure the modern code — keep it as close to the snippet as possible
77+
- Don't add the old code
78+
79+
---
80+
81+
## Running Proof Files
82+
83+
### Compile a single file
84+
85+
```bash
86+
java --enable-preview proof/language/TypeInferenceWithVar.java
87+
```
88+
89+
### Compile all proof files
90+
91+
```bash
92+
# Compile every proof file and report failures
93+
find proof -name '*.java' -exec sh -c '
94+
echo "Compiling: $1"
95+
java --enable-preview "$1" 2>&1 || echo "FAILED: $1"
96+
' _ {} \;
97+
```
98+
99+
### Prerequisites
100+
101+
- **Java 25+** — proof files use implicit classes and `void main()` which
102+
require `--enable-preview`
103+
104+
---
105+
106+
## Adding a Proof File
107+
108+
When adding a new pattern:
109+
110+
1. Create the content file under `content/category/slug.yaml`
111+
2. Create a proof file under `proof/category/SlugName.java`
112+
3. Copy the `modernCode` from the pattern into the `void main()` body
113+
4. Add imports and minimal scaffolding to make it compile
114+
5. Run `java --enable-preview proof/category/SlugName.java` to verify

0 commit comments

Comments
 (0)