Clashing identifiers are not renamed

[larsrh]

After updating to d82f8c7911e4c07e8fe4fd6f7685866537ad6d38, code like this gets emitted:

diff --git a/thy/generated/CakeML/Namespace.thy b/thy/generated/CakeML/Namespace.thy
index 380a0d4..f823c9a 100644
--- a/thy/generated/CakeML/Namespace.thy
+++ b/thy/generated/CakeML/Namespace.thy
@@ -16,38 +16,38 @@ begin
 type_synonym( 'k, 'v) alist0 =" ('k * 'v) list "

 (* Identifiers *)
-datatype( 'm, 'n) id0 =
+datatype( 'm, 'n) id =
     Short " 'n "
-  | Long " 'm " " ('m, 'n) id0 "
+  | Long " 'm " " ('m, 'n) id "

 (*val mk_id : forall 'n 'm. list 'm -> 'n -> id 'm 'n*)
-fun  mk_id  :: " 'm list \<Rightarrow> 'n \<Rightarrow>('m,'n)id0 "  where 
+fun  mk_id  :: " 'm list \<Rightarrow> 'n \<Rightarrow>('m,'n)id "  where 
      " mk_id [] n = ( Short n )"
     |" mk_id (mn # mns) n = ( Long mn (mk_id mns n))"

 (*val id_to_n : forall 'n 'm. id 'm 'n -> 'n*)
-fun  id_to_n  :: "('m,'n)id0 \<Rightarrow> 'n "  where 
+fun  id_to_n  :: "('m,'n)id \<Rightarrow> 'n "  where 
      " id_to_n (Short n) = ( n )"
-    |" id_to_n (Long _ id1) = ( id_to_n id1 )"
+    |" id_to_n (Long _ id) = ( id_to_n id )"

(The diff describes the output of 11c8efae4dbbd3b8867f40bcb28cfb1d52a7d54f vs. d82f8c7911e4c07e8fe4fd6f7685866537ad6d38.)

This does not work because id is an existing constant.

[bauereiss]

I tried extracting the above example from the CakeML source, but for me, the datatype gets correctly renamed; the "id" identifier is in isabelle_constants.

Do you maybe have the LEMLIB environment variable set to a path that does not have an isabelle_constants file?

[larsrh]

Thanks, I see. I had misunderstood your patch: I thought specifying -lib LEM=... is sufficient, i.e. LEMLIB is not required any longer, but I call it as follows now, which works:

LEMLIB="$LEM_LIBRARY" "$LEM_BINARY" -lib LEM="$LEM_LIBRARY" -isa -use_datatype_record -outdir "$GENERATED_TARGET" "${CAKEML_LEM_FILES[@]}"

[bauereiss]

Ah, yes, the standard library is still handled separately. The usage message for the -lib command line flag could probably be improved; what about the following:

" add a library path, in addition to the standard library at '"^(default_library)^"'. To change the latter, set the LEMLIB environment variable. Directories in the library path may optionally be associated with Isabelle session names, e.g. -lib MyLib=path/to/mylib. The standard library is associated with the session name LEM by default."

If you have suggestions to improve the wording, let me know.

By the way, I think the -lib flag in your call above is not really necessary, since the LEM session name should be known by default.

[larsrh]

Sounds good, thanks! And yes, it works without the flag.