lib: Requalify: better document annotation #813
Merged
Conversation
This file contains 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
Xaphiosis
added
enhancement
arch-split
|
Looks like this needs more work, some issues with creative requalify in CRefine got me :( |
corlewis
approved these changes
Aug 27, 2024
Previous attempts to update the code to allow ctrl+clicking on names resulted in markup overlap errors for arch_requalify commands. This was due to a misconception that YXML strings already containing correct position information (e.g. obtained via Parse.const) would be used directly by Proof_context.read_const/read_type_name. This is not the case. Instead, position information is adjusted for the content length, and since we add a prefix for L4V_ARCH, we got annotation that did not match the document text. After hours of digging to uncover the above issue, we get this: * the "check_parsed_nm" in gen_requalify was not an extra check, but a hook to do document annotation; updated comments * use Proof_Context.check_const/check_type_name with user-supplied name and parsed position of Parse.name, and manually report resulting markup (do not use previously resolved name as it could point to a hidden const/type) * since the above works for arch_requalify_const, the normal requalify_const becomes a simpler instance of it * the whole Parse.const/Parse.typ was a red herring and ultimately did not add anything to the code except for read_const/read_type_name interaction; removed The resulting code is simpler; large cautionary comments remain for future generations. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Document/test surprising interactions of hide_const, locales and requalify for the purposes of temporarily making arch-specific constants visible in theory scope. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Xaphiosis
force-pushed
the
arch-split_requalify_anno
branch
from
c11037f to
e949698
Compare
|
Updated to fix the lookup of a resolved name, because somehow it's possible to look up a short name and get a qualified name that's been hidden... which for whatever reason is fine to create aliases to, but not find to resolve to (we use this in Kernel_C for temporarily making things visible to C Parser). |
lsf37
approved these changes
Aug 27, 2024
corlewis
approved these changes
Aug 28, 2024
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.
Previous attempts to update the code to allow ctrl+clicking on names resulted in markup overlap errors for arch_requalify commands. This was due to a misconception that YXML strings already containing correct position information (e.g. obtained via Parse.const) would be used directly by Proof_context.read_const/read_type_name. This is not the case. Instead, position information is adjusted for the content length, and since we add a prefix for L4V_ARCH, we got annotation that did not match the document text.
After hours of digging to uncover the above issue, we get this:
The resulting code is simpler; a large cautionary comment remains for future generations.