h0nzZik · h0nzZik · Jun 29, 2024 · Jun 29, 2024 · Jun 29, 2024 · Jun 29, 2024
diff --git a/.github/workflows/build-and-profile.yml b/.github/workflows/build-and-profile.yml
@@ -39,14 +39,17 @@ jobs:
     - name: 'Build Minuska'
       run: nix build -L '.#minuska' --out-link ./result-minuska
 
-    - name: 'Build Coq examples'
-      run: nix build -L '.#examples-coq'
+    - name: 'Run standalone benchmarks'
+      run: nix develop -L '.#bench-standalone' --command ./bench-standalone/test.sh
 
-    - name: 'Run standalone examples'
-      run: nix develop -L '.#examples-standalone' --command ./examples-standalone/test.sh
+    - name: 'Run hybrid benchmarks'
+      run: nix develop -L '.#bench-hybrid' --command ./bench-hybrid/test.sh
 
-    - name: 'Run hybrid examples'
-      run: nix develop -L '.#examples-hybrid' --command ./examples-hybrid/test.sh
+    - name: 'Run Coq benchmarks'
+      run: nix develop -L '.#bench-coq' --command ./bench-coq/build-and-profile.sh
+
+    - name: 'Build old Coq examples'
+      run: nix build -L '.#old-examples-coq'
 
     - name: 'Build Docker image'
       run: nix build -L '.#minuska-docker' --out-link ./result-minuska-docker

