From 9ba9f495ee6c8e1dc14b564511369d2788f895eb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Mon, 27 May 2024 13:39:27 +0200 Subject: [PATCH 01/11] Showcase how to select smaller dataset --- smtcomp/main.py | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/smtcomp/main.py b/smtcomp/main.py index 46840ef5..0d0d98e2 100644 --- a/smtcomp/main.py +++ b/smtcomp/main.py @@ -323,7 +323,13 @@ def show_benchmarks_trivial_stats(data: Path, old_criteria: OLD_CRITERIA = False @app.command(rich_help_panel=selection_panel) -def show_sq_selection_stats(data: Path, seed: int, old_criteria: OLD_CRITERIA = False) -> None: +def show_sq_selection_stats( + data: Path, + seed: int, + old_criteria: OLD_CRITERIA = False, + min_use_benchmarks: int = defs.Config.min_used_benchmarks, + ratio_of_used_benchmarks: float = defs.Config.ratio_of_used_benchmarks, +) -> None: """ Show statistics on the benchmarks selected for single query track @@ -331,6 +337,8 @@ def show_sq_selection_stats(data: Path, seed: int, old_criteria: OLD_CRITERIA = Never compet.: old benchmarks never run competitively (more than one prover) """ + defs.Config.min_used_benchmarks = min_use_benchmarks + defs.Config.ratio_of_used_benchmarks = ratio_of_used_benchmarks datafiles = defs.DataFiles(data) benchmarks = pl.read_ipc(datafiles.cached_non_incremental_benchmarks) results = pl.read_ipc(datafiles.cached_previous_results) From d6e5d82f668f13523da3ed5725a6e628982679f4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Tue, 28 May 2024 05:46:43 +0200 Subject: [PATCH 02/11] Add an helper for the selection, and invert triviality --- smtcomp/defs.py | 15 +++++++++++++++ smtcomp/main.py | 20 ++++++++++---------- smtcomp/selection.py | 37 +++++++++++++++++++++++++------------ 3 files changed, 50 insertions(+), 22 deletions(-) diff --git a/smtcomp/defs.py b/smtcomp/defs.py index 69e0b77f..7ada296b 100644 --- a/smtcomp/defs.py +++ b/smtcomp/defs.py @@ -20,6 +20,21 @@ class Config: cpuCores = 4 min_used_benchmarks = 300 ratio_of_used_benchmarks = 0.5 + old_criteria = False + """"Do we try to emulate <= 2023 criteria that does not really follow the rules""" + invert_triviality = False + """Prioritize triviality as much as possible for testing purpose. + Look for simple problems instead of hard one""" + + def __init__(self: Config, seed: int | None) -> None: + self.__seed = seed + + def seed(self) -> int: + if self.__seed is None: + raise ValueError("The seed as not been set") + s = self.__seed + self.__seed = +1 + return s class DataFiles: diff --git a/smtcomp/main.py b/smtcomp/main.py index 0d0d98e2..8e8866d3 100644 --- a/smtcomp/main.py +++ b/smtcomp/main.py @@ -276,12 +276,12 @@ def show_benchmarks_trivial_stats(data: Path, old_criteria: OLD_CRITERIA = False Never compet.: old benchmarks never run competitively (more than one prover) """ + config = defs.Config(seed=None) + config.old_criteria = old_criteria datafiles = defs.DataFiles(data) benchmarks = pl.read_ipc(datafiles.cached_non_incremental_benchmarks) results = pl.read_ipc(datafiles.cached_previous_results) - benchmarks_with_trivial_info = smtcomp.selection.add_trivial_run_info( - benchmarks.lazy(), results.lazy(), old_criteria - ) + benchmarks_with_trivial_info = smtcomp.selection.add_trivial_run_info(benchmarks.lazy(), results.lazy(), config) b3 = ( benchmarks_with_trivial_info.group_by(["logic"]) .agg( @@ -329,6 +329,7 @@ def show_sq_selection_stats( old_criteria: OLD_CRITERIA = False, min_use_benchmarks: int = defs.Config.min_used_benchmarks, ratio_of_used_benchmarks: float = defs.Config.ratio_of_used_benchmarks, + invert_triviality: bool = False, ) -> None: """ Show statistics on the benchmarks selected for single query track @@ -337,13 +338,12 @@ def show_sq_selection_stats( Never compet.: old benchmarks never run competitively (more than one prover) """ - defs.Config.min_used_benchmarks = min_use_benchmarks - defs.Config.ratio_of_used_benchmarks = ratio_of_used_benchmarks - datafiles = defs.DataFiles(data) - benchmarks = pl.read_ipc(datafiles.cached_non_incremental_benchmarks) - results = pl.read_ipc(datafiles.cached_previous_results) - benchmarks_with_info = smtcomp.selection.add_trivial_run_info(benchmarks.lazy(), results.lazy(), old_criteria) - benchmarks_with_info = smtcomp.selection.sq_selection(benchmarks_with_info, seed) + config = defs.Config(seed=seed) + config.min_used_benchmarks = min_use_benchmarks + config.ratio_of_used_benchmarks = ratio_of_used_benchmarks + config.invert_triviality = invert_triviality + config.old_criteria = old_criteria + benchmarks_with_info = smtcomp.selection.helper_compute_sq(data, config) b3 = ( benchmarks_with_info.group_by(["logic"]) .agg( diff --git a/smtcomp/selection.py b/smtcomp/selection.py index 02a7c444..3dd1cc7e 100644 --- a/smtcomp/selection.py +++ b/smtcomp/selection.py @@ -22,8 +22,8 @@ c_file = pl.col("file") -def find_trivial(results: pl.LazyFrame, old_criteria: bool) -> pl.LazyFrame: - incoherence_scope = ["file", "year"] if old_criteria else ["file"] +def find_trivial(results: pl.LazyFrame, config: defs.Config) -> pl.LazyFrame: + incoherence_scope = ["file", "year"] if config.old_criteria else ["file"] tally = ( results # Remove incoherent results @@ -42,26 +42,24 @@ def find_trivial(results: pl.LazyFrame, old_criteria: bool) -> pl.LazyFrame: ) .group_by("file") .agg( - trivial=c_trivial.any() if old_criteria else c_trivial.all(), + trivial=c_trivial.any() if config.old_criteria else c_trivial.all(), run=True, ) ) return tally -def add_trivial_run_info( - benchmarks: pl.LazyFrame, previous_results: pl.LazyFrame, old_criteria: bool = False -) -> pl.LazyFrame: +def add_trivial_run_info(benchmarks: pl.LazyFrame, previous_results: pl.LazyFrame, config: defs.Config) -> pl.LazyFrame: - is_trivial = find_trivial(previous_results, old_criteria) + is_trivial = find_trivial(previous_results, config) return ( benchmarks.join(is_trivial, on="file", how="outer_coalesce") .fill_null(False) - .with_columns(new=pl.col("family").str.starts_with(str(defs.Config.current_year))) + .with_columns(new=pl.col("family").str.starts_with(str(config.current_year))) ) -def sq_selection(benchmarks_with_info: pl.LazyFrame, seed: int) -> pl.LazyFrame: +def sq_selection(benchmarks_with_info: pl.LazyFrame, config: defs.Config) -> pl.LazyFrame: used_logics = defs.logic_used_for_track(defs.Track.SingleQuery) # Keep only logics used by single query @@ -82,7 +80,7 @@ def sq_selection(benchmarks_with_info: pl.LazyFrame, seed: int) -> pl.LazyFrame: sample_size = pl.min_horizontal( c_all_len, pl.max_horizontal( - defs.Config.min_used_benchmarks, (c_all_len * defs.Config.ratio_of_used_benchmarks).floor().cast(pl.UInt32) + config.min_used_benchmarks, (c_all_len * config.ratio_of_used_benchmarks).floor().cast(pl.UInt32) ), ) new_sample_size = pl.min_horizontal(sample_size, c_new_len).cast(pl.UInt32) @@ -95,14 +93,14 @@ def sq_selection(benchmarks_with_info: pl.LazyFrame, seed: int) -> pl.LazyFrame: new_benchmarks_sampled = ( pl.col("new_benchmarks") .filter(new_sample_size > 0) - .list.sample(n=new_sample_size.filter(new_sample_size > 0), seed=seed) + .list.sample(n=new_sample_size.filter(new_sample_size > 0), seed=config.seed()) .list.explode() .drop_nulls() ) old_benchmarks_sampled = ( pl.col("old_benchmarks") .filter(old_sample_size > 0) - .list.sample(n=old_sample_size.filter(old_sample_size > 0), seed=seed + 1) + .list.sample(n=old_sample_size.filter(old_sample_size > 0), seed=config.seed()) .list.explode() .drop_nulls() ) @@ -115,3 +113,18 @@ def sq_selection(benchmarks_with_info: pl.LazyFrame, seed: int) -> pl.LazyFrame: return benchmarks_with_info.join(selected_benchmarks, on="file", how="outer_coalesce").with_columns( pl.col("selected").fill_null(False) ) + + +def helper_compute_sq(data: Path, config: defs.Config) -> pl.LazyFrame: + """ + Returned columns: file (uniq id), logic, family,name, status, asserts nunmber, trivial, run (in previous year), new (benchmarks), selected + """ + datafiles = defs.DataFiles(data) + benchmarks = pl.read_ipc(datafiles.cached_non_incremental_benchmarks) + results = pl.read_ipc(datafiles.cached_previous_results) + benchmarks_with_info = add_trivial_run_info(benchmarks.lazy(), results.lazy(), config) + if config.invert_triviality: + trivial_in_logic = pl.col("trivial").any().over(["logic"]) + inverted_or_not_trivial = pl.when(trivial_in_logic).then(pl.col("trivial").not_()).otherwise(pl.col("trivial")) + benchmarks_with_info = benchmarks_with_info.with_columns(trivial=inverted_or_not_trivial) + return sq_selection(benchmarks_with_info, config) From ba2cb9f017e85535ea3749d6dcbcf621c5399ae3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Tue, 28 May 2024 07:06:04 +0200 Subject: [PATCH 03/11] Summarize set of logics using "all" --- smtcomp/submission.py | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/smtcomp/submission.py b/smtcomp/submission.py index 4f0fa270..01a1dbb5 100644 --- a/smtcomp/submission.py +++ b/smtcomp/submission.py @@ -4,6 +4,7 @@ from rich.tree import Tree from smtcomp.defs import Submission +import smtcomp.defs as defs def read(file: str) -> Submission: @@ -20,9 +21,17 @@ def tree_summary(s: Submission) -> Tree: tree_track = tree_part.add(str(track)) for div, logics in sorted(divs.items()): tree_div = tree_track.add(str(div)) - slogics = map(str, logics) - for logic in sorted(slogics): - tree_div.add(logic) + not_logics = defs.tracks[track][div].difference(logics) + if len(not_logics) == 0: + tree_div.add("[italic]all[/italic]") + elif len(not_logics) <= 3 and len(not_logics) < len(logics): + slogics = map(str, not_logics) + for logic in sorted(slogics): + tree_div.add(f"[strike]{logic}[/strike]") + else: + slogics = map(str, logics) + for logic in sorted(slogics): + tree_div.add(logic) return tree From 67ac4cfa534503bb2228feecf027c70a4982cfd3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Jon=C3=A1=C5=A1?= <359542@mail.muni.cz> Date: Tue, 28 May 2024 15:20:42 +0200 Subject: [PATCH 04/11] Add machine specs. (#69) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Add machine specs. * Delete trailing whitespace. * Fix typo. --------- Co-authored-by: Martin Jonáš --- web/content/specs/index.md | 22 ++++++++++++++++++++++ web/hugo.toml | 5 +++++ 2 files changed, 27 insertions(+) create mode 100644 web/content/specs/index.md diff --git a/web/content/specs/index.md b/web/content/specs/index.md new file mode 100644 index 00000000..e8823859 --- /dev/null +++ b/web/content/specs/index.md @@ -0,0 +1,22 @@ ++++ +title = 'Machine Specifications' +date = 2024-05-28T08:08:10+02:00 +draft = false ++++ + +The single query, incremental, unsat-core, and model-validation tracks will be +run on the [VerifierCloud +cluster](https://vcloud.sosy-lab.org/cpachecker/webclient/master/info) owned by +LMU's Software and Computational Systems Lab +([SoSy-Lab](https://www.sosy-lab.org/)), who are kind enough to support our +competition with their computing power. The cluster is also used for +[Competition on Software Verification (SV-COMP)](https://sv-comp.sosy-lab.org/). + +To be more precise, the competition will be run on the 168 apollon nodes of the +cluster. Each of the nodes is equipped with `Intel Xeon E3-1230 v5 @ 3.40 GHz` +CPU and 33 GB of RAM. Each processor has 4 cores, which will be available to the +solver. + +It is also possible to locally emulate and test the computing environment on the +competition machines using the following instructions: +https://gitlab.com/sosy-lab/benchmarking/competition-scripts/#computing-environment-on-competition-machines diff --git a/web/hugo.toml b/web/hugo.toml index 8a35ca44..34e81bd1 100644 --- a/web/hugo.toml +++ b/web/hugo.toml @@ -45,6 +45,11 @@ theme = 'smtcomp' URL = '/rules.pdf' weight = 10 +[[menu.year]] + name = 'Specs' + URL = 'specs' + weight = 15 + [[menu.year]] name = 'Solver Submission' pageRef = 'solver_submission' From 56e1363a51256c960001b4e8bfd43206d6df07da Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Tue, 28 May 2024 16:16:06 +0200 Subject: [PATCH 05/11] Add seed, and more documentation --- smtcomp/defs.py | 19 +++++++++++++++++++ smtcomp/main.py | 4 ++++ 2 files changed, 23 insertions(+) diff --git a/smtcomp/defs.py b/smtcomp/defs.py index 7ada296b..e145fe71 100644 --- a/smtcomp/defs.py +++ b/smtcomp/defs.py @@ -1071,6 +1071,10 @@ def logic_used_for_track(t: Track) -> set[Logic]: class Logics(RootModel): + """ + Can be a list of logics or a regexp matched on all the existing logics + """ + root: list[Logic] @model_validator(mode="before") @@ -1095,6 +1099,14 @@ def logics_from_regexp(cls, data: str) -> list[Logic]: class Archive(BaseModel): + """ + The url must be record from http://zenodo.org for the final submission. So + the hash is not required because zenodo records are immutable. + + The hash can be used if you want to be sure of the archive used during the + test runs. + """ + url: HttpUrl h: Hash | None = None @@ -1148,6 +1160,12 @@ def uniq_id(self, name: str, archive: Archive) -> str: class Participation(BaseModel, extra="forbid"): + """ + tracks: select the participation tracks + divisions: add all the logics of those divisions in each track + logics: add all the specified logics in each selected track it exists + """ + tracks: list[Track] logics: Logics = Logics(root=[]) divisions: list[Division] = [] @@ -1202,6 +1220,7 @@ class Submission(BaseModel, extra="forbid"): system_description: HttpUrl solver_type: SolverType participations: Participations + seed: int | None = None @model_validator(mode="after") def check_archive(self) -> Submission: diff --git a/smtcomp/main.py b/smtcomp/main.py index 8e8866d3..c310fd56 100644 --- a/smtcomp/main.py +++ b/smtcomp/main.py @@ -352,6 +352,7 @@ def show_sq_selection_stats( old_never_ran=pl.col("file").filter(run=False, new=False).len(), new=pl.col("new").sum(), selected=pl.col("file").filter(selected=True).len(), + selected_already_run=pl.col("file").filter(selected=True, run=True).len(), ) .sort(by="logic") .collect() @@ -364,6 +365,7 @@ def show_sq_selection_stats( table.add_column("never compet.", justify="right", style="magenta") table.add_column("new", justify="right", style="magenta1") table.add_column("selected", justify="right", style="green3") + table.add_column("selected already run", justify="right", style="green4") used_logics = defs.logic_used_for_track(defs.Track.SingleQuery) for d in b3.to_dicts(): @@ -380,6 +382,7 @@ def show_sq_selection_stats( str(d["old_never_ran"]), str(d["new"]), str(d["selected"]), + str(d["selected_already_run"]), ) table.add_section() @@ -390,6 +393,7 @@ def show_sq_selection_stats( str(b3["old_never_ran"].sum()), str(b3["new"].sum()), str(b3["selected"].sum()), + str(b3["selected_already_run"].sum()), ) print(table) From 6dd841757f56184cc5b5f72c76dc93d7d9d8d08b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Wed, 29 May 2024 04:42:47 +0200 Subject: [PATCH 06/11] Add seed in template --- submissions/Readme.md | 2 +- submissions/template/template.json | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/submissions/Readme.md b/submissions/Readme.md index 1d117926..fc572829 100644 --- a/submissions/Readme.md +++ b/submissions/Readme.md @@ -6,7 +6,7 @@ The creation of new submission is done through the creation of a new json file in this directory and the submission of a Pull Request. It could be done directly from the web-interface and starting with a template: -[create a new submission](https://github.com/SMT-COMP/smt-comp.github.io/new/master/submissions?value=%7B%0A%20%20%20%20%22name%22%3A%20%22%3Csolver%20name%3E%22%2C%0A%20%20%20%20%22contributors%22%3A%20%5B%0A%20%20%20%20%20%20%20%20%22First%20Smith%22%2C%0A%20%20%20%20%20%20%20%20%7B%20%22name%22%3A%20%22Second%20Baker%22%2C%20%22website%22%3A%20%22http%3A%2F%2Fbaker.com%2F%22%20%7D%0A%20%20%20%20%5D%2C%0A%20%20%20%20%22contacts%22%3A%20%5B%22contact%20name%20%3Ccontact%40email.com%3E%22%5D%2C%0A%20%20%20%20%22archive%22%3A%20%7B%0A%20%20%20%20%20%20%20%20%22url%22%3A%20%22http%3A%2F%2Fexample.com%2Fsolver.tar.gz%22%2C%0A%20%20%20%20%20%20%20%20%22h%22%3A%20%7B%20%22sha256%22%3A%20%22012345%22%20%7D%0A%20%20%20%20%7D%2C%0A%20%20%20%20%22website%22%3A%20%22http%3A%2F%2Fexample.com%2F%22%2C%0A%20%20%20%20%22system_description%22%3A%20%22http%3A%2F%2Fexample.com%2Fsystem.pdf%22%2C%0A%20%20%20%20%22command%22%3A%20%5B%22relative_cmd%22%2C%20%22default_command_line%22%5D%2C%0A%20%20%20%20%22solver_type%22%3A%20%22Standalone%22%2C%0A%20%20%20%20%22participations%22%3A%20%5B%0A%20%20%20%20%20%20%20%20%7B%20%22tracks%22%3A%20%5B%22SingleQuery%22%5D%2C%20%22divisions%22%3A%20%5B%22Equality%22%5D%20%7D%2C%0A%20%20%20%20%20%20%20%20%7B%0A%20%20%20%20%20%20%20%20%20%20%20%20%22tracks%22%3A%20%5B%22SingleQuery%22%5D%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20%22logics%22%3A%20%22QF_.%2ALRA.%2A%22%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20%22command%22%3A%20%5B%22relative_cmd%22%2C%20%22other_option%22%5D%0A%20%20%20%20%20%20%20%20%7D%2C%0A%20%20%20%20%20%20%20%20%7B%0A%20%20%20%20%20%20%20%20%20%20%20%20%22tracks%22%3A%20%5B%22SingleQuery%22%5D%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20%22logics%22%3A%20%5B%22LIA%22%5D%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20%22archive%22%3A%20%7B%20%22url%22%3A%20%22http%3A%2F%2Fexample.com%2Fsolver_lia.tar.gz%22%20%7D%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20%22command%22%3A%20%5B%22relative_cmd%22%2C%20%22--super-lia%22%5D%0A%20%20%20%20%20%20%20%20%7D%0A%20%20%20%20%5D%0A%7D%0A) +[create a new submission](https://github.com/SMT-COMP/smt-comp.github.io/new/master/submissions?value=%7B%0A%20%20%20%20%22name%22%3A%20%22%3Csolver%20name%3E%22%2C%0A%20%20%20%20%22contributors%22%3A%20%5B%0A%20%20%20%20%20%20%20%20%22First%20Smith%22%2C%0A%20%20%20%20%20%20%20%20%7B%20%22name%22%3A%20%22Second%20Baker%22%2C%20%22website%22%3A%20%22http%3A%2F%2Fbaker.com%2F%22%20%7D%0A%20%20%20%20%5D%2C%0A%20%20%20%20%22contacts%22%3A%20%5B%22contact%20name%20%3Ccontact%40email.com%3E%22%5D%2C%0A%20%20%20%20%22archive%22%3A%20%7B%0A%20%20%20%20%20%20%20%20%22url%22%3A%20%22http%3A%2F%2Fexample.com%2Fsolver.tar.gz%22%2C%0A%20%20%20%20%20%20%20%20%22h%22%3A%20%7B%20%22sha256%22%3A%20%22012345%22%20%7D%0A%20%20%20%20%7D%2C%0A%20%20%20%20%22website%22%3A%20%22http%3A%2F%2Fexample.com%2F%22%2C%0A%20%20%20%20%22system_description%22%3A%20%22http%3A%2F%2Fexample.com%2Fsystem.pdf%22%2C%0A%20%20%20%20%22command%22%3A%20%5B%22relative_cmd%22%2C%20%22default_command_line%22%5D%2C%0A%20%20%20%20%22solver_type%22%3A%20%22Standalone%22%2C%0A%20%20%20%20%22seed%22%3A%20%2242%22%2C%0A%20%20%20%20%22participations%22%3A%20%5B%0A%20%20%20%20%20%20%20%20%7B%20%22tracks%22%3A%20%5B%22SingleQuery%22%5D%2C%20%22divisions%22%3A%20%5B%22Equality%22%5D%20%7D%2C%0A%20%20%20%20%20%20%20%20%7B%0A%20%20%20%20%20%20%20%20%20%20%20%20%22tracks%22%3A%20%5B%22SingleQuery%22%5D%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20%22logics%22%3A%20%22QF_.%2ALRA.%2A%22%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20%22command%22%3A%20%5B%22relative_cmd%22%2C%20%22other_option%22%5D%0A%20%20%20%20%20%20%20%20%7D%2C%0A%20%20%20%20%20%20%20%20%7B%0A%20%20%20%20%20%20%20%20%20%20%20%20%22tracks%22%3A%20%5B%22SingleQuery%22%5D%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20%22logics%22%3A%20%5B%22LIA%22%5D%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20%22archive%22%3A%20%7B%20%22url%22%3A%20%22http%3A%2F%2Fexample.com%2Fsolver_lia.tar.gz%22%20%7D%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20%22command%22%3A%20%5B%22relative_cmd%22%2C%20%22--super-lia%22%5D%0A%20%20%20%20%20%20%20%20%7D%0A%20%20%20%20%5D%0A%7D%0A) - The filename should start with the name of your solver and end with `.json` - The continuous integration will check the format diff --git a/submissions/template/template.json b/submissions/template/template.json index 3a123c96..14045240 100644 --- a/submissions/template/template.json +++ b/submissions/template/template.json @@ -13,6 +13,7 @@ "system_description": "http://example.com/system.pdf", "command": ["relative_cmd", "default_command_line"], "solver_type": "Standalone", + "seed": "42", "participations": [ { "tracks": ["SingleQuery"], "divisions": ["Equality"] }, { From c7e577965e4f417655e39c755481eba4b3cff7f3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Wed, 29 May 2024 04:43:53 +0200 Subject: [PATCH 07/11] Add aws_dockerfile for the page generation --- smtcomp/defs.py | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/smtcomp/defs.py b/smtcomp/defs.py index e145fe71..9fcf750f 100644 --- a/smtcomp/defs.py +++ b/smtcomp/defs.py @@ -1164,6 +1164,10 @@ class Participation(BaseModel, extra="forbid"): tracks: select the participation tracks divisions: add all the logics of those divisions in each track logics: add all the specified logics in each selected track it exists + + aws_dockerfile should be used only in conjunction with Cloud and Parallel track + + archive and command should not be used with Cloud and Parallel track. They superseed the one given at the root. """ tracks: list[Track] @@ -1171,8 +1175,18 @@ class Participation(BaseModel, extra="forbid"): divisions: list[Division] = [] archive: Archive | None = None command: Command | None = None + aws_dockerfile: str | None = None experimental: bool = False + @model_validator(mode="after") + def check_archive(self) -> Participation: + aws_track = {Track.Cloud, Track.Parallel} + if self.aws_dockerfile is not None and not set(self.tracks).issubset(aws_track): + raise ValueError("aws_dockerfile can be used only with Cloud and Parallel track") + if (self.archive is not None or self.command is not None) and not set(self.tracks).isdisjoint(aws_track): + raise ValueError("archive and command field can't be used with Cloud and Parallel track") + return self + def get(self, d: None | dict[Track, dict[Division, set[Logic]]] = None) -> dict[Track, dict[Division, set[Logic]]]: if d is None: d = {} From 7e1862f069650ab6cc1a172040c8875453656e2c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Mon, 27 May 2024 07:27:42 +0200 Subject: [PATCH 08/11] [CI] Download, unpack solver and generate a dumb test script --- .github/workflows/test-solver.yml | 58 +++++++++++++++++++++++ smtcomp/defs.py | 37 +++++++++++++-- smtcomp/generate_benchmarks.py | 23 ++++++++- smtcomp/main.py | 79 +++++++++++++++++++++++++++---- smtcomp/test_solver.py | 19 ++++++++ 5 files changed, 200 insertions(+), 16 deletions(-) create mode 100644 .github/workflows/test-solver.yml create mode 100644 smtcomp/test_solver.py diff --git a/.github/workflows/test-solver.yml b/.github/workflows/test-solver.yml new file mode 100644 index 00000000..25d696fe --- /dev/null +++ b/.github/workflows/test-solver.yml @@ -0,0 +1,58 @@ +name: TestSolver + +on: + pull_request: + paths: + - submissions/*.json + +jobs: + generate-test-script: + runs-on: ubuntu-latest + steps: + - name: Check out + uses: actions/checkout@v3 + + - uses: actions/cache@v3 + with: + path: ~/.cache/pre-commit + key: pre-commit-${{ hashFiles('.pre-commit-config.yaml') }} + + - name: Set up the environment + uses: ./.github/actions/setup-poetry-env + + - name: Compute changed files + id: changed-files + uses: tj-actions/changed-files@v41 + with: + files: | + submissions/*.json + + - name: Generate script + run: | + poetry run smtcomp generate-test-script test_data/ ${{ steps.changed-files.outputs.all_changed_files }} + rm -rf test_data/download + + - name: Archive directory + run: tar -cf test_data.tar test_data + + - name: Upload generated test script + uses: actions/upload-artifact@v4 + with: + name: generated_script + path: test_data.tar + + run-test-script: + needs: generate-test-script + runs-on: ubuntu-latest + container: registry.gitlab.com/sosy-lab/benchmarking/competition-scripts/user:latest + steps: + - name: Download generated test script + uses: actions/download-artifact@v4 + with: + name: generated_script + + - name: Unarchive + run: tar -xf test_data.tar + + - name: Run test script + run: python3 test_data/test_script.py diff --git a/smtcomp/defs.py b/smtcomp/defs.py index 9fcf750f..80abf247 100644 --- a/smtcomp/defs.py +++ b/smtcomp/defs.py @@ -5,7 +5,7 @@ import re from enum import Enum from pathlib import Path, PurePath -from typing import Any, Dict, Optional +from typing import Any, Dict, cast, Optional from pydantic import BaseModel, Field, RootModel, model_validator, ConfigDict from pydantic.networks import HttpUrl, validate_email @@ -1159,6 +1159,15 @@ def uniq_id(self, name: str, archive: Archive) -> str: return h.hexdigest() +class ParticipationCompleted(BaseModel, extra="forbid"): + """Participation using the default value in the submission root""" + + tracks: dict[Track, dict[Division, set[Logic]]] + archive: Archive + command: Command + experimental: bool + + class Participation(BaseModel, extra="forbid"): """ tracks: select the participation tracks @@ -1202,17 +1211,31 @@ def get(self, d: None | dict[Track, dict[Division, set[Logic]]] = None) -> dict[ logics.add(logic) return d + def complete(self, archive: Archive | None, command: Command | None) -> ParticipationCompleted: + archive = cast(Archive, archive if self.archive is None else self.archive) + command = cast(Command, command if self.command is None else self.command) + return ParticipationCompleted( + tracks=self.get(), archive=archive, command=command, experimental=self.experimental + ) + + +import itertools + class Participations(RootModel): root: list[Participation] - def get_divisions(self, track: Track) -> list[Division]: + def get_divisions(self, l: list[Track] = list(Track)) -> set[Division]: """ " Return the divisions in which the solver participates""" - return [] # TODO + tracks = self.get() + divs = [set(tracks[track].keys()) for track in l] + return functools.reduce(lambda x, y: x | y, divs) - def get_logics(self, track: Track) -> list[Logic]: + def get_logics(self, l: list[Track] = list(Track)) -> set[Logic]: """ " Return the logics in which the solver participates""" - return [] # TODO + tracks = self.get() + logics = itertools.chain.from_iterable([iter(tracks[track].values()) for track in l]) + return functools.reduce(lambda x, y: x | y, logics) def get(self, d: None | dict[Track, dict[Division, set[Logic]]] = None) -> dict[Track, dict[Division, set[Logic]]]: if d is None: @@ -1247,6 +1270,10 @@ def check_archive(self) -> Submission: def uniq_id(self) -> str: return hashlib.sha256(self.name.encode()).hexdigest() + def complete_participations(self) -> list[ParticipationCompleted]: + """Push defaults from the submission into participations""" + return [p.complete(self.archive, self.command) for p in self.participations.root] + class Smt2File(BaseModel): incremental: bool diff --git a/smtcomp/generate_benchmarks.py b/smtcomp/generate_benchmarks.py index e4ac673a..af819401 100644 --- a/smtcomp/generate_benchmarks.py +++ b/smtcomp/generate_benchmarks.py @@ -3,6 +3,25 @@ from smtcomp import defs +def path_trivial_benchmark(dst: Path, track: defs.Track, logic: defs.Logic, status: defs.Status) -> Path: + match track: + case defs.Track.Incremental: + suffix = "_inc" + case defs.Track.ModelValidation: + suffix = "_model" + case defs.Track.SingleQuery: + suffix = "" + case defs.Track.UnsatCore | defs.Track.ProofExhibition | defs.Track.Cloud | defs.Track.Parallel: + raise (ValueError("No trivial benchmarks yet for f{track}")) + match status: + case defs.Status.Sat: + return dst.joinpath("files", str(logic) + suffix + ".sat.smt2") + case defs.Status.Unsat: + return dst.joinpath("files", str(logic) + suffix + ".unsat.smt2") + case defs.Status.Unknown: + raise (ValueError("No trivial benchmarks yet for unknown")) + + def generate_trivial_benchmarks(dst: Path) -> None: dst.joinpath("files").mkdir(parents=True, exist_ok=True) for track, divisions in defs.tracks.items(): @@ -18,8 +37,8 @@ def generate_trivial_benchmarks(dst: Path) -> None: for _, theories in divisions.items(): for theory in theories: file = dst.joinpath(str(theory) + suffix) - file_sat = dst.joinpath("files", str(theory) + suffix + ".sat.smt2") - file_unsat = dst.joinpath("files", str(theory) + suffix + ".unsat.smt2") + file_sat = path_trivial_benchmark(dst, track, theory, defs.Status.Sat) + file_unsat = path_trivial_benchmark(dst, track, theory, defs.Status.Unsat) file.write_text("\n".join([str(file_sat.relative_to(dst)), str(file_unsat.relative_to(dst))])) diff --git a/smtcomp/main.py b/smtcomp/main.py index c310fd56..9156d918 100644 --- a/smtcomp/main.py +++ b/smtcomp/main.py @@ -1,7 +1,7 @@ import json import itertools from pathlib import Path -from typing import List, Optional, cast, Dict, Any, Annotated +from typing import List, Optional, cast, Dict, Any, Annotated, TextIO import rich from rich.progress import track import rich.style @@ -27,6 +27,8 @@ from smtcomp.unpack import write_cin, read_cin import smtcomp.scramble_benchmarks from rich.console import Console +import smtcomp.test_solver as test_solver + app = typer.Typer() @@ -142,21 +144,29 @@ def generate_benchexec( ) +# Should be moved somewhere else +def download_archive_aux(s: defs.Submission, dst: Path) -> None: + """ + Download and unpack + """ + dst.mkdir(parents=True, exist_ok=True) + if s.archive: + archive.download(s.archive, dst) + archive.unpack(s.archive, dst) + for p in s.participations.root: + if p.archive: + archive.download(p.archive, dst) + archive.unpack(p.archive, dst) + + @app.command(rich_help_panel=benchexec_panel) def download_archive(files: List[Path], dst: Path) -> None: """ Download and unpack """ for file in track(files): - dst.mkdir(parents=True, exist_ok=True) s = submission.read(str(file)) - if s.archive: - archive.download(s.archive, dst) - archive.unpack(s.archive, dst) - for p in s.participations.root: - if p.archive: - archive.download(p.archive, dst) - archive.unpack(p.archive, dst) + download_archive_aux(s, dst) @app.command() @@ -501,3 +511,54 @@ def scramble_benchmarks( """ smtcomp.scramble_benchmarks.scramble(competition_track, src, dstdir, scrambler, seed, max_workers) + + +@app.command() +def generate_test_script(outdir: Path, submissions: list[Path] = typer.Argument(None)) -> None: + def read_submission(file: Path) -> defs.Submission: + try: + return submission.read(str(file)) + except Exception as e: + rich.print(f"[red]Error during file parsing of {file}[/red]") + print(e) + exit(1) + + outdir.mkdir(parents=True, exist_ok=True) + test_solver.copy_me(outdir) + + trivial_bench = outdir.joinpath("trivial_bench") + smtcomp.generate_benchmarks.generate_trivial_benchmarks(trivial_bench) + + l = list(map(read_submission, submissions)) + script_output = outdir.joinpath("test_script.py") + with script_output.open("w") as out: + out.write("from test_solver import *\n") + out.write("init_test()\n") + out.write("\n") + out.write("""print("Testing provers")\n""") + for sub in l: + out.write(f"print({sub.name!r})\n") + download_archive_aux(sub, outdir) + for part in sub.complete_participations(): + for track, divisions in part.tracks.items(): + match track: + case defs.Track.Incremental: + statuses = [defs.Status.Sat, defs.Status.Unsat] + case defs.Track.ModelValidation: + statuses = [defs.Status.Sat] + case defs.Track.SingleQuery: + statuses = [defs.Status.Sat, defs.Status.Unsat] + case defs.Track.UnsatCore | defs.Track.ProofExhibition | defs.Track.Cloud | defs.Track.Parallel: + continue + for _, logics in divisions.items(): + for logic in logics: + for status in statuses: + file_sat = smtcomp.generate_benchmarks.path_trivial_benchmark( + trivial_bench, track, logic, status + ).relative_to(outdir) + cmd = ( + archive.archive_unpack_dir(part.archive, outdir) + .joinpath(part.command.binary) + .relative_to(outdir) + ) + out.write(f"test({str(cmd)!r},{part.command.arguments!r},{str(file_sat)!r})\n") diff --git a/smtcomp/test_solver.py b/smtcomp/test_solver.py new file mode 100644 index 00000000..61357549 --- /dev/null +++ b/smtcomp/test_solver.py @@ -0,0 +1,19 @@ +# This module is for the test script in the docker image +# It must use only module from the standard library +from pathlib import Path +import shutil +import subprocess, os + + +def copy_me(dstdir: Path) -> None: + shutil.copyfile(src=__file__, dst=dstdir.joinpath("test_solver.py"), follow_symlinks=True) + + +def init_test() -> None: + os.chdir(os.path.dirname(__file__)) + + +def test(cmd: str, args: list[str], file: str) -> None: + all = [cmd] + args + [file] + print(all, flush=True) + subprocess.run(all) From 2f600c3da79f477a115d22a2c8132ade49c8a679 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Wed, 29 May 2024 16:53:10 +0200 Subject: [PATCH 09/11] [CI] Parse prover output --- smtcomp/main.py | 9 ++++++- smtcomp/test_solver.py | 56 ++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 62 insertions(+), 3 deletions(-) diff --git a/smtcomp/main.py b/smtcomp/main.py index 9156d918..b834c788 100644 --- a/smtcomp/main.py +++ b/smtcomp/main.py @@ -561,4 +561,11 @@ def read_submission(file: Path) -> defs.Submission: .joinpath(part.command.binary) .relative_to(outdir) ) - out.write(f"test({str(cmd)!r},{part.command.arguments!r},{str(file_sat)!r})\n") + if status == defs.Status.Sat: + expected = "sat" + else: + expected = "unsat" + out.write( + f"test({str(cmd)!r},{part.command.arguments!r},{str(file_sat)!r},{expected!r})\n" + ) + out.write("end()\n") diff --git a/smtcomp/test_solver.py b/smtcomp/test_solver.py index 61357549..f5225133 100644 --- a/smtcomp/test_solver.py +++ b/smtcomp/test_solver.py @@ -3,17 +3,69 @@ from pathlib import Path import shutil import subprocess, os +import re def copy_me(dstdir: Path) -> None: shutil.copyfile(src=__file__, dst=dstdir.joinpath("test_solver.py"), follow_symlinks=True) +# copied from tools.py should be factorized +def parse_result(returnsignal: int | None, returncode: int, output: list[str]) -> str: + if returnsignal is None: + status = None + for line in output: + line = line.strip() + # ignore + if re.compile("^\s*(success|;.*)?\s*$").match(line): + continue + if line == "unsat": + return "unsat" + elif line == "sat": + return "sat" + else: + return "unknown" + return "unknown" + + elif (returnsignal == 9) or (returnsignal == 15): + status = "timeout" + + elif returnsignal == 9: + status = "KILLED BY SIGNAL 9" + elif returnsignal == 6: + status = "ABORTED" + elif returnsignal == 15: + status = "KILLED" + else: + status = f"ERROR ({returncode})" + + return status + + def init_test() -> None: os.chdir(os.path.dirname(__file__)) -def test(cmd: str, args: list[str], file: str) -> None: +exit_code = 0 + + +# Try to simulate runexec from benchexec +def test(cmd: str, args: list[str], file: str, expected: str) -> None: + global exit_code all = [cmd] + args + [file] print(all, flush=True) - subprocess.run(all) + result = subprocess.run(all, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + if result.returncode < 0: + returnsignal = -result.returncode + else: + returnsignal = None + answer = parse_result(returnsignal, result.returncode, result.stdout.decode().splitlines()) + if answer != expected: + print(f"\x1b[1;31mError expected {expected} result obtained {answer}\x1b[0m", flush=True) + exit_code = 1 + else: + print("\x1b[1;32mOK\x1b[0m", flush=True) + + +def end() -> None: + exit(exit_code) From 578ae189f9b0760236334ff2d8cb3ac67ea1d429 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Wed, 29 May 2024 17:14:36 +0200 Subject: [PATCH 10/11] Generate files for website during deployement - Allow to remove schema.html from repo - Will simplify all the file generations --- .github/workflows/deploy-website.yaml | 11 +++++++++ .gitignore | 2 +- web/content/solver_submission/schema.html | 27 ----------------------- 3 files changed, 12 insertions(+), 28 deletions(-) delete mode 100644 web/content/solver_submission/schema.html diff --git a/.github/workflows/deploy-website.yaml b/.github/workflows/deploy-website.yaml index 3e37b838..9e3ccf25 100644 --- a/.github/workflows/deploy-website.yaml +++ b/.github/workflows/deploy-website.yaml @@ -44,6 +44,17 @@ jobs: with: submodules: recursive fetch-depth: 0 + #For smtcomp script + - uses: actions/cache@v3 + with: + path: ~/.cache/pre-commit + key: pre-commit-${{ hashFiles('.pre-commit-config.yaml') }} + - name: Set up the environment + uses: ./.github/actions/setup-poetry-env + # Generate files using smtcomp tool + - name: Files generation + run: make submission-doc + ### - name: Setup Pages id: pages uses: actions/configure-pages@v4 diff --git a/.gitignore b/.gitignore index 40b64104..e23048c8 100644 --- a/.gitignore +++ b/.gitignore @@ -166,7 +166,7 @@ cython_debug/ # option (not recommended) you can uncomment the following to ignore the entire idea folder. #.idea/ -/web/content/solver_submission/schema.json +/web/content/solver_submission/schema.* schema_doc.css schema_doc.min.js *.feather diff --git a/web/content/solver_submission/schema.html b/web/content/solver_submission/schema.html deleted file mode 100644 index c594d8b8..00000000 --- a/web/content/solver_submission/schema.html +++ /dev/null @@ -1,27 +0,0 @@ - Submission

Submission

Type: object
No Additional Properties

root name

Name

Type: string

root contributors

Contributors

Type: array

Must contain a minimum of 1 items

No Additional Items

Each item of this array must be:

root contributors Contributor
Type: object

Contributors in the developement of the solver. If only name is provided,
it can be directly given.

 No Additional Properties
Examples:

"Jane Smith"
-
{
-    "name": "Jane Smith",
-    "website": "http://jane.smith.name"
-}
-

root contributors Contributor name

Name

Type: string

root contributors Contributor website

Website

Default: null

root contributors Contributor website anyOf item 0
Type: stringFormat: uri

Must be at least 1 characters long

Must be at most 2083 characters long

root contributors Contributor website anyOf item 1
Type: null

root contacts

Contacts

Type: array

Must contain a minimum of 1 items

No Additional Items

Each item of this array must be:

root contacts NameEmail
Type: object

Name and valide email "name <email>"
Example:

"Jane Smith <jane.smith@edu.world>"
-

root contacts NameEmail name

Name

Type: string

root contacts NameEmail email

Email

Type: string

root archive
Default: null

root archive anyOf Archive
Type: object

root archive anyOf Archive url

Url

Type: stringFormat: uri

Must be at least 1 characters long

Must be at most 2083 characters long

root archive anyOf Archive h
Default: null

root archive anyOf Archive h anyOf Hash
Type: object
No Additional Properties

root archive anyOf Archive h anyOf item 1
Type: null
root archive anyOf item 1
Type: null

root command
Default: null

Fields command given in participations have priority over this one

root command anyOf Command
Type: object

Command with its arguments to run after the extraction of the archive.

The path are relative to the directory in which the archive is unpacked.

The input file is added at the end of the list of arguments.

Two forms are accepted, using a dictionnary (separate binary and arguments) or a list ([binary]+arguments).

The command run in the given environment
https://gitlab.com/sosy-lab/benchmarking/competition-scripts/#computing-environment-on-competition-machines

No Additional Properties
Examples:

[
-    "relative_cmd",
-    "default_command_line"
-]
-
{
-    "arguments": [
-        "default_command_line"
-    ],
-    "binary": "relative_cmd"
-}
-

root command anyOf Command binary

Binary

Type: string

root command anyOf Command arguments

Arguments

Type: array of string Default: []
No Additional Items

Each item of this array must be:

root command anyOf Command arguments arguments items
Type: string

root command anyOf Command compa_starexec

Compa Starexec

Type: boolean Default: false

Used only for internal tests
root command anyOf item 1
Type: null

root website

Website

Type: stringFormat: uri

Must be at least 1 characters long

Must be at most 2083 characters long

root system_description

System Description

Type: stringFormat: uri

Must be at least 1 characters long

Must be at most 2083 characters long

root solver_type
Type: enum (of string)

Must be one of:

  • "wrapped"
  • "derived"
  • "Standalone"

root participations
Type: array
No Additional Items

Each item of this array must be:

root participations Participation
Type: object
No Additional Properties

root participations Participation tracks

Tracks

Type: array
No Additional Items

Each item of this array must be:

root participations Participation tracks Track
Type: enum (of string)

Must be one of:

  • "UnsatCore"
  • "SingleQuery"
  • "ProofExhibition"
  • "ModelValidation"
  • "Incremental"
  • "Cloud"
  • "Parallel"

root participations Participation logics
Type: array Default: []
No Additional Items

Each item of this array must be:

root participations Participation logics Logic
Type: enum (of string)

Must be one of:

  • "ABV"
  • "ABVFP"
  • "ABVFPLRA"
  • "ALIA"
  • "ANIA"
  • "AUFBV"
  • "AUFBVDTLIA"
  • "AUFBVDTNIA"
  • "AUFBVDTNIRA"
  • "AUFBVFP"
  • "AUFDTLIA"
  • "AUFDTLIRA"
  • "AUFDTNIRA"
  • "AUFFPDTNIRA"
  • "AUFLIA"
  • "AUFLIRA"
  • "AUFNIA"
  • "AUFNIRA"
  • "BV"
  • "BVFP"
  • "BVFPLRA"
  • "FP"
  • "FPLRA"
  • "LIA"
  • "LRA"
  • "NIA"
  • "NRA"
  • "QF_ABV"
  • "QF_ABVFP"
  • "QF_ABVFPLRA"
  • "QF_ALIA"
  • "QF_ANIA"
  • "QF_AUFBV"
  • "QF_AUFBVFP"
  • "QF_AUFBVLIA"
  • "QF_AUFBVNIA"
  • "QF_AUFLIA"
  • "QF_AUFNIA"
  • "QF_AX"
  • "QF_BV"
  • "QF_BVFP"
  • "QF_BVFPLRA"
  • "QF_BVLRA"
  • "QF_DT"
  • "QF_FP"
  • "QF_FPLRA"
  • "QF_IDL"
  • "QF_LIA"
  • "QF_LIRA"
  • "QF_LRA"
  • "QF_NIA"
  • "QF_NIRA"
  • "QF_NRA"
  • "QF_RDL"
  • "QF_S"
  • "QF_SLIA"
  • "QF_SNIA"
  • "QF_UF"
  • "QF_UFBV"
  • "QF_UFBVDT"
  • "QF_UFBVLIA"
  • "QF_UFDT"
  • "QF_UFDTLIA"
  • "QF_UFDTLIRA"
  • "QF_UFDTNIA"
  • "QF_UFFP"
  • "QF_UFFPDTNIRA"
  • "QF_UFIDL"
  • "QF_UFLIA"
  • "QF_UFLRA"
  • "QF_UFNIA"
  • "QF_UFNRA"
  • "UF"
  • "UFBV"
  • "UFBVDT"
  • "UFBVFP"
  • "UFBVLIA"
  • "UFDT"
  • "UFDTLIA"
  • "UFDTLIRA"
  • "UFDTNIA"
  • "UFDTNIRA"
  • "UFFPDTNIRA"
  • "UFIDL"
  • "UFLIA"
  • "UFLRA"
  • "UFNIA"
  • "UFNIRA"
  • "UFNRA"

root participations Participation divisions

Divisions

Type: array Default: []
No Additional Items

Each item of this array must be:

root participations Participation divisions Division
Type: enum (of string)

Must be one of:

  • "Arith"
  • "Bitvec"
  • "Equality"
  • "Equality+LinearArith"
  • "Equality+MachineArith"
  • "Equality+NonLinearArith"
  • "FPArith"
  • "QF_ADT+BitVec"
  • "QF_ADT+LinArith"
  • "QF_Bitvec"
  • "QF_Datatypes"
  • "QF_Equality"
  • "QF_Equality+Bitvec"
  • "QF_Equality+Bitvec+Arith"
  • "QF_Equality+LinearArith"
  • "QF_Equality+NonLinearArith"
  • "QF_FPArith"
  • "QF_LinearIntArith"
  • "QF_LinearRealArith"
  • "QF_NonLinearIntArith"
  • "QF_NonLinearRealArith"
  • "QF_Strings"

root participations Participation command
Default: null

root participations Participation command anyOf Command
Type: object

Command with its arguments to run after the extraction of the archive.

The path are relative to the directory in which the archive is unpacked.

The input file is added at the end of the list of arguments.

Two forms are accepted, using a dictionnary (separate binary and arguments) or a list ([binary]+arguments).

The command run in the given environment
https://gitlab.com/sosy-lab/benchmarking/competition-scripts/#computing-environment-on-competition-machines

No Additional Properties
Examples:

[
-    "relative_cmd",
-    "default_command_line"
-]
-
{
-    "arguments": [
-        "default_command_line"
-    ],
-    "binary": "relative_cmd"
-}
-

root participations Participation command anyOf Command arguments

Arguments

Type: array of string Default: []
No Additional Items

Each item of this array must be:

root participations Participation command anyOf Command arguments arguments items
Type: string

root participations Participation command anyOf Command compa_starexec

Compa Starexec

Type: boolean Default: false

Used only for internal tests
root participations Participation command anyOf item 1
Type: null

root participations Participation experimental

Experimental

Type: boolean Default: false
\ No newline at end of file From 300b8a57f5ad5b9f500320baaa4815c062859aa2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Wed, 29 May 2024 17:23:08 +0200 Subject: [PATCH 11/11] [CI] Install json-schema-for-human --- .github/workflows/deploy-website.yaml | 4 +++- Makefile | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/.github/workflows/deploy-website.yaml b/.github/workflows/deploy-website.yaml index 9e3ccf25..4d4e5f73 100644 --- a/.github/workflows/deploy-website.yaml +++ b/.github/workflows/deploy-website.yaml @@ -53,7 +53,9 @@ jobs: uses: ./.github/actions/setup-poetry-env # Generate files using smtcomp tool - name: Files generation - run: make submission-doc + run: | + pip install json-schema-for-humans + poetry run make submission-doc ### - name: Setup Pages id: pages diff --git a/Makefile b/Makefile index ad46a5aa..0dce426f 100644 --- a/Makefile +++ b/Makefile @@ -48,7 +48,7 @@ submission-doc: @poetry run smtcomp dump-json-schema $(GENERATED_SCHEMA_FILE) @echo "🚀 Generating html doc to $(GENERATED_SCHEMA_HTML)" @echo " Needs 'pip install json-schema-for-humans'" - generate-schema-doc --expand-buttons --no-link-to-reused-ref $(GENERATED_SCHEMA_FILE) $(GENERATED_SCHEMA_HTML) + @poetry run generate-schema-doc --expand-buttons --no-link-to-reused-ref $(GENERATED_SCHEMA_FILE) $(GENERATED_SCHEMA_HTML) hugo-server: (cd web; hugo server)