chore: add config for PyPI runtime publishing

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/

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
+# <https://test.pypi.org/project/DafnyRuntimePython/>.
+$ make upload-package-testpypi
+```
+
+4. Upload to PyPI:
+
+```bash
+$ make upload-package-pypi
+```
+
+You can view the uploaded package at <https://pypi.org/project/DafnyRuntimePython/>.
+
+## More info
+
+The packaging process is described in
+<https://packaging.python.org/en/latest/tutorials/packaging-projects/>

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=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/ *.egg-info/
+
+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/*

Source/DafnyRuntime/DafnyRuntimePython/pyproject.toml

@@ -0,0 +1,24 @@
+[project]
+name = "DafnyRuntimePython"
+version = "4.8.1"
+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"
+
+[build-system]
+requires = ["setuptools>=61.0"]
+build-backend = "setuptools.build_meta"
+
+[tool.setuptools]
+packages = ["_dafny", "System_"]

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

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...
 

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