Cannot generate HOL output

[xrchz]

Doing make hol-extraction under src produces the following error:

File "dwarf.lem", line 131, character 19 to line 131, character 31
  Type error: unbound variable for targets {hol}: print_endline
lem.mk:165: recipe for target 'hol-extraction' failed

This seems to be a debugging feature, so perhaps it could be excluded from the extraction to provers?
From the Lem library:

(* debugging functions; these should *not* be used in production code,
   but are invaluable in debugging the OCaml extraction, as long as

[PeterSewell]

On 25 May 2018 at 12:12, Ramana Kumar ***@***.***> wrote: Doing make hol-extraction under src produces the following error: File "dwarf.lem", line 131, character 19 to line 131, character 31 Type error: unbound variable for targets {hol}: print_endlinelem.mk:165: recipe for target 'hol-extraction' failed This seems to be a debugging feature, so perhaps it could be excluded from the extraction to provers? From the Lem library: (* debugging functions; these should *not* be used in production code, but are invaluable in debugging the OCaml extraction, as long as

As a quick fix, I think you can just comment out that my_debug5 definition and the (few) usages of it. Probably we've never previously generated prover code from dwarf.lem. More properly, we should have a debug_print_endline that gets mapped into nothing in the provers. p

…

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#19>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AErM5uno8YSF5gu-AvSdc6HksUCHS5gNks5t1-cQgaJpZM4UNy94> .

[cp526]

On 25/05/18 14:06, Peter Sewell wrote: On 25 May 2018 at 12:12, Ramana Kumar ***@***.***> wrote: > Doing make hol-extraction under src produces the following error: > > File "dwarf.lem", line 131, character 19 to line 131, character 31 > Type error: unbound variable for targets {hol}: print_endlinelem.mk:165: recipe for target 'hol-extraction' failed > > This seems to be a debugging feature, so perhaps it could be excluded from > the extraction to provers? > From the Lem library: > > (* debugging functions; these should *not* be used in production code, > but are invaluable in debugging the OCaml extraction, as long as > > As a quick fix, I think you can just comment out that my_debug5 definition and the (few) usages of it. Probably we've never previously generated prover code from dwarf.lem. More properly, we should have a debug_print_endline that gets mapped into nothing in the provers.

Don't know since when, but we do have debug.lem in the library, that contains print_string and print_endline.

…

p > — > You are receiving this because you are subscribed to this thread. > Reply to this email directly, view it on GitHub > <#19>, or mute the thread > <https://github.com/notifications/unsubscribe-auth/AErM5uno8YSF5gu-AvSdc6HksUCHS5gNks5t1-cQgaJpZM4UNy94> > . > — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#19 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AGUw4ue4C3b1SDR88gNuIoruvTMT6NBHks5t2AHCgaJpZM4UNy94>.

[xrchz]

I appreciate the quick fix, but unfortunately there are then other things in dwarf.lem that break when attempting HOL output. For example #20.

[xrchz]

Another example is as follows. This also looks debugging related, perhaps? There is a hex to string function in HOL, but not one that takes and uses a padding in the same way.

File "dwarf.lem", line 1334, character 22 to line 1334, character 49
  Type error: unbound variable for targets {hol}: unsafe_hex_string_of_natural
lem.mk:165: recipe for target 'hol-extraction' failed