Integrate Tej's simp-lang?
@tchajed has created https://github.com/tchajed/iris-simp-lang, which is a simple "demo language" to show how to use the Iris language interface. It even comes with an accompanying Youtube video! I took a look and watched the video, and I really like it.
I propose we give this more visibility by referencing it from the Iris repo and website, and also we should find some way to ensure that the Coq code remains compatible with latest Iris. The easiest way to do that would be to add an "iris_simp_lang" package in this repository and move the code there. The README could go into the subfolder. @tchajed would that work for you, or did you have other plans? I don't want to appropriate your work, just ensure that it does not bitrot. I could imagine declaring you the maintainer of that subdirectory, so you could e.g. merge MRs for it yourself. @robbertkrebbers what do you think?
I also have some more specific low-level comments, which I leave here just so I do not forget -- but it probably make more sense to discuss the high-level points first. It's really just one remark so far:
- In
heap_ra
, I find it confusing that you end up basically copying (parts of)gen_heap
. IMO it would make more sense to either usegen_heap
, or else (for the purpose of exposition) to define something that specifically works for values and locations of this language, but then it should not be called "gen(eral)".