Done ! At least, now coq compiles and seams to run OK.
I encountered a strange bug, anyway, and would like some advice about my fix. Also, this bug do not seams related to my particular architecture and, as far as I can tell, would hit any MIPS. At various occasions the coqtop program jumped in the wrong places. This was due to the code emited for some tail calls : | Lop(Itailcall_imm s) -> if s = !function_name then begin ` b {emit_label !tailrec_entry_point}\n` end else begin let n = frame_size() in if !contains_calls then ` lw $31, {emit_int(n - 4)}($sp)\n`; if !uses_gp then ` lw $gp, {emit_int(n - 8)}($sp)\n`; if n > 0 then ` addu $sp, $sp, {emit_int n}\n`; ` la $25, {emit_symbol s}\n`; liveregs i live_25; ` j $25\n` end Now when !uses_gp is true, then the gp register is restored. Only then the address of symbol s is fetched into register $25, and jumped to. The problem is : the pseudo instruction 'la' may result in some code that uses gp to reach the global offset table and read the address from there. The assembler will then assume that the gp is the one that was setup at the begening of the function, and not the one that's just restored from the stack. Maybe for small programs the value of gp is always the same (I only vaguely understand this global pointer thing) but it is not the case for coq. So I merely moved upward the 'la' instruction, before the 'lw gp,stack'. And it works, apparently. What do you think ? _______________________________________________ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs