!MfVXcmpKuyudZHcqil:matrix.org

The K Framework User Group

221 Members
The K Framework (kframework.org) and its applications to smart contracts.  EVM: github.com/kframework/evm-semantics Viper: github.com/kframework/viper-semantics47 Servers

Load older messages


SenderMessageTime
25 Aug 2020
@akigyosi:matrix.orgakigyosi joined the room.12:35:40
26 Aug 2020
@akigyosi:matrix.orgakigyosi

Hello. I am trying to build the k framework on Fedora 32 and I get the following error:

[INFO] Reactor Summary for K Framework Tool Parent 1.0-SNAPSHOT:
[INFO]
[INFO] K Framework Tool Parent ............................ SUCCESS [ 0.220 s]
[INFO] K Framework KORE ................................... SUCCESS [ 16.781 s]
[INFO] K Framework Tool Kernel ............................ SUCCESS [ 14.177 s]
[INFO] K Framework KTree .................................. SUCCESS [ 0.077 s]
[INFO] K Framework Ocaml Backend .......................... SUCCESS [ 0.289 s]
[INFO] K Framework Java Backend ........................... SUCCESS [ 2.691 s]
[INFO] K Framework Haskell Backend ........................ FAILURE [ 0.893 s]
[INFO] K Framework LLVM Backend Pattern Matching .......... SKIPPED
[INFO] K Framework LLVM Backend ........................... SKIPPED
[INFO] K Framework Tool Distribution ...................... SKIPPED
[INFO] ------------------------------------------------------------------------
[INFO] BUILD FAILURE
[INFO] ------------------------------------------------------------------------
[INFO] Total time: 35.638 s
[INFO] Finished at: 2020-08-26T23:42:05+03:00
[INFO] ------------------------------------------------------------------------
[ERROR] Failed to execute goal org.apache.maven.plugins:maven-antrun-plugin:1.7:run (build-haskell) on project haskell-backend: An Ant BuildException has occured: exec returned: 1
[ERROR] around Ant part ...<exec failonerror="true" dir="/home/alex/WORK/k/haskell-backend/src/main/native/haskell-backend" executable="stack">... @ 4:119 in /home/alex/WORK/k/haskell-backend/target/antrun/build-main.xml

I followed the instructions on the github page. I don't know what else to do.

20:45:21
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt @akigyosi, you likely need to install Haskell Stack program. Can you do stack --version and post the output? 22:13:24
27 Aug 2020
@akigyosi:matrix.orgakigyosi[alex@localhost ~]$ stack --version Version 2.3.3, Git revision cb44d51bed48b723a5deb08c3348c0b3ccfc437e x86_64 hpack-0.33.009:52:28
@akigyosi:matrix.orgakigyosi I have installed it from their website (like it says in the instructions) and then reinstalled using your script install-stack.sh. I tried both ways. After installation, I did stack upgrade 09:56:36
@akigyosi:matrix.orgakigyosiI've managed to build kore, after installing ncurses-dev, but I still can't build the K framework.12:46:44
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt We will need the error message you get to be posted. 13:58:26
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Likely the relevant output is not the last bit **[ERROR] Failed to execute... 13:58:43
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt It should come above all that, where it has a bunch of [INFO] or [EXEC] before it, and it will have a more specific error message there. 13:59:53
@franklinchen:matrix.orgfranklinchen joined the room.20:08:20
2 Sep 2020
@sorpaas:matrix.parity.ioWei Tang changed their display name from Wei Tang to Wei Tang (back next Mon!).00:05:26
@akigyosi:matrix.orgakigyosiI got a successful build. I had to find the equivalent packages for Fedora and reinstall them. I also installed some additional packages which I thought might help. Thanks for the support.18:00:05
5 Sep 2020
@babelkushal:matrix.orgbabelkushalHi, is there a way I can direct kprove to only explore certain paths for all-path-reachability (eg. path 10 - path 25)? My semantics has a lot of non-deterministic branches, and I'm thinking of running different kprove instances on different machines with this directive to effectively parallelise the job. Ofcourse kprove would have to have a canonical ordering of paths for this to work. Any help is appreciated!02:11:40
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Well, a simple way is to "guide" your non-determinism. You can do this by having an extra cell which contains a flag which tells it which branches to take (so you add that cell to each non-deterministic rule, and then a rule can only fire if the flag is set correctly for it). Then you can split the kprove claim into a bunch of separate claims, each one which provides a different variant of the flag on the LHS of the claim. Example (in semantics):
rule  k  a => b ...  /k   flag  X  /flag  requires 10 <=Int X andBool X  k a => c ...  /k   flag  X  /flag  requires 10 <=Int X andBool X  k a => d ...  /k   flag  X  /flag  requires 20 <=Int X andBool X  
And the proof, you can enable just the first two rules:

