support submodules in cryptol_load #2593
Draft
Conversation
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
Contributor
mtullsen
commented
Sep 10, 2025
mtullsen
commented
- Part of implementing Allow importing Cryptol submodules into SAW #1964.
- Refer also to Cleanup and Consolidate SAWScript import and load_cryptol (UI and implementation) #2569
- The goal is to do this in terms of the currently working import implementation.
- Builds on 1964 allow importing cryptol submodules into saw #2562
This was referenced Sep 9, 2025
mtullsen
force-pushed
the
tullsen/support-submodules-in-cryptol_load
branch
4 times, most recently
from
52b831f to
729af4c
Compare
mtullsen
force-pushed
the
tullsen/support-submodules-in-cryptol_load
branch
from
40352f9 to
d80957b
Compare
- See comments in mkCryptolModule that justify the refactor (i.e., that modEnv' == modEnv'')
- s/importModule/importCryptolModule/g;
… and updating code to reflect this
- CryptolModule (as known at the command line) is generalized to ExtCryptolModule,
- this allows for a module to be represented as EITHER
- CryptolModule (2 namespaces), or
- the name of a loaded module
- This allows for simpler and newly shared code
- This now should support submodules when we `cryptol_load`.
revert c923c71... improve submodule support for CLI `cryptol_load`
…actDefFromExtCryptolModule
mtullsen
force-pushed
the
tullsen/support-submodules-in-cryptol_load
branch
from
d80957b to
93fd2d8
Compare
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.