[CakeML-dev] Building the env-refactor branch

[Magnus Myreen]

I'm on that commit and I seem to get the following error while
building dependencies of the translator. -- Magnus

Holmake: Linking cmlPtreeConversionPropsScript.uo to produce
theory-builder executable
<<HOL message: Created theory "cmlPtreeConversionProps">>
error in quse /Users/mom22/cakeml-env/semantics/proofs/cmlPtreeConversionPropsScript.sml
: HOL_ERR {message = "No consistent parse", origin_function =
"typed_parse_in_context", origin_structure = "Parse"}
error in load cmlPtreeConversionPropsScript : HOL_ERR {message = "No
consistent parse", origin_function = "typed_parse_in_context",
origin_structure = "Parse"}
Holmake: Failed script build for cmlPtreeConversionPropsScript -
exited with code 1
Holmake: Finished recursive invocation in ../semantics/proofs
Holmake: Finished recursive invocation in ../semantics/alt_semantics/proofs

On 15 February 2017 at 12:15, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> I think it's c59c4caf4
>
> On 15 February 2017 at 18:04, Magnus Myreen <magnus.myreen at gmail.com> wrote:
>> Hi all,
>>
>> What is the correct HOL commit for building env-refactor?
>>
>> I'm asking because I hope to try to speed up ml_progLib, which is
>> making the bootstrap translation ridiculously slow at the moment (on
>> master). The improvement is best done on env-refactor because that
>> branch will soon be merged into master (I hope).
>>
>> Cheers,
>> Magnus
>>
>> _______________________________________________
>> Developers mailing list
>> Developers at cakeml.org
>> https://lists.cakeml.org/listinfo/developers