build bedrock2 semantics separately from the compiler about bedrock2 HOT 7 CLOSED

I agree! I think a separate makefile target is the way to go, I'll give it a shot this morning.

from bedrock2.

Ok so I did a bit of refactoring and added a Makefile target called ExprImp, so now you should be able to do what I just added to the REAMDE:

To build only the source language (ExprImp):

• run make in the bbv directory
• run make util in the riscv-coq directory
• run make ExprImp in the bedrock2 directory

Please let me know if it works (or if I screwed something up 😉).

from bedrock2.

from bedrock2.

Both ExprImp and riscv-coq need some general utility stuff such as monads and a bitwidth typeclass, and I don't want to duplicate this utility code. Currently, this utility code lives in riscv-coq/src/util. I could move it into a separate repo, but I don't think this would add any value.

from bedrock2.

I tried factoring the semantics out further. Please review https://github.com/mit-plv/bedrock2/compare/semantics-refactor for style and not semantics and give me feedback on whether you think this is a good direction.

from bedrock2.

(Stalled on coq/coq#7892, thinking about how to proceed.)

from bedrock2.

This works now.

from bedrock2.