Karl Palmskog (Sep 16 2022 at 09:43): 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?
Karl Palmskog (Sep 16 2022 at 09:45):if it's faster, please feel free to make changes to the repo directly
Pierre-Marie Pédrot (Sep 16 2022 at 09:49):Try removing Context.binder_name
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
Remove New
Pierre-Marie Pédrot (Sep 16 2022 at 09:53):what version are you porting this to?
Pierre-Marie Pédrot (Sep 16 2022 at 09:53):(sorry, can't read)
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
Pierre-Marie Pédrot (Sep 16 2022 at 09:54):you'll have a bit of trouble with that maybe
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.
Pierre-Marie Pédrot (Sep 16 2022 at 09:55):you should preemptively remove the calls to V82.tactic / V82.of_tactic
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
Karl Palmskog (Sep 16 2022 at 09:55):just completely remove? OK
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
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
no, to Tacticals.New.tclTHEN (generalize [mkVar v]) (clear [v]))
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
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
(and then adapt the code that mentions gl and stuff)
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
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 *)
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)
Gaëtan Gilbert (Sep 16 2022 at 15:21):V82 is going away so yes
Last updated: Apr 19 2024 at 15:02 UTC