<div dir="ltr">I am fixing the translation on CakeML 314a5e6 and HOL 572ce3d<div><br></div><div>Those work fine with the (old?) parsing scripts.</div><div><br></div><div>It would be helpful if you had a look at ml_progLib on env-refactor since I might have also inadvertently slowed it down by expanding things incorrectly.</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Feb 15, 2017 at 6:53 AM, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Yes unfortunately the parser is still broken because of location<br>
information. I think Michael and maybe Hugo are working on it (Michael<br>
fixed cmlPtreeConversion today, but not the Props yet apparently).<br>
<div class="HOEnZb"><div class="h5"><br>
On 15 February 2017 at 22:43, Magnus Myreen <<a href="mailto:magnus.myreen@gmail.com">magnus.myreen@gmail.com</a>> wrote:<br>
> I'm on that commit and I seem to get the following error while<br>
> building dependencies of the translator. -- Magnus<br>
><br>
> Holmake: Linking cmlPtreeConversionPropsScript.<wbr>uo to produce<br>
> theory-builder executable<br>
> <<HOL message: Created theory "cmlPtreeConversionProps">><br>
> error in quse /Users/mom22/cakeml-env/<wbr>semantics/proofs/<wbr>cmlPtreeConversionPropsScript.<wbr>sml<br>
> : HOL_ERR {message = "No consistent parse", origin_function =<br>
> "typed_parse_in_context", origin_structure = "Parse"}<br>
> error in load cmlPtreeConversionPropsScript : HOL_ERR {message = "No<br>
> consistent parse", origin_function = "typed_parse_in_context",<br>
> origin_structure = "Parse"}<br>
> Holmake: Failed script build for cmlPtreeConversionPropsScript -<br>
> exited with code 1<br>
> Holmake: Finished recursive invocation in ../semantics/proofs<br>
> Holmake: Finished recursive invocation in ../semantics/alt_semantics/<wbr>proofs<br>
><br>
> On 15 February 2017 at 12:15, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk">Ramana.Kumar@cl.cam.ac.uk</a>> wrote:<br>
>> I think it's c59c4caf4<br>
>><br>
>> On 15 February 2017 at 18:04, Magnus Myreen <<a href="mailto:magnus.myreen@gmail.com">magnus.myreen@gmail.com</a>> wrote:<br>
>>> Hi all,<br>
>>><br>
>>> What is the correct HOL commit for building env-refactor?<br>
>>><br>
>>> I'm asking because I hope to try to speed up ml_progLib, which is<br>
>>> making the bootstrap translation ridiculously slow at the moment (on<br>
>>> master). The improvement is best done on env-refactor because that<br>
>>> branch will soon be merged into master (I hope).<br>
>>><br>
>>> Cheers,<br>
>>> Magnus<br>
>>><br>
>>> ______________________________<wbr>_________________<br>
>>> Developers mailing list<br>
>>> <a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
>>> <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
<br>
______________________________<wbr>_________________<br>
Developers mailing list<br>
<a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
</div></div></blockquote></div><br></div>