K-user mailing list

[Mike Stay <stay AT pyrofex.net>]

That file compiles fine as written for me; it must be a problem with
your installation.  What does it say when you run it with --debug?

On Sat, Jul 22, 2017 at 9:05 PM, 
dongbiao830415 AT foxmail.com
<dongbiao830415 AT foxmail.com>
 wrote:
>
> [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
>
> module LAMBDA
>     imports LAMBDA-SYNTAX
> endmodule
>
> [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)
>
> [root@localhost hello]# kompile  lambda.k
> [Error] Internal: Uncaught exception thrown of type NoSuchElementException.
> Please rerun your program with the --debug flag to generate a stack trace,
> and
> file a bug report at https://github.com/kframework/k/issues (None.get)
>
> ________________________________
> dongbiao830415 AT foxmail.com
>
>
> From: Mike Stay
> Date: 2017-07-23 10:38
> To: dongbiao830415
> CC: k-user
> Subject: Re: [[K-user] ] Error while compiling lambda.k
> You defined the lambda-syntax module but not the lambda module.
>
> On Jul 22, 2017 5:49 PM, 
> "dongbiao830415 AT foxmail.com"
> <dongbiao830415 AT foxmail.com>
>  wrote:
>>
>>
>> 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



-- 
Mike Stay
CTO, Pyrofex Corp.