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/run_extractable.ml says

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

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: https://github.com/MetaCoq/metacoq/pull/855

Last updated: Jun 03 2023 at 18:01 UTC