bug ?

bug ?

[Jean-Christophe Filliatre]

Bonjour,

  En debugguant Coq avec Judicael, nous avons obtenu le resultat surprenant
suivant : soit toto.ml le programme suivant

------------------------
#open "hashtbl";;

let f x = 
  let t = new 10
  in add t x true;
     find t x
;;

if f 1 then output_string std_out "ok\n" ; flush std_out
;;
-----------------------

toujours dans le meme repertoire, je fais

-----------------------
% camlc toto.ml
% camlmktop -o essai toto.zo
% camllight essai
ok
>       Caml Light version 0.61
 
#trace "hashtbl__add";;
>> hashtbl__add is now traced.
- : unit = ()
##open "toto";;
hashtbl__add <-- <abstract>
hashtbl__add --> <fun>
hashtbl__add* <-- <poly>
hashtbl__add* --> <fun>
hashtbl__add** <-- <poly>
hashtbl__add** --> ()
#
-----------------------

qu'est-ce qui se passe ?!?!

--Jean-Christophe.

Re: bug ?

[Pierre Weis]

Bonjour,

This is just that the standard library is shared by the compiler and
the user: the compiler uses the same hashtbl__add function as
you. Thus, if you trace it, you can observe that the system uses it
when opening a module! There's nothing wrong here... By the way, don't
try to trace print_string, since once more the trace package uses the
same function, thus ... it's funny.

Pierre Weis
----------------------------------------------------------------------------
Projet Cristal
INRIA, BP 105, F-78153 Le Chesnay Cedex (France)
E-mail: Pierre.Weis@inria.fr
Telephone: +33 1 39 63 55 98
----------------------------------------------------------------------------