[CakeML] problem in bootstrapping to get to CakeML

[Yong Kiam]

Hi Milad,

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?

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.

On Tue, Jun 20, 2017 at 10:41 AM, Milad Ketabii <ketabii.math at gmail.com>
wrote:

> 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
>
> _______________________________________________
> Users mailing list
> Users at cakeml.org
> https://lists.cakeml.org/listinfo/users
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20170620/23ac444c/attachment.html>