[CakeML-dev] Dependencies

[Magnus Myreen]

Yes, compiler/backend/proofs currently depend on translator and
characteristic. This is caused by backendProofScript.sml using
evaluation in some proofs. The evaluation is done using compiler/eval,
which includes translator and characteristic. This dependency is a bit
unfortunate and somewhat unnecessary. We should try to split
compiler/eval into multiple files that we distribute through the
development.

I believe a quick fix is to comment out  ../../eval from the INCLUDES
line in the compiler/backend/proofs/Holmakefile. Such a change will
cause backendProof to fail, but I guess that doesn't matter for what
you are planning to work on.

Cheers,
Magnus

On 19 December 2016 at 03:59, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
> 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
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers