Stream: MetaCoq

Topic: segfaults?

view this post on Zulip Jason Gross (Feb 24 2023 at 00:41):

Does extracted TemplateMonad code containing tmCurrentModPath segfault? The Gallina version in template-coq/theories/TemplateMonad/Extractable.v is

| tmCurrentModPath : TM modpath

but the OCaml code in template-coq/src/ says

  | Coq_tmCurrentModPath ->
    tmMap (fun mp -> Obj.magic (quote_string (Names.ModPath.to_string mp)))

which seems to indicate that we're returning a string rather than a modpath?

view this post on Zulip Matthieu Sozeau (Feb 24 2023 at 15:50):

Oops, indeed

view this post on Zulip Jason Gross (Feb 28 2023 at 04:39):

I've submitted a PR that fixes this in passing:

Last updated: Jun 13 2024 at 07:01 UTC