diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index da9944558c..9159120fd6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -315,7 +315,8 @@ jobs: cd saw-remote-api/python/ poetry update poetry install - poetry run mypy saw_client/ + poetry run mypy --install-types --non-interactive saw_client/ || true + poetry run mypy --install-types --non-interactive saw_client/ os: macos-12 - name: Check docs test: saw-remote-api/scripts/check_docs.sh @@ -337,7 +338,7 @@ jobs: - uses: actions/setup-python@v2 with: - python-version: '3.9' + python-version: '3.11' - uses: abatilo/actions-poetry@v2.0.0 with: diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index 73d58e3a7d..df6d0441ee 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -1050,6 +1050,9 @@ importExpr sc env expr = C.ELocated _ e -> importExpr sc env e + C.EPropGuards {} -> + error "Using contsraint guards is not yet supported by SAW." + where the :: Maybe a -> IO a the = maybe (panic "importExpr" ["internal type error"]) return @@ -1063,6 +1066,9 @@ importExpr sc env expr = importExpr' :: SharedContext -> Env -> C.Schema -> C.Expr -> IO Term importExpr' sc env schema expr = case expr of + C.EPropGuards {} -> + error "Using contsraint guards is not yet supported by SAW." + C.ETuple es -> do ty <- the (C.isMono schema) ts <- the (C.tIsTuple ty) @@ -1284,6 +1290,10 @@ importDeclGroup declOpts sc env (C.Recursive [decl]) = case C.dDefinition decl of C.DPrim -> panic "importDeclGroup" ["Primitive declarations cannot be recursive:", show (C.dName decl)] + + C.DForeign {} -> + error "`foreign` imports may not be used in SAW specifications" + C.DExpr expr -> do env1 <- bindName sc (C.dName decl) (C.dSignature decl) env t' <- importSchema sc env (C.dSignature decl) @@ -1329,6 +1339,8 @@ importDeclGroup declOpts sc env (C.Recursive decls) = let extractDeclExpr decl = case C.dDefinition decl of C.DExpr expr -> importExpr' sc env2 (C.dSignature decl) expr + C.DForeign {} -> + error "`foreign` imports may not be used in SAW specifications" C.DPrim -> panic "importDeclGroup" [ "Primitive declarations cannot be recursive:" @@ -1366,6 +1378,9 @@ importDeclGroup declOpts sc env (C.Recursive decls) = importDeclGroup declOpts sc env (C.NonRecursive decl) = case C.dDefinition decl of + C.DForeign {} -> + error "`foreign` imports may not be used in SAW specifications" + C.DPrim | TopLevelDeclGroup primOpts <- declOpts -> do rhs <- importPrimitive sc primOpts env (C.dName decl) (C.dSignature decl) @@ -1480,7 +1495,7 @@ tNoUser initialTy = case C.tNoUser initialTy of C.TNewtype nt _ -> C.TRec $ C.ntFields nt t -> t - + -- | Deconstruct a cryptol tuple type as a pair according to the -- saw-core tuple type encoding. @@ -1596,6 +1611,10 @@ importMatches sc env [C.Let decl] importMatches sc env (C.Let decl : matches) = case C.dDefinition decl of + + C.DForeign {} -> + error "`foreign` imports may not be used in SAW specifications" + C.DPrim -> do panic "importMatches" ["Primitive declarations not allowed in 'let':", show (C.dName decl)] C.DExpr expr -> do diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs index 74892c7895..7abfd4e72f 100644 --- a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs +++ b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs @@ -372,7 +372,7 @@ loadCryptolModule :: IO (CryptolModule, CryptolEnv) loadCryptolModule sc primOpts env path = do let modEnv = eModuleEnv env - (m, modEnv') <- liftModuleM modEnv (MB.loadModuleByPath path) + (m, modEnv') <- liftModuleM modEnv (snd <$> MB.loadModuleByPath True path) checkNotParameterized m let ifaceDecls = getAllIfaceDecls modEnv' @@ -439,7 +439,7 @@ importModule sc env src as vis imps = do (m, modEnv') <- liftModuleM modEnv $ case src of - Left path -> MB.loadModuleByPath path + Left path -> snd <$> MB.loadModuleByPath True path Right mn -> snd <$> MB.loadModuleFrom True (MM.FromModule mn) checkNotParameterized m diff --git a/deps/cryptol b/deps/cryptol index 09f03264f7..4b89554988 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit 09f03264f7d37610bb1b145bb53e044316ccb76d +Subproject commit 4b89554988e1f755b6d8f49e6be08027aadbaacf diff --git a/saw-remote-api/python/mypy.ini b/saw-remote-api/python/mypy.ini index 648cc9bebb..4a9b277295 100644 --- a/saw-remote-api/python/mypy.ini +++ b/saw-remote-api/python/mypy.ini @@ -1,6 +1,6 @@ [mypy] no_implicit_optional = True -python_version = 3.7 +python_version = 3.11 warn_return_any = True warn_unused_configs = True warn_unused_ignores = True diff --git a/saw-remote-api/python/poetry.lock b/saw-remote-api/python/poetry.lock index b166c85c8b..1e7dcc9a21 100644 --- a/saw-remote-api/python/poetry.lock +++ b/saw-remote-api/python/poetry.lock @@ -1,10 +1,10 @@ [[package]] name = "argo-client" -version = "0.0.10" +version = "0.0.11" description = "A JSON RPC client library." category = "main" optional = false -python-versions = ">=3.7.0,<4" +python-versions = ">=3.8.0,<4" [package.dependencies] requests = ">=2.26.0,<3.0.0" @@ -28,32 +28,34 @@ python-versions = ">=3.6" [[package]] name = "charset-normalizer" -version = "2.0.12" +version = "3.0.1" description = "The Real First Universal Charset Detector. Open, modern and actively maintained alternative to Chardet." category = "main" optional = false -python-versions = ">=3.5.0" - -[package.extras] -unicode-backport = ["unicodedata2"] +python-versions = "*" [[package]] name = "cryptol" -version = "2.12.4" -description = "Cryptol client for the Cryptol 2.12 RPC server" +version = "2.13.1" +description = "Cryptol client for the Cryptol 2.13 RPC server" category = "main" optional = false -python-versions = ">=3.7.0,<4" +python-versions = ">=3.8.0,<4" +develop = true [package.dependencies] -argo-client = "0.0.10" -BitVector = ">=3.4.9,<4.0.0" -requests = ">=2.25.1,<3.0.0" -typing-extensions = ">=4.1.1,<5.0.0" +argo-client = "0.0.11" +BitVector = "^3.4.9" +requests = "^2.25.1" +typing-extensions = "^4.1.1" + +[package.source] +type = "directory" +url = "../../deps/cryptol/cryptol-remote-api/python" [[package]] name = "idna" -version = "3.3" +version = "3.4" description = "Internationalized Domain Names in Applications (IDNA)" category = "main" optional = false @@ -61,19 +63,22 @@ python-versions = ">=3.5" [[package]] name = "mypy" -version = "0.812" +version = "0.991" description = "Optional static typing for Python" category = "dev" optional = false -python-versions = ">=3.5" +python-versions = ">=3.7" [package.dependencies] -mypy-extensions = ">=0.4.3,<0.5.0" -typed-ast = ">=1.4.0,<1.5.0" -typing-extensions = ">=3.7.4" +mypy-extensions = ">=0.4.3" +tomli = {version = ">=1.1.0", markers = "python_version < \"3.11\""} +typing-extensions = ">=3.10" [package.extras] dmypy = ["psutil (>=4.0)"] +install-types = ["pip"] +python2 = ["typed-ast (>=1.4.0,<2)"] +reports = ["lxml"] [[package]] name = "mypy-extensions" @@ -85,33 +90,33 @@ python-versions = "*" [[package]] name = "requests" -version = "2.27.1" +version = "2.28.2" description = "Python HTTP for Humans." category = "main" optional = false -python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*, !=3.5.*" +python-versions = ">=3.7, <4" [package.dependencies] certifi = ">=2017.4.17" -charset-normalizer = {version = ">=2.0.0,<2.1.0", markers = "python_version >= \"3\""} -idna = {version = ">=2.5,<4", markers = "python_version >= \"3\""} +charset-normalizer = ">=2,<4" +idna = ">=2.5,<4" urllib3 = ">=1.21.1,<1.27" [package.extras] -socks = ["PySocks (>=1.5.6,!=1.5.7)", "win-inet-pton"] -use-chardet-on-py3 = ["chardet (>=3.0.2,<5)"] +socks = ["PySocks (>=1.5.6,!=1.5.7)"] +use_chardet_on_py3 = ["chardet (>=3.0.2,<6)"] [[package]] -name = "typed-ast" -version = "1.4.3" -description = "a fork of Python 2 and 3 ast modules with type comment support" +name = "tomli" +version = "2.0.1" +description = "A lil' TOML parser" category = "dev" optional = false -python-versions = "*" +python-versions = ">=3.7" [[package]] name = "typing-extensions" -version = "4.2.0" +version = "4.4.0" description = "Backported and Experimental Type Hints for Python 3.7+" category = "main" optional = false @@ -119,115 +124,40 @@ python-versions = ">=3.7" [[package]] name = "urllib3" -version = "1.26.9" +version = "1.26.14" description = "HTTP library with thread-safe connection pooling, file post, and more." category = "main" optional = false -python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*, <4" +python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*, !=3.5.*" [package.extras] -brotli = ["brotli (>=1.0.9)", "brotlicffi (>=0.8.0)", "brotlipy (>=0.6.0)"] -secure = ["certifi", "cryptography (>=1.3.4)", "idna (>=2.0.0)", "ipaddress", "pyOpenSSL (>=0.14)"] +brotli = ["brotlicffi (>=0.8.0)", "brotli (>=1.0.9)", "brotlipy (>=0.6.0)"] +secure = ["pyOpenSSL (>=0.14)", "cryptography (>=1.3.4)", "idna (>=2.0.0)", "certifi", "urllib3-secure-extra", "ipaddress"] socks = ["PySocks (>=1.5.6,!=1.5.7,<2.0)"] [metadata] lock-version = "1.1" python-versions = "^3.8" -content-hash = "49c7188786f994fbfb2eb67d447ba052aee0e090da5952eda39db840283e7e15" +content-hash = "3f94851a80911a65be8e6c8f325e221b391734f25f4fdbd556c082deb49d44f0" [metadata.files] -argo-client = [ - {file = "argo-client-0.0.10.tar.gz", hash = "sha256:a95e07201a5e23758e7bc6b2e1d594c61a71df02ff534ad7a8db32fdb991ed0b"}, - {file = "argo_client-0.0.10-py3-none-any.whl", hash = "sha256:d86e07bfc421faf9f25be6af2d4a0c7fd2ddef7a759488f6c05baa2ff2c1e390"}, -] +argo-client = [] bitvector = [ {file = "BitVector-3.5.0.tar.gz", hash = "sha256:cac2fbccf11e325115827ed7be03e5fd62615227b0bbf3fa5a18a842a221839c"}, ] -certifi = [ - {file = "certifi-2022.12.7-py3-none-any.whl", hash = "sha256:4ad3232f5e926d6718ec31cfc1fcadfde020920e278684144551c91769c7bc18"}, - {file = "certifi-2022.12.7.tar.gz", hash = "sha256:35824b4c3a97115964b408844d64aa14db1cc518f6562e8d7261699d1350a9e3"}, -] -charset-normalizer = [ - {file = "charset-normalizer-2.0.12.tar.gz", hash = "sha256:2857e29ff0d34db842cd7ca3230549d1a697f96ee6d3fb071cfa6c7393832597"}, - {file = "charset_normalizer-2.0.12-py3-none-any.whl", hash = "sha256:6881edbebdb17b39b4eaaa821b438bf6eddffb4468cf344f09f89def34a8b1df"}, -] -cryptol = [ - {file = "cryptol-2.12.4-py3-none-any.whl", hash = "sha256:7b87d3128c683f234618509600a0fc4c0fd2899a493cdd0ca389198128e785a7"}, - {file = "cryptol-2.12.4.tar.gz", hash = "sha256:588ada535994b52ac4b237edc230c7bb05822f6a0544f1dcf5aff60c800ebf1b"}, -] -idna = [ - {file = "idna-3.3-py3-none-any.whl", hash = "sha256:84d9dd047ffa80596e0f246e2eab0b391788b0503584e8945f2368256d2735ff"}, - {file = "idna-3.3.tar.gz", hash = "sha256:9d643ff0a55b762d5cdb124b8eaa99c66322e2157b69160bc32796e824360e6d"}, -] -mypy = [ - {file = "mypy-0.812-cp35-cp35m-macosx_10_9_x86_64.whl", hash = "sha256:a26f8ec704e5a7423c8824d425086705e381b4f1dfdef6e3a1edab7ba174ec49"}, - {file = "mypy-0.812-cp35-cp35m-manylinux1_x86_64.whl", hash = "sha256:28fb5479c494b1bab244620685e2eb3c3f988d71fd5d64cc753195e8ed53df7c"}, - {file = "mypy-0.812-cp35-cp35m-manylinux2010_x86_64.whl", hash = "sha256:9743c91088d396c1a5a3c9978354b61b0382b4e3c440ce83cf77994a43e8c521"}, - {file = "mypy-0.812-cp35-cp35m-win_amd64.whl", hash = "sha256:d7da2e1d5f558c37d6e8c1246f1aec1e7349e4913d8fb3cb289a35de573fe2eb"}, - {file = "mypy-0.812-cp36-cp36m-macosx_10_9_x86_64.whl", hash = "sha256:4eec37370483331d13514c3f55f446fc5248d6373e7029a29ecb7b7494851e7a"}, - {file = "mypy-0.812-cp36-cp36m-manylinux1_x86_64.whl", hash = "sha256:d65cc1df038ef55a99e617431f0553cd77763869eebdf9042403e16089fe746c"}, - {file = "mypy-0.812-cp36-cp36m-manylinux2010_x86_64.whl", hash = "sha256:61a3d5b97955422964be6b3baf05ff2ce7f26f52c85dd88db11d5e03e146a3a6"}, - {file = "mypy-0.812-cp36-cp36m-win_amd64.whl", hash = "sha256:25adde9b862f8f9aac9d2d11971f226bd4c8fbaa89fb76bdadb267ef22d10064"}, - {file = "mypy-0.812-cp37-cp37m-macosx_10_9_x86_64.whl", hash = "sha256:552a815579aa1e995f39fd05dde6cd378e191b063f031f2acfe73ce9fb7f9e56"}, - {file = "mypy-0.812-cp37-cp37m-manylinux1_x86_64.whl", hash = "sha256:499c798053cdebcaa916eef8cd733e5584b5909f789de856b482cd7d069bdad8"}, - {file = "mypy-0.812-cp37-cp37m-manylinux2010_x86_64.whl", hash = "sha256:5873888fff1c7cf5b71efbe80e0e73153fe9212fafdf8e44adfe4c20ec9f82d7"}, - {file = "mypy-0.812-cp37-cp37m-win_amd64.whl", hash = "sha256:9f94aac67a2045ec719ffe6111df543bac7874cee01f41928f6969756e030564"}, - {file = "mypy-0.812-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:d23e0ea196702d918b60c8288561e722bf437d82cb7ef2edcd98cfa38905d506"}, - {file = "mypy-0.812-cp38-cp38-manylinux1_x86_64.whl", hash = "sha256:674e822aa665b9fd75130c6c5f5ed9564a38c6cea6a6432ce47eafb68ee578c5"}, - {file = "mypy-0.812-cp38-cp38-manylinux2010_x86_64.whl", hash = "sha256:abf7e0c3cf117c44d9285cc6128856106183938c68fd4944763003decdcfeb66"}, - {file = "mypy-0.812-cp38-cp38-win_amd64.whl", hash = "sha256:0d0a87c0e7e3a9becdfbe936c981d32e5ee0ccda3e0f07e1ef2c3d1a817cf73e"}, - {file = "mypy-0.812-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:7ce3175801d0ae5fdfa79b4f0cfed08807af4d075b402b7e294e6aa72af9aa2a"}, - {file = "mypy-0.812-cp39-cp39-manylinux1_x86_64.whl", hash = "sha256:b09669bcda124e83708f34a94606e01b614fa71931d356c1f1a5297ba11f110a"}, - {file = "mypy-0.812-cp39-cp39-manylinux2010_x86_64.whl", hash = "sha256:33f159443db0829d16f0a8d83d94df3109bb6dd801975fe86bacb9bf71628e97"}, - {file = "mypy-0.812-cp39-cp39-win_amd64.whl", hash = "sha256:3f2aca7f68580dc2508289c729bd49ee929a436208d2b2b6aab15745a70a57df"}, - {file = "mypy-0.812-py3-none-any.whl", hash = "sha256:2f9b3407c58347a452fc0736861593e105139b905cca7d097e413453a1d650b4"}, - {file = "mypy-0.812.tar.gz", hash = "sha256:cd07039aa5df222037005b08fbbfd69b3ab0b0bd7a07d7906de75ae52c4e3119"}, -] +certifi = [] +charset-normalizer = [] +cryptol = [] +idna = [] +mypy = [] mypy-extensions = [ {file = "mypy_extensions-0.4.3-py2.py3-none-any.whl", hash = "sha256:090fedd75945a69ae91ce1303b5824f428daf5a028d2f6ab8a299250a846f15d"}, {file = "mypy_extensions-0.4.3.tar.gz", hash = "sha256:2d82818f5bb3e369420cb3c4060a7970edba416647068eb4c5343488a6c604a8"}, ] -requests = [ - {file = "requests-2.27.1-py2.py3-none-any.whl", hash = "sha256:f22fa1e554c9ddfd16e6e41ac79759e17be9e492b3587efa038054674760e72d"}, - {file = "requests-2.27.1.tar.gz", hash = "sha256:68d7c56fd5a8999887728ef304a6d12edc7be74f1cfa47714fc8b414525c9a61"}, -] -typed-ast = [ - {file = "typed_ast-1.4.3-cp35-cp35m-manylinux1_i686.whl", hash = "sha256:2068531575a125b87a41802130fa7e29f26c09a2833fea68d9a40cf33902eba6"}, - {file = "typed_ast-1.4.3-cp35-cp35m-manylinux1_x86_64.whl", hash = "sha256:c907f561b1e83e93fad565bac5ba9c22d96a54e7ea0267c708bffe863cbe4075"}, - {file = "typed_ast-1.4.3-cp35-cp35m-manylinux2014_aarch64.whl", hash = "sha256:1b3ead4a96c9101bef08f9f7d1217c096f31667617b58de957f690c92378b528"}, - {file = "typed_ast-1.4.3-cp35-cp35m-win32.whl", hash = "sha256:dde816ca9dac1d9c01dd504ea5967821606f02e510438120091b84e852367428"}, - {file = "typed_ast-1.4.3-cp35-cp35m-win_amd64.whl", hash = "sha256:777a26c84bea6cd934422ac2e3b78863a37017618b6e5c08f92ef69853e765d3"}, - {file = "typed_ast-1.4.3-cp36-cp36m-macosx_10_9_x86_64.whl", hash = "sha256:f8afcf15cc511ada719a88e013cec87c11aff7b91f019295eb4530f96fe5ef2f"}, - {file = "typed_ast-1.4.3-cp36-cp36m-manylinux1_i686.whl", hash = "sha256:52b1eb8c83f178ab787f3a4283f68258525f8d70f778a2f6dd54d3b5e5fb4341"}, - {file = "typed_ast-1.4.3-cp36-cp36m-manylinux1_x86_64.whl", hash = "sha256:01ae5f73431d21eead5015997ab41afa53aa1fbe252f9da060be5dad2c730ace"}, - {file = "typed_ast-1.4.3-cp36-cp36m-manylinux2014_aarch64.whl", hash = "sha256:c190f0899e9f9f8b6b7863debfb739abcb21a5c054f911ca3596d12b8a4c4c7f"}, - {file = "typed_ast-1.4.3-cp36-cp36m-win32.whl", hash = "sha256:398e44cd480f4d2b7ee8d98385ca104e35c81525dd98c519acff1b79bdaac363"}, - {file = "typed_ast-1.4.3-cp36-cp36m-win_amd64.whl", hash = "sha256:bff6ad71c81b3bba8fa35f0f1921fb24ff4476235a6e94a26ada2e54370e6da7"}, - {file = "typed_ast-1.4.3-cp37-cp37m-macosx_10_9_x86_64.whl", hash = "sha256:0fb71b8c643187d7492c1f8352f2c15b4c4af3f6338f21681d3681b3dc31a266"}, - {file = "typed_ast-1.4.3-cp37-cp37m-manylinux1_i686.whl", hash = "sha256:760ad187b1041a154f0e4d0f6aae3e40fdb51d6de16e5c99aedadd9246450e9e"}, - {file = "typed_ast-1.4.3-cp37-cp37m-manylinux1_x86_64.whl", hash = "sha256:5feca99c17af94057417d744607b82dd0a664fd5e4ca98061480fd8b14b18d04"}, - {file = "typed_ast-1.4.3-cp37-cp37m-manylinux2014_aarch64.whl", hash = "sha256:95431a26309a21874005845c21118c83991c63ea800dd44843e42a916aec5899"}, - {file = "typed_ast-1.4.3-cp37-cp37m-win32.whl", hash = "sha256:aee0c1256be6c07bd3e1263ff920c325b59849dc95392a05f258bb9b259cf39c"}, - {file = "typed_ast-1.4.3-cp37-cp37m-win_amd64.whl", hash = "sha256:9ad2c92ec681e02baf81fdfa056fe0d818645efa9af1f1cd5fd6f1bd2bdfd805"}, - {file = "typed_ast-1.4.3-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:b36b4f3920103a25e1d5d024d155c504080959582b928e91cb608a65c3a49e1a"}, - {file = "typed_ast-1.4.3-cp38-cp38-manylinux1_i686.whl", hash = "sha256:067a74454df670dcaa4e59349a2e5c81e567d8d65458d480a5b3dfecec08c5ff"}, - {file = "typed_ast-1.4.3-cp38-cp38-manylinux1_x86_64.whl", hash = "sha256:7538e495704e2ccda9b234b82423a4038f324f3a10c43bc088a1636180f11a41"}, - {file = "typed_ast-1.4.3-cp38-cp38-manylinux2014_aarch64.whl", hash = "sha256:af3d4a73793725138d6b334d9d247ce7e5f084d96284ed23f22ee626a7b88e39"}, - {file = "typed_ast-1.4.3-cp38-cp38-win32.whl", hash = "sha256:f2362f3cb0f3172c42938946dbc5b7843c2a28aec307c49100c8b38764eb6927"}, - {file = "typed_ast-1.4.3-cp38-cp38-win_amd64.whl", hash = "sha256:dd4a21253f42b8d2b48410cb31fe501d32f8b9fbeb1f55063ad102fe9c425e40"}, - {file = "typed_ast-1.4.3-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:f328adcfebed9f11301eaedfa48e15bdece9b519fb27e6a8c01aa52a17ec31b3"}, - {file = "typed_ast-1.4.3-cp39-cp39-manylinux1_i686.whl", hash = "sha256:2c726c276d09fc5c414693a2de063f521052d9ea7c240ce553316f70656c84d4"}, - {file = "typed_ast-1.4.3-cp39-cp39-manylinux1_x86_64.whl", hash = "sha256:cae53c389825d3b46fb37538441f75d6aecc4174f615d048321b716df2757fb0"}, - {file = "typed_ast-1.4.3-cp39-cp39-manylinux2014_aarch64.whl", hash = "sha256:b9574c6f03f685070d859e75c7f9eeca02d6933273b5e69572e5ff9d5e3931c3"}, - {file = "typed_ast-1.4.3-cp39-cp39-win32.whl", hash = "sha256:209596a4ec71d990d71d5e0d312ac935d86930e6eecff6ccc7007fe54d703808"}, - {file = "typed_ast-1.4.3-cp39-cp39-win_amd64.whl", hash = "sha256:9c6d1a54552b5330bc657b7ef0eae25d00ba7ffe85d9ea8ae6540d2197a3788c"}, - {file = "typed_ast-1.4.3.tar.gz", hash = "sha256:fb1bbeac803adea29cedd70781399c99138358c26d05fcbd23c13016b7f5ec65"}, -] -typing-extensions = [ - {file = "typing_extensions-4.2.0-py3-none-any.whl", hash = "sha256:6657594ee297170d19f67d55c05852a874e7eb634f4f753dbd667855e07c1708"}, - {file = "typing_extensions-4.2.0.tar.gz", hash = "sha256:f1c24655a0da0d1b67f07e17a5e6b2a105894e6824b92096378bb3668ef02376"}, -] -urllib3 = [ - {file = "urllib3-1.26.9-py2.py3-none-any.whl", hash = "sha256:44ece4d53fb1706f667c9bd1c648f5469a2ec925fcf3a776667042d645472c14"}, - {file = "urllib3-1.26.9.tar.gz", hash = "sha256:aabaf16477806a5e1dd19aa41f8c2b7950dd3c746362d7e3223dbe6de6ac448e"}, +requests = [] +tomli = [ + {file = "tomli-2.0.1-py3-none-any.whl", hash = "sha256:939de3e7a6161af0c887ef91b7d41a53e7c5a1ca976325f429cb46ea9bc30ecc"}, + {file = "tomli-2.0.1.tar.gz", hash = "sha256:de526c12914f0c550d15924c62d72abc48d6fe7364aa87328337a31007fe8a4f"}, ] +typing-extensions = [] +urllib3 = [] diff --git a/saw-remote-api/python/pyproject.toml b/saw-remote-api/python/pyproject.toml index c7f25d3fd6..2228786319 100644 --- a/saw-remote-api/python/pyproject.toml +++ b/saw-remote-api/python/pyproject.toml @@ -14,11 +14,11 @@ include = [ python = "^3.8" requests = "^2.25.1" BitVector = "^3.4.9" -cryptol = "2.12.4" # { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true } -argo-client = "0.0.10" +cryptol = { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true } +argo-client = "0.0.11" [tool.poetry.dev-dependencies] -mypy = "^0.812" +mypy = "^0.991" [build-system] requires = ["poetry>=1.1.4", "setuptools>=40.8.0"] diff --git a/saw-remote-api/scripts/run_rpc_tests.sh b/saw-remote-api/scripts/run_rpc_tests.sh index edcc35ed49..7810c71788 100755 --- a/saw-remote-api/scripts/run_rpc_tests.sh +++ b/saw-remote-api/scripts/run_rpc_tests.sh @@ -18,7 +18,8 @@ poetry install echo "Typechecking code with mypy..." # Don't run mypy on tests/ yet, as it doesn't play well with mypy. See #1125. -run_test poetry run mypy saw_client/ +run_test poetry run mypy --install-types --non-interactive saw_client/ || true +run_test poetry run mypy --install-types --non-interactive saw_client/ export SAW_SERVER=$(which saw-remote-api) if [[ ! -x "$SAW_SERVER" ]]; then diff --git a/src/SAWScript/AutoMatch/Cryptol.hs b/src/SAWScript/AutoMatch/Cryptol.hs index 56d26505d1..0720badb14 100644 --- a/src/SAWScript/AutoMatch/Cryptol.hs +++ b/src/SAWScript/AutoMatch/Cryptol.hs @@ -78,6 +78,7 @@ whereBindings _ = Nothing declDefExpr :: AST.DeclDef -> Maybe AST.Expr declDefExpr = \case AST.DPrim -> Nothing + AST.DForeign {} -> Nothing AST.DExpr expr -> Just expr -- | If a lambda is of the form @\(a,b,...,z) -> ...)@ then give the list of names bound in the tuple