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 notifications@github.com 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 https://github.com/rems-project/linksem/issues/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 notifications@github.com 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 https://github.com/rems-project/linksem/issues/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 https://github.com/rems-project/linksem/issues/19#issuecomment-392051884, 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