New Upstream Release - coq-hammer

QA Page
Maintainer email: debian-ocaml-maint@lists.debian.org
Automatic publish policy: main: push-derived , pristine-tar: push-derived , upstream: push-derived
Last processed: 2023-05-31T00:57 (took 2m40s)
Branch URL: https://salsa.debian.org/ocaml-team/coq-hammer.git -b master (taken from version 1.3.2+8.18-1)
Queue position: 105694 (a 46w1d wait)
Ready changes

Summary

Merged new upstream version: 1.3.2+8.17 (was: 1.3.2+8.16).
Diff

diff --git a/CHANGES.md b/CHANGES.md
index 668a296..88092af 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,7 +1,7 @@
 CoqHammer v. 1.3.2
 ==================
 
-Coq versions compatibility: 8.10, 8.11, 8.12, 8.13, 8.14, 8.15, 8.16.
+Coq versions compatibility: 8.10, 8.11, 8.12, 8.13, 8.14, 8.15, 8.16, 8.17.
 
 Overview of changes
 -------------------
diff --git a/Makefile b/Makefile
index bc9225f..a7b9a07 100644
--- a/Makefile
+++ b/Makefile
@@ -3,19 +3,22 @@ BINDIR ?= $(if $(COQBIN),$(COQBIN),`coqc -where | xargs dirname | xargs dirname`
 
 default: all
 
-all: tactics plugin
+all:
+	$(MAKE) tactics
+	$(MAKE) install-tactics
+	$(MAKE) plugin
 
 tactics: Makefile.coq.tactics
 	$(MAKE) -f Makefile.coq.tactics
 
-plugin: install-tactics Makefile.coq.plugin Makefile.coq.plugin.local
+plugin: Makefile.coq.plugin Makefile.coq.plugin.local
 	-rm -f META
 	$(MAKE) -f Makefile.coq.plugin
 
 mathcomp: Makefile.coq.mathcomp
 	$(MAKE) -f Makefile.coq.mathcomp
 
-install: install-plugin
+install: install-tactics install-plugin
 
 install-tactics: tactics
 	$(MAKE) -f Makefile.coq.tactics install
diff --git a/README.md b/README.md
index a4c588a..c1eb3c3 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,6 @@
-CoqHammer 1.3.2 for Coq 8.16
+CoqHammer 1.3.2 for Coq 8.17
 
-[![Travis](https://app.travis-ci.com/lukaszcz/coqhammer.svg?branch=v1.3.2-coq8.16)](https://app.travis-ci.com/lukaszcz/coqhammer/builds)
+[![Travis](https://app.travis-ci.com/lukaszcz/coqhammer.svg?branch=v1.3.2-coq8.17)](https://app.travis-ci.com/lukaszcz/coqhammer/builds)
 
 CoqHammer video tutorial:
 [part 1 (sauto)](https://www.youtube.com/watch?v=0c_utk9bVgU&list=PLXXF_svQE_b-9A5p2OKU7Tjz-NcE7H2xg),
@@ -21,7 +21,7 @@ documentation and installation instructions.
 
 Requirements
 ------------
-- [Coq 8.16](https://coq.inria.fr)
+- [Coq master](https://github.com/coq/coq)
 - for `hammer`: automated provers
   ([Vampire](https://vprover.github.io/download.html),
   [CVC4](http://cvc4.cs.stanford.edu/downloads/),
@@ -31,7 +31,7 @@ Requirements
 Copyright and license
 ---------------------
 
-Copyright (c) 2017-2020, Lukasz Czajka, TU Dortmund University.\
+Copyright (c) 2017-2023, Lukasz Czajka, TU Dortmund University.\
 Copyright (c) 2017-2018, Cezary Kaliszyk, University of Innsbruck.
 
 Distributed under the terms of LGPL 2.1, see the file
diff --git a/coq-hammer-tactics.opam b/coq-hammer-tactics.opam
index 4f7247f..a4bafbc 100644
--- a/coq-hammer-tactics.opam
+++ b/coq-hammer-tactics.opam
@@ -1,5 +1,5 @@
 opam-version: "2.0"
-version: "1.3.2+8.16"
+version: "1.3.2+8.17"
 maintainer: "lukaszcz@mimuw.edu.pl"
 
 homepage: "https://github.com/lukaszcz/coqhammer"
@@ -22,7 +22,7 @@ install: [
 ]
 depends: [
   "ocaml" {>= "4.08"}
-  "coq" {>= "8.16" & < "8.17~"}
+  "coq" {>= "8.17" & < "8.18~"}
 ]
 
 tags: [
diff --git a/coq-hammer.opam b/coq-hammer.opam
index 065ace3..7597090 100644
--- a/coq-hammer.opam
+++ b/coq-hammer.opam
@@ -1,5 +1,5 @@
 opam-version: "2.0"
-version: "1.3.2+8.16"
+version: "1.3.2+8.17"
 maintainer: "lukaszcz@mimuw.edu.pl"
 
 homepage: "https://github.com/lukaszcz/coqhammer"
@@ -21,7 +21,7 @@ install: [
 ]
 depends: [
   "ocaml" {>= "4.08"}
-  "coq" {>= "8.16" & < "8.17~"}
+  "coq" {>= "8.17" & < "8.18~"}
   ("conf-g++" {build} | "conf-clang" {build})
   "coq-hammer-tactics" {= version}
 ]
diff --git a/debian/changelog b/debian/changelog
index 0e250b0..6befdcb 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,9 @@
+coq-hammer (1.3.2+8.17-1) UNRELEASED; urgency=low
+
+  * New upstream release.
+
+ -- Debian Janitor <janitor@jelmer.uk>  Wed, 31 May 2023 00:54:55 -0000
+
 coq-hammer (1.3.2+8.16-2) unstable; urgency=medium
 
   * Change b-dep from libcoq-ocaml-dev to libcoq-core-ocaml-dev.
diff --git a/debian/patches/use_libexec.patch b/debian/patches/use_libexec.patch
index 051d4e4..ea79736 100644
--- a/debian/patches/use_libexec.patch
+++ b/debian/patches/use_libexec.patch
@@ -2,9 +2,11 @@ Description: put internal executables away in /usr/libexec
 Author: Julien Puydt
 Forwarded: https://github.com/lukaszcz/coqhammer/issues/139
 
---- coq-hammer.orig/src/plugin/opt.ml
-+++ coq-hammer/src/plugin/opt.ml
-@@ -128,7 +128,7 @@
+Index: coq-hammer.git/src/plugin/opt.ml
+===================================================================
+--- coq-hammer.git.orig/src/plugin/opt.ml
++++ coq-hammer.git/src/plugin/opt.ml
+@@ -128,7 +128,7 @@ let _ =
    in
    declare_bool_option gdopt
  
@@ -13,9 +15,11 @@ Forwarded: https://github.com/lukaszcz/coqhammer/issues/139
  
  let _ =
    let gdopt=
---- coq-hammer.orig/src/plugin/provers.ml
-+++ coq-hammer/src/plugin/provers.ml
-@@ -172,7 +172,7 @@
+Index: coq-hammer.git/src/plugin/provers.ml
+===================================================================
+--- coq-hammer.git.orig/src/plugin/provers.ml
++++ coq-hammer.git/src/plugin/provers.ml
+@@ -172,7 +172,7 @@ let call_eprover infile outfile =
    let tmt = string_of_int !Opt.atp_timelimit in
    let tmt2 = string_of_int (!Opt.atp_timelimit + 1) in
    let cmd =
diff --git a/src/lib/hhutils.ml b/src/lib/hhutils.ml
index e904197..b504211 100644
--- a/src/lib/hhutils.ml
+++ b/src/lib/hhutils.ml
@@ -299,9 +299,10 @@ let map_fold_constr f acc evd t =
     | Proj (p,c) ->
        let (acc1, c') = hlp m acc c in
        f m acc1 (mkProj(p,c'))
-    | Evar (evk,cl) ->
+    | Evar ((evk, _) as ev) ->
+       let cl = Evd.expand_existential evd ev in
        let (acc1, cl') = fold_list m acc cl in
-       f m acc1 (mkEvar(evk,cl'))
+       f m acc1 (mkLEvar evd (evk,cl'))
     | Case (ci,u,pms,p,iv,c,bl) ->
        let (acc, pms') = fold_arr m acc pms in
        let (acc, p') = fold_ctx m acc p in
@@ -368,7 +369,8 @@ let fold_constr f acc evd t =
     | Proj (p,c) ->
        let acc1 = hlp m acc c in
        f m acc1 t
-    | Evar (evk,cl) ->
+    | Evar ev ->
+       let cl = Evd.expand_existential evd ev in
        let acc1 = fold_list m acc cl in
        f m acc1 t
     | Case (ci,u,pms,p,iv,c,bl) ->
@@ -431,7 +433,8 @@ let fold_constr_shallow f acc evd t =
     | Proj (p,c) ->
        let acc1 = hlp acc c in
        f acc1 t
-    | Evar (evk,cl) ->
+    | Evar ev ->
+       let cl = Evd.expand_existential evd ev in
        let acc1 = fold_list acc cl in
        f acc1 t
     | Case (ci,u,pms,p,iv,c,bl) ->
@@ -469,10 +472,6 @@ let map_fold_constr_ker f acc t =
       in
       (ac1, Array.of_list (List.rev lst))
     in
-    let fold_list k ac lst =
-      let (ac, ar) = fold_arr k ac (Array.of_list lst) in
-      (ac, Array.to_list ar)
-    in
     let fold_ctx k ac (nas, c) =
       let (ac, c') = hlp (k + Array.length nas) ac c in
       (ac, (nas, c'))
@@ -504,9 +503,7 @@ let map_fold_constr_ker f acc t =
     | Proj (p,c) ->
        let (acc1, c') = hlp m acc c in
        f m acc1 (mkProj(p,c'))
-    | Evar (evk,cl) ->
-       let (acc1, cl') = fold_list m acc cl in
-       f m acc1 (mkEvar(evk,cl'))
+    | Evar _ -> assert false
     | Case (ci,u,pms,p,iv,c,bl) ->
        let (acc, pms') = fold_arr m acc pms in
        let (acc, p') = fold_ctx m acc p in
diff --git a/src/plugin/g_hammer.mlg b/src/plugin/g_hammer.mlg
index 508d8ef..97d7bdd 100644
--- a/src/plugin/g_hammer.mlg
+++ b/src/plugin/g_hammer.mlg
@@ -6,7 +6,7 @@ open Ltac_plugin
 open Stdarg
 open Tacarg
 
-let hammer_version_string = "CoqHammer 1.3.2 for Coq 8.16"
+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))
More details

Full run details
The Debian Janitor

New Upstream Release - coq-hammer

Ready changes

Summary

Diff

More details

Historical runs
