K-user mailing list

[Christos Kloukinas <c.kloukinas AT gmail.com>]

Hi Daniel,

following the instructions on installing K from the git repository I had 
created a small script for me that tries to set up the appropriate 
variables.

I've tested it only for Mac OS (Darwin), so it may be wrong for 
Linux/Windows - please double-check.


I imagine that some of these variables will need to be set inside your 
.bashrc (or equivalent) too.


Best,

Christos


On 31/07/2017 10:48, 
daparpon AT dsic.upv.es
 wrote:
> 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

#! /bin/sh -

KHOME=${HOME}/lib/k-git/
KRELEASE=${KHOME}/k/k-distribution/target/release/k
KPATH=${KRELEASE}/bin
UNAME=`uname`
if [ z${UNAME}z = zDarwinz ] ; then
        # Mac OS X: PATH=$PATH:${KRELEASE}/lib/native/osx 
DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH:${KRELEASE}/lib/native/osx 
        KPATH=${KPATH}:${KRELEASE}/lib/native/osx
        DYLD_LIBRARY_PATH=${DYLD_LIBRARY_PATH}:${KRELEASE}/lib/native/osx
elif [ z${UNAME}z = zLinuxz ] ; then
        # Linux i386: 
PATH=$PATH:${KRELEASE}/lib/native/linux:${KRELEASE}/lib/native/linux32 
LD_LIBRARY_PATH=$LD_LIBRARY_PATH:${KRELEASE}/lib/native/linux32 
        # Linux amd64: 
PATH=$PATH:${KRELEASE}/lib/native/linux:${KRELEASE}/lib/native/linux64 
LD_LIBRARY_PATH=$LD_LIBRARY_PATH:${KRELEASE}/lib/native/linux64
        
KPATH=${KPATH}:${KRELEASE}/lib/native/linux:${KRELEASE}/lib/native/linux32
        LD_LIBRARY_PATH=${LD_LIBRARY_PATH}:${KRELEASE}/lib/native/linux64
fi
PATH=${KPATH}:${PATH}


# Windows x86: 
PATH=$PATH;${KRELEASE}/lib\native\windows;${KRELEASE}/lib\native\windows32 
# Windows x64: 
PATH=$PATH;${KRELEASE}/lib\native\windows;${KRELEASE}/lib\native\windows64 
# Linux amd64: 
PATH=$PATH:${KRELEASE}/lib/native/linux:${KRELEASE}/lib/native/linux64 
LD_LIBRARY_PATH=$LD_LIBRARY_PATH:${KRELEASE}/lib/native/linux64


test -d ${KHOME} || mkdir -p ${KHOME}

cd ${KHOME} \
&& git clone https://github.com/kframework/k.git \
|| (cd ${KHOME}/k && git pull origin master)

cd ${KHOME}/k

mvn package