diff --git a/examples-coq/Makefile → bench-coq/Makefile b/examples-coq/Makefile → bench-coq/Makefile
diff --git a/minuska-bench/_CoqProject → bench-coq/_CoqProject b/minuska-bench/_CoqProject → bench-coq/_CoqProject
diff --git a/minuska-bench/build-and-profile.sh → bench-coq/build-and-profile.sh b/minuska-bench/build-and-profile.sh → bench-coq/build-and-profile.sh
diff --git a/minuska-bench/generate-v-files.py → bench-coq/generate-v-files.py b/minuska-bench/generate-v-files.py → bench-coq/generate-v-files.py
diff --git a/minuska-bench/parse-log-groups.py → bench-coq/parse-log-groups.py b/minuska-bench/parse-log-groups.py → bench-coq/parse-log-groups.py
diff --git a/minuska-bench/parse-timing-log.sh → bench-coq/parse-timing-log.sh b/minuska-bench/parse-timing-log.sh → bench-coq/parse-timing-log.sh
diff --git a/minuska-bench/stats-to-tex.sh → bench-coq/stats-to-tex.sh b/minuska-bench/stats-to-tex.sh → bench-coq/stats-to-tex.sh
diff --git a/...-bench/theories/benchmark-list.v.template → bench-coq/theories/benchmark-list.v.template b/...-bench/theories/benchmark-list.v.template → bench-coq/theories/benchmark-list.v.template
diff --git a/...-bench/theories/benchmark-template-head.v → bench-coq/theories/benchmark-template-head.v b/...-bench/theories/benchmark-template-head.v → bench-coq/theories/benchmark-template-head.v
diff --git a/minuska-bench/theories/benchmarking_in_coq.v → bench-coq/theories/benchmarking_in_coq.v b/minuska-bench/theories/benchmarking_in_coq.v → bench-coq/theories/benchmarking_in_coq.v
diff --git a/examples-hybrid/coqfiles/imp.v → bench-hybrid/coqfiles/imp.v b/examples-hybrid/coqfiles/imp.v → bench-hybrid/coqfiles/imp.v
diff --git a/examples-hybrid/imp-ast/count-1.imp → bench-hybrid/imp-ast/count-1.imp b/examples-hybrid/imp-ast/count-1.imp → bench-hybrid/imp-ast/count-1.imp
diff --git a/examples-hybrid/imp-ast/count-2.imp → bench-hybrid/imp-ast/count-2.imp b/examples-hybrid/imp-ast/count-2.imp → bench-hybrid/imp-ast/count-2.imp
diff --git a/examples-hybrid/imp-ast/count-3.imp → bench-hybrid/imp-ast/count-3.imp b/examples-hybrid/imp-ast/count-3.imp → bench-hybrid/imp-ast/count-3.imp
diff --git a/examples-hybrid/imp-ast/count-4.imp → bench-hybrid/imp-ast/count-4.imp b/examples-hybrid/imp-ast/count-4.imp → bench-hybrid/imp-ast/count-4.imp
diff --git a/examples-hybrid/imp-ast/count-5.imp → bench-hybrid/imp-ast/count-5.imp b/examples-hybrid/imp-ast/count-5.imp → bench-hybrid/imp-ast/count-5.imp
diff --git a/examples-hybrid/imp-ast/count-6.imp → bench-hybrid/imp-ast/count-6.imp b/examples-hybrid/imp-ast/count-6.imp → bench-hybrid/imp-ast/count-6.imp
diff --git a/examples-hybrid/imp-ast/count-7.imp → bench-hybrid/imp-ast/count-7.imp b/examples-hybrid/imp-ast/count-7.imp → bench-hybrid/imp-ast/count-7.imp
diff --git a/examples-hybrid/languages → bench-hybrid/languages b/examples-hybrid/languages → bench-hybrid/languages
diff --git a/bench-hybrid/tc-ast/tc10.ast b/bench-hybrid/tc-ast/tc10.ast
@@ -0,0 +1 @@
+(@builtin-int 10)
diff --git a/bench-hybrid/tc-ast/tc100.ast b/bench-hybrid/tc-ast/tc100.ast
@@ -0,0 +1 @@
+(@builtin-int 100)
diff --git a/bench-hybrid/tc-ast/tc20.ast b/bench-hybrid/tc-ast/tc20.ast
@@ -0,0 +1 @@
+(@builtin-int 20)
diff --git a/bench-hybrid/tc-ast/tc50.ast b/bench-hybrid/tc-ast/tc50.ast
@@ -0,0 +1 @@
+(@builtin-int 50)
diff --git a/examples-hybrid/test-imp/testCount1.v → bench-hybrid/test-imp/testCount1.v b/examples-hybrid/test-imp/testCount1.v → bench-hybrid/test-imp/testCount1.v
diff --git a/examples-hybrid/test-imp/testCount2.v → bench-hybrid/test-imp/testCount2.v b/examples-hybrid/test-imp/testCount2.v → bench-hybrid/test-imp/testCount2.v
diff --git a/examples-hybrid/test-imp/testCount3.v → bench-hybrid/test-imp/testCount3.v b/examples-hybrid/test-imp/testCount3.v → bench-hybrid/test-imp/testCount3.v
diff --git a/examples-hybrid/test-imp/testCount4.v → bench-hybrid/test-imp/testCount4.v b/examples-hybrid/test-imp/testCount4.v → bench-hybrid/test-imp/testCount4.v
diff --git a/examples-hybrid/test-imp/testCount5.v → bench-hybrid/test-imp/testCount5.v b/examples-hybrid/test-imp/testCount5.v → bench-hybrid/test-imp/testCount5.v
diff --git a/examples-hybrid/test-imp/testCount6.v → bench-hybrid/test-imp/testCount6.v b/examples-hybrid/test-imp/testCount6.v → bench-hybrid/test-imp/testCount6.v
diff --git a/examples-hybrid/test-imp/testCount7.v → bench-hybrid/test-imp/testCount7.v b/examples-hybrid/test-imp/testCount7.v → bench-hybrid/test-imp/testCount7.v
diff --git a/bench-hybrid/test-tc/testTC10.v b/bench-hybrid/test-tc/testTC10.v
@@ -0,0 +1,18 @@
+From Minuska Require
+  interp_loop
+.
+From Test Require
+  twocounters
+  tc10
+.
+
+Import String.
+Import Ascii.
+
+Time Compute (let steps := 10000 in
+  @interp_loop.interp_loop
+    default_everything.DSM
+    twocounters.lang_interpreter
+    steps
+    tc10.given_groundterm
+).
diff --git a/bench-hybrid/test-tc/testTC100.v b/bench-hybrid/test-tc/testTC100.v
@@ -0,0 +1,18 @@
+From Minuska Require
+  interp_loop
+.
+From Test Require
+  twocounters
+  tc100
+.
+
+Import String.
+Import Ascii.
+
+Time Compute (let steps := 10000 in
+  @interp_loop.interp_loop
+    default_everything.DSM
+    twocounters.lang_interpreter
+    steps
+    tc100.given_groundterm
+).
diff --git a/bench-hybrid/test-tc/testTC20.v b/bench-hybrid/test-tc/testTC20.v
@@ -0,0 +1,18 @@
+From Minuska Require
+  interp_loop
+.
+From Test Require
+  twocounters
+  tc20
+.
+
+Import String.
+Import Ascii.
+
+Time Compute (let steps := 10000 in
+  @interp_loop.interp_loop
+    default_everything.DSM
+    twocounters.lang_interpreter
+    steps
+    tc20.given_groundterm
+).
diff --git a/bench-hybrid/test-tc/testTC50.v b/bench-hybrid/test-tc/testTC50.v
@@ -0,0 +1,18 @@
+From Minuska Require
+  interp_loop
+.
+From Test Require
+  twocounters
+  tc50
+.
+
+Import String.
+Import Ascii.
+
+Time Compute (let steps := 10000 in
+  @interp_loop.interp_loop
+    default_everything.DSM
+    twocounters.lang_interpreter
+    steps
+    tc50.given_groundterm
+).
diff --git a/examples-hybrid/test.sh → bench-hybrid/test.sh b/examples-hybrid/test.sh → bench-hybrid/test.sh
@@ -9,6 +9,13 @@ pushd "$SCRIPT_DIR" > /dev/null
 
 TIME=$(which time)
 
