[CakeML-dev] Failed to build CakeML using build instructions

[Anthony Fox]

There is already a HOL pull request with a quick fix for this. Konrad is too busy to check it over right now, so it’s probably best to accept the pull request and he can repair things later on if there turns out to be a problem. (I didn’t study the code that closely or even test it with 5.6.)

> On 18 May 2017, at 14:05, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
> 
> I made an issue for this, and it saw some progress a bit ago but none recently
> 
> Sent from my phone
> 
>> On 18 May 2017, at 14:03, Magnus Myreen <magnus.myreen at gmail.com> wrote:
>> 
>> Hi developers,
>> 
>> I tried building the latest HOL and CakeML following the build instructions at:
>> 
>> https://github.com/CakeML/cakeml/blob/master/build-instructions.sh
>> 
>> Unfortunately, my attempt failed due to an error in HOL under the
>> formal-languages example:
>> 
>> charsetTheory                                                           FAILED!
>>         (Different type constructors)
>> Found near if ~>> (w, ... ...) = 1 then orb (w, IntInf.<< (...)) else w
>> /local/scratch/mom22/HOL/examples/formal-languages/regular/WordOps.sml:28:
>> error: Type error in function application.
>>   Function: Word.fromInt : Int.int -> Word.word
>>   Argument: width : int
>>   Reason:
>>      Can't unify Int.int (*In Basis*) with int (*In Basis*)
>>         (Different type constructors)
>> Found near if ~>> (w, ... ...) = 1 then orb (w, IntInf.<< (...)) else w
>> Static Errors
>> 
>> Is there a known work around? Should the build instructions be updated?
>> 
>> Cheers,
>> Magnus
>> 
>> _______________________________________________
>> Developers mailing list
>> Developers at cakeml.org
>> https://lists.cakeml.org/listinfo/developers
> 
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers