K-user mailing list

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

Hi, I was trying to follow the instructions:
cd /opt/k/uiuc
git clone https://github.com/kframework/k.git
cd k
git submodule update --init --recursive
sudo apt-get install build-essential m4 openjdk-8-jdk libgmp-dev 
libmpfr-dev pkg-config flex z3 libz3-dev maven opam python3 cmake 
clang-6.0 clang++-6.0 llvm-6.0 zlib1g-dev bison libboost-test-dev 
libyaml-cpp-dev libjemalloc-dev
curl https://sh.rustup.rs -sSf | sh
source $HOME/.cargo/env
rustup toolchain install 1.28.0
rustup default 1.28.0
curl -sSL https://get.haskellstack.org/ | sh
# mvn package

The following did work, as you suggested:
mvn package -Dllvm.backend.skip

Finished it with:
export K_HOME=/opt/k/uiuc/k
export PATH="${K_HOME}/k-distribution/bin:${PATH}"
export MAVEN_OPTS="-XX:+TieredCompilation"
${K_HOME}/k-distribution/target/release/k/bin/k-configure-opam
eval `opam config env`


Now I tried going into tutorial/1_k/2_imp/lesson_1 to try out imp:
$ kompile imp.k
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by 
com.google.inject.internal.cglib.core.$ReflectUtils$2 
(file:/opt/k/uiuc/k/k-distribution/target/release/k/lib/java/guice-4.0-beta5.jar) 
to method 
java.lang.ClassLoader.defineClass(java.lang.String,byte[],int,int,java.security.ProtectionDomain)
WARNING: Please consider reporting this to the maintainers of 
com.google.inject.internal.cglib.core.$ReflectUtils$2
WARNING: Use --illegal-access=warn to enable warnings of further illegal 
reflective access operations
WARNING: All illegal access operations will be denied in a future release
40 states, 1247 transitions, table size 5228 bytes
$ echo $?
0
$ krun tests/sum.imp
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by 
com.google.inject.internal.cglib.core.$ReflectUtils$2 
(file:/opt/k/uiuc/k/k-distribution/target/release/k/lib/java/guice-4.0-beta5.jar) 
to method 
java.lang.ClassLoader.defineClass(java.lang.String,byte[],int,int,java.security.ProtectionDomain)
WARNING: Please consider reporting this to the maintainers of 
com.google.inject.internal.cglib.core.$ReflectUtils$2
WARNING: Use --illegal-access=warn to enable warnings of further illegal 
reflective access operations
WARNING: All illegal access operations will be denied in a future release
<k>
  int n , sum , .Ids ; n = 100 ; sum = 0 ; while ( ! n <= 0 ) { sum = 
sum + n ; n = n + - 1 ; }
</k>
$ echo $?
0
$

That's not the output I expected - looks like it got stuck in the 
variable declarations. :-(
Not sure about the warnings from com.google.inject.internal.cglib.core 
either but I can live with them.

I actually wanted to try out sum-spec from lesson 8. When I try that I get:
$ ln -s ../../4_imp++/lesson_8/tests/sum-spec.k
$ krun -prove sum-spec.k
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by 
com.google.inject.internal.cglib.core.$ReflectUtils$2 
(file:/opt/k/uiuc/k/k-distribution/target/release/k/lib/java/guice-4.0-beta5.jar) 
to method 
java.lang.ClassLoader.defineClass(java.lang.String,byte[],int,int,java.security.ProtectionDomain)
WARNING: Please consider reporting this to the maintainers of 
com.google.inject.internal.cglib.core.$ReflectUtils$2
WARNING: Use --illegal-access=warn to enable warnings of further illegal 
reflective access operations
WARNING: All illegal access operations will be denied in a future release
[Error] Critical: Dynamic parameter expected a value of the form a=b but
got:rove (Dynamic parameter expected a value of the form a=b but got:rove)
$ echo $?
1
$

Any hints/pointers?

Best,
Chris

On 23/01/2019 18:09, Dwight Guth wrote:
> You need to follow the instructions in INSTALL.md in the root of the 
> repository if you want it to work out of the box. Alternatively, since 
> the LLVM backend is not completely ready yet for production usage, you 
> can just pass `-Dllvm.backend.skip` to `mvn package`.
>
> I would not recommend using github.com/kframework/k-legacy 
> <http://github.com/kframework/k-legacy> as it is completely 
> unsupported and probably full of bugs that will never be fixed.
>
> On Wed, Jan 23, 2019 at 11:09 AM Christos Kloukinas 
> <c.kloukinas AT gmail.com <mailto:c.kloukinas AT gmail.com>> wrote:
>
>     Hi, I'm trying to install K from github.
>
>
>     I've tried both the UIUC & the RV versions:
>
>     https://github.com/kframework/k
>
>     https://github.com/runtimeverification/k
>
>
>     For both I've followed the instructions on UIUC but when I try "mvn
>     package" everything builds fine apart from LLVM Backend.
>
>     The errors are mostly the same in both versions - the common files
>     that
>     are involved are:
>
>     - llvm-backend/src/main/native/llvm-backend/runtime/alloc/alloc.c
>
>     - llvm-backend/src/main/native/llvm-backend/runtime/alloc/collect.c
>
>     - llvm-backend/src/main/native/llvm-backend/include/runtime/header.h
>
>     -
>     llvm-backend/src/main/native/llvm-backend/runtime/strings/strings.cpp
>
>     UIUC also has an issue with:
>
>     -
>     
> llvm-backend/src/main/native/llvm-backend/matching/submodules/kore/src/main/haskell/kore/src/Kore/SMT/SMT.hs
>
>
>     I'm attaching the output of mvn package from LLVM down.
>
>
>     Anyone has an idea how I could proceed here?
>
>
>     Best,
>
>     Chris
>
>
>
>
>
>
> --
>
> Dwight Guth
>
> Director of Engineering
>
>
> Email: dwight.guth AT runtimeverification.com 
> <mailto:dwight.guth AT runtimeverification.com>
>
>
> <https://www.runtimeverification.com>
>
>
> <https://github.com/dwightguth><https://www.linkedin.com/company/3142238/><https://twitter.com/rv_inc>