+LOGFILEOUT="./log-stdout.txt"
+LOGFILEERR="./log-stderr.txt"
+if [[ -n "$VERBOSE" ]]; then
+  LOGFILEOUT=/dev/stdout
+  LOGFILEERR=/dev/stderr
+fi
+
 
 testInCoq() {
   rm -rf coqfiles
@@ -23,19 +30,28 @@ testInCoq() {
   minuska gt2coq ./imp-ast/count-5.imp coqfiles/count5.v
   minuska gt2coq ./imp-ast/count-6.imp coqfiles/count6.v
   minuska gt2coq ./imp-ast/count-7.imp coqfiles/count7.v
+  minuska def2coq ./languages/two-counters/two-counters.m coqfiles/twocounters.v
+  minuska gt2coq ./tc-ast/tc10.ast coqfiles/tc10.v
+  minuska gt2coq ./tc-ast/tc20.ast coqfiles/tc20.v
+  minuska gt2coq ./tc-ast/tc50.ast coqfiles/tc50.v
+  minuska gt2coq ./tc-ast/tc100.ast coqfiles/tc100.v
+
+
+
 
   echo "Compiling *.v files"
   pushd coqfiles > /dev/null
   for vfile in *.v; do
-    echo "Compiling $vfile" > /dev/null
-    coqc -R . Test "$vfile" > /dev/null 2>/dev/null
+    echo "Compiling $vfile" > "$LOGFILEOUT"
+    coqc -R . Test "$vfile" > "$LOGFILEOUT" 2>"$LOGFILEERR"
   done 
   popd > /dev/null
   cp test-imp/testCount*.v ./coqfiles/
+  cp test-tc/testTC*.v ./coqfiles/
   pushd coqfiles > /dev/null
-  for testvfile in testCount*.v; do
+  for testvfile in test*.v; do
     echo "coqc $testvfile"
-    "$TIME" --output "$testvfile.time" --format "%e" coqc -R . Test "$testvfile" 2> /dev/null | grep 'Finished transaction'
+    "$TIME" --output "$testvfile.time" --format "%e" coqc -R . Test "$testvfile" 2> "$LOGFILEERR" | grep 'Finished transaction'
     cat "$testvfile.time"
   done
   popd > /dev/null

diff --git a/examples-standalone/README.md → bench-standalone/README.md b/examples-standalone/README.md → bench-standalone/README.md
diff --git a/examples-standalone/languages → bench-standalone/languages b/examples-standalone/languages → bench-standalone/languages
diff --git a/examples-standalone/test.sh → bench-standalone/test.sh b/examples-standalone/test.sh → bench-standalone/test.sh
diff --git a/flake.nix b/flake.nix
@@ -101,12 +101,12 @@
       in {
         packages.minuska = minuskaFun { coqPackages = pkgs.coqPackages_8_19; } ;
 
-        packages.examples-coq
+        packages.old-examples-coq
         = pkgs.coqPackages_8_19.callPackage 
         ( { coq, stdenv }:
         stdenv.mkDerivation {
-          name = "examples-coq";
-          src = ./examples-coq;
+          name = "old-examples-coq";
+          src = ./old-examples-coq;
 
           propagatedBuildInputs = [
             self.outputs.packages.${system}.minuska
@@ -121,10 +121,10 @@
         } ) { } ;
 
 
-        packages.examples-standalone
+        packages.bench-standalone
         = pkgs.stdenv.mkDerivation {
-          name = "examples-standalone";
-          src = ./examples-standalone;
+          name = "bench-standalone";
+          src = ./bench-standalone;
           nativeBuildInputs = [
             self.outputs.packages.${system}.minuska
             pkgs.time
@@ -142,28 +142,28 @@
           #];
         };
 
-        packages.examples-hybrid
+        packages.bench-hybrid
         = pkgs.stdenv.mkDerivation {
-          name = "examples-hybrid";
-          src = ./examples-hybrid;
+          name = "bench-hybrid";
+          src = ./bench-hybrid;
           nativeBuildInputs = [
             self.outputs.packages.${system}.minuska
             pkgs.time
           ] ++ [self.outputs.packages.${system}.minuska.coqPackages.coq]
            ++ self.outputs.packages.${system}.minuska.coqLibraries ;
         };
 
-        packages.minuska-bench
+        packages.bench-coq
         = pkgs.coqPackages_8_19.callPackage 
         ( { coq, stdenv }:
         stdenv.mkDerivation {
-          name = "minuska-bench";
-          src = ./minuska-bench;
+          name = "bench-coq";
+          src = ./bench-coq;
 
           propagatedBuildInputs = [
             pkgs.time
             pkgs.python312
-            self.outputs.packages.${system}.examples-coq
+            self.outputs.packages.${system}.old-examples-coq
             #self.outputs.packages.${system}.examples-coq.coqPackages.coq
           ];
           enableParallelBuilding = true;
@@ -219,23 +219,23 @@
                 ];
               };
 
-          examples-standalone =
+          bench-standalone =
             let
-              examples-standalone = self.outputs.packages.${system}.examples-standalone;
+              bench-standalone = self.outputs.packages.${system}.bench-standalone;
             in
               pkgs.mkShell {
-                inputsFrom = [examples-standalone];
+                inputsFrom = [bench-standalone];
                 packages = [];
               };
 
-          minuska-bench =
+          bench-coq =
             let
-              minuska-bench = self.outputs.packages.${system}.minuska-bench;
+              bench-coq = self.outputs.packages.${system}.bench-coq;
             in
               pkgs.mkShell {
-                inputsFrom = [minuska-bench];
+                inputsFrom = [bench-coq];
                 packages = [
-                  minuska-bench.coqPackages.coq-lsp
+                  bench-coq.coqPackages.coq-lsp
                   #benchexec
                 ];
               };

diff --git a/minuska-bench/Makefile → old-examples-coq/Makefile b/minuska-bench/Makefile → old-examples-coq/Makefile
diff --git a/examples-coq/_CoqProject → old-examples-coq/_CoqProject b/examples-coq/_CoqProject → old-examples-coq/_CoqProject
diff --git a/examples-coq/src/example_lang_driver.ml → old-examples-coq/src/example_lang_driver.ml b/examples-coq/src/example_lang_driver.ml → old-examples-coq/src/example_lang_driver.ml
diff --git a/examples-coq/src/fib_native_driver.ml → old-examples-coq/src/fib_native_driver.ml b/examples-coq/src/fib_native_driver.ml → old-examples-coq/src/fib_native_driver.ml
diff --git a/examples-coq/src/generic_driver.ml → old-examples-coq/src/generic_driver.ml b/examples-coq/src/generic_driver.ml → old-examples-coq/src/generic_driver.ml
diff --git a/examples-coq/src/imp.ml → old-examples-coq/src/imp.ml b/examples-coq/src/imp.ml → old-examples-coq/src/imp.ml
diff --git a/examples-coq/src/imp_lexer.mll → old-examples-coq/src/imp_lexer.mll b/examples-coq/src/imp_lexer.mll → old-examples-coq/src/imp_lexer.mll
diff --git a/examples-coq/src/imp_parser.mly → old-examples-coq/src/imp_parser.mly b/examples-coq/src/imp_parser.mly → old-examples-coq/src/imp_parser.mly
diff --git a/examples-coq/src/sum_to_n_driver.ml → old-examples-coq/src/sum_to_n_driver.ml b/examples-coq/src/sum_to_n_driver.ml → old-examples-coq/src/sum_to_n_driver.ml
diff --git a/examples-coq/src/two_counters_driver.ml → old-examples-coq/src/two_counters_driver.ml b/examples-coq/src/two_counters_driver.ml → old-examples-coq/src/two_counters_driver.ml
diff --git a/examples-coq/theories/dep.v → old-examples-coq/theories/dep.v b/examples-coq/theories/dep.v → old-examples-coq/theories/dep.v
diff --git a/examples-coq/theories/examples.v → old-examples-coq/theories/examples.v b/examples-coq/theories/examples.v → old-examples-coq/theories/examples.v
diff --git a/examples-coq/theories/examples_unary_nat.v → ...xamples-coq/theories/examples_unary_nat.v b/examples-coq/theories/examples_unary_nat.v → ...xamples-coq/theories/examples_unary_nat.v
diff --git a/examples-coq/theories/extraction.v → old-examples-coq/theories/extraction.v b/examples-coq/theories/extraction.v → old-examples-coq/theories/extraction.v
diff --git a/examples-coq/trivial.m → old-examples-coq/trivial.m b/examples-coq/trivial.m → old-examples-coq/trivial.m