Skip to content

Fix Float16 bootstrap totality through carrier division - #48

Closed
isomorphisms wants to merge 1 commit into
float32-primitivefrom
fix/float16-bootstrap-totality
Closed

Fix Float16 bootstrap totality through carrier division#48
isomorphisms wants to merge 1 commit into
float32-primitivefrom
fix/float16-bootstrap-totality

Conversation

@isomorphisms

Copy link
Copy Markdown
Owner

Wegert's new hosted Edric/GLSL diagnostic reached a concrete failure before the shader backend: the float32-primitive head cannot bootstrap because Prelude.Float16 is under %default total while several calls to inherited prim__div_Double are marked non-covering by the compiler.

This keeps the Float16 module total rather than weakening it to %default covering. It follows the file's existing pattern for prim__mod_Integer and wraps only the carrier-level division primitive calls in assert_total:

  • the bounded halfStep recursion;
  • infinity construction used by binary16 overflow;
  • magnitude/step scaling before round-to-nearest-even;
  • the Fractional Float16 carrier division.

No numerical expression, rounding boundary, threshold, or public type changes.

The intended acceptance is the existing PR #6 bootstrap/source-profile CI plus the downstream Wegert host probe. If bootstrap advances and exposes a different real failure, that remains visible rather than being masked here.

Copy link
Copy Markdown
Owner Author

The focused fix is green on its own compiler boundary: source-profile completed successfully, including both Bootstrap compiler and Check Idriç Float16 coercion source profile; the private-Scheme-path job is also green.

That closes the specific prim__div_Double totality defect exposed by the Wegert host probe without weakening Prelude.Float16 to covering. The next downstream boundary is now the separate Wegert lane using this exact branch with the Mali mediump backend.

Copy link
Copy Markdown
Owner Author

Classification: SUPERSEDED by #49.

This PR preserved the then-needed bootstrap totality fix for Float16 division when the implementation was carried through Double. #49 deliberately removes that Double carrier, so this workaround is no longer an independent desired state.

This intermediate PR should not merge. Its branch is retained as #49's current stack base until the final Float16 line is rebased or retargeted onto current Idriç.

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.

1 participant