S.A.Owens at kent.ac.uk
Sun Dec 18 16:59:52 UTC 2016
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.
More information about the Developers