K-user mailing list

[<daparpon AT dsic.upv.es>]

Hi, Xiaohong. Which environment variables should I set, exactly? I checked the
installation instructions and the only one that I found was the $PATH of the
system, which for usability is recommended to contain the path to <k-root>/
bin. In fact, that is the way I had it when using K 3.4 and K 3.6, and it
worked...

I also checked the "kernelc.k" file requirements (in <k-root>/samples/kernelc)
and I found some dependencies that do not exist within the K 4.0 distribution.
To be more precise, they are the following:

require "modules/verification_lemmas.k"
require "patterns/int_set.k"

What can I do to solve this dependencies and compile this (already provided)
language specification effectively?

Regards,
Daniel

________________________________________
From:
xc3 AT illinois.edu

[xc3 AT illinois.edu]
Sent: Friday, July 28, 2017 08:04 PM
To:
k-user AT lists.cs.illinois.edu
Subject: RE: [[K-user] ] Error when compiling sample Kernel-C specification

Hi Daniel,

Usually this error message shows up when there is a "requries file.k" in your
definition but "file.k" does not exist. Please double check that you setup
all environment variables correctly, especially LD_LIBRARY_PATH. If that does
not solve the problem, could you please provide more information specially so
that we can help nail down the problem?

Also we are improving this error message, too.

Thanks,
Xiaohong

-------------------------
Chen, Xiaohong
BSc, Peking University
PhD student, UIUC

________________________________________
From:
daparpon AT dsic.upv.es

[daparpon AT dsic.upv.es]
Sent: Thursday, July 27, 2017 5:31 AM
To:
k-user AT lists.cs.illinois.edu
Subject: [[K-user] ] Error when compiling sample Kernel-C specification

Hi! I am interested in trying out the K 4.0 verification infrastructure to
learn about how it works and how I can integrate it within my project.
However, when I try to compile the Kernel-C specification provided in k/
samples/kernelc, I get the following error message:

"[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";;

Following the suggestion, I ran kompile again with the --debug flag, and in
return I got the description below:

"java.util.NoSuchElementException: No value present
at java.util.Optional.get(Optional.java:135)
at
org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:152)
at
org.kframework.parser.concrete2kore.ParserUtils.slurp(ParserUtils.java:119)
at
org.kframework.parser.concrete2kore.ParserUtils.loadModules(ParserUtils.java:207)
at
org.kframework.parser.concrete2kore.ParserUtils.loadDefinition(ParserUtils.java:254)
at
org.kframework.kompile.DefinitionParsing.parseDefinition(DefinitionParsing.java:169)
at
org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:153)
at
org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:149)
at org.kframework.kompile.Kompile.parseDefinition(Kompile.java:140)
at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:54)
at org.kframework.main.FrontEnd.main(FrontEnd.java:34)
at org.kframework.main.Main.runApplication(Main.java:415)
at org.kframework.main.Main.runApplication(Main.java:131)
at org.kframework.main.Main.main(Main.java:73)"

In fact, this last exception message is printed twice. What can I do to solve
this problem and compile the specification?

Thanks in advance,
Daniel