!MfVXcmpKuyudZHcqil:matrix.org

The K Framework User Group

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

Load older messages


SenderMessageTime
8 May 2024
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Transferring the link because the Matrix - Slack bridge didn't: > the nix code is here: https://github.com/eth-sc-comp/benchmarks/blob/e24a7182b317ea122dd75fcd91308a3dc3140596/flake.nix#L10 13:54:33
@xvwx:matrix.dapp.org.ukdxothanks everett <313:58:33
@_slack_runtimeverification_U02CDU166EL:matrix.orgbruce.collie Kup does do some additional caching (03BKBVPHT4?) but that should only be an optimisation rather than a correctness issue. I’ll take a look at the code and see if something obvious is wrong 14:04:33
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt I was thinking that perhaps the change in location of pyk repo and such could be causing issues? Because with kup it's using caches of the built expressions, but with nix flake directly it's reaching for the repositories themselves? 14:06:34
@_slack_runtimeverification_U03BKBVPHT4:matrix.orgsam.balco joined the room.14:13:34
@_slack_runtimeverification_U03BKBVPHT4:matrix.orgsam.balco It might well be that we keep that version in the k-framework-binary cachix cache but it fails to build from source because some external dependency we relied on is no longer available? 14:13:34
@_slack_runtimeverification_U03BKBVPHT4:matrix.orgsam.balco kup checks the binary cache first and just downloads the compiled versions of everything if there is ahit 14:15:57
@xvwx:matrix.dapp.org.ukdxoaha14:50:15
@xvwx:matrix.dapp.org.ukdxo I only had the k-framework binary cache 14:50:25
@xvwx:matrix.dapp.org.ukdxo Seems like adding k-framework-binary fixed the issues 14:50:46
@xvwx:matrix.dapp.org.ukdxodouble checking inside our docker container now14:50:54
@_slack_runtimeverification_U02CDU166EL:matrix.orgbruce.collie Interesting, seems unfortunate that kup can break like that even if this is a bit of an edge case! 15:18:17
@_slack_runtimeverification_U02CDU166EL:matrix.orgbruce.collie running nix build .#k --print-build-logs --option substitute false --rebuild at v6.1.77 of K to see if I can reproduce 15:18:31
@xvwx:matrix.dapp.org.ukdxo
In reply to @xvwx:matrix.dapp.org.uk
double checking inside our docker container now
yes confirmed that this was the issue
15:28:46
@xvwx:matrix.dapp.org.ukdxothank you for the help15:28:50
@xvwx:matrix.dapp.org.ukdxovery much appreciated <315:28:53
13 May 2024
@david:web3.foundationDavid | W3F changed their display name from David | W3F - OOO May 13 to David | W3F.06:31:59
24 May 2024
@rona06:matrix.orgna ro (rona) joined the room.22:06:52
28 May 2024
@hyperstructured.greg:matrix.orgGregory Makodzeba joined the room.03:16:14
3 Jun 2024
@david:web3.foundationDavid | W3F changed their display name from David | W3F to David | W3F - Slow responses until June 7.13:11:35
4 Jun 2024
@charmonium:matrix.org@charmonium:matrix.org left the room.13:59:44
7 Jun 2024
@david:web3.foundationDavid | W3F changed their display name from David | W3F - Slow responses until June 7 to David | W3F.09:34:20
28 Jun 2024
@david:web3.foundationDavid | W3F changed their display name from David | W3F to David | W3F - OOO (sick).06:20:09
1 Jul 2024
@david:web3.foundationDavid | W3F changed their display name from David | W3F - OOO (sick) to David | W3F.06:34:02
3 Jul 2024
@david:web3.foundationDavid | W3F changed their display name from David | W3F to David | W3F - OOO July 8.11:08:02
8 Jul 2024
@david:web3.foundationDavid | W3F changed their display name from David | W3F - OOO July 8 to David | W3F.06:49:49
20 Jul 2024
@snowflake100:matrix.orgsnowflake100 joined the room.00:26:54
@anony543:matrix.organony543 joined the room.02:17:09
@snowflake100:matrix.orgsnowflake100

Hi, I am new to the K framework and would like to understand better how to generate a compiler for a language with a formal semantics in K, such as is suggested by this diagram from https://runtimeverification.com/blog/k-framework-an-overview

Are there any good tutorials which cover generating a compiler? Or example repos?

Thanks.

02:38:36
@snowflake100:matrix.orgsnowflake100ima_a8f61ed.png
Download ima_a8f61ed.png
02:38:45

There are no newer messages yet.


Back to Room ListRoom Version: