[CakeML-dev] Dependencies

[Scott Owens]

I’m trying to work on source_to_modProof in compiler/backend/proofs on the env-refactor branch. However, doing a Holmake in that directory leads to a failure in building ml_progTheory. Why does the compiler backend depend on the translator? Should it? What can I do to work around the failure for now?

I don’t want to maintain the translator on env-refactor while it is being worked on separately, but I would like to get source_to_mod and mod_to_con working.

Scott