<div dir="ltr">That's fine for me, I'm going to update CakeML+HOL only when I've finished the translation directory (now getting stuck for non-pmatch reasons).<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Feb 15, 2017 at 9:49 AM, Magnus Myreen <span dir="ltr"><<a href="mailto:magnus.myreen@gmail.com" target="_blank">magnus.myreen@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 15 February 2017 at 14:57, Magnus Myreen <<a href="mailto:magnus.myreen@gmail.com">magnus.myreen@gmail.com</a>> wrote:<br>
> On 15 February 2017 at 14:55, Yong Kiam <<a href="mailto:tanyongkiam@gmail.com">tanyongkiam@gmail.com</a>> wrote:<br>
>> I am fixing the translation on CakeML 314a5e6 and HOL 572ce3d<br>
>><br>
>> Those work fine with the (old?) parsing scripts.<br>
>><br>
>> It would be helpful if you had a look at ml_progLib on env-refactor since I<br>
>> might have also inadvertently slowed it down by expanding things<br>
>> incorrectly.<br>
><br>
> I'm looking at it. I'll commit my edits to a branch off of<br>
> env-refactor (because my tinkering with ml_progLib is likely to break<br>
> the bootstrap).<br>
<br>
</span>I accidentally pushed my change directly to env-refactor. The<br>
translator directory builds with the improved ml_progLib. However, I<br>
can't test other directories due to breakage caused by recent parser<br>
changes.<br>
<div class="HOEnZb"><div class="h5"><br>
Cheers,<br>
Magnus<br>
<br>
>> On Wed, Feb 15, 2017 at 6:53 AM, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk">Ramana.Kumar@cl.cam.ac.uk</a>><br>
>> wrote:<br>
>>><br>
>>> 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>
>>><br>
>>> On 15 February 2017 at 22:43, Magnus Myreen <<a href="mailto:magnus.myreen@gmail.com">magnus.myreen@gmail.com</a>><br>
>>> 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<br>
>>> > /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<br>
>>> > ../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>><br>
>>> > 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>><br>
>>> >> 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>
>><br>
>><br>
</div></div></blockquote></div><br></div>