rule  k  a => ?_ ...  /k   flag  15  /flag 
02:45:42
@babelkushal:matrix.orgbabelkushalHm, changing semantics was my last resort, but this modification is clean, so I'll try this. Thanks! Although, I think that it might not be very straightforward, since I have rules like <k> ... SetItem(X) ... => Y </k> for having a non deterministic re-ordering, and its not immediately clear how do I fire orderings based on flag values.03:40:51
@babelkushal:matrix.orgbabelkushal

Hi, I am checking some reachability claims through kprove, of the following form:
rule <k> SOME_PROGRAM => ?X </k>
<S> .Set => ?Y </S>
ensures SOME_CONDITION_ON_S
Now, I am wondering how do I modify the claim to only check for reachability of SOME_CONDITION_ON_S only on paths when SOME_PROGRAM is completely executed and is not stuck midway?
Now, I could modify the semantics so that the program is rewritten to FAIL when its stuck, and then have a claim:
ensures SOME_CONDITION_ON_S orBool (?X ==k FAIL) , but I am reluctant to go this route because that would introduce a lot of new semantic rules.

On the same theme, bumping this question from a few weeks ago. Any help is appreciated!

03:42:43
@babelkushal:matrix.orgbabelkushal * Hm, changing semantics was my last resort, but this modification is clean, so I'll try this. Thanks! Although, I think that is might not be very straightforward, since I have rules like <k> ... SetItem(X) ... => Y </k> for having a non deterministic re-ordering, and its not immediately clear how do I fire orderings based on flag values.03:47:32
@babelkushal:matrix.orgbabelkushal * Hm, changing semantics was my last resort, but this modification is clean, so I'll try this. Thanks! Although, I think that it might not be very straightforward, since I have rules like <k> ... SetItem(X) ... => Y </k> for having a non deterministic re-ordering, and its not immediately clear how do I fire orderings based on flag values.03:48:07
7 Sep 2020
@sorpaas:matrix.parity.ioWei Tang changed their display name from Wei Tang (back next Mon!) to Wei Tang.06:26:11
12 Sep 2020
@xameer:matrix.org@xameer:matrix.org left the room.15:30:22
17 Sep 2020
@peter:chat.weho.stpeter 20:10:29
14 Sep 2020
@gkobeaga:matrix.org@gkobeaga:matrix.org left the room.21:54:14
16 Sep 2020
@thorsten:synod.im@thorsten:synod.im left the room.23:56:55
21 Sep 2020
@sorpaas:matrix.parity.ioWei Tang changed their display name from Wei Tang to Wei Tang (ooo Tue).18:06:00
22 Sep 2020
@sorpaas:matrix.parity.ioWei Tang changed their display name from Wei Tang (ooo Tue) to Wei Tang.19:22:06
@sorpaas:matrix.parity.ioWei Tang changed their display name from Wei Tang to Wei Tang -- ooo this week, sorry :(.23:22:13
23 Sep 2020
@david:web3.foundationDavid (ooo until Oct 2) changed their display name from David to David (ooo until Oct 2).17:08:17
25 Sep 2020
@indolering:matrix.orgindolering joined the room.20:18:45
26 Sep 2020
@peter:perthchat.orgpeter joined the room.14:23:54
27 Sep 2020
@sorpaas:matrix.parity.ioWei Tang changed their display name from Wei Tang -- ooo this week, sorry :( to Wei Tang.20:34:28

There are no newer messages yet.


Back to Room List