Skip to content

Commit 0331f43

Browse files
hyperpolymathclaude
andcommitted
docs(cookbook): drop the recipes this PR removed; regenerate the recipe list
JUSTFILE-COOKBOOK.adoc: - remove the build-typescript, test-typescript and watch sections; - correct the build-all, test-all and clean dependency lines; - regenerate the appendix recipe list from `just --list` and the dependency graph from the Justfile; - add a banner naming the nine sections that describe recipes the Justfile has not defined since before this PR. COOKBOOK.adoc: drop the test-typescript and watch-typescript lines. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WRvDivYwLSeVCJUrfjic3f
1 parent 3eb2284 commit 0331f43

2 files changed

Lines changed: 36 additions & 86 deletions

File tree

‎docs/COOKBOOK.adoc‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -699,7 +699,6 @@ just verify-z3 # Run Z3
699699
700700
# Test
701701
just test-all # All tests
702-
just test-typescript # TypeScript tests
703702
704703
# Stats
705704
just stats # Lines of code
@@ -716,7 +715,6 @@ just clean # Build artifacts
716715
just clean-all # Everything
717716
718717
# Development
719-
just watch-typescript # Watch mode
720718
just ci # Full CI pipeline
721719
just check-tools # Check dependencies
722720
----

‎docs/JUSTFILE-COOKBOOK.adoc‎

Lines changed: 36 additions & 84 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,8 @@ v1.0, 2025-11-22
1313

1414
This cookbook documents all `just` recipes in the Absolute Zero project. Every recipe is explained with examples, flags, and common usage patterns.
1515

16+
WARNING: `just --list` is authoritative. The Appendix recipe list and dependency graph were regenerated from it on 2026-10-01. Nine per-recipe sections below describe recipes the Justfile no longer defines: `build-z3`, `check-tools`, `clean-all`, `docs-adoc`, `docs-all`, `docs-proof-stats`, `install-help`, `loc` and `quick-check`. Treat them as historical until this cookbook is rewritten.
17+
1618
=== Quick Reference
1719

1820
[source,bash]
@@ -30,20 +32,20 @@ just ci # Run full CI pipeline
3032

3133
Build all proof systems and interpreters.
3234

33-
*Dependencies*: build-affinescript, build-coq, build-lean, build-agda, build-isabelle, build-typescript
35+
*Dependencies*: build-coq, build-lean, build-agda, build-isabelle, build-mizar, build-idris
3436

3537
[source,bash]
3638
----
3739
just build-all
3840
----
3941

4042
*What it does*:
41-
1. Builds AffineScript interpreters
42-
2. Compiles Coq proofs
43-
3. Compiles Lean 4 proofs
44-
4. Compiles Agda proofs
45-
5. Builds Isabelle/HOL proofs
46-
6. Compiles TypeScript (deprecated, will be removed)
43+
1. Compiles Coq proofs
44+
2. Compiles Lean 4 proofs
45+
3. Compiles Agda proofs
46+
4. Builds Isabelle/HOL proofs
47+
5. Checks Mizar proofs
48+
6. Builds the Idris2 ABI
4749

4850
*Exit codes*:
4951
- `0`: All builds successful
@@ -139,20 +141,6 @@ just verify-z3
139141
z3 -T:60 proofs/z3/cno_properties.smt2 # 60 second timeout
140142
----
141143

142-
=== build-typescript
143-
144-
⚠️ **DEPRECATED**: Will be removed. Use Deno instead.
145-
146-
[source,bash]
147-
----
148-
just build-typescript
149-
----
150-
151-
*Migration path*:
152-
- Replace with `deno task build`
153-
- Port TypeScript files to Deno
154-
- Remove `ts/` directory
155-
156144
== Verification Recipes
157145

158146
=== verify-all
@@ -252,33 +240,15 @@ just verify-z3
252240

253241
Run all tests (unit, integration, proofs).
254242

255-
*Dependencies*: test-interpreters, test-proofs
243+
*Dependencies*: test-proofs
256244

257245
[source,bash]
258246
----
259247
just test-all
260248
----
261249

