Unable to complete pl-tutorial/1_k/5_types/lesson_9 tutorial

[QWYNG]

Hi! I am a beginner in k. I was doing the tutorial and there are some parts that are not working properly. How to fix it?

In /k-distribution/pl-tutorial/1_k/5_types/lesson_9

⋊> ~/p/1/5/lesson_9 on master ↑ kompile lambda.k --backend haskell --no-haskell-binary
[Warning] Compiler: Could not find main syntax module with name LAMBDA-SYNTAX
in definition.  Use --syntax-module to specify one. Using LAMBDA as default.
⋊> ~/p/1/5/lesson_9 on master ↑ krun tests/identities-1.lambda
kore-exec: [337522] Error (ErrorException):
    Error: missing hook
    Symbol
        Lbl'Hash'metaKVariables'LParUndsRParUnds'UNIFICATION'Unds'Set'Unds'K{}
    declared with attribute
        hook{}("UNIFICATION.metaVariables")
    We don't recognize that hook and it was not given any rules.
    Please open a feature request at
        https://github.com/runtimeverification/haskell-backend/issues
    and include the text of this message.
    Workaround: Give rules for Lbl'Hash'metaKVariables'LParUndsRParUnds'UNIFICATION'Unds'Set'Unds'K{}
    CallStack (from HasCallStack):
      error, called at src/Kore/Rewrite/Function/Evaluator.hs:376:6 in kore-0.60.0.0-DQV5EvvJ1sWI4UtF1vuovR:Kore.Rewrite.Function.Evaluator
Created bug report: kore-exec.tar.gz
[Error] krun: kore-exec ./lambda-kompiled/definition.kore --module LAMBDA
--pattern
/var/folders/_m/v5lvps113rj1tqw9308ktky40000gn/T/.krun-2023-10-10-22-13-19-8w4oH
sCZ4C/tmp.in.SNenxv3cwo --output
/var/folders/_m/v5lvps113rj1tqw9308ktky40000gn/T/.krun-2023-10-10-22-13-19-8w4oH
sCZ4C/result.kore
[Error] krun: Backend crashed during rewriting with exit code 1

Environment

M2 Macs

⋊> ~/p/1/5/lesson_9 on master ↑ krun --version
K version:    v6.0.136
Build date:   火 10 10 19:44:19 JST 2023
⋊> ~/p/1/5/lesson_9 on master ↑ kompile --version
K version:    v6.0.136
Build date:   火 10 10 19:44:19 JST 2023

[Baltoli]

Thanks for your interest in K!

That particular language definition is not designed to work with the Haskell backend for K; it uses the substitution module which isn't implemented for that backend (that's the cause of the "missing hook" error you see). You should be able to use the LLVM backend to complete the lesson, so I'm going to close this issue for now.

Please let us know if there's anything else we can help you with, and feel free to reopen this issue if you run into problems with this lesson again!

[QWYNG]

@Baltoli Thank you for your help! But llvm backend does not seem to kompile /k-distribution/pl-tutorial/1_k/5_types/lesson_9/lambda.k

⋊> ~/p/1/5/lesson_9 on master ↑ kompile lambda.k --backend llvm
[Error] Compiler: Found existential variable not supported by concrete backend.
        Source(/Users/qwyng/k/k-distribution/pl-tutorial/1_k/5_types/lesson_9/lambda.k)
        Location(41,31,41,33)
        41 |      rule <k> lambda X:Id . E => ?T:Type -> E ~> setTenv(TEnv) ...</k>
           .                                  ^~
[Error] Compiler: Found existential variable not supported by concrete backend.
        Source(/Users/qwyng/k/k-distribution/pl-tutorial/1_k/5_types/lesson_9/lambda.k)
        Location(42,33,42,35)
        42 |           <tenv> TEnv => TEnv[X <- ?T] </tenv>
           .                                    ^~
[Error] Compiler: Found existential variable not supported by concrete backend.
        Source(/Users/qwyng/k/k-distribution/pl-tutorial/1_k/5_types/lesson_9/lambda.k)
        Location(44,39,44,41)
        44 |      rule T1:Type T2:Type => T1 = (T2 -> ?T:Type) ~> ?T
           .                                          ^~
[Error] Compiler: Found existential variable not supported by concrete backend.
        Source(/Users/qwyng/k/k-distribution/pl-tutorial/1_k/5_types/lesson_9/lambda.k)
        Location(44,51,44,53)
        44 |      rule T1:Type T2:Type => T1 = (T2 -> ?T:Type) ~> ?T
           .                                                      ^~
[Error] Compiler: Found existential variable not supported by concrete backend.
        Source(/Users/qwyng/k/k-distribution/pl-tutorial/1_k/5_types/lesson_9/lambda.k)
        Location(57,32,57,34)
        57 |      rule <k> mu X:Id . E:Exp => (?T:Type -> ?T) E ~> setTenv(TEnv) ...</k>
           .                                   ^~
[Error] Compiler: Found existential variable not supported by concrete backend.
        Source(/Users/qwyng/k/k-distribution/pl-tutorial/1_k/5_types/lesson_9/lambda.k)
        Location(57,43,57,45)
        57 |      rule <k> mu X:Id . E:Exp => (?T:Type -> ?T) E ~> setTenv(TEnv) ...</k>
           .                                              ^~
[Error] Compiler: Found existential variable not supported by concrete backend.
        Source(/Users/qwyng/k/k-distribution/pl-tutorial/1_k/5_types/lesson_9/lambda.k)
        Location(58,33,58,35)
        58 |           <tenv> TEnv => TEnv[X <- ?T] </tenv>
           .                                    ^~
[Error] Compiler: Had 7 structural errors.
[Warning] Compiler: Could not find main syntax module with name LAMBDA-SYNTAX
in definition.  Use --syntax-module to specify one. Using LAMBDA as default.

[Baltoli]

Ah, I was mistaken - that lesson actually uses an intersection of K features that are no longer supported: https://github.com/runtimeverification/k/commit/6c122465e238d5df71a8b4c2fe71d79ab2089216. This should be documented better; apologies for the confusion!

[Baltoli]

See #3704 @QWYNG - this is an oversight on our end; please let us know if we can help you further