Support for Coq 8.18

[SnarkBoojum]

I just tried to compile 1.3.2+8.17 with Coq 8.18 (yes, I know what the +8.17 means), and the compilation fails because some functions now return arrays instead of lists, and that means a .ml doesn't match with a .mli -- in src/lib/hhutils.ml.

[Of course I tried the naive fix to adapt the .mli, but it fails because a list was expected everywhere else...]

[SnarkBoojum]

I tried to be less naive ; that makes things compile:

--- coq-hammer.orig/src/lib/hhutils.ml
+++ coq-hammer/src/lib/hhutils.ml
@@ -213,7 +213,7 @@
   | Prod (na, ty, body) -> (na, ty) :: take_all_prods evd body
   | _ -> []

-let destruct_app = EConstr.decompose_app
+let destruct_app = EConstr.decompose_app_list

 let destruct_prod evd t =
   let prods = take_all_prods evd t
--- coq-hammer.orig/src/plugin/opt.ml
+++ coq-hammer/src/plugin/opt.ml
@@ -4,9 +4,10 @@

 let _ =
   let gdopt=
-    { optdepr=false;
+    { optdepr=None;
       optkey=["Hammer";"Predictions"];
       optread=(fun ()->Some !predictions_num);
+      optstage=Interp;
       optwrite=
    (function
         None -> predictions_num := 128
@@ -18,9 +19,10 @@

 let _ =
   let gdopt=
-    { optdepr=false;
+    { optdepr=None;
       optkey=["Hammer";"SAutoLimit"];
       optread=(fun ()->Some !sauto_timelimit);
+      optstage=Interp;
       optwrite=
    (function
         None -> sauto_timelimit := 1
@@ -32,9 +34,10 @@

 let _ =
   let gdopt=
-    { optdepr=false;
+    { optdepr=None;
       optkey=["Hammer";"ATPLimit"];
       optread=(fun ()->Some !atp_timelimit);
+      optstage=Interp;
       optwrite=
    (function
         None -> atp_timelimit := 10
@@ -46,9 +49,10 @@

 let _ =
   let gdopt=
-    { optdepr=false;
+    { optdepr=None;
       optkey=["Hammer";"ReconstrLimit"];
       optread=(fun ()->Some !reconstr_timelimit);
+      optstage=Interp;
       optwrite=
    (function
         None -> reconstr_timelimit := 10
@@ -60,9 +64,10 @@

 let _ =
   let gdopt=
-    { optdepr=false;
+    { optdepr=None;
       optkey=["Hammer";"MinimizationThreshold"];
       optread=(fun ()->Some !minimize_threshold);
+      optstage=Interp;
       optwrite=
    (function
         None -> minimize_threshold := 0
@@ -74,9 +79,10 @@

 let _ =
   let gdopt=
-    { optdepr=false;
+    { optdepr=None;
       optkey=["Hammer";"GSMode"];
       optread=(fun ()->Some !gs_mode);
+      optstage=Interp;
       optwrite=
    (function
         None -> gs_mode := 16
@@ -88,9 +94,10 @@

 let _ =
   let gdopt=
-    { optdepr=false;
+    { optdepr=None;
       optkey=["Hammer";"Eprover"];
       optread=(fun () -> !eprover_enabled);
+      optstage=Interp;
       optwrite=(fun b -> eprover_enabled := b)}
   in
   declare_bool_option gdopt
@@ -99,9 +106,10 @@

 let _ =
   let gdopt=
-    { optdepr=false;
+    { optdepr=None;
       optkey=["Hammer";"Vampire"];
       optread=(fun () -> !vampire_enabled);
+      optstage=Interp;
       optwrite=(fun b -> vampire_enabled := b)}
   in
   declare_bool_option gdopt
@@ -110,9 +118,10 @@

 let _ =
   let gdopt=
-    { optdepr=false;
+    { optdepr=None;
       optkey=["Hammer";"Z3"];
       optread=(fun () -> !z3_enabled);
+      optstage=Interp;
       optwrite=(fun b -> z3_enabled := b)}
   in
   declare_bool_option gdopt
@@ -121,9 +130,10 @@

 let _ =
   let gdopt=
-    { optdepr=false;
+    { optdepr=None;
       optkey=["Hammer";"CVC4"];
       optread=(fun () -> !cvc4_enabled);
+      optstage=Interp;
       optwrite=(fun b -> cvc4_enabled := b)}
   in
   declare_bool_option gdopt
@@ -132,9 +142,10 @@

 let _ =
   let gdopt=
-    { optdepr=false;
+    { optdepr=None;
       optkey=["Hammer";"PredictPath"];
       optread=(fun () -> !predict_path);
+      optstage=Interp;
       optwrite=(fun s -> predict_path := s)}
   in
   declare_string_option gdopt
@@ -143,9 +154,10 @@

 let _ =
   let gdopt=
-    { optdepr=false;
+    { optdepr=None;
       optkey=["Hammer";"PredictMethod"];
       optread=(fun () -> !predict_method);
+      optstage=Interp;
       optwrite=
         begin fun s ->
           if s = "knn" || s = "nbayes" || s = "rforest" then
@@ -160,9 +172,10 @@

 let _ =
   let gdopt=
-    { optdepr=false;
+    { optdepr=None;
       optkey=["Hammer";"Parallel"];
       optread=(fun () -> !parallel_mode);
+      optstage=Interp;
       optwrite=(fun b -> parallel_mode := b)}
   in
   declare_bool_option gdopt
@@ -171,18 +184,20 @@

 let _ =
   let gdopt=
-    { optdepr=false;
+    { optdepr=None;
       optkey=["Hammer";"Debug"];
       optread=(fun () -> !debug_mode);
+      optstage=Interp;
       optwrite=(fun b -> debug_mode := b)}
   in
   declare_bool_option gdopt

 let _ =
   let gdopt=
-    { optdepr=false;
+    { optdepr=None;
       optkey=["Hammer";"ClosureGuards"];
       optread=(fun () -> !Coq_transl_opts.opt_closure_guards);
+      optstage=Interp;
       optwrite=(fun b -> Coq_transl_opts.opt_closure_guards := b)}
   in
   declare_bool_option gdopt
@@ -191,9 +206,10 @@

 let _ =
   let gdopt=
-    { optdepr=false;
+    { optdepr=None;
       optkey=["Hammer";"FilterProgram"];
       optread=(fun () -> !filter_program);
+      optstage=Interp;
       optwrite=(fun b -> filter_program := b)}
   in
   declare_bool_option gdopt
@@ -202,9 +218,10 @@

 let _ =
   let gdopt=
-    { optdepr=false;
+    { optdepr=None;
       optkey=["Hammer";"FilterClasses"];
       optread=(fun () -> !filter_classes);
+      optstage=Interp;
       optwrite=(fun b -> filter_classes := b)}
   in
   declare_bool_option gdopt
@@ -213,9 +230,10 @@

 let _ =
   let gdopt=
-    { optdepr=false;
+    { optdepr=None;
       optkey=["Hammer";"FilterHurkens"];
       optread=(fun () -> !filter_hurkens);
+      optstage=Interp;
       optwrite=(fun b -> filter_hurkens := b)}
   in
   declare_bool_option gdopt
@@ -224,9 +242,10 @@

 let _ =
   let gdopt=
-    { optdepr=false;
+    { optdepr=None;
       optkey=["Hammer";"Blacklist"];
       optread=(fun () -> !search_blacklist);
+      optstage=Interp;
       optwrite=(fun b -> search_blacklist := b)}
   in
   declare_bool_option gdopt
--- coq-hammer.orig/src/plugin/hammer_main.ml
+++ coq-hammer/src/plugin/hammer_main.ml
@@ -33,6 +33,7 @@
 let hhterm_of_sort s = match Sorts.family s with
   | InSProp -> mk_id "$Prop"
   | InProp -> mk_id "$Prop"
+  | InQSort -> mk_id "$Sort"
   | InSet  -> mk_id "$Set"
   | InType -> mk_id "$Type"

--- coq-hammer.orig/src/plugin/g_hammer.mlg
+++ coq-hammer/src/plugin/g_hammer.mlg
@@ -8,10 +8,6 @@

 let hammer_version_string = "CoqHammer 1.3.2 for Coq 8.17"

-let () = Mltop.add_known_plugin (fun () ->
-  Flags.if_verbose Feedback.msg_info Pp.(str hammer_version_string))
-  "coq-hammer.plugin"
-
 open Hammer_main

 }

Note that for the src/plugin/opt.ml part, I wonder why there isn't a common function to build that object, taking as argument just what changes from one to the other - a simple refactoring might be in order.

[lukaszcz]

Thanks, but for Coq 8.18 you should try the master branch which is kept up to date with the development version of Coq. I'll update to Coq 8.18 once a Coq Platform with Coq 8.18 is in preparation.

Note that for the src/plugin/opt.ml part, I wonder why there isn't a common function to build that object, taking as argument just what changes from one to the other - a simple refactoring might be in order.

Maybe there should be, but I don't think that much can be abstracted here. In any case, pull request contributions are always welcome.