Stream: Coq devs & plugin devs

Topic: Constr.decompose_app


view this post on Zulip Guillaume Melquiond (Sep 01 2023 at 16:37):

While porting some plugin code to 8.18, I just noticed the existence of the following function in kernel/constr.mli:

let decompose_app c =
  match kind c with
    | App (f,cl) -> (f, cl)
    | _ -> (c,[||])

When have we stopped calling Array.copy on arrays that can be mutated from user code?
And similarly for Constr.mkApp.

view this post on Zulip Guillaume Melquiond (Sep 01 2023 at 16:41):

Or am I misremembering and we never locked down the internal structures of Coq's kernel?

view this post on Zulip Maxime Dénès (Sep 02 2023 at 10:03):

I don't remember we did.

view this post on Zulip Maxime Dénès (Sep 02 2023 at 10:03):

I thought it was part of the contract between kernel code and user code.

view this post on Zulip Gaëtan Gilbert (Sep 04 2023 at 14:36):

I don't think we ever called Array.copy on the App arrays
I guess before coq/coq@cec135641a08f8cdfae32aedbbc450008d9746cf (year 2000) applications were stored as DOPN(Appl, Array.append [|head|] args) so the args array got copied when building and destructing, but after that kind_of_term was the identity so the arrays were directly accessible

view this post on Zulip Pierre-Marie Pédrot (Sep 04 2023 at 14:44):

"Always has been." We've been introducing more safety principles in the kernel, e.g. strings not being mutable. Yet for arrays, OCaml doesn't provide an immutable variant so there is no way out if we care about array literals.


Last updated: Jun 22 2024 at 23:01 UTC