From 029d33c7c2c82fcce9e91ba73172530ef24010e3 Mon Sep 17 00:00:00 2001
From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
Date: Fri, 24 Nov 2023 18:09:41 +0100
Subject: [PATCH] Opam: added patch for coq-itauto.8.18.0

---
 ...une-calls-does-not-work-on-Windows-M.patch | 25 ++++++++++
 .../coq-itauto/coq-itauto.8.18.0/opam         | 50 +++++++++++++++++++
 2 files changed, 75 insertions(+)
 create mode 100644 opam/opam-coq-archive/released/packages/coq-itauto/coq-itauto.8.18.0/files/0001-Remove-root-on-dune-calls-does-not-work-on-Windows-M.patch
 create mode 100755 opam/opam-coq-archive/released/packages/coq-itauto/coq-itauto.8.18.0/opam

diff --git a/opam/opam-coq-archive/released/packages/coq-itauto/coq-itauto.8.18.0/files/0001-Remove-root-on-dune-calls-does-not-work-on-Windows-M.patch b/opam/opam-coq-archive/released/packages/coq-itauto/coq-itauto.8.18.0/files/0001-Remove-root-on-dune-calls-does-not-work-on-Windows-M.patch
new file mode 100644
index 0000000000..2ffe2e51ef
--- /dev/null
+++ b/opam/opam-coq-archive/released/packages/coq-itauto/coq-itauto.8.18.0/files/0001-Remove-root-on-dune-calls-does-not-work-on-Windows-M.patch
@@ -0,0 +1,25 @@
+From 828e973c631eeb4875ca94fb1a4d1bfb7ebc7866 Mon Sep 17 00:00:00 2001
+From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
+Date: Fri, 24 Nov 2023 17:57:28 +0100
+Subject: [PATCH] Remove --root on dune calls - does not work on Windows MinGW
+ cygwin cross
+
+---
+ src/patch/Makefile | 4 ++--
+ 1 file changed, 2 insertions(+), 2 deletions(-)
+
+diff --git a/src/patch/Makefile b/src/patch/Makefile
+index 6b347bd..d3ba762 100644
+--- a/src/patch/Makefile
++++ b/src/patch/Makefile
+@@ -1,5 +1,5 @@
+ mlpatch : lexer.mll parser.mly patch.ml mlpatch.ml
+-	dune build --root $(CURDIR)
++	dune build
+ 
+ clean :
+-	dune clean --root $(CURDIR)
++	dune clean
+-- 
+2.37.3
+
diff --git a/opam/opam-coq-archive/released/packages/coq-itauto/coq-itauto.8.18.0/opam b/opam/opam-coq-archive/released/packages/coq-itauto/coq-itauto.8.18.0/opam
new file mode 100755
index 0000000000..a472b734d4
--- /dev/null
+++ b/opam/opam-coq-archive/released/packages/coq-itauto/coq-itauto.8.18.0/opam
@@ -0,0 +1,50 @@
+opam-version: "2.0"
+maintainer: "frederic.besson@inria.fr"
+homepage: "https://gitlab.inria.fr/fbesson/itauto"
+dev-repo: "git+https://gitlab.inria.fr/fbesson/itauto.git"
+authors: ["Frédéric Besson"]
+bug-reports: ["frederic.besson@inria.fr" "https://gitlab.inria.fr/fbesson/itauto/-/issues"]
+license: "MIT"
+synopsis: "Reflexive SAT solver with Nelson-Oppen support, parameterised by a leaf tactic inside Coq"
+description: """
+itauto is a reflexive intuitionistic SAT solver parameterised by a theory module.
+When run inside Coq, the theory module wraps an arbitrary Coq tactic, e.g., the lia
+solver for linear arithmetic or the congruence solver for uninterpreted function symbols
+and constructors. Using a black-box Nelson-Oppen scheme for combination of theories,
+itauto also provides an SMT-like tactic for propositional reasoning modulo the solvers for
+both arithmetic and function symbols.
+"""
+
+build: [
+  [make "-j%{jobs}%"]
+ ]
+patches: [
+  "0001-Remove-root-on-dune-calls-does-not-work-on-Windows-M.patch"
+]
+install: [make "install"]
+depends: [
+  "ocaml" {>= "4.9~"}
+  "coq" {>= "8.18" & < "8.19"}
+  "dune" {>= "2.9"}
+]
+depopts: [ "ocamlformat" {build} ]
+
+tags: [
+  "category:Miscellaneous/Coq Extensions"
+  "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures"
+  "keyword:integers"
+  "keyword:SAT"
+  "keyword:SMT"
+  "keyword:Nelson-Oppen"
+  "keyword:automation"
+  "logpath:Cdcl"
+  "date:2023-08-16"
+]
+
+url {
+  src: "https://gitlab.inria.fr/fbesson/itauto/-/archive/8.18.0/itauto-8.18.0.tar.gz"
+  checksum: [
+    "md5=0f8f644252ea4eac5139672a2bc500fb"
+    "sha512=a6912de70f2bb0118f352b5190b171dc863f4d50733b1881b1382afd1b9dcbad85971feb0d2d3b64deceb13d5b91ce78d1d5b445c745ced03ea0cf0b7b15c177"
+  ]
+}