|7 Feb 2019|
|18:28:00||dwight.guth|| an alias even if you want |
|18:28:09||everett.hildenbrandt|| a macro was the next thing I was going to try for |
|18:28:52||dwight.guth|| my advice would be to have one production per complete opcode and use a rule like |
rule i32.extend_i64 => extend(i32, i64) [alias]
|18:29:05||dwight.guth|| and then you just write extend(i32, 64) in the rules in the semantics |
|18:29:28||dwight.guth|| that way the underscore is never a terminal in the grammar and you also get correct rules regarding layout |
|18:30:04||everett.hildenbrandt|| That's basically what we do now, but then we can't take advantage of two different pieces of common machinery used throughout the sematics (1) rules which unfold folded WASM into unfolded WASM, and (2) rules which type-check the arguments. |
|18:31:05||everett.hildenbrandt|| I think I can figure out a middle ground though, will take some tinkering. |
|18:31:38||dwight.guth|| hmmm? |
|18:31:55||dwight.guth|| sorry I don't understand how this approach is any different from what you're asking for except in syntax |
|18:32:09||dwight.guth|| it should be doable with exactly one extra rule per opcode and no other changes in the complexity of the semantics |
|18:33:02||everett.hildenbrandt|| We have common machinery which loads, typechecks, and unfolds opcodes (all wasm specific things). That machinery depends on things being in the general form of |
"(" TARGET_TYPE "." OPCODE_NAME ")"
|18:33:24||dwight.guth|| ah |
|18:33:33||dwight.guth|| well |
|18:33:40||dwight.guth|| in that case |
|18:33:51||dwight.guth|| you can just make the OPCODE_NAME be |
syntax OpCode ::= "extend_i64"
|18:34:06||dwight.guth|| the exact same process applies it's just that the alias only has one argument instead of two |
|18:35:36||everett.hildenbrandt|| It almost works, but not quite (was my first attempt). Actually because of another issue in the type-checking which I need to discuss with FTN1UV4H before moving forward with a fix. |
|18:36:17||dwight.guth|| well, regardless, it sounds like you have a path forward and you shouldn't really need "_" to be a terminal in your grammar |
|18:36:46||dwight.guth|| I agree that being able to support this would be good, but it's not going to happen anytime soon and your grammar will also be more accurate if you do it this way |
|13 Feb 2019|
|09:18:54||tkazana-eth joined the room.|
|14 Feb 2019|
|12:45:35||grigore.rosu|| @room Question for people interested in K. Any ideas what we can all do to make this happen? https://ethereum-magicians.org/t/jello-paper-as-canonical-evm-spec/2389
Basically to make KEVM into the cannonical EVM specification. |
|14:15:12||everett.hildenbrandt|| I think just continue to maintain KEVM and keep it up to date. There isn't someone who feels they have the authority to "make the switch", but since no one is really putting time into the yellow paper, and we're putting time into KEVM, I think it will be maintained for longer |
|14:32:14||grigore.rosu|| I think allowing an alternative syntax for configurations, something like in eDSL (e.g., |
k: stuff instead of
k stuff /k ) can also help.
And also when we get a chance to resurrect the Latex generator. All language frameworks have something similar: OTT, Spoofax.
|14:39:50||everett.hildenbrandt|| We can make a to-do for the latex generator. I think it would take about 2 days to have an MVP, and another week to polish. |
|14:40:02||everett.hildenbrandt|| I don't have the bandwidth at the moment, but can add it to my list. |
|14:52:48||grigore.rosu|| 8T2RJ802 thanks! WRT latex generator, we had two different styles: one with bubbles and one with angle barackets. We can start by revising those. The one with bubbles can be seen in this paper: http://fsl.cs.illinois.edu/FSL/papers/2013/rosu-serbanuta-2013-k/rosu-serbanuta-2013-k-public.pdf. The one with angle brackets is, for example, here: http://fsl.cs.illinois.edu/FSL/papers/2015/hathhorn-ellison-rosu-2015-pldi/hathhorn-ellison-rosu-2015-pldi-public.pdf. There were people who really hated the bubble notation and people who loved it, and people who really hated the angle notation and people who really liked it. I believe 7XNEMJHL implemented his own style, in the spirit of the angle notation; can you show us, 7XNEMJHL? 5FRLGXJ9 came up with a nice idea, to have a |
k.sty file with macros for all the K cells and constructs, and then get one or the other style by simply importing some different macro file (but the K latex generator was independent and unique). Anyway, we should probably discuss the details in other channels. Any other ideas what we can do to increase adoption?
|15:02:35||denis.bogdanas|| My style was angle brackets, but I extended it to support long rules. I extended k.sty so that brackets could have upt to 5 lines I think, and added a lot of line wraps. |
|15:03:49||grigore.rosu|| 7XNEMJHL can you send us a link to your PDF showing your notation at work? I think your PhD thesis? |
|15:05:27||denis.bogdanas|| Look at the appendix: https://fmse.info.uaic.ro/publication/a-complete-semantics-of-java/ |
|15:09:06||grigore.rosu|| 7XNEMJHL impressive that you managed to fit the entire configuration of Java on less than one page (page 116). Are you OK if I put a link to your thesis on the web, where people discuss the K notation? |