Repository navigation
Bring leap seconds and IXDTF slices onto main - #7
Merged
Merged
Conversation
…pen) isValidKnown checks second 60 against tzdata's leap-seconds.list, which Spec/Leap.lean copies line for line; siSeconds counts SI seconds since 1972, each leap second included, fromSiSeconds goes back, and taiMinusUtc gives TAI - UTC. The statements are in Spec.lean, and all are proved but the two about fromSiSeconds, which still carry sorry. Tests: 300,000 inputs with 0 failures, 34,402 of them checked against the table, which the test script reads itself, and 9,381 SI seconds turned back into timestamps. A one-off cross-check with ERFA, through pyerfa, finds 0 differences. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
`fromSiSeconds` turns SI seconds since 1972 back into the one UTC timestamp, valid by the table and from 1972 on, that has them, and gives one for every second up to 9999-12-31T23:59:59Z. With it, all seven leap second statements are proved, and `lake comparator --paranoid` accepts all 24 theorems. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
Types, code, the spec from RFC 9557's grammar and rules, seven statements and a proof skeleton. The proofs, the command-line request, the tests and the page are still to come. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
…; two of three proof files The ixdtf request prints the printed form, the erroneous verdict for the example application and the first u-ca tag. The tests write RFC 9557's grammar and rules again in Python: 300,000 inputs with 0 failures, 6,992 of them IXDTF strings. The suffix parser's proofs are still open. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
Planted bugs that the random inputs caught only a few times (a zone part of .., an offset out of range, -00:00, a critical tag repeated with the same values) now each have fixed cases, with 48 edge strings in all. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
…ding The spec and page lenses of an independent pre-review, each finding checked by a separate agent, found these. None is in the proofs. - TAI - UTC during a leap second was claimed but no statement covered it: `Spec.taiMinusUtc_leapsBefore` now fixes `taiMinusUtc` for every valid timestamp, and vectors give it at the first and last leap second. - Before 1972, `Spec.siSeconds_eq` does fix `siSeconds`, as Unix seconds less 63072000; the page said no statement covered it, and called the number SI seconds without limit. - The table's transcription is part of the spec, checked by the reviewer and the tests but no proof; it now says so under What is not proved, with the file's version, update stamp and hash line. The comment in Spec/Leap.lean now quotes what the file says. - `known` is now also sent near misses and mutated strings, so its REJECT answer is tested; a missing tzdata file fails with a message. - Vectors now close the SI round trip of both ends of the table. - Smaller wording: `isValid` keeps no table, not the library; ERFA is derived from SOFA, not the IAU's own; "three numbers in a row" rests on `siSeconds_eq`, not the order statement. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
# Conflicts: # tests/TEST-RESULTS.md
fromsi gets the malformed numbers fromunix has, among them 1_000, which String.toInt? reads and decimal refuses. known gets fixed strings that must answer REJECT, not NOLEAP, and the hex cases parse has. These short lists now come first, so a run with a small count has them. Rerun of the cross-check recorded. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
…docs nanoda ran out of stack evaluating parseSuffix on the long examples. The vectors that read a string now get their Ext from parseExt_iff, with the grammar's checks made by the code's own functions, so no kernel runs the whole parser. All six kernels accept. README, SPEC.md and bar.toml now cover parseExt, Ext.print, Ext.lookup and Ext.erroneous, and list Spec/Ixdtf.lean and Rfc3339/IxdtfTypes.lean as part of the specification. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
The leap slice's new fixed test cases now run first with the IXDTF examples and edges. Test record and cross-check rerun. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
…est gaps, wording Spec.ixdtf_vectors now has every example of RFC 9557, sections 1.2, 3.3, 3.4 and 4.2, critical zones that agree with the offset, a critical -00:00 zone that does not, and [Z] read as a zone name. The page says parseExt keeps parse's relaxation on second 60. The tests add -00:00 zones, a value list sharing a first part, and two critical tags with one key. The Temporal categories follow what that Temporal refuses. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
…bserved Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow
RFC 9557 (IXDTF): time zones and tags after the timestamp, proved
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Brings the leap seconds and IXDTF slices onto main.
Main is at the merge of PR #3. PR #4 merged into the from-unix branch and PR #5 merged into the leap-seconds branch, so neither slice was on main. This branch merges the leap-seconds branch tip into main.
The local merge was clean, with no conflicts. Lean build passed in 49 jobs, with sorry only in Spec.lean placeholders. The combined test run gave 300000 inputs and 0 failures, and tests/TEST-RESULTS.md was regenerated from that run. The only change in the regenerated file against the branch record is the Oracle Python version, 3.12.3 here against 3.13.17 there.