K-user mailing list

["dongbiao830415 AT foxmail.com" <dongbiao830415 AT foxmail.com>]

When using kompile(runtimeverification/k), it fails to compile the lambda.k(a very simple example).

cat lambda.k

[root@localhost hello]# cat lambda.k 
// Copyright (c) 2012-2016 K Team. All Rights Reserved.
module LAMBDA-SYNTAX
  syntax Val ::= Id
               | "lambda" Id "." Exp
  syntax Exp ::= Val
               | Exp Exp      [left]
               | "(" Exp ")"  [bracket]
endmodule

(1) kompile --no-prelude lambda.k. Output:

[root@localhost hello]# kompile --no-prelude lambda.k 
[Error] Compiler: Could not find sorts: [Id]
	Source(/root/src/c-semantics/hello/./lambda.k)
	Location(4,18,4,19)

(2) kompile lambda.k. Output:

[root@localhost hello]# kompile lambda.k
[Error] Compiler: Could not find main module with name LAMBDA in definition.
Use --main-module to specify one.

I don't know what the reason is.
Who has the latest K manual?
Thank you.

---

dongbiao830415 AT foxmail.com