CI: isolate .krml extraction rules for CBOR, COSE snapshots#259
Merged
Conversation
This commit has been entirely AI-generated by GitHub Copilot CLI 0.409.0 using Claude Opus 4.6. The prompts were: This directory contains the current state of EverParse pull request 244. Your job is to: 1. Refactor the rules in the local Makefiles in the src/cbor subdirectory tree, to create a new rule that extracts all .krml files for CBOR from the current behavior of the cbor-snapshot and cbor-test-snapshot rules from the main Makefile. 2. Create a rule in the main Makefile, cbor-extract-krml, depending on cbor-extract-pre, to use that new local rule, and make the existing cbor-snapshot and cbor-test-snapshot rules depend on that new rule. 3. Refactor the rules in the local Makefiles in the src/cose subdirectory tree, to create a new rule that extracts all .krml files for COSE from the current behavior of the cose-snapshot and cose-extract-test rules of the main Makefile. 4. Create a rule in the main Makefile, cose-extract-krml, depending on cddl, to use that new local rule, and make the existing cose-snapshot and cose-extract-test rules depend on that new rule. and Some rule in a COSE local Makefile seems to use `extract-krml` from its premises with `$<` or something similar. Please check and fix any such uses.
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.
Trying to answer Jonathan's question from FStarLang/karamel#679 (comment):
This PR isolates the Karamel calls and output in the nightly EverParse CI when automatically upgrading Karamel and producing the CBOR and COSE snapshots. With that, Karamel-specific output can be seen in Actions > Upgrade hashes, 3d doc, CBOR, COSE (nightly.yml) > Advance hashes > Generate CBOR snapshot with Karamel, and Actions > ... > Generate COSE snapshot with Karamel.
See for instance https://github.com/tahina-pro/quackyducky/actions/runs/22020102157/job/63627750125