From 34cd1f39bb8e76a8d0ba3febfa7fc336d0c3f912 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Sat, 29 Jun 2024 17:47:10 +0200 Subject: [PATCH 1/3] Hybrid tests for two-counters --- examples-hybrid/tc-ast/tc10.ast | 1 + examples-hybrid/tc-ast/tc100.ast | 1 + examples-hybrid/tc-ast/tc20.ast | 1 + examples-hybrid/tc-ast/tc50.ast | 1 + examples-hybrid/test-tc/testTC10.v | 18 ++++++++++++++++++ examples-hybrid/test-tc/testTC100.v | 18 ++++++++++++++++++ examples-hybrid/test-tc/testTC20.v | 18 ++++++++++++++++++ examples-hybrid/test-tc/testTC50.v | 18 ++++++++++++++++++ examples-hybrid/test.sh | 5 ++++- 9 files changed, 80 insertions(+), 1 deletion(-) create mode 100644 examples-hybrid/tc-ast/tc10.ast create mode 100644 examples-hybrid/tc-ast/tc100.ast create mode 100644 examples-hybrid/tc-ast/tc20.ast create mode 100644 examples-hybrid/tc-ast/tc50.ast create mode 100644 examples-hybrid/test-tc/testTC10.v create mode 100644 examples-hybrid/test-tc/testTC100.v create mode 100644 examples-hybrid/test-tc/testTC20.v create mode 100644 examples-hybrid/test-tc/testTC50.v diff --git a/examples-hybrid/tc-ast/tc10.ast b/examples-hybrid/tc-ast/tc10.ast new file mode 100644 index 00000000..059374ee --- /dev/null +++ b/examples-hybrid/tc-ast/tc10.ast @@ -0,0 +1 @@ +(@builtin-int 10) diff --git a/examples-hybrid/tc-ast/tc100.ast b/examples-hybrid/tc-ast/tc100.ast new file mode 100644 index 00000000..8b02f30d --- /dev/null +++ b/examples-hybrid/tc-ast/tc100.ast @@ -0,0 +1 @@ +(@builtin-int 100) diff --git a/examples-hybrid/tc-ast/tc20.ast b/examples-hybrid/tc-ast/tc20.ast new file mode 100644 index 00000000..aa6419c2 --- /dev/null +++ b/examples-hybrid/tc-ast/tc20.ast @@ -0,0 +1 @@ +(@builtin-int 20) diff --git a/examples-hybrid/tc-ast/tc50.ast b/examples-hybrid/tc-ast/tc50.ast new file mode 100644 index 00000000..e64ed299 --- /dev/null +++ b/examples-hybrid/tc-ast/tc50.ast @@ -0,0 +1 @@ +(@builtin-int 50) diff --git a/examples-hybrid/test-tc/testTC10.v b/examples-hybrid/test-tc/testTC10.v new file mode 100644 index 00000000..ed62a453 --- /dev/null +++ b/examples-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/examples-hybrid/test-tc/testTC100.v b/examples-hybrid/test-tc/testTC100.v new file mode 100644 index 00000000..69214f8e --- /dev/null +++ b/examples-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/examples-hybrid/test-tc/testTC20.v b/examples-hybrid/test-tc/testTC20.v new file mode 100644 index 00000000..0566f87e --- /dev/null +++ b/examples-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/examples-hybrid/test-tc/testTC50.v b/examples-hybrid/test-tc/testTC50.v new file mode 100644 index 00000000..7fa6f8e6 --- /dev/null +++ b/examples-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 b/examples-hybrid/test.sh index 23fa5742..184c4367 100755 --- a/examples-hybrid/test.sh +++ b/examples-hybrid/test.sh @@ -23,6 +23,8 @@ 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 echo "Compiling *.v files" pushd coqfiles > /dev/null @@ -32,8 +34,9 @@ testInCoq() { 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' cat "$testvfile.time" From 67787f9b2a4e3a9040f0141a143a5aebbc239418 Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Sat, 29 Jun 2024 18:25:55 +0200 Subject: [PATCH 2/3] rename and move stuff around --- .github/workflows/build-and-profile.yml | 15 +++++--- {examples-coq => bench-coq}/Makefile | 0 {minuska-bench => bench-coq}/_CoqProject | 0 .../build-and-profile.sh | 0 .../generate-v-files.py | 0 .../parse-log-groups.py | 0 .../parse-timing-log.sh | 0 {minuska-bench => bench-coq}/stats-to-tex.sh | 0 .../theories/benchmark-list.v.template | 0 .../theories/benchmark-template-head.v | 0 .../theories/benchmarking_in_coq.v | 0 .../coqfiles/imp.v | 0 .../imp-ast/count-1.imp | 0 .../imp-ast/count-2.imp | 0 .../imp-ast/count-3.imp | 0 .../imp-ast/count-4.imp | 0 .../imp-ast/count-5.imp | 0 .../imp-ast/count-6.imp | 0 .../imp-ast/count-7.imp | 0 {examples-hybrid => bench-hybrid}/languages | 0 .../tc-ast/tc10.ast | 0 .../tc-ast/tc100.ast | 0 .../tc-ast/tc20.ast | 0 .../tc-ast/tc50.ast | 0 .../test-imp/testCount1.v | 0 .../test-imp/testCount2.v | 0 .../test-imp/testCount3.v | 0 .../test-imp/testCount4.v | 0 .../test-imp/testCount5.v | 0 .../test-imp/testCount6.v | 0 .../test-imp/testCount7.v | 0 .../test-tc/testTC10.v | 0 .../test-tc/testTC100.v | 0 .../test-tc/testTC20.v | 0 .../test-tc/testTC50.v | 0 {examples-hybrid => bench-hybrid}/test.sh | 21 ++++++++-- .../README.md | 0 .../languages | 0 .../test.sh | 0 flake.nix | 38 +++++++++---------- {minuska-bench => old-examples-coq}/Makefile | 0 .../_CoqProject | 0 .../src/example_lang_driver.ml | 0 .../src/fib_native_driver.ml | 0 .../src/generic_driver.ml | 0 {examples-coq => old-examples-coq}/src/imp.ml | 0 .../src/imp_lexer.mll | 0 .../src/imp_parser.mly | 0 .../src/sum_to_n_driver.ml | 0 .../src/two_counters_driver.ml | 0 .../theories/dep.v | 0 .../theories/examples.v | 0 .../theories/examples_unary_nat.v | 0 .../theories/extraction.v | 0 {examples-coq => old-examples-coq}/trivial.m | 0 55 files changed, 45 insertions(+), 29 deletions(-) rename {examples-coq => bench-coq}/Makefile (100%) rename {minuska-bench => bench-coq}/_CoqProject (100%) rename {minuska-bench => bench-coq}/build-and-profile.sh (100%) rename {minuska-bench => bench-coq}/generate-v-files.py (100%) rename {minuska-bench => bench-coq}/parse-log-groups.py (100%) rename {minuska-bench => bench-coq}/parse-timing-log.sh (100%) rename {minuska-bench => bench-coq}/stats-to-tex.sh (100%) rename {minuska-bench => bench-coq}/theories/benchmark-list.v.template (100%) rename {minuska-bench => bench-coq}/theories/benchmark-template-head.v (100%) rename {minuska-bench => bench-coq}/theories/benchmarking_in_coq.v (100%) rename {examples-hybrid => bench-hybrid}/coqfiles/imp.v (100%) rename {examples-hybrid => bench-hybrid}/imp-ast/count-1.imp (100%) rename {examples-hybrid => bench-hybrid}/imp-ast/count-2.imp (100%) rename {examples-hybrid => bench-hybrid}/imp-ast/count-3.imp (100%) rename {examples-hybrid => bench-hybrid}/imp-ast/count-4.imp (100%) rename {examples-hybrid => bench-hybrid}/imp-ast/count-5.imp (100%) rename {examples-hybrid => bench-hybrid}/imp-ast/count-6.imp (100%) rename {examples-hybrid => bench-hybrid}/imp-ast/count-7.imp (100%) rename {examples-hybrid => bench-hybrid}/languages (100%) rename {examples-hybrid => bench-hybrid}/tc-ast/tc10.ast (100%) rename {examples-hybrid => bench-hybrid}/tc-ast/tc100.ast (100%) rename {examples-hybrid => bench-hybrid}/tc-ast/tc20.ast (100%) rename {examples-hybrid => bench-hybrid}/tc-ast/tc50.ast (100%) rename {examples-hybrid => bench-hybrid}/test-imp/testCount1.v (100%) rename {examples-hybrid => bench-hybrid}/test-imp/testCount2.v (100%) rename {examples-hybrid => bench-hybrid}/test-imp/testCount3.v (100%) rename {examples-hybrid => bench-hybrid}/test-imp/testCount4.v (100%) rename {examples-hybrid => bench-hybrid}/test-imp/testCount5.v (100%) rename {examples-hybrid => bench-hybrid}/test-imp/testCount6.v (100%) rename {examples-hybrid => bench-hybrid}/test-imp/testCount7.v (100%) rename {examples-hybrid => bench-hybrid}/test-tc/testTC10.v (100%) rename {examples-hybrid => bench-hybrid}/test-tc/testTC100.v (100%) rename {examples-hybrid => bench-hybrid}/test-tc/testTC20.v (100%) rename {examples-hybrid => bench-hybrid}/test-tc/testTC50.v (100%) rename {examples-hybrid => bench-hybrid}/test.sh (71%) rename {examples-standalone => bench-standalone}/README.md (100%) rename {examples-standalone => bench-standalone}/languages (100%) rename {examples-standalone => bench-standalone}/test.sh (100%) rename {minuska-bench => old-examples-coq}/Makefile (100%) rename {examples-coq => old-examples-coq}/_CoqProject (100%) rename {examples-coq => old-examples-coq}/src/example_lang_driver.ml (100%) rename {examples-coq => old-examples-coq}/src/fib_native_driver.ml (100%) rename {examples-coq => old-examples-coq}/src/generic_driver.ml (100%) rename {examples-coq => old-examples-coq}/src/imp.ml (100%) rename {examples-coq => old-examples-coq}/src/imp_lexer.mll (100%) rename {examples-coq => old-examples-coq}/src/imp_parser.mly (100%) rename {examples-coq => old-examples-coq}/src/sum_to_n_driver.ml (100%) rename {examples-coq => old-examples-coq}/src/two_counters_driver.ml (100%) rename {examples-coq => old-examples-coq}/theories/dep.v (100%) rename {examples-coq => old-examples-coq}/theories/examples.v (100%) rename {examples-coq => old-examples-coq}/theories/examples_unary_nat.v (100%) rename {examples-coq => old-examples-coq}/theories/extraction.v (100%) rename {examples-coq => old-examples-coq}/trivial.m (100%) diff --git a/.github/workflows/build-and-profile.yml b/.github/workflows/build-and-profile.yml index cc701f42..f06747f9 100644 --- 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 b/bench-coq/Makefile similarity index 100% rename from examples-coq/Makefile rename to bench-coq/Makefile diff --git a/minuska-bench/_CoqProject b/bench-coq/_CoqProject similarity index 100% rename from minuska-bench/_CoqProject rename to bench-coq/_CoqProject diff --git a/minuska-bench/build-and-profile.sh b/bench-coq/build-and-profile.sh similarity index 100% rename from minuska-bench/build-and-profile.sh rename to bench-coq/build-and-profile.sh diff --git a/minuska-bench/generate-v-files.py b/bench-coq/generate-v-files.py similarity index 100% rename from minuska-bench/generate-v-files.py rename to bench-coq/generate-v-files.py diff --git a/minuska-bench/parse-log-groups.py b/bench-coq/parse-log-groups.py similarity index 100% rename from minuska-bench/parse-log-groups.py rename to bench-coq/parse-log-groups.py diff --git a/minuska-bench/parse-timing-log.sh b/bench-coq/parse-timing-log.sh similarity index 100% rename from minuska-bench/parse-timing-log.sh rename to bench-coq/parse-timing-log.sh diff --git a/minuska-bench/stats-to-tex.sh b/bench-coq/stats-to-tex.sh similarity index 100% rename from minuska-bench/stats-to-tex.sh rename to bench-coq/stats-to-tex.sh diff --git a/minuska-bench/theories/benchmark-list.v.template b/bench-coq/theories/benchmark-list.v.template similarity index 100% rename from minuska-bench/theories/benchmark-list.v.template rename to bench-coq/theories/benchmark-list.v.template diff --git a/minuska-bench/theories/benchmark-template-head.v b/bench-coq/theories/benchmark-template-head.v similarity index 100% rename from minuska-bench/theories/benchmark-template-head.v rename to bench-coq/theories/benchmark-template-head.v diff --git a/minuska-bench/theories/benchmarking_in_coq.v b/bench-coq/theories/benchmarking_in_coq.v similarity index 100% rename from minuska-bench/theories/benchmarking_in_coq.v rename to bench-coq/theories/benchmarking_in_coq.v diff --git a/examples-hybrid/coqfiles/imp.v b/bench-hybrid/coqfiles/imp.v similarity index 100% rename from examples-hybrid/coqfiles/imp.v rename to bench-hybrid/coqfiles/imp.v diff --git a/examples-hybrid/imp-ast/count-1.imp b/bench-hybrid/imp-ast/count-1.imp similarity index 100% rename from examples-hybrid/imp-ast/count-1.imp rename to bench-hybrid/imp-ast/count-1.imp diff --git a/examples-hybrid/imp-ast/count-2.imp b/bench-hybrid/imp-ast/count-2.imp similarity index 100% rename from examples-hybrid/imp-ast/count-2.imp rename to bench-hybrid/imp-ast/count-2.imp diff --git a/examples-hybrid/imp-ast/count-3.imp b/bench-hybrid/imp-ast/count-3.imp similarity index 100% rename from examples-hybrid/imp-ast/count-3.imp rename to bench-hybrid/imp-ast/count-3.imp diff --git a/examples-hybrid/imp-ast/count-4.imp b/bench-hybrid/imp-ast/count-4.imp similarity index 100% rename from examples-hybrid/imp-ast/count-4.imp rename to bench-hybrid/imp-ast/count-4.imp diff --git a/examples-hybrid/imp-ast/count-5.imp b/bench-hybrid/imp-ast/count-5.imp similarity index 100% rename from examples-hybrid/imp-ast/count-5.imp rename to bench-hybrid/imp-ast/count-5.imp diff --git a/examples-hybrid/imp-ast/count-6.imp b/bench-hybrid/imp-ast/count-6.imp similarity index 100% rename from examples-hybrid/imp-ast/count-6.imp rename to bench-hybrid/imp-ast/count-6.imp diff --git a/examples-hybrid/imp-ast/count-7.imp b/bench-hybrid/imp-ast/count-7.imp similarity index 100% rename from examples-hybrid/imp-ast/count-7.imp rename to bench-hybrid/imp-ast/count-7.imp diff --git a/examples-hybrid/languages b/bench-hybrid/languages similarity index 100% rename from examples-hybrid/languages rename to bench-hybrid/languages diff --git a/examples-hybrid/tc-ast/tc10.ast b/bench-hybrid/tc-ast/tc10.ast similarity index 100% rename from examples-hybrid/tc-ast/tc10.ast rename to bench-hybrid/tc-ast/tc10.ast diff --git a/examples-hybrid/tc-ast/tc100.ast b/bench-hybrid/tc-ast/tc100.ast similarity index 100% rename from examples-hybrid/tc-ast/tc100.ast rename to bench-hybrid/tc-ast/tc100.ast diff --git a/examples-hybrid/tc-ast/tc20.ast b/bench-hybrid/tc-ast/tc20.ast similarity index 100% rename from examples-hybrid/tc-ast/tc20.ast rename to bench-hybrid/tc-ast/tc20.ast diff --git a/examples-hybrid/tc-ast/tc50.ast b/bench-hybrid/tc-ast/tc50.ast similarity index 100% rename from examples-hybrid/tc-ast/tc50.ast rename to bench-hybrid/tc-ast/tc50.ast diff --git a/examples-hybrid/test-imp/testCount1.v b/bench-hybrid/test-imp/testCount1.v similarity index 100% rename from examples-hybrid/test-imp/testCount1.v rename to bench-hybrid/test-imp/testCount1.v diff --git a/examples-hybrid/test-imp/testCount2.v b/bench-hybrid/test-imp/testCount2.v similarity index 100% rename from examples-hybrid/test-imp/testCount2.v rename to bench-hybrid/test-imp/testCount2.v diff --git a/examples-hybrid/test-imp/testCount3.v b/bench-hybrid/test-imp/testCount3.v similarity index 100% rename from examples-hybrid/test-imp/testCount3.v rename to bench-hybrid/test-imp/testCount3.v diff --git a/examples-hybrid/test-imp/testCount4.v b/bench-hybrid/test-imp/testCount4.v similarity index 100% rename from examples-hybrid/test-imp/testCount4.v rename to bench-hybrid/test-imp/testCount4.v diff --git a/examples-hybrid/test-imp/testCount5.v b/bench-hybrid/test-imp/testCount5.v similarity index 100% rename from examples-hybrid/test-imp/testCount5.v rename to bench-hybrid/test-imp/testCount5.v diff --git a/examples-hybrid/test-imp/testCount6.v b/bench-hybrid/test-imp/testCount6.v similarity index 100% rename from examples-hybrid/test-imp/testCount6.v rename to bench-hybrid/test-imp/testCount6.v diff --git a/examples-hybrid/test-imp/testCount7.v b/bench-hybrid/test-imp/testCount7.v similarity index 100% rename from examples-hybrid/test-imp/testCount7.v rename to bench-hybrid/test-imp/testCount7.v diff --git a/examples-hybrid/test-tc/testTC10.v b/bench-hybrid/test-tc/testTC10.v similarity index 100% rename from examples-hybrid/test-tc/testTC10.v rename to bench-hybrid/test-tc/testTC10.v diff --git a/examples-hybrid/test-tc/testTC100.v b/bench-hybrid/test-tc/testTC100.v similarity index 100% rename from examples-hybrid/test-tc/testTC100.v rename to bench-hybrid/test-tc/testTC100.v diff --git a/examples-hybrid/test-tc/testTC20.v b/bench-hybrid/test-tc/testTC20.v similarity index 100% rename from examples-hybrid/test-tc/testTC20.v rename to bench-hybrid/test-tc/testTC20.v diff --git a/examples-hybrid/test-tc/testTC50.v b/bench-hybrid/test-tc/testTC50.v similarity index 100% rename from examples-hybrid/test-tc/testTC50.v rename to bench-hybrid/test-tc/testTC50.v diff --git a/examples-hybrid/test.sh b/bench-hybrid/test.sh similarity index 71% rename from examples-hybrid/test.sh rename to bench-hybrid/test.sh index 184c4367..d5b34eb6 100755 --- a/examples-hybrid/test.sh +++ b/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 @@ -25,20 +32,26 @@ testInCoq() { 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 "test"*.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 b/bench-standalone/README.md similarity index 100% rename from examples-standalone/README.md rename to bench-standalone/README.md diff --git a/examples-standalone/languages b/bench-standalone/languages similarity index 100% rename from examples-standalone/languages rename to bench-standalone/languages diff --git a/examples-standalone/test.sh b/bench-standalone/test.sh similarity index 100% rename from examples-standalone/test.sh rename to bench-standalone/test.sh diff --git a/flake.nix b/flake.nix index 06757645..5f678427 100644 --- 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,10 +142,10 @@ #]; }; - 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 @@ -153,12 +153,12 @@ ++ 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 @@ -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 b/old-examples-coq/Makefile similarity index 100% rename from minuska-bench/Makefile rename to old-examples-coq/Makefile diff --git a/examples-coq/_CoqProject b/old-examples-coq/_CoqProject similarity index 100% rename from examples-coq/_CoqProject rename to old-examples-coq/_CoqProject diff --git a/examples-coq/src/example_lang_driver.ml b/old-examples-coq/src/example_lang_driver.ml similarity index 100% rename from examples-coq/src/example_lang_driver.ml rename to old-examples-coq/src/example_lang_driver.ml diff --git a/examples-coq/src/fib_native_driver.ml b/old-examples-coq/src/fib_native_driver.ml similarity index 100% rename from examples-coq/src/fib_native_driver.ml rename to old-examples-coq/src/fib_native_driver.ml diff --git a/examples-coq/src/generic_driver.ml b/old-examples-coq/src/generic_driver.ml similarity index 100% rename from examples-coq/src/generic_driver.ml rename to old-examples-coq/src/generic_driver.ml diff --git a/examples-coq/src/imp.ml b/old-examples-coq/src/imp.ml similarity index 100% rename from examples-coq/src/imp.ml rename to old-examples-coq/src/imp.ml diff --git a/examples-coq/src/imp_lexer.mll b/old-examples-coq/src/imp_lexer.mll similarity index 100% rename from examples-coq/src/imp_lexer.mll rename to old-examples-coq/src/imp_lexer.mll diff --git a/examples-coq/src/imp_parser.mly b/old-examples-coq/src/imp_parser.mly similarity index 100% rename from examples-coq/src/imp_parser.mly rename to old-examples-coq/src/imp_parser.mly diff --git a/examples-coq/src/sum_to_n_driver.ml b/old-examples-coq/src/sum_to_n_driver.ml similarity index 100% rename from examples-coq/src/sum_to_n_driver.ml rename to old-examples-coq/src/sum_to_n_driver.ml diff --git a/examples-coq/src/two_counters_driver.ml b/old-examples-coq/src/two_counters_driver.ml similarity index 100% rename from examples-coq/src/two_counters_driver.ml rename to old-examples-coq/src/two_counters_driver.ml diff --git a/examples-coq/theories/dep.v b/old-examples-coq/theories/dep.v similarity index 100% rename from examples-coq/theories/dep.v rename to old-examples-coq/theories/dep.v diff --git a/examples-coq/theories/examples.v b/old-examples-coq/theories/examples.v similarity index 100% rename from examples-coq/theories/examples.v rename to old-examples-coq/theories/examples.v diff --git a/examples-coq/theories/examples_unary_nat.v b/old-examples-coq/theories/examples_unary_nat.v similarity index 100% rename from examples-coq/theories/examples_unary_nat.v rename to old-examples-coq/theories/examples_unary_nat.v diff --git a/examples-coq/theories/extraction.v b/old-examples-coq/theories/extraction.v similarity index 100% rename from examples-coq/theories/extraction.v rename to old-examples-coq/theories/extraction.v diff --git a/examples-coq/trivial.m b/old-examples-coq/trivial.m similarity index 100% rename from examples-coq/trivial.m rename to old-examples-coq/trivial.m From 1cd350455f870fb029b49704b77069c06898ac6a Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Sat, 29 Jun 2024 18:34:10 +0200 Subject: [PATCH 3/3] fix nix --- flake.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/flake.nix b/flake.nix index 5f678427..99c16f8f 100644 --- a/flake.nix +++ b/flake.nix @@ -163,7 +163,7 @@ 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;