Skip to content

Automate proof script: add JBang CI runner for proof/ scripts#113

Closed
Copilot wants to merge 37 commits intoslug-prooffrom
copilot/automate-proof-script
Closed

Automate proof script: add JBang CI runner for proof/ scripts#113
Copilot wants to merge 37 commits intoslug-prooffrom
copilot/automate-proof-script

Conversation

Copy link
Contributor

Copilot AI commented Feb 27, 2026

No automated way existed to run all the proof scripts in the proof/ directory to verify they compile and execute correctly. This adds a JBang runner script and a GitHub Actions workflow as a CI gate for all proof scripts.

New: html-generators/proof.java

JBang script (Java 25) that:

  • Walks proof/**/*.java for all standalone JBang proof scripts
  • Runs each via jbang --quiet <file>, checking the exit code
  • Reports per-script OK/FAILED/TIMEOUT, exits 1 on any failure
  • --list flag lists all proof scripts

New: proof/ directory (105 scripts)

One JBang script per pattern (//JAVA 25+), organized by category mirroring content/:

proof/language/TypeInferenceWithVar.java
proof/collections/ImmutableListCreation.java
proof/streams/StreamTolist.java
...

Each script has a /// Proof: slug-name header and demonstrates the modern approach from the corresponding content YAML file.

New: .github/workflows/proof.yml

Runs jbang html-generators/proof.java on push/PR when proof/** changes, using Java 25 + JBang.

Supporting changes

  • CONTRIBUTING.md: Added step to create a proof script when adding a new pattern
  • html-generators/README.md: Added proof.java to the files table and documented the proof.yml workflow
  • .github/copilot-instructions.md: Added proof/ to the project structure and documented the proof script convention
Original prompt

This section details on the original issue you should resolve

<issue_title>[Feature] Automate proof script</issue_title>
<issue_description>### Describe the feature

We now have proof but we don't have a way to run all of them to verify all of them work.

Why would this be useful?

No response

Alternatives considered

No response</issue_description>

Comments on the Issue (you are @copilot in this section)


✨ Let Copilot coding agent set things up for you — coding agent works faster and does higher quality work when set up for your repo.

Copilot AI and others added 30 commits February 26, 2026 06:58
Co-authored-by: brunoborges <129743+brunoborges@users.noreply.github.com>
- Add 'it=🇮🇹 Italiano' to html-generators/locales.properties
- Create translations/strings/it.yaml with full UI string translations
- Create translations/content/it/ with 112 content translation files
  covering all categories: language, collections, strings, streams,
  concurrency, io, errors, datetime, security, tooling, enterprise

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Replace the bare → arrow in card footers with a translated
"learn more →" label for all 9 locales, making the clickable
action explicit.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add "learn more →" text to index card arrow links
Co-authored-by: brunoborges <129743+brunoborges@users.noreply.github.com>
…nt-italian

[WIP] Translate site content to Italian
Update French tagline for clarity
Co-authored-by: brunoborges <129743+brunoborges@users.noreply.github.com>
…to-ioprintln

Use IO.println in modern code slugs
Translate 10 collections and 10 concurrency pattern YAML files to Turkish.

- translations/content/tr/collections/collectors-teeing.yaml
- translations/content/tr/collections/copying-collections-immutably.yaml
- translations/content/tr/collections/immutable-list-creation.yaml
- translations/content/tr/collections/immutable-map-creation.yaml
- translations/content/tr/collections/immutable-set-creation.yaml
- translations/content/tr/collections/map-entry-factory.yaml
- translations/content/tr/collections/reverse-list-iteration.yaml
- translations/content/tr/collections/sequenced-collections.yaml
- translations/content/tr/collections/stream-toarray-typed.yaml
- translations/content/tr/collections/unmodifiable-collectors.yaml
- translations/content/tr/concurrency/completablefuture-chaining.yaml
- translations/content/tr/concurrency/concurrent-http-virtual.yaml
- translations/content/tr/concurrency/executor-try-with-resources.yaml
- translations/content/tr/concurrency/lock-free-lazy-init.yaml
- translations/content/tr/concurrency/process-api.yaml
- translations/content/tr/concurrency/scoped-values.yaml
- translations/content/tr/concurrency/stable-values.yaml
- translations/content/tr/concurrency/structured-concurrency.yaml
- translations/content/tr/concurrency/thread-sleep-duration.yaml
- translations/content/tr/concurrency/virtual-threads.yaml

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: brunoborges <129743+brunoborges@users.noreply.github.com>
- 6 datetime files: date-formatting, duration-and-period, hex-format,
  instant-precision, java-time-basics, math-clamp
- 16 enterprise files: ejb-timer-vs-jakarta-scheduler, ejb-vs-cdi,
  jdbc-resultset-vs-jpa-criteria, jdbc-vs-jooq, jdbc-vs-jpa,
  jndi-lookup-vs-cdi-injection, jpa-vs-jakarta-data,
  jsf-managed-bean-vs-cdi-named, manual-transaction-vs-declarative,
  mdb-vs-reactive-messaging, servlet-vs-jaxrs,
  singleton-ejb-vs-cdi-application-scoped, soap-vs-jakarta-rest,
  spring-api-versioning, spring-null-safety-jspecify,
  spring-xml-config-vs-annotations

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Translate 22 content YAML files to Turkish:
- errors: helpful-npe, multi-catch, null-in-switch, optional-chaining,
  optional-orelsethrow, record-based-errors, require-nonnull-else
- io: deserialization-filters, file-memory-mapping, files-mismatch,
  http-client, inputstream-transferto, io-class-console-io, path-of,
  reading-files, try-with-resources-effectively-final, writing-files
- security: key-derivation-functions, pem-encoding, random-generator,
  strong-random, tls-default

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add missing `cards.learnMore` key to Italian UI strings
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot AI and others added 4 commits February 27, 2026 14:46
- 11 streams files: collectors-flatmapping, optional-ifpresentorelse, optional-or,
  predicate-not, stream-gatherers, stream-iterate-predicate, stream-mapmulti,
  stream-of-nullable, stream-takewhile-dropwhile, stream-tolist, virtual-thread-executor
- 7 strings files: string-chars-stream, string-formatted, string-indent-transform,
  string-isblank, string-lines, string-repeat, string-strip
- 8 tooling files: aot-class-preloading, built-in-http-server, compact-object-headers,
  jfr-profiling, jshell-prototyping, junit6-with-jspecify, multi-file-source,
  single-file-execution

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Bring generate.py up to parity with generate.java (the source of truth).
Previously the Python script only produced English output and was missing
many features added to the Java generator.

Added:
- Full multi-locale build support (--locale, --all-locales flags)
- UI string loading from translations/strings/ with English fallback
- Content translation merging (resolveSnippet) from translations/content/
- Dotted-key token regex (e.g. {{nav.allPatterns}})
- Multi-pass token replacement (3 passes for nested tokens)
- Locale picker, hreflang links, and i18n script block rendering
- Contribute issue URLs (code, translation, suggest)
- Locale-aware URLs in nav arrows, related cards, and index cards
- i18n-aware difficultyDisplay and supportBadge lookups
- Locales loaded from html-generators/locales.properties

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…ions

[WIP] Add Turkish translations to the site
Copilot AI and others added 2 commits February 27, 2026 23:21
- Add html-generators/proof.java: JBang script (Java 25) that reads all
  content YAML files, finds those with an optional proofCode field, and
  runs each through JShell to verify they compile and execute correctly.
  Supports --list flag to show which patterns have/lack proofCode.

- Add .github/workflows/proof.yml: GitHub Actions workflow that triggers
  on content changes (push/PR) and runs jbang html-generators/proof.java
  with Java 25 + JBang.

- Add proofCode field to 10 representative patterns across categories:
  language (var, text-blocks, records, switch, instanceof), collections
  (immutable-list), streams (stream-tolist), strings (isBlank),
  concurrency (virtual-threads), datetime (java-time-basics)

- Update generate.java and generate.py to exclude proofCode from the
  search index (snippets.json) since it is CI-only metadata.

- Update content/template.json, html-generators/README.md,
  CONTRIBUTING.md, and copilot-instructions.md to document the new field.

Co-authored-by: brunoborges <129743+brunoborges@users.noreply.github.com>
…e of escaped ones

Co-authored-by: brunoborges <129743+brunoborges@users.noreply.github.com>
Copilot AI changed the title [WIP] Add automation for proof script verification Automate proof script: add proofCode field + JShell CI runner Feb 27, 2026
@brunoborges
Copy link
Member

@copilot you completely missed the proof folder that already contains java code!

… proofCode

The existing proof/ directory (from a parallel branch) contains 105 individual
JBang scripts - one per pattern - that were missed in the initial approach.

Changes:
- Add all 105 proof/**/*.java scripts from proof/ directory
- Rewrite html-generators/proof.java to run proof/**/*.java via jbang
  instead of parsing YAML proofCode fields through JShell
- Revert the proofCode field additions from 10 YAML content files
- Revert proofCode from generate.java/generate.py EXCLUDED_KEYS
- Revert proofCode from content/template.json
- Update .github/workflows/proof.yml to trigger on proof/** changes
- Update html-generators/README.md, CONTRIBUTING.md, and
  .github/copilot-instructions.md to document the proof/ directory

Co-authored-by: brunoborges <129743+brunoborges@users.noreply.github.com>
Copy link
Contributor Author

Copilot AI commented Feb 27, 2026

@copilot you completely missed the proof folder that already contains java code!

Fixed in commit 2564051. The proof/ directory with 105 existing JBang scripts was brought in and html-generators/proof.java was rewritten to run all proof/**/*.java files via jbang. The workflow now triggers on proof/** changes. I also reverted the YAML proofCode additions that were incorrect.

Copilot AI changed the title Automate proof script: add proofCode field + JShell CI runner Automate proof script: add JBang CI runner for proof/ scripts Feb 27, 2026
@brunoborges
Copy link
Member

@copilot this PR should be targeting the slug-proof branch, which already contains the proof folder

Copy link
Contributor Author

Copilot AI commented Feb 28, 2026

@copilot this PR should be targeting the slug-proof branch, which already contains the proof folder

Changing a PR's base branch requires action in the GitHub UI — I can't do that directly. To retarget this PR:

  1. Open the PR on GitHub
  2. Click Edit next to the PR title
  3. Change the base dropdown from main to copilot/implement-proof-for-slugs

Once the base is changed, the 105 proof/**/*.java files will disappear from the diff (since they already exist in that branch), leaving only the meaningful additions: html-generators/proof.java, .github/workflows/proof.yml, and the documentation updates.

@brunoborges brunoborges changed the base branch from main to slug-proof February 28, 2026 00:59
@brunoborges brunoborges deleted the copilot/automate-proof-script branch February 28, 2026 01:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

[Feature] Automate proof script

3 participants