The K Framework User Group

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

Load older messages

Timestamp Message
2 Sep 2019
14:34:10@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt My guess is the problem is that K only builds one lexer for the entire definition, even though it builds a separate parser for each module. So your token is being added to the lexer which is also used for domains.k, for example.
3 Sep 2019
05:39:46@salotz:matrix.orgsalotzWho would be the person to talk to about publishing the emacs mode to MELPA? Michael Ileman is listed as the author
11:26:47@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort Is it possible to invoke the parser on a String and get a K back? Something like an eval function? I'm being passed programs as strings within my program.
13:51:14@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt @salotz Michael Ileman isn't associated with RV or K AFAIK right now. He may have been a student at the university before who wrote it or something.
13:51:53@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Not sure anyone here will handle getting it published, I don't personally use emacs, not sure who on the team does. daejun.park? or rikard.hjort?
13:53:10@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt rikard.hjort it is possible to do that, nishantjr would know exactly how I think.
14:20:40@_slack_runtimeverification_U99TYNSG3:matrix.orgnishantjr rikard.hjort take a look at the rules implementing the import statement in "PROVER-DRIVER". It relies on #parseKAST which has only been implemented in the java and ocaml backend. I think Dwight would accept a corresponding #parseKORE for the LLVM and Haskell backends. https://github.com/kframework/matching-logic-prover/blob/master/prover/prover.md
15:32:52@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort thanks! I just realized that I will in fact not need it: all the cases where it is used are just to show that a parser should reject that string, so I don't think it's interesting for us.
17:12:52@_slack_runtimeverification_U5GEX1LJ3:matrix.orgbrandon.moore martin For tokens like that to work, you need to make sure the actual regex production is only imported into to syntax module (usually LANGUAGE-SYNTAX), but not into the main semantics module. You should also make sure the sort itself is introduced in a common module that's imported into both, either with productions for unproblematic syntax a pure declaration like syntax YULString.
18:58:38@salotz:matrix.orgsalotz everett.hildenbrandt: I know how to do it I kind of just wanted to get the blessing of someone on the K team to do it. I started a standalone repo to work on it in a more focused manner without having to PR the main K framework repo. There is also no lock-in from me doing it so its pretty low risk
19:02:10@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt @salotz I think you can feel free to publish it if you like, but I would also prefer that you upstream the contribution into our k-editor-support repository as well. Also, I notice that you're starting a community documentation repo (https://github.com/salotz/kay.community_docs), maybe you want to collaborate with nishantjr on his community documentation repo as well, you both seem to be trying to gather examples of K for "learning by example".
19:03:13@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt I would also appreciate if those examples were upstreamed into kframework/k under the file pending-documentation.md, which is where we're trying to dump all the "bespoke" knowledge about about K which you will only get by coming to this forum. Examples are always helpful in that document, we're trying to gather the content that would make for a K manual.
19:06:14@salotz:matrix.orgsalotz everett.hildenbrandt yes I am, I don't really know if that will go anywhere (and its a little bit of a testbed for me learning other things too) as I am new to the whole semantics and PLs in general. Best case would something like the clojure community docs, and sure I would be grateful to see what @nishantjr has going. I basically was looking at this repo by a guy in the RChain project https://github.com/Isaac-DeFrain/KFramework FYI
19:08:53@_slack_runtimeverification_U99TYNSG3:matrix.orgnishantjr Ive just got a couple of pages going. The idea is to have tests for all documentation that runs across all backends https://github.com/nishantjr/k-play https://raw.githubusercontent.com/nishantjr/k-play/master/conversions.md
19:09:40@salotz:matrix.orgsalotzlet me know if any of the content seems worthwhile to merge and I can do so
19:17:38@salotz:matrix.orgsalotzalso not sure how the mods think about splitting off some topic specific rooms. I don't want to pollute the dev chat. Could also split off to a community run chat room if there is interest
19:18:38@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Well, from our perspective, this is just one slack room of many internal to Runtime Verification, Inc. We have a handful of the channels bridged to corresponding riot channels, though those channels are not under a common riot org.
19:18:59@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt So maybe we should group those riot rooms together on that end, and allow creating more rooms.
19:28:02@salotz:matrix.orgsalotzokay I see, well I also don't want to start adding stuff to your todo list. Since this is the one that is visible to the potential enthusiast, I'll just try to gauge if there is any interest in a community organized one and leave you guys to your work. If anything comes of it later you can make a link to it somewhere on the other pages. In the meantime I will assume that chat here isn't spamming dev chat 🙂
19:29:32@salotz:matrix.orgsalotz nishantjr: In your examples are you using pandoc to tangle the code blocks or your own parser in the build script?
19:32:35@_slack_runtimeverification_U99TYNSG3:matrix.orgnishantjr pandoc and pandoc-table. I use pyyaml to parse the headers. You can install that via pip
19:41:09@salotz:matrix.orgsalotzok interesting wasn't aware of a pandoc tangle functionality. I usually write my stuff in emacs org-mode which works really well for this kind of stuff too
21:07:55@_slack_runtimeverification_U99TYNSG3:matrix.orgnishantjr @salotz Everett actually wrote a pandoc plugin for that functionality.
9 Sep 2019
16:37:56@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort daejun.park In the KJS paper (PLDI15), you describe that you managed to check how many rules of your semantics were exercised by the official test suite. How did you do that?
18:11:23@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth rikard.hjort I'm not sure how they did it but the recommended way to measure coverage of a semantics is to kompile it with the --coverage flag and then run kcovr $kompiled_dir -- $k_files > coverage.xml and then feed it into a tool that understands cobertura style xml reports
18:11:55@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth This will generate a coverage report where you can view each file and rules that are covered will be colored green
18:12:32@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth You also run the tests before running kcovr
10 Sep 2019
02:35:48@_slack_runtimeverification_U7M49CGSD:matrix.orgdaejun.park rikard.hjort I measured it in an ad-hoc way that does not work any longer, and I agree that you are better to use what dwight.guth suggested.
09:35:55@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort Great, thanks
17 Sep 2019
22:48:11@norman:utwente.ionorman joined the room.

There are no newer messages yet.

Back to Room List