[CakeML] problem in bootstrapping to get to CakeML

[Milad Ketabii]

Good day


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:

https://cakeml.org/download


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.

In the first kernel, after just a few minutes, I get the following error:

*Recursively calling Holmake in ../../../../translator*
*ml_translator_testTheory
 FAILED!*
* /home/users/u5711205/cakeml/translator/ml_translatorLib.sml:3431: error:
Value or constructor (NOT_NIL_EQ_LENGTH_NOT_0) has not been declared*
* Found near [NOT_NIL_EQ_LENGTH_NOT_0]*
* error in quse /home/users/u5711205/cakeml/translator/ml_translatorLib.sml
: Fail "Static Errors"*
* error in load $(CAKEMLDIR)/translator/ml_translatorLib : Fail "Static
Errors"*
* error in load ml_translator_testScript : Fail "Static Errors"*
* Static Errors*
*ml_module_demoTheory
M-KILLED*
*ml_pmatch_demoTheory
M-KILLED*
*ml_translator_demoTheory
 M-KILLED*


In the other kernel, the process continued for about six hours (on a
corei7/16GB/256SSD) but unfortunately I reached to the following error :


*compiler_x64ProgTheory
 FAILED*
*                  (CONCAT*
*                          (MAP explode*
*                                 (append (FST (compiler_x64 (TL (... ...
)) inp)))))) **
*           STDERR*
*              (STRCAT err*
*                    (explode (SND (compiler_x64 (TL MAP implode cl))
inp)))) **
*            (STDIN " " T * COMMANDLINE cl))*
*  failed.*
*  FAILED to prove theorem main_spec.*


I hope someone would kindly let me know where exactly has gone wrong and
how I could fix it.


thanks

Milad
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20170620/6be48757/attachment.html>