K-user mailing list

[Dwight Guth <dwight.guth AT runtimeverification.com>]

as for imp, you have gotten the correct behavior; however, lesson_1 is only a partial definition (the lessons in the k tutorial generally start from a partial definitiion and gradually add features in each lesson). If you just want a definition of imp to play around with, use lesson_5.

On Wed, Jan 23, 2019 at 1:14 PM Dwight Guth <dwight.guth AT runtimeverification.com> wrote:

You can ignore those warnings, I've been meaning to fix it but haven't had time yet as it doesn't break anything. As for the prover, the prover now has its own command line command: `kprove sum-spec.k`.

 You will need to kompile with `--backend java` for it to work though.

On Wed, Jan 23, 2019 at 1:05 PM Christos Kloukinas <c.kloukinas AT gmail.com> wrote:

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>
>
>
>
>
>

--

Dwight Guth

Director of Engineering

Email: dwight.guth AT runtimeverification.com

 

--

Dwight Guth

Director of Engineering

Email: dwight.guth AT runtimeverification.com