From 9ef259eace7d524c172c0893aba77fa76fefee6b Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Tue, 31 Oct 2023 13:17:20 +0100 Subject: [PATCH] test copy of https://github.com/runtimeverification/evm-semantics/pull/2094/ --- Makefile | 2 +- kevm-pyk/poetry.lock | 67 ++++++++++++- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- kevm-pyk/src/kevm_pyk/__main__.py | 160 ++++++++++++++++++++++++------ package/version | 2 +- 6 files changed, 199 insertions(+), 36 deletions(-) diff --git a/Makefile b/Makefile index a4798dc7a7..31a95d43f8 100644 --- a/Makefile +++ b/Makefile @@ -5,7 +5,7 @@ all: poetry # -------- PYTHON_BIN := python3.10 -KEVM_PYK_DIR := ./kevm-pyk +KEVM_PYK_DIR := $(abspath ./kevm-pyk) POETRY := poetry -C $(KEVM_PYK_DIR) POETRY_RUN := $(POETRY) run -- diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index adf2eb4d7b..18b982422f 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -1,9 +1,10 @@ -# This file is automatically @generated by Poetry 1.6.1 and should not be changed by hand. +# This file is automatically @generated by Poetry and should not be changed by hand. [[package]] name = "attrs" version = "23.1.0" description = "Classes Without Boilerplate" +category = "main" optional = false python-versions = ">=3.7" files = [ @@ -22,6 +23,7 @@ tests-no-zope = ["cloudpickle", "hypothesis", "mypy (>=1.1.1)", "pympler", "pyte name = "autoflake" version = "2.2.1" description = "Removes unused imports and unused variables" +category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -37,6 +39,7 @@ tomli = {version = ">=2.0.1", markers = "python_version < \"3.11\""} name = "black" version = "23.10.1" description = "The uncompromising code formatter." +category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -79,6 +82,7 @@ uvloop = ["uvloop (>=0.15.2)"] name = "classify-imports" version = "4.2.0" description = "Utilities for refactoring imports in python-like syntax." +category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -90,6 +94,7 @@ files = [ name = "click" version = "8.1.7" description = "Composable command line interface toolkit" +category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -104,6 +109,7 @@ colorama = {version = "*", markers = "platform_system == \"Windows\""} name = "cmd2" version = "2.4.3" description = "cmd2 - quickly build feature-rich and user-friendly interactive command line applications in Python" +category = "main" optional = false python-versions = ">=3.6" files = [ @@ -126,6 +132,7 @@ validate = ["flake8", "mypy", "types-pkg-resources"] name = "colorama" version = "0.4.6" description = "Cross-platform colored terminal text." +category = "dev" optional = false python-versions = "!=3.0.*,!=3.1.*,!=3.2.*,!=3.3.*,!=3.4.*,!=3.5.*,!=3.6.*,>=2.7" files = [ @@ -137,6 +144,7 @@ files = [ name = "coloredlogs" version = "15.0.1" description = "Colored terminal output for Python's logging module" +category = "main" optional = false python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*" files = [ @@ -154,6 +162,7 @@ cron = ["capturer (>=2.4)"] name = "coverage" version = "7.3.2" description = "Code coverage measurement for Python" +category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -221,6 +230,7 @@ toml = ["tomli"] name = "dill" version = "0.3.7" description = "serialize all of Python" +category = "main" optional = false python-versions = ">=3.7" files = [ @@ -235,6 +245,7 @@ graph = ["objgraph (>=1.7.2)"] name = "exceptiongroup" version = "1.1.3" description = "Backport of PEP 654 (exception groups)" +category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -249,6 +260,7 @@ test = ["pytest (>=6)"] name = "execnet" version = "2.0.2" description = "execnet: rapid multi-Python deployment" +category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -263,6 +275,7 @@ testing = ["hatch", "pre-commit", "pytest", "tox"] name = "filelock" version = "3.13.0" description = "A platform independent file lock." +category = "main" optional = false python-versions = ">=3.8" files = [ @@ -279,6 +292,7 @@ typing = ["typing-extensions (>=4.8)"] name = "flake8" version = "6.1.0" description = "the modular source code checker: pep8 pyflakes and co" +category = "dev" optional = false python-versions = ">=3.8.1" files = [ @@ -295,6 +309,7 @@ pyflakes = ">=3.1.0,<3.2.0" name = "flake8-bugbear" version = "23.9.16" description = "A plugin for flake8 finding likely bugs and design problems in your program. Contains warnings that don't belong in pyflakes and pycodestyle." +category = "dev" optional = false python-versions = ">=3.8.1" files = [ @@ -313,6 +328,7 @@ dev = ["coverage", "hypothesis", "hypothesmith (>=0.2)", "pre-commit", "pytest", name = "flake8-comprehensions" version = "3.14.0" description = "A flake8 plugin to help you write better list/set/dict comprehensions." +category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -327,6 +343,7 @@ flake8 = ">=3.0,<3.2.0 || >3.2.0" name = "flake8-quotes" version = "3.3.2" description = "Flake8 lint for quotes." +category = "dev" optional = false python-versions = "*" files = [ @@ -340,6 +357,7 @@ flake8 = "*" name = "flake8-type-checking" version = "2.5.1" description = "A flake8 plugin for managing type-checking imports & forward references" +category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -355,6 +373,7 @@ flake8 = "*" name = "graphviz" version = "0.20.1" description = "Simple Python interface for Graphviz" +category = "main" optional = false python-versions = ">=3.7" files = [ @@ -371,6 +390,7 @@ test = ["coverage", "mock (>=4)", "pytest (>=7)", "pytest-cov", "pytest-mock (>= name = "humanfriendly" version = "10.0" description = "Human friendly output for text interfaces using Python" +category = "main" optional = false python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*" files = [ @@ -385,6 +405,7 @@ pyreadline3 = {version = "*", markers = "sys_platform == \"win32\" and python_ve name = "importlib-metadata" version = "6.8.0" description = "Read metadata from Python packages" +category = "main" optional = false python-versions = ">=3.8" files = [ @@ -404,6 +425,7 @@ testing = ["flufl.flake8", "importlib-resources (>=1.3)", "packaging", "pyfakefs name = "iniconfig" version = "2.0.0" description = "brain-dead simple config-ini parsing" +category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -415,6 +437,7 @@ files = [ name = "inotify" version = "0.2.10" description = "An adapter to Linux kernel support for inotify directory-watching." +category = "dev" optional = false python-versions = "*" files = [ @@ -429,6 +452,7 @@ nose = "*" name = "isort" version = "5.12.0" description = "A Python utility / library to sort Python imports." +category = "dev" optional = false python-versions = ">=3.8.0" files = [ @@ -446,6 +470,7 @@ requirements-deprecated-finder = ["pip-api", "pipreqs"] name = "linkify-it-py" version = "2.0.2" description = "Links recognition library with FULL unicode support." +category = "main" optional = false python-versions = ">=3.7" files = [ @@ -466,6 +491,7 @@ test = ["coverage", "pytest", "pytest-cov"] name = "markdown-it-py" version = "2.2.0" description = "Python port of markdown-it. Markdown parsing, done right!" +category = "main" optional = false python-versions = ">=3.7" files = [ @@ -492,6 +518,7 @@ testing = ["coverage", "pytest", "pytest-cov", "pytest-regressions"] name = "mccabe" version = "0.7.0" description = "McCabe checker, plugin for flake8" +category = "dev" optional = false python-versions = ">=3.6" files = [ @@ -503,6 +530,7 @@ files = [ name = "mdit-py-plugins" version = "0.4.0" description = "Collection of plugins for markdown-it-py" +category = "main" optional = false python-versions = ">=3.8" files = [ @@ -522,6 +550,7 @@ testing = ["coverage", "pytest", "pytest-cov", "pytest-regressions"] name = "mdurl" version = "0.1.2" description = "Markdown URL utilities" +category = "main" optional = false python-versions = ">=3.7" files = [ @@ -533,6 +562,7 @@ files = [ name = "multiprocess" version = "0.70.15" description = "better multiprocessing and multithreading in Python" +category = "main" optional = false python-versions = ">=3.7" files = [ @@ -561,6 +591,7 @@ dill = ">=0.3.7" name = "mypy" version = "1.6.1" description = "Optional static typing for Python" +category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -607,6 +638,7 @@ reports = ["lxml"] name = "mypy-extensions" version = "1.0.0" description = "Type system extensions for programs checked with the mypy type checker." +category = "dev" optional = false python-versions = ">=3.5" files = [ @@ -618,6 +650,7 @@ files = [ name = "nose" version = "1.3.7" description = "nose extends unittest to make testing easier" +category = "dev" optional = false python-versions = "*" files = [ @@ -630,6 +663,7 @@ files = [ name = "packaging" version = "23.2" description = "Core utilities for Python packages" +category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -641,6 +675,7 @@ files = [ name = "pathos" version = "0.3.1" description = "parallel graph management and execution in heterogeneous computing" +category = "main" optional = false python-versions = ">=3.7" files = [ @@ -658,6 +693,7 @@ ppft = ">=1.7.6.7" name = "pathspec" version = "0.11.2" description = "Utility library for gitignore style pattern matching of file paths." +category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -669,6 +705,7 @@ files = [ name = "pep8-naming" version = "0.13.3" description = "Check PEP-8 naming conventions, plugin for flake8" +category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -683,6 +720,7 @@ flake8 = ">=5.0.0" name = "platformdirs" version = "3.11.0" description = "A small Python package for determining appropriate platform-specific dirs, e.g. a \"user data dir\"." +category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -698,6 +736,7 @@ test = ["appdirs (==1.4.4)", "covdefaults (>=2.3)", "pytest (>=7.4)", "pytest-co name = "pluggy" version = "1.3.0" description = "plugin and hook calling mechanisms for python" +category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -713,6 +752,7 @@ testing = ["pytest", "pytest-benchmark"] name = "pox" version = "0.3.3" description = "utilities for filesystem exploration and automated builds" +category = "main" optional = false python-versions = ">=3.7" files = [ @@ -724,6 +764,7 @@ files = [ name = "ppft" version = "1.7.6.7" description = "distributed and parallel Python" +category = "main" optional = false python-versions = ">=3.7" files = [ @@ -738,6 +779,7 @@ dill = ["dill (>=0.3.7)"] name = "psutil" version = "5.9.5" description = "Cross-platform lib for process and system monitoring in Python." +category = "main" optional = false python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*" files = [ @@ -764,6 +806,7 @@ test = ["enum34", "ipaddress", "mock", "pywin32", "wmi"] name = "pybind11" version = "2.11.1" description = "Seamless operability between C++11 and Python" +category = "main" optional = false python-versions = ">=3.6" files = [ @@ -778,6 +821,7 @@ global = ["pybind11-global (==2.11.1)"] name = "pycodestyle" version = "2.11.1" description = "Python style guide checker" +category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -789,6 +833,7 @@ files = [ name = "pyflakes" version = "3.1.0" description = "passive checker of Python programs" +category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -800,6 +845,7 @@ files = [ name = "pygments" version = "2.16.1" description = "Pygments is a syntax highlighting package written in Python." +category = "main" optional = false python-versions = ">=3.7" files = [ @@ -814,6 +860,7 @@ plugins = ["importlib-metadata"] name = "pyk" version = "0.1.486" description = "" +category = "main" optional = false python-versions = "^3.10" files = [] @@ -839,6 +886,7 @@ resolved_reference = "23a97935da94cded4392bc028cdf16bd6f7edd5b" name = "pyperclip" version = "1.8.2" description = "A cross-platform clipboard module for Python. (Only handles plain text for now.)" +category = "main" optional = false python-versions = "*" files = [ @@ -849,6 +897,7 @@ files = [ name = "pyreadline3" version = "3.4.1" description = "A python implementation of GNU readline." +category = "main" optional = false python-versions = "*" files = [ @@ -860,6 +909,7 @@ files = [ name = "pytest" version = "7.4.3" description = "pytest: simple powerful testing with Python" +category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -882,6 +932,7 @@ testing = ["argcomplete", "attrs (>=19.2.0)", "hypothesis (>=3.56)", "mock", "no name = "pytest-cov" version = "4.1.0" description = "Pytest plugin for measuring coverage." +category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -900,6 +951,7 @@ testing = ["fields", "hunter", "process-tests", "pytest-xdist", "six", "virtuale name = "pytest-mock" version = "3.12.0" description = "Thin-wrapper around the mock package for easier use with pytest" +category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -917,6 +969,7 @@ dev = ["pre-commit", "pytest-asyncio", "tox"] name = "pytest-timeout" version = "2.2.0" description = "pytest plugin to abort hanging tests" +category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -931,6 +984,7 @@ pytest = ">=5.0.0" name = "pytest-xdist" version = "3.3.1" description = "pytest xdist plugin for distributed testing, most importantly across multiple CPUs" +category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -951,6 +1005,7 @@ testing = ["filelock"] name = "pyupgrade" version = "3.15.0" description = "A tool to automatically upgrade syntax for newer versions." +category = "dev" optional = false python-versions = ">=3.8.1" files = [ @@ -965,6 +1020,7 @@ tokenize-rt = ">=5.2.0" name = "rich" version = "13.6.0" description = "Render rich text, tables, progress bars, syntax highlighting, markdown and more to the terminal" +category = "main" optional = false python-versions = ">=3.7.0" files = [ @@ -983,6 +1039,7 @@ jupyter = ["ipywidgets (>=7.5.1,<9)"] name = "textual" version = "0.27.0" description = "Modern Text User Interface framework" +category = "main" optional = false python-versions = ">=3.7,<4.0" files = [ @@ -1003,6 +1060,7 @@ dev = ["aiohttp (>=3.8.1)", "click (>=8.1.2)", "msgpack (>=1.0.3)"] name = "tokenize-rt" version = "5.2.0" description = "A wrapper around the stdlib `tokenize` which roundtrips." +category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -1014,6 +1072,7 @@ files = [ name = "tomli" version = "2.0.1" description = "A lil' TOML parser" +category = "main" optional = false python-versions = ">=3.7" files = [ @@ -1025,6 +1084,7 @@ files = [ name = "tomlkit" version = "0.11.8" description = "Style preserving TOML library" +category = "main" optional = false python-versions = ">=3.7" files = [ @@ -1036,6 +1096,7 @@ files = [ name = "typing-extensions" version = "4.8.0" description = "Backported and Experimental Type Hints for Python 3.8+" +category = "main" optional = false python-versions = ">=3.8" files = [ @@ -1047,6 +1108,7 @@ files = [ name = "uc-micro-py" version = "1.0.2" description = "Micro subset of unicode data files for linkify-it-py projects." +category = "main" optional = false python-versions = ">=3.7" files = [ @@ -1061,6 +1123,7 @@ test = ["coverage", "pytest", "pytest-cov"] name = "wcwidth" version = "0.2.8" description = "Measures the displayed width of unicode strings in a terminal" +category = "main" optional = false python-versions = "*" files = [ @@ -1072,6 +1135,7 @@ files = [ name = "xdg-base-dirs" version = "6.0.1" description = "Variables defined by the XDG Base Directory Specification" +category = "main" optional = false python-versions = ">=3.10,<4.0" files = [ @@ -1083,6 +1147,7 @@ files = [ name = "zipp" version = "3.17.0" description = "Backport of pathlib-compatible object wrapper for zip files" +category = "main" optional = false python-versions = ">=3.8" files = [ diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 3188c4b38d..58bb5b9401 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.332" +version = "1.0.333" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index d0cab81dab..c22ed709f8 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.332' +VERSION: Final = '1.0.333' diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index a874f750b0..ecdc88edec 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -1,11 +1,12 @@ from __future__ import annotations -import contextlib -import graphlib +import abc +import dataclasses import json import logging import os import sys +import tempfile import time from argparse import ArgumentParser from dataclasses import dataclass @@ -13,7 +14,7 @@ from pathlib import Path from typing import TYPE_CHECKING -from pathos.pools import ProcessPool # type: ignore +import multiprocess # type: ignore from pyk.cli.utils import file_path from pyk.cterm import CTerm from pyk.kast.outer import KApply, KRewrite, KSort, KToken @@ -44,7 +45,7 @@ if TYPE_CHECKING: from argparse import Namespace - from collections.abc import Callable, Iterable, Iterator + from collections.abc import Callable, Iterable, Mapping from typing import Any, Final, TypeVar from pyk.kast.outer import KClaim @@ -188,18 +189,40 @@ def exec_prove_legacy( raise SystemExit(1) -class ZeroProcessPool: - def map(self, f: Callable[[Any], Any], xs: list[Any]) -> list[Any]: - return [f(x) for x in xs] +class TodoQueueTask(abc.ABC): + ... -@contextlib.contextmanager -def wrap_process_pool(workers: int) -> Iterator[ZeroProcessPool | ProcessPool]: - if workers <= 1: - yield ZeroProcessPool() - else: - with ProcessPool(ncpus=workers) as pp: - yield pp +@dataclasses.dataclass +class TodoQueueProofTask(TodoQueueTask): + proof_id: str + + +@dataclasses.dataclass +class TodoQueueStop(TodoQueueTask): + ... + + +class DoneQueueTask(abc.ABC): + ... + + +@dataclasses.dataclass +class DoneQueueTaskFinished(DoneQueueTask): + claim_label: str + passed: bool + failure_log: list[str] | None + + +class MyEnvironment: + number_of_workers: int + # to_do_queue: multiprocessing.Queue # only instances of TodoQueueTask go there + # done_queue: multiprocessing.Queue # only instances of DoneQueueTask go there + + def __init__(self, number_of_workers: int): + self.number_of_workers = number_of_workers + self.to_do_queue = multiprocess.Queue() + self.done_queue = multiprocess.Queue() class JSONEncoder(json.JSONEncoder): @@ -305,6 +328,9 @@ def exec_prove( if smt_retry_limit is None: smt_retry_limit = 10 + if save_directory is None: + save_directory = Path(tempfile.TemporaryDirectory().name) + kevm = KEVM(definition_dir, use_directory=save_directory, bug_report=bug_report) include_dirs = [Path(include) for include in includes] @@ -324,9 +350,12 @@ def is_functional(claim: KClaim) -> bool: llvm_definition_dir = definition_dir / 'llvm-library' if use_booster else None _LOGGER.info(f'Extracting claims from file: {spec_file}') + + spec_module_name = spec_module if spec_module is not None else os.path.splitext(spec_file.name)[0].upper() + all_claims = kevm.get_claims( spec_file, - spec_module_name=spec_module, + spec_module_name=spec_module_name, include_dirs=include_dirs, md_selector=md_selector, claim_labels=claim_labels, @@ -334,9 +363,10 @@ def is_functional(claim: KClaim) -> bool: ) if all_claims is None: raise ValueError(f'No claims found in file: {spec_file}') + spec_module_name = spec_module if spec_module is not None else os.path.splitext(spec_file.name)[0].upper() all_claim_jobs = init_claim_jobs(spec_module_name, all_claims) - all_claim_jobs_by_label = {c.claim.label: c for c in all_claim_jobs} + all_claim_jobs_by_label: Mapping[str, KClaimJob] = {c.claim.label: c for c in all_claim_jobs} claims_graph = claim_dependency_dict(all_claims, spec_module_name=spec_module_name) def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]: @@ -435,23 +465,91 @@ def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]: return passed, failure_log - topological_sorter = graphlib.TopologicalSorter(claims_graph) - topological_sorter.prepare() - with wrap_process_pool(workers=workers) as process_pool: - selected_results: list[tuple[bool, list[str] | None]] = [] - selected_claims = [] - while topological_sorter.is_active(): - ready = topological_sorter.get_ready() - _LOGGER.info(f'Discharging proof obligations: {ready}') - curr_claim_list = [all_claim_jobs_by_label[label] for label in ready] - results: list[tuple[bool, list[str] | None]] = process_pool.map(_init_and_run_proof, curr_claim_list) - for label in ready: - topological_sorter.done(label) - selected_results.extend(results) - selected_claims.extend(curr_claim_list) + def worker(env: MyEnvironment) -> None: + while True: + msg = env.to_do_queue.get() + match msg: + case TodoQueueStop(): + return + case TodoQueueProofTask(claim_label): + try: + passed, failure_log = _init_and_run_proof(all_claim_jobs_by_label[claim_label]) + env.done_queue.put( + DoneQueueTaskFinished(claim_label=claim_label, passed=passed, failure_log=failure_log) + ) + except Exception as e: + env.done_queue.put( + DoneQueueTaskFinished(claim_label=claim_label, passed=False, failure_log=[str(e)]) + ) + + def coordinator(env: MyEnvironment, jobs_to_do: list[KClaimJob]) -> list[tuple[bool, list[str] | None]]: + id_to_job: dict[str, KClaimJob] = {job.claim.label: job for job in jobs_to_do} + remaining_job_labels: set[str] = {job.claim.label for job in jobs_to_do} + finished_job_labels: dict[str, tuple[bool, list[str] | None]] = {} + + def get_a_ready_id() -> str | None: + for job_label in remaining_job_labels: + if set({d.claim.label for d in id_to_job[job_label].dependencies}).issubset(finished_job_labels.keys()): + remaining_job_labels.remove(job_label) + return job_label + return None + + def put_all_ready_into_queue() -> int: + n = 0 + while True: + opt_proof_id: str | None = get_a_ready_id() + if opt_proof_id is None: + return n + env.to_do_queue.put(TodoQueueProofTask(opt_proof_id)) + n = n + 1 + + def process_incoming_message(msg: DoneQueueTask) -> bool: + match msg: + case DoneQueueTaskFinished(claim_label=claim_label, passed=passed, failure_log=failure_log): + finished_job_labels[claim_label] = (passed, failure_log) + return True + return False + + def take_all_proven_from_queue() -> int: + n = 0 + while not env.done_queue.empty(): + msg = env.done_queue.get() + if process_incoming_message(msg): + n = n + 1 + return n + + enqueued_counter: int = 0 + while True: + newly_removed_from_queue = take_all_proven_from_queue() + newly_enqueued = put_all_ready_into_queue() + enqueued_counter = enqueued_counter + newly_enqueued - newly_removed_from_queue + assert enqueued_counter >= 0 + if enqueued_counter == 0: + break + assert enqueued_counter > 0 + # We can wait for some incoming message. + # Unfortunately, a `wait_until_nonempty` primitive is missing, so we have to block using `get`. + msg = env.done_queue.get() + if process_incoming_message(msg): + enqueued_counter = enqueued_counter - 1 + # And now we are going to process all the other incoming messages (if any) + continue + # Now we want to stop all the workers + for _ in range(env.number_of_workers): + env.to_do_queue.put(TodoQueueStop()) + return [finished_job_labels[job.claim.label] for job in jobs_to_do] + + env = MyEnvironment(number_of_workers=workers) + worker_processes = [multiprocess.Process(target=worker, args=(env,)) for _ in range(workers)] + for w in worker_processes: + w.start() + all_claim_jobs_list = list(all_claim_jobs) + results = coordinator(env, all_claim_jobs_list) + for w in worker_processes: + w.join() failed = 0 - for job, r in zip(selected_claims, selected_results, strict=True): + for job, r in zip(all_claim_jobs_list, results, strict=True): passed, failure_log = r if passed: print(f'PROOF PASSED: {job.claim.label}') diff --git a/package/version b/package/version index 51dda02714..50b74d4d07 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.332 +1.0.333