Stream: Coq devs & plugin devs

Topic: Help porting plugin from 8.14 to master


view this post on Zulip Karl Palmskog (Sep 16 2022 at 09:43):

I have a plugin stuck on 8.14 that I'd like to get ported via 8.15 and 8.16 to master and add to Coq's CI: https://github.com/coq-community/stalmarck

Here's the current build error for dune build on 8.15:

File "tactic/staltac_lib.ml", line 263, characters 30-59:
263 |   let v = Context.binder_name (get_hyps (pf_hyps_types gl)) in
                                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This expression has type variable
       but an expression was expected of type 'a Context.binder_annot

Any hints for how to handle this?

view this post on Zulip Karl Palmskog (Sep 16 2022 at 09:45):

if it's faster, please feel free to make changes to the repo directly

view this post on Zulip Pierre-Marie Pédrot (Sep 16 2022 at 09:49):

Try removing Context.binder_name

view this post on Zulip Karl Palmskog (Sep 16 2022 at 09:51):

thanks, fixed that error, next error:

File "tactic/staltac_lib.ml", line 264, characters 27-48:
264 |   Proofview.V82.of_tactic (Tacticals.New.tclTHEN (generalize [mkVar v]) (clear [v])) gl
                                 ^^^^^^^^^^^^^^^^^^^^^
Error: Unbound module Tacticals.New

view this post on Zulip Pierre-Marie Pédrot (Sep 16 2022 at 09:52):

Remove New

view this post on Zulip Pierre-Marie Pédrot (Sep 16 2022 at 09:53):

what version are you porting this to?

view this post on Zulip Pierre-Marie Pédrot (Sep 16 2022 at 09:53):

(sorry, can't read)

view this post on Zulip Pierre-Marie Pédrot (Sep 16 2022 at 09:54):

I don't remember in which version we removed the V82 module, either 8.15 or 8.16

view this post on Zulip Pierre-Marie Pédrot (Sep 16 2022 at 09:54):

you'll have a bit of trouble with that maybe

view this post on Zulip Karl Palmskog (Sep 16 2022 at 09:54):

if you think it's easier with error messages for master, I can provide that. But this is when running 8.15.

view this post on Zulip Pierre-Marie Pédrot (Sep 16 2022 at 09:55):

you should preemptively remove the calls to V82.tactic / V82.of_tactic

view this post on Zulip Pierre-Marie Pédrot (Sep 16 2022 at 09:55):

everytime you see a gl around you should wrap the block of code into Proofview.Goal.enter begin fun gl -> ... end

view this post on Zulip Karl Palmskog (Sep 16 2022 at 09:55):

just completely remove? OK

view this post on Zulip Pierre-Marie Pédrot (Sep 16 2022 at 09:56):

it will break the typing, you have to sprinkle a few enter to replace to V82.tactic, and just remove the of_tactic

view this post on Zulip Karl Palmskog (Sep 16 2022 at 09:58):

hmm, so switch this:

 Proofview.V82.of_tactic (Tacticals.New.tclTHEN (generalize [mkVar v]) (clear [v])) gl

to this?

Proofview.Goal.enter begin fun gl ->
    (Tacticals.New.tclTHEN (generalize [mkVar v]) (clear [v])) gl
    end

view this post on Zulip Pierre-Marie Pédrot (Sep 16 2022 at 09:59):

no, to Tacticals.New.tclTHEN (generalize [mkVar v]) (clear [v]))

view this post on Zulip Pierre-Marie Pédrot (Sep 16 2022 at 10:00):

and the place that introduced the gl function (a toplevel binder) you write Proofview.Goal.enter begin fun gl -> (oldcode) end

view this post on Zulip Pierre-Marie Pédrot (Sep 16 2022 at 10:01):

like this:

let pop_prop_run =
  Proofview.Goal.enter begin fun gl ->
  let rec get_hyps shyp = match shyp with
      [] -> user_err (str "popProp: No proposition to generalize");
    | (is,cst)::shyp' ->
         let env = pf_env gl in
         let sigma = project gl in
         match kind sigma (Retyping.get_type_of env sigma cst) with
           Sort s when (match ESorts.kind sigma s with Sorts.Prop -> true | _ -> false) -> is
         | _            -> get_hyps shyp'
  in
  let v = Context.binder_name (get_hyps (pf_hyps_types gl)) in
  Tacticals.New.tclTHEN (generalize [mkVar v]) (clear [v])
  end

view this post on Zulip Pierre-Marie Pédrot (Sep 16 2022 at 10:01):

(and then adapt the code that mentions gl and stuff)

view this post on Zulip Karl Palmskog (Sep 16 2022 at 11:05):

that seems to work, but I still have the problem that Tacticals.New is not a valid module name in 8.15 and later

view this post on Zulip Gaëtan Gilbert (Sep 16 2022 at 11:09):

you can probably do some hack like

module New = Tacticals
open Tacticals
module ReallyNew = New (* if Tacticals.New exists then use it, else use Tacticals *)

view this post on Zulip Karl Palmskog (Sep 16 2022 at 15:03):

I think I managed to port it, but this diff felt quite shaky, even though it compiled:

- TACTIC EXTEND _stalt_ | [ "stalt" ] -> { Proofview.V82.tactic stalt_run } END
- TACTIC EXTEND _pop_prop_ | [ "pop_prop" ] -> { Proofview.V82.tactic pop_prop_run } END
+ TACTIC EXTEND _stalt_ | [ "stalt" ] -> { stalt_run } END
+ TACTIC EXTEND _pop_prop_ | [ "pop_prop" ] -> { pop_prop_run } END

but maybe it's supposed to be like that? (Proofview.V82 functionality not necessary)

view this post on Zulip Gaëtan Gilbert (Sep 16 2022 at 15:21):

V82 is going away so yes


Last updated: Feb 05 2023 at 21:03 UTC