Stream: Coq devs & plugin devs

Topic: Constr.decompose_app

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.

Guillaume Melquiond (Sep 01 2023 at 16:41):

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

Maxime Dénès (Sep 02 2023 at 10:03):

I don't remember we did.

Maxime Dénès (Sep 02 2023 at 10:03):

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

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

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: Nov 29 2023 at 21:01 UTC