search

runtimeverification / haskell-backend

The symbolic execution engine powering the K Framework
BSD 3-Clause "New" or "Revised" License
210 stars 42 forks source link

[Haskell-Performance] Low productivity warning while prooving with KPlutus #3341

Closed ChristianoBraga closed 1 year ago

ChristianoBraga commented 2 years ago

Steps to reproduce the warning

While proving with KPlutus I get this low productivity warning which tells me to open a bug report at the Haskell backend. I created a branch with the problem (which is on the master at this time anyways): https://github.com/runtimeverification/plutus-core-semantics/tree/prod-drop

The following steps should be enough to reproduce the problem:

  1. Clone KPlutus repo https://github.com/runtimeverification/plutus-core-semantics.
  2. Change to plutus-core-semantics.
  3. Switch to prod-drop branch.
  4. git submodule update --init --recursive
  5. make deps
  6. make build
  7. make tests/specs/Oracle/claims.md.prove

Here is my output:

❯ time make tests/specs/Oracle/claims.md.prove                                                 
kplc kompile --backend haskell tests/specs/Oracle/verification.md --directory tests/specs/Oracle/verification/haskell
== /data/RV/plutus-core-semantics/.build/usr/bin/kplc: kompile tests/specs/Oracle/verification.md --directory tests/specs/Oracle/verification/haskell --backend haskell -I /data/RV/plutus-cor
e-semantics/.build/usr/lib/kplutus/include/kframework -I /data/RV/plutus-core-semantics/.build/usr/lib/kplutus/blockchain-k-plugin/include/kframework --hook-namespaces KRYPTO --emit-json --m
d-selector k | libcrypto-extra | symbolic                                                      
[Warning] Compiler: Could not find main syntax module with name
VERIFICATION-SYNTAX in definition.  Use --syntax-module to specify one. Using                                                                                                                 
VERIFICATION as default.
kplc prove --directory tests/specs/Oracle/verification/haskell tests/specs/Oracle/claims.md 
== /data/RV/plutus-core-semantics/.build/usr/bin/kplc: kprove --directory tests/specs/Oracle/verification/haskell tests/specs/Oracle/claims.md -I /data/RV/plutus-core-semantics/.build/usr/li
b/kplutus/include/kframework -I /data/RV/plutus-core-semantics/.build/usr/lib/kplutus/blockchain-k-plugin/include/kframework
kore-exec: [192517276] Warning (WarnIfLowProductivity):
    Productivity dropped to: 89%
    Relevant K files include:
        /data/RV/plutus-core-semantics/tests/specs/Oracle/verification.md
        /data/RV/plutus-core-semantics/tests/specs/Oracle/claims.md
    Poor productivity may indicate a performance bug.
    Please file a bug report: https://github.com/runtimeverification/haskell-backend/issues
#Top
make tests/specs/Oracle/claims.md.prove  264.52s user 6.87s system 130% cpu 3:27.98 total
ehildenb commented 1 year ago

@ChristianoBraga can you please submit a bug report tarball here? You can do that by adding --bug-report my-bug-report to the invocation of kore-exec, which you can do by doing export KORE_EXEC_OPTS='--bug-report my-bug-report' before the call to make ... that you have there.

ChristianoBraga commented 1 year ago

Actually, it stopped happening 😁 I will do as you say should it start again... Thank you!

On Thu, Nov 17, 2022 at 1:45 PM Everett Hildenbrandt < @.***> wrote:

@ChristianoBraga https://github.com/ChristianoBraga can you please submit a bug report tarball here? You can do that by adding --bug-report my-bug-report to the invocation of kore-exec, which you can do by doing export KORE_EXEC_OPTS='--bug-report my-bug-report' before the call to make ... that you have there.

— Reply to this email directly, view it on GitHub https://github.com/runtimeverification/haskell-backend/issues/3341#issuecomment-1318914646, or unsubscribe https://github.com/notifications/unsubscribe-auth/AFNNCEL6UZ2BIKSO62IDSLTWIZOMNANCNFSM6AAAAAARQIUQZA . You are receiving this because you were mentioned.Message ID: @.***>