disable Lake benchmarks

leanprover · Jan 9, 2025 · c8d16d9 · c8d16d9
1 parent 3d95137
commit c8d16d9
Showing 1 changed file with 114 additions and 114 deletions.
diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml
@@ -117,120 +117,120 @@
     cmd: ./deriv.lean.out 10
   build_config:
     cmd: ./compile.sh deriv.lean
-- attributes:
-    description: lake build clean
-    tags: [slow]
-  run_config:
-    <<: *time
-    cmd: |
-      bash -c "
-      set -ex
-      ulimit -s unlimited
-      cd inundation
-      lake -flakefile-clean.lean clean
-      lake -flakefile-clean.lean build
-      "
-  build_config:
-    cmd: |
-      bash -c "
-      set -ex
-      ulimit -s unlimited
-      cd inundation
-      cp lakefile.lean lakefile-clean.lean
-      lake -flakefile-clean.lean -Ktest=Clean run mkBuild
-      lake -flakefile-clean.lean build
-      "
-- attributes:
-    description: lake build no-op
-    tags: [fast]
-  run_config:
-    <<: *time
-    cmd: |
-      bash -c "
-      set -ex
-      ulimit -s unlimited
-      lake -dinundation -flakefile-nop.lean build
-      "
-  build_config:
-    cmd: |
-      bash -c "
-      set -ex
-      ulimit -s unlimited
-      cd inundation
-      cp lakefile.lean lakefile-nop.lean
-      lake -flakefile-nop.lean -Ktest=Nop run mkBuild
-      lake -flakefile-nop.lean build
-      "
-- attributes:
-    description: lake config elab
-    tags: [fast]
-  run_config:
-    <<: *time
-    cmd: |
-      bash -c "
-      set -ex
-      ulimit -s unlimited
-      lake -dinundation -flakefile-rc.lean -R run nop
-      "
-  build_config:
-    cmd: cp inundation/lakefile.lean inundation/lakefile-rc.lean
-- attributes:
-    description: lake config import
-    tags: [fast]
-  run_config:
-    <<: *time
-    cmd: |
-      bash -c "
-      set -ex
-      ulimit -s unlimited
-      lake -dinundation run nop
-      "
-  build_config:
-    cmd: |
-      bash -c "
-      set -ex
-      ulimit -s unlimited
-      lake -dinundation run nop
-      "
-- attributes:
-    description: lake config tree
-    tags: [fast]
-  run_config:
-    <<: *time
-    cmd: |
-      bash -c "
-      set -ex
-      ulimit -s unlimited
-      lake -dinundation/test/tree run nop
-      "
-  build_config:
-    cmd: |
-      lake -dinundation run mkTree
-      lake -dinundation/test/tree update
-- attributes:
-    description: lake env
-    tags: [fast]
-  run_config:
-    <<: *time
-    cmd: |
-      bash -c "
-      set -ex
-      ulimit -s unlimited
-      lake -dinundation env true
-      "
-  build_config:
-    cmd: lake -dinundation env true
-- attributes:
-    description: lake startup
-    tags: [fast]
-  run_config:
-    <<: *time
-    cmd: |
-      bash -c "
-      set -ex
-      ulimit -s unlimited
-      lake self-check
-      "
+#- attributes:
+#    description: lake build clean
+#    tags: [slow]
+#  run_config:
+#    <<: *time
+#    cmd: |
+#      bash -c "
+#      set -ex
+#      ulimit -s unlimited
+#      cd inundation
+#      lake -flakefile-clean.lean clean
+#      lake -flakefile-clean.lean build
+#      "
+#  build_config:
+#    cmd: |
+#      bash -c "
+#      set -ex
+#      ulimit -s unlimited
+#      cd inundation
+#      cp lakefile.lean lakefile-clean.lean
+#      lake -flakefile-clean.lean -Ktest=Clean run mkBuild
+#      lake -flakefile-clean.lean build
+#      "
+#- attributes:
+#    description: lake build no-op
+#    tags: [fast]
+#  run_config:
+#    <<: *time
+#    cmd: |
+#      bash -c "
+#      set -ex
+#      ulimit -s unlimited
+#      lake -dinundation -flakefile-nop.lean build
+#      "
+#  build_config:
+#    cmd: |
+#      bash -c "
+#      set -ex
+#      ulimit -s unlimited
+#      cd inundation
+#      cp lakefile.lean lakefile-nop.lean
+#      lake -flakefile-nop.lean -Ktest=Nop run mkBuild
+#      lake -flakefile-nop.lean build
+#      "
+#- attributes:
+#    description: lake config elab
+#    tags: [fast]
+#  run_config:
+#    <<: *time
+#    cmd: |
+#      bash -c "
+#      set -ex
+#      ulimit -s unlimited
+#      lake -dinundation -flakefile-rc.lean -R run nop
+#      "
+#  build_config:
+#    cmd: cp inundation/lakefile.lean inundation/lakefile-rc.lean
+#- attributes:
+#    description: lake config import
+#    tags: [fast]
+#  run_config:
+#    <<: *time
+#    cmd: |
+#      bash -c "
+#      set -ex
+#      ulimit -s unlimited
+#      lake -dinundation run nop
+#      "
+#  build_config:
+#    cmd: |
+#      bash -c "
+#      set -ex
+#      ulimit -s unlimited
+#      lake -dinundation run nop
+#      "
+#- attributes:
+#    description: lake config tree
+#    tags: [fast]
+#  run_config:
+#    <<: *time
+#    cmd: |
+#      bash -c "
+#      set -ex
+#      ulimit -s unlimited
+#      lake -dinundation/test/tree run nop
+#      "
+#  build_config:
+#    cmd: |
+#      lake -dinundation run mkTree
+#      lake -dinundation/test/tree update
+#- attributes:
+#    description: lake env
+#    tags: [fast]
+#  run_config:
+#    <<: *time
+#    cmd: |
+#      bash -c "
+#      set -ex
+#      ulimit -s unlimited
+#      lake -dinundation env true
+#      "
+#  build_config:
+#    cmd: lake -dinundation env true
+#- attributes:
+#    description: lake startup
+#    tags: [fast]
+#  run_config:
+#    <<: *time
+#    cmd: |
+#      bash -c "
+#      set -ex
+#      ulimit -s unlimited
+#      lake self-check
+#      "
 - attributes:
     description: language server startup
     tags: [fast]