Repository navigation
kernel: move to upstream ShenOSKernel 43.1 at ec16a9f (deref-once type checker) - #31
Merged
Merged
Conversation
…e checker) Vendor the klambda built from unmodified Shen-Language/shen-sources ec16a9f, the merge of shen-sources#117. shen.by-hypothesis and shen.search-user-datatypes now dereference the checked term once per call, instead of once per hypothesis or datatype rule. (version) stays "43.1". The archive is ShenOSKernel-43.1-ec16a9f.tar.gz from pyrex41/shen-sources release upstream-ec16a9f, sha256 060066a8f84d9a2f7d41cb3b37b986a8d4653279752b739b5063cd648d9baacd. The kernel AOT modules are regenerated with scripts/codegen-kernel-aot.sh. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
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.
Moves the vendored klambda to upstream Shen-Language/shen-sources
ec16a9f. That is the 43.1 release plus shen-sources#117: the type checker now dereferences (copies) the checked term once pershen.by-hypothesis/shen.search-user-datatypescall, instead of once per hypothesis or datatype rule. Both functions also fail at once on an empty list.(version)is still"43.1".Kernel
ShenOSKernel-43.1-ec16a9f.tar.gzfrom https://github.com/pyrex41/shen-sources/releases/tag/upstream-ec16a9f. It is unmodified upstream sources, built with the repo'smake klambda/make release. sha256060066a8f84d9a2f7d41cb3b37b986a8d4653279752b739b5063cd648d9baacd..klfiles are replaced.kernel/tests/andkernel/stlib/are unchanged, and identical to the archive.t-star.klchanges. The other 12 changed files are gensym renumbering.crates/shen-rust/src/aot/kernel/*.rsis regenerated withscripts/codegen-kernel-aot.sh.kernel/klambda/PROVENANCE.md, the README and the CHANGELOG record the provenance.Gates (local, macOS arm64)
scripts/gates.sh: gates 0-10 all PASS. That covers shengen-codegen, fmt + clippy, build, cargo test, shen-check, tcb-audit, kernel-aot-audit, kernel-tests (canonical, 154/0), kernel-tests-debug, kernel-tests-debug-gc and cedar-equiv.read-file-as-bytelist: shen/load.shen: No such file or directory.Speed (b-typed,
/usr/bin/time -l, one pair)An earlier two-round trial of the same change (#117 without its empty-list early exit) left c-untyped and d-g5 flat.
🤖 Generated with Claude Code