Merged
Conversation
added 6 commits
April 14, 2026 22:51
ASSUMEs referenced by an @export-decorated DECIDE now become parameters of the exported function across the stack (typecheck schema, jl4-service HTTP/MCP evaluation, jl4-mlir lowering). Non-exported DECIDEs keep the original extern-import model. A new typecheck diagnostic rejects @export functions whose GIVEN or referenced ASSUME has a FUNCTION type — surfacing uniformly in jl4-lsp, jl4-wasm, and jl4-service deploy via a single CheckError variant. Also: truncate sanitized MCP property names to 60 chars with stable hash-suffix dedup so Anthropic's 64-char property-key regex is always satisfied (previously ~74-char names were rejected).
… deploy error - Lower the auto-mode rule-count threshold from 20 to 10 (docs + ExplorerPage). - Re-enable the deploy button with "Retry" on request failure instead of a dead "Error" label. - tool-card: let parameter rows wrap and use margin spacing so long names don't overflow.
Connection state could get pinned on 'connecting' if getConnectionState cached it before verifyConnection ran. Replace the in-flight promise dedup with a generation counter: mutators bump the gen via invalidate(), stale verifies discard their results in commit(), and getConnectionState always delegates to verifyConnection so callers get a terminal state. Also dedup identical state emits and guarantee initialize() ends on a terminal state regardless of /auth/session outcome. UX: the sidebar menu now shows Disconnect instead of the Sign-In link while in the connecting state, so the user can cancel a stuck attempt.
- Extend isFunctionTypeExpanded to recurse into MAYBE/LIST/etc. type arguments so MAYBE OF FUNCTION is also rejected at @export. - Unify collectFreeRefs / collectAllRefs into collectReferencedUniques (upstream filters handle semantic specialisation). - Replace the "force wrapper path" patch with a proper direct-AST fix: evaluateDirectAST now inlines the function body with LET bindings for both GIVEN parameters and referenced ASSUMEs when ASSUMEs are present. This keeps the fast path instead of falling back to the wrapper. - jl4-mlir: keep the exported function's extended ABI, and fill missing ASSUME args at internal call sites by calling the ASSUME's extern (one helper, invoked centrally from callL4). - Add unit tests: 7 ExportValidationSpec cases (including MAYBE wrappers and type synonyms), 2 jl4-mlir end-to-end lowering cases, and 2 jl4-service integration cases exercising the ASSUME eval path. - Drop the wrapperParams local rename in Backend/Jl4.hs.
Flow param name, type, and badge inline so the type sits behind wrapping names instead of pinned to the right column. Increase line-height for readability and drop the extra row gap/padding.
Function-typed ASSUMEs stay as 'ValAssumed' at runtime — calling them from an exported function produces a stuck "assumed term" error rather than a value, so the schema/catalogue would advertise a tool that can't actually be evaluated. Restore the strict typecheck rejection (covers GIVEN + referenced ASSUME) and remove @export from three legal examples whose bodies invoke function-typed ASSUMEs: - jl4/examples/legal/british-citizen-act.l4 - jl4/examples/legal/anti-social.l4 - jl4/examples/ok/assume-as-given.l4 (Test 4 only) Update the affected goldens and refresh the ASSUME doc and SKILL note to explain the runtime-evaluation reason behind the restriction. All 1114 tests across jl4-core, jl4, jl4-service, and jl4-mlir pass.
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
1 participant
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.
No description provided.