From 1f2715a5838f0b56b35983d48e12847b945f5d4e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Fri, 31 Jan 2025 17:02:35 +0100 Subject: [PATCH] Generate `lake` project (#4748) * Make `cookiecutter` a runtime dependency * Add logic for project generation * Add integration test for project generatiion --- .github/actions/with-k-docker/Dockerfile | 7 +- flake.nix | 2 +- nix/pyk-overlay.nix | 4 +- pyk/poetry.lock | 446 +++++++++++++++++- pyk/pyproject.toml | 5 + pyk/src/pyk/k2lean4/__init__.py | 1 - pyk/src/pyk/klean/__init__.py | 1 + pyk/src/pyk/klean/generate.py | 87 ++++ pyk/src/pyk/{k2lean4 => klean}/k2lean4.py | 26 +- pyk/src/pyk/{k2lean4 => klean}/model.py | 13 +- pyk/src/pyk/klean/template/cookiecutter.json | 4 + .../.gitignore | 1 + .../lakefile.toml | 9 + .../lean-toolchain | 1 + .../{{ cookiecutter.library_name }}.lean | 1 + .../Prelude.lean | 189 ++++---- pyk/src/pyk/kore/internal.py | 8 +- pyk/src/tests/integration/klean/__init__.py | 0 .../tests/integration/klean/test_generate.py | 48 ++ 19 files changed, 737 insertions(+), 116 deletions(-) delete mode 100644 pyk/src/pyk/k2lean4/__init__.py create mode 100644 pyk/src/pyk/klean/__init__.py create mode 100644 pyk/src/pyk/klean/generate.py rename pyk/src/pyk/{k2lean4 => klean}/k2lean4.py (97%) rename pyk/src/pyk/{k2lean4 => klean}/model.py (96%) create mode 100644 pyk/src/pyk/klean/template/cookiecutter.json create mode 100644 pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/.gitignore create mode 100644 pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/lakefile.toml create mode 100644 pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/lean-toolchain create mode 100644 pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/{{ cookiecutter.library_name }}.lean rename pyk/src/pyk/{k2lean4 => klean/template/{{ cookiecutter.package_name }}/{{ cookiecutter.library_name }}}/Prelude.lean (56%) create mode 100644 pyk/src/tests/integration/klean/__init__.py create mode 100644 pyk/src/tests/integration/klean/test_generate.py diff --git a/.github/actions/with-k-docker/Dockerfile b/.github/actions/with-k-docker/Dockerfile index 853c1a1cefa..a2febf5ebda 100644 --- a/.github/actions/with-k-docker/Dockerfile +++ b/.github/actions/with-k-docker/Dockerfile @@ -31,7 +31,7 @@ RUN rm /kframework.deb ARG USER_ID=9876 ARG GROUP_ID=9876 -RUN groupadd -g ${GROUP_ID} user \ +RUN groupadd -g ${GROUP_ID} user \ && useradd -m -u ${USER_ID} -s /bin/sh -g user user USER user @@ -40,3 +40,8 @@ WORKDIR /home/user ENV PATH=/home/user/.local/bin:${PATH} RUN curl -sSL https://install.python-poetry.org | python3 - --version 1.8.5 \ && poetry --version + +ENV PATH=/home/user/.elan/bin:${PATH} +RUN curl -O https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \ + && sh elan-init.sh -y \ + && rm elan-init.sh diff --git a/flake.nix b/flake.nix index 6e1521f5dad..4813da73ecf 100644 --- a/flake.nix +++ b/flake.nix @@ -84,7 +84,7 @@ mk-k-framework = { haskell-backend-bins, llvm-kompile-libs }: prev.callPackage ./nix/k.nix { - mvnHash = "sha256-HkAwMZq2vvrnEgT1Ksoxb5YnQ8+CMQdB2Sd/nR0OttU="; + mvnHash = "sha256-DVuyqwG11OY4uaaGwXTZOtyWefGye8l3yMSp3Cc7SeI="; manualMvnArtifacts = [ "org.scala-lang:scala-compiler:2.13.13" "ant-contrib:ant-contrib:1.0b3" diff --git a/nix/pyk-overlay.nix b/nix/pyk-overlay.nix index 70455675a5c..0bb5a8d99df 100644 --- a/nix/pyk-overlay.nix +++ b/nix/pyk-overlay.nix @@ -12,10 +12,10 @@ checkGroups = [ ]; overrides = p2n.defaultPoetryOverrides.extend (self: super: { - pygments = super.pygments.overridePythonAttrs + urllib3 = super.urllib3.overridePythonAttrs ( old: { - buildInputs = (old.buildInputs or [ ]) ++ [ super.hatchling ]; + buildInputs = (old.buildInputs or [ ]) ++ [ super.hatch-vcs ]; } ); }); diff --git a/pyk/poetry.lock b/pyk/poetry.lock index 81d40e2ee1b..873290b972e 100644 --- a/pyk/poetry.lock +++ b/pyk/poetry.lock @@ -1,4 +1,23 @@ -# This file is automatically @generated by Poetry 1.8.3 and should not be changed by hand. +# This file is automatically @generated by Poetry 1.8.5 and should not be changed by hand. + +[[package]] +name = "arrow" +version = "1.3.0" +description = "Better dates & times for Python" +optional = false +python-versions = ">=3.8" +files = [ + {file = "arrow-1.3.0-py3-none-any.whl", hash = "sha256:c728b120ebc00eb84e01882a6f5e7927a53960aa990ce7dd2b10f39005a67f80"}, + {file = "arrow-1.3.0.tar.gz", hash = "sha256:d4540617648cb5f895730f1ad8c82a65f2dad0166f57b75f3ca54759c4d67a85"}, +] + +[package.dependencies] +python-dateutil = ">=2.7.0" +types-python-dateutil = ">=2.8.10" + +[package.extras] +doc = ["doc8", "sphinx (>=7.0.0)", "sphinx-autobuild", "sphinx-autodoc-typehints", "sphinx_rtd_theme (>=1.3.0)"] +test = ["dateparser (==1.*)", "pre-commit", "pytest", "pytest-cov", "pytest-mock", "pytz (==2021.1)", "simplejson (==3.*)"] [[package]] name = "attrs" @@ -34,6 +53,20 @@ files = [ pyflakes = ">=3.0.0" tomli = {version = ">=2.0.1", markers = "python_version < \"3.11\""} +[[package]] +name = "binaryornot" +version = "0.4.4" +description = "Ultra-lightweight pure Python package to check if a file is binary or text." +optional = false +python-versions = "*" +files = [ + {file = "binaryornot-0.4.4-py2.py3-none-any.whl", hash = "sha256:b8b71173c917bddcd2c16070412e369c3ed7f0528926f70cac18a6c97fd563e4"}, + {file = "binaryornot-0.4.4.tar.gz", hash = "sha256:359501dfc9d40632edc9fac890e19542db1a287bbcfa58175b66658392018061"}, +] + +[package.dependencies] +chardet = ">=3.0.2" + [[package]] name = "black" version = "24.4.2" @@ -80,6 +113,129 @@ d = ["aiohttp (>=3.7.4)", "aiohttp (>=3.7.4,!=3.9.0)"] jupyter = ["ipython (>=7.8.0)", "tokenize-rt (>=3.2.0)"] uvloop = ["uvloop (>=0.15.2)"] +[[package]] +name = "certifi" +version = "2024.12.14" +description = "Python package for providing Mozilla's CA Bundle." +optional = false +python-versions = ">=3.6" +files = [ + {file = "certifi-2024.12.14-py3-none-any.whl", hash = "sha256:1275f7a45be9464efc1173084eaa30f866fe2e47d389406136d332ed4967ec56"}, + {file = "certifi-2024.12.14.tar.gz", hash = "sha256:b650d30f370c2b724812bee08008be0c4163b163ddaec3f2546c1caf65f191db"}, +] + +[[package]] +name = "chardet" +version = "5.2.0" +description = "Universal encoding detector for Python 3" +optional = false +python-versions = ">=3.7" +files = [ + {file = "chardet-5.2.0-py3-none-any.whl", hash = "sha256:e1cf59446890a00105fe7b7912492ea04b6e6f06d4b742b2c788469e34c82970"}, + {file = "chardet-5.2.0.tar.gz", hash = "sha256:1b3b6ff479a8c414bc3fa2c0852995695c4a026dcd6d0633b2dd092ca39c1cf7"}, +] + +[[package]] +name = "charset-normalizer" +version = "3.4.1" +description = "The Real First Universal Charset Detector. Open, modern and actively maintained alternative to Chardet." +optional = false +python-versions = ">=3.7" +files = [ + {file = "charset_normalizer-3.4.1-cp310-cp310-macosx_10_9_universal2.whl", hash = "sha256:91b36a978b5ae0ee86c394f5a54d6ef44db1de0815eb43de826d41d21e4af3de"}, + {file = "charset_normalizer-3.4.1-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:7461baadb4dc00fd9e0acbe254e3d7d2112e7f92ced2adc96e54ef6501c5f176"}, + {file = "charset_normalizer-3.4.1-cp310-cp310-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:e218488cd232553829be0664c2292d3af2eeeb94b32bea483cf79ac6a694e037"}, + {file = "charset_normalizer-3.4.1-cp310-cp310-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:80ed5e856eb7f30115aaf94e4a08114ccc8813e6ed1b5efa74f9f82e8509858f"}, + {file = "charset_normalizer-3.4.1-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:b010a7a4fd316c3c484d482922d13044979e78d1861f0e0650423144c616a46a"}, + {file = "charset_normalizer-3.4.1-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:4532bff1b8421fd0a320463030c7520f56a79c9024a4e88f01c537316019005a"}, + {file = "charset_normalizer-3.4.1-cp310-cp310-musllinux_1_2_aarch64.whl", hash = "sha256:d973f03c0cb71c5ed99037b870f2be986c3c05e63622c017ea9816881d2dd247"}, + {file = "charset_normalizer-3.4.1-cp310-cp310-musllinux_1_2_i686.whl", hash = "sha256:3a3bd0dcd373514dcec91c411ddb9632c0d7d92aed7093b8c3bbb6d69ca74408"}, + {file = "charset_normalizer-3.4.1-cp310-cp310-musllinux_1_2_ppc64le.whl", hash = "sha256:d9c3cdf5390dcd29aa8056d13e8e99526cda0305acc038b96b30352aff5ff2bb"}, + {file = "charset_normalizer-3.4.1-cp310-cp310-musllinux_1_2_s390x.whl", hash = "sha256:2bdfe3ac2e1bbe5b59a1a63721eb3b95fc9b6817ae4a46debbb4e11f6232428d"}, + {file = "charset_normalizer-3.4.1-cp310-cp310-musllinux_1_2_x86_64.whl", hash = "sha256:eab677309cdb30d047996b36d34caeda1dc91149e4fdca0b1a039b3f79d9a807"}, + {file = "charset_normalizer-3.4.1-cp310-cp310-win32.whl", hash = "sha256:c0429126cf75e16c4f0ad00ee0eae4242dc652290f940152ca8c75c3a4b6ee8f"}, + {file = "charset_normalizer-3.4.1-cp310-cp310-win_amd64.whl", hash = "sha256:9f0b8b1c6d84c8034a44893aba5e767bf9c7a211e313a9605d9c617d7083829f"}, + {file = "charset_normalizer-3.4.1-cp311-cp311-macosx_10_9_universal2.whl", hash = "sha256:8bfa33f4f2672964266e940dd22a195989ba31669bd84629f05fab3ef4e2d125"}, + {file = "charset_normalizer-3.4.1-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:28bf57629c75e810b6ae989f03c0828d64d6b26a5e205535585f96093e405ed1"}, + {file = "charset_normalizer-3.4.1-cp311-cp311-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:f08ff5e948271dc7e18a35641d2f11a4cd8dfd5634f55228b691e62b37125eb3"}, + {file = "charset_normalizer-3.4.1-cp311-cp311-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:234ac59ea147c59ee4da87a0c0f098e9c8d169f4dc2a159ef720f1a61bbe27cd"}, + {file = "charset_normalizer-3.4.1-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:fd4ec41f914fa74ad1b8304bbc634b3de73d2a0889bd32076342a573e0779e00"}, + {file = "charset_normalizer-3.4.1-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:eea6ee1db730b3483adf394ea72f808b6e18cf3cb6454b4d86e04fa8c4327a12"}, + {file = "charset_normalizer-3.4.1-cp311-cp311-musllinux_1_2_aarch64.whl", hash = "sha256:c96836c97b1238e9c9e3fe90844c947d5afbf4f4c92762679acfe19927d81d77"}, + {file = "charset_normalizer-3.4.1-cp311-cp311-musllinux_1_2_i686.whl", hash = "sha256:4d86f7aff21ee58f26dcf5ae81a9addbd914115cdebcbb2217e4f0ed8982e146"}, + {file = "charset_normalizer-3.4.1-cp311-cp311-musllinux_1_2_ppc64le.whl", hash = "sha256:09b5e6733cbd160dcc09589227187e242a30a49ca5cefa5a7edd3f9d19ed53fd"}, + {file = "charset_normalizer-3.4.1-cp311-cp311-musllinux_1_2_s390x.whl", hash = "sha256:5777ee0881f9499ed0f71cc82cf873d9a0ca8af166dfa0af8ec4e675b7df48e6"}, + {file = "charset_normalizer-3.4.1-cp311-cp311-musllinux_1_2_x86_64.whl", hash = "sha256:237bdbe6159cff53b4f24f397d43c6336c6b0b42affbe857970cefbb620911c8"}, + {file = "charset_normalizer-3.4.1-cp311-cp311-win32.whl", hash = "sha256:8417cb1f36cc0bc7eaba8ccb0e04d55f0ee52df06df3ad55259b9a323555fc8b"}, + {file = "charset_normalizer-3.4.1-cp311-cp311-win_amd64.whl", hash = "sha256:d7f50a1f8c450f3925cb367d011448c39239bb3eb4117c36a6d354794de4ce76"}, + {file = "charset_normalizer-3.4.1-cp312-cp312-macosx_10_13_universal2.whl", hash = "sha256:73d94b58ec7fecbc7366247d3b0b10a21681004153238750bb67bd9012414545"}, + {file = "charset_normalizer-3.4.1-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:dad3e487649f498dd991eeb901125411559b22e8d7ab25d3aeb1af367df5efd7"}, + {file = "charset_normalizer-3.4.1-cp312-cp312-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:c30197aa96e8eed02200a83fba2657b4c3acd0f0aa4bdc9f6c1af8e8962e0757"}, + {file = "charset_normalizer-3.4.1-cp312-cp312-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:2369eea1ee4a7610a860d88f268eb39b95cb588acd7235e02fd5a5601773d4fa"}, + {file = "charset_normalizer-3.4.1-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:bc2722592d8998c870fa4e290c2eec2c1569b87fe58618e67d38b4665dfa680d"}, + {file = "charset_normalizer-3.4.1-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:ffc9202a29ab3920fa812879e95a9e78b2465fd10be7fcbd042899695d75e616"}, + {file = "charset_normalizer-3.4.1-cp312-cp312-musllinux_1_2_aarch64.whl", hash = "sha256:804a4d582ba6e5b747c625bf1255e6b1507465494a40a2130978bda7b932c90b"}, + {file = "charset_normalizer-3.4.1-cp312-cp312-musllinux_1_2_i686.whl", hash = "sha256:0f55e69f030f7163dffe9fd0752b32f070566451afe180f99dbeeb81f511ad8d"}, + {file = "charset_normalizer-3.4.1-cp312-cp312-musllinux_1_2_ppc64le.whl", hash = "sha256:c4c3e6da02df6fa1410a7680bd3f63d4f710232d3139089536310d027950696a"}, + {file = "charset_normalizer-3.4.1-cp312-cp312-musllinux_1_2_s390x.whl", hash = "sha256:5df196eb874dae23dcfb968c83d4f8fdccb333330fe1fc278ac5ceeb101003a9"}, + {file = "charset_normalizer-3.4.1-cp312-cp312-musllinux_1_2_x86_64.whl", hash = "sha256:e358e64305fe12299a08e08978f51fc21fac060dcfcddd95453eabe5b93ed0e1"}, + {file = "charset_normalizer-3.4.1-cp312-cp312-win32.whl", hash = "sha256:9b23ca7ef998bc739bf6ffc077c2116917eabcc901f88da1b9856b210ef63f35"}, + {file = "charset_normalizer-3.4.1-cp312-cp312-win_amd64.whl", hash = "sha256:6ff8a4a60c227ad87030d76e99cd1698345d4491638dfa6673027c48b3cd395f"}, + {file = "charset_normalizer-3.4.1-cp313-cp313-macosx_10_13_universal2.whl", hash = "sha256:aabfa34badd18f1da5ec1bc2715cadc8dca465868a4e73a0173466b688f29dda"}, + {file = "charset_normalizer-3.4.1-cp313-cp313-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:22e14b5d70560b8dd51ec22863f370d1e595ac3d024cb8ad7d308b4cd95f8313"}, + {file = "charset_normalizer-3.4.1-cp313-cp313-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:8436c508b408b82d87dc5f62496973a1805cd46727c34440b0d29d8a2f50a6c9"}, + {file = "charset_normalizer-3.4.1-cp313-cp313-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:2d074908e1aecee37a7635990b2c6d504cd4766c7bc9fc86d63f9c09af3fa11b"}, + {file = "charset_normalizer-3.4.1-cp313-cp313-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:955f8851919303c92343d2f66165294848d57e9bba6cf6e3625485a70a038d11"}, + {file = "charset_normalizer-3.4.1-cp313-cp313-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:44ecbf16649486d4aebafeaa7ec4c9fed8b88101f4dd612dcaf65d5e815f837f"}, + {file = "charset_normalizer-3.4.1-cp313-cp313-musllinux_1_2_aarch64.whl", hash = "sha256:0924e81d3d5e70f8126529951dac65c1010cdf117bb75eb02dd12339b57749dd"}, + {file = "charset_normalizer-3.4.1-cp313-cp313-musllinux_1_2_i686.whl", hash = "sha256:2967f74ad52c3b98de4c3b32e1a44e32975e008a9cd2a8cc8966d6a5218c5cb2"}, + {file = "charset_normalizer-3.4.1-cp313-cp313-musllinux_1_2_ppc64le.whl", hash = "sha256:c75cb2a3e389853835e84a2d8fb2b81a10645b503eca9bcb98df6b5a43eb8886"}, + {file = "charset_normalizer-3.4.1-cp313-cp313-musllinux_1_2_s390x.whl", hash = "sha256:09b26ae6b1abf0d27570633b2b078a2a20419c99d66fb2823173d73f188ce601"}, + {file = "charset_normalizer-3.4.1-cp313-cp313-musllinux_1_2_x86_64.whl", hash = "sha256:fa88b843d6e211393a37219e6a1c1df99d35e8fd90446f1118f4216e307e48cd"}, + {file = "charset_normalizer-3.4.1-cp313-cp313-win32.whl", hash = "sha256:eb8178fe3dba6450a3e024e95ac49ed3400e506fd4e9e5c32d30adda88cbd407"}, + {file = "charset_normalizer-3.4.1-cp313-cp313-win_amd64.whl", hash = "sha256:b1ac5992a838106edb89654e0aebfc24f5848ae2547d22c2c3f66454daa11971"}, + {file = "charset_normalizer-3.4.1-cp37-cp37m-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:f30bf9fd9be89ecb2360c7d94a711f00c09b976258846efe40db3d05828e8089"}, + {file = "charset_normalizer-3.4.1-cp37-cp37m-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:97f68b8d6831127e4787ad15e6757232e14e12060bec17091b85eb1486b91d8d"}, + {file = "charset_normalizer-3.4.1-cp37-cp37m-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:7974a0b5ecd505609e3b19742b60cee7aa2aa2fb3151bc917e6e2646d7667dcf"}, + {file = "charset_normalizer-3.4.1-cp37-cp37m-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:fc54db6c8593ef7d4b2a331b58653356cf04f67c960f584edb7c3d8c97e8f39e"}, + {file = "charset_normalizer-3.4.1-cp37-cp37m-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:311f30128d7d333eebd7896965bfcfbd0065f1716ec92bd5638d7748eb6f936a"}, + {file = "charset_normalizer-3.4.1-cp37-cp37m-musllinux_1_2_aarch64.whl", hash = "sha256:7d053096f67cd1241601111b698f5cad775f97ab25d81567d3f59219b5f1adbd"}, + {file = "charset_normalizer-3.4.1-cp37-cp37m-musllinux_1_2_i686.whl", hash = "sha256:807f52c1f798eef6cf26beb819eeb8819b1622ddfeef9d0977a8502d4db6d534"}, + {file = "charset_normalizer-3.4.1-cp37-cp37m-musllinux_1_2_ppc64le.whl", hash = "sha256:dccbe65bd2f7f7ec22c4ff99ed56faa1e9f785482b9bbd7c717e26fd723a1d1e"}, + {file = "charset_normalizer-3.4.1-cp37-cp37m-musllinux_1_2_s390x.whl", hash = "sha256:2fb9bd477fdea8684f78791a6de97a953c51831ee2981f8e4f583ff3b9d9687e"}, + {file = "charset_normalizer-3.4.1-cp37-cp37m-musllinux_1_2_x86_64.whl", hash = "sha256:01732659ba9b5b873fc117534143e4feefecf3b2078b0a6a2e925271bb6f4cfa"}, + {file = "charset_normalizer-3.4.1-cp37-cp37m-win32.whl", hash = "sha256:7a4f97a081603d2050bfaffdefa5b02a9ec823f8348a572e39032caa8404a487"}, + {file = "charset_normalizer-3.4.1-cp37-cp37m-win_amd64.whl", hash = "sha256:7b1bef6280950ee6c177b326508f86cad7ad4dff12454483b51d8b7d673a2c5d"}, + {file = "charset_normalizer-3.4.1-cp38-cp38-macosx_10_9_universal2.whl", hash = "sha256:ecddf25bee22fe4fe3737a399d0d177d72bc22be6913acfab364b40bce1ba83c"}, + {file = "charset_normalizer-3.4.1-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:8c60ca7339acd497a55b0ea5d506b2a2612afb2826560416f6894e8b5770d4a9"}, + {file = "charset_normalizer-3.4.1-cp38-cp38-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:b7b2d86dd06bfc2ade3312a83a5c364c7ec2e3498f8734282c6c3d4b07b346b8"}, + {file = "charset_normalizer-3.4.1-cp38-cp38-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:dd78cfcda14a1ef52584dbb008f7ac81c1328c0f58184bf9a84c49c605002da6"}, + {file = "charset_normalizer-3.4.1-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:6e27f48bcd0957c6d4cb9d6fa6b61d192d0b13d5ef563e5f2ae35feafc0d179c"}, + {file = "charset_normalizer-3.4.1-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:01ad647cdd609225c5350561d084b42ddf732f4eeefe6e678765636791e78b9a"}, + {file = "charset_normalizer-3.4.1-cp38-cp38-musllinux_1_2_aarch64.whl", hash = "sha256:619a609aa74ae43d90ed2e89bdd784765de0a25ca761b93e196d938b8fd1dbbd"}, + {file = "charset_normalizer-3.4.1-cp38-cp38-musllinux_1_2_i686.whl", hash = "sha256:89149166622f4db9b4b6a449256291dc87a99ee53151c74cbd82a53c8c2f6ccd"}, + {file = "charset_normalizer-3.4.1-cp38-cp38-musllinux_1_2_ppc64le.whl", hash = "sha256:7709f51f5f7c853f0fb938bcd3bc59cdfdc5203635ffd18bf354f6967ea0f824"}, + {file = "charset_normalizer-3.4.1-cp38-cp38-musllinux_1_2_s390x.whl", hash = "sha256:345b0426edd4e18138d6528aed636de7a9ed169b4aaf9d61a8c19e39d26838ca"}, + {file = "charset_normalizer-3.4.1-cp38-cp38-musllinux_1_2_x86_64.whl", hash = "sha256:0907f11d019260cdc3f94fbdb23ff9125f6b5d1039b76003b5b0ac9d6a6c9d5b"}, + {file = "charset_normalizer-3.4.1-cp38-cp38-win32.whl", hash = "sha256:ea0d8d539afa5eb2728aa1932a988a9a7af94f18582ffae4bc10b3fbdad0626e"}, + {file = "charset_normalizer-3.4.1-cp38-cp38-win_amd64.whl", hash = "sha256:329ce159e82018d646c7ac45b01a430369d526569ec08516081727a20e9e4af4"}, + {file = "charset_normalizer-3.4.1-cp39-cp39-macosx_10_9_universal2.whl", hash = "sha256:b97e690a2118911e39b4042088092771b4ae3fc3aa86518f84b8cf6888dbdb41"}, + {file = "charset_normalizer-3.4.1-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:78baa6d91634dfb69ec52a463534bc0df05dbd546209b79a3880a34487f4b84f"}, + {file = "charset_normalizer-3.4.1-cp39-cp39-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:1a2bc9f351a75ef49d664206d51f8e5ede9da246602dc2d2726837620ea034b2"}, + {file = "charset_normalizer-3.4.1-cp39-cp39-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:75832c08354f595c760a804588b9357d34ec00ba1c940c15e31e96d902093770"}, + {file = "charset_normalizer-3.4.1-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:0af291f4fe114be0280cdd29d533696a77b5b49cfde5467176ecab32353395c4"}, + {file = "charset_normalizer-3.4.1-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:0167ddc8ab6508fe81860a57dd472b2ef4060e8d378f0cc555707126830f2537"}, + {file = "charset_normalizer-3.4.1-cp39-cp39-musllinux_1_2_aarch64.whl", hash = "sha256:2a75d49014d118e4198bcee5ee0a6f25856b29b12dbf7cd012791f8a6cc5c496"}, + {file = "charset_normalizer-3.4.1-cp39-cp39-musllinux_1_2_i686.whl", hash = "sha256:363e2f92b0f0174b2f8238240a1a30142e3db7b957a5dd5689b0e75fb717cc78"}, + {file = "charset_normalizer-3.4.1-cp39-cp39-musllinux_1_2_ppc64le.whl", hash = "sha256:ab36c8eb7e454e34e60eb55ca5d241a5d18b2c6244f6827a30e451c42410b5f7"}, + {file = "charset_normalizer-3.4.1-cp39-cp39-musllinux_1_2_s390x.whl", hash = "sha256:4c0907b1928a36d5a998d72d64d8eaa7244989f7aaaf947500d3a800c83a3fd6"}, + {file = "charset_normalizer-3.4.1-cp39-cp39-musllinux_1_2_x86_64.whl", hash = "sha256:04432ad9479fa40ec0f387795ddad4437a2b50417c69fa275e212933519ff294"}, + {file = "charset_normalizer-3.4.1-cp39-cp39-win32.whl", hash = "sha256:3bed14e9c89dcb10e8f3a29f9ccac4955aebe93c71ae803af79265c9ca5644c5"}, + {file = "charset_normalizer-3.4.1-cp39-cp39-win_amd64.whl", hash = "sha256:49402233c892a461407c512a19435d1ce275543138294f7ef013f0b63d5d3765"}, + {file = "charset_normalizer-3.4.1-py3-none-any.whl", hash = "sha256:d98b1668f06378c6dbefec3b92299716b931cd4e6061f3c875a71ced1780ab85"}, + {file = "charset_normalizer-3.4.1.tar.gz", hash = "sha256:44251f18cd68a75b56585dd00dae26183e102cd5e0f9f1466e6df5da2ed64ea3"}, +] + [[package]] name = "classify-imports" version = "4.2.0" @@ -155,6 +311,27 @@ humanfriendly = ">=9.1" [package.extras] cron = ["capturer (>=2.4)"] +[[package]] +name = "cookiecutter" +version = "2.6.0" +description = "A command-line utility that creates projects from project templates, e.g. creating a Python package project from a Python package project template." +optional = false +python-versions = ">=3.7" +files = [ + {file = "cookiecutter-2.6.0-py3-none-any.whl", hash = "sha256:a54a8e37995e4ed963b3e82831072d1ad4b005af736bb17b99c2cbd9d41b6e2d"}, + {file = "cookiecutter-2.6.0.tar.gz", hash = "sha256:db21f8169ea4f4fdc2408d48ca44859349de2647fbe494a9d6c3edfc0542c21c"}, +] + +[package.dependencies] +arrow = "*" +binaryornot = ">=0.4.4" +click = ">=7.0,<9.0.0" +Jinja2 = ">=2.7,<4.0.0" +python-slugify = ">=4.0.0" +pyyaml = ">=5.3.1" +requests = ">=2.23.0" +rich = "*" + [[package]] name = "coverage" version = "7.5.3" @@ -406,6 +583,20 @@ pytz = ["pytz (>=2014.1)"] redis = ["redis (>=3.0.0)"] zoneinfo = ["backports.zoneinfo (>=0.2.1)", "tzdata (>=2024.1)"] +[[package]] +name = "idna" +version = "3.10" +description = "Internationalized Domain Names in Applications (IDNA)" +optional = false +python-versions = ">=3.6" +files = [ + {file = "idna-3.10-py3-none-any.whl", hash = "sha256:946d195a0d259cbba61165e88e65941f16e9b36ea6ddb97f00452bae8b1287d3"}, + {file = "idna-3.10.tar.gz", hash = "sha256:12f65c9b470abda6dc35cf8e63cc574b1c52b11df2c86030af0ac09b01b13ea9"}, +] + +[package.extras] +all = ["flake8 (>=7.1.1)", "mypy (>=1.11.2)", "pytest (>=8.3.2)", "ruff (>=0.6.2)"] + [[package]] name = "importlib-metadata" version = "7.1.0" @@ -450,6 +641,23 @@ files = [ [package.extras] colors = ["colorama (>=0.4.6)"] +[[package]] +name = "jinja2" +version = "3.1.5" +description = "A very fast and expressive template engine." +optional = false +python-versions = ">=3.7" +files = [ + {file = "jinja2-3.1.5-py3-none-any.whl", hash = "sha256:aba0f4dc9ed8013c424088f68a5c226f7d6097ed89b246d7749c2ec4175c6adb"}, + {file = "jinja2-3.1.5.tar.gz", hash = "sha256:8fefff8dc3034e27bb80d67c671eb8a9bc424c0ef4c0826edbff304cceff43bb"}, +] + +[package.dependencies] +MarkupSafe = ">=2.0" + +[package.extras] +i18n = ["Babel (>=2.7)"] + [[package]] name = "linkify-it-py" version = "2.0.3" @@ -496,6 +704,76 @@ profiling = ["gprof2dot"] rtd = ["attrs", "myst-parser", "pyyaml", "sphinx", "sphinx-copybutton", "sphinx-design", "sphinx_book_theme"] testing = ["coverage", "pytest", "pytest-cov", "pytest-regressions"] +[[package]] +name = "markupsafe" +version = "3.0.2" +description = "Safely add untrusted strings to HTML/XML markup." +optional = false +python-versions = ">=3.9" +files = [ + {file = "MarkupSafe-3.0.2-cp310-cp310-macosx_10_9_universal2.whl", hash = "sha256:7e94c425039cde14257288fd61dcfb01963e658efbc0ff54f5306b06054700f8"}, + {file = "MarkupSafe-3.0.2-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:9e2d922824181480953426608b81967de705c3cef4d1af983af849d7bd619158"}, + {file = "MarkupSafe-3.0.2-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:38a9ef736c01fccdd6600705b09dc574584b89bea478200c5fbf112a6b0d5579"}, + {file = "MarkupSafe-3.0.2-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:bbcb445fa71794da8f178f0f6d66789a28d7319071af7a496d4d507ed566270d"}, + {file = "MarkupSafe-3.0.2-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:57cb5a3cf367aeb1d316576250f65edec5bb3be939e9247ae594b4bcbc317dfb"}, + {file = "MarkupSafe-3.0.2-cp310-cp310-musllinux_1_2_aarch64.whl", hash = "sha256:3809ede931876f5b2ec92eef964286840ed3540dadf803dd570c3b7e13141a3b"}, + {file = "MarkupSafe-3.0.2-cp310-cp310-musllinux_1_2_i686.whl", hash = "sha256:e07c3764494e3776c602c1e78e298937c3315ccc9043ead7e685b7f2b8d47b3c"}, + {file = "MarkupSafe-3.0.2-cp310-cp310-musllinux_1_2_x86_64.whl", hash = "sha256:b424c77b206d63d500bcb69fa55ed8d0e6a3774056bdc4839fc9298a7edca171"}, + {file = "MarkupSafe-3.0.2-cp310-cp310-win32.whl", hash = "sha256:fcabf5ff6eea076f859677f5f0b6b5c1a51e70a376b0579e0eadef8db48c6b50"}, + {file = "MarkupSafe-3.0.2-cp310-cp310-win_amd64.whl", hash = "sha256:6af100e168aa82a50e186c82875a5893c5597a0c1ccdb0d8b40240b1f28b969a"}, + {file = "MarkupSafe-3.0.2-cp311-cp311-macosx_10_9_universal2.whl", hash = "sha256:9025b4018f3a1314059769c7bf15441064b2207cb3f065e6ea1e7359cb46db9d"}, + {file = "MarkupSafe-3.0.2-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:93335ca3812df2f366e80509ae119189886b0f3c2b81325d39efdb84a1e2ae93"}, + {file = "MarkupSafe-3.0.2-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:2cb8438c3cbb25e220c2ab33bb226559e7afb3baec11c4f218ffa7308603c832"}, + {file = "MarkupSafe-3.0.2-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:a123e330ef0853c6e822384873bef7507557d8e4a082961e1defa947aa59ba84"}, + {file = "MarkupSafe-3.0.2-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:1e084f686b92e5b83186b07e8a17fc09e38fff551f3602b249881fec658d3eca"}, + {file = "MarkupSafe-3.0.2-cp311-cp311-musllinux_1_2_aarch64.whl", hash = "sha256:d8213e09c917a951de9d09ecee036d5c7d36cb6cb7dbaece4c71a60d79fb9798"}, + {file = "MarkupSafe-3.0.2-cp311-cp311-musllinux_1_2_i686.whl", hash = "sha256:5b02fb34468b6aaa40dfc198d813a641e3a63b98c2b05a16b9f80b7ec314185e"}, + {file = "MarkupSafe-3.0.2-cp311-cp311-musllinux_1_2_x86_64.whl", hash = "sha256:0bff5e0ae4ef2e1ae4fdf2dfd5b76c75e5c2fa4132d05fc1b0dabcd20c7e28c4"}, + {file = "MarkupSafe-3.0.2-cp311-cp311-win32.whl", hash = "sha256:6c89876f41da747c8d3677a2b540fb32ef5715f97b66eeb0c6b66f5e3ef6f59d"}, + {file = "MarkupSafe-3.0.2-cp311-cp311-win_amd64.whl", hash = "sha256:70a87b411535ccad5ef2f1df5136506a10775d267e197e4cf531ced10537bd6b"}, + {file = "MarkupSafe-3.0.2-cp312-cp312-macosx_10_13_universal2.whl", hash = "sha256:9778bd8ab0a994ebf6f84c2b949e65736d5575320a17ae8984a77fab08db94cf"}, + {file = "MarkupSafe-3.0.2-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:846ade7b71e3536c4e56b386c2a47adf5741d2d8b94ec9dc3e92e5e1ee1e2225"}, + {file = "MarkupSafe-3.0.2-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:1c99d261bd2d5f6b59325c92c73df481e05e57f19837bdca8413b9eac4bd8028"}, + {file = "MarkupSafe-3.0.2-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:e17c96c14e19278594aa4841ec148115f9c7615a47382ecb6b82bd8fea3ab0c8"}, + {file = "MarkupSafe-3.0.2-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:88416bd1e65dcea10bc7569faacb2c20ce071dd1f87539ca2ab364bf6231393c"}, + {file = "MarkupSafe-3.0.2-cp312-cp312-musllinux_1_2_aarch64.whl", hash = "sha256:2181e67807fc2fa785d0592dc2d6206c019b9502410671cc905d132a92866557"}, + {file = "MarkupSafe-3.0.2-cp312-cp312-musllinux_1_2_i686.whl", hash = "sha256:52305740fe773d09cffb16f8ed0427942901f00adedac82ec8b67752f58a1b22"}, + {file = "MarkupSafe-3.0.2-cp312-cp312-musllinux_1_2_x86_64.whl", hash = "sha256:ad10d3ded218f1039f11a75f8091880239651b52e9bb592ca27de44eed242a48"}, + {file = "MarkupSafe-3.0.2-cp312-cp312-win32.whl", hash = "sha256:0f4ca02bea9a23221c0182836703cbf8930c5e9454bacce27e767509fa286a30"}, + {file = "MarkupSafe-3.0.2-cp312-cp312-win_amd64.whl", hash = "sha256:8e06879fc22a25ca47312fbe7c8264eb0b662f6db27cb2d3bbbc74b1df4b9b87"}, + {file = "MarkupSafe-3.0.2-cp313-cp313-macosx_10_13_universal2.whl", hash = "sha256:ba9527cdd4c926ed0760bc301f6728ef34d841f405abf9d4f959c478421e4efd"}, + {file = "MarkupSafe-3.0.2-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:f8b3d067f2e40fe93e1ccdd6b2e1d16c43140e76f02fb1319a05cf2b79d99430"}, + {file = "MarkupSafe-3.0.2-cp313-cp313-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:569511d3b58c8791ab4c2e1285575265991e6d8f8700c7be0e88f86cb0672094"}, + {file = "MarkupSafe-3.0.2-cp313-cp313-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:15ab75ef81add55874e7ab7055e9c397312385bd9ced94920f2802310c930396"}, + {file = "MarkupSafe-3.0.2-cp313-cp313-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:f3818cb119498c0678015754eba762e0d61e5b52d34c8b13d770f0719f7b1d79"}, + {file = "MarkupSafe-3.0.2-cp313-cp313-musllinux_1_2_aarch64.whl", hash = "sha256:cdb82a876c47801bb54a690c5ae105a46b392ac6099881cdfb9f6e95e4014c6a"}, + {file = "MarkupSafe-3.0.2-cp313-cp313-musllinux_1_2_i686.whl", hash = "sha256:cabc348d87e913db6ab4aa100f01b08f481097838bdddf7c7a84b7575b7309ca"}, + {file = "MarkupSafe-3.0.2-cp313-cp313-musllinux_1_2_x86_64.whl", hash = "sha256:444dcda765c8a838eaae23112db52f1efaf750daddb2d9ca300bcae1039adc5c"}, + {file = "MarkupSafe-3.0.2-cp313-cp313-win32.whl", hash = "sha256:bcf3e58998965654fdaff38e58584d8937aa3096ab5354d493c77d1fdd66d7a1"}, + {file = "MarkupSafe-3.0.2-cp313-cp313-win_amd64.whl", hash = "sha256:e6a2a455bd412959b57a172ce6328d2dd1f01cb2135efda2e4576e8a23fa3b0f"}, + {file = "MarkupSafe-3.0.2-cp313-cp313t-macosx_10_13_universal2.whl", hash = "sha256:b5a6b3ada725cea8a5e634536b1b01c30bcdcd7f9c6fff4151548d5bf6b3a36c"}, + {file = "MarkupSafe-3.0.2-cp313-cp313t-macosx_11_0_arm64.whl", hash = "sha256:a904af0a6162c73e3edcb969eeeb53a63ceeb5d8cf642fade7d39e7963a22ddb"}, + {file = "MarkupSafe-3.0.2-cp313-cp313t-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:4aa4e5faecf353ed117801a068ebab7b7e09ffb6e1d5e412dc852e0da018126c"}, + {file = "MarkupSafe-3.0.2-cp313-cp313t-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:c0ef13eaeee5b615fb07c9a7dadb38eac06a0608b41570d8ade51c56539e509d"}, + {file = "MarkupSafe-3.0.2-cp313-cp313t-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:d16a81a06776313e817c951135cf7340a3e91e8c1ff2fac444cfd75fffa04afe"}, + {file = "MarkupSafe-3.0.2-cp313-cp313t-musllinux_1_2_aarch64.whl", hash = "sha256:6381026f158fdb7c72a168278597a5e3a5222e83ea18f543112b2662a9b699c5"}, + {file = "MarkupSafe-3.0.2-cp313-cp313t-musllinux_1_2_i686.whl", hash = "sha256:3d79d162e7be8f996986c064d1c7c817f6df3a77fe3d6859f6f9e7be4b8c213a"}, + {file = "MarkupSafe-3.0.2-cp313-cp313t-musllinux_1_2_x86_64.whl", hash = "sha256:131a3c7689c85f5ad20f9f6fb1b866f402c445b220c19fe4308c0b147ccd2ad9"}, + {file = "MarkupSafe-3.0.2-cp313-cp313t-win32.whl", hash = "sha256:ba8062ed2cf21c07a9e295d5b8a2a5ce678b913b45fdf68c32d95d6c1291e0b6"}, + {file = "MarkupSafe-3.0.2-cp313-cp313t-win_amd64.whl", hash = "sha256:e444a31f8db13eb18ada366ab3cf45fd4b31e4db1236a4448f68778c1d1a5a2f"}, + {file = "MarkupSafe-3.0.2-cp39-cp39-macosx_10_9_universal2.whl", hash = "sha256:eaa0a10b7f72326f1372a713e73c3f739b524b3af41feb43e4921cb529f5929a"}, + {file = "MarkupSafe-3.0.2-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:48032821bbdf20f5799ff537c7ac3d1fba0ba032cfc06194faffa8cda8b560ff"}, + {file = "MarkupSafe-3.0.2-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:1a9d3f5f0901fdec14d8d2f66ef7d035f2157240a433441719ac9a3fba440b13"}, + {file = "MarkupSafe-3.0.2-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:88b49a3b9ff31e19998750c38e030fc7bb937398b1f78cfa599aaef92d693144"}, + {file = "MarkupSafe-3.0.2-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:cfad01eed2c2e0c01fd0ecd2ef42c492f7f93902e39a42fc9ee1692961443a29"}, + {file = "MarkupSafe-3.0.2-cp39-cp39-musllinux_1_2_aarch64.whl", hash = "sha256:1225beacc926f536dc82e45f8a4d68502949dc67eea90eab715dea3a21c1b5f0"}, + {file = "MarkupSafe-3.0.2-cp39-cp39-musllinux_1_2_i686.whl", hash = "sha256:3169b1eefae027567d1ce6ee7cae382c57fe26e82775f460f0b2778beaad66c0"}, + {file = "MarkupSafe-3.0.2-cp39-cp39-musllinux_1_2_x86_64.whl", hash = "sha256:eb7972a85c54febfb25b5c4b4f3af4dcc731994c7da0d8a0b4a6eb0640e1d178"}, + {file = "MarkupSafe-3.0.2-cp39-cp39-win32.whl", hash = "sha256:8c4e8c3ce11e1f92f6536ff07154f9d49677ebaaafc32db9db4620bc11ed480f"}, + {file = "MarkupSafe-3.0.2-cp39-cp39-win_amd64.whl", hash = "sha256:6e296a513ca3d94054c2c881cc913116e90fd030ad1c656b3869762b754f5f8a"}, + {file = "markupsafe-3.0.2.tar.gz", hash = "sha256:ee55d3edf80167e48ea11a923c7386f4669df67d7994554387f84e7d8b0a2bf0"}, +] + [[package]] name = "mccabe" version = "0.7.0" @@ -867,6 +1145,37 @@ psutil = ["psutil (>=3.0)"] setproctitle = ["setproctitle"] testing = ["filelock"] +[[package]] +name = "python-dateutil" +version = "2.9.0.post0" +description = "Extensions to the standard Python datetime module" +optional = false +python-versions = "!=3.0.*,!=3.1.*,!=3.2.*,>=2.7" +files = [ + {file = "python-dateutil-2.9.0.post0.tar.gz", hash = "sha256:37dd54208da7e1cd875388217d5e00ebd4179249f90fb72437e91a35459a0ad3"}, + {file = "python_dateutil-2.9.0.post0-py2.py3-none-any.whl", hash = "sha256:a8b2bc7bffae282281c8140a97d3aa9c14da0b136dfe83f850eea9a5f7470427"}, +] + +[package.dependencies] +six = ">=1.5" + +[[package]] +name = "python-slugify" +version = "8.0.4" +description = "A Python slugify application that also handles Unicode" +optional = false +python-versions = ">=3.7" +files = [ + {file = "python-slugify-8.0.4.tar.gz", hash = "sha256:59202371d1d05b54a9e7720c5e038f928f45daaffe41dd10822f3907b937c856"}, + {file = "python_slugify-8.0.4-py2.py3-none-any.whl", hash = "sha256:276540b79961052b66b7d116620b36518847f52d5fd9e3a70164fc8c50faa6b8"}, +] + +[package.dependencies] +text-unidecode = ">=1.3" + +[package.extras] +unidecode = ["Unidecode (>=1.1.1)"] + [[package]] name = "pyupgrade" version = "3.16.0" @@ -881,6 +1190,89 @@ files = [ [package.dependencies] tokenize-rt = ">=5.2.0" +[[package]] +name = "pyyaml" +version = "6.0.2" +description = "YAML parser and emitter for Python" +optional = false +python-versions = ">=3.8" +files = [ + {file = "PyYAML-6.0.2-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:0a9a2848a5b7feac301353437eb7d5957887edbf81d56e903999a75a3d743086"}, + {file = "PyYAML-6.0.2-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:29717114e51c84ddfba879543fb232a6ed60086602313ca38cce623c1d62cfbf"}, + {file = "PyYAML-6.0.2-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:8824b5a04a04a047e72eea5cec3bc266db09e35de6bdfe34c9436ac5ee27d237"}, + {file = "PyYAML-6.0.2-cp310-cp310-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:7c36280e6fb8385e520936c3cb3b8042851904eba0e58d277dca80a5cfed590b"}, + {file = "PyYAML-6.0.2-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:ec031d5d2feb36d1d1a24380e4db6d43695f3748343d99434e6f5f9156aaa2ed"}, + {file = "PyYAML-6.0.2-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:936d68689298c36b53b29f23c6dbb74de12b4ac12ca6cfe0e047bedceea56180"}, + {file = "PyYAML-6.0.2-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:23502f431948090f597378482b4812b0caae32c22213aecf3b55325e049a6c68"}, + {file = "PyYAML-6.0.2-cp310-cp310-win32.whl", hash = "sha256:2e99c6826ffa974fe6e27cdb5ed0021786b03fc98e5ee3c5bfe1fd5015f42b99"}, + {file = "PyYAML-6.0.2-cp310-cp310-win_amd64.whl", hash = "sha256:a4d3091415f010369ae4ed1fc6b79def9416358877534caf6a0fdd2146c87a3e"}, + {file = "PyYAML-6.0.2-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:cc1c1159b3d456576af7a3e4d1ba7e6924cb39de8f67111c735f6fc832082774"}, + {file = "PyYAML-6.0.2-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:1e2120ef853f59c7419231f3bf4e7021f1b936f6ebd222406c3b60212205d2ee"}, + {file = "PyYAML-6.0.2-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:5d225db5a45f21e78dd9358e58a98702a0302f2659a3c6cd320564b75b86f47c"}, + {file = "PyYAML-6.0.2-cp311-cp311-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:5ac9328ec4831237bec75defaf839f7d4564be1e6b25ac710bd1a96321cc8317"}, + {file = "PyYAML-6.0.2-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:3ad2a3decf9aaba3d29c8f537ac4b243e36bef957511b4766cb0057d32b0be85"}, + {file = "PyYAML-6.0.2-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:ff3824dc5261f50c9b0dfb3be22b4567a6f938ccce4587b38952d85fd9e9afe4"}, + {file = "PyYAML-6.0.2-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:797b4f722ffa07cc8d62053e4cff1486fa6dc094105d13fea7b1de7d8bf71c9e"}, + {file = "PyYAML-6.0.2-cp311-cp311-win32.whl", hash = "sha256:11d8f3dd2b9c1207dcaf2ee0bbbfd5991f571186ec9cc78427ba5bd32afae4b5"}, + {file = "PyYAML-6.0.2-cp311-cp311-win_amd64.whl", hash = "sha256:e10ce637b18caea04431ce14fabcf5c64a1c61ec9c56b071a4b7ca131ca52d44"}, + {file = "PyYAML-6.0.2-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:c70c95198c015b85feafc136515252a261a84561b7b1d51e3384e0655ddf25ab"}, + {file = "PyYAML-6.0.2-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:ce826d6ef20b1bc864f0a68340c8b3287705cae2f8b4b1d932177dcc76721725"}, + {file = "PyYAML-6.0.2-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:1f71ea527786de97d1a0cc0eacd1defc0985dcf6b3f17bb77dcfc8c34bec4dc5"}, + {file = "PyYAML-6.0.2-cp312-cp312-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:9b22676e8097e9e22e36d6b7bda33190d0d400f345f23d4065d48f4ca7ae0425"}, + {file = "PyYAML-6.0.2-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:80bab7bfc629882493af4aa31a4cfa43a4c57c83813253626916b8c7ada83476"}, + {file = "PyYAML-6.0.2-cp312-cp312-musllinux_1_1_aarch64.whl", hash = "sha256:0833f8694549e586547b576dcfaba4a6b55b9e96098b36cdc7ebefe667dfed48"}, + {file = "PyYAML-6.0.2-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:8b9c7197f7cb2738065c481a0461e50ad02f18c78cd75775628afb4d7137fb3b"}, + {file = "PyYAML-6.0.2-cp312-cp312-win32.whl", hash = "sha256:ef6107725bd54b262d6dedcc2af448a266975032bc85ef0172c5f059da6325b4"}, + {file = "PyYAML-6.0.2-cp312-cp312-win_amd64.whl", hash = "sha256:7e7401d0de89a9a855c839bc697c079a4af81cf878373abd7dc625847d25cbd8"}, + {file = "PyYAML-6.0.2-cp313-cp313-macosx_10_13_x86_64.whl", hash = "sha256:efdca5630322a10774e8e98e1af481aad470dd62c3170801852d752aa7a783ba"}, + {file = "PyYAML-6.0.2-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:50187695423ffe49e2deacb8cd10510bc361faac997de9efef88badc3bb9e2d1"}, + {file = "PyYAML-6.0.2-cp313-cp313-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:0ffe8360bab4910ef1b9e87fb812d8bc0a308b0d0eef8c8f44e0254ab3b07133"}, + {file = "PyYAML-6.0.2-cp313-cp313-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:17e311b6c678207928d649faa7cb0d7b4c26a0ba73d41e99c4fff6b6c3276484"}, + {file = "PyYAML-6.0.2-cp313-cp313-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:70b189594dbe54f75ab3a1acec5f1e3faa7e8cf2f1e08d9b561cb41b845f69d5"}, + {file = "PyYAML-6.0.2-cp313-cp313-musllinux_1_1_aarch64.whl", hash = "sha256:41e4e3953a79407c794916fa277a82531dd93aad34e29c2a514c2c0c5fe971cc"}, + {file = "PyYAML-6.0.2-cp313-cp313-musllinux_1_1_x86_64.whl", hash = "sha256:68ccc6023a3400877818152ad9a1033e3db8625d899c72eacb5a668902e4d652"}, + {file = "PyYAML-6.0.2-cp313-cp313-win32.whl", hash = "sha256:bc2fa7c6b47d6bc618dd7fb02ef6fdedb1090ec036abab80d4681424b84c1183"}, + {file = "PyYAML-6.0.2-cp313-cp313-win_amd64.whl", hash = "sha256:8388ee1976c416731879ac16da0aff3f63b286ffdd57cdeb95f3f2e085687563"}, + {file = "PyYAML-6.0.2-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:24471b829b3bf607e04e88d79542a9d48bb037c2267d7927a874e6c205ca7e9a"}, + {file = "PyYAML-6.0.2-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:d7fded462629cfa4b685c5416b949ebad6cec74af5e2d42905d41e257e0869f5"}, + {file = "PyYAML-6.0.2-cp38-cp38-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:d84a1718ee396f54f3a086ea0a66d8e552b2ab2017ef8b420e92edbc841c352d"}, + {file = "PyYAML-6.0.2-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:9056c1ecd25795207ad294bcf39f2db3d845767be0ea6e6a34d856f006006083"}, + {file = "PyYAML-6.0.2-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:82d09873e40955485746739bcb8b4586983670466c23382c19cffecbf1fd8706"}, + {file = "PyYAML-6.0.2-cp38-cp38-win32.whl", hash = "sha256:43fa96a3ca0d6b1812e01ced1044a003533c47f6ee8aca31724f78e93ccc089a"}, + {file = "PyYAML-6.0.2-cp38-cp38-win_amd64.whl", hash = "sha256:01179a4a8559ab5de078078f37e5c1a30d76bb88519906844fd7bdea1b7729ff"}, + {file = "PyYAML-6.0.2-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:688ba32a1cffef67fd2e9398a2efebaea461578b0923624778664cc1c914db5d"}, + {file = "PyYAML-6.0.2-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:a8786accb172bd8afb8be14490a16625cbc387036876ab6ba70912730faf8e1f"}, + {file = "PyYAML-6.0.2-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:d8e03406cac8513435335dbab54c0d385e4a49e4945d2909a581c83647ca0290"}, + {file = "PyYAML-6.0.2-cp39-cp39-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:f753120cb8181e736c57ef7636e83f31b9c0d1722c516f7e86cf15b7aa57ff12"}, + {file = "PyYAML-6.0.2-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:3b1fdb9dc17f5a7677423d508ab4f243a726dea51fa5e70992e59a7411c89d19"}, + {file = "PyYAML-6.0.2-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:0b69e4ce7a131fe56b7e4d770c67429700908fc0752af059838b1cfb41960e4e"}, + {file = "PyYAML-6.0.2-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:a9f8c2e67970f13b16084e04f134610fd1d374bf477b17ec1599185cf611d725"}, + {file = "PyYAML-6.0.2-cp39-cp39-win32.whl", hash = "sha256:6395c297d42274772abc367baaa79683958044e5d3835486c16da75d2a694631"}, + {file = "PyYAML-6.0.2-cp39-cp39-win_amd64.whl", hash = "sha256:39693e1f8320ae4f43943590b49779ffb98acb81f788220ea932a6b6c51004d8"}, + {file = "pyyaml-6.0.2.tar.gz", hash = "sha256:d584d9ec91ad65861cc08d42e834324ef890a082e591037abe114850ff7bbc3e"}, +] + +[[package]] +name = "requests" +version = "2.32.3" +description = "Python HTTP for Humans." +optional = false +python-versions = ">=3.8" +files = [ + {file = "requests-2.32.3-py3-none-any.whl", hash = "sha256:70761cfe03c773ceb22aa2f671b4757976145175cdfca038c02654d061d6dcc6"}, + {file = "requests-2.32.3.tar.gz", hash = "sha256:55365417734eb18255590a9ff9eb97e9e1da868d4ccd6402399eaf68af20a760"}, +] + +[package.dependencies] +certifi = ">=2017.4.17" +charset-normalizer = ">=2,<4" +idna = ">=2.5,<4" +urllib3 = ">=1.21.1,<3" + +[package.extras] +socks = ["PySocks (>=1.5.6,!=1.5.7)"] +use-chardet-on-py3 = ["chardet (>=3.0.2,<6)"] + [[package]] name = "rich" version = "13.7.1" @@ -914,6 +1306,17 @@ files = [ docs = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "pygments-github-lexers (==0.0.5)", "pyproject-hooks (!=1.1)", "rst.linker (>=1.9)", "sphinx (>=3.5)", "sphinx-favicon", "sphinx-inline-tabs", "sphinx-lint", "sphinx-notfound-page (>=1,<2)", "sphinx-reredirects", "sphinxcontrib-towncrier"] testing = ["build[virtualenv] (>=1.0.3)", "filelock (>=3.4.0)", "importlib-metadata", "ini2toml[lite] (>=0.14)", "jaraco.develop (>=7.21)", "jaraco.envs (>=2.2)", "jaraco.path (>=3.2.0)", "jaraco.test", "mypy (==1.10.0)", "packaging (>=23.2)", "pip (>=19.1)", "pyproject-hooks (!=1.1)", "pytest (>=6,!=8.1.1)", "pytest-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=2.2)", "pytest-home (>=0.5)", "pytest-mypy", "pytest-perf", "pytest-ruff (>=0.3.2)", "pytest-subprocess", "pytest-timeout", "pytest-xdist (>=3)", "tomli", "tomli-w (>=1.0.0)", "virtualenv (>=13.0.0)", "wheel"] +[[package]] +name = "six" +version = "1.17.0" +description = "Python 2 and 3 compatibility utilities" +optional = false +python-versions = "!=3.0.*,!=3.1.*,!=3.2.*,>=2.7" +files = [ + {file = "six-1.17.0-py2.py3-none-any.whl", hash = "sha256:4721f391ed90541fddacab5acf947aa0d3dc7d27b2e1e8eda2be8970586c3274"}, + {file = "six-1.17.0.tar.gz", hash = "sha256:ff70335d468e7eb6ec65b95b99d3a2836546063f63acc5171de367e834932a81"}, +] + [[package]] name = "snowballstemmer" version = "2.2.0" @@ -936,6 +1339,17 @@ files = [ {file = "sortedcontainers-2.4.0.tar.gz", hash = "sha256:25caa5a06cc30b6b83d11423433f65d1f9d76c4c6a0c90e3379eaa43b9bfdb88"}, ] +[[package]] +name = "text-unidecode" +version = "1.3" +description = "The most basic Text::Unidecode port" +optional = false +python-versions = "*" +files = [ + {file = "text-unidecode-1.3.tar.gz", hash = "sha256:bad6603bb14d279193107714b288be206cac565dfa49aa5b105294dd5c4aab93"}, + {file = "text_unidecode-1.3-py2.py3-none-any.whl", hash = "sha256:1311f10e8b895935241623731c2ba64f4c455287888b18189350b67134a822e8"}, +] + [[package]] name = "textual" version = "0.27.0" @@ -989,6 +1403,17 @@ files = [ {file = "types_psutil-5.9.5.20240516-py3-none-any.whl", hash = "sha256:83146ded949a10167d9895e567b3b71e53ebc5e23fd8363eab62b3c76cce7b89"}, ] +[[package]] +name = "types-python-dateutil" +version = "2.9.0.20241206" +description = "Typing stubs for python-dateutil" +optional = false +python-versions = ">=3.8" +files = [ + {file = "types_python_dateutil-2.9.0.20241206-py3-none-any.whl", hash = "sha256:e248a4bc70a486d3e3ec84d0dc30eec3a5f979d6e7ee4123ae043eedbb987f53"}, + {file = "types_python_dateutil-2.9.0.20241206.tar.gz", hash = "sha256:18f493414c26ffba692a72369fea7a154c502646301ebfe3d56a04b3767284cb"}, +] + [[package]] name = "typing-extensions" version = "4.12.2" @@ -1014,6 +1439,23 @@ files = [ [package.extras] test = ["coverage", "pytest", "pytest-cov"] +[[package]] +name = "urllib3" +version = "2.3.0" +description = "HTTP library with thread-safe connection pooling, file post, and more." +optional = false +python-versions = ">=3.9" +files = [ + {file = "urllib3-2.3.0-py3-none-any.whl", hash = "sha256:1cee9ad369867bfdbbb48b7dd50374c0967a0bb7710050facf0dd6911440e3df"}, + {file = "urllib3-2.3.0.tar.gz", hash = "sha256:f8c5449b3cf0861679ce7e0503c7b44b5ec981bec0d1d3795a07f1ba96f0204d"}, +] + +[package.extras] +brotli = ["brotli (>=1.0.9)", "brotlicffi (>=0.8.0)"] +h2 = ["h2 (>=4,<5)"] +socks = ["pysocks (>=1.5.6,!=1.5.7,<2.0)"] +zstd = ["zstandard (>=0.18.0)"] + [[package]] name = "wcwidth" version = "0.2.13" @@ -1054,4 +1496,4 @@ test = ["big-O", "importlib-resources", "jaraco.functools", "jaraco.itertools", [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "ceee3227b60208193d4f1cdbbb5fd52ea428e31f521d3e9226234827615fc732" +content-hash = "d68e4d3e42c6afe82f422433eb2260b436cc4001a839646c108b84de9c444296" diff --git a/pyk/pyproject.toml b/pyk/pyproject.toml index a56b90d220f..d4818c7da5b 100644 --- a/pyk/pyproject.toml +++ b/pyk/pyproject.toml @@ -19,6 +19,7 @@ from = "src" python = "^3.10" cmd2 = "^2.4.2" coloredlogs = "^15.0.1" +cookiecutter = "^2.6.0" filelock = "^3.9.0" graphviz = "^0.20.1" hypothesis = "^6.103.1" @@ -91,3 +92,7 @@ ignore_missing_imports = true [[tool.mypy.overrides]] module = "coloredlogs" ignore_missing_imports = true + +[[tool.mypy.overrides]] +module = "cookiecutter.*" +ignore_missing_imports = true diff --git a/pyk/src/pyk/k2lean4/__init__.py b/pyk/src/pyk/k2lean4/__init__.py deleted file mode 100644 index f8cc8f95ded..00000000000 --- a/pyk/src/pyk/k2lean4/__init__.py +++ /dev/null @@ -1 +0,0 @@ -from .k2lean4 import K2Lean4 diff --git a/pyk/src/pyk/klean/__init__.py b/pyk/src/pyk/klean/__init__.py new file mode 100644 index 00000000000..0adf1bce1ae --- /dev/null +++ b/pyk/src/pyk/klean/__init__.py @@ -0,0 +1 @@ +from .generate import GenContext, generate diff --git a/pyk/src/pyk/klean/generate.py b/pyk/src/pyk/klean/generate.py new file mode 100644 index 00000000000..dcb1db4697a --- /dev/null +++ b/pyk/src/pyk/klean/generate.py @@ -0,0 +1,87 @@ +from __future__ import annotations + +from pathlib import Path +from typing import TYPE_CHECKING, TypedDict + +from ..kore.internal import KoreDefn +from .k2lean4 import K2Lean4 +from .model import Module + +if TYPE_CHECKING: + from collections.abc import Callable, Iterable + + +class GenContext(TypedDict): + package_name: str + library_name: str + + +def generate( + definition_dir: str | Path, + context: GenContext, + *, + output_dir: str | Path | None = None, +) -> Path: + definition_dir = Path(definition_dir) + output_dir = Path(output_dir) if output_dir is not None else Path('.') + + defn = _load_defn(definition_dir) + k2lean4 = K2Lean4(defn) + genmodel = { + 'Sorts': (k2lean4.sort_module, ['Prelude']), + 'Func': (k2lean4.func_module, ['Sorts']), + 'Inj': (k2lean4.inj_module, ['Sorts']), + 'Rewrite': (k2lean4.rewrite_module, ['Func', 'Inj']), + } + + modules = _gen_modules(context['library_name'], genmodel) + res = _gen_template(output_dir, context) + _write_modules(res, modules) + return res + + +def _gen_template(output_dir: Path, context: GenContext) -> Path: + from cookiecutter.generate import generate_files + + template_dir = Path(__file__).parent / 'template' + gen_res = generate_files( + repo_dir=str(template_dir), + output_dir=str(output_dir), + context={'cookiecutter': context}, + ) + + res = Path(gen_res) + assert res.is_dir() + return res + + +def _load_defn(definition_dir: Path) -> KoreDefn: + from ..kore.parser import KoreParser + + kore_text = (definition_dir / 'definition.kore').read_text() + definition = KoreParser(kore_text).definition() + + defn = KoreDefn.from_definition(definition) + defn = defn.project_to_rewrites() + return defn + + +def _gen_modules( + library_name: str, + genmodel: dict[str, tuple[Callable[[], Module], list[str]]], +) -> dict[Path, Module]: + def gen_module(generator: Callable[[], Module], imports: Iterable[str]) -> Module: + imports = tuple(f'{library_name}.{importt}' for importt in imports) + module = generator() + module = Module(imports=imports, commands=module.commands) + return module + + return { + Path(library_name) / f'{name}.lean': gen_module(generator, imports) + for name, (generator, imports) in genmodel.items() + } + + +def _write_modules(output_dir: Path, modules: dict[Path, Module]) -> None: + for path, module in modules.items(): + (output_dir / path).write_text(str(module)) diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/klean/k2lean4.py similarity index 97% rename from pyk/src/pyk/k2lean4/k2lean4.py rename to pyk/src/pyk/klean/k2lean4.py index 5a2247f3669..6fd83cfadf0 100644 --- a/pyk/src/pyk/k2lean4/k2lean4.py +++ b/pyk/src/pyk/klean/k2lean4.py @@ -200,10 +200,20 @@ def _symbol_ctor(self, sort: str, symbol: str) -> Ctor: def _symbol_ident(symbol: str) -> str: if symbol.startswith('Lbl'): symbol = symbol[3:] - symbol = unmunge(symbol) - if not _VALID_LEAN_IDENT.fullmatch(symbol): - symbol = f'«{symbol}»' - return symbol + return K2Lean4._escape_ident(symbol, kore=True) + + @staticmethod + def _var_ident(var: str) -> str: + assert var.startswith('Var') + return K2Lean4._escape_ident(var[3:], kore=True) + + @staticmethod + def _escape_ident(ident: str, *, kore: bool = False) -> str: + if kore: + ident = unmunge(ident) + if not _VALID_LEAN_IDENT.fullmatch(ident): + ident = f'«{ident}»' + return ident def _structure(self, sort: str) -> Structure: fields = self.structures[sort] @@ -334,14 +344,10 @@ def _rewrite_ctor(self, rule: RewriteRule) -> Ctor: @staticmethod def _rewrite_name(rule: RewriteRule) -> str: if rule.label: - return rule.label.replace('-', '_').replace('.', '_') + label = rule.label.replace('-', '_').replace('.', '_') + return K2Lean4._escape_ident(label) return f'_{rule.uid[:7]}' - @staticmethod - def _var_ident(name: str) -> str: - assert name.startswith('Var') - return K2Lean4._symbol_ident(name[3:]) - def _elim_fun_apps(self, pattern: Pattern, free: Iterator[str]) -> tuple[Pattern, dict[str, Pattern]]: """Replace ``foo(bar(x))`` with ``z`` and return mapping ``{y: bar(x), z: foo(y)}`` with ``y``, ``z`` fresh variables.""" defs: dict[str, Pattern] = {} diff --git a/pyk/src/pyk/k2lean4/model.py b/pyk/src/pyk/klean/model.py similarity index 96% rename from pyk/src/pyk/k2lean4/model.py rename to pyk/src/pyk/klean/model.py index c53e4c2a531..180619b4535 100644 --- a/pyk/src/pyk/k2lean4/model.py +++ b/pyk/src/pyk/klean/model.py @@ -20,14 +20,23 @@ def indent(text: str, n: int) -> str: @final @dataclass(frozen=True) class Module: + imports: tuple[str, ...] commands: tuple[Command, ...] - def __init__(self, commands: Iterable[Command] | None = None): + def __init__( + self, + imports: Iterable[str] | None = None, + commands: Iterable[Command] | None = None, + ): + imports = tuple(imports) if imports is not None else () commands = tuple(commands) if commands is not None else () + object.__setattr__(self, 'imports', imports) object.__setattr__(self, 'commands', commands) def __str__(self) -> str: - return '\n\n'.join(str(command) for command in self.commands) + imports = '\n'.join(f'import {importt}' for importt in self.imports) + commands = '\n\n'.join(str(command) for command in self.commands) + return '\n\n'.join(section for section in [imports, commands] if section) class Command(ABC): ... diff --git a/pyk/src/pyk/klean/template/cookiecutter.json b/pyk/src/pyk/klean/template/cookiecutter.json new file mode 100644 index 00000000000..0a69ea6c353 --- /dev/null +++ b/pyk/src/pyk/klean/template/cookiecutter.json @@ -0,0 +1,4 @@ +{ + "package_name": null, + "library_name": null +} diff --git a/pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/.gitignore b/pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/.gitignore new file mode 100644 index 00000000000..bfb30ec8c76 --- /dev/null +++ b/pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/lakefile.toml b/pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/lakefile.toml new file mode 100644 index 00000000000..115105e1cff --- /dev/null +++ b/pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/lakefile.toml @@ -0,0 +1,9 @@ +name = "{{ cookiecutter.package_name }}" +version = "0.1.0" +defaultTargets = ["{{ cookiecutter.library_name }}"] +weakLeanArgs = [ + "-D maxHeartbeats=10000000" +] + +[[lean_lib]] +name = "{{ cookiecutter.library_name }}" diff --git a/pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/lean-toolchain b/pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/lean-toolchain new file mode 100644 index 00000000000..2bf5ad0447d --- /dev/null +++ b/pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/lean-toolchain @@ -0,0 +1 @@ +stable diff --git a/pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/{{ cookiecutter.library_name }}.lean b/pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/{{ cookiecutter.library_name }}.lean new file mode 100644 index 00000000000..65df05e04cf --- /dev/null +++ b/pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/{{ cookiecutter.library_name }}.lean @@ -0,0 +1 @@ +import {{ cookiecutter.library_name }}.Rewrite diff --git a/pyk/src/pyk/k2lean4/Prelude.lean b/pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/{{ cookiecutter.library_name }}/Prelude.lean similarity index 56% rename from pyk/src/pyk/k2lean4/Prelude.lean rename to pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/{{ cookiecutter.library_name }}/Prelude.lean index a7d4e04c63b..c13cdce3031 100644 --- a/pyk/src/pyk/k2lean4/Prelude.lean +++ b/pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/{{ cookiecutter.library_name }}/Prelude.lean @@ -27,7 +27,6 @@ abbrev SortInt : Type := Int abbrev SortString : Type := String abbrev SortStringBuffer : Type := String -namespace MapHookDef /- The `Map` sort represents a generalized associative array. Each key can be paired with an arbitrary value, and can be used to reference its associated value. @@ -57,50 +56,49 @@ structure MapHookSig (K V : Type) where nodup : forall al : map, List.Nodup (keys al) -- We use axioms to have uninterpreted functions -variable (K V : Type) -axiom mapCAx : Type -- Map Carrier -axiom unitAx : mapCAx -axiom consAx : K → V → mapCAx → mapCAx -axiom lookupAx : mapCAx → K → Option V -axiom lookupAx? : mapCAx → K → V -- lookup with default -axiom updateAx : K → V → mapCAx → mapCAx -axiom deleteAx : mapCAx → K → mapCAx -axiom concatAx : mapCAx → mapCAx → Option mapCAx -axiom differenceAx : mapCAx → mapCAx → mapCAx -axiom updateMapAx : mapCAx → mapCAx → mapCAx -axiom removeAllAx : mapCAx → List K → mapCAx -axiom keysAx : mapCAx → List K -axiom in_keysAx : mapCAx → K → Bool -axiom valuesAx : mapCAx → List V -axiom sizeAx : mapCAx → Nat -axiom includesAx : mapCAx → mapCAx → Bool -- map inclusion -axiom choiceAx : mapCAx → K -- arbitrary key from a map -axiom nodupAx : forall m, List.Nodup (keysAx K m) +namespace MapHookDef + variable (K V : Type) + axiom mapCAx : Type -- Map Carrier + axiom unitAx : mapCAx + axiom consAx : K → V → mapCAx → mapCAx + axiom lookupAx : mapCAx → K → Option V + axiom lookupAx? : mapCAx → K → V -- lookup with default + axiom updateAx : K → V → mapCAx → mapCAx + axiom deleteAx : mapCAx → K → mapCAx + axiom concatAx : mapCAx → mapCAx → Option mapCAx + axiom differenceAx : mapCAx → mapCAx → mapCAx + axiom updateMapAx : mapCAx → mapCAx → mapCAx + axiom removeAllAx : mapCAx → List K → mapCAx + axiom keysAx : mapCAx → List K + axiom in_keysAx : mapCAx → K → Bool + axiom valuesAx : mapCAx → List V + axiom sizeAx : mapCAx → Nat + axiom includesAx : mapCAx → mapCAx → Bool -- map inclusion + axiom choiceAx : mapCAx → K -- arbitrary key from a map + axiom nodupAx : forall m, List.Nodup (keysAx K m) +end MapHookDef -- Uninterpreted Map implementation noncomputable def MapHook (K V : Type) : MapHookSig K V := - { map := mapCAx, - unit := unitAx, - cons := consAx K V, - lookup := lookupAx K V, - lookup? := lookupAx? K V, - update := updateAx K V, - delete := deleteAx K, - concat := concatAx, - difference := differenceAx, - updateMap := updateMapAx, - removeAll := removeAllAx K, - keys := keysAx K, - in_keys := in_keysAx K, - values := valuesAx V, - size := sizeAx, - includes := includesAx, - choice := choiceAx K, - nodup := nodupAx K } - -end MapHookDef + { map := MapHookDef.mapCAx, + unit := MapHookDef.unitAx, + cons := MapHookDef.consAx K V, + lookup := MapHookDef.lookupAx K V, + lookup? := MapHookDef.lookupAx? K V, + update := MapHookDef.updateAx K V, + delete := MapHookDef.deleteAx K, + concat := MapHookDef.concatAx, + difference := MapHookDef.differenceAx, + updateMap := MapHookDef.updateMapAx, + removeAll := MapHookDef.removeAllAx K, + keys := MapHookDef.keysAx K, + in_keys := MapHookDef.in_keysAx K, + values := MapHookDef.valuesAx V, + size := MapHookDef.sizeAx, + includes := MapHookDef.includesAx, + choice := MapHookDef.choiceAx K, + nodup := MapHookDef.nodupAx K } -namespace SetHookDef /- Implementation of immutable, associative, commutative sets of `KItem`. The sets are nilpotent, i.e., the concatenation of two sets containing elements in common is `#False` (note however, this may be silently allowed during concrete execution). @@ -120,35 +118,34 @@ structure SetHookSig (T : Type) where size : set → Int choice : set → T -variable (T : Type) -axiom setCAx : Type -axiom unitAx : setCAx -axiom concatAx : setCAx → setCAx → Option setCAx -axiom elementAx : T → setCAx -axiom unionAx : setCAx → setCAx → setCAx -axiom intersectionAx : setCAx → setCAx → setCAx -axiom differenceAx : setCAx → setCAx → setCAx -axiom inSetAx : T → setCAx → Bool -axiom inclusionAx : setCAx → setCAx → Bool -axiom sizeAx : setCAx → Int -axiom choiceAx : setCAx → T +namespace SetHookDef + variable (T : Type) + axiom setCAx : Type + axiom unitAx : setCAx + axiom concatAx : setCAx → setCAx → Option setCAx + axiom elementAx : T → setCAx + axiom unionAx : setCAx → setCAx → setCAx + axiom intersectionAx : setCAx → setCAx → setCAx + axiom differenceAx : setCAx → setCAx → setCAx + axiom inSetAx : T → setCAx → Bool + axiom inclusionAx : setCAx → setCAx → Bool + axiom sizeAx : setCAx → Int + axiom choiceAx : setCAx → T +end SetHookDef noncomputable def SetHook (T : Type) : SetHookSig T := - { set := setCAx, - unit := unitAx, - concat := concatAx, - element := elementAx T, - union := unionAx, - intersection := intersectionAx, - difference := differenceAx, - inSet := inSetAx T, - inclusion := inclusionAx, - size := sizeAx, - choice := choiceAx T } + { set := SetHookDef.setCAx, + unit := SetHookDef.unitAx, + concat := SetHookDef.concatAx, + element := SetHookDef.elementAx T, + union := SetHookDef.unionAx, + intersection := SetHookDef.intersectionAx, + difference := SetHookDef.differenceAx, + inSet := SetHookDef.inSetAx T, + inclusion := SetHookDef.inclusionAx, + size := SetHookDef.sizeAx, + choice := SetHookDef.choiceAx T } -end SetHookDef - -namespace ListHookDef /- The `List` sort is an ordered collection that may contain duplicate elements. -/ @@ -177,37 +174,37 @@ structure listHookSig (T : Type) where inList : T → list → Bool size : list → Int -variable (T : Type) -axiom listCAx : Type -axiom unitAx : listCAx -axiom concatAx : listCAx → listCAx → Option listCAx -axiom elementAx : T → listCAx -axiom pushAx : T → listCAx → listCAx -axiom getAx : Int → listCAx → Option T -axiom updteAx : Int → T → listCAx → Option listCAx -axiom makeAx : Int → T → Option listCAx -axiom updateAllAx : listCAx → Int → listCAx → Option listCAx -axiom fillAx : listCAx → Int → T → Option listCAx -axiom rangeAx : listCAx → Int → Int → Option listCAx -axiom inListAx : T → listCAx → Bool -axiom sizeAx : listCAx → Int +namespace ListHookDef + variable (T : Type) + axiom listCAx : Type + axiom unitAx : listCAx + axiom concatAx : listCAx → listCAx → Option listCAx + axiom elementAx : T → listCAx + axiom pushAx : T → listCAx → listCAx + axiom getAx : Int → listCAx → Option T + axiom updteAx : Int → T → listCAx → Option listCAx + axiom makeAx : Int → T → Option listCAx + axiom updateAllAx : listCAx → Int → listCAx → Option listCAx + axiom fillAx : listCAx → Int → T → Option listCAx + axiom rangeAx : listCAx → Int → Int → Option listCAx + axiom inListAx : T → listCAx → Bool + axiom sizeAx : listCAx → Int +end ListHookDef noncomputable def ListHook (T : Type) : listHookSig T := - { list := listCAx, - unit := unitAx, - concat := concatAx, - element := elementAx T, - push := pushAx T, - get := getAx T, - updte := updteAx T, - make := makeAx T, - updateAll := updateAllAx, - fill := fillAx T, - range := rangeAx, - inList := inListAx T, - size := sizeAx } - -end ListHookDef + { list := ListHookDef.listCAx, + unit := ListHookDef.unitAx, + concat := ListHookDef.concatAx, + element := ListHookDef.elementAx T, + push := ListHookDef.pushAx T, + get := ListHookDef.getAx T, + updte := ListHookDef.updteAx T, + make := ListHookDef.makeAx T, + updateAll := ListHookDef.updateAllAx, + fill := ListHookDef.fillAx T, + range := ListHookDef.rangeAx, + inList := ListHookDef.inListAx T, + size := ListHookDef.sizeAx } class Inj (From To : Type) : Type where inj (x : From) : To diff --git a/pyk/src/pyk/kore/internal.py b/pyk/src/pyk/kore/internal.py index cfafb1e75a3..cf542573061 100644 --- a/pyk/src/pyk/kore/internal.py +++ b/pyk/src/pyk/kore/internal.py @@ -202,7 +202,7 @@ def _config_symbols(self) -> set[str]: symbols: list[str] = [] if sort in self.collections: coll = self.collections[sort] - symbols += (coll.concat, coll.element, coll.unit) + symbols += [coll.concat, coll.element, coll.unit] symbols += self.constructors.get(sort, ()) pending.extend(sort for symbol in symbols for sort in self._symbol_sorts(symbol)) @@ -231,4 +231,10 @@ def _rewrite_symbols(self) -> set[str]: for symbol in collect_symbols(function_rule.to_axiom().pattern) ) + # If the symbol consumes or produces a collection, collection function symbols are relevant + for sort in self._symbol_sorts(symbol): + if sort in self.collections: + coll = self.collections[sort] + pending.update([coll.concat, coll.element, coll.unit]) + return res diff --git a/pyk/src/tests/integration/klean/__init__.py b/pyk/src/tests/integration/klean/__init__.py new file mode 100644 index 00000000000..e69de29bb2d diff --git a/pyk/src/tests/integration/klean/test_generate.py b/pyk/src/tests/integration/klean/test_generate.py new file mode 100644 index 00000000000..b09f33ac85a --- /dev/null +++ b/pyk/src/tests/integration/klean/test_generate.py @@ -0,0 +1,48 @@ +from __future__ import annotations + +from subprocess import CalledProcessError +from typing import TYPE_CHECKING + +import pytest + +from pyk import klean +from pyk.utils import run_process_2 + +if TYPE_CHECKING: + from pathlib import Path + + from pyk.testing import Kompiler + + +@pytest.fixture +def imp_definition(kompile: Kompiler) -> Path: + from ..utils import K_FILES + + return kompile(main_file=K_FILES / 'imp.k') + + +@pytest.fixture +def skip_if_no_lake() -> None: + try: + run_process_2(['which', 'lean']) + except CalledProcessError: + pytest.skip('lean not installed') + + +def test_generate( + skip_if_no_lake: None, + imp_definition: Path, + tmp_path: Path, +) -> None: + project_dir = klean.generate( + definition_dir=imp_definition, + output_dir=tmp_path, + context={ + 'package_name': 'klean-imp', + 'library_name': 'KLeanImp', + }, + ) + + proc_res = run_process_2(['lake', 'build'], cwd=project_dir, check=False) + if proc_res.returncode: + pytest.fail(proc_res.stdout)