diff --git a/packages/coqide/coqide.8.19.0/opam b/packages/coqide/coqide.8.19.0/opam
new file mode 100644
index 00000000000..1687d009f9d
--- /dev/null
+++ b/packages/coqide/coqide.8.19.0/opam
@@ -0,0 +1,51 @@
+opam-version: "2.0"
+synopsis: "The Coq Proof Assistant --- GTK3 IDE"
+description: """
+Coq is a formal proof management system. It provides
+a formal language to write mathematical definitions, executable
+algorithms and theorems together with an environment for
+semi-interactive development of machine-checked proofs.
+
+This package provides the CoqIDE, a graphical user interface for the
+development of interactive proofs."""
+maintainer: ["The Coq development team <coqdev@inria.fr>"]
+authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+license: "LGPL-2.1-only"
+homepage: "https://coq.inria.fr/"
+doc: "https://coq.github.io/doc/"
+bug-reports: "https://github.com/coq/coq/issues"
+depends: [
+  "dune" {>= "2.9"}
+  "ocamlfind" {build}
+  "conf-findutils" {build}
+  "conf-adwaita-icon-theme"
+  "coqide-server" {= version}
+  "cairo2" {>= "0.6.4"}
+  "lablgtk3-sourceview3" {>= "3.1.2"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
+dev-repo: "git+https://github.com/coq/coq.git"
+
+url {
+  src: "https://github.com/coq/coq/releases/download/V8.19.0/coq-8.19.0.tar.gz"
+  checksum: [
+    "md5=64b49dbc3205477bd7517642c0b9cbb6"
+    "sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b"
+  ]
+}