<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">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/translator/ml_translatorLib.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/translator/ml_translatorLib.sml : Fail "Static Errors"</i></div><div><i> error in load $(CAKEMLDIR)/translator/ml_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><div><br></div><div>Milad</div></div>