262250
*Test suites*:
263-
1. Interpreter tests (Brainfuck, Whitespace, Malbolge)
264-
2. Proof verification tests
265-
3. Example CNO validation
266-
267-
=== test-typescript
268-
269-
⚠️ **DEPRECATED**: Use `deno test` instead.
270-
271-
[source,bash]
272-
----
273-
just test-typescript
274-
----
275-
276-
*Migration*:
277-
[source,bash]
278-
----
279-
# New approach:
280-
deno test --allow-read tests/
281-
----
251+
1. Proof verification tests (`test-proofs`)
282252

283253
== Container Recipes
284254

@@ -405,7 +375,7 @@ just docs-adoc
405375

406376
Clean all build artifacts.
407377

408-
*Dependencies*: clean-coq, clean-lean, clean-typescript, clean-affinescript
378+
*Dependencies*: clean-coq, clean-lean
409379

410380
[source,bash]
411381
----
@@ -415,8 +385,6 @@ just clean
415385
*What gets deleted*:
416386
- Coq: `*.vo`, `*.vok`, `*.vos`, `*.glob`
417387
- Lean: `.lake/` directory
418-
- TypeScript: `node_modules/`, `dist/`
419-
- AffineScript: `lib/`
420388

421389
=== clean-coq
422390

@@ -521,19 +489,6 @@ just quick-check || exit 1
521489

522490
== Development Recipes
523491

524-
=== watch
525-
526-
Watch TypeScript files for changes.
527-
528-
⚠️ **DEPRECATED**: Use `deno task dev` instead.
529-
530-
[source,bash]
531-
----
532-
just watch
533-
# New:
534-
deno task dev
535-
----
536-
537492
=== format
538493

539494
Format AffineScript code.
@@ -896,57 +851,52 @@ Available recipes:
896851
build-agda
897852
build-all
898853
build-coq
854+
build-elm
855+
build-idris
899856
build-isabelle
900857
build-lean
901-
build-affinescript
902-
build-typescript
903-
check-tools
858+
build-mizar
904859
ci
905860
clean
906-
clean-all
907861
clean-coq
862+
clean-elm
908863
clean-lean
909-
clean-affinescript
910-
clean-typescript
911864
container-build
912865
container-shell
913866
container-test-all
914867
container-verify
915868
default
916-
docs-adoc
917-
docs-all
918-
docs-proof-stats
919869
docker-build
920870
docker-verify
871+
docs
872+
echidna-check
873+
echidna-complete FILE
874+
echidna-list
875+
echidna-repl
876+
echidna-suggest FILE
877+
echidna-verify
921878
format
922879
help
923-
install-help
924-
install-npm
925-
install-provers-fedora
926-
install-provers-ubuntu
927-
install-python
928880
lint
929-
loc
930881
paper
931882
proof-status
932-
quick-check
933-
run-brainfuck FILE
934-
run-example LANG FILE
935-
run-malbolge FILE
936-
run-whitespace FILE
883+
run-elm
937884
stats
938885
test-all
939-
test-interpreters
940886
test-proofs
941-
test-typescript
887+
verify
942888
verify-agda
943889
verify-all
944890
verify-coq
891+
verify-gate-selftest
892+
verify-idris
945893
verify-isabelle
946894
verify-lean
895+
verify-lean-core
896+
verify-mizar
947897
verify-z3
948898
view-docs
949-
watch
899+
wiki-sync
950900
----
951901

952902
=== Recipe Dependencies Graph
@@ -955,21 +905,23 @@ Available recipes:
955905
----
956906
ci
957907
├── build-all
958-
│ ├── build-affinescript
959908
│ ├── build-coq
960909
│ ├── build-lean
961910
│ ├── build-agda
962911
│ ├── build-isabelle
963-
│ └── build-typescript
912+
│ ├── build-mizar
913+
│ └── build-idris
964914
├── test-all
965-
│ ├── test-interpreters
966915
│ └── test-proofs
967916
└── verify-all
968917
├── verify-coq (depends on build-coq)
969918
├── verify-z3
970919
├── verify-lean
971920
├── verify-agda (depends on build-agda)
972-
└── verify-isabelle (depends on build-isabelle)
921+
├── verify-isabelle (depends on build-isabelle)
922+
├── verify-mizar (depends on build-mizar)
923+
├── verify-idris (depends on build-idris)
924+
└── verify-gate-selftest
973925
----
974926

975927
---

0 commit comments

Comments
 (0)