Stream: Coq devs & plugin devs

Topic: ✔ Calling Ltac2 from Ocaml


view this post on Zulip Mathis Bouverot-Dupuis (Jul 11 2024 at 13:06):

In my case Tac2env.globals returns an empty map. Is this normal ?

view this post on Zulip Gaëtan Gilbert (Jul 11 2024 at 13:14):

no

view this post on Zulip Mathis Bouverot-Dupuis (Jul 11 2024 at 13:15):

any ideas on what could be wrong ?

view this post on Zulip Gaëtan Gilbert (Jul 11 2024 at 13:16):

IDK show your code

view this post on Zulip Mathis Bouverot-Dupuis (Jul 11 2024 at 13:20):

I have this ocaml tactic :

let test_tac () : unit tactic =
  let open Ltac2_plugin in
  let globals = Tac2env.globals () |> Names.KNmap.bindings in
  Feedback.msg_notice
    (Pp.str ("count = " ^ string_of_int (List.length globals)));
  Tacticals.tclIDTAC

Which I call from Coq :

Lemma test : True.
test_tac.

And it prints count = 0.

view this post on Zulip Mathis Bouverot-Dupuis (Jul 11 2024 at 13:21):

Oh never mind I found the problem

view this post on Zulip Mathis Bouverot-Dupuis (Jul 11 2024 at 13:22):

I was calling the tactic test_tac from a file where I didn't import Ltac2 (I'm in the process of switching from Ltac to Ltac2). After importing Ltac2 the map is longer empty.

view this post on Zulip Notification Bot (Jul 11 2024 at 13:30):

Mathis Bouverot-Dupuis has marked this topic as resolved.

view this post on Zulip Gaëtan Gilbert (Jul 11 2024 at 13:35):

you mean Require not Import?

view this post on Zulip Mathis Bouverot-Dupuis (Jul 11 2024 at 13:37):

From Ltac2 Require Import Ltac2 to be precise. Sorry for the confusion, the distinction between Import/Require is not clear to me.

view this post on Zulip Mathis Bouverot-Dupuis (Jul 11 2024 at 13:38):

Read up on the distinction and now it makes sense that Require was necessary.


Last updated: Oct 13 2024 at 01:02 UTC