From 89f380660a96942efcd4cabcbee0728e5d3f8044 Mon Sep 17 00:00:00 2001 From: Yasunari Watanabe Date: Sun, 20 Jun 2021 23:23:41 +0900 Subject: [PATCH] Reordering --- README.md | 11 ++++++++++- .../suslik/synthesis/CertificationBenchmarks.scala | 2 +- ssl-htt | 2 +- 3 files changed, 12 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 16a36a3b0..ef76dab34 100644 --- a/README.md +++ b/README.md @@ -159,6 +159,11 @@ for all three target frameworks. (Section "Artifact Structure" below shows the location of these files.) Then, for the standard benchmarks, it will also compile the generated certificates. +These are the default evaluation configuration, and the exact actions that will +be performed under this configuration are written to timestamped `.log` files in +the `certify` directory before each run. This configuration can be modified +by setting the `--configure` flag. See section "Customizing Benchmark Options" +for details. As this script produces verbose output, you may consider teeing the script's output to a log file for viewing/debugging later, instead of running the script @@ -404,7 +409,7 @@ This will load an Emacs session in your terminal window. Some useful commands: - `C-c C-u` to move backward in the current buffer's Coq proof - `C-x C-c` (type "yes" if prompted) to exit Emacs. -### Customizing the Benchmark Options +### Customizing Benchmark Options You may wish to run the benchmarks with alternative settings. @@ -442,6 +447,10 @@ the desired option (`y` or `n`). The default settings are: - _For advanced benchmarks_: Synthesize programs in all benchmark groups. Then generate (but _don't_ compile) certificates for HTT only. +Each execution of the script generates a timestamped `.log` file listing +exactly what actions will be performed given the user-specified configuration, +which may be useful for debugging. + ### Downloading and Compiling Sources All four projects have been compiled/installed ahead of time and are ready to diff --git a/src/main/scala/org/tygus/suslik/synthesis/CertificationBenchmarks.scala b/src/main/scala/org/tygus/suslik/synthesis/CertificationBenchmarks.scala index f490d4df7..59309761f 100644 --- a/src/main/scala/org/tygus/suslik/synthesis/CertificationBenchmarks.scala +++ b/src/main/scala/org/tygus/suslik/synthesis/CertificationBenchmarks.scala @@ -266,8 +266,8 @@ object CertificationBenchmarks { "certification-benchmarks/tree" ) val allAdvanced = List( - "certification-benchmarks-advanced/bst", "certification-benchmarks-advanced/dll", + "certification-benchmarks-advanced/bst", "certification-benchmarks-advanced/srtl", ) val defaultStandardConfig: BenchmarkConfig = BenchmarkConfig(allTargets, allStandard, allStandard, compile = true, "standard") diff --git a/ssl-htt b/ssl-htt index 9a83a522b..9cd3ad2ee 160000 --- a/ssl-htt +++ b/ssl-htt @@ -1 +1 @@ -Subproject commit 9a83a522b49df38c57ca6987a7608df6f4f13d9c +Subproject commit 9cd3ad2eecff82ebcd87c6902191da0c0cb7101b