Re: [Hol-developers] compile error on examples of rev 5887

[Konrad S. <sl...@cs...>]

Hi Lu,

   That error comes because I upgraded simpsets to
have an extra field a while ago. Seems like you upgraded
ARM but not the rest of the system? I am not sure
what the best approach is. Maybe stop by sometime tomorrow and
we can talk about it?

Konrad.

On Oct 1, 2008, at 3:24 PM, Lu Zhao wrote:

> Hey,
>
> For certain reason, I need to compile HOL rev 5887. A strange problem
> that I'm having now is that I got the following error when I built
> examples/ARM/v4:
>
> Compiling armLib.sml
> File "armLib.sml", line 20-24, characters 4-805:
> ! ....{convs = map conv_rec [(Parse.Term [QUOTE " (*#loc 20
> 30*)swp"]),(Parse.Term [QUOTE " (*#loc 20 38*)mrs"]),(Parse.Term  
> [QUOTE
> " (*#loc 20 46*)msr"]),(Parse.Term [QUOTE " (*#loc 20 54*) 
> data_proc"]),
> !              (Parse.Term [QUOTE " (*#loc 21 16*)mla_mul"]),
> (Parse.Term [QUOTE " (*#loc 21 29*)ldr_str"]),(Parse.Term [QUOTE
> " (*#loc 21 41*)ldrh_strh"]), (Parse.Term [QUOTE " (*#loc 21
> 56*)ldm_stm"]),
> !              (Parse.Term [QUOTE " (*#loc 22 16*)br"]),(Parse.Term
> [QUOTE " (*#loc 22 23*)swi_ex"]), (Parse.Term [QUOTE " (*#loc 22
> 35*)cdp_und"]), (Parse.Term [QUOTE " (*#loc 22 48*)mcr"]),(Parse.Term
> [QUOTE " (*#loc 22 56*)mrc"]),(Parse.Term [QUOTE " (*#loc 22
> 64*)ldc_stc"]),
> !              (Parse.Term [QUOTE " (*#loc 23 16*)unexec"])],
> !    rewrs = [], congs = [], filter = NONE, ac = [], dprocs = []}.
> ! Type clash: expression of type
> !   {ac : 'a, congs : 'b, convs : 'c, dprocs : 'd, filter : 'e,  
> rewrs :
> 'f}
> ! cannot have type
> !   {ac : (thm * thm) list, congs : thm list,
>      convs :
>        {conv : (term list -> term -> thm) -> term list -> term -> thm,
>         key : (term list * term) option, name : string, trace : int}
> list,
>      dprocs : reducer list, filter : (thm -> thm list) option,
>      name : string option, rewrs : thm list}
> ! because record label  name  is missing
>
> A similar error as the following occured, when I built
> examples/mc-logic.
>
> File "set_sepLib.sml", line 12-15, characters 50-202:
>
> ! ..................................................{
> !   ac = [], congs = [],
> !   convs = [{ name  = name, conv = K (K conv), key = SOME([],  
> pattern),
> trace = 10 }],
> !   dprocs = [], filter = NONE, rewrs = []}.
> ! Type clash: expression of type
> !   {ac : 'a, congs : 'b, convs : 'c, dprocs : 'd, filter : 'e,  
> rewrs :
> 'f}
> ! cannot have type
> !   {ac : (thm * thm) list, congs : thm list,
>      convs :
>        {conv : (term list -> term -> thm) -> term list -> term -> thm,
>         key : (term list * term) option, name : string, trace : int}
> list,
>      dprocs : reducer list, filter : (thm -> thm list) option,
>      name : string option, rewrs : thm list}
> ! because record label  name  is missing
>
> However, on another computer, there was not a problem in building
> examples/ARM/v4 and mc-logic. The only difference is that the error
> version was freshly checked out by svn co -r 5887 ... and the work
> version was upgraded from rev 5874.
>
> Any ideas on how to fix this except to upgrade to the latest version?
> Since the latest version reported error on some previous HOL scripts.
>
> Lu
>
>
>
> ---------------------------------------------------------------------- 
> ---
> This SF.Net email is sponsored by the Moblin Your Move Developer's  
> challenge
> Build the coolest Linux based applications with Moblin SDK & win  
> great prizes
> Grand prize is a trip for two to an Open Source event anywhere in  
> the world
> http://moblin-contest.org/redirect.php?banner_id=100&url=/
> _______________________________________________
> Hol-developers mailing list
> Hol...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-developers