From 3a111e02493bcee634eeb2a18441356d21ffecb7 Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Thu, 28 Mar 2024 10:46:47 -0700 Subject: [PATCH 1/6] chore: add config for PyPI runtime publishing --- .../DafnyRuntimePython/.gitignore | 30 +++++++++++++++++++ .../DafnyRuntime/DafnyRuntimePython/Makefile | 20 ++++++++++++- .../DafnyRuntimePython/pyproject.toml | 21 +++++++++++++ .../{System_.py => src/System_/__init__.py} | 0 .../{_dafny.py => src/_dafny/__init__.py} | 0 5 files changed, 70 insertions(+), 1 deletion(-) create mode 100644 Source/DafnyRuntime/DafnyRuntimePython/.gitignore create mode 100644 Source/DafnyRuntime/DafnyRuntimePython/pyproject.toml rename Source/DafnyRuntime/DafnyRuntimePython/{System_.py => src/System_/__init__.py} (100%) rename Source/DafnyRuntime/DafnyRuntimePython/{_dafny.py => src/_dafny/__init__.py} (100%) diff --git a/Source/DafnyRuntime/DafnyRuntimePython/.gitignore b/Source/DafnyRuntime/DafnyRuntimePython/.gitignore new file mode 100644 index 00000000000..219db0e8069 --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimePython/.gitignore @@ -0,0 +1,30 @@ +### from https://github.com/github/gitignore/blob/main/Python.gitignore + +# Byte-compiled / optimized / DLL files +__pycache__/ +*.py[cod] +*$py.class + +# Distribution / packaging +.Python +build/ +develop-eggs/ +dist/ +downloads/ +eggs/ +.eggs/ +lib/ +lib64/ +parts/ +sdist/ +var/ +wheels/ +share/python-wheels/ +*.egg-info/ +.installed.cfg +*.egg +MANIFEST + +# Environments +.env +venv/ diff --git a/Source/DafnyRuntime/DafnyRuntimePython/Makefile b/Source/DafnyRuntime/DafnyRuntimePython/Makefile index a84b57ef0b9..6f3cf0555c1 100644 --- a/Source/DafnyRuntime/DafnyRuntimePython/Makefile +++ b/Source/DafnyRuntime/DafnyRuntimePython/Makefile @@ -3,7 +3,9 @@ DAFNY = dotnet run --project ../../Dafny --no-build -- GENERATED_SYSTEM_MODULE_SOURCE=../obj/systemModulePopulator-py/System_.py -GENERATED_SYSTEM_MODULE_TARGET=System_.py +GENERATED_SYSTEM_MODULE_TARGET=src/System_/__init__.py + +VIRTUALENV = venv all: check-system-module @@ -15,3 +17,19 @@ check-system-module: build-system-module update-system-module: build-system-module cp $(GENERATED_SYSTEM_MODULE_SOURCE) $(GENERATED_SYSTEM_MODULE_TARGET) + +setup-venv: + python -m venv --clear $(VIRTUALENV) + $(VIRTUALENV)/bin/pip install --upgrade build twine + +clean-package: + rm -rf dist/ + +build-package: + $(VIRTUALENV)/bin/python -m build + +upload-package-testpypi: + $(VIRTUALENV)/bin/python -m twine upload --repository testpypi dist/* + +upload-package-pypi: + $(VIRTUALENV)/bin/python -m twine upload dist/* diff --git a/Source/DafnyRuntime/DafnyRuntimePython/pyproject.toml b/Source/DafnyRuntime/DafnyRuntimePython/pyproject.toml new file mode 100644 index 00000000000..c5969e8a31b --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimePython/pyproject.toml @@ -0,0 +1,21 @@ +[build-system] +requires = ["setuptools>=61.0"] +build-backend = "setuptools.build_meta" + +[project] +name = "DafnyRuntimePython" +version = "4.7.0" +authors = [ + { name = "The Dafny core team", email = "core-team@dafny.org" }, +] +description = "Dafny runtime for Python" +requires-python = ">=3.8" +classifiers = [ + "Programming Language :: Python :: 3", + "License :: OSI Approved :: MIT License", + "Operating System :: OS Independent", +] + +[project.urls] +Homepage = "https://github.com/dafny-lang/dafny" +Issues = "https://github.com/dafny-lang/dafny/issues" diff --git a/Source/DafnyRuntime/DafnyRuntimePython/System_.py b/Source/DafnyRuntime/DafnyRuntimePython/src/System_/__init__.py similarity index 100% rename from Source/DafnyRuntime/DafnyRuntimePython/System_.py rename to Source/DafnyRuntime/DafnyRuntimePython/src/System_/__init__.py diff --git a/Source/DafnyRuntime/DafnyRuntimePython/_dafny.py b/Source/DafnyRuntime/DafnyRuntimePython/src/_dafny/__init__.py similarity index 100% rename from Source/DafnyRuntime/DafnyRuntimePython/_dafny.py rename to Source/DafnyRuntime/DafnyRuntimePython/src/_dafny/__init__.py From 15903a9dbc10b6708ae491f1b9cac15eb158c54c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 10 Oct 2024 16:19:38 +0200 Subject: [PATCH 2/6] Attempted fix --- Source/DafnyRuntime/DafnyRuntimePython/Makefile | 2 +- .../DafnyRuntimePython/{src => }/System_/__init__.py | 0 .../DafnyRuntimePython/{src => }/_dafny/__init__.py | 0 3 files changed, 1 insertion(+), 1 deletion(-) rename Source/DafnyRuntime/DafnyRuntimePython/{src => }/System_/__init__.py (100%) rename Source/DafnyRuntime/DafnyRuntimePython/{src => }/_dafny/__init__.py (100%) diff --git a/Source/DafnyRuntime/DafnyRuntimePython/Makefile b/Source/DafnyRuntime/DafnyRuntimePython/Makefile index 6f3cf0555c1..caa9863277e 100644 --- a/Source/DafnyRuntime/DafnyRuntimePython/Makefile +++ b/Source/DafnyRuntime/DafnyRuntimePython/Makefile @@ -3,7 +3,7 @@ DAFNY = dotnet run --project ../../Dafny --no-build -- GENERATED_SYSTEM_MODULE_SOURCE=../obj/systemModulePopulator-py/System_.py -GENERATED_SYSTEM_MODULE_TARGET=src/System_/__init__.py +GENERATED_SYSTEM_MODULE_TARGET=System_/__init__.py VIRTUALENV = venv diff --git a/Source/DafnyRuntime/DafnyRuntimePython/src/System_/__init__.py b/Source/DafnyRuntime/DafnyRuntimePython/System_/__init__.py similarity index 100% rename from Source/DafnyRuntime/DafnyRuntimePython/src/System_/__init__.py rename to Source/DafnyRuntime/DafnyRuntimePython/System_/__init__.py diff --git a/Source/DafnyRuntime/DafnyRuntimePython/src/_dafny/__init__.py b/Source/DafnyRuntime/DafnyRuntimePython/_dafny/__init__.py similarity index 100% rename from Source/DafnyRuntime/DafnyRuntimePython/src/_dafny/__init__.py rename to Source/DafnyRuntime/DafnyRuntimePython/_dafny/__init__.py From 693e602b45234a7d7b545da3dc92ddc0b3c232be Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 10 Oct 2024 17:37:48 +0200 Subject: [PATCH 3/6] Fix expect files --- .../LitTest/comp/compile1verbose/CompileAndThenRun.dfy.expect | 4 ++-- .../LitTests/LitTest/comp/compile3/JustRun.dfy.expect | 4 ++-- .../LitTest/comp/manualcompile/ManualCompile.dfy.expect | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1verbose/CompileAndThenRun.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1verbose/CompileAndThenRun.dfy.expect index e6db659bdd6..9d23f677a5f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1verbose/CompileAndThenRun.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1verbose/CompileAndThenRun.dfy.expect @@ -100,7 +100,7 @@ hello, Dafny Dafny program verifier finished with 0 verified, 0 errors Wrote textual form of target program to CompileAndThenRun-py/__main__.py Additional output written to CompileAndThenRun-py/CompileAndThenRun-py.dtr -Additional output written to CompileAndThenRun-py/System_.py -Additional output written to CompileAndThenRun-py/_dafny.py +Additional output written to CompileAndThenRun-py/System_/__init__.py +Additional output written to CompileAndThenRun-py/_dafny/__init__.py Additional output written to CompileAndThenRun-py/module_.py hello, Dafny diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile3/JustRun.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile3/JustRun.dfy.expect index 9a175e6acda..e78785a18c3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile3/JustRun.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile3/JustRun.dfy.expect @@ -108,8 +108,8 @@ hello, Dafny Dafny program verifier finished with 0 verified, 0 errors Wrote textual form of target program to JustRun-py/__main__.py Additional output written to JustRun-py/JustRun-py.dtr -Additional output written to JustRun-py/System_.py -Additional output written to JustRun-py/_dafny.py +Additional output written to JustRun-py/System_/__init__.py +Additional output written to JustRun-py/_dafny/__init__.py Additional output written to JustRun-py/module_.py Running... diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy.expect index 4c7fa20c8bb..8edb238e481 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy.expect @@ -100,7 +100,7 @@ hello, Dafny Dafny program verifier finished with 0 verified, 0 errors Wrote textual form of target program to ManualCompile-py/__main__.py Additional output written to ManualCompile-py/ManualCompile-py.dtr -Additional output written to ManualCompile-py/System_.py -Additional output written to ManualCompile-py/_dafny.py +Additional output written to ManualCompile-py/System_/__init__.py +Additional output written to ManualCompile-py/_dafny/__init__.py Additional output written to ManualCompile-py/module_.py hello, Dafny From a38d657980dfc4aa1bff73d84fbe8b07787e8dfe Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Mon, 14 Oct 2024 14:31:05 -0700 Subject: [PATCH 4/6] ensure _dafny gets packaged, fix version number When using the "flat layout", setuptools' auto-discovery only considers a single top-level module. See . --- .../DafnyRuntime/DafnyRuntimePython/pyproject.toml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimePython/pyproject.toml b/Source/DafnyRuntime/DafnyRuntimePython/pyproject.toml index c5969e8a31b..c18e2ce8a0c 100644 --- a/Source/DafnyRuntime/DafnyRuntimePython/pyproject.toml +++ b/Source/DafnyRuntime/DafnyRuntimePython/pyproject.toml @@ -1,10 +1,6 @@ -[build-system] -requires = ["setuptools>=61.0"] -build-backend = "setuptools.build_meta" - [project] name = "DafnyRuntimePython" -version = "4.7.0" +version = "4.8.1" authors = [ { name = "The Dafny core team", email = "core-team@dafny.org" }, ] @@ -19,3 +15,10 @@ classifiers = [ [project.urls] Homepage = "https://github.com/dafny-lang/dafny" Issues = "https://github.com/dafny-lang/dafny/issues" + +[build-system] +requires = ["setuptools>=61.0"] +build-backend = "setuptools.build_meta" + +[tool.setuptools] +packages = ["_dafny", "System_"] From 50bb52ea265253b2fd9442c46076a018fd8a1efa Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Mon, 14 Oct 2024 15:03:00 -0700 Subject: [PATCH 5/6] add BUILDING.md --- .../DafnyRuntimePython/BUILDING.md | 62 +++++++++++++++++++ .../DafnyRuntime/DafnyRuntimePython/Makefile | 2 +- 2 files changed, 63 insertions(+), 1 deletion(-) create mode 100644 Source/DafnyRuntime/DafnyRuntimePython/BUILDING.md diff --git a/Source/DafnyRuntime/DafnyRuntimePython/BUILDING.md b/Source/DafnyRuntime/DafnyRuntimePython/BUILDING.md new file mode 100644 index 00000000000..4213a37604a --- /dev/null +++ b/Source/DafnyRuntime/DafnyRuntimePython/BUILDING.md @@ -0,0 +1,62 @@ +# Building the DafnyRuntimePython + +## Prerequisites + +- the `dotnet` CLI, to build Dafny +- Python, to build and upload the package +- [TestPyPI credentials](https://packaging.python.org/en/latest/guides/using-testpypi/), if you will upload to TestPyPI +- PyPI credentials, if you will upload to PyPI + +## Steps + +1. Ensure that the `System_` module is up-to-date: + +```bash +# Ensure that the Dafny build is up-to-date, +# as it will be used to compile the System_ module. +$ dotnet build --project ../../Dafny + +# Compile the System_ runtime module. +$ make update-system-module +``` + +2. Build the distribution package: + +```bash +# Set up the build tooling +$ make setup-venv + +# Remove old build artifacts +$ make clean-package + +# Build the distribution package +$ make build-package +``` + +3. Check that the distribution package looks right locally and on TestPyPI, + as (production) PyPI does not allow overwriting uploaded packages: + +```bash +# List the distribution package's files, and check that: +# 1. the version number is correct +# 2. the `System_/__init__.py` file exists +# 3. the `dafny/__init__.py` file exists +$ tar tf dist/dafnyruntimepython-X.Y.Z.tar.gz + +# Upload to TestPyPI, and check that it appears correct at +# . +$ make upload-package-testpypi +``` + +4. Upload to PyPI: + +```bash +$ make upload-package-pypi +``` + +You can view the uploaded package at . + +## More info + +The packaging process is described in + diff --git a/Source/DafnyRuntime/DafnyRuntimePython/Makefile b/Source/DafnyRuntime/DafnyRuntimePython/Makefile index caa9863277e..fbb75ec8bdb 100644 --- a/Source/DafnyRuntime/DafnyRuntimePython/Makefile +++ b/Source/DafnyRuntime/DafnyRuntimePython/Makefile @@ -23,7 +23,7 @@ setup-venv: $(VIRTUALENV)/bin/pip install --upgrade build twine clean-package: - rm -rf dist/ + rm -rf dist/ *.egg-info/ build-package: $(VIRTUALENV)/bin/python -m build From bf58adb3a97d6aa34cdda132791f21eb3601bce2 Mon Sep 17 00:00:00 2001 From: Alex Chew Date: Mon, 14 Oct 2024 22:01:34 -0700 Subject: [PATCH 6/6] rerun CI