| 2 Sep 2019 |
| 14:34:10 |  everett.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 | Who would be the person to talk to about publishing the emacs mode to MELPA? Michael Ileman is listed as the author |
| 11:26:47 |  rikard.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 | everett.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 | everett.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 | everett.hildenbrandt | rikard.hjort it is possible to do that, nishantjr would know exactly how I think. |
| 14:20:40 |  nishantjr | 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 | rikard.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 |  brandon.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 | 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 | everett.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 | everett.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 | 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 | nishantjr | 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 | let me know if any of the content seems worthwhile to merge and I can do so |
| 19:17:38 | salotz | also 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 | everett.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 | everett.hildenbrandt | So maybe we should group those riot rooms together on that end, and allow creating more rooms. |
| 19:28:02 | salotz | okay 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 | nishantjr: In your examples are you using pandoc to tangle the code blocks or your own parser in the build script? |
| 19:32:35 | nishantjr | pandoc and pandoc-table. I use pyyaml to parse the headers. You can install that via pip |
| 19:41:09 | salotz | ok 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 | nishantjr | @salotz Everett actually wrote a pandoc plugin for that functionality. |
| 9 Sep 2019 |
| 16:37:56 | rikard.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 |  dwight.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 | dwight.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 | dwight.guth | You also run the tests before running kcovr |
| 10 Sep 2019 |
| 02:35:48 |  daejun.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 | rikard.hjort | Great, thanks |
| 17 Sep 2019 |
| 22:48:11 | |  norman joined the room. |
