Gaëtan Gilbert (Dec 07 2023 at 11:01): Gaëtan Gilbert (Dec 07 2023 at 11:01):suppose I define an external with an imperative effect such as
let () = define "foo" (unit @-> ret unit) @@ fun () ->
Feedback.msg_info Pp.(str "hello")
and use it like
Ltac2 @ external foo : unit -> unit := "coq-core.plugins.ltac2" "foo".
Goal True /\ True.
Succeed split; Control.enter foo. (* 1 hello *)
Succeed split; exact I; Control.enter foo. (* 1 hello *)
This happens because enter is defined as
let thaw f = Tac2ffi.apply f [v_unit]
let () =
define "enter" (closure @-> tac unit) @@ fun f ->
let f = Proofview.tclIGNORE (thaw f) in
Proofview.tclINDEPENDENT f
thaw applies the ocaml closure outside the enter
This behaviour seems like a bug, but I'm not sure which code should be considered buggy.
Maybe thaw should be defined as let thaw f = tclUNIT () >>= fun () -> Tac2ffi.apply f [v_unit]?
Maybe the external should be defined as
let () = define "foo" (unit @-> tac unit) @@ fun () ->
tclUNIT () >>= fun () ->
Feedback.msg_info Pp.(str "hello");
tclUNIT ()
or use tclLIFT?
I think there is no way to get buggy behaviour with the stdlib externals but it seems fragile, for instance
Goal True /\ True.
let a := Array.make 0 () in
split; exact I; Control.enter (Array.set a 0).
attempts to do the array.set, catches the ocaml invalid_argument exception and goes into throw. We don't see the exception because throw uses tclLIFT.
We don't see an incorrect set with
Goal True /\ True.
let a := Array.make 1 0 in
split; exact I; Control.enter (fun () => Array.set a 0 1).
because the interpreter on Array.set a 0 1 does List.Monad.map interp args >>= fun args -> apply head args but this seems fragile as in principle the interpreter could see that the arguments are values and don't need to go through the monad
Pierre-Marie Pédrot (Dec 07 2023 at 11:16):The problem is the definition of the external, you must wrap the effect in a tclLIFT
Janno (Dec 07 2023 at 11:40):Does that mean Array.set is implemented incorrectly? I think my expectation would be for it to not execute at all in the first example.
Pierre-Marie Pédrot (Dec 07 2023 at 11:57):The implementation is definitely incorrect, indeed.
Pierre-Marie Pédrot (Dec 07 2023 at 11:59):An easy fix is to wrap the function in the definition of thedefine function used in the OCaml API to register externals
Janno (Dec 07 2023 at 12:41):Is that a specific fix for Array.set or a more general proposal? In the latter case, how would it work for primitives that mix non-logical and logical operations?
Gaëtan Gilbert (Dec 07 2023 at 12:42):WDYM?
Janno (Dec 07 2023 at 12:50):I guess I just don't yet understand the proposal for changing define
Pierre-Marie Pédrot (Dec 07 2023 at 12:52):The spec is that a function of arity n passed to refine is indeed a pure function of arity n, returning a monadic value.
Pierre-Marie Pédrot (Dec 07 2023 at 12:52):binding the monadic value may perform effects but it's fine
Pierre-Marie Pédrot (Dec 07 2023 at 12:52):so there is no logical vs. nonlogical distinction
Gaëtan Gilbert (Dec 07 2023 at 12:53):where's refine coming from?
I mean why are you talking about refine?
Pierre-Marie Pédrot (Dec 07 2023 at 12:53):what are you talking about?
Pierre-Marie Pédrot (Dec 07 2023 at 12:53):sorry, I meant *define
Janno (Dec 07 2023 at 12:59):Okay, so I understand that you are advocating for the spec of define to be what you describe above and that makes sense to me. I am still not sure what this proposal here entails, though:
An easy fix is to wrap the function in the definition of the define function used in the OCaml API to register externals
Pierre-Marie Pédrot (Dec 07 2023 at 13:02):It's a local fix in the OCaml code that will globally make everything work magically by η-expanding the argument function (we know the arity statically) and wrapping the return value into a monadic delay.
Pierre-Marie Pédrot (Dec 07 2023 at 13:02):even if the argument doesn't respect the spec, the function called at runtime will
Janno (Dec 07 2023 at 13:05):Instead of using the argument function f x1 .. xN directly we use tclUNIT () >>= fun () -> f x1 .. xN?
Pierre-Marie Pédrot (Dec 07 2023 at 13:06):something along those lines, yes
Janno (Apr 24 2024 at 11:20):Has anything happened on this front after https://github.com/coq/coq/issues/18631 was opened? I just tried using the Ltac2Compiler again and had to do quite a bit of debugging to find out that Array.empty is apparently implemented incorrectly and breaks if compiled. I am not really sure where the thunking should go with a primitive that takes zero arguments but I suppose tclLIFT (NonLogical.make (fun () -> ..))) might do it. Help would be appreciated. But the bigger question to me seems to be what should be done to avoid this pitfall. The idea to do thunking automatically seems to have been discarded. Could it still be wroth it to at least add a new kind of define return type that indicates impurity, adds a unit argument to the signature of the expected function to signal that something weird is happening, and wraps the result in tclLIFT (NonLogical.make ..)?
Janno (Apr 24 2024 at 11:23):I suppose tclUNIT () >>= fun () -> ... would also do the trick. Which one is more canonical?
Gaëtan Gilbert (Apr 24 2024 at 11:25):Array.empty is apparently implemented incorrectly and breaks if compiled
Array.empty being incorrect sounds extremely unlikely
Gaëtan Gilbert (Apr 24 2024 at 11:26):Has anything happened on this front after https://github.com/coq/coq/issues/18631 was opened?
no
Janno (Apr 24 2024 at 11:27):Require Import Ltac2Compiler.Ltac2Compiler.
From Ltac2 Require Import Array.
Ltac2 test () := Array.empty.
Ltac2 Eval Array.length (test ()).
Ltac2 Compile Array.empty.
Ltac2 Eval Array.length (test ()). (* Fails with anomaly in `Tac2ffi.to_array` *)
Maybe there is a different explanation.
Gaëtan Gilbert (Apr 24 2024 at 11:29):that's probably a bug of the compiler
Janno (Apr 24 2024 at 11:30):Oh, I see. I guess I was primed by fixing all our own external functions (that had actual issues with thunking).
Janno (Apr 24 2024 at 11:39):Your fix seems to work.
Last updated: Oct 12 2024 at 13:01 UTC