<div dir="ltr">Hi Milad,<div><br></div><div>We usually build the bootstrap off the head of master on github of both HOL4 and CakeML. Which commits were you using for the build?</div><div><br></div><div>The first one looks like it might come from an older version of HOL4. I'm not sure about the second, I will try a local bootstrap of CakeML now to check that out.</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Jun 20, 2017 at 10:41 AM, Milad Ketabii <span dir="ltr"><<a href="mailto:ketabii.math@gmail.com" target="_blank">ketabii.math@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Good day<div><br></div><div><br></div><div>I need to use CakeML for a project, and have been trying to go through the instructions given under the section bootstrapping of the link:</div><div><br></div><div><a href="https://cakeml.org/download" target="_blank">https://cakeml.org/download</a>  <br></div><div><br></div><div><br></div><div>The first item proceeds without any apparent error/problem. However, when I go for the second step (which is running the command Holmake in the designated directory) I get error messages. This happens for two different kernels.</div><div><br></div><div>In the first kernel, after just a few minutes, I get the following error:</div><div><br></div><div><div><i>Recursively calling Holmake in ../../../../translator</i></div><div><i>ml_translator_testTheory                                                  FAILED!</i></div><div><i> /home/users/u5711205/cakeml/<wbr>translator/ml_translatorLib.<wbr>sml:3431: error: Value or constructor (NOT_NIL_EQ_LENGTH_NOT_0) has not been declared</i></div><div><i> Found near [NOT_NIL_EQ_LENGTH_NOT_0]</i></div><div><i> error in quse /home/users/u5711205/cakeml/<wbr>translator/ml_translatorLib.<wbr>sml : Fail "Static Errors"</i></div><div><i> error in load $(CAKEMLDIR)/translator/ml_<wbr>translatorLib : Fail "Static Errors"</i></div><div><i> error in load ml_translator_testScript : Fail "Static Errors"</i></div><div><i> Static Errors</i></div><div><i>ml_module_demoTheory                                                   M-KILLED</i></div><div><i>ml_pmatch_demoTheory                                                   M-KILLED</i></div><div><i>ml_translator_demoTheory                                                M-KILLED</i></div></div><div><br></div><div><br></div><div>In the other kernel, the process continued for about six hours (on a corei7/16GB/256SSD) but unfortunately I reached to the following error :</div><div><br></div><div><br></div><div><i>compiler_x64ProgTheory                                                    FAILED</i></div><div><i>                  (CONCAT</i></div><div><i>                          (MAP explode</i></div><div><i>                                 (append (FST (compiler_x64 (TL (... ... )) inp)))))) *</i></div><div><i>           STDERR</i></div><div><i>              (STRCAT err</i></div><div><i>                    (explode (SND (compiler_x64 (TL MAP implode cl)) inp)))) *</i></div><div><i>            (STDIN " " T * COMMANDLINE cl))</i></div><div><i>  failed.</i></div><div><i>  FAILED to prove theorem main_spec.</i></div><div><br></div><div><br></div><div>I hope someone would kindly let me know where exactly has gone wrong and how I could fix it.</div><div><br></div><div><br></div><div>thanks</div><span class="HOEnZb"><font color="#888888"><div><br></div><div>Milad</div></font></span></div>
<br>______________________________<wbr>_________________<br>
Users mailing list<br>
<a href="mailto:Users@cakeml.org">Users@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/users" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/users</a><br>
<br></blockquote></div><br></div>