Skip to content

1964 allow importing cryptol submodules into saw #2562

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 21 commits into from
Sep 17, 2025
Merged

1964 allow importing cryptol submodules into saw #2562

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
d556a0f
comments, typos, wibbles.
mtullsen Sep 8, 2025
5d857a1
refactor: rename lookupCryptolModule to extractDefFromCryptolModule
mtullsen Sep 8, 2025
f265961
refactors: various
mtullsen Sep 8, 2025
19ae7cc
add tests for submodules in saw
mtullsen Sep 9, 2025
11e5aad
refactor: remove (always the same) argument from loadCryptolModule
mtullsen Sep 9, 2025
5aaff5d
refactor: belated.
mtullsen Sep 9, 2025
6f268a6
refactors: various & small; comments; white space
mtullsen Sep 9, 2025
5f8ae36
refactors: various & small
mtullsen Sep 9, 2025
667df2f
refactor: refactor loadCryptolModule and importModule to highlight co…
mtullsen Sep 9, 2025
a906b1d
Fix code to handle submodules in SAWScript imports.
mtullsen Sep 9, 2025
c923c71
improve submodule support for CLI `cryptol_load`
mtullsen Sep 9, 2025
03390ec
Bump deps/cryptol
mtullsen Sep 13, 2025
ab11d57
remove unrelated gitignores
mtullsen Sep 14, 2025
ae2127a
improve and add haddock and other comments and FIXMEs
mtullsen Sep 14, 2025
bb89ba9
refactor: change updateFFITypes (and calls to)
mtullsen Sep 14, 2025
e27537d
improve comments (per PR review requests)
mtullsen Sep 16, 2025
43adb99
add test that currently fails, document this.
mtullsen Sep 16, 2025
9effbfd
refactor: put initialization code in proximity; whitespace.
mtullsen Sep 16, 2025
2024835
Bump deps/cryptol
mtullsen Sep 16, 2025
3beefca
comment: fix to address proper Issue/PR.
mtullsen Sep 16, 2025
66025b0
Bump deps/cryptol
mtullsen Sep 16, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion crux-mir-comp/src/Mir/Cryptol.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -241,7 +241,7 @@ loadCryptolFunc col sig modulePath name = do
ce' <- liftIO $ SAW.importModule sc ce (Right modName) Nothing SAW.PublicAndPrivate Nothing
liftIO (writeIORef (mirCryEnv mirState) ce')
-- (m, _ce') <- liftIO $ SAW.loadCryptolModule sc ce (Text.unpack modulePath)
-- tt <- liftIO $ SAW.lookupCryptolModule m (Text.unpack name)
-- tt <- liftIO $ SAW.extractDefFromCryptolModule m (Text.unpack name)
tt <- liftIO $ SAW.parseTypedTerm sc ce' $
SAW.InputText name "<string>" 1 1

Expand Down
Loading
Loading